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