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]]? 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 Cavallo]] ## In progress ### Cohomology [[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) [[Eilenberg-MacLane space]] * 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 [[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 [[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. ### 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 [[van Kampen theorem]] * Mike's proofs are in the book and [Favonia formalized it](http://hott.github.com/HoTT-Agda/Homotopy.VanKampen.html). {{deadlink}} ### Covering spaces [[Covering space]] * Favonia's proofs (link in flux due to library rewrite). ### Blakers-Massey [[Blakers-Massey theorem]] * Favonia/Peter/Guillaume/Dan's formalization of Peter/Eric/Dan's proof (link in flux due to library rewrite). category: homotopy theory