[Agda] Quotient types in Agda, if you Trust Me

[Andrew Pitts]

Wouldn't it be nice to have quotient types in Agda?

By quotient types I mean that given any type A : Set and any relation
R : A -> A -> Set, there should be a type A / R : Set and a function
_mod R : A -> A / R for which there is a proof
equ : {x y : A}(r : R x y) -> x mod R ≡ y mod R and which is
category-theoretically universal, in a suitable sense, with this
property.

One can use such types to avoid "setoid hell". And they make function
extensionality derivable.

I am happy to have this just for h-sets, that is, to have something
that works when we allow Agda to use full dependent pattern matching
and hence can prove uniqueness of identity proofs.

The attached file (quotient.agda) is a way of providing such quotient
types using an enhanced version of Dan Licata's trick with "private"
and "postulate" declarations to define an interval type

<http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/>

The enhancements are two-fold:

1. Use primTrustMe rather than postulates for improved computational
behaviour, inspired by Alan Jeffrey's recent post to this list:

<https://groups.google.com/forum/#!topic/homotopytypetheory/hTAVT6CGbrs>

2. Careful combination of thunking and private declarations to ensure
(we hope!) that the function _mod R : A -> A / R sending an element to
its equivalence class cannot be proved to be an injection outside the
scope of the private declarations. (It is injective with the private
declations, and if it could be proved injective outside their scope,
one can easily derive a logical contradiction.) This is adapted from
the hott-agda development

<https://github.com/dlicata335/hott-agda/blob/master/lib/spaces/hithacks.agda>

of Dan Licata, Guillaume Brunerie, Eric Finster and Dan Grayson. The
"thunking Yoga" used to avoid logical inconsistency in quotient.agda at
first seems more complicated than it need be. But we (Dan Licata, Alan
Jeffrey and I) were able to break simpler schemes.

So here's a challenge.

Can anyone fill the hole in

open import quotient

data Empty : Set where

contradiction : Empty
contradiction = {!!}

without any further use of primTrustMe or postulate?

Or convince me that that is not possibe?

Andy Pitts
-------------- next part --------------
A non-text attachment was scrubbed...
Name: quotient.agda
Type: application/octet-stream
Size: 11234 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20150513/8515f0e1/quotient.obj