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