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

[Dan Licata]

Nice! 

I think this works because the quotient type has only one constructor, and because Andy defined the private datatype as a record: you need to know that 

g = (#in (λ _ → #in (#out (g unit))) at type # (Unit → # A)

When we do higher inductive types (see the hithacks.agda linked below), I think you need the propositional funext, because the elimination rule will match on the private datatype.


BTW, a bit more on the motivation for the tricks in hithacks.agda: what I really want is a private datatype for which nothing is exported besides the public declarations in the module.  However, some of the analyses that Agda does break this abstraction---in particular, injectivity and disjointness of constructors (for the datatype) and unused argument analysis (for the eliminator).  The thunking and "phantom" datatype are meant to disable these analyses---e.g. Agda seems unwilling to let you split an equality in unit->A where it would let you split the corresponding equality in A.  This is a twist on a hack for disabling injectivity and disjointness that is described in
https://github.com/HoTT/HoTT-Agda/blob/master/lib/types/HIT_README.txt
which Agda now seems to be immune to.  

Would the Agda maintainers be willing to accept a patch that added a less hacky way to disable these analyses?  E.g.

{-# NO_INJECTIVITY_OR_DISJOINTNESS #-}
datatype I = Zero  | One
(Now Zero and One are treated like variables instead of constructors for the purposes of injectivity/disjointness)

{-# NO_UNUSED_ARGUMENT_ANALYSIS #-}
f : A -> B -> C
f x _ = … 
(second argument is treated as relevant even though it is not).

It would be nice for those of us who use Agda for HoTT to have an official way to disable these analyses, rather than having to invent new workarounds as Agda's analyses improve.

Also, are there other analyses we should be worried about?

-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