Code

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

Main sources:

• Vladimir Voevodsky’s GitHub repository (the original source).
• The HoTT GitHub repository.

Tutorials:

• Andrej Bauer’s Coq tutorials.

Individual repos:

• Andrej’s GitHub repository, including useful tactics and lovely CoqDoc documentation.
• Peter LeFanu Lumsdaine’s GitHub repository.
• Favonia’s GitHub repository.

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.

• Nils Anders Danielsson and Thierry Coquand’s Agda code (HTML listings here), which proves (among other things) that Ωⁿ is abelian for n≥2.

To add something to this list, just leave a reply below.