Equivalence relations

Definition

An equivalence relation on a set $S$ is a binary relation $\equiv$ on $S$ that is:

• reflexive: $x \equiv x$ for all $x: S$;
• symmetric: $x \equiv y$ if $y \equiv x$; and
• transitive: $x \equiv z$ if $x \equiv y \equiv z$.

(One can also define it as a relation that is both reflexive and euclidean.) The dual of an equivalence relation is an apartness relation.

Setoids

A setoid is a set equipped with an equivalence relation.

Equivalently, a setoid is a groupoid enriched over the cartesian monoidal category of truth values. Equivalently, a setoid is a groupoid that is 0-truncated. Then the equivalence relation on $S$ is a way of making $S$ into the set of objects of such a groupoid.

It may well be useful to consider several possible equivalence relations on a given set. When considering a single equivalence relation once and for all, however, it is common to take the quotient set $S/{\equiv}$ and use that instead. As a groupoid, any setoid is equivalent to a set in this way (although in the absence of the axiom of choice, it is only a “weak” or ana-equivalence).

Setoids are still important in foundations of mathematics where quotient sets don't always exist and the above equivalence cannot be carried out. However, arguably this is a terminological mismatch, and such people should say ‘set’ where they say ‘setoid’ and something else (such as ‘preset’, ‘type’, or ‘completely presented set’) where they say ‘set’. (See page 9 of these lecture notes.)

References

For the history of the notion of equivalence relation see this MO discussion.

Revised on July 1, 2013 10:15:07 by Urs Schreiber (89.204.139.146)