Step
*
of Lemma
csm-equiv-path2
No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _}]. ∀[cA:G +⊢ Compositon(A)]. ∀[cB:G +⊢ Compositon(B)]. ∀[f:{G ⊢ _:Equiv(A;B)}]. ∀[H:j⊢].
∀[s:H j⟶ G].
  ((equiv-path2(G;A;B;cA;cB;f))s+
  = 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
{ (Intros
   THEN (Assert ⌜G.𝕀, ((q=0) ∨ (q=1)) ⊢ (if (q=0) then (A)p else (B)p)⌝⋅
        THENM (RW (AddrC [2;4] (UnfoldC `equiv-path2`)) 0
               THEN (InstLemma `csm-glue-comp` [⌜G.𝕀⌝;⌜H.𝕀⌝]⋅ THENA Auto)
               THEN (RWO "-1" 0 THENA Auto))
        )
   ) }
1
.....assertion..... 
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
⊢ G.𝕀, ((q=0) ∨ (q=1)) ⊢ (if (q=0) then (A)p else (B)p)
2
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)))s+ ⊢→ (((if (q=0) then (A)p else (B)p))s+, (cubical-equiv-by-cases(G;B;f))s+)] ((B)p)s+) 
= 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:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_\}].  \mforall{}[cA:G  +\mvdash{}  Compositon(A)].  \mforall{}[cB:G  +\mvdash{}  Compositon(B)].
\mforall{}[f:\{G  \mvdash{}  \_:Equiv(A;B)\}].  \mforall{}[H:j\mvdash{}].  \mforall{}[s:H  j{}\mrightarrow{}  G].
    ((equiv-path2(G;A;B;cA;cB;f))s+  =  equiv-path2(H;(A)s;(B)s;(cA)s;(cB)s;(f)s))
By
Latex:
(Intros
  THEN  (Assert  \mkleeneopen{}G.\mBbbI{},  ((q=0)  \mvee{}  (q=1))  \mvdash{}  (if  (q=0)  then  (A)p  else  (B)p)\mkleeneclose{}\mcdot{}
            THENM  (RW  (AddrC  [2;4]  (UnfoldC  `equiv-path2`))  0
                          THEN  (InstLemma  `csm-glue-comp`  [\mkleeneopen{}G.\mBbbI{}\mkleeneclose{};\mkleeneopen{}H.\mBbbI{}\mkleeneclose{}]\mcdot{}  THENA  Auto)
                          THEN  (RWO  "-1"  0  THENA  Auto))
            )
  )
Home
Index