UF IAS 2012 Archive
HomotopyGroupsOfSpheres

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

π4(S3)

π3(S2)

At least one proof has been formalized

Freudenthal Suspension Theorem

Implies π_k(Sn) = π_k+1(Sn+1) whenever k <= 2n - 2

π_n(Sn)

π_k(Sn) for k < n

π2(S2)

π1(S1)

A paper mostly about the encode/decode-style proof, but also describing the relationship between the two.

Created on April 19, 2018 at 17:16:58 by Univalent foundations special year 2012