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 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 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 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.