---

Step * of Lemma unit-path-type

No Annotations
∀[G:j⊢]. ∀[x,y:{G ⊢ _:1}].  ∀a,b:{G ⊢ _:(Path_1 x y)}.  (a = b ∈ {G ⊢ _:(Path_1 x y)})
BY
{ (Auto THEN BLemma `paths-equal` THEN Auto) }

1
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)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[x,y:\{G  \mvdash{}  \_:1\}].    \mforall{}a,b:\{G  \mvdash{}  \_:(Path\_1  x  y)\}.    (a  =  b)


By

---

Latex:
(Auto  THEN  BLemma  `paths-equal`  THEN  Auto)

---

Home Index