Localization in Homotopy Type Theory

zbMath1439.18023arXiv1807.04155MaRDI QIDQ5217587

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

Publication date: 24 February 2020

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

zbMATH Keywords

localizationhomotopy type theoryunivalence axiomreflective 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)

Related Items (6)

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

Cites Work

• Unnamed Item
• The homotopy theory of type theories
• Cellular spaces, null spaces and homotopy localization
• Localizing with Respect to Self-Maps of the Circle
• Localization and Periodicity in Unstable Homotopy Theory
• Eilenberg-MacLane spaces in homotopy type theory
• Semantics of higher inductive types
• Nilpotent types and fracture squares in homotopy type theory
• Higher Groups in Homotopy Type Theory
• Sequential Colimits in Homotopy Type Theory
• Modalities in homotopy type theory
• $L'$-localization in an $\infty$-topos
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Homotopy limits in type theory

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