This forms the basis of Vladimir Voevodsky’s Univalent Foundations program, which uses Coq to generate and verify proofs with homotopical content. Collected here are various resources for working (and playing) with HoTT in Coq, mostly hosted at GitHub. See the resources below for examples, and for instructions on how to set up your own Coq system and GitHub repository so you can get Coqing and share the results.
- Andrej Bauer’s Coq tutorials.
- Andrej’s GitHub repository, including useful tactics and lovely CoqDoc documentation.
- Peter LeFanu Lumsdaine’s GitHub repository.
- Favonia’s GitHub repository.
- Jeremy Avigad’s Coq proof that the higher homotopy groups are abelian, adapted from Dan Licata’s Agda proof. (See Dan’s March 26 blog post.)
- Mike Shulman’s proof that is correct. (See Mike’s post.)
- A repository of files for Inductive types in HoTT, by Steve Awodey, Nicola Gambino, and Kristina Sojakova. (See this post.)
Another proof assistant is Agda. Agda includes some more advanced features than Coq, but lacks a tactic language; also one must use the option --without-K for consistency with homotopy type theory. Here are some links to Agda code implementing aspects of homotopy type theory.
- Nils Anders Danielsson and Thierry Coquand’s Agda code (HTML listings here), which proves (among other things) that Ωn is abelian for n≥2.
To add something to this list, just leave a reply below.