dedekind::relational::Intersect< R, S, Meet > Struct Template Reference

The point-free composite meet R∩S = Δ† ∘ (R⊗S) ∘ Δ: copy the shared domain, run both legs in parallel, merge their codomain outputs where they agree. The arrow-level (spider) realisation of the relational intersection, whose (Copy,Merge) legs are certified by IsMeetAsRightAdjoint — the same R∩S the extensional operator& above computes over Set<pair>, spelled point-free. More...

Collaboration diagram for dedekind::relational::Intersect< R, S, Meet >:

Public Types
using	Domain = dedekind::category::Dom<R>
using	Codomain = dedekind::category::Cod<R>

Public Member Functions
constexpr Codomain	operator() (const Domain &a) const
	The composite meet (R∩S)(a)=Δ†((R⊗S)(Δ(a))): copy the domain, run both legs, merge their codomain outputs where they agree.

Public Attributes
R	r {}
S	s {}

Detailed Description

template<dedekind::category::IsArrow R, dedekind::category::IsArrow S, typename Meet>
requires std::same_as<dedekind::category::Dom<R>, dedekind::category::Dom<S>> && std::same_as<dedekind::category::Cod<R>, dedekind::category::Cod<S>> && dedekind::category::IsMeetAsRightAdjoint< dedekind::category::Copy<dedekind::category::Cod<R>>, dedekind::category::Merge<dedekind::category::Cod<R>, Meet>>
struct dedekind::relational::Intersect< R, S, Meet >

The point-free composite meet R∩S = Δ† ∘ (R⊗S) ∘ Δ: copy the shared domain, run both legs in parallel, merge their codomain outputs where they agree. The arrow-level (spider) realisation of the relational intersection, whose (Copy,Merge) legs are certified by IsMeetAsRightAdjoint — the same R∩S the extensional operator& above computes over Set<pair>, spelled point-free.

Warning

Not dispatch-safe as a glb (#950 review). This is the meet composite by intent, but its requires clause gates only the STRUCTURAL Δ⊣∧ shape via IsMeetAsRightAdjoint, which is deliberately true for Merge<A,Sup> (the JOIN) too. So Intersect<R,S,Sup> is publicly constructible and computes a join under an intersection name. glb-correctness is the injected Meet's obligation, NOT something this composite discharges; closing it is deferred to #908 (reify predicate variance) plus the value-level product-order leg, FIXME(#946). Do NOT branch dispatch on the mere existence of this type as if it guaranteed a meet.

Template Parameters

R	the left leg X→Y.
S	the right leg X→Y (same domain and codomain as R).
Meet	the injected glb on the CODOMAIN Y, forwarded to Merge.

Note

Legs are X→Y, not endo (#954). The Copy fans the shared DOMAIN X (Δ:X→X×X); the Merge glb lives on the shared CODOMAIN Y (Δ†:Y×Y→Y), where the two legs' outputs are met. The composite is X→Y. This types the relational / predicate meet R∩S directly: legs R,S:X→Ω, Merge = ∧ on Ω (a set is χ:X→Ω). The endo case X=Y is the special case where Copy and Merge share the carrier; Intersect<Identity,Identity> still collapses to the identity (idempotence a∧a=a).

Member Function Documentation

operator()()

template<dedekind::category::IsArrow R, dedekind::category::IsArrow S, typename Meet>

Codomain dedekind::relational::Intersect< R, S, Meet >::operator() ( const Domain & a ) const

inlineconstexpr

The composite meet (R∩S)(a)=Δ†((R⊗S)(Δ(a))): copy the domain, run both legs, merge their codomain outputs where they agree.

Parameters

a	the input value in X.

Returns

R(a)⊓S(a) in Y, the injected glb of the two legs' outputs.

Note

The requires clause gates only the STRUCTURAL Δ⊣∧ shape on the codomain (crossed signatures + posetal carrier + definite variance). It does NOT certify that Meet is the glb rather than the lub; that is the injected op's obligation (see IsMeetAsRightAdjoint), tightened later via #908 + the value-level product-order leg, FIXME(#946).

---

The documentation for this struct was generated from the following file:

• src/main/modules/dedekind/relational/dyadic.cppm