Step
*
2
2
of Lemma
equiv-term-0
.....wf.....
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G ⊢ _}
4. T : {G ⊢ _}
5. f : {G ⊢ _:Equiv(T;A)}
6. a : {G ⊢ _:A}
7. t : Top
8. c : Top
9. cF : G +⊢ Compositon(Fiber(equiv-fun(f);a))
10. ctr : {G ⊢ _:Fiber(equiv-fun(f);a)}
11. contr-center(equiv-contr(f;a)) = ctr ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}
12. xx : Top
13. (contr-path(equiv-contr(f;a);fiber-point(t;c)))p @ q = xx ∈ Top
14. ∀[a@0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)]}]. ∀[xx:Top].
(comp (cF)p [0(𝔽) ⊢→ xx] a@0 = transprt(G;(cF)p;a@0) ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)]})
15. Z : {G ⊢ _:𝔽}
16. Z = phi ∈ {G ⊢ _:𝔽}
17. Z = 0(𝔽) ∈ {G ⊢ _:𝔽}
18. ∀[u:{G, Z.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}]. ∀[a0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][Z |⟶ (u)[0(𝕀)]]}].
(comp (cF)p [Z ⊢→ u] a0 ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)][Z |⟶ (u)[1(𝕀)]]})
⊢ ctr ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][Z |⟶ (xx)[0(𝕀)]]}
BY
{ MemTypeCD }
1
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G ⊢ _}
4. T : {G ⊢ _}
5. f : {G ⊢ _:Equiv(T;A)}
6. a : {G ⊢ _:A}
7. t : Top
8. c : Top
9. cF : G +⊢ Compositon(Fiber(equiv-fun(f);a))
10. ctr : {G ⊢ _:Fiber(equiv-fun(f);a)}
11. contr-center(equiv-contr(f;a)) = ctr ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}
12. xx : Top
13. (contr-path(equiv-contr(f;a);fiber-point(t;c)))p @ q = xx ∈ Top
14. ∀[a@0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)]}]. ∀[xx:Top].
(comp (cF)p [0(𝔽) ⊢→ xx] a@0 = transprt(G;(cF)p;a@0) ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)]})
15. Z : {G ⊢ _:𝔽}
16. Z = phi ∈ {G ⊢ _:𝔽}
17. Z = 0(𝔽) ∈ {G ⊢ _:𝔽}
18. ∀[u:{G, Z.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}]. ∀[a0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][Z |⟶ (u)[0(𝕀)]]}].
(comp (cF)p [Z ⊢→ u] a0 ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)][Z |⟶ (u)[1(𝕀)]]})
⊢ ctr ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)]}
2
.....set predicate.....
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G ⊢ _}
4. T : {G ⊢ _}
5. f : {G ⊢ _:Equiv(T;A)}
6. a : {G ⊢ _:A}
7. t : Top
8. c : Top
9. cF : G +⊢ Compositon(Fiber(equiv-fun(f);a))
10. ctr : {G ⊢ _:Fiber(equiv-fun(f);a)}
11. contr-center(equiv-contr(f;a)) = ctr ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}
12. xx : Top
13. (contr-path(equiv-contr(f;a);fiber-point(t;c)))p @ q = xx ∈ Top
14. ∀[a@0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)]}]. ∀[xx:Top].
(comp (cF)p [0(𝔽) ⊢→ xx] a@0 = transprt(G;(cF)p;a@0) ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)]})
15. Z : {G ⊢ _:𝔽}
16. Z = phi ∈ {G ⊢ _:𝔽}
17. Z = 0(𝔽) ∈ {G ⊢ _:𝔽}
18. ∀[u:{G, Z.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}]. ∀[a0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][Z |⟶ (u)[0(𝕀)]]}].
(comp (cF)p [Z ⊢→ u] a0 ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)][Z |⟶ (u)[1(𝕀)]]})
⊢ (xx)[0(𝕀)] = ctr ∈ {G, Z ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)]}
3
.....wf.....
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. A : {G ⊢ _}
4. T : {G ⊢ _}
5. f : {G ⊢ _:Equiv(T;A)}
6. a : {G ⊢ _:A}
7. t : Top
8. c : Top
9. cF : G +⊢ Compositon(Fiber(equiv-fun(f);a))
10. ctr : {G ⊢ _:Fiber(equiv-fun(f);a)}
11. contr-center(equiv-contr(f;a)) = ctr ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}
12. xx : Top
13. (contr-path(equiv-contr(f;a);fiber-point(t;c)))p @ q = xx ∈ Top
14. ∀[a@0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)]}]. ∀[xx:Top].
(comp (cF)p [0(𝔽) ⊢→ xx] a@0 = transprt(G;(cF)p;a@0) ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)]})
15. Z : {G ⊢ _:𝔽}
16. Z = phi ∈ {G ⊢ _:𝔽}
17. Z = 0(𝔽) ∈ {G ⊢ _:𝔽}
18. ∀[u:{G, Z.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}]. ∀[a0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][Z |⟶ (u)[0(𝕀)]]}].
(comp (cF)p [Z ⊢→ u] a0 ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)][Z |⟶ (u)[1(𝕀)]]})
19. a@0 : {G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)]}
⊢ istype((xx)[0(𝕀)] = a@0 ∈ {G, Z ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)]})
Latex:
Latex:
.....wf.....
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. a : \{G \mvdash{} \_:A\}
7. t : Top
8. c : Top
9. cF : G +\mvdash{} Compositon(Fiber(equiv-fun(f);a))
10. ctr : \{G \mvdash{} \_:Fiber(equiv-fun(f);a)\}
11. contr-center(equiv-contr(f;a)) = ctr
12. xx : Top
13. (contr-path(equiv-contr(f;a);fiber-point(t;c)))p @ q = xx
14. \mforall{}[a@0:\{G \mvdash{} \_:((Fiber(equiv-fun(f);a))p)[0(\mBbbI{})]\}]. \mforall{}[xx:Top].
(comp (cF)p [0(\mBbbF{}) \mvdash{}\mrightarrow{} xx] a@0 = transprt(G;(cF)p;a@0))
15. Z : \{G \mvdash{} \_:\mBbbF{}\}
16. Z = phi
17. Z = 0(\mBbbF{})
18. \mforall{}[u:\{G, Z.\mBbbI{} \mvdash{} \_:(Fiber(equiv-fun(f);a))p\}].
\mforall{}[a0:\{G \mvdash{} \_:((Fiber(equiv-fun(f);a))p)[0(\mBbbI{})][Z |{}\mrightarrow{} (u)[0(\mBbbI{})]]\}].
(comp (cF)p [Z \mvdash{}\mrightarrow{} u] a0 \mmember{} \{G \mvdash{} \_:((Fiber(equiv-fun(f);a))p)[1(\mBbbI{})][Z |{}\mrightarrow{} (u)[1(\mBbbI{})]]\})
\mvdash{} ctr \mmember{} \{G \mvdash{} \_:((Fiber(equiv-fun(f);a))p)[0(\mBbbI{})][Z |{}\mrightarrow{} (xx)[0(\mBbbI{})]]\}
By
Latex:
MemTypeCD
Home
Index