Homotopy Type Theory
Eilenberg-MacLane Spaces in Homotopy Type Theory

Eilenberg-MacLane Spaces in Homotopy Type Theory. Dan Licata and Eric Finster, LICS 2014

Links

• Dan’s link
• Eric’s link
• and code

Abstract

Homotopy type theory is an extension of Martin-Löf type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs of homotopy-theoretic theorems, in a way that is very amenable to computer-checked proofs in proof assistants such as Coq and Agda. In this paper, we give a computer-checked construction of Eilenberg-MacLane spaces. For an abelian group $G$, an EilenbergMacLane space $K(G,n)$ is a space (type) whose $n^{th}$ homotopy group? is $G$, and whose homotopy groups are trivial otherwise. These spaces are a basic tool in algebraic topology; for example, they can be used to build spaces with specified homotopy groups, and to define the notion of cohomology with coefficients in $G$. Their construction in type theory is an illustrative example, which ties together many of the constructions and methods that have been used in homotopy type theory so far.

See also

• References
• Eilenberg-Mac Lane space
• Synthetic homotopy theory

category: reference