---

Step * of Lemma cubicalpath-app_wf

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[t:{X ⊢ _:Path(A)}]. ∀[r:{X ⊢ _:𝕀}].  (t @ r ∈ {X ⊢ _:A})
BY
{ (Unfold `pathtype` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[t:\{X  \mvdash{}  \_:Path(A)\}].  \mforall{}[r:\{X  \mvdash{}  \_:\mBbbI{}\}].    (t  @  r  \mmember{}  \{X  \mvdash{}  \_:A\})


By

---

Latex:
(Unfold  `pathtype`  0  THEN  ProveWfLemma)

---

Home Index