Proof of Nuprl Lemma : csm-equiv-term

Step * of Lemma csm-equiv-term

No Annotations

∀[G:j⊢]. ∀[phi:{G ⊢ _:𝔽}]. ∀[A,T:{G ⊢ _}]. ∀[f:{G ⊢ _:Equiv(T;A)}]. ∀[t:{G, phi ⊢ _:T}]. ∀[a:{G ⊢ _:A}].

∀[c:{G, phi ⊢ _:(Path_A a app(equiv-fun(f); t))}]. ∀[cF:G ⊢ Compositon(Fiber(equiv-fun(f);a))]. ∀[H:j⊢]. ∀[s:H j⟶ G].

  ((equiv f [phi ⊢→ (t,  c)] a)s
  = equiv (f)s [(phi)s ⊢→ ((t)s,  (c)s)] (a)s
  ∈ {H ⊢ _:Fiber(equiv-fun((f)s);(a)s)[(phi)s |⟶ fiber-point((t)s;(c)s)]})
BY
{ (RepeatFor 7 (Intro)
   THEN (Assert app(equiv-fun(f); t) ∈ {G, phi ⊢ _:A} BY
               (MemCD THEN Try (RWO "cubical-fun-subset" 0) THEN Auto))
   THEN Intros
   THEN Unhide
   THEN Unfold `equiv-term` 0
   THEN (GenConclTerm ⌜equiv-contr(f;a)⌝⋅ THENA Auto)
   THEN RenameVar `e' (-2)

   THEN (RepUR ``let`` 0 THEN (InstLemma `cubical-fiber_wf` [⌜G⌝;⌜T⌝;⌜A⌝;⌜equiv-fun(f)⌝;⌜a⌝]⋅ THENA Auto))

THEN (Assert fiber-point(t;c) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)} BY
(InferEqualType

                THENL [(RWO  "fiber-subset" 0 THEN Auto); (MemCD THEN RWW "cubical-fun-subset" 0 THEN Auto)]

               ))
   THEN (InstLemma `csm-comp_term` [⌜G⌝;⌜phi⌝;⌜(Fiber(equiv-fun(f);a))p⌝;⌜(cF)p⌝]⋅ THENA Auto)
   THEN (Assert contr-center(e) ∈ {G, phi ⊢ _:Fiber(equiv-fun(f);a)} BY
               (SubsumeC ⌜{G ⊢ _:Fiber(equiv-fun(f);a)}⌝⋅ THEN Auto))
   THEN (Assert contr-path(e;fiber-point(t;c)) ∈ {G, phi ⊢ _:(Path_Fiber(equiv-fun(f);a) contr-center(e)

                                                                   fiber-point(t;c))} BY

(MemCD THEN RWW "contractible-type-subset" 0 THEN Auto))

   THEN (InstHyp [⌜(contr-path(e;fiber-point(t;c)))p @ q⌝;⌜contr-center(e)⌝;⌜H⌝;⌜s⌝] (-3)⋅ THENA Try (Trivial))) }

1
.....wf.....
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))}

⊢ (contr-path(e;fiber-point(t;c)))p @ q ∈ {G, phi.𝕀 ⊢ _:(Fiber(equiv-fun(f);a))p}

2
.....wf.....
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))}

⊢ contr-center(e) ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)][phi |⟶ ((contr-path(e;fiber-point(t;c)))p @ q)[0(𝕀)]]}

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

⊢ (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:
No Annotations \mforall{}[G:j\mvdash{}]. \mforall{}[phi:\{G \mvdash{} \_:\mBbbF{}\}]. \mforall{}[A,T:\{G \mvdash{} \_\}]. \mforall{}[f:\{G \mvdash{} \_:Equiv(T;A)\}]. \mforall{}[t:\{G, phi \mvdash{} \_:T\}]. \mforall{}[a:\{G \mvdash{} \_:A\}]. \mforall{}[c:\{G, phi \mvdash{} \_:(Path\_A a app(equiv-fun(f); t))\}]. \mforall{}[cF:G \mvdash{} Compositon(Fiber(equiv-fun(f);a))]. \mforall{}[H:j\mvdash{}]. \mforall{}[s:H j{}\mrightarrow{} G]. ((equiv f [phi \mvdash{}\mrightarrow{} (t, c)] a)s = equiv (f)s [(phi)s \mvdash{}\mrightarrow{} ((t)s, (c)s)] (a)s) By Latex: (RepeatFor 7 (Intro) THEN (Assert app(equiv-fun(f); t) \mmember{} \{G, phi \mvdash{} \_:A\} BY (MemCD THEN Try (RWO "cubical-fun-subset" 0) THEN Auto)) THEN Intros THEN Unhide THEN Unfold `equiv-term` 0 THEN (GenConclTerm \mkleeneopen{}equiv-contr(f;a)\mkleeneclose{}\mcdot{} THENA Auto) THEN RenameVar `e' (-2) THEN (RepUR ``let`` 0 THEN (InstLemma `cubical-fiber\_wf` [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}equiv-fun(f)\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{} THENA Auto) ) THEN (Assert fiber-point(t;c) \mmember{} \{G, phi \mvdash{} \_:Fiber(equiv-fun(f);a)\} BY (InferEqualType THENL [(RWO "fiber-subset" 0 THEN Auto) ; (MemCD THEN RWW "cubical-fun-subset" 0 THEN Auto)] )) THEN (InstLemma `csm-comp\_term` [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}(Fiber(equiv-fun(f);a))p\mkleeneclose{};\mkleeneopen{}(cF)p\mkleeneclose{}]\mcdot{} THENA Auto) THEN (Assert contr-center(e) \mmember{} \{G, phi \mvdash{} \_:Fiber(equiv-fun(f);a)\} BY (SubsumeC \mkleeneopen{}\{G \mvdash{} \_:Fiber(equiv-fun(f);a)\}\mkleeneclose{}\mcdot{} THEN Auto)) THEN (Assert contr-path(e;fiber-point(t;c)) \mmember{} \{G, phi \mvdash{} \_:(Path\_Fiber(equiv-fun(f);a) contr-center(e) fiber-point(t;c))\} BY (MemCD THEN RWW "contractible-type-subset" 0 THEN Auto)) THEN (InstHyp [\mkleeneopen{}(contr-path(e;fiber-point(t;c)))p @ q\mkleeneclose{};\mkleeneopen{}contr-center(e)\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}] (-3)\mcdot{} THENA Try (Trivial) )) Home Index