The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Thank you both for answers - Bas and Roman!

On Fri, Mar 24, 2017 at 1:35 PM, Roman <effectfully AT gmail.com> wrote:

Hi. I'm the author of that Agda library. AFAIK there is no real
implementation of OTT. Epigram 2 could be one, but it was never
released. The Francesco Mazzoli's thesis ([1]) is about building a
proof assistant around OTT, but:

> The author learnt the hard way the implementation challenges for such a project, and ran out of time while implementing observational equality. While the constructs and typing rules are present, the machinery to make it happen (equality reduction, coercions, quotation, etc.) is not present yet.

There is also an Agda formalization (my library is not a
formalization) by Conor McBride ([2]), but it's not a usable eDSL (and
has no user-defined data types).

You can use my library for simple things that involve just sigma, pi,
universes, top and bottom, but I use my own version of descriptions,
so in order to introduce new data types into the OTT universe you'll
have to study that generic programming machinery. Inductive families
are supported as well, but are hard to use, because Agda's unification
is nailed to definitional equality, so you have to manually take care
of all the observational unification constraints (see [3]).

All in all, if you want to write something serious with OTT, there
doesn't seem to be an implementation. If you want to feel a taste of
OTT, my library should be fine. In the latter case feel free to ask
questions, I don't have much time now, but I'll try to help.

[1] http://www.doc.ic.ac.uk/teaching/distinguished-projects/2013/f.mazzoli.pdf
[2] http://mazzo.li/epilogue/index.html%3Fp=1098.html
[3] http://stackoverflow.com/questions/38957229/pattern-matching-in-observational-type-theory