dedekind::category::IsProductParthood Concept Reference

Bridge: a product P with parts A and B IS a mereological parthood in the projection-access reading. More...

Concept definition

template<typename P, typename A, typename B, typename WholeProject std::identity>
concept dedekind::category::IsProductParthood =  IsSpecies<P> && IsSpecies<A> && IsSpecies<B> &&
                            IsProjectedProduct<P, A, B, WholeProject>

Detailed Description

Bridge: a product P with parts A and B IS a mereological parthood in the projection-access reading.

limit__Product_Parthood_Bridge

Bridge: every product is a mereological parthood (#573 / #643).

The bridge concept lives here in :limit because :limit already imports :mereology (the reverse would be a cycle), so this partition is the natural marriage point between the universal-property product vocabulary and Leśniewski's parthood vocabulary.

Names the structural equivalence between the universal-property product (Burris-Sankappanavar §I.1; Mac Lane CWM III.4) and the Leśniewski-style mereological reading: A and B are parts of P, accessed through canonical projections. In Pierce-language (Basic Category Theory §1.4) the bridge reads as: π_1(p) and π_2(p) are the atomic part-access operations. In pointer-like wrapper language, the same operations spell p->fst and p->snd. Same difference.

Which reading of "parthood"?

Two readings of parthood coexist in this codebase, and the bridge encodes only the first:

1. Projection-access reading (this concept): A is a part of P iff there exists a canonical projection P → A, witnessed structurally by an IsProductProjection -inhabiting callable. This is the reading the universal-property product canonically supplies.
2. Predicate reading (:mereology IsPartOfRelation): A is a part of P iff one of part <= whole / whole(part) / whole[part] returns Ω. This is the order-theoretic / characteristic-function reading.

The bridge intentionally does NOT establish an IsPartOfRelation -encoded witness alongside the projection witness; those encodings ride on independent operator surfaces that std::pair does not currently overload. Future slices of #573 may add an IsPartOfRelation companion witness once a natural Ω-valued predicate (e.g. "is @c x @c == @c π_1(p)?") is wired in.

Constraint

The concept is anchored on IsProjectedProduct, so the type-system gate matches the textbook claim "P is a product, hence parthood (projection-access)". By default WholeProject is std::identity, reducing the bridge to a direct IsProduct<P, A, B> check that std::pair walks out of the box.

Pluggability

Quotient-style wholes whose part-access does not go through .first / .second can supply a custom WholeProject policy that materialises a std::pair -shaped view of the parts (#573 slice 4 onward). This mirrors IsProjectedProduct's default-template-parameter pattern — the bridge is currently a structural alias of IsProjectedProduct stated under a parthood name; future slices may sharpen it further.

Sollbruchstelle (#573)

Downstream code that wants "A is mereologically part of P (projection-access)" writes IsProductParthood<P, A, B> rather than recapitulating IsProduct, and the name signals the parthood reading explicitly.

Template Parameters

P	The product whole (an IsSpecies object).
A	The left part (an IsSpecies object).
B	The right part (an IsSpecies object).
WholeProject	Optional projection policy materialising a pair- shaped view of P (default: std::identity).