The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi Robin

On 2 Jun 2008, at 15:24, Robin Green wrote:

> On Mon, 2 Jun 2008 15:07:24 +0100
> Conor McBride 
> <conor AT strictlypositive.org>
>  wrote:
>
> > PS In the last few days, I've managed to
> > construct the extensional universe from
> > "Observational Equality, Now!" (Altenkirch,
> > McBride, Swierstra, 2007) in Coq. By
> > reflecting on this universe, one can build
> > an equality which is extensional and
> > substitutive, whilst retaining canonicity
> > for datatypes.
>
> I'd be interested in using this. Is a public release expected soon?

We're hoping to write about it sooner rather than
later. I'm happy to attach the file here. I don't
know how useful it is in its current state. What's
in it:

  * a treatment of the universe with 0, 1, 2, Pi,
    Sigma, and W, presented via the usual
    (size inflating) trick for encoding induction
    recursion; the only large elimination is "big
    if" for 2.
  * the identification of a propositional
    fragment of that universe
  * the presentation of equality for sets in the
    universe and for values in those sets
  * the implementation of coercion between equal
    sets

The crucial point is that computation is only
strict in proofs when eliminating absurditity,
so we are free to add *propositional* axioms
as long as they are consistent, without breaking
the canonicity property for *sets*. We use this
freedom wherever it saves us work, as well as
in places where we're asserting extensional
equations.

I haven't yet given the example of Nat with
its induction principle yet, but it worked ok
when we did the corresponding thing in Agda 2.

Our motivation is metatheoretical. What we get
out of this work is a simulation of the
evaluation behaviour of Observational Type
Theory in Coq. I wouldn't care to predict
whether this development would be especially
useful as a library, but you're welcome to
whatever it may bring you.

All the best

Conor

Attachment: ott.v
Description: Binary data