nLab Eilenberg-MacLane space type

Idea

Let $G$ be an abelian group, and $n$ a natural number. The Eilenberg-MacLane space $K(G,n)$ is the unique space that has $\pi_n(K(G,n))\cong G$ and its other homotopy groups trivial. These spaces are a basic tool in classical algebraic topology, they can be used to define cohomology.

There is an analogous construction in homotopy type theory.

Definition

Let $G$ be a group. The Eilenberg-MacLane space type $K(G,1)$ is the higher inductive 1-type with the following constructors:

• $base : K(G,1)$
• $loop : G \to (base = base)$
• $id : loop(e) = refl_{base}$
• $comp : \prod_{(x,y:G)} loop(x \cdot y) = loop(y) \circ loop(x)$

$base$ is a point of $K(G,1)$, $loop$ is a function that constructs a path from $base$ to $base$ for each element of $G$. $id$ says the path constructed from the identity element is the trivial loop. Finally, $comp$ says that the path constructed from group multiplication of elements is the concatenation of paths.

It should be noted that this type is 1-truncated which could be added as another constructor:

• $\displaystyle \prod_{x,y:K(G,1)} \prod_{p,q:x=y} \prod_{r,s:p=q} r = s$

Recursion principle

To define a function $f : K(G,1) \to C$ for some type $C$, it suffices to give

• a point $c : C$
• a family of loops $l : G \to (c = c)$
• a path $l(e)=id$
• a path $l(x \cdot y) = l(y) \circ l(x)$
• a proof that $C$ is a 1-type.

Then $f$ satisfies the equations

$$f(base) \equiv c$$

$$ap_{f} (loop(x))=l(x)$$

It should be noted that the above can be compressed, to specify a function $f : K(G,1) \to C$, it suffices to give:

• a proof that $C$ is a 1-type
• a point $c : C$
• a group homomorphism from $G$ to $\Omega(C,c)$

See also

• higher inductive type

• Eilenberg-MacLane space

• cohomology in homotopy type theory

References

• Dan Licata, Eric Finster, Eilenberg-MacLane spaces in homotopy type theory, CSL-LICS ‘14 66 (2014) 1-9 [pdf text, Agda HoTT code, web discussion, doi:10.1145/2603088.2603153]

• Floris van Doorn, §42 in: On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory (2018) [arXiv:1808.10690]

• Ulrik Buchholtz, J. Daniel Christensen, Jarl G. Taxerås Flaten, Egbert Rijke, Central H-spaces and banded types [arXiv:2301.02636]

• David Wärn, Eilenberg-MacLane spaces and stabilisation in homotopy type theory, J. Homotopy Relat. Struct. 18 (2023) 357–368 [arXiv:2301.03685, doi:10.1007/s40062-023-00330-5]

Formal proof that the $K(G,-)$ form a spectrum:

• github.com/HoTT/HoTT-Agda/blob/master/homotopy/EilenbergMacLane.agda