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.

Main sources:


Individual repos:

Some individual results:


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.

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

3 Responses to Code

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

  2. favonia says:

    Hi, my old repository (on the current list) is in Agda, not Coq. BTW, maybe we should list as well?

  3. blaisorblade says:

    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?

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s