An intensional dependent type theory called the Calculus of Inductive Constructions (CIC) has implementations in proof assistants such as Coq and Agda. The Martin-Lof type theory can be seen as a fragment of CIC. The standard univalent model that allows one to use MLTT to formalize abstract mathematics in the univalent style has been informally checked to extend to some of the subsets of CIC.

The question of whether a standard univalent model can be extended to all of the CIC is open and somewhat fluid since the the type theory that is implemented in Coq and in even greater degree in Agda is changing from one release to another.

This situation led to the development of two different approaches to univalent formalization of mathematics in Coq and Agda.

The UniMath library uses only the MLTT fragment of the CIC (with some exceptions in the Ktheory library). This however makes it impossible to carry through some important constructions such as the set quotients of types without running into an increase of complexity due to the way the universes are managed in Coq. To circumvent this problem while waiting for the changes in the universe management that will allow to use Resizing Rules the UniMath library uses type-in-type patch that is expected to become an off-the-shelf option in Coq 8.5.

The HoTT library took the opposite approach of using freely all of the features of the CIC and adding to them more features that can be broadly described as experiments with various approaches to higher inductive types. One of the main directions of current work in HoTT is the development of an infrastructure that will allow to formally certify new features for their compatibility with the standard model.


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 Foundations  GitHub repository (this is the original source that is not updated anymore, the main Foundations library is now a part of UniMath).
  • UniMath GitHub repository that contains libraries Foundations, RezkCompletion, Ktheory and PAdics.


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.

5 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?

  4. Ali Caglayan says:

    We should add the Lean implementation (maybe even the Spectral library).

  5. GeoffChurch says:

    “Jeremy Avigad’s [Coq proof] that the higher homotopy groups are abelian” is a dead link

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 )

Connecting to %s