[Agda] quotient types

[Ondrej Rypacek]

Thanks,
I've started using them. I have one syntactical issue though, which is
I guess a more general misunderstanding.

Relation.Binary.Setoid defines a binary operator _≈_ for the
equivalence. But how do I use it as an operator?
I end up writing something like

_≈_ S x y

all the time anyway. I'd like to write x ≈ y , but how to bring S (the
setoid) into the context ?

Cheers,
Ondrej



On 30 November 2010 16:58, Nils Anders Danielsson <nad at cs.nott.ac.uk> wrote:
> On 2010-11-30 13:07, Ondrej Rypacek wrote:
>>
>> What is the best way to approximate quotients in Agda?
>
> One option is to use setoids. The standard library uses setoids quite a
> lot.
>
> --
> /NAD
>