---

Step * 1 of Lemma unit-path-type


1. G : CubicalSet{j}
2. x : {G ⊢ _:1}
3. y : {G ⊢ _:1}
4. a : {G ⊢ _:(Path_1 x y)}
5. b : {G ⊢ _:(Path_1 x y)}
⊢ a = b ∈ {G ⊢ _:Path(1)}
BY
{ (BLemma `unit-pathtype` THEN Auto) }

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  x  :  \{G  \mvdash{}  \_:1\}
3.  y  :  \{G  \mvdash{}  \_:1\}
4.  a  :  \{G  \mvdash{}  \_:(Path\_1  x  y)\}
5.  b  :  \{G  \mvdash{}  \_:(Path\_1  x  y)\}
\mvdash{}  a  =  b


By

---

Latex:
(BLemma  `unit-pathtype`  THEN  Auto)

---

Home Index