Eilenberg-MacLane spaces and stabilisation in homotopy type theory

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.

v2: 7 pages, adds missing uniqueness proof

References in corpus (1)

• Introduction to Homotopy Type Theory

Cited by in corpus (2)

• Computational Synthetic Cohomology Theory in Homotopy Type Theory
• Central H-spaces and banded types