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
$n\backslash k$
0
1
2
3
4
0
[$\pi_0(S^0)$](#pinsn)
[$\pi_0(S^1)$](#piksn)
[$\pi_0(S^2)$](#piksn)
[$\pi_0(S^3)$](#piksn)
[$\pi_0(S^4)$](#piksn)
1
$\pi_1(S^0)$
[$\pi_1(S^1)$](#pinsn)
[$\pi_1(S^2)$](#piksn)
[$\pi_1(S^3)$](#piksn)
[$\pi_1(S^4)$](#piksn)
2
$\pi_2(S^0)$
$\pi_2(S^1)$
[$\pi_2(S^2)$](#pinsn)
[$\pi_2(S^3)$](#piksn)
[$\pi_2(S^4)$](#piksn)
3
$\pi_3(S^0)$
$\pi_3(S^1)$
[$\pi_3(S^2)$](#pi3s2)
[$\pi_3(S^3)$](#pinsn)
[$\pi_3(S^4)$](#piksn)
4
$\pi_4(S^0)$
$\pi_4(S^1)$
[$\pi_4(S^2)$](#hopff)
[$\pi_4(S^3)$](#pi4s3)
[$\pi_4(S^4)$](#pinsn)
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.