---

Step * 2 1 of Lemma csm-equiv-path2


1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. cA : G +⊢ Compositon(A)
5. cB : G +⊢ Compositon(B)
6. f : {G ⊢ _:Equiv(A;B)}
7. H : CubicalSet{j}
8. s : H j⟶ G
9. G.𝕀, ((q=0) ∨ (q=1)) ⊢ (if (q=0) then (A)p else (B)p)
10. ∀[A:{G.𝕀 ⊢ _}]. ∀[psi:{G.𝕀 ⊢ _:𝔽}]. ∀[T:{G.𝕀, psi ⊢ _}]. ∀[cA,cT,f,tau:Top].
      ((comp(Glue [psi ⊢→ (T, f)] A) )tau ~ comp(Glue [(psi)tau ⊢→ ((T)tau, (f)tau)] (A)tau) )
⊢ comp(Glue [((q=0) ∨ (q=1)) ⊢→ ((if ((q=0))s+ then ((A)s)p else ((B)s)p), (cubical-equiv-by-cases(G;B;f))s+)] ((B)s)p) 
= equiv-path2(H;(A)s;(B)s;(cA)s;(cB)s;(f)s)
∈ H.𝕀 +⊢ Compositon(equiv-path1(H;(A)s;(B)s;(f)s))
BY
{ (Subst' (case-type-comp(G.𝕀; (q=0); (q=1); (A)p; (B)p; (cA)p; (cB)p))s+ ~ case-type-comp(H.𝕀;
                                                                                           (q=0);
                                                                                           (q=1);
                                                                                           ((A)s)p;
                                                                                           ((B)s)p;
                                                                                           ((cA)s)p;
                                                                                           ((cB)s)p) 0
   THENA ((RWO "csm-case-type-comp" 0 THENA Auto)
          THEN (EqCD THEN (RWW  "csm-face-zero csm-face-one" 0 THENA Auto))
          THEN CsmUnfoldingComp
          THEN Trivial)
   ) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. cA : G +⊢ Compositon(A)
5. cB : G +⊢ Compositon(B)
6. f : {G ⊢ _:Equiv(A;B)}
7. H : CubicalSet{j}
8. s : H j⟶ G
9. G.𝕀, ((q=0) ∨ (q=1)) ⊢ (if (q=0) then (A)p else (B)p)
10. ∀[A:{G.𝕀 ⊢ _}]. ∀[psi:{G.𝕀 ⊢ _:𝔽}]. ∀[T:{G.𝕀, psi ⊢ _}]. ∀[cA,cT,f,tau:Top].
      ((comp(Glue [psi ⊢→ (T, f)] A) )tau ~ comp(Glue [(psi)tau ⊢→ ((T)tau, (f)tau)] (A)tau) )
⊢ comp(Glue [((q=0) ∨ (q=1)) ⊢→ ((if ((q=0))s+ then ((A)s)p else ((B)s)p), (cubical-equiv-by-cases(G;B;f))s+)] ((B)s)p) 
= equiv-path2(H;(A)s;(B)s;(cA)s;(cB)s;(f)s)
∈ H.𝕀 +⊢ Compositon(equiv-path1(H;(A)s;(B)s;(f)s))

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_\}
3.  B  :  \{G  \mvdash{}  \_\}
4.  cA  :  G  +\mvdash{}  Compositon(A)
5.  cB  :  G  +\mvdash{}  Compositon(B)
6.  f  :  \{G  \mvdash{}  \_:Equiv(A;B)\}
7.  H  :  CubicalSet\{j\}
8.  s  :  H  j{}\mrightarrow{}  G
9.  G.\mBbbI{},  ((q=0)  \mvee{}  (q=1))  \mvdash{}  (if  (q=0)  then  (A)p  else  (B)p)
10.  \mforall{}[A:\{G.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[psi:\{G.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[T:\{G.\mBbbI{},  psi  \mvdash{}  \_\}].  \mforall{}[cA,cT,f,tau:Top].
            ((comp(Glue  [psi  \mvdash{}\mrightarrow{}  (T,  f)]  A)  )tau  \msim{}  comp(Glue  [(psi)tau  \mvdash{}\mrightarrow{}  ((T)tau,  (f)tau)]  (A)tau)  )
\mvdash{}  comp(Glue  [((q=0)  \mvee{}  (q=1))  \mvdash{}\mrightarrow{}  ((if  ((q=0))s+  then  ((A)s)p  else  ((B)s)p),
                                                                  (cubical-equiv-by-cases(G;B;f))s+)]  ((B)s)p) 
=  equiv-path2(H;(A)s;(B)s;(cA)s;(cB)s;(f)s)


By

---

Latex:
(Subst'  (case-type-comp(G.\mBbbI{};  (q=0);  (q=1);  (A)p;  (B)p;  (cA)p;  (cB)p))s+  \msim{}  case-type-comp(H.\mBbbI{};
                                                                                                                                                                                  (q=0);
                                                                                                                                                                                  (q=1);
                                                                                                                                                                                  ((A)s)p;
                                                                                                                                                                                  ((B)s)p;
                                                                                                                                                                                  ((cA)s)p;
                                                                                                                                                                                  ((cB)s)p)  0
  THENA  ((RWO  "csm-case-type-comp"  0  THENA  Auto)
                THEN  (EqCD  THEN  (RWW    "csm-face-zero  csm-face-one"  0  THENA  Auto))
                THEN  CsmUnfoldingComp
                THEN  Trivial)
  )

---

Home Index