---

Step * of Lemma equiv-path_wf

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[f:{G ⊢ _:Equiv(decode(A);decode(B))}].  (EquivPath(G;A;B;f) ∈ {G ⊢ _:(Path_c𝕌 A B)})
BY
{ (Intros⋅
   THEN Unfold `equiv-path` 0
   THEN (InstLemma `term-to-path-wf` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜c𝕌⌝;⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN (RWO "csm-cubical-universe" (-1) THENA Auto)
   THEN Unhide
   THEN BHyp -1
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(decode(A);decode(B))\}].
    (EquivPath(G;A;B;f)  \mmember{}  \{G  \mvdash{}  \_:(Path\_c\mBbbU{}  A  B)\})


By

---

Latex:
(Intros\mcdot{}
  THEN  Unfold  `equiv-path`  0
  THEN  (InstLemma  `term-to-path-wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "csm-cubical-universe"  (-1)  THENA  Auto)
  THEN  Unhide
  THEN  BHyp  -1
  THEN  Auto)

---

Home Index