Showing changes from revision #3 to #4:
Added | Removed | Changed
Eilenberg-MacLane Spaces in Homotopy Type Theory
< . Eilenberg-MacLane Spaces in Homotopy Type TheoryDan 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 , an EilenbergMacLane space is a space (type) whose homotopy group? is , 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 . 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.