---

Step * 1 of Lemma csm-equiv_path


1. G : CubicalSet{j}
2. A : {G ⊢ _:c𝕌}
3. B : {G ⊢ _:c𝕌}
4. f : {G ⊢ _:Equiv(decode(A);decode(B))}
5. H : CubicalSet{j}
6. s : H j⟶ G
7. ∀[A,B:{G ⊢ _}]. ∀[cA:G +⊢ Compositon(A)]. ∀[cB:G +⊢ Compositon(B)]. ∀[f:{G ⊢ _:Equiv(A;B)}].
     (equiv-path2(G;A;B;cA;cB;f) ∈ G.𝕀 +⊢ Compositon(equiv-path1(G;A;B;f)))
8. equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f) ∈ G.𝕀 +⊢ Compositon(equiv-path1(G;decode(A);decode(B);f))
9. ∀[T:{G.𝕀 ⊢ _}]. ∀[cT:G.𝕀 ⊢ CompOp(T)]. ∀[H:j⊢]. ∀[s:H j⟶ G.𝕀].  ((encode(T;cT))s = encode((T)s;(cT)s) ∈ {H ⊢ _:c𝕌})
10. (encode(equiv-path1(G;decode(A);decode(B);f);cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f)
                                                     ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))))s+
= encode((equiv-path1(G;decode(A);decode(B);f))s+;(cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f)
                                                       ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f)))s+)
∈ {H.𝕀 ⊢ _:c𝕌}
⊢ (encode(equiv-path1(G;decode(A);decode(B);f);cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f)
                                                   ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))))s+
= encode(equiv-path1(H;decode((A)s);decode((B)s);(f)s);
         cfun-to-cop(H.𝕀;equiv-path1(H;decode((A)s);decode((B)s);(f)s)
             ;equiv-path2(H;decode((A)s);decode((B)s);CompFun((A)s);CompFun((B)s);(f)s)))
∈ {H.𝕀 ⊢ _:c𝕌}
BY
{ (Assert ⌜encode((equiv-path1(G;decode(A);decode(B);f))s+;
                  (cfun-to-cop(G.𝕀;equiv-path1(G;decode(A);decode(B);f)
                       ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f)))s+)
           = encode(equiv-path1(H;decode((A)s);decode((B)s);(f)s);
                    cfun-to-cop(H.𝕀;equiv-path1(H;decode((A)s);decode((B)s);(f)s)
                        ;equiv-path2(H;decode((A)s);decode((B)s);CompFun((A)s);CompFun((B)s);(f)s)))
           ∈ {H.𝕀 ⊢ _:c𝕌}⌝⋅
THENM Eq
) }

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

---

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.  H  :  CubicalSet\{j\}
6.  s  :  H  j{}\mrightarrow{}  G
7.  \mforall{}[A,B:\{G  \mvdash{}  \_\}].  \mforall{}[cA:G  +\mvdash{}  Compositon(A)].  \mforall{}[cB:G  +\mvdash{}  Compositon(B)].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(A;B)\}].
          (equiv-path2(G;A;B;cA;cB;f)  \mmember{}  G.\mBbbI{}  +\mvdash{}  Compositon(equiv-path1(G;A;B;f)))
8.  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))
9.  \mforall{}[T:\{G.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cT:G.\mBbbI{}  \mvdash{}  CompOp(T)].  \mforall{}[H:j\mvdash{}].  \mforall{}[s:H  j{}\mrightarrow{}  G.\mBbbI{}].
          ((encode(T;cT))s  =  encode((T)s;(cT)s))
10.  (encode(equiv-path1(G;decode(A);decode(B);f);
                        cfun-to-cop(G.\mBbbI{};equiv-path1(G;decode(A);decode(B);f)
                                ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))))s+
=  encode((equiv-path1(G;decode(A);decode(B);f))s+;
                  (cfun-to-cop(G.\mBbbI{};equiv-path1(G;decode(A);decode(B);f)
                            ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f)))s+)
\mvdash{}  (encode(equiv-path1(G;decode(A);decode(B);f);
                    cfun-to-cop(G.\mBbbI{};equiv-path1(G;decode(A);decode(B);f)
                            ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f))))s+
=  encode(equiv-path1(H;decode((A)s);decode((B)s);(f)s);
                  cfun-to-cop(H.\mBbbI{};equiv-path1(H;decode((A)s);decode((B)s);(f)s)
                          ;equiv-path2(H;decode((A)s);decode((B)s);CompFun((A)s);CompFun((B)s);(f)s)))


By

---

Latex:
(Assert  \mkleeneopen{}encode((equiv-path1(G;decode(A);decode(B);f))s+;
                                (cfun-to-cop(G.\mBbbI{};equiv-path1(G;decode(A);decode(B);f)
                                          ;equiv-path2(G;decode(A);decode(B);CompFun(A);CompFun(B);f)))s+)
                  =  encode(equiv-path1(H;decode((A)s);decode((B)s);(f)s);
                                    cfun-to-cop(H.\mBbbI{};equiv-path1(H;decode((A)s);decode((B)s);(f)s)
                                            ;equiv-path2(H;decode((A)s);decode((B)s);CompFun((A)s);CompFun((B)s);(f)s)))\mkleeneclose{}\mcdot{}
THENM  Eq
)

---

Home Index