An important aspect of HoTT is the fact that intensional Martin-Löf type theory has a computational implementation in proof assistants like Coq and Agda. This forms the basis of Vladimir Voevodsky’s Univalent Foundations program, which uses proof assistants 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.
Some individual results:
- 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.
- The Agda section of the HoTT repository.
- Dan Licata’s GitHub repository.
- Favonia’s GitHub repository.
- Nils Anders Danielsson and Thierry Coquand’s Agda code (HTML listings here).
To add something to this list, just leave a reply below.