---

Step * 1 of Lemma equiv_path-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𝕌
BY
{ ((InstLemma `universe-encode-decode` [⌜G⌝;⌜B⌝]⋅ THENA Auto)
   THEN Fold `same-cubical-term` (-1)
   THEN NthHypEqGen (-1)
   THEN (EqCDA THENL [(SubsumeC ⌜{G ⊢' _}⌝⋅ THEN Auto); (EqCDA THENL [Auto; Id])])) }

1
.....subterm..... T:t
3:n
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𝕌}
11. G ⊢ encode(decode(B);compOp(B))=B:c𝕌
⊢ (cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f);C))[1(𝕀)]
= compOp(B)
∈ G ⊢ CompOp((equiv-path1(G;decode(A);decode(B);f))[1(𝕀)])

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `universe-encode-decode`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `same-cubical-term`  (-1)
  THEN  NthHypEqGen  (-1)
  THEN  (EqCDA  THENL  [(SubsumeC  \mkleeneopen{}\{G  \mvdash{}'  \_\}\mkleeneclose{}\mcdot{}  THEN  Auto);  (EqCDA  THENL  [Auto;  Id])]))

---

Home Index