---

Step * of Lemma csm-pathtype

No Annotations
∀X,Delta:j⊢. ∀s:Delta j⟶ X. ∀A:{X ⊢ _}.  ((Path(A))s = Path((A)s) ∈ {Delta ⊢ _})
BY
{ (Auto THEN RepUR ``pathtype`` 0 THEN RWO "csm-cubical-fun" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X,Delta:j\mvdash{}.  \mforall{}s:Delta  j{}\mrightarrow{}  X.  \mforall{}A:\{X  \mvdash{}  \_\}.    ((Path(A))s  =  Path((A)s))


By

---

Latex:
(Auto  THEN  RepUR  ``pathtype``  0  THEN  RWO  "csm-cubical-fun"  0  THEN  Auto)

---

Home Index