Formalized Homotopy Theory (Rev #3, changes)

Showing changes from revision #2 to #3:
Added | ~~Removed~~ | ~~Chan~~ged

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.

- Guillaume proved that there is some
~~n~~~~such~~~~that~~~~π4(S3)~~~~is~~~~Z_n.~~~~With~~~~a~~~~computational~~~~interpretation,~~~~we~~~~could~~~~run~~~~this~~~~proof~~~~and~~~~check~~~~that~~~~it’s~~~~2.~~$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$.

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

- Prove that
~~K(G,n)~~~~is~~~~a~~~~spectrum~~~~(Eric?).~~$K(G,n)$ is a spectrum (Eric?). - To do cohomology with finite coefficients, all we need is the boring work of defining
~~Z/pZ~~~~as~~~~an~~~~explicit~~~~group.~~$\mathbb{Z}/p\mathbb{Z}$ as an explicit group. - Calculate some cohomology groups.

- Dan’s proof for n-types.

- Dan’s construction.

Implies~~ π_k(Sn)~~~~ =~~~~ π_k+1(Sn+1)~~~~ whenever~~~~ k~~~~ <=~~~~ 2n~~~~ -~~~~ 2~~$\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.~~$2n$-connected.

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

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

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

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

- Chris/Peter/Jeremy’s development (link?).

- Mike’s proofs are in the book and Favonia formalized it.

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

Revision on March 31, 2014 at 18:06:55 by David Roberts. See the history of this page for a list of all contributions to it.