Nilpotent Types and Fracture Squares in Homotopy Type Theory
Algebraic Topology
2022-01-27 v2 Category 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.
Keywords
Cite
@article{arxiv.1903.03245,
title = {Nilpotent Types and Fracture Squares in Homotopy Type Theory},
author = {Luis Scoccola},
journal= {arXiv preprint arXiv:1903.03245},
year = {2022}
}
Comments
35 pages; minor improvements from published version (2020)