dedekind::category::IsCongruenceQuotient Concept Reference

Q is a quotient of a carrier V by a declared congruence R for Op and reduces from V — the relational reading of the H leg. More...

Concept definition

template<typename Q, typename Op>
concept dedekind::category::IsCongruenceQuotient = 
    requires {
      typename quotient_congruence<Q>::type;
      typename quotient_congruence<Q>::carrier;
    } &&
    IsCongruence<quotient_congruence_t<Q>, quotient_congruence_carrier_t<Q>,
                 Op> &&
    requires(quotient_congruence_carrier_t<Q> v) {
      { Q{v} } -> std::same_as<Q>;  
    }

Detailed Description

Q is a quotient of a carrier V by a declared congruence R for Op and reduces from V — the relational reading of the H leg.

Holds when (1) Q declares a quotient_congruence whose relation R is a genuine congruence on its carrier V (IsCongruence<R,V,Op>: an equivalence preserved by Op), and (2) the canonical projection \(V \twoheadrightarrow Q\) exists — Q is constructible from a carrier value (Q{v}) — so Q is tied to V/R, not merely accompanied by a free-floating congruence. A bare marker type with no reduction is rejected.

Clause (2) is the honest ceiling: a full quotient proof ( \(\forall a,b:\ \mathrm{proj}\,a=\mathrm{proj}\,b \iff R(a,b)\)) is Rice-undecidable, so the concept certifies the structural tie (a congruence on V plus a reduction V\to Q), not the extensional identity. The H-leg analogue of IsSubalgebra (S), and independent of IsQuotientAlgebra (see the note above): a carrier may certify its own traits directly yet still be witnessed relationally as V/R.

Template Parameters

Q	the quotient carrier (declares quotient_congruence, reduces from V).
Op	the carrier operation the congruence must respect (e.g.\ std::plus).