---

Step * of Lemma term-to-path-wf

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[u,v:{X ⊢ _:A}].
  ∀a:{X.𝕀 ⊢ _:(A)p}. (<>(a) ∈ {X ⊢ _:(Path_A u v)}) supposing (X ⊢ (a)[0(𝕀)]=u:A and X ⊢ (a)[1(𝕀)]=v:A)
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[u,v:\{X  \mvdash{}  \_:A\}].
    \mforall{}a:\{X.\mBbbI{}  \mvdash{}  \_:(A)p\}
        (<>(a)  \mmember{}  \{X  \mvdash{}  \_:(Path\_A  u  v)\})  supposing  (X  \mvdash{}  (a)[0(\mBbbI{})]=u:A  and  X  \mvdash{}  (a)[1(\mBbbI{})]=v:A)


By

---

Latex:
Auto

---

Home Index