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

Showing changes from revision #5 to #6: 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?

Cast of characters so far: Jeremy Avigad, Guillaume Brunerie, Favonia, Eric Finster, Chris Kapulkin, Dan Licata, Peter Lumsdaine, Mike Shulman. 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.

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

Cohomology

  • Prove To that do cohomology with finite coefficients, all we need is the boring work of defining K ( / G p,n) K(G,n) \mathbb{Z}/p\mathbb{Z} is as a an spectrum explicit (Eric?). group.
  • To Calculate do some more cohomology with groups. finite coefficients, all we need is the boring work of defining/p\mathbb{Z}/p\mathbb{Z} as an explicit group.
  • Calculate Compute some the cohomology loop groups. space ofthis construction and use it to define spectra.

At least one proof has been formalized

Whitehead’s theorem

K(G,n)

Cohomology

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

Blakers-Massey

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

Revision on March 1, 2015 at 01:13:41 by ecavallo?. See the history of this page for a list of all contributions to it.