_Localization in Homotopy Type Theory_, [[J. Daniel Christensen]], [[Morgan Opie]], [[Egbert Rijke]], [[Luis Scoccola]], ## Links ## [arXiv:1807.04155](https://arxiv.org/abs/1807.04155) ### Abstract ### 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 $X$, the natural map $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 $L$, the subuniverse of $L$-separated types is again a reflective subuniverse, which we call $L_0$. Furthermore, we prove results establishing that $L_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)$ with $G$ abelian. We also include a partial converse to the main theorem. ## See also ## * [[Modalities in homotopy type theory]] * [[References]] category: reference