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.
Guillaume has proved that there exists an Guillaume Brunerie has proved that there exists an such that such that is is . Given a computational interpretation, we could run this proof and check that . Given a computational interpretation, we could run this proof and check that is 2. Added June 2016: Brunerie now has a proof that is 2. Added June 2016: Brunerie now has a proof that , using cohomology calculations and a Gysin sequence argument.
At least one proof has been formalized
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 Peter LeFanu Lumsdaine 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 with it in it.
Guillaume’s proof that the total space of the Hopf fibration is Guillaume Brunerie’s proof that the total space of the Hopf fibration is , together with , together with , imply this by a long-exact-sequence argument.
Peter’s encode/decode-style proof, Peter LeFanu Lumsdaine’s encode/decode-style proof, formalized by Dan, using a clever lemma about maps out of two n-connected types.Dan Licata, using a clever lemma about maps out of two n-connected types.
Guillaume’s proof using the total space the Hopf fibration.Guillaume Brunerie’s proof using the total space the Hopf fibration.
Dan’s encode/decode-style Dan Licata’s encode/decode-style proof.
Mike’s proof by contractibility of total space of universal cover (Mike Shulman’s proof by contractibility of total space of universal cover (HoTT blog).
Dan’s encode/decode-style proof (Dan Licata’s encode/decode-style proof (HoTT blog). A paper mostly about the encode/decode-style proof, but also describing the relationship between the two.
Guillaume’s proof using the flattening lemma.Guillaume Brunerie’s proof using the flattening lemma.