---

Step * of Lemma path-point_wf

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[pth:{X ⊢ _:(Path_A a b)}].  (path-point(pth) ∈ {X.𝕀 ⊢ _:(A)p})
BY
{ (Auto
   THEN Unfold `path-point` 0
   THEN InstLemma `cubical-path-app_wf` [X.𝕀;⌜(A)p⌝;⌜(a)p⌝;⌜(b)p⌝;⌜(pth)p⌝;⌜q⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[pth:\{X  \mvdash{}  \_:(Path\_A  a  b)\}].
    (path-point(pth)  \mmember{}  \{X.\mBbbI{}  \mvdash{}  \_:(A)p\})


By

---

Latex:
(Auto
  THEN  Unfold  `path-point`  0
  THEN  InstLemma  `cubical-path-app\_wf`  [X.\mBbbI{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}(a)p\mkleeneclose{};\mkleeneopen{}(b)p\mkleeneclose{};\mkleeneopen{}(pth)p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index