Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
An equivalence relation on a set $S$ is a binary relation $\equiv$ on $S$ that is:
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, 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:
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).
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
and for all objects $a:A_0$ and $b:A_0$,
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.
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 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.
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.
set-like structure in homotopy type theory?
For the history of the notion of equivalence relation see this MO discussion.
Last revised on June 17, 2023 at 06:43:41. See the history of this page for a list of all contributions to it.