---

Step * of Lemma equiv-path2-1

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _}]. ∀[f:{G ⊢ _:Equiv(A;B)}]. ∀[cA:G +⊢ Compositon(A)]. ∀[cB:G +⊢ Compositon(B)].
  ((equiv-path2(G;A;B;cA;cB;f))[1(𝕀)] = cB ∈ G +⊢ Compositon(B))
BY
{ (Intros
   THEN (Assert G.𝕀, ((q=0) ∨ (q=1)) ⊢ (if (q=0) then (A)p else (B)p) BY
               ((GenConcl ⌜q = i ∈ {G.𝕀 ⊢ _:𝕀}⌝⋅ THENA Auto)
                THEN (GenConcl ⌜(A)p = AA ∈ {G.𝕀 ⊢ _}⌝⋅ THENA Auto)
                THEN GenConcl ⌜(B)p = BB ∈ {G.𝕀 ⊢ _}⌝⋅
                THEN Auto))
   THEN Unfold `equiv-path2` 0
   THEN (Assert ⌜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))⌝⋅
         THENM Assert ⌜G ⊢ (1(𝔽) ⇒ (((q=0) ∨ (q=1)))[1(𝕀)])⌝⋅
         THENM ((Assert (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(𝕀)]) BY
                       (BLemma `csm-glue-comp-agrees` THEN Auto))
                THEN (Assert ⌜(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(𝕀)])⌝⋅
                      THENM Assert ⌜G +⊢ Compositon(((if (q=0) then (A)p else (B)p))[1(𝕀)])
                                    = G +⊢ Compositon(B)
                                    ∈ 𝕌{[j 2 | i 2]}⌝⋅
                      THENM Eq)
                ))) }

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)
⊢ 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))

2
.....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))
⊢ G ⊢ (1(𝔽) ⇒ (((q=0) ∨ (q=1)))[1(𝕀)])

3
.....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(𝕀)])
⊢ (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(𝕀)])

4
.....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]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(A;B)\}].  \mforall{}[cA:G  +\mvdash{}  Compositon(A)].
\mforall{}[cB:G  +\mvdash{}  Compositon(B)].
    ((equiv-path2(G;A;B;cA;cB;f))[1(\mBbbI{})]  =  cB)


By

---

Latex:
(Intros
  THEN  (Assert  G.\mBbbI{},  ((q=0)  \mvee{}  (q=1))  \mvdash{}  (if  (q=0)  then  (A)p  else  (B)p)  BY
                          ((GenConcl  \mkleeneopen{}q  =  i\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  (GenConcl  \mkleeneopen{}(A)p  =  AA\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  GenConcl  \mkleeneopen{}(B)p  =  BB\mkleeneclose{}\mcdot{}
                            THEN  Auto))
  THEN  Unfold  `equiv-path2`  0
  THEN  (Assert  \mkleeneopen{}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))\mkleeneclose{}\mcdot{}
              THENM  Assert  \mkleeneopen{}G  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  (((q=0)  \mvee{}  (q=1)))[1(\mBbbI{})])\mkleeneclose{}\mcdot{}
              THENM  ((Assert  (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{})]  BY
                                          (BLemma  `csm-glue-comp-agrees`  THEN  Auto))
                            THEN  (Assert  \mkleeneopen{}(case-type-comp(G.\mBbbI{};  (q=0);  (q=1);  (A)p;  (B)p;  (cA)p;  (cB)p))[1(\mBbbI{})]
                                                        =  cB\mkleeneclose{}\mcdot{}
                                        THENM  Assert  \mkleeneopen{}G  +\mvdash{}  Compositon(((if  (q=0)  then  (A)p  else  (B)p))[1(\mBbbI{})])
                                                                    =  G  +\mvdash{}  Compositon(B)\mkleeneclose{}\mcdot{}
                                        THENM  Eq)
                            )))

---

Home Index