---

Step * of Lemma equiv_path-1

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[f:{G ⊢ _:Equiv(decode(A);decode(B))}].  G ⊢ (equiv_path(G;A;B;f))[1(𝕀)]=B:c𝕌
BY
{ (Intros⋅
   THEN Unfold `same-cubical-term` 0
   THEN Unfold `equiv_path` 0
   THEN (InstLemma  `equiv-path2_wf` [⌜G⌝;⌜decode(A)⌝;⌜decode(B)⌝]⋅ THENA Auto)
   THEN (InstHyp [⌜CompFun(A)⌝;⌜CompFun(B)⌝;⌜f⌝] (-1)⋅ THENA Auto)
   THEN (GenConclTerm ⌜equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f)⌝⋅ THENA Auto)
   THEN RenameVar `C' (-2)
   THEN RepUR ``let`` 0
   THEN (InstLemma `comp-fun-to-comp-op_wf` [⌜G.𝕀⌝;⌜equiv-path1(G;decode(A);decode(B);f)⌝;⌜C⌝]⋅ THENA Auto)
   THEN (InstLemma `csm-universe-encode` [⌜G.𝕀⌝;⌜equiv-path1(G;decode(A);decode(B);f)⌝;
         ⌜cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f);C)⌝;⌜G⌝;⌜[1(𝕀)]⌝]⋅
         THENA Auto
         )
   THEN Fold `same-cubical-term` 0
   THEN (HypSubst'  (-1) 0 THENA (Auto THEN SubsumeC ⌜{G ⊢' _}⌝⋅ THEN Auto))) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. ∀[cA:G +⊢ Compositon(decode(A))]. ∀[cB:G +⊢ Compositon(decode(B))]. ∀[f:{G ⊢ _:Equiv(decode(A);decode(B))}].
     (equiv-path2(G;decode(A);decode(B);cA;cB;f) ∈ G.𝕀 +⊢ Compositon(equiv-path1(G;decode(A);decode(B);f)))
6. equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f) ∈ G.𝕀 +⊢ Compositon(equiv-path1(G;decode(A);decode(B);f))
7. C : G.𝕀 +⊢ Compositon(equiv-path1(G;decode(A);decode(B);f))
8. equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f)
= C
∈ G.𝕀 +⊢ Compositon(equiv-path1(G;decode(A);decode(B);f))
9. cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f);C) ∈ G.𝕀 ⊢ CompOp(equiv-path1(G;decode(A);decode(B);f))
10. (encode(equiv-path1(G;decode(A);decode(B);f);cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f);C)))[1(𝕀)]
= encode((equiv-path1(G;decode(A);decode(B);f))[1(𝕀)];(cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f);C))[1(𝕀)])
∈ {G ⊢ _:c𝕌}
⊢ G ⊢ encode((equiv-path1(G;decode(A);decode(B);f))[1(𝕀)];(cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f)
                                                               ;C))[1(𝕀)])=B:c𝕌

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(decode(A);decode(B))\}].
    G  \mvdash{}  (equiv\_path(G;A;B;f))[1(\mBbbI{})]=B:c\mBbbU{}


By

---

Latex:
(Intros\mcdot{}
  THEN  Unfold  `same-cubical-term`  0
  THEN  Unfold  `equiv\_path`  0
  THEN  (InstLemma    `equiv-path2\_wf`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}decode(A)\mkleeneclose{};\mkleeneopen{}decode(B)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}CompFun(A)\mkleeneclose{};\mkleeneopen{}CompFun(B)\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RenameVar  `C'  (-2)
  THEN  RepUR  ``let``  0
  THEN  (InstLemma  `comp-fun-to-comp-op\_wf`  [\mkleeneopen{}G.\mBbbI{}\mkleeneclose{};\mkleeneopen{}equiv-path1(G;decode(A);decode(B);f)\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (InstLemma  `csm-universe-encode`  [\mkleeneopen{}G.\mBbbI{}\mkleeneclose{};\mkleeneopen{}equiv-path1(G;decode(A);decode(B);f)\mkleeneclose{};
              \mkleeneopen{}cfun-to-cop(G.\mBbbI{};equiv-path1(G;decode(A);decode(B);f);C)\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}[1(\mBbbI{})]\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Fold  `same-cubical-term`  0
  THEN  (HypSubst'    (-1)  0  THENA  (Auto  THEN  SubsumeC  \mkleeneopen{}\{G  \mvdash{}'  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index