Eilenberg-MacLane Spaces in Homotopy Type Theory (Rev #3, changes)

Showing changes from revision #2 to #3:
Added | ~~Removed~~ | ~~Chan~~ged

*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 $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.

category: reference

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