Eilenberg-MacLane spaces and stabilisation in homotopy type theory
Algebraic Topology
2025-04-14 v2 Logic in Computer Science
Abstract
In this note, we study the delooping of spaces and maps in homotopy type theory. We show that in some cases, spaces have a unique delooping, and give a simple description of the delooping in these cases. We explain why some maps, such as group homomorphisms, have a unique delooping. We discuss some applications to Eilenberg-MacLane spaces and cohomology.
Cite
@article{arxiv.2301.03685,
title = {Eilenberg-MacLane spaces and stabilisation in homotopy type theory},
author = {David Wärn},
journal= {arXiv preprint arXiv:2301.03685},
year = {2025}
}
Comments
v2: 7 pages, adds missing uniqueness proof