---

Step * of Lemma unit-pathtype

No Annotations
∀[G:j⊢]. ∀a,b:{G ⊢ _:Path(1)}.  (a = b ∈ {G ⊢ _:Path(1)})
BY
{ (Auto THEN CubicalTermEqual THEN Auto) }

1
1. G : CubicalSet{j}
2. a : {G ⊢ _:Path(1)}
3. b : {G ⊢ _:Path(1)}
4. I : fset(ℕ)
5. a1 : G(I)
⊢ (a I a1) = (b I a1) ∈ Path(1)(a1)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  CubicalTermEqual  THEN  Auto)

---

Home Index