Proof of Nuprl Lemma : csm-equiv-term

Step * 3 1 2 2 of Lemma csm-equiv-term

.....subterm..... T:t
2:n
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(𝕀)] ∈ {H, (phi)s ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)]}

BY
{ ((GenConclTerm ⌜contr-path(e;fiber-point(t;c))⌝⋅ THENA Auto)

   THEN (GenConcl ⌜(v)p = xx ∈ {G.𝕀, (phi)p ⊢ _:((Path_Fiber(equiv-fun(f);a) contr-center(e) fiber-point(t;c)))p}⌝⋅

         THENA Auto
         )
   THEN (Assert G.𝕀, (phi)p ⊢ (Fiber(equiv-fun(f);a))p BY
               (SubsumeC ⌜{G.𝕀 ⊢ _}⌝⋅ THEN Auto))
   THEN (Assert (contr-center(e))p ∈ {G.𝕀, (phi)p ⊢ _:(Fiber(equiv-fun(f);a))p} BY
               (SubsumeC ⌜{G.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}⌝⋅ THEN Auto))
   THEN (Assert q ∈ {G.𝕀, (phi)p ⊢ _:𝕀} BY
               (SubsumeC ⌜{G.𝕀 ⊢ _:𝕀}⌝⋅ THEN Auto))) }

1
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(𝕀)]}
22. v : {G, phi ⊢ _:(Path_Fiber(equiv-fun(f);a) contr-center(e) fiber-point(t;c))}

23. contr-path(e;fiber-point(t;c)) = v ∈ {G, phi ⊢ _:(Path_Fiber(equiv-fun(f);a) contr-center(e) fiber-point(t;c))}

24. xx : {G.𝕀, (phi)p ⊢ _:((Path_Fiber(equiv-fun(f);a) contr-center(e) fiber-point(t;c)))p}
25. (v)p = xx ∈ {G.𝕀, (phi)p ⊢ _:((Path_Fiber(equiv-fun(f);a) contr-center(e) fiber-point(t;c)))p}
26. G.𝕀, (phi)p ⊢ (Fiber(equiv-fun(f);a))p
27. (contr-center(e))p ∈ {G.𝕀, (phi)p ⊢ _:(Fiber(equiv-fun(f);a))p}
28. q ∈ {G.𝕀, (phi)p ⊢ _:𝕀}
⊢ ((xx @ q)s+)[1(𝕀)] ∈ {H, (phi)s ⊢ _:(((Fiber(equiv-fun(f);a))p)s+)[1(𝕀)]}

Latex:

Latex:
.....subterm..... T:t 2:n 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 21. a@0 : \{H \mvdash{} \_:(((Fiber(equiv-fun(f);a))p)s+)[1(\mBbbI{})]\} \mvdash{} (((contr-path(e;fiber-point(t;c)))p @ q)s+)[1(\mBbbI{})] \mmember{} \{H, (phi)s \mvdash{} \_:(((Fiber(equiv-fun(f);a))p)s+)[1(\mBbbI{})]\} By Latex: ((GenConclTerm \mkleeneopen{}contr-path(e;fiber-point(t;c))\mkleeneclose{}\mcdot{} THENA Auto) THEN (GenConcl \mkleeneopen{}(v)p = xx\mkleeneclose{}\mcdot{} THENA Auto) THEN (Assert G.\mBbbI{}, (phi)p \mvdash{} (Fiber(equiv-fun(f);a))p BY (SubsumeC \mkleeneopen{}\{G.\mBbbI{} \mvdash{} \_\}\mkleeneclose{}\mcdot{} THEN Auto)) THEN (Assert (contr-center(e))p \mmember{} \{G.\mBbbI{}, (phi)p \mvdash{} \_:(Fiber(equiv-fun(f);a))p\} BY (SubsumeC \mkleeneopen{}\{G.\mBbbI{} \mvdash{} \_:(Fiber(equiv-fun(f);a))p\}\mkleeneclose{}\mcdot{} THEN Auto)) THEN (Assert q \mmember{} \{G.\mBbbI{}, (phi)p \mvdash{} \_:\mBbbI{}\} BY (SubsumeC \mkleeneopen{}\{G.\mBbbI{} \mvdash{} \_:\mBbbI{}\}\mkleeneclose{}\mcdot{} THEN Auto))) Home Index