[Agda] extending setoid

[Nils Anders Danielsson]

On 2013-08-07 10:37, Sergei Meshveliani wrote:
> mapSetoid : {c l l' : Level} → (A : Setoid c l) → (Y : Set l') →
>                                      (Y → Setoid.Carrier A) → Setoid l' l
> mapSetoid {c} {l} {l'} A Y f =  ...

There is something like this in Relation.Binary.On.

-- 
/NAD