---

Step * of Lemma cubical-subst_wf

No Annotations
∀[G:j⊢]. ∀[A:{G ⊢' _}]. ∀[a,b:{G ⊢ _:A}]. ∀[p:{G ⊢ _:(Path_A a b)}]. ∀[f:{G ⊢ _:(A ⟶ c𝕌)}].
∀[x:{G ⊢ _:decode(app(f; a))}].
  (cubical-subst(G;f;p;x) ∈ {G ⊢ _:decode(app(f; b))})
BY
{ (RepeatFor 6 (Intro⋅)
   THEN (InstLemma `cubical-app_wf_fun` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜A⌝;⌜c𝕌⌝;⌜f⌝;⌜a⌝]⋅ THENA Auto)
   THEN (InstLemma `cubical-app_wf_fun` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G⌝;⌜A⌝;⌜c𝕌⌝;⌜f⌝;⌜b⌝]⋅ THENA Auto)
   THEN Intro⋅
   THEN (Assert map-path(G;f;p) ∈ {G ⊢ _:(Path_c𝕌 app(f; a) app(f; b))} BY
               (InstLemma `map-path_wf` [⌜parm{j}⌝;⌜parm{i'}⌝]⋅ THEN BHyp -1 THEN Auto))
   THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A:\{G  \mvdash{}'  \_\}].  \mforall{}[a,b:\{G  \mvdash{}  \_:A\}].  \mforall{}[p:\{G  \mvdash{}  \_:(Path\_A  a  b)\}].  \mforall{}[f:\{G  \mvdash{}  \_:(A  {}\mrightarrow{}  c\mBbbU{})\}].
\mforall{}[x:\{G  \mvdash{}  \_:decode(app(f;  a))\}].
    (cubical-subst(G;f;p;x)  \mmember{}  \{G  \mvdash{}  \_:decode(app(f;  b))\})


By

---

Latex:
(RepeatFor  6  (Intro\mcdot{})
  THEN  (InstLemma  `cubical-app\_wf\_fun`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `cubical-app\_wf\_fun`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Intro\mcdot{}
  THEN  (Assert  map-path(G;f;p)  \mmember{}  \{G  \mvdash{}  \_:(Path\_c\mBbbU{}  app(f;  a)  app(f;  b))\}  BY
                          (InstLemma  `map-path\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}  THEN  BHyp  -1  THEN  Auto))
  THEN  ProveWfLemma)

---

Home Index