Homotopy Type Theory
Eilenberg-MacLane Spaces in Homotopy Type Theory

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


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 GG, an EilenbergMacLane space K(G,n)K(G,n) is a space (type) whose n thn^{th} homotopy group? is GG, 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 GG. 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

category: reference

Last revised on October 12, 2018 at 10:31:26. See the history of this page for a list of all contributions to it.