Here are some links to proofs about homotopy theory, formalized in homotopy type theory. Please add! +--{: .query} 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. ## In progress ### π4(S3) * Guillaume proved that there is some n such that π4(S3) is Z_n. With a computational interpretation, we could run this proof and check that it's 2. ### π3(S2) * 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](https://github.com/dlicata335/hott-agda/blob/master/homotopy/Hopf.agda) with it in it. * Guillaume's proof that the total space of the Hopf fibration is S3, together with π_n(Sn), imply this by a long-exact-sequence argument, but this hasn't been formalized. ### Cohomology * Prove that K(G,n) is a spectrum (Eric?). * To do cohomology with finite coefficients, all we need is the boring work of defining Z/pZ as an explicit group. * Calculate some cohomology groups. ## At least one proof has been formalized ### Whitehead's theorem * Dan's proof for [n-types](https://github.com/dlicata335/hott-agda/blob/master/homotopy/Whitehead.agda). ### K(G,n) * Dan's [construction](https://github.com/dlicata335/hott-agda/blob/master/homotopy/KGn.agda). ### Freudenthal Suspension Theorem Implies π_k(Sn) = π_k+1(Sn+1) whenever k <= 2n - 2 * Peter's encode/decode-style proof, [formalized](https://github.com/dlicata335/hott-agda/blob/master/homotopy/Freudenthal.agda) 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](https://github.com/dlicata335/hott-agda/blob/master/homotopy/FreudenthalConnected.agda) by Dan, which shows that the relevant map is 2n-connected. ### π_n(Sn) * Dan and Guillaume's [encode/decode-style proof using iterated loop spaces](https://github.com/dlicata335/hott-agda/blob/master/homotopy/PiNSN.agda) (for single-loop presentation). * Guillaume's proof (for suspension definition). * Dan's [proof from Freudenthal suspension theorem](https://github.com/dlicata335/hott-agda/blob/master/homotopy/PiSnSusp.agda) (for suspension definition). ### π_k(Sn) for k < n * Guillaume's proof (see the book). * Dan's encode/decode-style proof [for pi^1(S^2) only](https://github.com/dlicata335/hott-agda/blob/master/homotopy/Pi1S2.agda). * Dan's encode/decode-style proof [for all k < n](https://github.com/dlicata335/hott-agda/blob/master/homotopy/PiKSNLess.agda). * Dan's [proof from Freudenthal suspension theorem](https://github.com/dlicata335/hott-agda/blob/master/homotopy/PiSnSusp.agda) (for suspension definition). ### π2(S2) * Guillaume's proof. * Dan's encode/decode-style [proof](https://github.com/dlicata335/hott-agda/tree/master/homotopy/pi2s2). ### π1(S1) * Mike's proof by contractibility of total space of universal cover ([HoTT blog](http://uf-ias-2012.wikispaces.com/ofpost)). * Dan's encode/decode-style proof ([HoTT blog](http://homotopytypetheory.org/2012/06/07/a-simpler-proof-that-%CF%80%E2%82%81s%C2%B9-is-z/)). A [paper](http://arxiv.org/abs/1301.3443) mostly about the encode/decode-style proof, but also describing the relationship between the two. * Guillaume's proof using the flattening lemma. ### Homotopy limits * Chris/Peter/Jeremy's development (link?). ### Van Kampen * Mike's proofs are in the book and [Favonia formalized it](http://hott.github.com/HoTT-Agda/Homotopy.VanKampen.html). ### Covering spaces * Favonia's proofs (link in flux due to library rewrite). ### Blakers-Massey * Favonia/Peter/Guillaume/Dan's formalization of Peter/Eric/Dan's proof (link in flux due to library rewrite).