Nilpotent Types and Fracture Squares in Homotopy Type Theory

Abstract

We develop the basic theory of nilpotent types and their localizations away from sets of numbers in Homotopy Type Theory. For this, general results about the classifying spaces of fibrations with fiber an Eilenberg-Mac Lane space are proven. We also construct fracture squares for localizations away from sets of numbers. All of our proofs are constructive.

35 pages; minor improvements from published version (2020)

References in corpus (5)

• Modalities in homotopy type theory
• Semantics of higher inductive types
• The homotopy theory of type theories
• All $(\infty ,1)$-toposes have strict univalent universes
• Localization in Homotopy Type Theory

Cited by in corpus (4)

• All $(\infty ,1)$-toposes have strict univalent universes
• The Hurewicz theorem in Homotopy Type Theory
• Epimorphisms and Acyclic Types in Univalent Foundations
• Central H-spaces and banded types