dedekind::category::IsSubobjectFamilyMember Concept Reference

Compile-time meeting-point pins (#698 Slice 10) — three structurally distinct carriers at the same Form-chain rows. More...

Concept definition

template<typename R, typename A, typename L>
concept dedekind::category::IsSubobjectFamilyMember =  requires {
  
  typename std::remove_cvref_t<R>::Domain;
  typename std::remove_cvref_t<R>::logic_species;
  requires std::same_as<typename std::remove_cvref_t<R>::Domain, A>;
  requires std::same_as<typename std::remove_cvref_t<R>::logic_species, L>;
}

Detailed Description

Compile-time meeting-point pins (#698 Slice 10) — three structurally distinct carriers at the same Form-chain rows.

lattice__Boolean_Canonical_Witnesses

lattice__Slice_10_Meeting_Point

The closing slice for #698 establishes that the Form-chain machinery is genuinely carrier-uniform: same code, three readings. The full meeting-point matrix (rows × carriers) lives in test/cpp/.../meeting_point_test.cpp; the pins below are the compile-time anchors that catch regressions at compile-time rather than runtime.

Per feedback_static_assert_in_main: cross-partition / cross- carrier invariants live as static_assert in the main .cppm source when there's no mock-type dependency.

Carriers covered here:

• size_t: large finite totally-ordered chain (Slices 6/7 already pinned bool and int).
• Sup / Inf identity: the Form-chain Meet / Join slots are the value-returning :mereology lattice ops Sup / Inf (pinned via an explicit instantiation that names them, #934).

A type R is a member of the subobject family over ambient A in classifier L.

The lattice operations on Sub(A) (meet, join, complement) close over the family of subobjects of A in L, not over a single predicate-type closed carrier. Concretely, when no structural collapse fires (a structured_and / structured_or reduction to a halfspace, interval, Singleton, Ø or 𝔸, or an IsComplementPair short-circuit), A & B returns a Meet<A,B> carrying both operand sets (dually, | returns a Join<A,B>). The node is a different type, but over the same Ambient and logic_species.

lattice__Family_Anchor

The ambient A is the anchor (per #712 review): a subobject family is determined by the pair (A, L), and family membership is recognised by metadata equality: a family is "a space of parts" anchored on its ambient, and the parts (subobjects) belong to it by virtue of sharing that ambient.

lattice__Family_Generalisation_Door

Per #712 review: if the (A, L) anchoring proves too restrictive in some future regime (e.g. "families over a category rather than a single ambient" — fibrations, sheaves over a site, dependent power objects), the family concept can be generalised by adding template parameters or splitting the anchor. The current shape is the minimum that supports the Slice 8 architectural commit; broader generalisations land if and when a concrete consumer surfaces a need.

Template Parameters

R	The candidate family member (typically the result type of meet / join / complement).
A	The ambient object.
L	The classifier (logic species).