equivalence relation

Equivalence relations


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

  • reflexive: xxx \equiv x for all x:Sx: S;
  • symmetric: xyx \equiv y if yxy \equiv x; and
  • transitive: xzx \equiv z if xyzx \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.


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 SS is a way of making SS 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/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


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

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