Here are some links to proofs about homotopy theory, formalized in homotopy type theory. Please add! +--{: .query} 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, Evan Cavallo ## In progress ### $\pi_4(S^3)$ {#Brunerie} * 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](https://groups.google.com/d/topic/homotopytypetheory/63Nut20zfFE/discussion) 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](https://github.com/dlicata335/hott-agda/blob/master/homotopy/Hopf.agda) 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](https://github.com/HoTT/HoTT-Agda/blob/master/homotopy/SpaceFromGroups.agda) and use it to define spectra. ## At least one proof has been formalized ### Whitehead's theorem * Dan's proof for [n-types](https://github.com/dlicata335/hott-agda/blob/master/homotopy/Whitehead.agda). ### K(G,n) * Dan's [construction](https://github.com/dlicata335/hott-agda/blob/master/homotopy/KGn.agda). * $K(G,n)$ is a spectrum, [formalized](https://github.com/HoTT/HoTT-Agda/blob/master/homotopy/EilenbergMacLane.agda) ### Cohomology * [Deriving cohomology theories from spectra](https://github.com/HoTT/HoTT-Agda/blob/master/cohomology/SpectrumModel.agda) * [Mayer-Vietoris sequence](https://github.com/HoTT/HoTT-Agda/blob/master/cohomology/MayerVietoris.agda), with [exposition](http://www.contrib.andrew.cmu.edu/~ecavallo/works/mayer-vietoris.pdf) * [Cohomology of the n-torus](https://github.com/HoTT/HoTT-Agda/blob/master/cohomology/Torus.agda), 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](https://github.com/dlicata335/hott-agda/blob/master/homotopy/Freudenthal.agda) 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](https://github.com/dlicata335/hott-agda/blob/master/homotopy/FreudenthalConnected.agda) 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](https://github.com/dlicata335/hott-agda/blob/master/homotopy/PiNSN.agda) (for single-loop presentation). * Guillaume's proof (for suspension definition). * Dan's [proof from Freudenthal suspension theorem](https://github.com/dlicata335/hott-agda/blob/master/homotopy/PiSnSusp.agda) (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](https://github.com/dlicata335/hott-agda/blob/master/homotopy/Pi1S2.agda). * Dan's encode/decode-style proof [for all $k \lt n$](https://github.com/dlicata335/hott-agda/blob/master/homotopy/PiKSNLess.agda). * Dan's [proof from Freudenthal suspension theorem](https://github.com/dlicata335/hott-agda/blob/master/homotopy/PiSnSusp.agda) (for suspension definition). ### $\pi_2(S^2)$ * Guillaume's proof. * Dan's encode/decode-style [proof](https://github.com/dlicata335/hott-agda/tree/master/homotopy/pi2s2). ### $\pi_1(S^1)$ * Mike's proof by contractibility of total space of universal cover ([HoTT blog](http://uf-ias-2012.wikispaces.com/ofpost)). * Dan's encode/decode-style proof ([HoTT blog](http://homotopytypetheory.org/2012/06/07/a-simpler-proof-that-%CF%80%E2%82%81s%C2%B9-is-z/)). A [paper](http://arxiv.org/abs/1301.3443) 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](http://arxiv.org/abs/1304.0680) [Coq code](https://github.com/peterlefanulumsdaine/hott-limits/) ### Van Kampen * Mike's proofs are in the book and [Favonia formalized it](http://hott.github.com/HoTT-Agda/Homotopy.VanKampen.html). ### 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).