dedekind::category::SetAsProduct Concept Reference

Set := (Underlying, Classifier) read as a product, in the projection-access sense. More...

Concept definition

template<typename S, typename Underlying, typename Classifier>
concept dedekind::category::SetAsProduct =  IsSubobject<S, Underlying> && requires {
  
  
  
  
  
  
  
  
  
  requires std::same_as<std::invoke_result_t<S const&, Underlying const&>,
                        Classifier>;
}

Detailed Description

Set := (Underlying, Classifier) read as a product, in the projection-access sense.

Names the product reading of a set object explicitly — a set is a pair of (i) its underlying ambient species Underlying, accessed type-level via S::Domain, and (ii) its classifier codomain Classifier, recognised structurally via the call shape S(a) -> Classifier. Sibling to IsSubobject, which names the predicate reading "S is a subobject of A". The two readings carve the same surface from different angles.

Post-#681 semantic shift

Prior to the structural refactor, Classifier named the type of the characteristic-morphism projector (decltype(s.χ)). The static χ projector has been retired in favour of structural recognition (S is the characteristic morphism via operator()), so Classifier is now the codomain L::Ω that S(a) produces, not the predicate-type wrapper. Concrete examples: for a Set under Boole, Classifier = bool; for a Set under Kleene, Classifier = Ternary.

Why this concept exists (#573 / #644 — Sollbruchstelle)

The user's framing for the HAS-A maturation: "a set should be a product in the @c :cartesian sense of an underlying and predicates." This concept names that seam. It refines IsSubobject by adding a typed obligation that the classifier codomain is Classifier — a structural witness that the (Underlying, Classifier) decomposition is recoverable. Downstream slices (#573 slice 3 AlgebraAsProduct, slice 4 pilot witness) compose on this name.

Relation to IsProductParthood

The bridge concept IsProductParthood in :limit asserts the structural product-as-parthood reading uniformly via IsProjectedProduct. SetAsProduct is the set-level specialisation, but the asymmetry "Underlying is a type, Classifier is a codomain" keeps a direct IsProductParthood composition awkward at this slice; the concepts are logical siblings, not typed dependencies.

Template Parameters

S	The set object.
Underlying	The ambient species (an IsSpecies object).
Classifier	The codomain of S-as-predicate (L::Ω).