dedekind::sets Namespace Reference

Namespaces
namespace	detail_complement_involution
namespace	detail_recursion_witness

Classes
struct	ResidueClass
	The class \(\{x \in \mathbb{N} \mid x \equiv r \pmod n\}\), read analytically: the materialisation of ℕ | (π % n == r). More...
struct	Ø
	∅: The Initial Object. Extensional (Size 0). More...
struct	default_cardinality
	Trait behind default_cardinality_t: ℵ_0 for every carrier (the countable fiction of #680) ... More...
struct	default_cardinality< bool >
	... except bool, which is Finite by its representation. More...
struct	𝔸
	The universal set over the carrier T: the terminal object ⊤ of Sub(T), the reified type constraint. More...
struct	SetObjectLeaf
	A leaf that is a set object, the property over_nodes lifts. More...
struct	is_set_object
	A set object: a leaf, or a node over set objects on one domain, by category's over_nodes, the rule its opt-in | and & follow too. More...
struct	Subobjects
	The subobjects of a carrier in a logic, \(\mathrm{Sub}(T, L)\) ( \(\mathrm{Sub}(\mathbb{A}_T)\), \(\chi\) valued in L), as an object: the domain or codomain of an arrow on sets — the complement, the pushforward along an injection. No one type is this object: every set object over the carrier in that logic presents it (the expression grammar is a type-indexed family: 𝔸, a comprehension, a Meet / Join / Not node), and the universe, its top, is the representative, so category::IsArrow checks an arrow on sets at the universe and asks the result to be a set object over it (morphism__Objects_And_Their_Presentations). A universe's cardinality class is a bound, not part of the object. More...
struct	subobject_order
	The subset (⊆) order on the subobject lattice Sub(T), keyed by the logic species L. This is the injected order (Ord) under which the generic lattice-law term reducer (category:lattice_term, #865/#890) normalises set expressions: Ø is its bottom (⊥, initial), 𝔸 its top (⊤, terminal). Keying by L lets the algebra markers distinguish Boole (a Boolean subobject lattice, every law) from Kleene (Heyting / De Morgan, no complement collapse). More...
struct	codomain_reduce
	The codomain leg of the two-axis reduce (#894). More...
struct	codomain_reduce< Ø< T, L > >
struct	codomain_reduce< 𝔸< T, L, C > >
struct	is_extensional< 𝔸< T, L, C > >
struct	Finite
struct	is_extensional
	Primary trait: Is a species defined by its members? More...
struct	is_extensional< T >
struct	ℵ
struct	ExtensionalCardinal
	Finite extensional cardinal: one machine word W. More...
struct	CardinalityEffect
	Draft writer-like cardinality effect carrier. More...
struct	SignedExtensionalCardinal
	Signed one-word integer: two's complement in the signed word S. More...
struct	PositiveInfinity
struct	NegativeInfinity
struct	NaZ
struct	SetExpr
	Opt-in CRTP base that supplies the ETCS set surface to a specialized set expression. It provides Member, ι (the subobject inclusion), Codomain, logic_species, and the set-lattice trait members. It keys the classifier χ off the Derived's own operator(). More...
struct	answer_logic
	The species of a predicate's answer, relative to the base's species L: an answer already in L::Ω is in L (so a Chain<int> universe accepts an int-valued predicate), otherwise the answer type names its species (classifier_logic_t; no default). More...
struct	answer_logic< L, Answer >
struct	datum_cardinality
struct	datum_cardinality< Predicate, Base >
struct	Comprehension
struct	UniversalPredicate
	The universal predicate: accepts every element of T. More...
struct	EmptyPredicate
	The empty predicate: rejects every element of T. More...
struct	UnknownPredicate
	The archetypal undecidable predicate: answers Unknown everywhere. More...
struct	SetCombine
	The injected leaf-combiner (the reducer's Combine policy) for the subobject lattice: at an order-incomparable residual, hand the two set leaves to the carrier's domain ∧ / ∨ on their runtime data and let the reducer fold the result again. Two plain sets over one universe combine through their predicates (structured_and / structured_or via ADL, elevated back to a set); a value leaf (an Interval) combines directly. Each leg is present only where the carrier actually combines the pair, so elsewhere the residual stays a Meet / Join node. More...
struct	set_predicate
	The predicate of a PLAIN set, a Comprehension over the universe 𝔸<T,L> (::type absent otherwise); PlainSet gates the plain-set-only branches (complement pair, predicate negation) so a compound node (Meet / Join) takes the node path. More...
struct	set_predicate< Comprehension< 𝔸< T, L, C >, P > >
struct	Complement
	The complement as an arrow on the object \(\mathrm{Sub}(T, L)\) (Subobjects, :boundaries), \(S \mapsto \neg S\): an endomorphism, its domain and codomain the one object, presented by every set object over T in L. It is an involution by the reducer's own law \(\neg\neg A \to A\): operator~ peels the node, so ~~s is s, by type, for every presentation s; the certificate reads that law at the representative. The first arrow on sets category::IsInvolution admits: the concept quantifies over the object, not over one value type (morphism__Objects_And_Their_Presentations). More...
struct	InitialObjectArrow
	InitialObjectArrow<Init, Target> — the unique arrow from the initial object into any subobject (Init → Target), i.e. the empty function / the ⊥-of-Sub(U) leg. Dual to inclusion_arrow: where that reifies an inclusion into the ambient, this reifies the initiality mediator out of Ø. Gated on category::IsInitialObject<Init> so only a genuine initial object (Ø, tagged) can be the source; the body forwards the (vacuous) Member value and is unreachable in practice (Ø has no members). Canonical span leg for a pushout A ← Ø → B, replacing hand-rolled per-instance span structs. #881. More...
struct	SymbolicImagePredicate
	Symbolic image-of-intensional-Set predicate (#602 layer 1). More...
struct	ComposedIsoImagePredicate
	Composed predicate for the iso-decidable image(f, Set) specialisation below: y ↦ S(f^{-1}(y)) where S is the source set's characteristic and f^{-1} is the iso's inverse. More...
struct	ComposedRetractImagePredicate
	Composed predicate for the retract-decidable image(f, Set) specialisation: y ↦ let mx = retract(f)(y); mx.has_value() ? S(mx.value()) : L::False. More...
struct	ExtensionalSet
struct	universe_cardinality
	The cardinality class of a set object's universe. More...
struct	universe_cardinality< 𝔸< T, L, C > >
struct	product_cardinality
struct	product_cardinality< Finite, Finite >
struct	product_cardinality< Finite, ℵ< N > >
struct	product_cardinality< ℵ< N >, Finite >
struct	product_cardinality< ℵ< M >, ℵ< N > >
struct	SumMembership
	Membership of a sum: the copairing \([\chi_a, \chi_b]\), each answer lifted into the join of the summands' species. A named functor (the product's dual is the meet of its cylinders, ProductMembership). More...
struct	sum_universe
	The sum of two set objects: the subobject (a, b) of the coproduct of their carriers, \(|a + b| = |a| + |b|\) (the join on the cardinal lattice, as for the product). Reduced where the types decide it: More...
struct	sum_universe< 𝔸< X, LA, CA >, 𝔸< Y, LB, CB > >
struct	Restrict
	\(\iota_K^{-1}\) as an arrow: the restriction, lifted into the sum's logic (a summand given in a smaller logic sits in the sum's by \(\Sigma \hookrightarrow \Omega\)). The right adjoint of Inject. Defined on every presentation restriction reaches: the sums, their lattice nodes, the boundaries. More...
struct	Inject
	\(\exists_{\iota_K}\): a set of the summand as the set of the sum that is it on its summand and empty on the other, kept as a sum (the strength reduction a | Ø → a is the inverse direction). The left adjoint of Restrict. More...
struct	descent
	A descent: \(\pi_i - c\), a slot stepped down by a constant, and the slot it steps on. c > 0 is checked when the χ node is built. That the descent ends is Archimedes' axiom, that enough steps of c exceed any magnitude [1]. More...
struct	descent< BinOp< std::minus<>, Projection< I >, Const< K > > >
struct	Env
	The point and the set under definition, threaded through a body: the term nodes read it as the point (conversion, and term_value below), Self reads it as the set. More...
struct	Self
	The set under definition pulled back along the terms: χ(t₁, …) is \(x \mapsto \chi(t_1(x), \ldots)\) with \(\chi\) the comprehension's own classifier, unknown until the former closes it. A relational predicate (an operand of && / ||), evaluable only through an Env. More...
struct	ChiTag
	The classifier under definition: χ(terms…) in a former's body is the set being formed, applied to the terms. More...
struct	DescendsAt
	The measure algebra at the points X for position J: a χ node passes when its argument in position J descends on the coordinate J stands for; every node when all its legs pass; any other leaf vacuously. More...
struct	BindArgs
	The binding of the arguments of every χ in a body at the points X: each a term bound there, a constant cast into its coordinate's carrier. The body's own binding treats a χ as a leaf, so its arguments are bound here. More...
struct	Rec
	The recursion, closed: the base's membership, then the body evaluated with this very predicate in scope for its Self nodes. More...
struct	Point
struct	RelAnd
	Meet (conjunction) of two relational predicates, the result of && on them. More...
struct	RelOr
	Join (disjunction) of two relational predicates, the result of || on them, dual to RelAnd. More...
struct	Const
	A constant, carried as a value. More...
struct	BinOp
	a op b, the operator a standard functor (std::plus<>, minus, multiplies, divides, modulus) applied in one carrier. More...
struct	Ap
	An arrow applied to a term, f(a). More...
struct	CondT
	McCarthy's conditional on terms: a where p holds, else b. More...
struct	Cmp
	The atom a R b over two terms, a relational predicate. More...
struct	Term
	A term built at run time, the grammar with its shape a value; defined after the binding below. More...
struct	Pred
	A relational predicate built at run time: comparisons of terms and their connectives; defined after the binding below. More...
struct	Slots
	The slot algebra: the slots a term or a relational predicate mentions, as a bit mask (bit i for π_i, bit 0 for the unary π). A node mentions the union of its legs' slots; a predicate the grammar does not know mentions every slot, so no certificate reads more into it than it says. More...
struct	On
	The carrier a rule is stated for, as a tag. A rule admits(On<C>, key, divisor_is_constant) says that the operator key is in the signature of C: a symbol one of the carrier's certified varieties has. It is declared in this namespace beside the certificate and found by ADL, so it is in force where that module is imported: the comparisons beside the partial orders (order:poset), // and % beside IsDividableChain (order:completeness), a field's / beside IsField (algebra:field); + - * and == != here, whose certificates are category's. Without a rule an operator is not in the signature. More...
struct	FieldDivision
	The two divisions Python tells apart, as keys: a field's, and the Euclidean one of an ordered carrier with remainder. The typed grammar's std::divides<> is the carrier's own, admitted where either is. More...
struct	EuclideanDivision
struct	rel_key
	A comparison's key: the standard functor it is. More...
struct	rel_key< Rel::Lt >
struct	rel_key< Rel::Le >
struct	rel_key< Rel::Gt >
struct	rel_key< Rel::Ge >
struct	rel_key< Rel::Eq >
struct	rel_key< Rel::Ne >
struct	not_admitted
	Refused at the carrier: an operator not total there, a division by a term, an order comparison on an unordered carrier, a slot the points have not. Raised when a term built at run time is bound. More...
struct	point_sorts
	The sorts of a point type: the carriers of its coordinates, each once. A carrier value has one sort; a pair of two carriers two (one where they agree). A term built at run time names no carrier until it is bound, and every node then has a sort: a projection its slot's, a constant its context's, an operator its operands' common one, a comparison 𝔹. More...
struct	point_sorts< std::pair< A, B > >
struct	Row
	A row: a point of an n-ary product whose arity and columns' sorts are data. Each cell is a value of one of the carriers Cs, and the cell's alternative is its column's sort, so a row is its own schema. Slots are π_1 … π_n. More...
struct	point_sorts< Row< Cs... > >
struct	with_carrier
	The tuple S with C appended, unless C is in it already. More...
struct	with_carrier< std::tuple< Cs... >, C >
struct	value_sum
	The value of a term built at run time at a point: the one sort's carrier, or the sum of the sorts where there are more. More...
struct	value_sum< std::tuple< A > >
struct	value_sum< std::tuple< A, B, Cs... > >
struct	ReadAs
	The coordinate slot of the point p, read in the sort C the dispatch chose; the point itself for the unary π. More...
struct	EmbedsAt
	Whether the sort b embeds into the sort a, at points of P. More...
struct	ConstantAs
	A constant read in the sort C: a numeral cast into it, a constant of a sort (a bool, a Ternary) read in its own and embedded. More...
struct	Value
	The value algebra: a term or a predicate folded at the point p. A projection reads its coordinate, a constant is its value, a predicate the grammar does not know is evaluated as itself; an operator or a comparison combines its operands in the carrier of the non-constant one; an applied arrow converts its argument into its domain. More...
struct	Verdict
struct	Bound
	The result of a binding: nothing but the checks that ran. More...
struct	Bind
	The binding algebra at the points X: a constant beside a term (a, b of an operator, a comparison or a conditional) meets the term's carrier now; a constant under an arrow meets the arrow's domain. A leaf binds trivially. More...
struct	PinConstant
	A numeral read in the sort C and written back as a constant of that sort, through lift; a carrier lift has no constant for keeps the numeral. More...
struct	Definition
	A slot's definition: the term t of a conjunct π_slot == t (or t == π_slot) with t free of the slot, and the conjunction without it. ∃π_slot. P is then the rest with t for π_slot: the existential is eliminated by substitution. Dually, under ∀ a disjunct π_slot != t defines it: ∀g. (g ≠ t ∨ Q) ≡ Q[t/g]. More...
struct	NoConstants
	No carrier value as a constant: the lift that names nothing, so eliminate_quantifiers eliminates by definition alone and leaves every quantifier over a chain to the search. More...
struct	ChainValues
	The values of a finite chain as constants, through lift: the cases of Shannon's expansion; none for any other carrier. More...
struct	ShiftDown
	The slots above an eliminated bound slot, moved down by one. More...
struct	CondSplit
	A term with its first conditional taken out: the condition, and the term with the conditional replaced by each branch. More...
struct	Total
	The totality algebra at the points X: a node is total when its legs are, and an operator when it is admitted on its carrier (admits, the gate the value algebra enforces: total there, or dividing by a nonzero constant), an applied arrow when the arrow is total and its argument already has the arrow's domain (a conversion may fail). A predicate the grammar does not know is not certified. More...
struct	graph_atom
	π_2 == t, or t == π_2, with t mentioning only the first slot: the graph of the function x ↦ t(x). term is t. More...
struct	graph_atom< Cmp< Rel::Eq, T, Projection< 2 > > >
struct	graph_atom< Cmp< Rel::Eq, Projection< 2 >, T > >
struct	MentionsSelf
	The self algebra: a term or predicate mentions the set under definition when one of its leaves is a χ node; every node passes it up. More...
struct	Projection
	The projection π_k: the k-th component of a product. More...

Concepts
concept	IsPairing
	A carrier that is the product of its two legs and is built from them (the pairing ⟨a, b⟩): a set over it answers r(a, b) as r(⟨a, b⟩) (#1047). IsProduct, plus construction from the legs: std::pair, Complex (ℂ ≅ ℝ×ℝ) and Rational (the pairing then the quotient ℤ×ℤ → ℚ, so r(n, d) asks whether n/d is a member).
concept	HasSetComplement
	A set with a set complement: ~s is formed (the reducer's Not node, or a type's own closed-form complement).
concept	Is𝔸
	A universe: the terminal object of Sub(T) — the reified type constraint 𝔸<T,L,C> itself (carrier, logic, cardinality class).
concept	Is𝔸Of
	U is the universe leg of S: a universe over the same carrier under the same logic.
concept	IsSetObjectLeaf
	The leaf case: a set object that carries the subobject surface itself (Definition Lwv) together with its two legs.
concept	IsSetObject
	An object of the category Set: a leaf carrying the subobject surface and its legs, or a lattice node — Meet / Join / Not — over set objects on one carrier. The node case is structural: the node's χ is the pointwise evaluation category:lattice already gives it (an arrow into Ω), its universe is its operands', its classifier is the node itself. This is the opaque arm, "the AST is the set", without any set semantics in the lattice partition: the member shape, the inclusion ι and the pullback / pushout apex legs are a sets-side view (as_pullback / as_pushout in :expressions), not a property of the node. The same-logic requirement of the leaf surface is not imposed on nodes: Ø<T,Kleene> ∧ S<T,Boole> is a set object whose reduction the bounded law and the codomain leg decide.
concept	HasUpperBound
	ETCS-aligned upper bound for meet/intersection cardinality.
concept	IsCardinality
concept	IsCountable
concept	IsFinite
concept	IsExtensional
concept	IsWrappingWord
	A machine word that is the wrapping ring ℤ/2^w: an unsigned built-in integer (not bool) that the category registrations certify as a commutative ring under + and *, periodic under +, and totally ordered.
concept	IsRingIntegral
	The old name of IsIntegerChain, which never claimed a ring.
concept	HasDecidableMembership
	S's membership map ranges into two-valued (classical) logic.
concept	IsDecidableSet
	A Boolean-valued L-set: an IsLSet whose membership is decidable (χ factors through the dominance Σ ↪ Ω; logic_species is Boole).
concept	HasCardinalityType
	The cardinality bound a comprehension inherits: the datum's when it declares one, else the base's.
concept	IsDatum
	A datum over T: a predicate on T (an arrow into a truth object) that is not itself a set. Point, Bounds, LowerCut.
concept	PlainSet
concept	HasStructuredAnd
	Downstream specialization hook for structured predicate conjunction.
concept	HasStructuredOr
	Downstream specialization hook for structured predicate disjunction.
concept	IsLogicalTerm
	A term of the set grammar, the operand sort of && / ||: an arrow (a predicate, a set, a node over arrows) or a point-free relational fragment (π_1 ⋈ π_2, tagged is_rel_predicate, which meets its domain only at the former &). A bare truth value is not a term: bool && bool stays the host language's, and a constant beside a predicate lifts through :topoi.
concept	SetShaped
	A set-shaped carrier: exposes the ambient Domain and the logic_species. The gate constraint for the power-set customization point; the ordered specialisation conjoins it (so it subsumes this gate and wins by partial ordering for the carriers it handles).
concept	StdSetLike
concept	NatZedPair
	The two carriers of the one cross-carrier pair the library ships, ℕ ↪ ℤ on the variant proxies: A is a set object over Cardinality, B one over SignedCardinality, in the same species. Any set object qualifies (a halfspace, a comprehension, a node): only χ is read.
concept	HeterogeneousPair
	Two set objects on different carriers (the ℕ / ℤ pair aside): the operands of a sum.
concept	IsWhereClause
	Quantifiers over a finite carrier, decided by type through the finite quotient rather than by enumeration.
concept	WellFounded
	A carrier a descent terminates on: the unsigned words, ℕ's shadows, with 0 at the bottom. (Cardinality joins once its monus is a term.).
concept	HasTermValueAt
	A term with a value at the points X: term_value(t, x) is formed.
concept	BindsAt
	A term that binds at the points X: bind_check<X>(t) is formed.
concept	ComparesEqualTo
	The equality atom {x : T | x == pivot}, the datum of the pure equality theory, the one leaf every regular carrier offers (a point in ℂ is this). On a chain the cut subsumes it, x == p ⟺ x ≥ p ∧ x ≤ p. The pivot is a value; the set is Finite whatever the species.
concept	IsRelPredicate
	A relational predicate: a predicate on the points of a product (or of a carrier, for an atom on π), tagged is_rel_predicate; it meets its universe only at the former &.
concept	IsTerm
	A term of the grammar.
concept	IsConstant
	A value that can stand as a constant beside a term: copyable, with state, and not itself part of the grammar (a term, a predicate, an arrow, or an empty tag). The term test comes first, so asking this of a carrier never asks for the carrier's own equality.
concept	TermOperands
	The operands of an operator of the grammar: at least one term, the other a term or a constant.
concept	EmbedsInto
	A value of the sort D is read in the sort C: the same sort, or a truth chain along the dominance into C's species (𝔹 ↪ K₃, the registered lift_logic). The one coercion of the grammar; any other pair of carriers meets through an arrow applied, never implied.
concept	IsGraphAtom
	An atom that is the graph of a function of the first slot.

Typedefs
template<typename T>
using	dedekind::sets::default_cardinality_t = typename default_cardinality<T>::type
	The cardinality class a carrier declares by its representation: Finite for bool, ℵ_0 otherwise. This is the default of 𝔸's third parameter, so 𝔸<bool> is classified Finite and its cardinality metadata is honest (the species is Boole regardless).
template<typename D>
using	dedekind::sets::leg_1_t
	The legs of a product carrier: the types π_1 and π_2 return.
template<typename D>
using	dedekind::sets::leg_2_t
template<IsSetObject S>
using	dedekind::sets::universe_t
	The type of a set object's universe leg.
template<typename Term, typename L = Boole, typename Combine = no_leaf_combine>
using	dedekind::sets::subobject_reduce_t
	The lattice-law term reducer localised to the subobject lattice Sub(T): normalise Term under subobject_order<L> as both the semantic order (Ord, boundedness / distributivity) and the canonicalisation order (Less). The set-level meet and join routes fold through this one alias (the boundary operators below, and the free operator& / operator| over IsSubobject in :expressions), so the injected-order policy for Sub(T) is named in a single place (#865/#890, Phase 2). Complement does not route here: the free operator! in :expressions is a certified involution that eliminates double negation via the :involution witness (!!A ≡ A).
template<typename R>
using	dedekind::sets::codomain_reduce_t = typename codomain_reduce<R>::type
using	dedekind::sets::u64 = std::uint64_t
	u64 — the machine word, the carrier of the ring ℤ/2⁶⁴, named as the Python surface names it.
using	dedekind::sets::ℵ_0 = ℵ<0>
	Countable Infinity.
using	dedekind::sets::ℶ_1 = ℵ<1>
	The Continuum (assuming GCH).
using	dedekind::sets::Cardinality = std::variant<ExtensionalCardinal<>, ℵ_0>
	Sum type for finite vs countably infinite cardinalities; the library's bona-fide proxy for \(\mathbb{N}\) modulo physical limits.
using	dedekind::sets::SignedCardinality
	Signed counterpart of Cardinality with ±ℵ_0 escalation; the library's bona-fide proxy for \(\mathbb{Z}\) modulo physical limits.
template<typename Base, typename Predicate>
using	comprehension_logic_t
	The logic species of {base | pred}: the join (in the species semilattice, category::join_logic_t) of the base's species and the species of the predicate's answer, so a Kleene predicate over a Boole base lifts the base rather than truncating itself, and a Kleene predicate over a Percent base answers in Percent. A pair with no join (a K₃ answer over a Chain<int> base) is refused here.
template<typename A, typename B>
using	dedekind::sets::ProductMembership
	Membership of a cartesian product: \((x, y) \in A \times B \iff x \in A \wedge y \in B\), the meet of the two cylinders \(\chi_A \circ \pi_1\) and \(\chi_B \circ \pi_2\). So \(\chi_{A \times B} = \wedge \circ (\chi_A \times \chi_B)\) and \(A \times B = (A \times Y) \cap (X \times B)\): no predicate of its own, the library's meet (in the join of the factors' species, each answer lifted) over its projections composed with the factors.
using	CanonicalIntSet = 𝔸<int>
using	CanonicalIntProductSet
using	CanonicalIntProductDomain = typename CanonicalIntProductSet::Domain
template<typename UA, typename UB>
using	sum_universe_t = typename sum_universe<UA, UB>::type
template<std::equality_comparable T, IsOckhamAlgebra L = Boole>
using	dedekind::sets::Singleton = Comprehension<𝔸<T, L>, Point<T>>
	\(\{x\}\) as a set: the equality atom over the universe of T. An alias, not a noun: its operators are every comprehension's (the reducer's nodes); what is specific to a point follows as free functions.
template<typename A, typename B, typename RA, typename RB>
using	meet_t = typename decltype(meet_type<A, B, RA, RB>())::type
template<Rel R>
using	rel_key_t = typename rel_key<R>::type
template<typename P>
using	dedekind::sets::point_sorts_t = typename point_sorts<P>::type
template<typename P>
using	dedekind::sets::term_sorts_t
	The sorts a term at points of P takes: the points' carriers first (a slot's sort is its index there), then the truth chains a set applied to a term lands in, ap(S, t) of sort S's codomain.
template<typename P>
using	dedekind::sets::rt_value_t = typename value_sum<point_sorts_t<P>>::type
template<typename X, typename T>
using	dedekind::sets::value_at_t
	The value type a term takes at a point of type X.
template<IsGraphAtom P>
using	dedekind::sets::graph_term_t = typename graph_atom<P>::term
	The term of a graph atom.

Enumerations
enum class	dedekind::sets::Rel {   Lt , Le , Gt , Ge ,   Eq , Ne }
	The comparison an atom makes.
enum class	dedekind::sets::Arith {   Add , Sub , Mul , Div ,   FloorDiv , Mod }
	An operator of a term built at run time. Python's / and // are both the carrier's division; what differs is where each is admitted (a field, an ordered word).

Functions
template<typename C> requires dedekind::category::IsField<C, std::plus<C>, std::multiplies<C>> && dedekind::category::IsClosedUnder<C, std::divides<>>
constexpr bool	dedekind::sets::admits (On< C >, FieldDivision, bool divisor_is_constant)
	Division by a nonzero constant is in a field's signature: multiplication by the inverse (category::IsField, the axiomatic claim; the carrier closes under /). Its free algebra is the field's polynomials, with the constant's inverse a coefficient (:polynomial).
template<typename L, typename C, std::integral K1, std::integral K2>
constexpr ResidueClass< L >	dedekind::sets::operator& (const 𝔸< Cardinality, L, C > &, const Cmp< Rel::Eq, BinOp< std::modulus<>, Projection< 0 >, Const< K1 > >, Const< K2 > > &c)
	ℕ & (π % n == r): the residue class, decided analytically. A residue outside \([0, n)\) is never met, so π % 3 == 3 is empty. ADL finds it through the 𝔸<Cardinality> operand.
template<typename C> requires dedekind::order::IsDividableChain<C>
constexpr bool	dedekind::sets::admits (On< C >, EuclideanDivision, bool divisor_is_constant)
template<typename C> requires dedekind::order::IsDividableChain<C>
constexpr bool	dedekind::sets::admits (On< C >, std::modulus<>, bool divisor_is_constant)
template<dedekind::order::IsTotallyOrdered T, dedekind::category::IsOckhamAlgebra L, IsCardinality C, Rel R, typename K> requires (dedekind::order::is_order_rel(R))
constexpr dedekind::order::Interval< T, L >	dedekind::sets::operator& (const 𝔸< T, L, C > &, const Cmp< R, Projection< 0 >, Const< K > > &c)
	An order atom π ⋈ k on a chain is the ray it names, whatever the constant's type: the constant meets the carrier exactly or the binding raises. Declared beside 𝔸 and the atom, so ADL finds it.
template<typename C> requires dedekind::order::IsPartiallyOrdered<C>
constexpr bool	dedekind::sets::admits (On< C >, std::less<>, bool)
template<typename C> requires dedekind::order::IsPartiallyOrdered<C>
constexpr bool	dedekind::sets::admits (On< C >, std::less_equal<>, bool)
template<typename C> requires dedekind::order::IsPartiallyOrdered<C>
constexpr bool	dedekind::sets::admits (On< C >, std::greater<>, bool)
template<typename C> requires dedekind::order::IsPartiallyOrdered<C>
constexpr bool	dedekind::sets::admits (On< C >, std::greater_equal<>, bool)
template<typename S, typename T2, typename L> requires (IsLSet<S> && !std::same_as<S, Ø<typename S::Domain, L>>)
constexpr auto	dedekind::sets::operator* (const S &, const Ø< T2, L > &)
	S × Ø = Ø<pair<S::Domain, T2>, Boole>. Empty annihilates the cartesian product on the right. Symmetric companion to Ø::operator*; carrier widens to the pair type, codomain Boolean (an empty product is decided, #894).
template<typename T, typename L, typename C>
constexpr 𝔸< T, L, C >	dedekind::sets::universe (const 𝔸< T, L, C > &u)
	A universe is its own universe: the fixpoint of the universe leg.
template<IsLSet S> requires (!dedekind::category::IsTerminalObject<S>)
constexpr auto	dedekind::sets::universe (const S &)
	Default universe leg: 𝔸 over the set object's carrier and logic (the 𝔸 variable template's own default or specialisation for T).
template<IsLSet S>
constexpr S	dedekind::sets::classifier (const S &s)
	Default classifier leg: the set is its predicate (Definition Lwv, "the predicate χ_S is the set").
template<typename A, typename B, typename L, typename C>
constexpr auto	dedekind::sets::component (const 𝔸< std::pair< A, B >, L, C > &, dedekind::category::At< 1 >)
	The universe of a pair carrier is the product of the factor universes, 𝔸 ≅ 𝔸 × 𝔸: π_1 / π_2 project it (through their component hook) to the factors, so IsProduct<𝔸<pair<A,B>,L>, 𝔸<A,L>, 𝔸<B,L>> holds — the structural content of "a relation is a subobject of A × B" (Definition Trsk, §4), read off its universe leg.
template<typename A, typename B, typename L, typename C>
constexpr auto	dedekind::sets::component (const 𝔸< std::pair< A, B >, L, C > &, dedekind::category::At< 2 >)
template<typename R>
constexpr auto	dedekind::sets::finalize_combine (R r)
	The value-level twin of codomain_reduce_t: finalize a reduced normal-form value along the codomain leg (#894). When the reduced type is a IsBoundaryObject whose codomain re-tag actually changes the type, the result is a decided boundary, so construct the re-tagged (Boole) boundary; otherwise (an identity re-tag, or a non-boundary) the value passes through unchanged, so a tagged non-default-constructible survivor keeps its value. This is the single home for the value-finalization law: this partition's Ø / 𝔸 meet & join operators call it directly (they are declared below it), and :expressions (downstream) reuses it for the general subobject combine, so the rule is spelled once rather than duplicated. FIXME(#894): boundary → Boole is the only rule for now; the general form is image(χ) ⊆ Σ folded on the Kleene image lattice.
template<typename T, typename L>
constexpr Ø< T, L >	materialize_bounds (LatticeBottom< T, subobject_order< L > >)
template<typename T, typename L>
constexpr 𝔸< T, L >	materialize_bounds (LatticeTop< T, subobject_order< L > >)
template<typename R>
constexpr R	materialize_bounds (R r)
template<typename L = Boole, typename Combine = no_leaf_combine, IsSetObject Node>
constexpr auto	dedekind::sets::subobject_reduce (const Node &node)
	The domain reduce: fold a subobject lattice Node value (a Meet / Join / Not over Sub(T), or a leaf) to its normal-form value under subobject_order<L> through the one reducer (category::Reduce under cata), make an abstract bound concrete, then finalize the codomain leg. The same fold at compile time names the type subobject_reduce_t; at run time it preserves a runtime-stateful operand (a Singleton holding a value) where the normal form is that operand, so it is the entry the Python surface calls. The four Ø / 𝔸 meet & join operators and the free & / | / ~ over IsSetObject (:expressions) all route through here.
template<typename T, typename L, typename S> requires (IsLSet<S> && std::same_as<typename S::Domain, T>)
constexpr auto	dedekind::sets::operator& (const Ø< T, L > &, const S &s)
	Ø & S / Ø | S: Ø is the ⊥ of Sub(T) meeting / joining any set. Free operators (the Ø-LHS members were retired); overload resolution pins them by the Ø operand.
template<typename T, typename L, typename S> requires (IsLSet<S> && std::same_as<typename S::Domain, T>)
constexpr auto	dedekind::sets::operator| (const Ø< T, L > &, const S &s)
	Ø | S = S (⊥ is the join unit); see operator&.
template<typename T, typename L, typename C, typename S> requires (IsLSet<S> && std::same_as<typename S::Domain, T>)
constexpr auto	dedekind::sets::operator& (const 𝔸< T, L, C > &, const S &s)
	𝔸 & S / 𝔸 | S: 𝔸 is the ⊤ of Sub(T) meeting / joining any set. Free operators (the 𝔸-LHS members were retired); pinned by the 𝔸 operand.
template<typename T, typename L, typename C, typename S> requires (IsLSet<S> && std::same_as<typename S::Domain, T>)
constexpr auto	dedekind::sets::operator| (const 𝔸< T, L, C > &, const S &s)
	𝔸 | S = 𝔸 (⊤ is the join annihilator); see operator&.
template<typename S1, typename S2>
constexpr std::size_t	dedekind::sets::bound_meet (const S1 &lhs, const S2 &rhs)
template<typename S1, typename S2>
constexpr std::size_t	dedekind::sets::bound_join (const S1 &lhs, const S2 &rhs)
	ETCS-aligned upper bound for join/union cardinality.
template<IsWrappingWord W>
constexpr std::variant< ExtensionalCardinal< W >, ℵ_0 >	dedekind::sets::add_or_ℵ_0 (const ExtensionalCardinal< W > &lhs, const ExtensionalCardinal< W > &rhs)
template<IsWrappingWord W>
constexpr std::variant< ExtensionalCardinal< W >, ℵ_0 >	dedekind::sets::mul_or_ℵ_0 (const ExtensionalCardinal< W > &lhs, const ExtensionalCardinal< W > &rhs)
constexpr Cardinality	dedekind::sets::finite_cardinality (std::size_t n)
	Convenience constructor for finite cardinal values.
constexpr Cardinality	dedekind::sets::add (const Cardinality &lhs, const Cardinality &rhs)
	Cardinal addition under the finite/ℵ_0 policy.
constexpr Cardinality	dedekind::sets::mul (const Cardinality &lhs, const Cardinality &rhs)
	Cardinal multiplication under the finite/ℵ_0 policy.
constexpr std::strong_ordering	dedekind::sets::compare (const Cardinality &lhs, const Cardinality &rhs)
	Total comparison over the finite/ℵ_0 fragment.
constexpr bool	dedekind::sets::operator== (const Cardinality &lhs, const Cardinality &rhs) noexcept
	Explicit == on Cardinality. std::variant supplies a defaulted operator== inside the module's purview, but it is not reachable across the dedekind.sets module boundary (the <variant> header lives in the global module fragment, so its operator templates are not exported). Defining the operator explicitly in dedekind::sets — where ADL can find it from importers like dedekind.numbers — closes that gap so IsPartiallyOrdered<Cardinality> / std::three_way_comparable<Cardinality> fire downstream.
constexpr Cardinality	dedekind::sets::operator+ (const Cardinality &lhs, const Cardinality &rhs) noexcept
	+ on Cardinality wraps the existing add() policy (saturating to ℵ_0 on overflow).
constexpr Cardinality	dedekind::sets::successor (const Cardinality &n) noexcept
	The NNO steps on the ℕ proxy, as the free customization points the order layer's point collapse calls (category:nno, found here by ADL): successor is + finite_cardinality(1), saturating at ℵ_0 (its fixpoint); predecessor is the monus — 0 is its fixpoint (ℕ has no negatives), and ℵ_0 is fixed again. The :nno arrow Successor<Cardinality> delegates here, so the law is spelled once.
constexpr Cardinality	dedekind::sets::predecessor (const Cardinality &n) noexcept
constexpr Cardinality	dedekind::sets::operator++ (Cardinality n) noexcept
	++n / --n: the successor and the predecessor of the ℕ proxy, by value, saturating at ℵ₀ and stepping down by monus (#1002).
constexpr Cardinality	dedekind::sets::operator-- (Cardinality n) noexcept
constexpr Cardinality	dedekind::sets::operator* (const Cardinality &lhs, const Cardinality &rhs) noexcept
	* on Cardinality wraps the existing mul() policy.
constexpr Cardinality	dedekind::sets::operator/ (const Cardinality &lhs, const Cardinality &rhs) noexcept
	Euclidean division on Cardinality. Convention follows the ExtensionalCardinal<> totalisation: division by zero yields zero; finite / ℵ_0 yields zero (the limit); ℵ_0 / finite-non-zero yields ℵ_0; ℵ_0 / ℵ_0 yields ℵ_0 (saturation rather than indeterminate — Cardinality has no NaZ-equivalent sentinel; the ℕ proxy keeps the policy total).
constexpr Cardinality	dedekind::sets::operator% (const Cardinality &lhs, const Cardinality &rhs) noexcept
	Euclidean remainder on Cardinality. Mirrors the operator/ convention: finite % finite delegates to the underlying ExtensionalCardinal<>'s %; finite % ℵ_0 returns the lhs (the limit-style "remainder is the original" reading); operations with ℵ_0 on the lhs saturate to ℵ_0.
constexpr std::strong_ordering	dedekind::sets::operator<=> (const Cardinality &lhs, const Cardinality &rhs) noexcept
	Spaceship on Cardinality wraps compare() (finite values compare via the underlying ExtensionalCardinal<> spaceship; ℵ_0 dominates every finite value). Returns std::strong_ordering — there is no NaN-equivalent in the ℕ proxy.
constexpr std::size_t	dedekind::sets::realize_to_size_t (const Cardinality &value, std::size_t transfinite_sentinel=std::numeric_limits< std::size_t >::max())
	Realize a cardinality value to std::size_t with explicit boundary.
constexpr CardinalityEffect	dedekind::sets::unit_effect (Cardinality value)
	Unit for cardinality effect composition.
template<typename F> requires std::invocable<F&, const Cardinality&> && std::convertible_to<std::invoke_result_t<F&, const Cardinality&>, CardinalityEffect>
constexpr CardinalityEffect	dedekind::sets::bind_effect (const CardinalityEffect &effect, F f)
	Sequential composition of cardinality effects.
constexpr ExtensionalCardinal	dedekind::sets::inverse (ExtensionalCardinal<> value, std::plus< ExtensionalCardinal<> >)
	Additive inverse of ExtensionalCardinal<> (two's-complement).
template<typename T> requires requires(T x) { { -x } -> std::convertible_to<T>; }
constexpr T	dedekind::sets::inverse (const T &x, std::plus< T >)
	Generic additive inverse for a carrier supporting unary negation: the +-inverse is -x, inferred from the negation structure rather than registered per carrier.
constexpr bool	dedekind::sets::is_finite (const SignedCardinality &v) noexcept
	Is this signed cardinal a FINITE ℤ value (not ±ℵ_0 / NaZ)? The public query behind Honest-Rejection guards at the carrier boundary — e.g. Rational::simplify skips euclidean_gcd (which would not terminate on a NaZ, since NaZ % · == NaZ) when a numerator/denominator is a non-finite sentinel (#680).
template<std::integral S>
constexpr SignedCardinality	dedekind::sets::finite_signed_cardinality (S value) noexcept
	Convenience constructor for finite signed values.
template<std::integral K>
constexpr Cardinality	dedekind::sets::carrier_cast (std::type_identity< Cardinality >, K k)
	An integer constant meeting ℕ or ℤ, the hook the term grammar's carrier_cast reaches by ADL: exactly, or a domain error for a negative constant meeting ℕ.
template<std::integral K>
constexpr SignedCardinality	dedekind::sets::carrier_cast (std::type_identity< SignedCardinality >, K k)
constexpr SignedCardinality	dedekind::sets::operator- (const SignedCardinality &v) noexcept
	Unary negation: swaps signs and ±ℵ_0; preserves NaZ.
constexpr SignedCardinality	dedekind::sets::operator+ (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Addition with ±ℵ_0 escalation on overflow.
constexpr SignedCardinality	dedekind::sets::operator- (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Subtraction, computed directly so that only an overflowing difference saturates (a + (−b) would saturate −min first, so min − min would not be 0). Infinities as for a + (−b).
constexpr SignedCardinality	dedekind::sets::successor (const SignedCardinality &n) noexcept
	The step up on the ℤ proxy, the free customization point the order layer's point collapse calls (category:nno, found here by ADL), as on Cardinality: +1 through the saturating +, so +ℵ_0 is a fixpoint and NaZ propagates.
constexpr SignedCardinality	dedekind::sets::predecessor (const SignedCardinality &n) noexcept
	The step down on the ℤ proxy: −1 through the saturating -, so −ℵ_0 is a fixpoint and NaZ propagates. Unlike ℕ there is no monus: ℤ steps down past zero.
constexpr SignedCardinality	dedekind::sets::operator* (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Multiplication with ±ℵ_0 escalation on overflow. 0 * ±ℵ_0 is indeterminate (returns NaZ).
constexpr SignedCardinality	dedekind::sets::operator/ (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Truncating division. Division by zero and ±ℵ_0/±ℵ_0 return NaZ; finite/±ℵ_0 returns 0 (the limit); ±ℵ_0 divided by a non-zero finite value saturates to signed infinity according to the operand signs.
constexpr SignedCardinality	dedekind::sets::operator% (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Truncating remainder. Mirrors C++ semantics on the finite alternative; non-finite operands give NaZ.
constexpr std::partial_ordering	dedekind::sets::compare_signed (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Partial ordering on the extended integers: −ℵ_0 < finite < +ℵ_0; NaZ is unordered with respect to everything (including itself), mirroring IEEE-NaN's unordered semantics. Returning std::partial_ordering rather than std::strong_ordering is the principled choice: NaZ compares unordered, which keeps ordering and equality (variant's defaulted ==, which finds NaZ == NaZ true) consistent without forcing a fake equal answer.
constexpr bool	dedekind::sets::operator< (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	< derived from compare_signed; required by IsInteger. For NaZ operands the comparison is unordered so this returns false, mirroring IEEE-NaN's < behaviour.
constexpr bool	dedekind::sets::operator== (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Explicit homogeneous == on SignedCardinality (#669).
constexpr std::partial_ordering	dedekind::sets::operator<=> (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	Explicit homogeneous <=> on SignedCardinality (#669).
constexpr std::weak_ordering	dedekind::sets::constant_order (const SignedCardinality &lhs, const SignedCardinality &rhs) noexcept
	The structural order of signed cardinalities as constants of a term (#884, canonical's sort key): total, unlike <=>. By alternative first (finite, +∞, −∞, then NaZ), a finite value by its order.
template<std::integral T>
constexpr std::strong_ordering	dedekind::sets::operator<=> (const Cardinality &lhs, T rhs) noexcept
	Cardinality <=> std::integral. ℵ_0 is greater than any finite integer; negative signed values are below the entire ℕ proxy (no element of Cardinality is negative), which is encoded as lhs > rhs. Otherwise the comparison reduces to the ExtensionalCardinal<> spaceship. Delegates the integral lift through ExtensionalCardinal<>'s existing std::integral ctor, which subsumes bool / size_t / signed-non-negative paths uniformly — avoiding std::make_unsigned_t (undefined for bool).
template<std::integral T>
constexpr bool	dedekind::sets::operator== (const Cardinality &lhs, T rhs) noexcept
	Cardinality == std::integral. Negative signed values and ℵ_0 never equal a finite integer; the finite alternative delegates to ExtensionalCardinal<>'s defaulted ==.
template<std::integral T>
constexpr std::partial_ordering	dedekind::sets::operator<=> (const SignedCardinality &lhs, T rhs) noexcept
	SignedCardinality <=> std::integral. Lifts rhs to a finite SignedCardinality and routes through compare_signed; NaZ on lhs propagates as std::partial_ordering::unordered, mirroring IEEE-NaN's unordered semantics.
template<std::integral T>
constexpr bool	dedekind::sets::operator== (const SignedCardinality &lhs, T rhs) noexcept
	SignedCardinality == std::integral. NaZ and ±ℵ_0 never equal a finite integer; the finite alternative delegates to SignedExtensionalCardinal<>'s canonical-zero-aware equality.
template<std::floating_point F>
constexpr std::partial_ordering	dedekind::sets::operator<=> (const Cardinality &lhs, F rhs) noexcept
	Cardinality <=> std::floating_point. ℵ_0 is greater than every finite double (and equivalent to +inf); negative finite floats and -inf land strictly below the ℕ proxy. A NaN rhs returns std::partial_ordering::unordered. Finite-vs-finite is settled in integer domain via compare_unsigned_to_floating, which stays precision-correct even when the underlying word exceeds 2^digits <F>.
template<std::floating_point F>
constexpr bool	dedekind::sets::operator== (const Cardinality &lhs, F rhs) noexcept
	Cardinality == std::floating_point. Equality requires either ℵ_0 vs +inf, or finite lhs equal to a finite, non-negative, integer-valued rhs in the carrier's representable range. Float rounding cannot fake equality (eq_unsigned_to_floating compares in integer domain).
template<std::floating_point F>
constexpr std::partial_ordering	dedekind::sets::operator<=> (const SignedCardinality &lhs, F rhs) noexcept
	SignedCardinality <=> std::floating_point. NaZ propagates as unordered (mirrors compare_signed's NaZ semantics); ±ℵ_0 maps to ±inf-equivalent; NaN rhs returns unordered. Finite-vs-finite is settled by sign-aware delegation to the unsigned integer- domain helper, so the comparison stays precision-correct even when the underlying magnitude exceeds 2^digits <F>.
template<std::floating_point F>
constexpr bool	dedekind::sets::operator== (const SignedCardinality &lhs, F rhs) noexcept
	SignedCardinality == std::floating_point. NaZ / NaN never equal anything; ±ℵ_0 equals only ±inf; finite delegates to the integer-domain eq_unsigned_to_floating on the magnitude with sign reconciled, so float rounding cannot fake equality on large-magnitude integers.
constexpr SignedCardinality	dedekind::sets::lift_cardinality_to_signed (const Cardinality &c) noexcept
	Lift Cardinality into SignedCardinality via the canonical ℕ ↪ ℤ embedding direction. Public, exported: this is the canonical variant-level ℕ ↪ ℤ embedding that the carrier-lattice diagram (Figure 1 in paper.tex) labels at the top row. The machine-layer counterpart is embed_uint_sint_ in numbers:integer (an arrow<unsigned, int> sign reinterpretation, structurally distinct from the variant- layer canonical embedding here). Lives in sets:cardinality so the cross-variant operators below reach it without crossing the sets → numbers module boundary; an exported arrow form lift_ℕ_ℤ_ wrapping this function lives in numbers:integer for monic-arrow registration in the carrier lattice.
constexpr std::partial_ordering	dedekind::sets::operator<=> (const Cardinality &lhs, const SignedCardinality &rhs) noexcept
	Cardinality <=> SignedCardinality. Routes through the canonical ℕ ↪ ℤ lift and compare_signed; NaZ on the rhs propagates as unordered.
constexpr bool	dedekind::sets::operator== (const Cardinality &lhs, const SignedCardinality &rhs) noexcept
	Cardinality == SignedCardinality. NaZ never equals anything; otherwise the canonical lift settles the comparison.
constexpr SignedCardinality	dedekind::sets::operator- (const Cardinality &v) noexcept
	Closure-forcing unary minus on Cardinality: well-defined on every natural, with codomain widened to SignedCardinality. Delegates to the canonical lift lift_cardinality_to_signed and SignedCardinality's existing unary -, so canonicalisation rules (canonical +0 for negation-of-zero; +ℵ_0 → -ℵ_0 sentinel flip) flow from a single source of truth. This is the smallest possible elementwise statement of the Grothendieck construction in code.
constexpr Cardinality	dedekind::sets::abs (const SignedCardinality &z) noexcept
	Retraction direction: abs : ℤ → ℕ. The math- honest signature for absolute value: every element of SignedCardinality has a non-negative magnitude, so the result type is Cardinality (not SignedCardinality), announcing the non-negativity guarantee at the type level.
constexpr SignedCardinality	dedekind::sets::operator- (const Cardinality &a, const Cardinality &b) noexcept
	Closure-forcing binary minus on Cardinality: well-defined as a function ℕ × ℕ → ℤ; ℕ isn't closed under it. The operator's existence with the wider return type is the Grothendieck embedding made operational at the binary level. Routes through lift_cardinality_to_signed on both operands and dispatches to SignedCardinality's -.
constexpr SignedCardinality	dedekind::sets::operator+ (const Cardinality &a, const SignedCardinality &b) noexcept
	Closed cross-carrier addition: Cardinality + SignedCardinality lifts the Cardinality through the canonical embedding and dispatches to SignedCardinality's +. Closes in ℤ. Carrier-promotion in the math-correct direction (larger carrier wins).
constexpr SignedCardinality	dedekind::sets::operator+ (const SignedCardinality &a, const Cardinality &b) noexcept
	Symmetric: SignedCardinality + Cardinality. Delegates to the canonical direction; addition is commutative on ℤ.
constexpr SignedCardinality	dedekind::sets::operator- (const Cardinality &a, const SignedCardinality &b) noexcept
	Closure-forcing cross-carrier subtraction: Cardinality - SignedCardinality. Result is in ℤ — well-defined on the (ℕ, ℤ) pair as a function into ℤ.
constexpr SignedCardinality	dedekind::sets::operator- (const SignedCardinality &a, const Cardinality &b) noexcept
	Symmetric: SignedCardinality - Cardinality. Lifts b through the embedding; result is in ℤ. Subtraction is not commutative, so this is a separate overload, not a delegation.
constexpr SignedCardinality	dedekind::sets::operator* (const Cardinality &a, const SignedCardinality &b) noexcept
	Closed cross-carrier multiplication: Cardinality * SignedCardinality lifts and dispatches. Closes in ℤ.
constexpr SignedCardinality	dedekind::sets::operator* (const SignedCardinality &a, const Cardinality &b) noexcept
	Symmetric: SignedCardinality * Cardinality. Multiplication is commutative; delegates to the canonical direction.
template<IsWrappingWord W>
constexpr ExtensionalCardinal< W >	dedekind::sets::successor (const ExtensionalCardinal< W > &n) noexcept
	The NNO's step on the extensional cardinals, the wrapping ring \(\mathbb{Z}/2^w\): n + 1 and n - 1 modulo the word, as on the word itself.
template<IsWrappingWord W>
constexpr ExtensionalCardinal< W >	dedekind::sets::predecessor (const ExtensionalCardinal< W > &n) noexcept
template<std::integral S>
constexpr SignedExtensionalCardinal< S >	dedekind::sets::successor (const SignedExtensionalCardinal< S > &n) noexcept
template<std::integral S>
constexpr SignedExtensionalCardinal< S >	dedekind::sets::predecessor (const SignedExtensionalCardinal< S > &n) noexcept
template<typename T, IsOckhamAlgebra L, IsCardinality C, IsDatum< T > P>
constexpr auto	dedekind::sets::operator& (const 𝔸< T, L, C > &, P p)
	The set former 𝔸<T, L>{} & P = \(\{x \in T \mid P(x)\}\) for a datum P (a point π == v, a cut π > v): the meet with the subobject P classifies (#826; | is the join only).
template<typename T, IsOckhamAlgebra L, IsCardinality C, IsRelPredicate P> requires (only_slot(slots_v<P>, 0)) && (!contains_self_v<P>) && std::convertible_to<std::invoke_result_t<const P&, const T&>, bool>
constexpr auto	dedekind::sets::operator& (const 𝔸< T, L, C > &, P p)
	𝔸<T> & atom for an atom on the unary π (ℕ & (π % 3 == 0)): the atom evaluated at each element.
template<typename T, IsOckhamAlgebra L, IsCardinality C, typename K> requires (!requires { typename T::first_type; })
constexpr auto	dedekind::sets::operator& (const 𝔸< T, L, C > &, Pred< K > p)
	𝔸<T> & pred for a predicate built at run time: bound to the carrier now, every operator admitted there or refused (not_admitted), every constant meeting it. Pairs take the product former.
template<typename S, typename P> requires IsSetObject<S> && (!IsSetObject<P>) && (!IsLSet<P>)
void	dedekind::sets::operator| (const S &, const P &)=delete
	S | P for a set and a non-set: refused. The filter is the meet, S & P (#826); | is the join of two sets only.
template<typename TargetL, IsSetObject S> requires dedekind::category::LiftsTo<typename S::logic_species, TargetL>
constexpr auto	dedekind::sets::lift_to (const S &s)
	Bring a set object to the species TargetL along the dominance: the identity when it is already there, else the comprehension {x ∈ 𝔸<T, TargetL> | s(x)}. Its species is the join, which is TargetL since s's species embeds into it, and its χ is lift_logic<TargetL>(s(x)) (the universe answers ⊤): the lift is composition with the dominance embedding, no wrapper type. It does not preserve the operand's structural type (interval / halfspace), so a cross-species combine materialises pointwise rather than collapsing structurally. Constrained to a registered inclusion, so a downward or unsupported lift is rejected at the gate.
template<typename T, IsOckhamAlgebra L, typename Reduced>
constexpr auto	dedekind::sets::elevate_meet (Reduced reduced)
	Value-level elevate of a structured_and result to the meet's normal-form value: an empty reduction is the initial object Ø; a finite reduction (a point) is itself a set-like leaf (returned bare); any other reduction is a named predicate wrapped back into a comprehension. (Extracted verbatim from the pre-reducer operator& structured_and branch so SetCombine's type and this value stay in lockstep.).
template<typename T, typename L, typename Reduced>
constexpr auto	dedekind::sets::elevate_join (Reduced reduced)
	Value-level elevate of a structured_or result to the join's normal-form value: a covering pair is the universe 𝔸 (returned bare); any other reduction (a wider halfspace) is wrapped back into a Set. Dual of elevate_meet.
template<typename Base, typename Predicate>
constexpr auto	dedekind::sets::universe (const Comprehension< Base, Predicate > &)
template<typename T, IsOckhamAlgebra L, typename P, IsCardinality C>
constexpr P	dedekind::sets::classifier (const Comprehension< 𝔸< T, L, C >, P > &s)
template<typename LHS, typename RHS> requires IsSetObject<LHS> && IsSetObject<RHS> && (!(dedekind::category::builds_lattice_nodes<LHS>::value && dedekind::category::builds_lattice_nodes<RHS>::value)) && std::same_as<typename LHS::Domain, typename RHS::Domain> && std::same_as<typename LHS::logic_species, typename RHS::logic_species>
constexpr auto	dedekind::sets::operator& (const LHS &lhs, const RHS &rhs)
	The subobject-lattice meet A & B, over any two IsSubobject operands sharing a carrier and logic. It folds Meet<A,B> through the reducer; SetCombine supplies the domain structured_and at the incomparable residual. The normal form materialises to Ø, 𝔸, an operand, or a structured leaf. An irreducible meet becomes a Meet carrying both operand sets.
template<typename LHS, typename RHS> requires IsSetObject<LHS> && IsSetObject<RHS> && (!(dedekind::category::builds_lattice_nodes<LHS>::value && dedekind::category::builds_lattice_nodes<RHS>::value)) && std::same_as<typename LHS::Domain, typename RHS::Domain> && std::same_as<typename LHS::logic_species, typename RHS::logic_species>
constexpr auto	dedekind::sets::operator| (const LHS &lhs, const RHS &rhs)
	The subobject-lattice join A | B, dual to operator&. An irreducible join becomes a Join carrying both operand sets.
template<typename LHS, typename RHS> requires IsSetObject<LHS> && IsSetObject<RHS> && (!(dedekind::category::builds_lattice_nodes<LHS>::value && dedekind::category::builds_lattice_nodes<RHS>::value)) && std::same_as<typename LHS::Domain, typename RHS::Domain> && (!std::same_as<typename LHS::logic_species, typename RHS::logic_species>) && dedekind::category::HaveLogicJoin<typename LHS::logic_species, typename RHS::logic_species>
constexpr auto	dedekind::sets::operator& (const LHS &lhs, const RHS &rhs)
	Cross-species meet (#894, step i): two subobjects over the same carrier but different codomains join to the more expressive one (the species semilattice's join, category::join_logic_t; refused when no shipped species is above both); lift both there, then the same-species meet above folds them. This lets a mixed Boole ∩ Kleene combine into the reducer at all. Same-species combines are untouched (this overload requires the species to differ, so it never competes with the meet above).
template<typename LHS, typename RHS> requires IsSetObject<LHS> && IsSetObject<RHS> && (!(dedekind::category::builds_lattice_nodes<LHS>::value && dedekind::category::builds_lattice_nodes<RHS>::value)) && std::same_as<typename LHS::Domain, typename RHS::Domain> && (!std::same_as<typename LHS::logic_species, typename RHS::logic_species>) && dedekind::category::HaveLogicJoin<typename LHS::logic_species, typename RHS::logic_species>
constexpr auto	dedekind::sets::operator| (const LHS &lhs, const RHS &rhs)
	Cross-species join, dual to the cross-species meet (#894, step i).
template<IsPredicate P> requires IsSetObject<std::remove_cvref_t<P>>
constexpr auto	dedekind::sets::operator~ (const P &p)
	The set complement ~A (#829: ~ is the SET complement; ! is the predicate complement, which category::operator! supplies as a formal Morphism). ~A is the reducer's own Not node — a first-class subobject whose χ is the codomain reflection Ω::RFL of A's, generic over any bounded chain (Boole !, Kleene ¬U=U, and any registered Chain). There is no bespoke wrapper and no is_set_node_v tag: the gate is the structural IsSubobject, and because category defines no operator~ there is nothing to out-prioritise, so the tag that once disambiguated the two operator! overloads is gone (#963). The const reference parameter (matching operator& / operator|) makes this a FALLBACK that loses partial ordering to a type-specific complement, so a :order Halfspace / Singleton operator~ still wins for its own type (its closed-form collapse, e.g. ~Above<5> = AtMost<5>).
template<typename LHS, typename RHS> requires IsSetObject<LHS> && IsSetObject<RHS> && std::same_as<typename LHS::Domain, typename RHS::Domain> && std::same_as<typename LHS::logic_species, typename RHS::logic_species>
constexpr auto	dedekind::sets::operator^ (const LHS &a, const RHS &b)
	Symmetric difference A △ B (set-theoretic XOR; #469), a FREE combinator over IsSubobject (like & / | / ~), so it composes uniformly whether an operand is a Set, a Meet / Join, or a Not complement node. The textbook identity A△B = (A∩ ¬B)∪(¬A∩B): no bespoke XOR predicate — ~ / & / | carry the per-carrier logic and the reducer collapses the result, including A△¬A = 𝔸 via the join-complement law on a complemented codomain. The disjoint fast path (A∩B = Ø ⟹ A△B = A∪B) is kept for the halfspace-style compile-time collapse.
template<IsSetObject LHS, IsSetObject RHS> requires std::same_as<typename LHS::Domain, typename RHS::Domain> && (!std::same_as<typename LHS::logic_species, typename RHS::logic_species>) && dedekind::category::HaveLogicJoin<typename LHS::logic_species, typename RHS::logic_species>
constexpr auto	dedekind::sets::operator^ (const LHS &a, const RHS &b)
	Cross-species symmetric difference: both operands are lifted into the join of their species and △ is computed there (as for & and |).
template<typename A, typename B> requires IsSetObject<Meet<A, B>> && IsSubobject<A, typename A::Domain> && IsSubobject<B, typename B::Domain>
constexpr auto	dedekind::sets::as_pullback (const Meet< A, B > &m)
	The pullback apex of an applied meet: the same set, viewed with the subobject surface and the projection legs π_1 / π_2 (IsPullback), category's view over the node.
template<typename A, typename B> requires IsSetObject<Join<A, B>> && IsSubobject<A, typename A::Domain> && IsSubobject<B, typename B::Domain>
constexpr auto	dedekind::sets::as_pushout (const Join< A, B > &j)
	The pushout apex of an applied join, dual to as_pullback.
template<dedekind::category::IsArrow F, IsSetObject S> requires std::same_as<dedekind::category::Dom<std::remove_cvref_t<F>>, typename S::Domain>
constexpr auto	dedekind::sets::image (F &&, const S &)
	image(f, {x ∈ 𝔸 | P}) — image of an intensional set under an arrow. Layer 1 of #602.
template<dedekind::category::IsIsomorphism F, IsSetObject S> requires std::same_as<dedekind::category::Dom<std::remove_cvref_t<F>>, typename S::Domain>
constexpr auto	dedekind::sets::image (F &&f, const S &s)
	image(iso f, {x ∈ 𝔸 | P}) — decidable specialisation for isomorphism arrows (#602 Layer 2 entry).
template<typename T, typename L, typename C, dedekind::category::IsIsomorphism F> requires (std::same_as<dedekind::category::Dom<std::remove_cvref_t<F>>, T> && !dedekind::category::IsTerminalMorphism<std::remove_cvref_t<F>>)
constexpr auto	dedekind::sets::image (F &&, const 𝔸< T, L, C > &)
	image of the unbounded universe under an iso F:T→U is the universe of the codomain, 𝔸: an iso is surjective, so it fixes the universe setwise — but onto U, not T. For an endo-iso (U==T) this is 𝔸<T> unchanged; for a heterogeneous iso (e.g. Modular<2> → bool) it correctly returns 𝔸<bool> so callers can query codomain values.
template<dedekind::category::IsRetractableArrow F, IsSetObject S> requires std::same_as<dedekind::category::Dom<std::remove_cvref_t<F>>, typename S::Domain> && (!dedekind::category::IsIsomorphism<std::remove_cvref_t<F>>)
constexpr auto	dedekind::sets::image (F &&f, const S &s)
	image(monic-with-retract f, {x ∈ 𝔸 | P}) — decidable specialisation for monic arrows that ship a retract (a partial inverse via the retract(f) ADL hook). #602 Layer 2 / Case A.
template<typename T, typename L, typename Predicate, typename C, typename LB>
constexpr auto	dedekind::sets::operator^ (const Comprehension< 𝔸< T, L, C >, Predicate > &s, const Ø< T, LB > &)
	Set ^ Ø = Set (symmetric difference with empty is identity). Symmetric of Ø::operator^(S): picks up S ^ Ø when the boundary is on the right, keeping the structural collapse type-level. The boundary's species tag is immaterial (∅ is decided), so it is not matched against the set's.
template<typename T, typename L, typename C, typename Predicate, typename LB, typename CB>
constexpr auto	dedekind::sets::operator^ (const Comprehension< 𝔸< T, L, C >, Predicate > &s, const 𝔸< T, LB, CB > &)
	Set ^ 𝔸 = ¬Set (symmetric difference with the universe is the complement). Symmetric of 𝔸::operator^(S); the universe's species tag is immaterial (⊤ is decided). ~ is the SET complement (a set object); ! would be the predicate complement, an arrow.
template<IsLogicalTerm P1, IsLogicalTerm P2> requires (!IsPredicatePair<P1, P2>)
constexpr auto	dedekind::sets::operator&& (P1 &&p1, P2 &&p2)
	Predicate-level conjunction p1 && p2: structured_and when a domain collapse applies, else the reducer's Meet node, a callable predicate \(\chi_1 \wedge \chi_2\) that also carries its operands via π_1 / π_2. It is the same AST the set-level combinators use, so a set-builder Set{x | p1 && p2} shares one representation with A & B. There is no separate AndPredicate. A pair of predicates over one species is :topoi's conjunction (IsPredicatePair, which closes on IsPredicate); this one takes every other pair of terms.
template<IsLogicalTerm P1, IsLogicalTerm P2> requires (!IsPredicatePair<P1, P2>)
constexpr auto	dedekind::sets::operator|| (P1 &&p1, P2 &&p2)
	Predicate-level disjunction p1 || p2, dual to operator&&: structured_or when a collapse applies, else the reducer's Join node; a pair of predicates over one species is :topoi's (IsPredicatePair).
template<typename S> requires SetShaped<S>
auto	dedekind::sets::power_set (const S &)=delete
	Power set \(\mathfrak{P}(S)\) — the default declaration (customization-point gate).
template<typename S> requires SetShaped<S>
auto	dedekind::sets::𝔓 (const S &)=delete
	Textbook fraktur-P alias for power_set (the deleted default gate). Mirrored on the Python side as dedekind.sets.𝔓.
template<typename T, typename L>
constexpr auto	dedekind::sets::power_set (const Ø< T, L > &)
	\(\mathfrak{P}(\emptyset) = \{\emptyset\}\) — the one power set that needs no subobject normal-form, so it is a closed form here in :sets.
template<typename T, typename L>
constexpr auto	dedekind::sets::𝔓 (const Ø< T, L > &)
template<typename StdSetLike, typename T, typename L, typename Hash, typename Equal> requires detail::StdSetLikeOf<StdSetLike, T>
constexpr auto	dedekind::sets::to_std (const dedekind::sets::ExtensionalSet< T, L, Hash, Equal > &source) -> StdSetLike
template<typename StdSetLike, typename ExtSet>
constexpr auto	dedekind::sets::to_std (const ExtSet &) -> StdSetLike
template<typename T, typename Alloc> requires dedekind::category::IsHashFunction<std::hash<T>, T> && std::regular<T>
constexpr auto	dedekind::sets::from_std (const std::set< T, std::less< T >, Alloc > &source) -> dedekind::sets::ExtensionalSet< T >
template<typename T, typename Alloc> requires (!dedekind::category::IsHashFunction<std::hash<T>, T> || !std::regular<T>)
constexpr auto	dedekind::sets::from_std (const std::set< T, std::less< T >, Alloc > &) -> dedekind::sets::ExtensionalSet< T >
template<typename T, typename Compare, typename Alloc> requires (!std::same_as<Compare, std::less<T>>)
constexpr auto	dedekind::sets::from_std (const std::set< T, Compare, Alloc > &) -> dedekind::sets::ExtensionalSet< T >
template<typename T, typename Hash, typename Equal, typename Alloc>
constexpr auto	dedekind::sets::from_std (const std::unordered_set< T, Hash, Equal, Alloc > &source) -> dedekind::sets::ExtensionalSet< T, dedekind::category::Boole, Hash, Equal >
template<typename StdSetLike> requires dedekind::sets::StdSetLike<StdSetLike>
constexpr auto	dedekind::sets::from_std (const StdSetLike &) -> dedekind::sets::ExtensionalSet< typename StdSetLike::value_type >
template<typename ExtSet, typename StdSetLike>
constexpr auto	dedekind::sets::from_std (const StdSetLike &) -> ExtSet
template<typename U, typename Chi> requires std::ranges::input_range<const U> && std::totally_ordered<std::ranges::range_value_t<const U>> && std::invocable<const Chi&, std::ranges::range_reference_t<const U>> && std::constructible_from< bool, std::invoke_result_t< const Chi&, std::ranges::range_reference_t<const U>>>
constexpr auto	dedekind::sets::ext (const U &universe, Chi chi)
	μ: Int ⇀ Ext, the partial retraction of ambient_set.
template<typename T, typename Hash, typename Equal, typename Alloc, typename F> requires std::invocable<F&, const T&>
constexpr auto	dedekind::sets::image (F f, const std::unordered_set< T, Hash, Equal, Alloc > &s)
	image(f, std::unordered_set<T, Hash, Equal, Alloc>). An rvalue source binds here too: the image is a new container either way.
template<typename T, typename Compare, typename Alloc, typename F> requires std::invocable<F&, const T&>
constexpr auto	dedekind::sets::image (F f, const std::set< T, Compare, Alloc > &s)
	image(f, std::set<T, Compare, Alloc>).
template<typename T, typename Hash, typename Equal, typename Alloc, typename P> requires std::predicate<const P&, const T&>
constexpr auto	dedekind::sets::filter (P p, const std::unordered_set< T, Hash, Equal, Alloc > &s)
	filter(p, std::unordered_set<T, Hash, Equal, Alloc>).
template<typename T, typename Compare, typename Alloc, typename P> requires std::predicate<const P&, const T&>
constexpr auto	dedekind::sets::filter (P p, const std::set< T, Compare, Alloc > &s)
	filter(p, std::set<T, Compare, Alloc>).
template<typename A, typename B> requires NatZedPair<A, B>
constexpr auto	dedekind::sets::operator& (const A &lhs, const B &rhs)
	Cross-carrier meet: a set over ℕ & a set over ℤ → a set over ℕ (carrier strength-reduction; closes a slice of #362). The intersection is contained in ℕ, so the result carrier is Cardinality.
template<typename A, typename B> requires NatZedPair<B, A>
constexpr auto	dedekind::sets::operator& (const A &lhs, const B &rhs)
	Symmetric: a set over ℤ & a set over ℕ delegates to the canonical direction; the result still tightens to ℕ.
template<typename A, typename B> requires NatZedPair<A, B>
constexpr auto	dedekind::sets::operator| (const A &lhs, const B &rhs)
	Cross-carrier join: a set over ℕ | a set over ℤ → a set over ℤ (carrier widening; closes a slice of #362). The union may contain negative integers from the rhs side, so the result carrier widens to ℤ.
template<typename A, typename B> requires NatZedPair<B, A>
constexpr auto	dedekind::sets::operator| (const A &lhs, const B &rhs)
	Symmetric: a set over ℤ | a set over ℕ delegates to the canonical direction; the result still widens to ℤ.
template<typename A, typename B>
constexpr ProductMembership< A, B >	product_membership (const A &a, const B &b)
	The product's membership, built from its factors.
template<typename T1, typename L1, typename P1, typename T2, typename L2, typename P2, typename C1, typename C2> requires dedekind::category::HaveLogicJoin< typename Comprehension<𝔸<T1, L1, C1>, P1>::logic_species, typename Comprehension<𝔸<T2, L2, C2>, P2>::logic_species>
constexpr auto	dedekind::sets::cartesian_product (const Comprehension< 𝔸< T1, L1, C1 >, P1 > &a, const Comprehension< 𝔸< T2, L2, C2 >, P2 > &b)
	Cartesian product of two sets: {(a,b) | a ∈ A, b ∈ B}.
template<typename A, typename LA, typename CA, typename B, typename LB, typename CB> requires dedekind::category::HaveLogicJoin<LA, LB>
constexpr auto	dedekind::sets::cartesian_product (const 𝔸< A, LA, CA > &a, const 𝔸< B, LB, CB > &b)
	\(\mathbb{A}_A \times \mathbb{A}_B = \mathbb{A}_{A\times B}\): the product of two universes is the universe over the pair carrier, in the join of the factors' species.
template<IsSetObject A, IsSetObject B>
constexpr auto	dedekind::sets::cartesian_product (const A &a, const B &b)
	Cartesian product over arbitrary set objects.
template<typename A, typename LA, typename CA, typename B, typename LB, typename CB> requires std::same_as<LA, LB>
constexpr auto	dedekind::sets::operator* (const 𝔸< A, LA, CA > &a, const 𝔸< B, LB, CB > &b)
	The universal set of products: \(\mathbb{A}_A \times \mathbb{A}_B = \mathbb{A}_{A\times B}\), spelled as the universe over the product carrier (IsProduct).
template<typename T1, typename L1, typename P1, typename T2, typename L2, typename P2, typename C1, typename C2> requires std::same_as<L1, L2>
constexpr auto	dedekind::sets::operator* (const Comprehension< 𝔸< T1, L1, C1 >, P1 > &a, const Comprehension< 𝔸< T2, L2, C2 >, P2 > &b)
	Infix sugar for cartesian product over sets.
template<IsSetObject A, IsSetObject B>
constexpr auto	dedekind::sets::operator* (const A &a, const B &b)
	Infix sugar for cartesian product over ambient species values. A set is also an arrow (its χ), and IsSetObject says so, so this overload is more constrained than the arrows' * (the product functor, category:cartesian): on sets, * is the cartesian product.
template<typename T1, typename T2, typename L, typename C, typename A, typename B>
constexpr auto	dedekind::sets::component (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, ProductMembership< A, B > > &s, dedekind::category::At< 1 >)
	The product of two set objects is their categorical product, not only their carriers' (#970, #1039): π_1 / π_2 on A × B return the factor set objects, which the membership already carries. With the carrier-level IsProduct above and the universes' (boundaries), IsProduct<decltype(A * B), A, B> holds for set objects.
template<typename T1, typename T2, typename L, typename C, typename A, typename B>
constexpr auto	dedekind::sets::component (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, ProductMembership< A, B > > &s, dedekind::category::At< 2 >)
template<Is𝔸 USum, IsSetObject A, IsSetObject B>
constexpr auto	sum_over (const A &a, const B &b)
	The subobject (a, b) of the sum over the universe USum, as built: no reduction. sum reduces first; the pushforward Inject never does.
template<IsSetObject A, IsSetObject B>
constexpr auto	dedekind::sets::sum (const A &a, const B &b)
template<typename A, typename B> requires HeterogeneousPair<A, B>
constexpr auto	dedekind::sets::operator| (const A &a, const B &b)
	a | b on different carriers: their sum.
template<typename A, typename B> requires HeterogeneousPair<A, B>
constexpr auto	dedekind::sets::operator& (const A &, const B &)
	a & b on different carriers: the summands of a sum are disjoint, so the meet is the empty set of the sum.
template<std::size_t K, typename X, typename Y, typename L, typename C, typename A, typename B> requires (K == 1 || K == 2)
constexpr auto	dedekind::sets::restriction (const Comprehension< 𝔸< std::variant< X, Y >, L, C >, SumMembership< A, B > > &s)
	The restriction of a set of a sum to its k-th summand, \(\iota_k^{-1}(s)\): the forward map of the lattice isomorphism \(\mathrm{Sub}(X + Y) \cong \mathrm{Sub}(X) \times \mathrm{Sub}(Y)\). A pair of sets is no set: the sum itself is the coproduct of its summands in Set, not their product, so it carries no π_k.
template<std::size_t K, typename X, typename Y, typename T2, typename L, typename C, typename A, typename B> requires (K == 1 || K == 2) && requires(const A& a) { restriction<K>(a); }
constexpr auto	dedekind::sets::restriction (const Comprehension< 𝔸< std::pair< std::variant< X, Y >, T2 >, L, C >, ProductMembership< A, B > > &r)
	A relation out of a sum restricted to one summand: \((A + B) \times C \cong A \times C + B \times C\) (distributivity), so \((\iota_k \times \mathrm{id})^{-1}(s \times c) = \iota_k^{-1}(s) \times c\). A relation Either<a, b> ⇸ c that only accepts a is the relation a ⇸ c.
template<std::size_t K, typename X, typename Y, typename L, typename C> requires (K == 1 || K == 2)
constexpr auto	dedekind::sets::restriction (const 𝔸< std::variant< X, Y >, L, C > &)
	\(\iota_K^{-1}\) is a lattice homomorphism (a pullback preserves \(\wedge, \vee, \neg, \bot, \top\)): the restriction reaches through the lattice's nodes to the sums beneath, and the boundaries restrict to the boundaries — the universe of the sum to the universe of the summand (the sum's cardinality class kept: a sound bound, the summand's own is not recorded on a bare universe), Ø to Ø.
template<std::size_t K, typename X, typename Y, typename L> requires (K == 1 || K == 2)
constexpr auto	dedekind::sets::restriction (const Ø< std::variant< X, Y >, L > &)
template<std::size_t K, typename A> requires (K == 1 || K == 2) && requires(const A& a) { restriction<K>(a); }
constexpr auto	dedekind::sets::restriction (const dedekind::category::Not< A > &n)
template<std::size_t K, typename A, typename B> requires (K == 1 || K == 2) && requires(const A& a, const B& b) { restriction<K>(a); restriction<K>(b); }
constexpr auto	dedekind::sets::restriction (const dedekind::category::Meet< A, B > &m)
template<std::size_t K, typename A, typename B> requires (K == 1 || K == 2) && requires(const A& a, const B& b) { restriction<K>(a); restriction<K>(b); }
constexpr auto	dedekind::sets::restriction (const dedekind::category::Join< A, B > &j)
template<typename L>
constexpr L::Ω	in_species (auto v)
	A verdict in the species L: an == that answers in L::Ω passes through, one that answers bool (a sized or structural equality) is lifted to ⊥ / ⊤.
template<dedekind::category::IsLSet S, IsWhereClause< S > P>
constexpr S::logic_species::Ω	dedekind::sets::exists (const S &s, P p)
template<dedekind::category::IsLSet S, IsWhereClause< S > P> requires HasDecidableMembership<S> || dedekind::category::IsBoundaryObject<S>
constexpr S::logic_species::Ω	dedekind::sets::forall (const S &s, P p)
	Bounded \(\forall\) over a decidable S (its χ in 𝔹: the Δ grade, HasDecidableMembership) or a boundary in any species (χ constant). There the identity \(\forall x \in S.\,P \iff (S|P = S)\) holds in L, because for two-valued \(\chi_S\) the internal equality \((\chi_S \wedge \chi_P \Leftrightarrow \chi_S)\) coincides with the implication \(\chi_S \Rightarrow \chi_P\). In a Heyting algebra that is a theorem for every \(\chi_S\); Ω here is a De Morgan chain (#901) whose material implication is not a residuum, so over an L-valued S the bounded \(\forall = \bigwedge (\chi_S \Rightarrow \chi_P)\) needs the chain's residuated implication, which is #980's remainder.
template<IsRingIntegral auto I, typename K> requires std::copyable<K>
constexpr Projection< I >	descent_slot (const BinOp< std::minus<>, Projection< I >, Const< K > > &t)
	The legs of a descent \(\pi_i - c\): the slot it steps on and the step c. Read through these on the descent's own shape, so a body generic in the term names no member of it (Rule 2).
template<IsRingIntegral auto I, typename K> requires std::copyable<K>
constexpr K	descent_step (const BinOp< std::minus<>, Projection< I >, Const< K > > &t)
template<typename T, typename X> requires HasTermValueAt<T, X>
constexpr std::optional< value_at_t< X, T > >	self_arg (const T &t, const X &x)
	A χ argument's value at a point: the term's value, or nullopt for a descent below the carrier's bottom (no point of the universe, so the pulled-back membership is false there).
template<IsRingIntegral auto I, typename T, typename R>
constexpr decltype(auto)	dedekind::sets::term_value (Projection< I > p, const Env< T, R > &e)
	A projection read at an Env is read at its point.
template<typename T, typename... Vs>
constexpr T	point_of (const Vs &... vs)
	A point of T from the terms' values: the scalar, or the pair.
template<typename Term, typename X, std::size_t S>
consteval bool	descends_on ()
	Whether Term is a descent on slot S at points of X: the shape descent names, on that slot, whose carrier is well-founded.
template<typename Node, typename X, std::size_t... Js>
consteval bool	some_measure (std::index_sequence< Js... >)
template<typename K> requires std::copyable<K>
constexpr K	constant_value (const Const< K > &c)
	The value of a constant term, read on its own shape.
template<IsSetObject S, typename Body> requires contains_self_v<Body> && self_descends_v<Body, typename S::Domain> && std::same_as< std::invoke_result_t<const S&, const typename S::Domain&>, bool>
constexpr auto	dedekind::sets::operator& (const S &base, Body body)
	The former that closes a recursion: S & body with a χ in the body is \(\{x \in S \mid body(x)\}\) where χ is that set. Viable only for a structural recursion over a decidable base; general recursion finds no former.
template<std::semiregular T, IsOckhamAlgebra L, IsCardinality C, typename K>
constexpr auto	dedekind::sets::operator& (const 𝔸< T, L, C > &u, const Cmp< Rel::Eq, Projection< 0 >, Const< K > > &c)
	𝔸<T> & (π == v): the singleton {v}, the constant converted into the carrier exactly or the binding raising. Declared beside 𝔸 and the atom, so ADL finds it.
template<std::equality_comparable T, IsOckhamAlgebra L, IsCardinality C>
constexpr T	dedekind::sets::origin (const Comprehension< 𝔸< T, L, C >, Point< T > > &s)
	The pivot of a point, ε of the comonad reading (the counit {x} ↦ x).
template<std::equality_comparable T, IsOckhamAlgebra L1, IsCardinality C1, IsOckhamAlgebra L2, IsCardinality C2>
constexpr bool	dedekind::sets::operator== (const Comprehension< 𝔸< T, L1, C1 >, Point< T > > &a, const Comprehension< 𝔸< T, L2, C2 >, Point< T > > &b)
	Two points are the same set iff their pivots agree, whatever the species each was tagged with.
template<std::equality_comparable T, IsOckhamAlgebra L, IsCardinality C, IsLSet S> requires std::same_as<typename S::logic_species, L> && (!requires { typename S::is_universal_boundary; }) && (!std::same_as<S, Comprehension<𝔸<T, L, C>, Point<T>>>)
constexpr L::Ω	dedekind::sets::operator<= (const Comprehension< 𝔸< T, L, C >, Point< T > > &s, const S &other)
	{pivot} ⊆ S ⟺ pivot ∈ S, in the shared species L (the universal set keeps its own X ⊆ 𝔸 overload).
template<std::equality_comparable T, IsOckhamAlgebra L, IsCardinality C1, IsOckhamAlgebra L2, IsCardinality C>
constexpr bool	dedekind::sets::operator== (const Comprehension< 𝔸< T, L, C1 >, Point< T > > &, const 𝔸< T, L2, C > &)
	A point is the whole universe only on the unit carrier: {x} == 𝔸<T> iff T has exactly one value (category::One). On every other carrier it is false — the forall leg for the == fragment (𝔸<bool>{} & (π == v) collapses to a Singleton<bool>, and forall asks whether that point is all of 𝔹). Lives here, not in :order, so ADL finds it from sets-level generic code.
template<std::equality_comparable T, IsOckhamAlgebra L, IsCardinality C1, IsOckhamAlgebra L2, IsCardinality C>
constexpr bool	dedekind::sets::operator== (const 𝔸< T, L2, C > &u, const Comprehension< 𝔸< T, L, C1 >, Point< T > > &s)
template<IsOckhamAlgebra L, IsCardinality C>
constexpr auto	dedekind::sets::operator~ (const Comprehension< 𝔸< bool, L, C >, Point< bool > > &s)
	Complement of a point on the two-element carrier is the other point: ~{b} = {!b}. On a larger carrier the complement of a point is not a point, so there is deliberately no overload there and the generic Not node applies. Lives next to Singleton so ADL finds it wherever the type is used.
template<std::equality_comparable T1, IsOckhamAlgebra L1, IsCardinality C1, std::equality_comparable T2, IsOckhamAlgebra L2, IsCardinality C2>
constexpr auto	dedekind::sets::operator* (const Comprehension< 𝔸< T1, L1, C1 >, Point< T1 > > &a, const Comprehension< 𝔸< T2, L2, C2 >, Point< T2 > > &b)
	Product of two points: \(\{a\}\times\{b\}=\{(a,b)\}\), the point of the pair. A structural collapse (the product-side analogue of the complement-pair collapse), so a product of points is equality-comparable, not merely membership-testable: η(a)*η(b) == η(std::pair{a,b}). General products keep the predicate-set form of :expressions cartesian_product.
template<typename A, typename B, typename L, typename C>
constexpr auto	dedekind::sets::component (const Comprehension< 𝔸< std::pair< A, B >, L, C >, Point< std::pair< A, B > > > &s, dedekind::category::At< 1 >)
	The legs of a point of a pair, \(\{(a, b)\} = \{a\} \times \{b\}\): the product of two points collapses to this point, and its projections are the two points again (#970).
template<typename A, typename B, typename L, typename C>
constexpr auto	dedekind::sets::component (const Comprehension< 𝔸< std::pair< A, B >, L, C >, Point< std::pair< A, B > > > &s, dedekind::category::At< 2 >)
template<IsOckhamAlgebra L = Boole, typename T>
constexpr auto	dedekind::sets::singleton (T value)
	singleton: \(T \to \mathrm{Singleton}\langle T\rangle\) — the power-set monad's unit \(\eta\) (see the section note).
template<typename T>
constexpr auto	dedekind::sets::η (T value)
	η — the idiomatic spelling of singleton: the power-set monad's unit \(\eta : x \mapsto \{x\}\). The name matches the categorical unit dedekind::category::η (the tag-dispatched η / pure of :monad, §above) and the grammar's η generator (paper Listing~2). \(\eta(x)\) is the least set containing x, so \(\eta(x) \in \mathfrak{P}(S) \iff x \in S\). The monad's μ (union-flatten) and full functor are #691; the enumerated power set is #840; the Sub(C) subobject lattice 𝔓 is order:powerset (#830) — three distinct reifications of the power object, all sharing this unit.
template<typename T>
constexpr auto	dedekind::sets::ι (T value)
	ι — the singleton read as an inclusion (a mono), the other categorical hat of the same map η / singleton names. Where η is the power-set monad's unit, ι is the injection of each point as its singleton subobject, \(\iota : T \rightarrowtail \mathcal{P}(T)\), \(x \mapsto \{x\}\) — the atoms of the power-set Boolean algebra, and injective (mathematically a mono). It follows the iota-for-inclusion convention it shares with the coproduct injections ι_1 / ι_2 (:cartesian) and the Galois inclusion ι of the ceiling/floor adjunctions ⌈·⌉ ⊣ ι ⊣ ⌊·⌋ (:adjunction). Same underlying map as η; the name picks out the subobject-inclusion reading.
template<std::equality_comparable T, IsOckhamAlgebra L, IsCardinality C, dedekind::category::IsArrow Func> requires std::same_as<dedekind::category::Dom<Func>, T> && IsSetObject<dedekind::category::Cod<Func>>
constexpr auto	dedekind::sets::operator>>= (const Comprehension< 𝔸< T, L, C >, Point< T > > &s, const Func &f)
	The Bricks of the Singleton Monad.
template<std::equality_comparable T, IsOckhamAlgebra L, IsCardinality C, dedekind::category::IsArrow Func> requires std::same_as<dedekind::category::Dom<Func>, Comprehension<𝔸<T, L, C>, Point<T>>>
constexpr auto	dedekind::sets::operator<<= (const Comprehension< 𝔸< T, L, C >, Point< T > > &s, const Func &f)
	Co-Kleisli extend on a point, {x} <<= f = {f({x})}.
template<IsOckhamAlgebra L, IsCardinality C, IsArrow F>
constexpr auto	dedekind::sets::image (F &&f, const Comprehension< 𝔸< Dom< std::remove_cvref_t< F > >, L, C >, Point< Dom< std::remove_cvref_t< F > > > > &s)
	Image of a Singleton under an IsArrow.
template<IsOckhamAlgebra L, typename T, IsCardinality C, typename F> requires IsTerminalMorphism<std::remove_cvref_t<F>> && std::same_as<Dom<std::remove_cvref_t<F>>, T>
constexpr auto	dedekind::sets::image (F &&, const 𝔸< T, L, C > &)
	Terminal-codomain-arrow collapse for image(F, S): when F is an IsTerminalMorphism (F: T → One), the image is structurally degenerate.
template<typename L, typename T, typename F> requires dedekind::category::IsTerminalMorphism<std::remove_cvref_t<F>> && std::same_as<dedekind::category::Dom<std::remove_cvref_t<F>>, T>
constexpr auto	dedekind::sets::image (F &&, const Ø< T, L > &)
template<Rel R, typename X, typename Y>
constexpr bool	dedekind::sets::rel_apply (const X &x, const Y &y)
	x R y.
constexpr Rel	dedekind::sets::negate (Rel r)
	The De Morgan dual of a comparison: !(x R y) is x negate(R) y.
template<typename X>
constexpr auto	dedekind::sets::term_of (X x)
	A term as itself, a constant as Const.
template<typename Op, typename A, typename B>
constexpr auto	make_binop (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator+ (A a, B b)
	The arithmetic of terms.
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator- (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator* (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator/ (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator% (A a, B b)
template<typename F, typename A> requires IsArrow<std::remove_cvref_t<F>> && IsTerm<A>
constexpr Ap< std::remove_cvref_t< F >, A >	dedekind::sets::ap (F f, A a)
	ap(f, a): the arrow f applied to the term a.
template<typename P, typename A, typename B> requires IsRelPredicate<P> && TermOperands<A, B>
constexpr auto	dedekind::sets::cond (P p, A a, B b)
	cond(p, a, b): a where p holds, else b.
constexpr bool	dedekind::sets::only_slot (unsigned mask, unsigned slot)
	Whether a mask names at most the given slot.
template<std::integral T, std::floating_point F>
constexpr bool	in_integer_range (F x)
template<typename C, typename K>
constexpr C	dedekind::sets::carrier_cast (const K &k)
	A constant converted into the carrier C it meets: exactly, or not at all. Between built-in types: in range, then a round trip that keeps the sign. A carrier with its own rule states it beside its definition as carrier_cast(std::type_identity<C>, k), found by ADL (ℕ refuses a negative constant); any other class carrier converts by its constructor.
template<IsRingIntegral auto I, typename P>
constexpr decltype(auto)	dedekind::sets::term_value (Projection< I >, const P &p)
	A projection read at a point: its coordinate, or the point itself for the unary π. An overload for another kind of point (an environment) is found by ADL.
template<typename A, typename B, typename RA, typename RB>
constexpr auto	meet_type ()
	The carrier two operands meet in: a constant takes the other's, two terms their common type.
template<typename V, typename T, typename R>
constexpr V	into (const R &x)
	The value x of the operand T placed in the carrier V: a constant exactly or not at all (carrier_cast), a term's value by conversion.
template<typename Op, typename C> requires requires { typename Op::is_transparent; }
constexpr auto	apply_at (const C &a, const C &b)
	The transparent operator Op applied at the carrier C, as the typed std::plus<C> would apply it: an arithmetic result is converted back to C, so a narrow carrier wraps instead of promoting, and a comparison keeps its bool. No type constructor is taken as an argument.
template<typename C, typename Key>
constexpr bool	dedekind::sets::admits (On< C >, Key, bool)
	No rule: not admitted.
template<typename C> requires IsCommutativeMonoid<C, std::plus<C>>
constexpr bool	dedekind::sets::admits (On< C >, std::plus<>, bool)
	+ - * where the carrier's certified laws have the symbol: + on a commutative monoid, - on an abelian group (a - b is a + (-b)), * on a monoid. A magma is total and closed, so the Pst total operator surface is inside the laws; ℕ's monus is not, until its variety is named.
template<typename C> requires IsAbelianGroup<C, std::plus<C>> && IsClosedUnder<C, std::minus<>>
constexpr bool	dedekind::sets::admits (On< C >, std::minus<>, bool)
template<typename C> requires IsMonoid<C, std::multiplies<C>>
constexpr bool	dedekind::sets::admits (On< C >, std::multiplies<>, bool)
template<typename C>
constexpr bool	dedekind::sets::admits (On< C > c, std::divides<>, bool divisor_is_constant)
	The carrier's own division, by a nonzero constant: a field's or the Euclidean one, whichever rule the carrier has.
template<std::equality_comparable C>
constexpr bool	dedekind::sets::admits (On< C >, std::equal_to<>, bool)
	== and != where the carrier compares.
template<std::equality_comparable C>
constexpr bool	dedekind::sets::admits (On< C >, std::not_equal_to<>, bool)
constexpr const char *	dedekind::sets::spelling (Arith op)
	The spelling of an operator, for a refusal.
template<typename P>
constexpr std::size_t	dedekind::sets::slot_sort (unsigned slot, const P &rep=P{})
	The sort of the slot slot at points of P, an index into point_sorts_t.
template<typename P>
constexpr std::size_t	dedekind::sets::one_sort (const P &rep=P{})
	The points' one sort, where every slot has the same; no_sort on a product of several.
template<typename P>
constexpr std::size_t	dedekind::sets::default_sort (std::size_t s, const P &rep=P{})
	The sort of a tree of constants without a context: the points' one sort where they have one.
template<typename P, std::size_t I = 0, typename F>
constexpr auto	dedekind::sets::with_sort (std::size_t s, const F &f)
	Apply f to the sort s of P as a type: f(type_identity<C>). s is a valid index (the caller joined the sorts).
template<typename C, typename D> requires EmbedsInto<D, C>
constexpr C	dedekind::sets::embed_into (const D &d)
	d read in the sort C.
template<typename C, typename D>
constexpr C	read_as (const D &d)
	d read in the sort C where it embeds, refused elsewhere.
template<typename C, typename P>
constexpr C	coordinate_as (unsigned slot, const P &p)
template<typename C>
constexpr bool	op_admitted (Arith op, bool divisor_is_constant)
	Whether op is admitted on the carrier C, with the divisor a constant (nonzero, checked when the term was built) or a term: the rules above and beside their certificates, read at run time.
template<typename C>
constexpr bool	dedekind::sets::rel_admitted (Rel r)
	Whether the comparison r is admitted on C: == and != where it compares, the order comparisons where the order's rule is in force (order:poset).
template<typename C>
constexpr C	apply_op (Arith op, const C &x, const C &y)
	x op y in the carrier C, for an admitted operator, through the typed functor; a branch whose expression the carrier has not is not instantiated (the typed functor's body would be, so the guard asks the expression).
template<typename C>
constexpr bool	dedekind::sets::compare_rel (Rel r, const C &x, const C &y)
	x r y for a comparison known at run time, admitted when the term was bound; the branches a carrier has not are not instantiated.
template<typename P, std::size_t I = 0, typename K>
constexpr std::size_t	dedekind::sets::constant_sort (const K &k)
	The sort a constant names by itself, at points of P: the first sort C with constant_of(type_identity<C>, k) (found by ADL) true, for a constant written as a value of C (a bool, a Ternary) rather than a numeral; no_sort otherwise, a numeral taking its context's sort.
template<typename P>
constexpr std::size_t	dedekind::sets::join_sorts (std::size_t a, std::size_t b)
	The common sort of two operands at points of P: a constant takes the other's, and a truth chain meets its dominance in the larger (𝔹 and K₃ in K₃).
template<typename P>
constexpr bool	dedekind::sets::sort_embeds (std::size_t from, std::size_t into)
	Whether a value of the sort from is read in the sort into at points of P (EmbedsInto): the same sort, or along the dominance.
template<std::size_t I, typename... Cs>
constexpr std::variant< Cs... >	default_cell (std::size_t sort)
	A cell of the sort sort, its carrier's default value: a row built from a schema is a representative of its points.
template<typename... Cs>
constexpr Row< Cs... >	dedekind::sets::with_bound (const Row< Cs... > &rep, std::size_t sort)
	The row rep extended by a column of the sort sort: the point a quantifier's body is read at. Any other point has no column to bind.
template<typename P>
constexpr P	dedekind::sets::with_bound (const P &, std::size_t)
template<typename C, typename... Cs>
constexpr void	dedekind::sets::set_bound (Row< Cs... > &row, const C &v)
	The last cell of row set to v, of the sort C: the bound column's value under a quantifier.
template<typename C, typename P>
constexpr void	dedekind::sets::set_bound (P &, const C &)
template<typename C>
constexpr C	dedekind::sets::search_value (std::uint64_t i)
	The i-th value of a carrier for a bounded search: a finite chain cycles through its values from ⊥, an unsigned word counts up, and any other carrier states its enumeration as nth_value(type_identity<C>, i), found by ADL beside its definition (Modular: 0, 1, −1, 2, −2, …).
template<typename... Cs>
constexpr Row< Cs... >	dedekind::sets::row_of_sorts (const std::vector< std::size_t > &sorts)
	The row whose columns have the sorts sorts: a representative of the points of that schema, for binding and normal forms.
template<typename P, typename C, typename K>
constexpr C	dedekind::sets::constant_as (const K &k)
template<typename P, typename K>
constexpr std::size_t	dedekind::sets::sort_of (const Term< K > &t, const P &rep=P{})
	The sort of a term built at run time at points of P, from its projections and its constants of a sort (constant_sort): no_sort for a tree of numerals, which takes its context's. Defined with Term.
template<typename P, typename K>
constexpr dedekind::category::Ternary	dedekind::sets::verdict (const Pred< K > &t, const P &point, std::uint64_t budget=std::uint64_t{1}<< 16)
	The verdict of a predicate at a point, in K₃: a comparison or a quantifier over a finite chain is decided (⊤ or ⊥); a quantifier over an infinite carrier searches its first budget values (search_value): a witness of ∃ is ⊤, a counterexample to ∀ is ⊥, and an exhausted budget is U, never the other verdict (Σ, respectively Π: the run-time reading of Semidecided). Same-kind quantifiers over infinite carriers nested below (a middle object of several columns) share the budget, b values each with b^k ≤ budget; an opposite quantifier over an infinite carrier inside answers U. The connectives are Kleene's.
constexpr bool	power_within (std::uint64_t b, unsigned k, std::uint64_t n)
	Whether b^k ≤ n, without overflow.
constexpr std::uint64_t	root_within (std::uint64_t n, unsigned k)
	The largest b with b^k ≤ n (n ≥ 1): the values each of k nested searches may try within a budget of n, found by bisection, logarithmic in n.
template<typename T, typename P>
constexpr auto	dedekind::sets::term_value (const T &t, const P &p)
	The value of a term or predicate at a point.
template<typename C, typename K, typename P>
constexpr C	dedekind::sets::term_value_as (const Term< K > &t, const P &p)
	A term built at run time read in the sort C its context names (the other side of a graph atom, say), at the point p.
template<Rel R, typename A, typename B>
constexpr auto	make_cmp (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator== (A a, B b)
	The comparisons of terms. The term operand is tested first, so a candidate never asks a carrier for its own equality.
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator!= (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator< (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator<= (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator> (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator>= (A a, B b)
template<IsRelPredicate A, IsRelPredicate B>
constexpr RelAnd< A, B >	dedekind::sets::structured_and (A a, B b)
	The meet and join of two relational predicates under the reducer's customization-point names, so the set-level & / | on two relations over one product collapse to one comprehension.
template<IsRelPredicate A, IsRelPredicate B>
constexpr RelOr< A, B >	dedekind::sets::structured_or (A a, B b)
template<Rel R, typename A, typename B>
constexpr Cmp< negate(R), A, B >	dedekind::sets::operator! (const Cmp< R, A, B > &c)
	!atom flips the comparison.
template<typename A, typename B>
constexpr auto	dedekind::sets::operator! (const RelAnd< A, B > &p)
	De Morgan on the connectives: !(p && q) is !p || !q, and dually.
template<typename A, typename B>
constexpr auto	dedekind::sets::operator! (const RelOr< A, B > &p)
template<typename X, typename T>
constexpr void	dedekind::sets::bind_check (const T &t, const X &rep=X{})
	Bind a term or atom to the points X it is evaluated at: every constant meets the carrier of the term beside it now, so a constant the carrier cannot hold raises at construction, not at the first evaluation (a compile error in constexpr code).
template<typename K>
constexpr bool	dedekind::sets::has_quantifier (const Pred< K > &p)
	Whether a predicate has a quantifier anywhere, a conditional's guard in a comparison's operands included.
template<typename K>
constexpr bool	has_quantifier (const Term< K > &t)
	Whether a term has a quantifier in a conditional's guard.
template<typename K>
constexpr unsigned	dedekind::sets::slots (const Term< K > &t)
	The slots a term built at run time mentions, as a mask: the run-time twin of slots_v, read with the same only_slot.
template<typename K>
constexpr unsigned	dedekind::sets::slots (const Pred< K > &p)
template<typename P, typename K, typename Lift>
constexpr Pred< K >	dedekind::sets::pin_constants (const Pred< K > &p, const Lift &lift, const P &rep)
	The predicate with every numeral pinned to the sort its context gives it at points of P: the constant then names its sort itself, so the term keeps its meaning when it moves (substituted into another context by ap, or split by lift_conditionals into an atom with no slot left).
template<typename P, typename K, typename Lift>
constexpr Term< K >	pin_term (const Term< K > &t, std::size_t s, const Lift &lift, const P &rep)
	The term t, of the sort s at points of P, with every numeral pinned to it.
template<typename K>
constexpr std::optional< Definition< K > >	dedekind::sets::defining_term (const Pred< K > &p, unsigned slot, bool universal=false)
	The first conjunct of p, leftmost, that defines the slot (the first disjunct, for universal); nothing where none does.
template<typename K>
constexpr std::optional< dedekind::sets::Definition< K > >	defined_through (const dedekind::sets::Pred< K > &q, unsigned slot, bool universal, unsigned bound)
	A definition of the slot found through a block of quantifiers of the same kind (which commute): the defining atom's term, free of the slots those quantifiers bind, and the block with that atom removed.
template<typename P, typename K, typename Lift>
constexpr dedekind::sets::Pred< K >	dedekind::sets::eliminate_quantifiers (const dedekind::sets::Pred< K > &p, const Lift &lift, const P &rep=P{})
	The predicate with every quantifier eliminated that can be, the atoms left as written: innermost first, by substitution where an atom defines the bound column (a conjunct π_h == t under ∃, a disjunct π_h != t under ∀: the fusion law), else by Shannon's expansion over a finite chain (∨ under ∃, ∧ under ∀). A quantifier over an infinite carrier no atom defines is kept, as is one over a chain whose values lift cannot name (NoConstants: by definition only). Read on the predicate as written (pinned, conditionals not lifted): normalising an atom first would turn the defining shape π_h == t into π_h − t == 0.
constexpr bool	dedekind::sets::only_arguments (unsigned mask, unsigned n)
	Whether a mask names only slots among π_1 … π_{n−1}, the arguments of a graph whose result is π_n.
template<typename K>
constexpr const Term< K > *	dedekind::sets::graph_term (const Pred< K > &p, unsigned n=2)
	The term of a graph atom built at run time, π_n == t or t == π_n with t mentioning only π_1 … π_{n−1}; nullptr for any other predicate. The run-time twin of IsGraphAtom: such a relation is functional by its shape, and entire once bound, since binding admits every operator only where it is total on the carrier (or divides by a nonzero constant).
template<typename K>
constexpr bool	dedekind::sets::same_shape (const Term< K > &x, const Term< K > &y)
	The same tree: the same nodes, slots, operators and comparisons, and equal constants. Syntactic, so sound for equality of what two normal forms denote and silent on two different trees.
template<typename K>
constexpr bool	dedekind::sets::same_shape (const Pred< K > &x, const Pred< K > &y)
	The same predicate tree, atom by atom.
template<typename K>
constexpr std::optional< CondSplit< K > >	split_cond (const Term< K > &t)
	The first conditional of t, leftmost, split out; nullopt for a term without one.
template<typename K>
constexpr Pred< K >	dedekind::sets::lift_conditionals (const Pred< K > &p)
	The predicate with every conditional lifted out of its atoms: cond(q, a, b) R c is (q ∧ a R c) ∨ (¬q ∧ b R c), the law of McCarthy's conditional, until no atom has one. The same set at every point; an applied set ap(S, t) == ⊤, the conditional cond(χ_S[π:=t], ⊤, ⊥) compared, becomes χ_S[π:=t] once the decided atoms are folded (algebra:polynomial's canonical).
template<typename K>
constexpr Pred< K >	by_cases (const Pred< K > &q, const Pred< K > &x, const Pred< K > &y)
	(q ∧ x) ∨ (¬q ∧ y), each part lifted.
template<IsGraphAtom P>
constexpr graph_term_t< P >	dedekind::sets::graph_term (const P &p)
	The term of a graph atom, the side that is not π_2.
template<typename A, typename B> requires requires { typename A::Domain; typename B::Domain; } && std::same_as<typename A::Domain, typename B::Domain> && (!IsBoundaryObject<A>) && (!IsBoundaryObject<B>) && IsStepTerm<A> && IsStepTerm<B> && std::same_as<typename A::logic_species, typename B::logic_species>
constexpr auto	operator== (const A &a, const B &b)
	Equality of two set terms of a chain as sets of the carrier, in the species: one traversal of their normal forms, so it is extensional ((0, 3) and [1, 3) are the same set of ℤ).
template<typename P, typename S, IsArrow T>
constexpr Prefixed< P, S, T >	operator& (const Symmetric< P, S, T > &s, const Prefix &p)
template<typename A, typename Pred> requires IsSpecies<A> && std::invocable<std::decay_t<Pred>, const A&> && IsΩ<std::invoke_result_t<std::decay_t<Pred>, const A&>>
constexpr auto	ambient_set (Pred predicate)
	Construct a set object over ambient species A from a characteristic predicate.
template<typename S> requires IsSubobject<std::remove_cvref_t<S>, typename std::remove_cvref_t<S>::Domain>
constexpr SubobjectInclusion< std::remove_cvref_t< S > >	inclusion_arrow (const S &s)
The legs of a node, for @c cata (@c category::f_algebra)
The term functor stated once per node: the sub-terms, by reference. A projection, a constant, and a predicate the grammar does not know are leaves. An arrow applied to a term has one leg, the term (the arrow is a datum of the node).
template<typename Op, typename A, typename B>
constexpr auto	dedekind::sets::legs (const BinOp< Op, A, B > &t)
template<typename F, typename A>
constexpr auto	dedekind::sets::legs (const Ap< F, A > &t)
template<typename P, typename A, typename B>
constexpr auto	dedekind::sets::legs (const CondT< P, A, B > &t)
template<Rel R, typename A, typename B>
constexpr auto	dedekind::sets::legs (const Cmp< R, A, B > &t)
template<typename A, typename B>
constexpr auto	dedekind::sets::legs (const RelAnd< A, B > &t)
template<typename A, typename B>
constexpr auto	dedekind::sets::legs (const RelOr< A, B > &t)

Variables
template<typename T, typename L>
const Ø< T, L >	Ø< T, L >::χ {}
template<typename T, IsOckhamAlgebra L, IsCardinality C>
const 𝔸< T, L, C >	𝔸< T, L, C >::χ {}
constexpr auto	dedekind::sets::ℕ = 𝔸<Cardinality>{}
	The canonical Natural-numbers universe ℕ = 𝔸<Cardinality> (post-#559).
constexpr auto	dedekind::sets::𝔹 = 𝔸<bool>{}
	𝔹 — the canonical Boolean universe 𝔸<bool>{}, the finite set \(\{\mathtt{false},\mathtt{true}\}\). This is the one symbol downstream code refers to (no partition re-exports or re-aliases it); the carrier is bool and is spelled directly in type positions. Companion to ℕ for the point-free set-builder surface 𝔹 | π == true.
constexpr auto	dedekind::sets::U64 = 𝔸<u64, Boole, Finite>{}
	U64 — the universe over the word, 𝔸<u64>{}: finite by representation, the twin of Python's U64 (A(u64)).
constexpr auto	dedekind::sets::lift_ℕ_ℤ_
	Canonical variant-layer embedding ℕ ↪ ℤ: Cardinality → SignedCardinality, exposed as a first-class arrow object for the carrier-lattice diagram.
constexpr auto	dedekind::sets::embed_𝕂3_ℤ_
	Canonical embedding K3 ↪ ℤ: Ternary → SignedCardinality.
constexpr auto	dedekind::sets::abs_
	Arrow form of abs: an exported arrow<SignedCardinality, Cardinality> object. Registered epic (surjective) below: every Cardinality is the image of itself ( abs(lift_ℕ_ℤ_(c)) = c) and of its negation; the map is sign-folding, conflating +n and -n. Companion to the injective lift_ℕ_ℤ_ in numbers:integer — together they exhibit the split-mono pair from the carrier-lattice diagram (Figure 1).
template<typename S>
constexpr bool	is_empty_set_v = false
	Whether S is an empty set by its type (Ø).
template<typename T, typename L>
constexpr bool	is_empty_set_v< Ø< T, L > > = true
template<typename T>
constexpr bool	is_descent_v = descent<T>::value
constexpr ChiTag	dedekind::sets::χ {}
template<typename... Ts>
constexpr bool	is_self_v< Self< Ts... > > = true
template<typename X, std::size_t J>
constexpr std::size_t	slot_at
	The coordinate a position of χ's arguments stands for at points of X: the point itself (slot 0) for a scalar, slot J + 1 of a pair.
template<typename X>
constexpr std::size_t	arity_v
	The number of coordinates of a point of X.
template<typename Term, typename X, std::size_t S>
constexpr bool	descends_on_v = descends_on<Term, X, S>()
template<typename Node, typename T>
constexpr bool	dedekind::sets::self_descends_v
	The structural-recursion gate: one coordinate on which every Self in the body descends. Vacuous without a Self.
constexpr Projection< 1 >	dedekind::sets::𝑥 {}
constexpr Projection< 2 >	dedekind::sets::𝑦 {}
constexpr Projection< 3 >	dedekind::sets::𝑧 {}
template<typename T>
constexpr bool	is_runtime_term_v = false
template<typename K>
constexpr bool	is_runtime_term_v< Term< K > > = true
template<typename T>
constexpr bool	is_term_v = false
template<IsRingIntegral auto I>
constexpr bool	is_term_v< Projection< I > > = true
template<typename K>
constexpr bool	is_term_v< Const< K > > = true
template<typename Op, typename A, typename B>
constexpr bool	is_term_v< BinOp< Op, A, B > > = true
template<typename F, typename A>
constexpr bool	is_term_v< Ap< F, A > > = true
template<typename P, typename A, typename B>
constexpr bool	is_term_v< CondT< P, A, B > > = true
template<typename T>
constexpr unsigned	dedekind::sets::slots_v
	The slots T mentions, through any cv-ref (a constexpr variable's decltype is const).
template<typename T>
constexpr bool	is_const_v = false
template<typename K>
constexpr bool	is_const_v< Const< K > > = true
template<typename P>
constexpr bool	is_row_v = false
template<typename... Cs>
constexpr bool	is_row_v< Row< Cs... > > = true
template<typename C, typename S>
constexpr bool	dedekind::sets::is_sort_of_v = false
	Whether C is one of the sorts S.
template<typename C, typename... Cs>
constexpr bool	is_sort_of_v< C, std::tuple< Cs... > >
constexpr std::size_t	dedekind::sets::no_sort = static_cast<std::size_t>(-1)
	No sort yet: a tree of constants alone, which takes the sort of its context.
template<typename X, typename T>
constexpr bool	dedekind::sets::is_total_term_v
	A term total at every point of type X.
template<typename T>
constexpr bool	dedekind::sets::is_self_v = false
	Whether a leaf is the set under definition, a χ node; :recursion registers it.
template<typename T>
constexpr bool	dedekind::sets::contains_self_v
	Whether T mentions the set under definition.
constexpr Projection< 0 >	π
	The unary projection, the identity: the variable of a comprehension over one carrier.
template<std::size_t K>
constexpr Projection< K >	π_
	The family: π_<k> is the k-th projection of a flat product.
constexpr Projection< 1 >	π_1
	The projections of a pair (and the first three of a tuple).
constexpr Projection< 2 >	π_2
constexpr Projection< 3 >	π_3

Detailed Description

boundaries__Mereology

boundaries__Mereology_2

singleton__Mereology

singleton__Mereology_2

Typedef Documentation

CanonicalIntProductSet

using dedekind::sets::CanonicalIntProductSet

Initial value:

 
    decltype(cartesian_product(std::declval<const CanonicalIntSet&>(),
                               std::declval<const CanonicalIntSet&>()))

Cardinality

using dedekind::sets::Cardinality = std::variant<ExtensionalCardinal<>, ℵ_0>

export

Sum type for finite vs countably infinite cardinalities; the library's bona-fide proxy for \(\mathbb{N}\) modulo physical limits.

The variant (ExtensionalCardinal<>, ℵ_0) is not a cyclic carrier (it does not wrap modulo capacity); on overflow it escalates — saturates — into ℵ_0 via the add / mul helpers below. The explicit overflow story is "you reached countable infinity" rather than the C++ default of silent wrap or UB. The finite fragment is ExtensionalCardinal<>, one std::size_t word (so the variant is not a bignum). The ℵ_0 alternative marks the saturation regime that takes over once the word cannot hold the result.

Strictly mathematically, \(\mathbb{N} \cup \{\aleph_0\}\) is not a monoid in the textbook sense (e.g. left-cancellation fails on the saturating element). The library's pragmatic certificate accepts it as a proxy for \(\mathbb{N}\) because the finite fragment is \(\mathbb{N}\) exactly and the saturation is the explicit overflow contract: "if you compute beyond memory limits, you saturate at @c ℵ_0". Downstream code that requires strict-ℕ behaviour should test the finite-fragment alternative (std::holds_alternative<ExtensionalCardinal<>>). See the sibling SignedCardinality below for the ℤ proxy on the same pattern.

comprehension_logic_t

template<typename Base, typename Predicate>

using dedekind::sets::comprehension_logic_t

Initial value:

 
    join_logic_t<typename Base::logic_species,
                 typename answer_logic<
                     typename Base::logic_species,
                     std::invoke_result_t<const Predicate&,
                                          const typename Base::Domain&>>::type>

The logic species of {base | pred}: the join (in the species semilattice, category::join_logic_t) of the base's species and the species of the predicate's answer, so a Kleene predicate over a Boole base lifts the base rather than truncating itself, and a Kleene predicate over a Percent base answers in Percent. A pair with no join (a K₃ answer over a Chain<int> base) is refused here.

default_cardinality_t

template<typename T>

using dedekind::sets::default_cardinality_t = typename default_cardinality<T>::type

export

The cardinality class a carrier declares by its representation: Finite for bool, ℵ_0 otherwise. This is the default of 𝔸's third parameter, so 𝔸<bool> is classified Finite and its cardinality metadata is honest (the species is Boole regardless).

Template Parameters

T	the carrier.

graph_term_t

template<IsGraphAtom P>

using dedekind::sets::graph_term_t = typename graph_atom<P>::term

export

The term of a graph atom.

Template Parameters

P

the atom.

leg_1_t

template<typename D>

using dedekind::sets::leg_1_t

export

Initial value:

 std::remove_cvref_t<decltype(dedekind::category::π_1(
    std::declval<const D&>()))>

The legs of a product carrier: the types π_1 and π_2 return.

Template Parameters

D	the carrier.

leg_2_t

template<typename D>

using dedekind::sets::leg_2_t

export

Initial value:

 std::remove_cvref_t<decltype(dedekind::category::π_2(
    std::declval<const D&>()))>

ProductMembership

template<typename A, typename B>

using dedekind::sets::ProductMembership

export

Initial value:

 dedekind::category::Meet<
    dedekind::category::Compose<
        dedekind::category::Π<
            1, std::pair<typename A::Domain, typename B::Domain>>,
        A>,
    dedekind::category::Compose<
        dedekind::category::Π<
            2, std::pair<typename A::Domain, typename B::Domain>>,
        B>>

Membership of a cartesian product: \((x, y) \in A \times B \iff x \in A \wedge y \in B\), the meet of the two cylinders \(\chi_A \circ \pi_1\) and \(\chi_B \circ \pi_2\). So \(\chi_{A \times B} = \wedge \circ (\chi_A \times \chi_B)\) and \(A \times B = (A \times Y) \cap (X \times B)\): no predicate of its own, the library's meet (in the join of the factors' species, each answer lifted) over its projections composed with the factors.

SignedCardinality

using dedekind::sets::SignedCardinality

export

Initial value:

 
    std::variant<SignedExtensionalCardinal<>, PositiveInfinity,
                 NegativeInfinity, NaZ>

Signed counterpart of Cardinality with ±ℵ_0 escalation; the library's bona-fide proxy for \(\mathbb{Z}\) modulo physical limits.

Variant of (SignedExtensionalCardinal<>, +ℵ_0, −ℵ_0, NaZ). The finite alternative is the default-constructed first slot, so SignedCardinality{} is canonical zero.

Same picture as Cardinality (the ℕ proxy), with a sign added:

• Not cyclic — arithmetic does not wrap modulo capacity.
• On signed overflow, escalates (saturates) into ±ℵ_0 according to the sign of the operands.
• Indeterminate forms (+ℵ_0 + (−ℵ_0), 0 * ±ℵ_0, ±ℵ_0 / ±ℵ_0, x / 0) propagate the NaZ sentinel IEEE-NaN-style rather than throwing, keeping the carrier usable in constexpr / NTTP-shaped contexts that cannot observe exceptions.
• The finite fragment SignedExtensionalCardinal<> is one two's-complement word (so the variant is not a bignum). The explicit overflow story is escalation to \(\pm \aleph_0\), not bigint growth: signed-overflow UB and silent wrap are replaced by the saturation behaviour.

Strictly mathematically, \(\mathbb{Z} \cup \{\pm \aleph_0, \mathit{NaZ}\}\) is not a group in the textbook sense (+ℵ_0 + (−ℵ_0) = NaZ breaks the inverse law for the saturating elements). The library's pragmatic certificate accepts it as a proxy for \(\mathbb{Z}\) because the finite fragment is \(\mathbb{Z}\) exactly and the saturation / NaZ behaviour is the explicit overflow contract: "if you compute beyond memory limits, you saturate at @c ±ℵ_0; if you compute an indeterminate form, you get @c NaZ". Downstream code that requires strict-ℤ behaviour should test the finite-fragment alternative (std::holds_alternative<SignedExtensionalCardinal<>>).

Same shape as how unsigned int's IsRing claim is "modulo wrap" rather than literal \(\mathbb{Z}\) — the project's stance is that the truthful name for the carrier includes the overflow / saturation behaviour, and the trait registry pins what the carrier actually does at the limits.

Singleton

template<std::equality_comparable T, IsOckhamAlgebra L = Boole>

using dedekind::sets::Singleton = Comprehension<𝔸<T, L>, Point<T>>

export

\(\{x\}\) as a set: the equality atom over the universe of T. An alias, not a noun: its operators are every comprehension's (the reducer's nodes); what is specific to a point follows as free functions.

Template Parameters

T	the carrier.
L	the species the membership answer is valued in.

subobject_reduce_t

template<typename Term, typename L = Boole, typename Combine = no_leaf_combine>

using dedekind::sets::subobject_reduce_t

export

Initial value:

 
    reduce_t<Term, subobject_order<L>, subobject_order<L>, Combine>

The lattice-law term reducer localised to the subobject lattice Sub(T): normalise Term under subobject_order<L> as both the semantic order (Ord, boundedness / distributivity) and the canonicalisation order (Less). The set-level meet and join routes fold through this one alias (the boundary operators below, and the free operator& / operator| over IsSubobject in :expressions), so the injected-order policy for Sub(T) is named in a single place (#865/#890, Phase 2). Complement does not route here: the free operator! in :expressions is a certified involution that eliminates double negation via the :involution witness (!!A ≡ A).

term_sorts_t

template<typename P>

using dedekind::sets::term_sorts_t

export

Initial value:

 
    typename with_carrier<typename with_carrier<point_sorts_t<P>, bool>::type,
                          dedekind::category::Ternary>::type

The sorts a term at points of P takes: the points' carriers first (a slot's sort is its index there), then the truth chains a set applied to a term lands in, ap(S, t) of sort S's codomain.

Template Parameters

P	the point type.

universe_t

template<IsSetObject S>

using dedekind::sets::universe_t

export

Initial value:

 
    std::remove_cvref_t<decltype(universe(std::declval<const S&>()))>

The type of a set object's universe leg.

value_at_t

template<typename X, typename T>

using dedekind::sets::value_at_t

export

Initial value:

 std::remove_cvref_t<decltype(term_value(
    std::declval<const T&>(), std::declval<const X&>()))>

The value type a term takes at a point of type X.

Function Documentation

η()

template<typename T>

auto dedekind::sets::η ( T value )

constexprexport

η — the idiomatic spelling of singleton: the power-set monad's unit \(\eta : x \mapsto \{x\}\). The name matches the categorical unit dedekind::category::η (the tag-dispatched η / pure of :monad, §above) and the grammar's η generator (paper Listing~2). \(\eta(x)\) is the least set containing x, so \(\eta(x) \in \mathfrak{P}(S) \iff x \in S\). The monad's μ (union-flatten) and full functor are #691; the enumerated power set is #840; the Sub(C) subobject lattice 𝔓 is order:powerset (#830) — three distinct reifications of the power object, all sharing this unit.

Template Parameters

T	the pivot's type.

ι()

template<typename T>

auto dedekind::sets::ι ( T value )

constexprexport

ι — the singleton read as an inclusion (a mono), the other categorical hat of the same map η / singleton names. Where η is the power-set monad's unit, ι is the injection of each point as its singleton subobject, \(\iota : T \rightarrowtail \mathcal{P}(T)\), \(x \mapsto \{x\}\) — the atoms of the power-set Boolean algebra, and injective (mathematically a mono). It follows the iota-for-inclusion convention it shares with the coproduct injections ι_1 / ι_2 (:cartesian) and the Galois inclusion ι of the ceiling/floor adjunctions ⌈·⌉ ⊣ ι ⊣ ⌊·⌋ (:adjunction). Same underlying map as η; the name picks out the subobject-inclusion reading.

Note

This is mathematical motivation, not a concept claim: ι(x) returns a point set (its callable is the membership classifier \(T \to \Omega\)), not a reified arrow carrying an IsMonicArrow monicity witness (:morphism). Reifying/certifying the unit arrow is a separate step.

Template Parameters

T	the pivot's type.

abs()

Cardinality dedekind::sets::abs ( const SignedCardinality & z )

constexprexportnoexcept

Retraction direction: abs : ℤ → ℕ. The math- honest signature for absolute value: every element of SignedCardinality has a non-negative magnitude, so the result type is Cardinality (not SignedCardinality), announcing the non-negativity guarantee at the type level.

Categorically, abs is a retraction (left inverse) of the canonical embedding embed_uint_sint_ on the non-negative fragment of ℤ — i.e., abs ∘ embed_uint_sint_ = id_ℕ — extended by sign- folding on the negative fragment. This is the downward complement of the closure-forcing -Cardinality direction above: where unary - widens ℕ → ℤ along the Grothendieck embedding, abs narrows ℤ → ℕ along the same embedding's retraction. Closes #436.

Sentinel handling:

• finite_signed_cardinality(n) (any sign) → finite Cardinality with magnitude |n|.
• PositiveInfinity → ℵ_0 (the bound on the magnitude escalates to ℵ_0).
• NegativeInfinity → ℵ_0 (sign is folded; magnitude escalates).
• NaZ → ℵ_0 by analogy with the IEEE-NaN-style propagation that #396 chose for the saturating semantics; NaZ has no well-defined magnitude, but the saturated answer is the conservative bound.

cardinality__Relationship_to_std_abs

Conceptually the same operation as std::abs at a different carrier layer, with two load-bearing differences:

1. Type-honest codomain. The natural categorical signature for absolute value is int → unsigned (the image is exactly the non-negative ints, which canonically embed into unsigned). C++'s std::abs(int) → int is type- dishonest about this: the result is always non-negative but the return type doesn't say so, and the caller has to know. This abs's variant-layer signature SignedCardinality → Cardinality (i.e. ℤ → ℕ) is the honest version of the same operation: the type announces non-negativity. In other words, the variant abs is to the (type-honest) int → unsigned absolute value what lift_ℕ_ℤ_ is to the unsigned-to- signed widening — both honour at the variant layer what the machine layer signs implicitly.

2. Total. std::abs(int) has undefined behaviour at INT_MIN (since -INT_MIN overflows the signed range). The variant carrier SignedCardinality has no such pathology — the magnitude of the most-negative finite value is representable as a non-negative Cardinality, and the saturating ±ℵ_0 / NaZ cases extend the operation totally.

The commuting square (std::abs vs this abs across the machine ↔ variant lifts, with the post-std::abs side coerced to unsigned to make the codomain match) holds on the non-INT_MIN fragment of int and is partial at INT_MIN — std::abs(INT_MIN) is UB, while abs(embed_sint_ℤ_(INT_MIN)) is a finite Cardinality with magnitude |INT_MIN| (computable via the unsigned-modular expression 0u - static_cast<unsigned>(INT_MIN) — well- defined for any int width per std::numeric_limits<int>::digits, no 32-bit ABI assumption). This is the same Honest-Rejection / saturating-extension pattern the project runs for int / unsigned vs the variant carriers.

See also

std::abs (machine-layer counterpart; type-dishonest int → int signature; partial under UB at INT_MIN).

lift_ℕ_ℤ_ in numbers:integer (the injective half of the split-mono Figure 1 pair).

admits() [1/4]

template<typename C>

bool dedekind::sets::admits ( On< C > c, std::divides<> , bool divisor_is_constant )

constexprexport

The carrier's own division, by a nonzero constant: a field's or the Euclidean one, whichever rule the carrier has.

Template Parameters

C	the carrier.

admits() [2/4]

template<typename C, typename Key>

bool dedekind::sets::admits ( On< C > , Key , bool  )

constexprexport

No rule: not admitted.

Template Parameters

C	the carrier.
Key	the operator.

admits() [3/4]

template<std::equality_comparable C>

bool dedekind::sets::admits ( On< C > , std::equal_to<> , bool  )

constexprexport

== and != where the carrier compares.

Template Parameters

C	the carrier.

admits() [4/4]

template<typename C>
requires IsCommutativeMonoid<C, std::plus<C>>

bool dedekind::sets::admits ( On< C > , std::plus<> , bool  )

constexprexport

+ - * where the carrier's certified laws have the symbol: + on a commutative monoid, - on an abelian group (a - b is a + (-b)), * on a monoid. A magma is total and closed, so the Pst total operator surface is inside the laws; ℕ's monus is not, until its variety is named.

Template Parameters

C	the carrier.

ap()

template<typename F, typename A>
requires IsArrow<std::remove_cvref_t<F>> && IsTerm<A>

Ap< std::remove_cvref_t< F >, A > dedekind::sets::ap ( F f, A a )

constexprexport

ap(f, a): the arrow f applied to the term a.

Template Parameters

F	the arrow.
A	the term.

apply_at()

template<typename Op, typename C>
requires requires { typename Op::is_transparent; }

auto dedekind::sets::apply_at ( const C & a, const C & b )

constexpr

The transparent operator Op applied at the carrier C, as the typed std::plus<C> would apply it: an arithmetic result is converted back to C, so a narrow carrier wraps instead of promoting, and a comparison keeps its bool. No type constructor is taken as an argument.

Template Parameters

Op	the transparent operator.
C	the carrier.

as_pullback()

template<typename A, typename B>
requires IsSetObject<Meet<A, B>> && IsSubobject<A, typename A::Domain> && IsSubobject<B, typename B::Domain>

auto dedekind::sets::as_pullback ( const Meet< A, B > & m )

constexprexport

The pullback apex of an applied meet: the same set, viewed with the subobject surface and the projection legs π_1 / π_2 (IsPullback), category's view over the node.

Parameters

m

the meet.

Returns

its apex.

as_pushout()

template<typename A, typename B>
requires IsSetObject<Join<A, B>> && IsSubobject<A, typename A::Domain> && IsSubobject<B, typename B::Domain>

auto dedekind::sets::as_pushout ( const Join< A, B > & j )

constexprexport

The pushout apex of an applied join, dual to as_pullback.

Parameters

j

the join.

Returns

its apex.

bind_check()

template<typename X, typename T>

void dedekind::sets::bind_check ( const T & t, const X & rep = X{} )

constexprexport

Bind a term or atom to the points X it is evaluated at: every constant meets the carrier of the term beside it now, so a constant the carrier cannot hold raises at construction, not at the first evaluation (a compile error in constexpr code).

Template Parameters

X	the point type.
T	the term.

bound_join()

template<typename S1, typename S2>

std::size_t dedekind::sets::bound_join ( const S1 & lhs, const S2 & rhs )

constexprexport

ETCS-aligned upper bound for join/union cardinality.

For extensional sets with explicit upper_bound(), this is the saturating sum bound(A) + bound(B). For intensional/transfinite species, the function returns the maximal finite sentinel.

by_cases()

template<typename K>

Pred< K > dedekind::sets::by_cases ( const Pred< K > & q, const Pred< K > & x, const Pred< K > & y )

constexpr

(q ∧ x) ∨ (¬q ∧ y), each part lifted.

Parameters

q	the condition.
x	where it holds.
y	where it fails.

carrier_cast() [1/2]

template<typename C, typename K>

C dedekind::sets::carrier_cast ( const K & k )

constexprexport

A constant converted into the carrier C it meets: exactly, or not at all. Between built-in types: in range, then a round trip that keeps the sign. A carrier with its own rule states it beside its definition as carrier_cast(std::type_identity<C>, k), found by ADL (ℕ refuses a negative constant); any other class carrier converts by its constructor.

Template Parameters

C	the carrier.
K	the constant's type.

Parameters

k	the constant.

carrier_cast() [2/2]

template<std::integral K>

Cardinality dedekind::sets::carrier_cast ( std::type_identity< Cardinality > , K k )

constexprexport

An integer constant meeting ℕ or ℤ, the hook the term grammar's carrier_cast reaches by ADL: exactly, or a domain error for a negative constant meeting ℕ.

Template Parameters

K	the constant's type.

Parameters

k	the constant.

cartesian_product() [1/2]

template<IsSetObject A, IsSetObject B>

auto dedekind::sets::cartesian_product ( const A & a, const B & b )

constexprexport

Cartesian product over arbitrary set objects.

Normalises each operand to a plain set over its universe and delegates to the plain × plain product, which reconciles the species at their join.

cartesian_product() [2/2]

template<typename T1, typename L1, typename P1, typename T2, typename L2, typename P2, typename C1, typename C2>
requires dedekind::category::HaveLogicJoin< typename Comprehension<𝔸<T1, L1, C1>, P1>::logic_species, typename Comprehension<𝔸<T2, L2, C2>, P2>::logic_species>

auto dedekind::sets::cartesian_product ( const Comprehension< 𝔸< T1, L1, C1 >, P1 > & a, const Comprehension< 𝔸< T2, L2, C2 >, P2 > & b )

constexprexport

Cartesian product of two sets: {(a,b) | a ∈ A, b ∈ B}.

Constructs a comprehension over 𝔸<pair<T1,T2>> whose membership predicate checks element-wise membership in both component sets.

compare()

std::strong_ordering dedekind::sets::compare ( const Cardinality & lhs, const Cardinality & rhs )

constexprexport

Total comparison over the finite/ℵ_0 fragment.

finite < ℵ_0, and ℵ_0 == ℵ_0.

component() [1/2]

template<typename A, typename B, typename L, typename C>

auto dedekind::sets::component ( const Comprehension< 𝔸< std::pair< A, B >, L, C >, Point< std::pair< A, B > > > & s, dedekind::category::At< 1 >  )

constexprexport

The legs of a point of a pair, \(\{(a, b)\} = \{a\} \times \{b\}\): the product of two points collapses to this point, and its projections are the two points again (#970).

Parameters

s	the point of the pair.

Returns

the point of the first / second coordinate.

component() [2/2]

template<typename T1, typename T2, typename L, typename C, typename A, typename B>

auto dedekind::sets::component ( const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, ProductMembership< A, B > > & s, dedekind::category::At< 1 >  )

constexprexport

The product of two set objects is their categorical product, not only their carriers' (#970, #1039): π_1 / π_2 on A × B return the factor set objects, which the membership already carries. With the carrier-level IsProduct above and the universes' (boundaries), IsProduct<decltype(A * B), A, B> holds for set objects.

Parameters

s	the product.

Returns

the first / second factor.

cond()

template<typename P, typename A, typename B>
requires IsRelPredicate<P> && TermOperands<A, B>

auto dedekind::sets::cond ( P p, A a, B b )

constexprexport

cond(p, a, b): a where p holds, else b.

Template Parameters

P	a relational predicate.
A,B	the branches.

constant_order()

std::weak_ordering dedekind::sets::constant_order ( const SignedCardinality & lhs, const SignedCardinality & rhs )

constexprexportnoexcept

The structural order of signed cardinalities as constants of a term (#884, canonical's sort key): total, unlike <=>. By alternative first (finite, +∞, −∞, then NaZ), a finite value by its order.

Parameters

lhs,rhs

the constants.

constant_sort()

template<typename P, std::size_t I = 0, typename K>

std::size_t dedekind::sets::constant_sort ( const K & k )

constexprexport

The sort a constant names by itself, at points of P: the first sort C with constant_of(type_identity<C>, k) (found by ADL) true, for a constant written as a value of C (a bool, a Ternary) rather than a numeral; no_sort otherwise, a numeral taking its context's sort.

Template Parameters

P	the point type.

Parameters

k	the constant.

constant_value()

template<typename K>
requires std::copyable<K>

K dedekind::sets::constant_value ( const Const< K > & c )

constexpr

The value of a constant term, read on its own shape.

Template Parameters

K	the constant's type.

Parameters

c	the constant.

default_sort()

template<typename P>

std::size_t dedekind::sets::default_sort ( std::size_t s, const P & rep = P{} )

constexprexport

The sort of a tree of constants without a context: the points' one sort where they have one.

Exceptions

not_admitted

on a product of several carriers, where a constant alone names none.

Parameters

rep	a point of P.

defining_term()

template<typename K>

std::optional< Definition< K > > dedekind::sets::defining_term ( const Pred< K > & p, unsigned slot, bool universal = false )

constexprexport

The first conjunct of p, leftmost, that defines the slot (the first disjunct, for universal); nothing where none does.

Parameters

p	the predicate.
slot	the slot.
universal	whether the slot is bound by ∀ rather than ∃.

descent_slot()

template<IsRingIntegral auto I, typename K>
requires std::copyable<K>

Projection< I > dedekind::sets::descent_slot ( const BinOp< std::minus<>, Projection< I >, Const< K > > & t )

constexpr

The legs of a descent \(\pi_i - c\): the slot it steps on and the step c. Read through these on the descent's own shape, so a body generic in the term names no member of it (Rule 2).

Template Parameters

K	the step's type.

Parameters

t	the descent.

elevate_meet()

template<typename T, IsOckhamAlgebra L, typename Reduced>

auto dedekind::sets::elevate_meet ( Reduced reduced )

constexprexport

Value-level elevate of a structured_and result to the meet's normal-form value: an empty reduction is the initial object Ø; a finite reduction (a point) is itself a set-like leaf (returned bare); any other reduction is a named predicate wrapped back into a comprehension. (Extracted verbatim from the pre-reducer operator& structured_and branch so SetCombine's type and this value stay in lockstep.).

expressions__Reducer_Leaf_Combiner

The set meet / join route through the generic lattice-law term reducer (category:lattice_term, #865/#890) under subobject_order<L>. The reducer owns the structural laws (bounded, idempotence, absorption, ...); the domain-specific collapse of two order-incomparable set leaves is the injected leaf-combiner SetCombine. It reduces the structured_and / structured_or of two halfspaces into an interval, say. It reaches :order via ADL (order is downstream of sets, so ADL is the cycle-free customisation point), exactly as the pre-reducer operator& / operator| did.

Template Parameters

T	the carrier.
L	the species.
Reduced	the reducer's result: an EmptyPredicate, a sized leaf, or a named predicate.

eliminate_quantifiers()

template<typename P, typename K, typename Lift>

dedekind::sets::Pred< K > dedekind::sets::eliminate_quantifiers ( const dedekind::sets::Pred< K > & p, const Lift & lift, const P & rep = P{} )

constexprexport

The predicate with every quantifier eliminated that can be, the atoms left as written: innermost first, by substitution where an atom defines the bound column (a conjunct π_h == t under ∃, a disjunct π_h != t under ∀: the fusion law), else by Shannon's expansion over a finite chain (∨ under ∃, ∧ under ∀). A quantifier over an infinite carrier no atom defines is kept, as is one over a chain whose values lift cannot name (NoConstants: by definition only). Read on the predicate as written (pinned, conditionals not lifted): normalising an atom first would turn the defining shape π_h == t into π_h − t == 0.

Template Parameters

P	the point type.

Parameters

p	the predicate.
lift	a value into a constant that names its sort.
rep	a point of P.

embed_into()

template<typename C, typename D>
requires EmbedsInto<D, C>

C dedekind::sets::embed_into ( const D & d )

constexprexport

d read in the sort C.

Template Parameters

C

the sort.

Parameters

d	the value.

ext()

template<typename U, typename Chi>
requires std::ranges::input_range<const U> && std::totally_ordered<std::ranges::range_value_t<const U>> && std::invocable<const Chi&, std::ranges::range_reference_t<const U>> && std::constructible_from< bool, std::invoke_result_t< const Chi&, std::ranges::range_reference_t<const U>>>

auto dedekind::sets::ext ( const U & universe, Chi chi )

constexprexport

μ: Int ⇀ Ext, the partial retraction of ambient_set.

Enumerate a finite, enumerable universe and collect the elements the characteristic predicate chi accepts into a std::set (the container). Total only when the universe is finite/enumerable and χ decidable; the naturals themselves have no finite materialisation. This is why Trsk is strictly more expressive than std::set (the embedding ambient_set is total, this retraction is not), and why the price of staying in the purely intensional regime is discharging membership by proof (concepts, factorisations) rather than by enumeration.

Note

The std::set target additionally requires the value type to be totally ordered; a regular-but-unordered carrier is rejected at the constraint rather than hard-erroring in the body.

filter()

template<typename T, typename Hash, typename Equal, typename Alloc, typename P>
requires std::predicate<const P&, const T&>

auto dedekind::sets::filter ( P p, const std::unordered_set< T, Hash, Equal, Alloc > & s )

constexprexport

filter(p, std::unordered_set<T, Hash, Equal, Alloc>).

Filter is always endomorphic on the element type, so the source's Hash/Equal/Alloc are preserved unconditionally. The predicate is applied as a const value (Rule 1): a predicate that must mutate itself to answer is refused at the constraint.

graph_term() [1/2]

template<IsGraphAtom P>

graph_term_t< P > dedekind::sets::graph_term ( const P & p )

constexprexport

The term of a graph atom, the side that is not π_2.

Parameters

p

the atom.

graph_term() [2/2]

template<typename K>

const Term< K > * dedekind::sets::graph_term ( const Pred< K > & p, unsigned n = 2 )

constexprexport

The term of a graph atom built at run time, π_n == t or t == π_n with t mentioning only π_1 … π_{n−1}; nullptr for any other predicate. The run-time twin of IsGraphAtom: such a relation is functional by its shape, and entire once bound, since binding admits every operator only where it is total on the carrier (or divides by a nonzero constant).

Parameters

p	the predicate.
n	the result slot, the last (2 on a pair).

has_quantifier()

template<typename K>

bool dedekind::sets::has_quantifier ( const Pred< K > & p )

constexprexport

Whether a predicate has a quantifier anywhere, a conditional's guard in a comparison's operands included.

Parameters

p	the predicate.

image() [1/5]

template<IsOckhamAlgebra L, typename T, IsCardinality C, typename F>
requires IsTerminalMorphism<std::remove_cvref_t<F>> && std::same_as<Dom<std::remove_cvref_t<F>>, T>

auto dedekind::sets::image ( F && , const 𝔸< T, L, C > &  )

constexprexport

Terminal-codomain-arrow collapse for image(F, S): when F is an IsTerminalMorphism (F: T → One), the image is structurally degenerate.

(#661)

• image(F, Ø<T, L>) → Ø<One, L> — empty source maps to empty image.
• image(F, 𝔸<T, L, C>) → Singleton<One, L>{One{}} — inhabited source collapses to the singleton on One.
• image(F, a point over T) falls through to the generic image(F, point) above (correct: the point {F(pivot)} = {One{}}).

Predicate-based Comprehension sources fall through to the symbolic-fallback image() in :expressions (inhabitation undecidable in general).

Template Parameters

L	the species.
T	the carrier.
C	the cardinality.
F	the terminal morphism T → 1.

image() [2/5]

template<dedekind::category::IsArrow F, IsSetObject S>
requires std::same_as<dedekind::category::Dom<std::remove_cvref_t<F>>, typename S::Domain>

auto dedekind::sets::image ( F && , const S &  )

constexprexport

image(f, {x ∈ 𝔸 | P}) — image of an intensional set under an arrow. Layer 1 of #602.

Sister overload in the image dispatch table, alongside

• image(f, Singleton) (:sets:singleton; extensional, exact).
• image(f, std::set / std::unordered_set) (:sets:extensional; extensional, exact via enumeration).
• this overload (intensional, symbolic with Kleene).

The result is itself an intensional Set on the codomain U = Cod<F>, with Kleene as the logic species and the always-Unknown SymbolicImagePredicate as the predicate. This honestly admits the indecision — the existential ∃x ∈ T. P(x) ∧ y == f(x) is undecidable on transfinite carriers without further structure (a partial inverse for f, or finiteness of T).

IsArrow<F> is the gate (the project's general arrow concept); IsMonicArrow<F> would be the natural strengthening for the decidable-specialisation path (layer 2).

image() [3/5]

template<IsOckhamAlgebra L, IsCardinality C, IsArrow F>

auto dedekind::sets::image ( F && f, const Comprehension< 𝔸< Dom< std::remove_cvref_t< F > >, L, C >, Point< Dom< std::remove_cvref_t< F > > > > & s )

constexprexport

Image of a Singleton under an IsArrow.

singleton__Image

For an arrow f : T → U and a singleton {x} ⊂ T, the categorical image is f({x}) = {f(x)} ⊂ U. This is the cardinality-1 instance of the powerset-monad Kleisli bind: equivalent to s >>= (η ∘ f), where η wraps a value in a singleton (the Singleton-monad unit).

singleton__Image_Categorical_Anchor

Type-level breadcrumbs (placed downstream in morphologies:archimedean rather than below in this partition; see the closing note for why) tie the image construction back to:

• IsArrow: the source-side requirement. f's Domain must match the singleton's pivot type.
• The Kleisli triple's >>= (above): image(f, s) is the Singleton specialisation of the Set-monad's bind, factored through η.
• The image's tier ( IsExtensional, HasDecidableMembership): preserved by the lift, since Singleton has cardinality 1 in both source and target.

Filed under #602's layer-1 plan: per-shape image dispatch, Singleton source as the entry point. The same shape generalises to ExtensionalSet (sister source post-#598) and predicate sets (lazy / iso-witnessed cases). Note: the per-wrapper overload shape is itself due for dissolution under #607's Juliet-clean refactor; this slice lands the entry-point breadcrumbs in their current form.

image() [4/5]

template<dedekind::category::IsRetractableArrow F, IsSetObject S>
requires std::same_as<dedekind::category::Dom<std::remove_cvref_t<F>>, typename S::Domain> && (!dedekind::category::IsIsomorphism<std::remove_cvref_t<F>>)

auto dedekind::sets::image ( F && f, const S & s )

constexprexport

image(monic-with-retract f, {x ∈ 𝔸 | P}) — decidable specialisation for monic arrows that ship a retract (a partial inverse via the retract(f) ADL hook). #602 Layer 2 / Case A.

When f is a monomorphism (IsMonicArrow) AND ships a retract retract(f) : Cod(f) → std::optional<Dom(f)>, the image of an intensional Set is mechanically recoverable via the retract:

image(f, S)(y)
  = let mx = retract(f)(y);
    mx.has_value() ? S(*mx) : L::False

The retract contract is std::optional -shaped specifically (the IsRetractableArrow concept in :morphism gates on std::same_as<std::optional<Dom<F>>>); generalising to the project's broader IsPotential surface (Partial<T> / TernaryResult<T> etc.) is a deliberate follow-up.

This is independent of the IsIsomorphism specialisation above (#657 sister): although every iso has a structural total retract, this PR does not auto-register a retract hook for arbitrary iso arrows, so iso routes through the IsIsomorphism overload unchanged. The retract path handles the monic-but-not-iso case — most carrier-lattice embeddings in the project (embed_𝔹_ℕ, embed_uint_ℕ, embed_sint_ℤ, ...) are monic and admit a natural retract, and can opt in to this path by registering a retract overload alongside their existing is_monic_arrow_v declaration.

The result keeps the source's logic species L (no demotion to Ternary) and stores the composed predicate carrying both the source set and the retract callable.

Disambiguation against the iso overload

The !IsIsomorphism guard in the requires-clause keeps iso arrows on the simpler unconditional-inverse path above (#657) in the hypothetical case where a user did opt an iso arrow into the retract path (by registering a retract hook on it). Without that guard, an iso arrow that also happened to be retractable would be ambiguous between the two overloads; with it, iso always wins.

image() [5/5]

template<dedekind::category::IsIsomorphism F, IsSetObject S>
requires std::same_as<dedekind::category::Dom<std::remove_cvref_t<F>>, typename S::Domain>

auto dedekind::sets::image ( F && f, const S & s )

constexprexport

image(iso f, {x ∈ 𝔸 | P}) — decidable specialisation for isomorphism arrows (#602 Layer 2 entry).

When f admits an inverse f^{-1} (the IsIsomorphism gate), the image of an intensional Set under f is mechanically recoverable via predicate composition:

image(f, S) = { y ∈ Cod(f) | S(f^{-1}(y)) }

The result is a Comprehension<𝔸<U, L>, ComposedIsoImagePredicate<...>> — the same logic species L as the source (no demotion to Ternary), and a composed predicate that evaluates membership through the inverse. This is strictly stronger than the IsArrow fallback above, which honestly returns the always-Unknown SymbolicImagePredicate; iso arrows preserve decidability of the image because the existential ∃x ∈ T. P(x) ∧ y == f(x) reduces to a single test P(f^{-1}(y)).

Overload resolution picks this specialisation over the IsArrow one by partial-ordering (IsIsomorphism subsumes IsArrow).

expressions__Image_Iso_Layer2_Anchor

Layer-2 entry from the #602 layering proposal: the "predicate-set with iso" path that the Layer-1 overload's docstring flagged as the natural strengthening. Layer-2 continues with the retract path immediately below (Case A / #659), and further with enumerable-source (Case B / #660) and terminal-codomain (Case C / #661) over follow-up slices.

in_species()

template<typename L>

L::Ω dedekind::sets::in_species ( auto v )

constexpr

A verdict in the species L: an == that answers in L::Ω passes through, one that answers bool (a sized or structural equality) is lifted to ⊥ / ⊤.

Template Parameters

L	the species.

Parameters

v	the verdict.

inclusion_arrow()

template<typename S>
requires IsSubobject<std::remove_cvref_t<S>, typename std::remove_cvref_t<S>::Domain>

SubobjectInclusion< std::remove_cvref_t< S > > dedekind::category::inclusion_arrow ( const S & s )

constexpr

Parameters

s	a subobject.

Returns

its inclusion, an arrow.

into()

template<typename V, typename T, typename R>

V dedekind::sets::into ( const R & x )

constexpr

The value x of the operand T placed in the carrier V: a constant exactly or not at all (carrier_cast), a term's value by conversion.

Template Parameters

V	the carrier.
T	the operand term.

inverse()

template<typename T>
requires requires(T x) { { -x } -> std::convertible_to<T>; }

T dedekind::sets::inverse ( const T & x, std::plus< T >  )

constexprexport

Generic additive inverse for a carrier supporting unary negation: the +-inverse is -x, inferred from the negation structure rather than registered per carrier.

This is the canonical inverse(x, op) bridge that category::inverse_v (and the reified group-inverse arrow algebra::Inverse<T, +>, #959) consume. It covers SignedCardinality (ℤ) — which was asserted invertible (is_invertible_v) but had no computation bridge — and any sibling additive carrier, so the additive inverse need not be hand-registered per type. The ExtensionalCardinal<> overload above is a more-specialised non-template and still wins for it.

Note

The gate is unary negation ({-x}), the computational witness of an additive inverse — not IsGroup. Gating on IsGroup would be circular: IsGroup routes through IsInvertible / is_invertible_v, and forcing that evaluation for every candidate T during overload resolution trips a non-constant-expression substitution. Unary - is the honest, SFINAE-friendly signal that -x is the inverse.

join_sorts()

template<typename P>

std::size_t dedekind::sets::join_sorts ( std::size_t a, std::size_t b )

constexprexport

The common sort of two operands at points of P: a constant takes the other's, and a truth chain meets its dominance in the larger (𝔹 and K₃ in K₃).

Exceptions

not_admitted

where two carriers meet.

lift_conditionals()

template<typename K>

Pred< K > dedekind::sets::lift_conditionals ( const Pred< K > & p )

constexprexport

The predicate with every conditional lifted out of its atoms: cond(q, a, b) R c is (q ∧ a R c) ∨ (¬q ∧ b R c), the law of McCarthy's conditional, until no atom has one. The same set at every point; an applied set ap(S, t) == ⊤, the conditional cond(χ_S[π:=t], ⊤, ⊥) compared, becomes χ_S[π:=t] once the decided atoms are folded (algebra:polynomial's canonical).

Parameters

p	the predicate.

materialize_bounds()

template<typename T, typename L>

Ø< T, L > dedekind::sets::materialize_bounds ( LatticeBottom< T, subobject_order< L > > )

constexpr

boundaries__Engine_Routed_Lattice_Ops

The boundary meet / join are no longer hand-spelled inside Ø and 𝔸. They route through the generic lattice-law term reducer (category:lattice_term, #865/#890): the term Meet<boundary,S> / Join<boundary,S> is reduced under subobject_order<L>, where Ø is the ⊥ (initial) and 𝔸 the ⊤ (terminal) of Sub(T). The reducer's bounded law then supplies the four identities the members used to spell by hand (⊥∧X=⊥, ⊥∨X=X, ⊤∧X=X, ⊤∨X=⊤).

The four Ø / 𝔸 meet & join operators build the Meet / Join node value and hand it to the value-first subobject_reduce below.

meet_type()

template<typename A, typename B, typename RA, typename RB>

auto dedekind::sets::meet_type ( )

constexpr

The carrier two operands meet in: a constant takes the other's, two terms their common type.

Template Parameters

A,B	the operand terms.
RA,RB	the types of their values.

mul()

Cardinality dedekind::sets::mul ( const Cardinality & lhs, const Cardinality & rhs )

constexprexport

Cardinal multiplication under the finite/ℵ_0 policy.

x * ℵ_0 = ℵ_0 for any x.

negate()

Rel dedekind::sets::negate ( Rel r )

constexprexport

The De Morgan dual of a comparison: !(x R y) is x negate(R) y.

Parameters

r	the comparison.

one_sort()

template<typename P>

std::size_t dedekind::sets::one_sort ( const P & rep = P{} )

constexprexport

The points' one sort, where every slot has the same; no_sort on a product of several.

Parameters

rep	a point of P.

only_arguments()

bool dedekind::sets::only_arguments ( unsigned mask, unsigned n )

constexprexport

Whether a mask names only slots among π_1 … π_{n−1}, the arguments of a graph whose result is π_n.

Parameters

mask	the slots.
n	the result slot.

only_slot()

bool dedekind::sets::only_slot ( unsigned mask, unsigned slot )

constexprexport

Whether a mask names at most the given slot.

Parameters

mask	the slots.
slot	the one allowed.

op_admitted()

template<typename C>

bool dedekind::sets::op_admitted ( Arith op, bool divisor_is_constant )

constexpr

Whether op is admitted on the carrier C, with the divisor a constant (nonzero, checked when the term was built) or a term: the rules above and beside their certificates, read at run time.

Template Parameters

C	the carrier.

operator!() [1/2]

template<Rel R, typename A, typename B>

Cmp< negate(R), A, B > dedekind::sets::operator! ( const Cmp< R, A, B > & c )

constexprexport

!atom flips the comparison.

Parameters

c

the atom.

operator!() [2/2]

template<typename A, typename B>

auto dedekind::sets::operator! ( const RelAnd< A, B > & p )

constexprexport

De Morgan on the connectives: !(p && q) is !p || !q, and dually.

Parameters

p	the conjunction or disjunction.

operator&() [1/8]

template<typename L, typename C, std::integral K1, std::integral K2>

ResidueClass< L > dedekind::sets::operator& ( const 𝔸< Cardinality, L, C > & , const Cmp< Rel::Eq, BinOp< std::modulus<>, Projection< 0 >, Const< K1 > >, Const< K2 > > & c )

constexprexport

ℕ & (π % n == r): the residue class, decided analytically. A residue outside \([0, n)\) is never met, so π % 3 == 3 is empty. ADL finds it through the 𝔸<Cardinality> operand.

Template Parameters

K1	the modulus's type.
K2	the residue's type.

operator&() [2/8]

template<dedekind::order::IsTotallyOrdered T, dedekind::category::IsOckhamAlgebra L, IsCardinality C, Rel R, typename K>
requires (dedekind::order::is_order_rel(R))

dedekind::order::Interval< T, L > dedekind::sets::operator& ( const 𝔸< T, L, C > & , const Cmp< R, Projection< 0 >, Const< K > > & c )

constexprexport

An order atom π ⋈ k on a chain is the ray it names, whatever the constant's type: the constant meets the carrier exactly or the binding raises. Declared beside 𝔸 and the atom, so ADL finds it.

Template Parameters

T	the carrier.
R	the order relation.
K	the constant's type.

operator&() [3/8]

template<typename T, IsOckhamAlgebra L, IsCardinality C, IsRelPredicate P>
requires (only_slot(slots_v<P>, 0)) && (!contains_self_v<P>) && std::convertible_to<std::invoke_result_t<const P&, const T&>, bool>

auto dedekind::sets::operator& ( const 𝔸< T, L, C > & , P p )

constexprexport

𝔸<T> & atom for an atom on the unary π (ℕ & (π % 3 == 0)): the atom evaluated at each element.

Template Parameters

T	the carrier.
P	the atom.

operator&() [4/8]

template<typename T, IsOckhamAlgebra L, IsCardinality C, IsDatum< T > P>

auto dedekind::sets::operator& ( const 𝔸< T, L, C > & , P p )

constexprexport

The set former 𝔸<T, L>{} & P = \(\{x \in T \mid P(x)\}\) for a datum P (a point π == v, a cut π > v): the meet with the subobject P classifies (#826; | is the join only).

Template Parameters

T	the carrier.
L	the species.
C	the cardinality.
P	the datum.

operator&() [5/8]

template<typename T, IsOckhamAlgebra L, IsCardinality C, typename K>
requires (!requires { typename T::first_type; })

auto dedekind::sets::operator& ( const 𝔸< T, L, C > & , Pred< K > p )

constexprexport

𝔸<T> & pred for a predicate built at run time: bound to the carrier now, every operator admitted there or refused (not_admitted), every constant meeting it. Pairs take the product former.

Template Parameters

T	the carrier.
K	the constants' type.

operator&() [6/8]

template<std::semiregular T, IsOckhamAlgebra L, IsCardinality C, typename K>

auto dedekind::sets::operator& ( const 𝔸< T, L, C > & u, const Cmp< Rel::Eq, Projection< 0 >, Const< K > > & c )

constexprexport

𝔸<T> & (π == v): the singleton {v}, the constant converted into the carrier exactly or the binding raising. Declared beside 𝔸 and the atom, so ADL finds it.

Template Parameters

T	the carrier.
K	the constant's type.

operator&() [7/8]

template<IsSetObject S, typename Body>
requires contains_self_v<Body> && self_descends_v<Body, typename S::Domain> && std::same_as< std::invoke_result_t<const S&, const typename S::Domain&>, bool>

auto dedekind::sets::operator& ( const S & base, Body body )

constexprexport

The former that closes a recursion: S & body with a χ in the body is \(\{x \in S \mid body(x)\}\) where χ is that set. Viable only for a structural recursion over a decidable base; general recursion finds no former.

Template Parameters

S	the base.
Body	the body.

operator&() [8/8]

template<typename P, typename S, IsArrow T>

Prefixed< P, S, T > dedekind::category::operator& ( const Symmetric< P, S, T > & s, const Prefix & p )

constexpr

Parameters

s	the section.
p	the prefix.

Returns

their meet.

operator&&()

template<IsLogicalTerm P1, IsLogicalTerm P2>
requires (!IsPredicatePair<P1, P2>)

auto dedekind::sets::operator&& ( P1 && p1, P2 && p2 )

constexprexport

Predicate-level conjunction p1 && p2: structured_and when a domain collapse applies, else the reducer's Meet node, a callable predicate \(\chi_1 \wedge \chi_2\) that also carries its operands via π_1 / π_2. It is the same AST the set-level combinators use, so a set-builder Set{x | p1 && p2} shares one representation with A & B. There is no separate AndPredicate. A pair of predicates over one species is :topoi's conjunction (IsPredicatePair, which closes on IsPredicate); this one takes every other pair of terms.

Template Parameters

P1	the left term.
P2	the right term.

operator*()

template<typename A, typename LA, typename CA, typename B, typename LB, typename CB>
requires std::same_as<LA, LB>

auto dedekind::sets::operator* ( const 𝔸< A, LA, CA > & a, const 𝔸< B, LB, CB > & b )

constexprexport

The universal set of products: \(\mathbb{A}_A \times \mathbb{A}_B = \mathbb{A}_{A\times B}\), spelled as the universe over the product carrier (IsProduct).

Two total factors carry no restriction to lift, so the product is the pure product universe 𝔸<pair<A,B>> — not a refinement of it. This is the base case of the cylinder decomposition \(A\times B = \pi_1^{-1}(A)\cap\pi_2^{-1}(B)\): with A, B universal both cylinders are the whole universe, so their intersection is too. A restricted factor instead lifts its predicate onto its axis (dedekind.order: π_I over a halfspace), refining this universe into a proper subobject. The old melting form (pa(first) && pb(second) captured in an anonymous closure) discarded the factor structure; keeping the universe explicit lets dom / cod read the factors back.

operator+()

template<typename A, typename B>
requires TermOperands<A, B>

auto dedekind::sets::operator+ ( A a, B b )

constexprexport

The arithmetic of terms.

Template Parameters

A,B	the operands.

operator++()

Cardinality dedekind::sets::operator++ ( Cardinality n )

constexprexportnoexcept

++n / --n: the successor and the predecessor of the ℕ proxy, by value, saturating at ℵ₀ and stepping down by monus (#1002).

Why by value, and why only on types of our own.

• A user-defined operator need not mutate. Taken by value, ++n returns a new value and leaves n alone, so it keeps Rule 1 (no reference parameter, no reference returned, no state) and is the posture's spelling of Successor; it applies to a constant too. There is no postfix form: by value, n++ would be n itself.
• The built-in ++ mutates. On a const built-in it does not compile ("cannot assign to variable with const-qualified type"), so const already makes the compiler hold Rule 1 at the operator.
• It cannot be replaced: an overloaded operator must have a parameter of class or enumeration type, so no operator++ may be declared for size_t, const or not. Its successor is n + 1, or successor(n).
• The standard's incrementable concepts ask ++i for an I&, so they do not admit the by-value form, and std::views::iota does not walk such a type; chain_view walks by successor and cover instead.
• For counts with a by-value ++, a type of our own is the route: a struct around the word, or the smallest strong typedef the language has, enum class Nat : size_t {}, whose values are the word's and which std::to_underlying converts back.

  Parameters

  n	the element.

  Returns

  its successor (predecessor).

operator<<=()

template<std::equality_comparable T, IsOckhamAlgebra L, IsCardinality C, dedekind::category::IsArrow Func>
requires std::same_as<dedekind::category::Dom<Func>, Comprehension<𝔸<T, L, C>, Point<T>>>

auto dedekind::sets::operator<<= ( const Comprehension< 𝔸< T, L, C >, Point< T > > & s, const Func & f )

constexprexport

Co-Kleisli extend on a point, {x} <<= f = {f({x})}.

singleton__Singleton_CoKleisli_Triple

(<<=)

Template Parameters

T	the carrier.
L	the species.
C	the cardinality.
Func	the co-Kleisli arrow, a point → a value.

operator<=>()

std::partial_ordering dedekind::sets::operator<=> ( const SignedCardinality & lhs, const SignedCardinality & rhs )

constexprexportnoexcept

Explicit homogeneous <=> on SignedCardinality (#669).

Returns std::partial_ordering because NaZ is unordered with non-NaZ operands (IEEE-NaN-style). Special-case: NaZ <=> NaZ returns std::partial_ordering::equivalent so that the == above (which returns true on NaZ-vs-NaZ for std::equality_comparable reflexivity) and this <=> agree on the equivalence case, per std::three_way_comparable's contract (a == b) ↔ std::is_eq(a <=> b). Mixed NaZ vs non-NaZ comparisons remain unordered.

Required for std::three_way_comparable<SignedCardinality, std::partial_ordering> to fire downstream. Pairs with the == above to close the full standard-concept surface for the saturating ℤ proxy.

operator==() [1/2]

template<typename A, typename B>
requires TermOperands<A, B>

auto dedekind::sets::operator== ( A a, B b )

constexprexport

The comparisons of terms. The term operand is tested first, so a candidate never asks a carrier for its own equality.

Template Parameters

A,B	the operands.

operator==() [2/2]

bool dedekind::sets::operator== ( const SignedCardinality & lhs, const SignedCardinality & rhs )

constexprexportnoexcept

Explicit homogeneous == on SignedCardinality (#669).

Mirrors the == on Cardinality above: the std::variant's defaulted == lives inside the module's purview and is not reachable across the dedekind.sets module boundary (the <variant> header is in the global module fragment). Defining the operator explicitly in dedekind::sets — where ADL can find it from importers like dedekind.numbers and dedekind.algebra:ordered_algebra — closes the gap so std::equality_comparable<SignedCardinality>, std::regular<SignedCardinality>, and std::three_way_comparable<SignedCardinality, std::partial_ordering> fire downstream.

NaZ-vs-NaZ returns true: this is the variant-alternative equality reading, required for == to be an equivalence relation (reflexivity). The companion <=> below mirrors this — the NaZ-vs-NaZ case is special-cased to return std::partial_ordering::equivalent so that == and <=> agree on this pair, per C++20's std::three_way_comparable contract (a == b) ↔ std::is_eq(a <=> b). NaZ vs non-NaZ remains unordered in <=> (and false in ==), preserving IEEE-NaN-style unordered semantics for mixed comparisons.

Closes #669, which itself closes the persistent local-only build failure on sint.cppm:228 (embed_sint_ℤ(η(42)).pivot == finite_signed_cardinality(42)).

operator>>=()

template<std::equality_comparable T, IsOckhamAlgebra L, IsCardinality C, dedekind::category::IsArrow Func>
requires std::same_as<dedekind::category::Dom<Func>, T> && IsSetObject<dedekind::category::Cod<Func>>

auto dedekind::sets::operator>>= ( const Comprehension< 𝔸< T, L, C >, Point< T > > & s, const Func & f )

constexprexport

The Bricks of the Singleton Monad.

Kleisli Bind for points:

1. Sample the pivot (The Pull).
2. Apply the Kleisli Arrow f: T -> Singleton<U, L>.

operator^()

template<IsSetObject LHS, IsSetObject RHS>
requires std::same_as<typename LHS::Domain, typename RHS::Domain> && (!std::same_as<typename LHS::logic_species, typename RHS::logic_species>) && dedekind::category::HaveLogicJoin<typename LHS::logic_species, typename RHS::logic_species>

auto dedekind::sets::operator^ ( const LHS & a, const RHS & b )

constexprexport

Cross-species symmetric difference: both operands are lifted into the join of their species and △ is computed there (as for & and |).

Template Parameters

LHS	/
RHS	set objects on one carrier, of different species with a join.

operator|() [1/2]

template<typename A, typename B>
requires NatZedPair<A, B>

auto dedekind::sets::operator| ( const A & lhs, const B & rhs )

constexprexport

Cross-carrier join: a set over ℕ | a set over ℤ → a set over ℤ (carrier widening; closes a slice of #362). The union may contain negative integers from the rhs side, so the result carrier widens to ℤ.

Membership for v : ℤ:

• If v lives in the image of ℕ ↪ ℤ (non-negative, not NaZ, not -ℵ_0), evaluate lhs on the projected ℕ value and OR with rhs(v).
• Otherwise v is not in ℕ, so lhs(v) is structurally false; the union reduces to rhs(v).

operator|() [2/2]

template<typename S, typename P>
requires IsSetObject<S> && (!IsSetObject<P>) && (!IsLSet<P>)

void dedekind::sets::operator| ( const S & , const P &  )

exportdelete

S | P for a set and a non-set: refused. The filter is the meet, S & P (#826); | is the join of two sets only.

Template Parameters

S	the set.
P	the would-be filter.

operator||()

template<IsLogicalTerm P1, IsLogicalTerm P2>
requires (!IsPredicatePair<P1, P2>)

auto dedekind::sets::operator|| ( P1 && p1, P2 && p2 )

constexprexport

Predicate-level disjunction p1 || p2, dual to operator&&: structured_or when a collapse applies, else the reducer's Join node; a pair of predicates over one species is :topoi's (IsPredicatePair).

Template Parameters

P1	the left term.
P2	the right term.

operator~()

template<IsPredicate P>
requires IsSetObject<std::remove_cvref_t<P>>

auto dedekind::sets::operator~ ( const P & p )

constexprexport

The set complement ~A (#829: ~ is the SET complement; ! is the predicate complement, which category::operator! supplies as a formal Morphism). ~A is the reducer's own Not node — a first-class subobject whose χ is the codomain reflection Ω::RFL of A's, generic over any bounded chain (Boole !, Kleene ¬U=U, and any registered Chain). There is no bespoke wrapper and no is_set_node_v tag: the gate is the structural IsSubobject, and because category defines no operator~ there is nothing to out-prioritise, so the tag that once disambiguated the two operator! overloads is gone (#963). The const reference parameter (matching operator& / operator|) makes this a FALLBACK that loses partial ordering to a type-specific complement, so a :order Halfspace / Singleton operator~ still wins for its own type (its closed-form collapse, e.g. ~Above<5> = AtMost<5>).

The complement is a certified involution: ~~A ≡ A, peeled here at the leaf (the reducer's ¬¬A→A). Because ~A is a Not node, the reducer's own complement laws apply in operator& / operator|: ¬(A∧B)→¬A∨¬B (De Morgan) and a∧¬a→⊥ / a∨¬a→⊤ when the codomain Ω is complemented.

pin_constants()

template<typename P, typename K, typename Lift>

Pred< K > dedekind::sets::pin_constants ( const Pred< K > & p, const Lift & lift, const P & rep )

constexprexport

The predicate with every numeral pinned to the sort its context gives it at points of P: the constant then names its sort itself, so the term keeps its meaning when it moves (substituted into another context by ap, or split by lift_conditionals into an atom with no slot left).

Parameters

p	the predicate.
lift	a value of a sort into a constant that names it (constant_of).

pin_term()

template<typename P, typename K, typename Lift>

Term< K > dedekind::sets::pin_term ( const Term< K > & t, std::size_t s, const Lift & lift, const P & rep )

constexpr

The term t, of the sort s at points of P, with every numeral pinned to it.

Parameters

t	the term.
s	its sort.
lift	a value of a sort into a constant that names it.
rep	a point of P.

point_of()

template<typename T, typename... Vs>

T dedekind::sets::point_of ( const Vs &... vs )

constexpr

A point of T from the terms' values: the scalar, or the pair.

Template Parameters

T	the point's type.
Vs	the values.

power_set() [1/2]

template<typename T, typename L>

auto dedekind::sets::power_set ( const Ø< T, L > & )

constexprexport

\(\mathfrak{P}(\emptyset) = \{\emptyset\}\) — the one power set that needs no subobject normal-form, so it is a closed form here in :sets.

The empty set has exactly one subset (itself), so its power set is the singleton \(\{\emptyset\}\) (cardinality \(1 = 2^0\), not \(\emptyset\)). That singleton is exactly the universe over the one-inhabitant domain Ø<T,L>: every empty set is equal to every other (Ø's cross-carrier ==), so 𝔸 over the empty-set carrier has a single inhabitant, \(\emptyset\) itself. No Sub, no ordered carrier, no Rice-walled subobject enumeration — which is why the empty node of the grammar can be discharged upstream of the interval specialisation. This is a more-specialised overload than the deleted SetShaped gate, so it wins by partial ordering.

power_set() [2/2]

template<typename S>
requires SetShaped<S>

auto dedekind::sets::power_set ( const S & )

exportdelete

Power set \(\mathfrak{P}(S)\) — the default declaration (customization-point gate).

Establishes the :sets-level signature for power_set / 𝔓 and is =delete d, so a set-shaped base with no decidable power set is a clean type error (type-check failure by default). The decidable specialisations live downstream, where the subset order does: dedekind.order:powerset gives the ordered / convex case ( \(\mathfrak{P}(S) = \mathbb{A}\langle\mathrm{Sub}(C)\rangle \mid X \subseteq S\) over the subobject domain Sub(C), an interval), covering 𝔸 / Singleton / Halfspace / Interval by coercion; a finite-carrier / erased case may follow (#830). The one exception is \(\mathfrak{P} (\emptyset) = \{\emptyset\}\), which needs no subobject domain and is a closed form here in :sets (below). Same shape as exists / forall (an algebraic default lifted by per-carrier decidable specialisations). A non-set-shaped argument fails SetShaped and matches nothing (also a type error).

See also

Lambek and Scott [5]

predecessor() [1/3]

template<IsWrappingWord W>

ExtensionalCardinal< W > dedekind::sets::predecessor ( const ExtensionalCardinal< W > & n )

constexprexportnoexcept

Parameters

n	a cardinal.

Returns

its predecessor, modulo the word.

predecessor() [2/3]

SignedCardinality dedekind::sets::predecessor ( const SignedCardinality & n )

constexprexportnoexcept

The step down on the ℤ proxy: −1 through the saturating -, so −ℵ_0 is a fixpoint and NaZ propagates. Unlike ℕ there is no monus: ℤ steps down past zero.

Parameters

n	the value to step from.

Returns

n − 1, saturating.

predecessor() [3/3]

template<std::integral S>

SignedExtensionalCardinal< S > dedekind::sets::predecessor ( const SignedExtensionalCardinal< S > & n )

constexprexportnoexcept

Parameters

n	a signed cardinal.

Returns

its predecessor, modulo the word.

product_membership()

template<typename A, typename B>

ProductMembership< A, B > dedekind::sets::product_membership ( const A & a, const B & b )

constexpr

The product's membership, built from its factors.

Parameters

a
b	the factors.

realize_to_size_t()

std::size_t dedekind::sets::realize_to_size_t ( const Cardinality & value, std::size_t transfinite_sentinel = std::numeric_limits<std::size_t>::max() )

constexprexport

Realize a cardinality value to std::size_t with explicit boundary.

Parameters

transfinite_sentinel

Value used for non-finite cardinalities.

rel_admitted()

template<typename C>

bool dedekind::sets::rel_admitted ( Rel r )

constexprexport

Whether the comparison r is admitted on C: == and != where it compares, the order comparisons where the order's rule is in force (order:poset).

Template Parameters

C	the carrier.

rel_apply()

template<Rel R, typename X, typename Y>

bool dedekind::sets::rel_apply ( const X & x, const Y & y )

constexprexport

x R y.

Template Parameters

R	the comparison.

Parameters

x	the left value.
y	the right value.

restriction() [1/3]

template<std::size_t K, typename X, typename Y, typename L, typename C>
requires (K == 1 || K == 2)

auto dedekind::sets::restriction ( const 𝔸< std::variant< X, Y >, L, C > & )

constexprexport

\(\iota_K^{-1}\) is a lattice homomorphism (a pullback preserves \(\wedge, \vee, \neg, \bot, \top\)): the restriction reaches through the lattice's nodes to the sums beneath, and the boundaries restrict to the boundaries — the universe of the sum to the universe of the summand (the sum's cardinality class kept: a sound bound, the summand's own is not recorded on a bare universe), Ø to Ø.

Template Parameters

K	the summand.

restriction() [2/3]

template<std::size_t K, typename X, typename Y, typename T2, typename L, typename C, typename A, typename B>
requires (K == 1 || K == 2) && requires(const A& a) { restriction<K>(a); }

auto dedekind::sets::restriction ( const Comprehension< 𝔸< std::pair< std::variant< X, Y >, T2 >, L, C >, ProductMembership< A, B > > & r )

constexprexport

A relation out of a sum restricted to one summand: \((A + B) \times C \cong A \times C + B \times C\) (distributivity), so \((\iota_k \times \mathrm{id})^{-1}(s \times c) = \iota_k^{-1}(s) \times c\). A relation Either<a, b> ⇸ c that only accepts a is the relation a ⇸ c.

Template Parameters

K	the summand.

Parameters

r	the relation.

restriction() [3/3]

template<std::size_t K, typename X, typename Y, typename L, typename C, typename A, typename B>
requires (K == 1 || K == 2)

auto dedekind::sets::restriction ( const Comprehension< 𝔸< std::variant< X, Y >, L, C >, SumMembership< A, B > > & s )

constexprexport

The restriction of a set of a sum to its k-th summand, \(\iota_k^{-1}(s)\): the forward map of the lattice isomorphism \(\mathrm{Sub}(X + Y) \cong \mathrm{Sub}(X) \times \mathrm{Sub}(Y)\). A pair of sets is no set: the sum itself is the coproduct of its summands in Set, not their product, so it carries no π_k.

Template Parameters

K	the summand, 1 or 2.

Parameters

s	the set of the sum.

row_of_sorts()

template<typename... Cs>

Row< Cs... > dedekind::sets::row_of_sorts ( const std::vector< std::size_t > & sorts )

constexprexport

The row whose columns have the sorts sorts: a representative of the points of that schema, for binding and normal forms.

Template Parameters

Cs	the carriers.

Parameters

sorts

an index into Cs per column.

same_shape() [1/2]

template<typename K>

bool dedekind::sets::same_shape ( const Pred< K > & x, const Pred< K > & y )

constexprexport

The same predicate tree, atom by atom.

Parameters

x,y	the predicates.

same_shape() [2/2]

template<typename K>

bool dedekind::sets::same_shape ( const Term< K > & x, const Term< K > & y )

constexprexport

The same tree: the same nodes, slots, operators and comparisons, and equal constants. Syntactic, so sound for equality of what two normal forms denote and silent on two different trees.

Parameters

x,y	the terms.

search_value()

template<typename C>

C dedekind::sets::search_value ( std::uint64_t i )

constexprexport

The i-th value of a carrier for a bounded search: a finite chain cycles through its values from ⊥, an unsigned word counts up, and any other carrier states its enumeration as nth_value(type_identity<C>, i), found by ADL beside its definition (Modular: 0, 1, −1, 2, −2, …).

Template Parameters

C	the carrier.

Parameters

i	the index.

self_arg()

template<typename T, typename X>
requires HasTermValueAt<T, X>

std::optional< value_at_t< X, T > > dedekind::sets::self_arg ( const T & t, const X & x )

constexpr

A χ argument's value at a point: the term's value, or nullopt for a descent below the carrier's bottom (no point of the universe, so the pulled-back membership is false there).

Template Parameters

X	the point type.

set_bound()

template<typename C, typename... Cs>

void dedekind::sets::set_bound ( Row< Cs... > & row, const C & v )

constexprexport

The last cell of row set to v, of the sort C: the bound column's value under a quantifier.

Parameters

row	the extended row.
v	the value.

singleton()

template<IsOckhamAlgebra L = Boole, typename T>

auto dedekind::sets::singleton ( T value )

constexprexport

singleton: \(T \to \mathrm{Singleton}\langle T\rangle\) — the power-set monad's unit \(\eta\) (see the section note).

singleton__The_Set_Monad_Realization

The singleton \(x \mapsto \{x\}\) is the unit of the power-set monad. It is the power-set instance of the categorical unit machinery in dedekind.category: the tag-dispatched η / pure and its siblings μ / ε / δ (:monad, laws checked by IsMonad; η / ε live in :natural), whose Frobenius monad (IsFrobenius, #632) carrier is std::tuple (:kleisli). The power-set monad's own functor (η

• the union-flatten μ) is tracked in #691. Distinct from the two other reifications of the power object: dedekind.order:powerset (#830) is the Sub(C) subobject lattice 𝔓 (a Set), and the enumeration (the characteristic relation \(\chi : S \to 2\) over a countable carrier) is #840.

  Template Parameters

  L	the species.
  T	the pivot's type (decayed into the carrier).

slot_sort()

template<typename P>

std::size_t dedekind::sets::slot_sort ( unsigned slot, const P & rep = P{} )

constexprexport

The sort of the slot slot at points of P, an index into point_sorts_t.

: read off the type, or off a representative row, whose cells are its schema.

Exceptions

not_admitted

for a slot the points have not.

Parameters

rep	a point of P (any, for a typed point).

slots()

template<typename K>

unsigned dedekind::sets::slots ( const Term< K > & t )

constexprexport

The slots a term built at run time mentions, as a mask: the run-time twin of slots_v, read with the same only_slot.

Parameters

t

the term.

sort_embeds()

template<typename P>

bool dedekind::sets::sort_embeds ( std::size_t from, std::size_t into )

constexprexport

Whether a value of the sort from is read in the sort into at points of P (EmbedsInto): the same sort, or along the dominance.

Parameters

from,into

indices into term_sorts_t

.

sort_of()

template<typename P, typename K>

std::size_t dedekind::sets::sort_of ( const Term< K > & t, const P & rep = P{} )

constexprexport

The sort of a term built at run time at points of P, from its projections and its constants of a sort (constant_sort): no_sort for a tree of numerals, which takes its context's. Defined with Term.

Template Parameters

P	the point type.

split_cond()

template<typename K>

std::optional< CondSplit< K > > dedekind::sets::split_cond ( const Term< K > & t )

constexpr

The first conditional of t, leftmost, split out; nullopt for a term without one.

Parameters

t

the term.

structured_and()

template<IsRelPredicate A, IsRelPredicate B>

RelAnd< A, B > dedekind::sets::structured_and ( A a, B b )

constexprexport

The meet and join of two relational predicates under the reducer's customization-point names, so the set-level & / | on two relations over one product collapse to one comprehension.

Template Parameters

A,B	the operands.

successor() [1/3]

template<IsWrappingWord W>

ExtensionalCardinal< W > dedekind::sets::successor ( const ExtensionalCardinal< W > & n )

constexprexportnoexcept

The NNO's step on the extensional cardinals, the wrapping ring \(\mathbb{Z}/2^w\): n + 1 and n - 1 modulo the word, as on the word itself.

Parameters

n	a cardinal.

Returns

its successor.

successor() [2/3]

SignedCardinality dedekind::sets::successor ( const SignedCardinality & n )

constexprexportnoexcept

The step up on the ℤ proxy, the free customization point the order layer's point collapse calls (category:nno, found here by ADL), as on Cardinality: +1 through the saturating +, so +ℵ_0 is a fixpoint and NaZ propagates.

Parameters

n	the value to step from.

Returns

n + 1, saturating.

successor() [3/3]

template<std::integral S>

SignedExtensionalCardinal< S > dedekind::sets::successor ( const SignedExtensionalCardinal< S > & n )

constexprexportnoexcept

Parameters

n	a signed cardinal.

Returns

its successor, modulo the word.

term_of()

template<typename X>

auto dedekind::sets::term_of ( X x )

constexprexport

A term as itself, a constant as Const.

Parameters

x	the operand.

term_value() [1/2]

template<typename T, typename P>

auto dedekind::sets::term_value ( const T & t, const P & p )

constexprexport

The value of a term or predicate at a point.

Parameters

t	the term.
p	the point.

term_value() [2/2]

template<IsRingIntegral auto I, typename P>

decltype(auto) dedekind::sets::term_value ( Projection< I > , const P & p )

constexprexport

A projection read at a point: its coordinate, or the point itself for the unary π. An overload for another kind of point (an environment) is found by ADL.

Parameters

p	the point.

term_value_as()

template<typename C, typename K, typename P>

C dedekind::sets::term_value_as ( const Term< K > & t, const P & p )

constexprexport

A term built at run time read in the sort C its context names (the other side of a graph atom, say), at the point p.

Template Parameters

C

the sort.

Parameters

t	the term.
p	the point.

universe()

template<typename T, typename L, typename C>

𝔸< T, L, C > dedekind::sets::universe ( const 𝔸< T, L, C > & u )

constexprexport

A universe is its own universe: the fixpoint of the universe leg.

boundaries__SetObject_Legs

The default legs of a set object (IsSetObject, :boundaries): every set object over a carrier T under logic L has the universe 𝔸<T,L> unless it says otherwise, and IS its own classifier unless it carries a separate predicate datum. The defaults live here because 𝔸 does; a type with sharper knowledge (a comprehension: its base's universe; Set: its predicate; an :order arm over a carrier with a known cardinality class) overloads in its own module and wins by partial ordering.

verdict()

template<typename P, typename K>

dedekind::category::Ternary dedekind::sets::verdict ( const Pred< K > & t, const P & point, std::uint64_t budget = std::uint64_t{1} << 16 )

constexprexport

The verdict of a predicate at a point, in K₃: a comparison or a quantifier over a finite chain is decided (⊤ or ⊥); a quantifier over an infinite carrier searches its first budget values (search_value): a witness of ∃ is ⊤, a counterexample to ∀ is ⊥, and an exhausted budget is U, never the other verdict (Σ, respectively Π: the run-time reading of Semidecided). Same-kind quantifiers over infinite carriers nested below (a middle object of several columns) share the budget, b values each with b^k ≤ budget; an opposite quantifier over an infinite carrier inside answers U. The connectives are Kleene's.

Template Parameters

P	the point type.

Parameters

t	the predicate.
point	the point.
budget	the search's values.

with_bound()

template<typename... Cs>

Row< Cs... > dedekind::sets::with_bound ( const Row< Cs... > & rep, std::size_t sort )

constexprexport

The row rep extended by a column of the sort sort: the point a quantifier's body is read at. Any other point has no column to bind.

Parameters

rep	the row.
sort	the bound column's sort.

with_sort()

template<typename P, std::size_t I = 0, typename F>

auto dedekind::sets::with_sort ( std::size_t s, const F & f )

constexprexport

Apply f to the sort s of P as a type: f(type_identity<C>). s is a valid index (the caller joined the sorts).

Template Parameters

P	the point type.
I	the first candidate.

Variable Documentation

ℕ

auto dedekind::sets::ℕ = 𝔸<Cardinality>{}

inlineconstexprexport

The canonical Natural-numbers universe ℕ = 𝔸<Cardinality> (post-#559).

Per #559's chosen direction (option A): the named species symbols (𝔹 / ℕ / ℤ / ℚ / ℝ / ℂ / 𝔻) denote the universe values (constexpr instances of 𝔸 over the carrier), not carrier types. Carrier types are spelled directly (bool, Cardinality, SignedExtensionalCardinal<>, ...) in template-type-parameter positions; the math symbols denote the sets.

This makes ℕ | (π ⋈ c) the canonical spelling for a subset of the natural-numbers universe, close to textbook notation.

Pre-#559 the spelling was using ℕ = dedekind::sets::Cardinality (carrier-type alias, post-#402); the ~110 type-context sites of ℕ in concept gates and static_asserts were migrated to Cardinality directly in step 1 of the ℕ slice.

Carrier reading retained: Cardinality is the variant ℕ-proxy (= std::variant<ExtensionalCardinal<>, ℵ_0>) — saturating to ℵ_0 on overflow rather than wrapping the way unsigned int would. The structural advantage: the variant honestly models ℕ (no additive inverses; rig-not-ring), whereas unsigned int is structurally more than ℕ (modular ring with additive inverses). Witnesses (IsRig, IsCommutativeMonoid, IsTotallyOrdered, IsDirectedSet, IsDirectedPoset, ...) are now expressed against Cardinality directly.

abs_

auto dedekind::sets::abs_

inlineconstexprexport

Initial value:

=
    dedekind::category::arrow<SignedCardinality, Cardinality>(
        [](const SignedCardinality& z) noexcept { return abs(z); })

Arrow form of abs: an exported arrow<SignedCardinality, Cardinality> object. Registered epic (surjective) below: every Cardinality is the image of itself ( abs(lift_ℕ_ℤ_(c)) = c) and of its negation; the map is sign-folding, conflating +n and -n. Companion to the injective lift_ℕ_ℤ_ in numbers:integer — together they exhibit the split-mono pair from the carrier-lattice diagram (Figure 1).

arity_v

template<typename X>

std::size_t dedekind::sets::arity_v

inlineconstexpr

Initial value:

=
    requires { typename X::first_type; } ? 2 : 1

The number of coordinates of a point of X.

contains_self_v

template<typename T>

bool dedekind::sets::contains_self_v

inlineconstexprexport

Initial value:

= decltype(cata(
    MentionsSelf{}, std::declval<const std::remove_cvref_t<T>&>()))::value

Whether T mentions the set under definition.

Template Parameters

T	the term or predicate.

embed_𝕂3_ℤ_

auto dedekind::sets::embed_𝕂3_ℤ_

inlineconstexprexport

Initial value:

=
    arrow<Ternary, dedekind::sets::SignedCardinality>(
        [](const Ternary& t) noexcept -> dedekind::sets::SignedCardinality {
          switch (t) {
            case Ternary::False:
              return dedekind::sets::finite_signed_cardinality(-1);
            case Ternary::Unknown:
              return dedekind::sets::finite_signed_cardinality(0);
            case Ternary::True:
              return dedekind::sets::finite_signed_cardinality(1);
          }
          return dedekind::sets::SignedCardinality{dedekind::sets::NaZ{}};
        })

Canonical embedding K3 ↪ ℤ: Ternary → SignedCardinality.

Maps False → -1, Unknown → 0, True → 1. Lands on the variant ℤ-proxy carrier SignedCardinality (closes #430, a #402 prerequisite); the previous int codomain made the K3 → variant-ℤ chain require an explicit machine-side extraction step. The unreachable default returns NaZ for IEEE-NaN-style propagation if a non-canonical Ternary value were ever constructed (cannot happen in practice — Ternary is a closed enum).

is_self_v

template<typename T>

bool dedekind::sets::is_self_v = false

inlineconstexprexport

Whether a leaf is the set under definition, a χ node; :recursion registers it.

Template Parameters

T

the leaf.

is_sort_of_v< C, std::tuple< Cs... > >

template<typename C, typename... Cs>

bool dedekind::sets::is_sort_of_v< C, std::tuple< Cs... > >

inlineconstexpr

Initial value:

=
    (std::same_as<C, Cs> || ...)

is_total_term_v

template<typename X, typename T>

bool dedekind::sets::is_total_term_v

inlineconstexprexport

Initial value:

=
    decltype(cata(Total<X>{}, std::declval<const T&>()))::value

A term total at every point of type X.

Template Parameters

X	the point type.
T	the term.

lift_ℕ_ℤ_

auto dedekind::sets::lift_ℕ_ℤ_

inlineconstexprexport

Initial value:

=
    arrow<dedekind::sets::Cardinality, dedekind::sets::SignedCardinality>(
        [](const dedekind::sets::Cardinality& c) noexcept {
          return dedekind::sets::lift_cardinality_to_signed(c);
        })

Canonical variant-layer embedding ℕ ↪ ℤ: Cardinality → SignedCardinality, exposed as a first-class arrow object for the carrier-lattice diagram.

Wraps dedekind::sets::lift_cardinality_to_signed (the public function definition; lives in sets:cardinality to remain reachable from cross-variant comparison operators without crossing the sets → numbers module boundary). This arrow form is the named monic morphism the carrier-lattice Figure 1 labels at the variant-layer top row. The corresponding machine-layer horizontal arrow (arrow<unsigned, int>, previously embed_uint_sint_) was removed in #670 as deprecated; the carrier-lattice diagram is consequently missing that middle-row machine-layer ℕ→ℤ link until a follow-up restores it on the new ℤ carrier (SignedCardinality). Registered as monic below.

self_descends_v

template<typename Node, typename T>

bool dedekind::sets::self_descends_v

inlineconstexprexport

Initial value:

=
    some_measure<Node, T>(std::make_index_sequence<arity_v<T>>{})

The structural-recursion gate: one coordinate on which every Self in the body descends. Vacuous without a Self.

Template Parameters

Node	the body.
T	the point type.

slot_at

template<typename X, std::size_t J>

std::size_t dedekind::sets::slot_at

inlineconstexpr

Initial value:

=
    requires { typename X::first_type; } ? J + 1 : 0

The coordinate a position of χ's arguments stands for at points of X: the point itself (slot 0) for a scalar, slot J + 1 of a pair.

Template Parameters

X	the point type.
J	the position, from 0.

slots_v

template<typename T>

unsigned dedekind::sets::slots_v

inlineconstexprexport

Initial value:

= decltype(cata(
    Slots{}, std::declval<const std::remove_cvref_t<T>&>()))::value

The slots T mentions, through any cv-ref (a constexpr variable's decltype is const).

Template Parameters

T	the term or predicate.