# Nilpotent Types and Fracture Squares in Homotopy Type Theory

## TL;DR

This paper develops the theory of nilpotent types and fracture squares within Homotopy Type Theory, providing constructive proofs for classifying spaces and localizations, advancing the understanding of homotopical structures.

## Contribution

It introduces a constructive framework for nilpotent types and fracture squares in Homotopy Type Theory, including new results on classifying spaces of fibrations with Eilenberg-Mac Lane fibers.

## Key findings

- Constructive proofs for classifying spaces of fibrations.
- Development of fracture squares for localizations.
- Foundations for nilpotent types 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.