Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
In a finitely complete category $C$, a congruence on an object $X$ is an internal equivalence relation on $X$.
This means that it consists of a subobject of the product $R \subseteq X \times X$ equipped with the following morphisms:
internal reflexivity: $r \colon X \to R$ which is a section both of $p_1$ and of $p_2$;
internal symmetry: $s \colon R \to R$ which interchanges $p_1$ and $p_2$, namely $p_1\circ s = p_2$ and $p_2\circ s = p_1$;
internal transitivity: $t: R \times_X R \to R$; where with the notation for the projections in the cartesian square
the following holds: $p_1 = \pi_1 \circ i$, $p_2 = \pi_2 \circ i$, $p_1\circ q_1 = p_1\circ t$ and $p_2\circ q_2 = p_2\circ t$.
Since $i$ is a monomorphism, the maps $r$, $s$, and $t$ are necessarily unique if they exist.
Equivalently, a congruence on $X$ is an internal category with $X$ the object of objects, such that the (source,target)-map is a monomorphism and such that if there is there is a morphism $x_1 \to x_2$ then there is also a morphism $x_2 \to x_1$ (internally).
A congruence which is the kernel pair of some morphism (example 1) is called effective.
The coequalizer of a congruence is called a quotient object.
The quotient of an effective congruence is called an effective quotient.
A regular category is called an exact category if every congruence is effective.
An effective congruence, def. 2, is always the kernel pair of its quotient, def. 3, if that quotient exists.
Every kernel pair is a congruence.
An equivalence relation is precisely a congruence in Set.
The eponymous example is congruence modulo $n$ (for a fixed natural number $n$), which can be considered a congruence on $\mathbb{N}$ in the category of rigs, or on $\mathbb{Z}$ in the category of rings.
A quotient group by a normal subgroup $K \hookrightarrow G$ is the quotient of the relation $G \times K \stackrel{(p_1,p_2)}{\hookrightarrow} G \times G$, where $p_1$ is projection on the first factor and $p_2$ is multiplication in $G$ (these are source and target maps in the action groupoid $G \sslash K$).
A special case of this is that of a quotient module.
The notions of regular category and exact category can naturally be formulated in terms of congruences. A “higher arity” version, corresponding to coherent categories and pretoposes is discussed at familial regularity and exactness.
A Mal'cev category is a finitely complete category in which every internal relation satisfying reflexivity is thereby actually a congruence.
Higher-categorical generalizations are that of a 2-congruence and of a groupoid object in an (∞,1)-category. See also (n,r)-congruence.