Homotopy Type Theory
Formalized Homotopy Theory (Rev #11, changes)

Showing changes from revision #10 to #11: Added | Removed | Changed

Here are some links to proofs about homotopy theory, formalized in homotopy type theory. Please add!

Maybe we could figure out a way not to duplicate stuff between this page and homotopy groups of spheres?

Ali: Results about homotopy groups of spheres should go there, everything else here.

Cast of characters so far: Jeremy Avigad, Guillaume Brunerie, Favonia, Eric Finster, Chris Kapulkin, Dan Licata, Peter Lumsdaine, Mike Shulman, Evan CavalloJeremy Avigad, Guillaume Brunerie, Favonia, Eric Finster, Chris Kapulkin, Dan Licata, Peter Lumsdaine, Mike Shulman, Evan Cavallo

In progress

π 4(S 3)\pi_4(S^3)

  • Guillaume proved that there is some nn such that π 4(S 3)\pi_4(S^3) is /n\mathbb{Z}/n\mathbb{Z}. With a computational interpretation, we could run this proof and check that n=2n=2.

  • On 14 February 2016 Guillaume announced a proof that n=2n=2, via a proof involving the Thom construction and Gysin sequences.

π 3(S 2)\pi_3(S^2)

  • Peter’s construction of 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 S 3S^3, together with π n(S n)\pi_n(S^n), imply this by a long-exact-sequence argument, but this hasn’t been formalized.


  • To do cohomology with finite coefficients, all we need is the boring work of defining /p\mathbb{Z}/p\mathbb{Z} as an explicit group.
  • Calculate some more cohomology groups.
  • Compute the loop space of this construction and use it to define spectra.

At least one proof has been formalized

Whitehead’s theorem



Freudenthal Suspension Theorem

Implies π k(S n)=π k+1(S n+1)\pi_k(S^n) = \pi_{k+1}(S^{n+1}) whenever k2n2k \leq 2n - 2

  • Peter’s encode/decode-style proof, formalized by Dan, using a clever lemma about maps out of 2 n-connected types. This is the “95%” version, which shows that the relevant map is an equivalence on truncations.
  • The full “100%” version, formalized by Dan, which shows that the relevant map is 2n2n-connected.

π n(S n)\pi_n(S^n)

π k(S n)\pi_k(S^n) for k<nk \lt n

π 2(S 2)\pi_2(S^2)

  • Guillaume’s proof.
  • Dan’s encode/decode-style proof.

π 1(S 1)\pi_1(S^1)

  • Mike’s proof by contractibility of total space of universal cover (HoTT blog).
  • Dan’s encode/decode-style proof (HoTT blog). A paper mostly about the encode/decode-style proof, but also describing the relationship between the two.
  • Guillaume’s proof using the flattening lemma.

Homotopy limits

  • Jeremy Avigad, Chris Kapulkin and Peter Lumsdaine arXiv Coq code

Van Kampen

Covering spaces

  • Favonia’s proofs (link in flux due to library rewrite).


  • Favonia/Peter/Guillaume/Dan’s formalization of Peter/Eric/Dan’s proof (link in flux due to library rewrite).

category: homotopy theory

Revision on January 19, 2019 at 12:54:05 by Ali Caglayan. See the history of this page for a list of all contributions to it.