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
Guillaume has proved that there exists an such that is . Given a computational interpretation, we could run this proof and check that is 2.
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, but this hasn’t been formalized.
At least one proof has been formalized
Freudenthal Suspension Theorem
Implies whenever
Peter’s encode/decode-style proof, formalized by Dan, using a clever lemma about maps out of two n-connected types.