Documentation

We define a congruence relation to be an equivalence relation which satisfies the following functionality law for for α,β ∷ *, m,n ∷ α and f ∷ α → β:

 Congruence α, Eq β, (m == n) true ⊢ (f m == f n) true

One way to look at the Congruence class is through the lens of setoids; then it classifies those types for whom "being the domain of an operation" and being the "domain of a function" are synonymous. Another way to look at it is in the following sense: Congruence α forces all functions out of α to be extensional.

But usually, when developing setoids, you have a separate type of functions which respect value equivalence, and then every function has a proof obligation; then the raw functions of the outer theory are "operations" until they can be shown to be functional. This is tractable in type theory, but in Haskell and ML, it is not: when we can, it is better to rely upon data abstraction and composition to enforce our laws for us, so that proofs come for free.