Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Eilenberg-MacLane spaces and stabilisation in homotopy type theory

David Wärn

TL;DR

The note develops a type-theoretic approach to delooping in HoTT by introducing the cofree TX construction that assigns a potential delooping to a pointed type X via X-torsors. It identifies precise connectivity and truncation conditions under which deloopings are unique and when maps between loop spaces lift to maps between deloopings, including a concrete description of Ω−1f. Armed with these tools, the paper builds Eilenberg–MacLane spaces K(G,n), derives relationships for πn(Sn) and Freudenthal-type identifications, and defines cohomology operations such as the cup product and Steenrod squares within this framework. The results yield elimination principles and structural correspondences that mirror classical algebraic topology, enabling a coherent, type-theoretic construction of cohomology theories and their operations inside HoTT. The approach is well-suited to formalisation and paves the way for a deeper, infinitary theory of higher groups and morphisms between them.

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.

Eilenberg-MacLane spaces and stabilisation in homotopy type theory

TL;DR

The note develops a type-theoretic approach to delooping in HoTT by introducing the cofree TX construction that assigns a potential delooping to a pointed type X via X-torsors. It identifies precise connectivity and truncation conditions under which deloopings are unique and when maps between loop spaces lift to maps between deloopings, including a concrete description of Ω−1f. Armed with these tools, the paper builds Eilenberg–MacLane spaces K(G,n), derives relationships for πn(Sn) and Freudenthal-type identifications, and defines cohomology operations such as the cup product and Steenrod squares within this framework. The results yield elimination principles and structural correspondences that mirror classical algebraic topology, enabling a coherent, type-theoretic construction of cohomology theories and their operations inside HoTT. The approach is well-suited to formalisation and paves the way for a deeper, infinitary theory of higher groups and morphisms between them.

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.
Paper Structure (9 sections, 11 theorems, 19 equations, 1 figure)

This paper contains 9 sections, 11 theorems, 19 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Delooping types
  3. Delooping maps
  4. Applications
  5. $\boldsymbol{\mathrm{K}(G,n)}$
  6. $\boldsymbol{\pi_n(S^n)}$
  7. The cup product
  8. Steenrod squares
  9. Concluding remarks

Key Result

Theorem 2

If the type $((Y,h,\mu) : TX) \times Y$ of pointed torsors is contractible, then $TX$ is a delooping of $X$. That is, we have a point $\mathrm{pt}_{TX} : TX$ with an equivalence $\Omega(TX, \mathrm{pt}_{TX}) \simeq_\mathrm{pt} X$. Moreover, $TX$ is the unique delooping of $X$ in this case.

Figures (1)

  • Figure :

Theorems & Definitions (20)

  • Definition 1
  • Theorem 2
  • proof
  • Lemma 3
  • proof
  • Lemma 4
  • Corollary 5
  • proof
  • Corollary 6
  • proof
  • ...and 10 more