---

Step * 4 of Lemma equiv-path2-1

.....assertion..... 
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. f : {G ⊢ _:Equiv(A;B)}
5. cA : G +⊢ Compositon(A)
6. cB : G +⊢ Compositon(B)
7. G.𝕀, ((q=0) ∨ (q=1)) ⊢ (if (q=0) then (A)p else (B)p)
8. case-type-comp(G.𝕀; (q=0); (q=1); (A)p; (B)p; (cA)p; (cB)p)
   ∈ G.𝕀, ((q=0) ∨ (q=1)) +⊢ Compositon((if (q=0) then (A)p else (B)p))
9. G ⊢ (1(𝔽) ⇒ (((q=0) ∨ (q=1)))[1(𝕀)])
10. (comp(Glue [((q=0) ∨ (q=1)) ⊢→ ((if (q=0) then (A)p else (B)p), cubical-equiv-by-cases(G;B;f))] (B)p) )[1(𝕀)]
= (case-type-comp(G.𝕀; (q=0); (q=1); (A)p; (B)p; (cA)p; (cB)p))[1(𝕀)]
∈ G +⊢ Compositon(((if (q=0) then (A)p else (B)p))[1(𝕀)])
11. (case-type-comp(G.𝕀; (q=0); (q=1); (A)p; (B)p; (cA)p; (cB)p))[1(𝕀)]
= cB
∈ G +⊢ Compositon(((if (q=0) then (A)p else (B)p))[1(𝕀)])
⊢ G +⊢ Compositon(((if (q=0) then (A)p else (B)p))[1(𝕀)]) = G +⊢ Compositon(B) ∈ 𝕌{[j 2 | i 2]}
BY
{ ((RWW  "csm-case-type csm-face-or csm-face-one csm-face-zero" 0 THENA Auto)
   THEN (Subst' ((B)p)[1(𝕀)] ~ (B)1(G) 0 THENA (CsmUnfolding THEN Auto))
   THEN (Subst' ((A)p)[1(𝕀)] ~ (A)1(G) 0 THENA (CsmUnfolding THEN Auto))
   THEN (Subst' (q)[1(𝕀)] ~ 1(𝕀) 0 THENA (CsmUnfolding THEN Auto))
   THEN EqCDA
   THEN SubsumeC ⌜{G ⊢ _}⌝⋅
   THEN Auto) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. B : {G ⊢ _}
4. f : {G ⊢ _:Equiv(A;B)}
5. cA : G +⊢ Compositon(A)
6. cB : G +⊢ Compositon(B)
7. G.𝕀, ((q=0) ∨ (q=1)) ⊢ (if (q=0) then (A)p else (B)p)
8. case-type-comp(G.𝕀; (q=0); (q=1); (A)p; (B)p; (cA)p; (cB)p)
   ∈ G.𝕀, ((q=0) ∨ (q=1)) +⊢ Compositon((if (q=0) then (A)p else (B)p))
9. G ⊢ (1(𝔽) ⇒ (((q=0) ∨ (q=1)))[1(𝕀)])
10. (comp(Glue [((q=0) ∨ (q=1)) ⊢→ ((if (q=0) then (A)p else (B)p), cubical-equiv-by-cases(G;B;f))] (B)p) )[1(𝕀)]
= (case-type-comp(G.𝕀; (q=0); (q=1); (A)p; (B)p; (cA)p; (cB)p))[1(𝕀)]
∈ G +⊢ Compositon(((if (q=0) then (A)p else (B)p))[1(𝕀)])
11. (case-type-comp(G.𝕀; (q=0); (q=1); (A)p; (B)p; (cA)p; (cB)p))[1(𝕀)]
= cB
∈ G +⊢ Compositon(((if (q=0) then (A)p else (B)p))[1(𝕀)])
⊢ (if (1(𝕀)=0) then (A)1(G) else (B)1(G)) = B ∈ {G ⊢ _}

---

Latex:

---

Latex:
.....assertion..... 
1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_\}
3.  B  :  \{G  \mvdash{}  \_\}
4.  f  :  \{G  \mvdash{}  \_:Equiv(A;B)\}
5.  cA  :  G  +\mvdash{}  Compositon(A)
6.  cB  :  G  +\mvdash{}  Compositon(B)
7.  G.\mBbbI{},  ((q=0)  \mvee{}  (q=1))  \mvdash{}  (if  (q=0)  then  (A)p  else  (B)p)
8.  case-type-comp(G.\mBbbI{};  (q=0);  (q=1);  (A)p;  (B)p;  (cA)p;  (cB)p)
      \mmember{}  G.\mBbbI{},  ((q=0)  \mvee{}  (q=1))  +\mvdash{}  Compositon((if  (q=0)  then  (A)p  else  (B)p))
9.  G  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  (((q=0)  \mvee{}  (q=1)))[1(\mBbbI{})])
10.  (comp(Glue  [((q=0)  \mvee{}  (q=1))  \mvdash{}\mrightarrow{}  ((if  (q=0)  then  (A)p  else  (B)p),  cubical-equiv-by-cases(G;B;f))]
                            (B)p)  )[1(\mBbbI{})]
=  (case-type-comp(G.\mBbbI{};  (q=0);  (q=1);  (A)p;  (B)p;  (cA)p;  (cB)p))[1(\mBbbI{})]
11.  (case-type-comp(G.\mBbbI{};  (q=0);  (q=1);  (A)p;  (B)p;  (cA)p;  (cB)p))[1(\mBbbI{})]  =  cB
\mvdash{}  G  +\mvdash{}  Compositon(((if  (q=0)  then  (A)p  else  (B)p))[1(\mBbbI{})])  =  G  +\mvdash{}  Compositon(B)


By

---

Latex:
((RWW    "csm-case-type  csm-face-or  csm-face-one  csm-face-zero"  0  THENA  Auto)
  THEN  (Subst'  ((B)p)[1(\mBbbI{})]  \msim{}  (B)1(G)  0  THENA  (CsmUnfolding  THEN  Auto))
  THEN  (Subst'  ((A)p)[1(\mBbbI{})]  \msim{}  (A)1(G)  0  THENA  (CsmUnfolding  THEN  Auto))
  THEN  (Subst'  (q)[1(\mBbbI{})]  \msim{}  1(\mBbbI{})  0  THENA  (CsmUnfolding  THEN  Auto))
  THEN  EqCDA
  THEN  SubsumeC  \mkleeneopen{}\{G  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index