What's this page about? Informally, a setoid is a type equipped with an equivalence relation, say "===". A morphism (of setoids) is a function such that for all x1,x2 in the domain, x1 === x2 implies f x1 === f x2 (we say it respects or preserves the equivalence).

Setoids are employed whenever Leibniz equality is too strong for your purposes. They are implemented in the Classes.* libraries.

The purpose of this page is to collect miscellaneous tips about the subject. Many of these were given by mattam on IRC.

I'll loosely collect conjectures here, so take this page with a grain of salt.