_Eilenberg-MacLane Spaces in Homotopy Type Theory_. [[Dan Licata]] and [[Eric Finster]], LICS 2014 ## Links ## * [Dan's link](http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf) * [Eric's link](http://ericfinster.github.io/files/emhott.pdf) * and [code](https://github.com/dlicata335/hott-agda/blob/master/homotopy/KGn.agda) ### 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