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.
Table
0
1
2
3
4
0
1
2
3
4
In progress
Guillaume Brunerie has proved that there exists an such that is . Given a computational interpretation, we could run this proof and check 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 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 Brunerie’s proof that the total space of the Hopf fibration is , together with , imply this by a long-exact-sequence argument.
Mike Shulman’s proof by contractibility of total space of universal cover (HoTT blog).
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.