Proof of Nuprl Lemma : csm-equiv-term

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(𝕀)]]}].

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(𝕀)]]}].

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