Eilenberg-MacLane Spaces in HoTT

Eilenberg-MacLane Spaces in HoTT

For those of you who have been waiting with bated breath to find out what happened to your favorite characters after the end of Chapter 8 of the HoTT book, there is now a new installment:

Eilenberg-MacLane Spaces in Homotopy Type Theory
Dan Licata and Eric Finster
To appear at LICS 2014; pre-print available here.
Agda available here.

Homotopy type theory is an extension of Martin-Lof 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 Eilenberg-MacLane space K(G,n) is a space (type) whose nth 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.

The Agda formalization of this result was actually done last spring at IAS; the only thing new in the paper is the “informalization” of it.  This write-up would have gone in Chapter 8 of the book, but we ran out of time on the book before writing it up.  Overall, I like how this example builds on and ties together a bunch of different techniques and lemmas (e.g. encode-decode gets used a few different times; Peter Lumsdaine’s connectedness lemmas that went into the proof of the Freudenthal suspension theorem gets used, as does Freudenthal itself).  When doing the proof, it was kind of fun to actually get to use some lemmas, since most of the previous proofs had required inventing and developing large chunks of library code.