Setoids

root edited this page Oct 11, 2017 · 4 revisions

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.

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.