Localization in Homotopy Type Theory

zbMATH Open1439.18023arXiv1807.04155MaRDI QIDQ5217587FDOQ5217587

Authors: J. Daniel Christensen, Morgan Opie, Egbert Rijke, Luis Nerio Scoccola 

Publication date: 24 February 2020

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 $Xo{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^{\prime }$. Furthermore, we prove results establishing that $L^{\prime }$ 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.

Full work available at URL: https://arxiv.org/abs/1807.04155

Recommendations

• scientific article; zbMATH DE number 2001302
• Locally cartesian closed categories and type theory
• Homotopy type theory
• Homotopy Type Theory
• Localizations in motivic homotopy theory
• scientific article; zbMATH DE number 2094827
• Localization in Hochschild homology
• Type theory and homotopy
• The homotopy theory of type theories
• Local homotopy theory

zbMATH Keywords

localizationunivalence axiomhomotopy type theoryreflective subuniverseseparated typesynthetic homotopy theory

Mathematics Subject Classification ID

Localization and completion in homotopy theory (55P60) Localization of categories, calculus of fractions (18E35) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Cites Work

• Cellular spaces, null spaces and homotopy localization
• More concise algebraic topology. Localization, completion, and model categories
• Homotopy type theory. Univalent foundations of mathematics
• Localization and Periodicity in Unstable Homotopy Theory
• The homotopy theory of type theories
• Homotopy limits in type theory
• Semantics of higher inductive types
• Modalities in homotopy type theory
• $L'$-localization in an $\infty$-topos
• Localizing with Respect to Self-Maps of the Circle
• Nilpotent types and fracture squares in homotopy type theory
• Eilenberg-MacLane spaces in homotopy type theory
• Higher groups in homotopy type theory
• Sequential colimits in homotopy type theory

Cited In (7)

• $L'$-localization in an $\infty$-topos
• Non-accessible localizations
• Characterizations of modalities and lex modalities
• Nilpotent types and fracture squares in homotopy type theory
• Left-exact localizations of \(\infty\)-topoi. II: Grothendieck topologies
• The Hurewicz theorem in homotopy type theory
• Modal descent

This page was built for publication: Localization in Homotopy Type Theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5217587)