---

Step * of Lemma equal-paths-eta

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[p,q:{X ⊢ _:Path(A)}].
  p = q ∈ {X ⊢ _:Path(A)} supposing path-eta(p) = path-eta(q) ∈ {X.𝕀 ⊢ _:(A)p}
BY
{ Intros }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. p : {X ⊢ _:Path(A)}
4. q : {X ⊢ _:Path(A)}
5. path-eta(p) = path-eta(q) ∈ {X.𝕀 ⊢ _:(A)p}
⊢ p = q ∈ {X ⊢ _:Path(A)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[p,q:\{X  \mvdash{}  \_:Path(A)\}].    p  =  q  supposing  path-eta(p)  =  path-eta(q)


By

---

Latex:
Intros

---

Home Index