dedekind::category::IsMeetAsRightAdjoint Concept Reference

The STRUCTURAL shape of "the meet @c ∧ is the right adjoint of the diagonal @c Δ" (Δ⊣∧): the reified theory this slice postulates as a type-check. More...

Concept definition

template<typename Cp, typename Mg, typename Leq std::less_equal<Dom<Cp>>>
concept dedekind::category::IsMeetAsRightAdjoint = 
    IsGaloisConnection<Cp, Mg, ProductLeq<Leq, Leq>> &&
    IsPosetal<Dom<Cp>, Leq> && IsCopy<Cp>

Detailed Description

The STRUCTURAL shape of "the meet @c ∧ is the right adjoint of the diagonal @c Δ" (Δ⊣∧): the reified theory this slice postulates as a type-check.

Note

The shape (crossed signatures + a posetal carrier + matched variance) cannot see whether the merge computes the glb or the lub; the law leg is_adjoint_v can, because it is registered per glb (Inf on a chain, ∧ on bool) next to the proof, so the join Sup is rejected (the witness below). A merge with another injected op is rejected until its own fact is registered; #908 would derive the variance structurally.

Δ:P→P×P (copy) is the left adjoint, ∧:P×P→P the right, so the pair is an IsGaloisConnection whose left leg is the diagonal (its codomain is the square of its domain). The Galois test Δ(c)≤(a,b) ⟺ c≤∧(a,b), with Δc=(c,c) under the product order, unfolds to the glb universal property c≤a and c≤b ⟺ c≤a∧b. C++ concepts cannot quantify over c,a,b, so that equivalence is the engineer's honesty obligation (as with IsGaloisConnection); the structural shape names the signatures.

Note

Monotonicity is INHERITED, not re-gated here: IsGaloisConnection was tightened (#946) to require MATCHED variance (both legs monotone, or both antitone), so both Cp and Mg must carry a declared, and agreeing, variance (see the is_monotone_v registrations above). That rejects a variance-less or mismatched-polarity merge; the meet-vs-join residual is closed by the law leg is_adjoint_v, registered per glb. #908 (reify predicate variance) would derive the variance structurally; #791 certifies the monotone / join operations themselves.

Threaded orders (#950). The Galois legs live on P×P (Copy's codomain, Merge's domain), so their variance is tested against the COMPONENTWISE product order ProductLeq<Leq,Leq> (≤×), while the base carrier P is checked posetal under Leq itself. Leq is no longer inert: it flows into BOTH the product order threaded through IsGaloisConnection and the IsPosetal check (#950 review), so a custom poset relation is honoured rather than silently overridden by a hard-coded std::less_equal<>.

Template Parameters

Cp	the copy/diagonal Δ.
Mg	the meet/merge ∧.
Leq	the order on P; defaults to std::less_equal

. The product order on P×P is derived as ProductLeq<Leq,Leq>.