Code

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.

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

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.