[Agda] Data.Setoid ?

Wolfram Kahl kahl at cas.mcmaster.ca
Thu Nov 22 23:36:51 CET 2012

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:


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




More information about the Agda mailing list