Eilenberg-MacLane spaces and stabilisation in homotopy type theory

TL;DR

This paper explores the properties of delooping in homotopy type theory, demonstrating conditions for uniqueness and applying these results to Eilenberg-MacLane spaces and cohomology.

Contribution

It provides a characterization of unique delooping in homotopy type theory and applies it to classical spaces and cohomological concepts.

Findings

Spaces have unique delooping under certain conditions

Group homomorphisms have a unique delooping

Applications to Eilenberg-MacLane spaces and cohomology

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.