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.

翻译：本文研究了同伦类型论中空间与映射的消环化。我们证明了在某些情况下空间具有唯一的消环化，并给出了这些情况下消环化的简单描述。我们解释了为何某些映射（如群同态）具有唯一的消环化，并讨论了有关Eilenberg-MacLane空间及上同调的一些应用。