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

[Matteo Acerbi]

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