Here are some links to proofs about homotopy theory, formalized in homotopy type theory. Please add!
Maybe we could figure out a way not to duplicate stuff between this page and homotopy groups of spheres?
Cast of characters so far: Jeremy Avigad, Guillaume Brunerie, Favonia, Eric Finster, Chris Kapulkin, Dan Licata, Peter Lumsdaine, Mike Shulman, Evan Cavallo
In progress
Guillaume proved that there is some such that is . With a computational interpretation, we could run this proof and check that .
On 14 February 2016 Guillaume announced a proof that , via a proof involving the Thom construction and Gysin sequences.
Peter’s construction of the Hopf fibration as a dependent type. Lots of people around know the construction, but I don’t know anywhere it’s written up. Here’s some Agda code with it in it.
Guillaume’s proof that the total space of the Hopf fibration is , together with , imply this by a long-exact-sequence argument, but this hasn’t been formalized.
Cohomology
To do cohomology with finite coefficients, all we need is the boring work of defining 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 -connected.