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

[Dan Licata]

PS: I should say that implementing quotients using this trick does not give you something that is  really computationally nice (like quotients in OTT, for example)---there are still stuck non-reflexivity equality proofs, and transport etc. will get stuck on those.  But it is easier to work with than using only axioms, because the eliminator computes definitionally on the points of the type (but not on the paths).  

-Dan

On May 13, 2015, at 9:58 AM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> Computationally nice quotients in Agda would be great!
> 
> I don't know how it impacts the safeness of this encoding, but your
> #unit-fun-ext is provable just by refl, since Agda has eta rules for
> record types.
> 
> This also means that you don't need the transport in the definition of elim.
> 
> Best,
> Andrea
> 
> 
> On Wed, May 13, 2015 at 3:00 PM, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk> wrote:
>> 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
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda