Homotopy Type Theory Formalized Homotopy Theory > history (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!

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

$\pi_4(S^3)$

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

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

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

Cohomology

• To do cohomology with finite coefficients, all we need is the boring work of defining $\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

• Dan’s proof for n-types.

K(G,n)

• Dan’s construction.
• $K(G,n)$ is a spectrum, formalized

Cohomology

• Deriving cohomology theories from spectra
• Mayer-Vietoris sequence, with exposition
• Cohomology of the n-torus, which could be easily extended to any finite product of spheres.

Freudenthal Suspension Theorem

Implies $\pi_k(S^n) = \pi_{k+1}(S^{n+1})$ whenever $k \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 $2n$-connected.

$\pi_n(S^n)$

• Dan and Guillaume’s encode/decode-style proof using iterated loop spaces (for single-loop presentation).
• Guillaume’s proof (for suspension definition).
• Dan’s proof from Freudenthal suspension theorem (for suspension definition).

$\pi_k(S^n)$ for $k \lt n$

• Guillaume’s proof (see the book).
• Dan’s encode/decode-style proof for $\pi_1(S^2)$ only.
• Dan’s encode/decode-style proof for all $k \lt n$.
• Dan’s proof from Freudenthal suspension theorem (for suspension definition).

$\pi_2(S^2)$

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

$\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

• Mike’s proofs are in the book and Favonia formalized it. {{deadlink}}

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