Localization in Homotopy Type Theory

MaRDI QIDQ5217587zbMATH OpenFDO

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

Publication date 24 February 2020

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

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)

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.

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

Cites work

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

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)