---

Step * 2 of Lemma partial-term-1_wf


1. [H] : CubicalSet{j}
2. [A] : {H.𝕀 ⊢ _}
3. [phi] : {H ⊢ _:𝔽}
4. [u] : {H.𝕀, (phi)p ⊢ _:A}
5. ((phi)p)[1(𝕀)] ∈ {H ⊢ _:𝔽}
⊢ u[1] ∈ {H, phi ⊢ _:(A)[1(𝕀)]}
BY
{ (Unfold `partial-term-1` 0
   THEN (InstLemma `context-subset-map` [⌜H.𝕀⌝;⌜(phi)p⌝;⌜H⌝;⌜[1(𝕀)]⌝]⋅ THENA Auto)
   THEN InferEqualType) }

1
1. H : CubicalSet{j}
2. A : {H.𝕀 ⊢ _}
3. phi : {H ⊢ _:𝔽}
4. u : {H.𝕀, (phi)p ⊢ _:A}
5. ((phi)p)[1(𝕀)] ∈ {H ⊢ _:𝔽}
6. [1(𝕀)] ∈ H, ((phi)p)[1(𝕀)] j⟶ H.𝕀, (phi)p
⊢ {H, ((phi)p)[1(𝕀)] ⊢ _:(A)[1(𝕀)]} = {H, phi ⊢ _:(A)[1(𝕀)]} ∈ 𝕌{[i | j']}

2
1. H : CubicalSet{j}
2. A : {H.𝕀 ⊢ _}
3. phi : {H ⊢ _:𝔽}
4. u : {H.𝕀, (phi)p ⊢ _:A}
5. ((phi)p)[1(𝕀)] ∈ {H ⊢ _:𝔽}
6. [1(𝕀)] ∈ H, ((phi)p)[1(𝕀)] j⟶ H.𝕀, (phi)p
7. {H, ((phi)p)[1(𝕀)] ⊢ _:(A)[1(𝕀)]} = {H, phi ⊢ _:(A)[1(𝕀)]} ∈ 𝕌{[i | j']}
⊢ (u)[1(𝕀)] ∈ {H, ((phi)p)[1(𝕀)] ⊢ _:(A)[1(𝕀)]}

---

Latex:

---

Latex:

1.  [H]  :  CubicalSet\{j\}
2.  [A]  :  \{H.\mBbbI{}  \mvdash{}  \_\}
3.  [phi]  :  \{H  \mvdash{}  \_:\mBbbF{}\}
4.  [u]  :  \{H.\mBbbI{},  (phi)p  \mvdash{}  \_:A\}
5.  ((phi)p)[1(\mBbbI{})]  \mmember{}  \{H  \mvdash{}  \_:\mBbbF{}\}
\mvdash{}  u[1]  \mmember{}  \{H,  phi  \mvdash{}  \_:(A)[1(\mBbbI{})]\}


By

---

Latex:
(Unfold  `partial-term-1`  0
  THEN  (InstLemma  `context-subset-map`  [\mkleeneopen{}H.\mBbbI{}\mkleeneclose{};\mkleeneopen{}(phi)p\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}[1(\mBbbI{})]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InferEqualType)

---

Home Index