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

[Andrew Pitts]

Dear Andrea,

On 13 May 2015 at 14:58, 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.

Oh yes -- silly me. (Incidentally Agsy (C-c C-a) can't see that for
some reason.)

So that's one of the two uses of primTrustMe eliminated. Can you get
rid of the other one? :-)

Updated quotient.agda attached.

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