Step
*
3
of Lemma
csm-equiv-term
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G ⊢ _}
4. T : {G ⊢ _}
5. f : {G ⊢ _:Equiv(T;A)}
6. t : {G, phi ⊢ _:T}
7. a : {G ⊢ _:A}
8. app(equiv-fun(f); t) ∈ {G, phi ⊢ _:A}
9. c : {G, phi ⊢ _:(Path_A a app(equiv-fun(f); t))}
10. cF : G ⊢ Compositon(Fiber(equiv-fun(f);a))
11. H : CubicalSet{j}
12. s : H j⟶ G
13. e : {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
14. equiv-contr(f;a) = e ∈ {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
15. G ⊢ Fiber(equiv-fun(f);a)
16. fiber-point(t;c) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
17. ∀[u:{G, phi.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}]. ∀[a0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}].
    ∀[Delta:j⊢]. ∀[s:Delta j⟶ G].
      ((comp (cF)p [phi ⊢→ u] a0)s
      = comp ((cF)p)s+ [(phi)s ⊢→ (u)s+] (a0)s
      ∈ {Delta ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)][(phi)s |⟶ ((u)s+)[1(𝕀)]]})
18. contr-center(e) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
19. contr-path(e;fiber-point(t;c)) ∈ {G, phi ⊢ _:(Path_Fiber(equiv-fun(f);a) contr-center(e) fiber-point(t;c))}
20. (comp (cF)p [phi ⊢→ (contr-path(e;fiber-point(t;c)))p @ q] contr-center(e))s
= comp ((cF)p)s+ [(phi)s ⊢→ ((contr-path(e;fiber-point(t;c)))p @ q)s+] (contr-center(e))s
∈ {H ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)][(phi)s |⟶ (((contr-path(e;fiber-point(t;c)))p @ q)s+)[1(𝕀)]]}
⊢ (comp (cF)p [phi ⊢→ (contr-path(e;fiber-point(t;c)))p @ q] contr-center(e))s
= comp ((cF)s)p [(phi)s ⊢→ (contr-path(equiv-contr((f)s;(a)s);fiber-point((t)s;(c)s)))p @ q]
      contr-center(equiv-contr((f)s;(a)s))
∈ {H ⊢ _:Fiber(equiv-fun((f)s);(a)s)[(phi)s |⟶ fiber-point((t)s;(c)s)]}
BY
{ Assert ⌜{a@0:{H ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)]}| 
           (((contr-path(e;fiber-point(t;c)))p @ q)s+)[1(𝕀)]
           = a@0
           ∈ {H, (phi)s ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)]}}  ∈ 𝕌{[i' | j']}⌝⋅ }
1
.....assertion..... 
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G ⊢ _}
4. T : {G ⊢ _}
5. f : {G ⊢ _:Equiv(T;A)}
6. t : {G, phi ⊢ _:T}
7. a : {G ⊢ _:A}
8. app(equiv-fun(f); t) ∈ {G, phi ⊢ _:A}
9. c : {G, phi ⊢ _:(Path_A a app(equiv-fun(f); t))}
10. cF : G ⊢ Compositon(Fiber(equiv-fun(f);a))
11. H : CubicalSet{j}
12. s : H j⟶ G
13. e : {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
14. equiv-contr(f;a) = e ∈ {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
15. G ⊢ Fiber(equiv-fun(f);a)
16. fiber-point(t;c) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
17. ∀[u:{G, phi.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}]. ∀[a0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}].
    ∀[Delta:j⊢]. ∀[s:Delta j⟶ G].
      ((comp (cF)p [phi ⊢→ u] a0)s
      = comp ((cF)p)s+ [(phi)s ⊢→ (u)s+] (a0)s
      ∈ {Delta ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)][(phi)s |⟶ ((u)s+)[1(𝕀)]]})
18. contr-center(e) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
19. contr-path(e;fiber-point(t;c)) ∈ {G, phi ⊢ _:(Path_Fiber(equiv-fun(f);a) contr-center(e) fiber-point(t;c))}
20. (comp (cF)p [phi ⊢→ (contr-path(e;fiber-point(t;c)))p @ q] contr-center(e))s
= comp ((cF)p)s+ [(phi)s ⊢→ ((contr-path(e;fiber-point(t;c)))p @ q)s+] (contr-center(e))s
∈ {H ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)][(phi)s |⟶ (((contr-path(e;fiber-point(t;c)))p @ q)s+)[1(𝕀)]]}
⊢ {a@0:{H ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)]}| 
   (((contr-path(e;fiber-point(t;c)))p @ q)s+)[1(𝕀)] = a@0 ∈ {H, (phi)s ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)]}} 
  ∈ 𝕌{[i' | j']}
2
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G ⊢ _}
4. T : {G ⊢ _}
5. f : {G ⊢ _:Equiv(T;A)}
6. t : {G, phi ⊢ _:T}
7. a : {G ⊢ _:A}
8. app(equiv-fun(f); t) ∈ {G, phi ⊢ _:A}
9. c : {G, phi ⊢ _:(Path_A a app(equiv-fun(f); t))}
10. cF : G ⊢ Compositon(Fiber(equiv-fun(f);a))
11. H : CubicalSet{j}
12. s : H j⟶ G
13. e : {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
14. equiv-contr(f;a) = e ∈ {G ⊢ _:Contractible(Fiber(equiv-fun(f);a))}
15. G ⊢ Fiber(equiv-fun(f);a)
16. fiber-point(t;c) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
17. ∀[u:{G, phi.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}]. ∀[a0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}].
    ∀[Delta:j⊢]. ∀[s:Delta j⟶ G].
      ((comp (cF)p [phi ⊢→ u] a0)s
      = comp ((cF)p)s+ [(phi)s ⊢→ (u)s+] (a0)s
      ∈ {Delta ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)][(phi)s |⟶ ((u)s+)[1(𝕀)]]})
18. contr-center(e) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)}
19. contr-path(e;fiber-point(t;c)) ∈ {G, phi ⊢ _:(Path_Fiber(equiv-fun(f);a) contr-center(e) fiber-point(t;c))}
20. (comp (cF)p [phi ⊢→ (contr-path(e;fiber-point(t;c)))p @ q] contr-center(e))s
= comp ((cF)p)s+ [(phi)s ⊢→ ((contr-path(e;fiber-point(t;c)))p @ q)s+] (contr-center(e))s
∈ {H ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)][(phi)s |⟶ (((contr-path(e;fiber-point(t;c)))p @ q)s+)[1(𝕀)]]}
21. {a@0:{H ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)]}| 
     (((contr-path(e;fiber-point(t;c)))p @ q)s+)[1(𝕀)] = a@0 ∈ {H, (phi)s ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)]}} 
    ∈ 𝕌{[i' | j']}
⊢ (comp (cF)p [phi ⊢→ (contr-path(e;fiber-point(t;c)))p @ q] contr-center(e))s
= comp ((cF)s)p [(phi)s ⊢→ (contr-path(equiv-contr((f)s;(a)s);fiber-point((t)s;(c)s)))p @ q]
      contr-center(equiv-contr((f)s;(a)s))
∈ {H ⊢ _:Fiber(equiv-fun((f)s);(a)s)[(phi)s |⟶ fiber-point((t)s;(c)s)]}
Latex:
Latex:
1.  G  :  CubicalSet\{j\}
2.  phi  :  \{G  \mvdash{}  \_:\mBbbF{}\}
3.  A  :  \{G  \mvdash{}  \_\}
4.  T  :  \{G  \mvdash{}  \_\}
5.  f  :  \{G  \mvdash{}  \_:Equiv(T;A)\}
6.  t  :  \{G,  phi  \mvdash{}  \_:T\}
7.  a  :  \{G  \mvdash{}  \_:A\}
8.  app(equiv-fun(f);  t)  \mmember{}  \{G,  phi  \mvdash{}  \_:A\}
9.  c  :  \{G,  phi  \mvdash{}  \_:(Path\_A  a  app(equiv-fun(f);  t))\}
10.  cF  :  G  \mvdash{}  Compositon(Fiber(equiv-fun(f);a))
11.  H  :  CubicalSet\{j\}
12.  s  :  H  j{}\mrightarrow{}  G
13.  e  :  \{G  \mvdash{}  \_:Contractible(Fiber(equiv-fun(f);a))\}
14.  equiv-contr(f;a)  =  e
15.  G  \mvdash{}  Fiber(equiv-fun(f);a)
16.  fiber-point(t;c)  \mmember{}  \{G,  phi  \mvdash{}  \_:Fiber(equiv-fun(f);a)\}
17.  \mforall{}[u:\{G,  phi.\mBbbI{}  \mvdash{}  \_:(Fiber(equiv-fun(f);a))p\}].
        \mforall{}[a0:\{G  \mvdash{}  \_:((Fiber(equiv-fun(f);a))p)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}].  \mforall{}[Delta:j\mvdash{}].
        \mforall{}[s:Delta  j{}\mrightarrow{}  G].
            ((comp  (cF)p  [phi  \mvdash{}\mrightarrow{}  u]  a0)s  =  comp  ((cF)p)s+  [(phi)s  \mvdash{}\mrightarrow{}  (u)s+]  (a0)s)
18.  contr-center(e)  \mmember{}  \{G,  phi  \mvdash{}  \_:Fiber(equiv-fun(f);a)\}
19.  contr-path(e;fiber-point(t;c))  \mmember{}  \{G,  phi  \mvdash{}  \_:(Path\_Fiber(equiv-fun(f);a)  contr-center(e)
                                                                                                              fiber-point(t;c))\}
20.  (comp  (cF)p  [phi  \mvdash{}\mrightarrow{}  (contr-path(e;fiber-point(t;c)))p  @  q]  contr-center(e))s
=  comp  ((cF)p)s+  [(phi)s  \mvdash{}\mrightarrow{}  ((contr-path(e;fiber-point(t;c)))p  @  q)s+]  (contr-center(e))s
\mvdash{}  (comp  (cF)p  [phi  \mvdash{}\mrightarrow{}  (contr-path(e;fiber-point(t;c)))p  @  q]  contr-center(e))s
=  comp  ((cF)s)p  [(phi)s  \mvdash{}\mrightarrow{}  (contr-path(equiv-contr((f)s;(a)s);fiber-point((t)s;(c)s)))p  @  q]
            contr-center(equiv-contr((f)s;(a)s))
By
Latex:
Assert  \mkleeneopen{}\{a@0:\{H  \mvdash{}  \_:(((Fiber(equiv-fun(f);a))p)s+)[1(\mBbbI{})]\}| 
                  (((contr-path(e;fiber-point(t;c)))p  @  q)s+)[1(\mBbbI{})]  =  a@0\}    \mmember{}  \mBbbU{}\{[i'  |  j']\}\mkleeneclose{}\mcdot{}
Home
Index