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.

### Coq

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:

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

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.

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

### Agda

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.

Pingback: Unifying Programming and Math – The Dependent Type Revolution | Atomic Spin

Hi, my old repository (on the current list) is in Agda, not Coq. BTW, maybe we should list https://github.com/HoTT/HoTT-Agda as well?

I’m just an Agda user, so not an expert on foundations of mathematics AFAIK, –without-K significantly limit the use of type refinement in pattern matching, one important convenience of using Agda. Can HoTT be used as a foundation for Agda reasoning? Does one need to an embedding of standard type theory inside HoTT to justify that? How annoying is that, during practical Agda usage?