---

Step * of Lemma path-type-p

No Annotations
∀[X:j⊢]. ∀[A,B:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}].  ((X.B ⊢ Path_(A)p (a)p (b)p) = ((Path_A a b))p ∈ {X.B ⊢ _})
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A,B:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].    ((X.B  \mvdash{}  Path\_(A)p  (a)p  (b)p)  =  ((Path\_A  a  b))p)


By

---

Latex:
Auto

---

Home Index