Here's a quick reference for the state of the art on homotopy groups of spheres in HoTT. Everything listed here is also discussed on the page on [[Formalized Homotopy Theory]]. ## In progress ### π4(S3) * Guillaume has proved that there exists an n such that π4(S3) is Z_n, and given a computational interpretation, we could run this proof and check that n is 2. ### π3(S2) * Peter L. has constructed 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. ## At least one proof has been formalized ### 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 two n-connected types. ### π_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) (for single-loop presentation). * 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 using the total space the Hopf fibration. * 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.