cohomology * To do cohomology with finite coefficients, all we need is the boring work of defining $\mathbb{Z}/p\mathbb{Z}$ as an explicit group. * Calculate some more cohomology groups. * Compute the loop space of this construction and use it to define spectra.

Peter’s encode/decode-style proof, formalized by Dan, using a clever lemma about maps out of 2 n-connected types. This is the “95%” version, which shows that the relevant map is an equivalence on truncations.

The full “100%” version, formalized by Dan, which shows that the relevant map is $2n$-connected.

Homotopy limits

Jeremy Avigad, Chris Kapulkin and Peter Lumsdaine arXivCoq code