# Congruence

A term that denotes a class of relationships between algebras and which is dual to bisimulation.

Let us consider as an example the algebra of natural numbers with zero and sum as operations. It is obvious that, if `x = y`, then:

`a + x = a + y.`

In other words, let us consider a context `a + []`: we can fill the hole `[]` with two equal quantities, and obtain two equal quantities. For instance, being `3 = 2 + 1` we have that:

`a + (3) = a + (2 + 1)` for every `a`.

This property of the equality relation is said "replacing equals with equals", or "substitutivity", or "compatibility with the operations", or - less commonly - "congruence".

In category-theoretic terms, given two algebras `A1` and `A2`, a congruence is an algebra `A3` with a span of homomorphisms from `A3` to both `A1` and `A2`. A homomorphism from an algebra to another one is a function ensuring substitutivity, and thus it can be also said to be a "congruence map": a pair of homomorphisms is, in some sense, a congruence relationship.

The word "congruence", however, is more commonly used to indicate a substitutive equivalence. We recall that R is an equivalence relation on a set if it is reflexive (`a R a`), symmetric (if `a R b`, then `b R a`), and transitive (if `a R b` and `b R c`, then `a R c`). These are also the core properties of the equality relation `=`, and we can say that, in a sense, an equivalence relation on a set is a "new kind of equality" over the elements of the set, having a coarser grain than `=` (i.e., equating more elements than `=`, which plainly equates an element only with itself). But an algebra is something more than a plain set, and it turns out that congruences have all the properties we want for defining "new kind of equalities" for algebras: All the properties of equivalence plus substitutivity.