A homogeneous binary relation R on a carrier V is a congruence w.r.t. operation Op when it is an equivalence relation and respects Op. More...

Concept definition

template<typename R, typename V, typename Op>
concept dedekind::category::IsCongruence =  IsEquivalence<V, R> && is_congruence_v<R, V, Op> &&
                       requires(const V& v, const Op& op) {
                         { op(v, v) } -> std::convertible_to<V>;
                       }

Detailed Description

A homogeneous binary relation R on a carrier V is a congruence w.r.t. operation Op when it is an equivalence relation and respects Op.

Stratifies IsEquivalence by the operation that must be respected: every congruence is an equivalence relation, but not every equivalence relation is a congruence (a textbook foil: |x| = |y| on ℤ is an equivalence but not a congruence for +, since 3 ~ -3 and 5 ~ 5 yet 3+5 = 8 ≄ 2 = -3+5).

Universal-algebra reference: Burris-Sankappanavar §II.5. Form-chain row 2 in the quotient categorification (#718).

Template Parameters

R	The candidate equivalence-relation type.
V	The homogeneous carrier on which `R` lives.
Op	The binary operation `V` `×` `V` `→` `V` that `R` must preserve.

cartesian__IsCongruence_Op_Shape_Gate

The concept body requires Op to be structurally well-formed as a binary operation V × V → V: Op(v, v) must be callable and produce a result convertible back to V. Without this shape gate, a malformed Op could be registered via is_congruence_v and the concept would still pass — type-checked meaninglessness. The gate is structural-shape only (mirroring the upstream relation traits' shape-only semantics), not a verification of the congruence law itself, which remains an opt-in honesty obligation.