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

[Dan Licata]

Hi Matteo,

Oops, the second datatype and the #out and #in functions were supposed to be indented into the private block, but they weren't.  I think the updated version on github prevents this problem?

Assuming the injectivity/disjointness analyses could be disabled, how would your proposal for private pattern matching be different than a private datatype?

-Dan

On May 13, 2015, at 11:05 AM, Matteo Acerbi <matteo.acerbi at gmail.com> wrote:

> On Wed, May 13, 2015 at 3:00 PM, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk> wrote:
>> 
>> [..]
>> 
>> 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?
>> 
>> [..]
> 
> After commenting out the open holes in hithacks.agda, on my system
> (Agda 7b727e0) this is accepted:
> 
> module challenge where
> 
> open import hithacks
> 
> txe : ∀ {l1}{X : Set l1}{l2}{Y : X → Set l2}{f g : (x : X) → Y x} →
>        f == g → ∀ x → f x == g x
> txe id _ = id
> 
> contradiction : Void
> contradiction = ne (txe (ap (λ f x → f x) (ap #out (seg <>))) _)
>  where open Private
>        ne : _ → Void
>        ne ()
> 
> At AIM XX I proposed to add the possibility to define datatypes and
> functions over
> them inside a specially marked block, while disabling pattern matching
> for them outside
> the block.
> 
> Do you agree this could be an useful feature?
> 
> I don't know whether it would be difficult to implement: for sure, I
> don't know how to
> implement that myself. :-)
> 
> Best,
> Matteo
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda