UF IAS 2012 Archive Coq Working Group

Here is the current state of Coq for HoTT.

Matthieu Sozeau and Hugo Herbelin implemented two command-line options for the trunk version of Coq that replace some of the patches:

The option -warn-universe-inconsistency turns universe inconsistencies into warnings rather than errors.
The option -relevant-equality conforms the interpretation of universe levels in inductive types to the homotopy interpretation.

Matthieu is working on better universe polymoprhism which will eliminate the need for the first option (which is a hack).

Andrej Bauer wrote configuration scripts for the HoTT library that use autoconf. This makes the library a bit easier to install. The library however requires the latest version of Coq with the new command line options.

There is an ongoing effort to put the ssreflect tactics (just the tactics, no math components) into HoTT, but we’re meeting some technical difficulties.

The Coq working group meets on Wednesday 1:30 — 3 and is occasionally used for some talks.

A page on type classes