---

Step * 1 of Lemma term-to-path-equal


1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. u : {X ⊢ _:A}
4. v : {X ⊢ _:A}
5. a : {X.𝕀 ⊢ _:(A)p}
6. X ⊢ (a)[1(𝕀)]=v:A
7. X ⊢ (a)[0(𝕀)]=u:A
8. <>(a) ∈ {X ⊢ _:(Path_A u v)}
⊢ ∀[b:{X.𝕀 ⊢ _:(A)p}]. X ⊢ <>(a) = X ⊢ <>(b) ∈ {X ⊢ _:(Path_A u v)} supposing a = b ∈ {X.𝕀 ⊢ _:(A)p}
BY
{ Intros }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. u : {X ⊢ _:A}
4. v : {X ⊢ _:A}
5. a : {X.𝕀 ⊢ _:(A)p}
6. X ⊢ (a)[1(𝕀)]=v:A
7. X ⊢ (a)[0(𝕀)]=u:A
8. <>(a) ∈ {X ⊢ _:(Path_A u v)}
9. b : {X.𝕀 ⊢ _:(A)p}
10. a = b ∈ {X.𝕀 ⊢ _:(A)p}
⊢ X ⊢ <>(a) = X ⊢ <>(b) ∈ {X ⊢ _:(Path_A u v)}

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  u  :  \{X  \mvdash{}  \_:A\}
4.  v  :  \{X  \mvdash{}  \_:A\}
5.  a  :  \{X.\mBbbI{}  \mvdash{}  \_:(A)p\}
6.  X  \mvdash{}  (a)[1(\mBbbI{})]=v:A
7.  X  \mvdash{}  (a)[0(\mBbbI{})]=u:A
8.  <>(a)  \mmember{}  \{X  \mvdash{}  \_:(Path\_A  u  v)\}
\mvdash{}  \mforall{}[b:\{X.\mBbbI{}  \mvdash{}  \_:(A)p\}].  X  \mvdash{}  <>(a)  =  X  \mvdash{}  <>(b)  supposing  a  =  b


By

---

Latex:
Intros

---

Home Index