---

Step * 1 1 of Lemma csm-equiv-path1

.....assertion..... 
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. f : {G ⊢ _:Equiv(A;B)}
5. H : CubicalSet{j}
6. s : H j⟶ G
7. ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (A)p
8. ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (B)p
9. ∀phi:{H.𝕀 ⊢ _:𝔽}. H.𝕀, phi ⊢ ((A)s)p
10. ∀phi:{H.𝕀 ⊢ _:𝔽}. H.𝕀, phi ⊢ ((B)s)p
11. (Glue [((q=0) ∨ (q=1)) ⊢→ ((if (q=0) then (A)p else (B)p);equiv-fun(cubical-equiv-by-cases(G;B;f)))] (B)p)s+
= H.𝕀 ⊢ Glue [(((q=0) ∨ (q=1)))s+ ⊢→ (((if (q=0) then (A)p else (B)p))
                                       s+;(equiv-fun(cubical-equiv-by-cases(G;B;f)))s+)] ((B)p)s+
∈ {H.𝕀 ⊢ _}
⊢ H.𝕀 ⊢ Glue [(((q=0) ∨ (q=1)))s+ ⊢→ (((if (q=0) then (A)p else (B)p))
                                       s+;(equiv-fun(cubical-equiv-by-cases(G;B;f)))s+)] ((B)p)s+
= H.𝕀 ⊢ Glue [((q=0) ∨ (q=1)) ⊢→ ((if (q=0) then ((A)s)p else ((B)s)
                                                               p);equiv-fun(cubical-equiv-by-cases(H;(B)s;(f)s)))] ((B)
                                                                                                                     s)p
∈ {H.𝕀 ⊢ _}
BY
{ ((Subst' ((B)p)s+ ~ ((B)s)p 0 THENA CsmUnfoldingComp)
   THEN (Subst' (((q=0) ∨ (q=1)))s+ ~ ((q=0) ∨ (q=1)) 0
         THENA ((RWW "csm-face-or csm-face-zero csm-face-one" 0 THENA Auto) THEN EqCD THEN Auto)
         )
   THEN (Subst' ((if (q=0) then (A)p else (B)p))s+ ~ (if (q=0) then ((A)s)p else ((B)s)p) 0
         THENA ((RWW "csm-case-type csm-face-zero" 0 THENM CsmUnfolding) THEN Auto)
         )
   THEN (RWO "csm-equiv-fun" 0 THENA Auto)
   THEN RepeatFor 2 (EqCDA)) }

1
.....subterm..... T:t
1:n
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. f : {G ⊢ _:Equiv(A;B)}
5. H : CubicalSet{j}
6. s : H j⟶ G
7. ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (A)p
8. ∀phi:{G.𝕀 ⊢ _:𝔽}. G.𝕀, phi ⊢ (B)p
9. ∀phi:{H.𝕀 ⊢ _:𝔽}. H.𝕀, phi ⊢ ((A)s)p
10. ∀phi:{H.𝕀 ⊢ _:𝔽}. H.𝕀, phi ⊢ ((B)s)p
11. (Glue [((q=0) ∨ (q=1)) ⊢→ ((if (q=0) then (A)p else (B)p);equiv-fun(cubical-equiv-by-cases(G;B;f)))] (B)p)s+
= H.𝕀 ⊢ Glue [(((q=0) ∨ (q=1)))s+ ⊢→ (((if (q=0) then (A)p else (B)p))
                                       s+;(equiv-fun(cubical-equiv-by-cases(G;B;f)))s+)] ((B)p)s+
∈ {H.𝕀 ⊢ _}
⊢ (cubical-equiv-by-cases(G;B;f))s+
= cubical-equiv-by-cases(H;(B)s;(f)s)
∈ {H.𝕀, ((q=0) ∨ (q=1)) ⊢ _:Equiv((if (q=0) then ((A)s)p else ((B)s)p);((B)s)p)}

---

Latex:

---

Latex:
.....assertion..... 
1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_\}
3.  B  :  \{G  \mvdash{}  \_\}
4.  f  :  \{G  \mvdash{}  \_:Equiv(A;B)\}
5.  H  :  CubicalSet\{j\}
6.  s  :  H  j{}\mrightarrow{}  G
7.  \mforall{}phi:\{G.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}.  G.\mBbbI{},  phi  \mvdash{}  (A)p
8.  \mforall{}phi:\{G.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}.  G.\mBbbI{},  phi  \mvdash{}  (B)p
9.  \mforall{}phi:\{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}.  H.\mBbbI{},  phi  \mvdash{}  ((A)s)p
10.  \mforall{}phi:\{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}.  H.\mBbbI{},  phi  \mvdash{}  ((B)s)p
11.  (Glue  [((q=0)  \mvee{}  (q=1))  \mvdash{}\mrightarrow{}  ((if  (q=0)  then  (A)p  else  (B)p);
                                                              equiv-fun(cubical-equiv-by-cases(G;B;f)))]  (B)p)s+
=  H.\mBbbI{}  \mvdash{}  Glue  [(((q=0)  \mvee{}  (q=1)))s+  \mvdash{}\mrightarrow{}  (((if  (q=0)  then  (A)p  else  (B)p))
                                                                              s+;(equiv-fun(cubical-equiv-by-cases(G;B;f)))s+)]  ((B)p)s+
\mvdash{}  H.\mBbbI{}  \mvdash{}  Glue  [(((q=0)  \mvee{}  (q=1)))s+  \mvdash{}\mrightarrow{}  (((if  (q=0)  then  (A)p  else  (B)p))
                                                                              s+;(equiv-fun(cubical-equiv-by-cases(G;B;f)))s+)]  ((B)p)s+
=  H.\mBbbI{}  \mvdash{}  Glue  [((q=0)  \mvee{}  (q=1))  \mvdash{}\mrightarrow{}  ((if  (q=0)  then  ((A)s)
                                                                                                    p  else  ((B)s)
                                                                                                                    p);equiv-fun(...))]  ((B)s)p


By

---

Latex:
((Subst'  ((B)p)s+  \msim{}  ((B)s)p  0  THENA  CsmUnfoldingComp)
  THEN  (Subst'  (((q=0)  \mvee{}  (q=1)))s+  \msim{}  ((q=0)  \mvee{}  (q=1))  0
              THENA  ((RWW  "csm-face-or  csm-face-zero  csm-face-one"  0  THENA  Auto)  THEN  EqCD  THEN  Auto)
              )
  THEN  (Subst'  ((if  (q=0)  then  (A)p  else  (B)p))s+  \msim{}  (if  (q=0)  then  ((A)s)p  else  ((B)s)p)  0
              THENA  ((RWW  "csm-case-type  csm-face-zero"  0  THENM  CsmUnfolding)  THEN  Auto)
              )
  THEN  (RWO  "csm-equiv-fun"  0  THENA  Auto)
  THEN  RepeatFor  2  (EqCDA))

---

Home Index