---

Step * of Lemma cubical-path-app_wf

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[t:{X ⊢ _:(Path_A a b)}]. ∀[r:{X ⊢ _:𝕀}].  (t @ r ∈ {X ⊢ _:A})
BY
{ ProveWfLemma }

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index