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

Thus, an equivalence relation is a symmetric preorder.

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

If $R$ is any relation on $S$, there is a smallest equivalence relation containing $R$ (noting that an intersection of an arbitrary family of equivalence relations is again such; see also Moore closure), called the equivalence relation generated by $R$.

In homotopy type theory

In homotopy type theory, since propositions are subsingletons, an equivalence relation on a type $T$ is a type family $x \equiv y$ indexed by elements $x:T$ and $y:T$ with witnesses of reflexivity, transitivity, and symmetry, and propositional truncation:

$$\mathrm{refl}(x):x \equiv x$$

$$\mathrm{trans}(x, y, z):x \equiv y \times y \equiv z \to x \equiv z$$

$$\mathrm{sym}(x, y):x \equiv y \to y \equiv x$$

$$\mathrm{proptrunc}(x, y):\prod_{p:x \equiv y} \prod_{q:x \equiv y} p = q$$

One then further distinguishes between a type with an equivalence relation (a symmetric preordered type) and an h-set with an equivalence relation (a symmetric proset).

Extensional functions

Let $A \coloneqq (A_0, \equiv_A)$ and $B:\coloneqq (B_0, \equiv_B)$ be two symmetric preordered types. An extensional function $f:A \to B$ consists of a function $f_0:A_0 \to B_0$ and for all elements $a:A_0$ and $b:A_0$ a function $f_\equiv(a, b):(a \equiv_A b) \to (f_0(a) \equiv_B f_0(b))$.

The identity function $id_A:A \to A$ is an extensional function which consists of the identity function $id_{A_0}:A_0 \to A_0$ for all elements $a:A_0$ and $b:A_0$, the identity function $id_\equiv(a, b):(a \equiv_A b) \to (a \equiv_A b))$.

Given symmetric preordered types $A \coloneqq (A_0, \equiv_A)$, $B:\coloneqq (B_0, \equiv_B)$, and $C \coloneqq (C_0, \equiv_C)$, the composition $g \circ f:A \to C$ of extensional functions $f:A \to B$ and $g:B \to C$ is defined as

$$(g \circ f)_0 \coloneqq g_0 \circ f_0$$

and for all objects $a:A_0$ and $b:A_0$,

$$(g \circ f)_\equiv(a, b) \coloneqq g_equiv(f_0(a), f_0(b)) \circ f_equiv(a, b)$$

Injections, surjections, and bijections

An extensional function $f:A \to B$ is a injection if for all elements $b:B_0$ the type of elements $a:A_0$ with a witness $p(a, b):f_0(a) \equiv b$ is a subsingleton.

An extensional function $f:A \to B$ is a surjection if for all elements $b:B_0$ the type of elements $a:A_0$ with a witness $p(a, b):f_0(a) \equiv b$ is a pointed type.

An extensional function $f:A \to B$ is a bijection if it is both an injection and a surjection; i.e. for all elements $b:B_0$ the type of elements $a:A_0$ with a witness $p(a, b):f_0(a) \equiv b$ is a pointed subsingleton, or a singleton.

Bijections, isomorphisms, and equivalences

An extensional function $f:A \to B$ is a bijection if for all elements $b:B_0$ the type of elements $a:A_0$ with a witness $p(a, b):f_0(a) \equiv b$ is a singleton.

An extensional function $f:A \to B$ is an isomorphism if there exist an extensional functiom $g:B \to A$ with witnesses $\mathrm{ret}(f, g):g \circ f = id_{A}$ and $\mathrm{sec}(f, g):f \circ g = id_{B}$.

An extensional function $f:A \to B$ is an equivalence if the function $f_0:A_0 \to B_0$ is an equivalence of types and for all elements $a:A_0$ and $b:A_0$ the function $f_\equiv(a, b):(a \equiv_A b) \to (f_0(a) \equiv_B f_0(b))$ is an equivalence of types.

The only symmetric preordered types for which bijection, isomorphism, and equivalence are the same are the symmetric posets, which are the h-sets.

A categorical view

A set equipped with an equivalence relation can be regarded as a groupoid enriched over the cartesian monoidal category of truth values. Equivalently, it 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 set with an equivalence relation 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 set with an equivalence relation 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).

A set equipped with an equivalence relation is sometimes called a setoid, see there for more.

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

• Bishop set

• congruence

• complete loop graph

• stable equivalence relation

• pseudo-equivalence relation

• quotient equivalence relation

• enriched set

• monoidal symmetric proset

• set-like structure in homotopy type theory?

• tolerance relation

References

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