<style type="text/css">CODE { font-family: sans-serif; font-weight: bold; }</style>
A *(term) that denotes a class of relationships between _(algebras|Algebra and Coalgebra) 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 <code>x = y</code>, then:

<code>a + x = a + y.</code>

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

<code>a + (3) = a + (2 + 1)</code> for every <code>a</code>.

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|category theory) terms, given two algebras <code>A1</code> and <code>A2</code>, a congruence is an algebra <code>A3</code> with a span of homomorphisms from <code>A3</code> to both <code>A1</code> and <code>A2</code>. 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 <em>relationship</em>. 

The word "congruence", however, is more commonly used to indicate a substitutive <em>equivalence</em>. We recall that R is an equivalence relation on a set if it is reflexive (<code>a R a</code>), symmetric (if <code>a R b</code>, then <code>b R a</code>), and transitive (if <code>a R b</code> and <code>b R c</code>, then <code>a R c</code>). These are also the core properties of the equality relation <code>=</code>, 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 <code>=</code> (i.e., equating more elements than <code>=</code>, 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. 