Homotopy Type Theory Localization in Homotopy Type Theory > history (changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

Localization in Homotopy Type Theory < , Localization in Homotopy Type TheoryJ. Daniel Christensen, Morgan Opie, Egbert Rijke, Luis Scoccola,



We study localization at a prime in homotopy type theory, using self maps of the circle. Our main result is that for a pointed, simply connected? type XX, the natural map XX (p)X \to X_{(p)} induces algebraic localizations on all homotopy groups?. In order to prove this, we further develop the theory of reflective subuniverses?. In particular, we show that for any reflective subuniverse LL, the subuniverse of LL-separated types is again a reflective subuniverse, which we call L 0L_0. Furthermore, we prove results establishing that L 0L_0 is almost left exact?. We next focus on localization with respect to a map, giving results on preservation of coproducts? and connectivity?. We also study how such localizations interact with other reflective subuniverses and orthogonal factorization systems?. As key steps towards proving the main theorem, we show that localization at a prime commutes with taking loop spaces for a pointed, simply connected type, and explicitly describe the localization of an Eilenberg-Mac Lane space K(G,n)K(G, n) with GG abelian. We also include a partial converse to the main theorem.

See also

category: reference

Last revised on June 9, 2022 at 16:06:51. See the history of this page for a list of all contributions to it.