[Agda] Data.Setoid ?

[Wolfram Kahl]

Hi Jacques,

> Does anyone have a definition of setoid equivalence?  I mean equivalence 
> between two setoids (over the same carrier set) ?

The standard library even has it for different carrier sets:

  Function.Inverse.Inverse

For the same carrier sets, you could just use relation equivalence,
which you would need to define as symmetric closure of

  Relation.Binary._⇒_


;-)


Wolfram