Setoids
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.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.