[Agda] standard instance proposal

[Nils Anders Danielsson]

On 2013-01-11 16:12, Serge D. Mechveliani wrote:
> It remains
>
>> (III)
>>    setoidByMap : {c c' l' : Level} -> (C : Set c) -> (B : Setoid c' l') ->
>>                                       (C -> Setoid.Carrier B) -> Setoid _ _
>>
>> builds the setoid  A  on  C  from a setoid  B  and a map
>> f : C -> Carrier B   -- in a natural way:
>> a =C a' =  f a \~~ f a'.
>>
>> (is such in the library?).

Almost. See Relation.Binary.On.

-- 
/NAD