---

Step * of Lemma csm-path-type-id-adjoin

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index