nLab
equivalence relation

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. (However, we should be cautious with this terminology, since the people who typically use setoids begin with an impoverished notion of set and then introduce setoids specifically to fix this, as described below.)

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. Equivalently, a setoid is a (0,1)-category whose each morphism is iso, or a symmetric preordered set.

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

• A partial equivalence relation is a symmetric and transitive relation.

• A congruence is a notion of equivalence relation internal to a suitable category.

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

Related concepts

• setoid

• congruence

References

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