Congruences of binary operations clarified

The definition of congruences of binary operations is well known, and they are widely used in semigroup theory and related branches of abstract algebra. We can make the definition of a congruence into an input/output relation, and thereby make it more intuitive / easier to understand and put it in the larger context of input/output relations. In order to do this, we must first introduce the idea of the cartesian product of two set partitions.

Cartesian product of set partitions:
Let $A$ and $B$ be sets, and let $P,Q$ be set partitions of $A$ and $B$ respectively. Then $P \times Q$ is the set partition on the cartesian product $A \times B$ defined by equality of $P$ in the first index and equality by $Q$ in the second index. $$(a,b) =_{P \times Q} (c,d) \iff (a =_P c) \land (b =_Q d)$$ It is not hard to see that a given set partition can have a product defined over itself by making both set partitions equal. This will determine the input set partition on the congruences of binary operation. $$(a,b) =_{P^2} (c,d) \iff (a =_P c) \land (b =_P d)$$ This sort of construction can even be generalized to any equality of n-tuple for use in universal algebra. In this way, all congruences can be defined as input/output relations where some piece of information determines another piece of information within a function.

Congruences as input/output relations:
It is not hard to see then that congruences of a binary operation $f$ are defined by input/output relationships of the form $P^2 \to P$. In other words, $$(a,b) =_{P^2} (c,d) \implies f(a,b) =_P f(c,d)$$ As is the case with all input/output relations this produces a quotient operation $P^2 \to P$ which describes how the $P^2$ input information completely determines the $P$ output information.