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.)

Variants and generalizations

The notion of equivalence relation internal to a suitable category is the notion of congruence.

The generalization of this to (∞,1)-category theory is that of groupoid object in an (∞,1)-category.