Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind.sets Module Reference

Concepts

concept  dedekind::sets::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  dedekind::sets::HasSetComplement
 A set with a set complement: ~s is formed (the reducer's Not node, or a type's own closed-form complement).
concept  dedekind::sets::Is𝔸
 A universe: the terminal object of Sub(T) — the reified type constraint 𝔸<T,L,C> itself (carrier, logic, cardinality class).
concept  dedekind::sets::Is𝔸Of
 U is the universe leg of S: a universe over the same carrier under the same logic.
concept  dedekind::sets::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  dedekind::sets::HasUpperBound
 ETCS-aligned upper bound for meet/intersection cardinality.
concept  dedekind::sets::StdSetLike
concept  dedekind::sets::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  dedekind::sets::IsTerm
 A term of the grammar.
concept  dedekind::sets::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  dedekind::sets::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  dedekind::sets::IsGraphAtom
 An atom that is the graph of a function of the first slot.
concept  dedekind::sets::HasDecidableMembership
 S's membership map ranges into two-valued (classical) logic.
concept  dedekind::sets::IsDecidableSet
 A Boolean-valued L-set: an IsLSet whose membership is decidable (χ factors through the dominance Σ ↪ Ω; logic_species is Boole).
concept  dedekind::sets::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  dedekind::sets::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  dedekind::sets::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  dedekind::sets::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  dedekind::sets::IsCardinality
concept  dedekind::sets::IsCountable
concept  dedekind::sets::IsFinite
concept  dedekind::sets::IsExtensional
concept  dedekind::sets::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  dedekind::sets::IsRingIntegral
 The old name of IsIntegerChain, which never claimed a ring.
concept  dedekind::sets::IsWhereClause
 Quantifiers over a finite carrier, decided by type through the finite quotient rather than by enumeration.
concept  dedekind::sets::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.).

Classes

struct  dedekind::sets::Ø< T, L >
 ∅: The Initial Object. Extensional (Size 0). More...
struct  dedekind::sets::𝔸< T, L, C >
 The universal set over the carrier T: the terminal object ⊤ of Sub(T), the reified type constraint. More...
struct  dedekind::sets::Subobjects< T, L >
 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  dedekind::sets::subobject_order< L >
 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  dedekind::sets::ExtensionalSet< T, L, Hash, Equal >
struct  dedekind::sets::RelAnd< A, B >
 Meet (conjunction) of two relational predicates, the result of && on them. More...
struct  dedekind::sets::RelOr< A, B >
 Join (disjunction) of two relational predicates, the result of || on them, dual to RelAnd. More...
struct  dedekind::sets::Const< K >
 A constant, carried as a value. More...
struct  dedekind::sets::BinOp< Op, A, B >
 a op b, the operator a standard functor (std::plus<>, minus, multiplies, divides, modulus) applied in one carrier. More...
struct  dedekind::sets::Ap< F, A >
 An arrow applied to a term, f(a). More...
struct  dedekind::sets::CondT< P, A, B >
 McCarthy's conditional on terms: a where p holds, else b. More...
struct  dedekind::sets::Cmp< R, A, B >
 The atom a R b over two terms, a relational predicate. More...
struct  dedekind::sets::Term< K >
 A term built at run time, the grammar with its shape a value; defined after the binding below. More...
struct  dedekind::sets::Pred< K >
 A relational predicate built at run time: comparisons of terms and their connectives; defined after the binding below. More...
struct  dedekind::sets::On< C >
 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  dedekind::sets::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  dedekind::sets::EuclideanDivision
struct  dedekind::sets::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  dedekind::sets::Row< Cs >
 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  dedekind::sets::Definition< K >
 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  dedekind::sets::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  dedekind::sets::SetExpr< Derived, DomainT, L >
 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  dedekind::sets::Comprehension< Base, Predicate >
struct  dedekind::sets::UniversalPredicate< T >
 The universal predicate: accepts every element of T. More...
struct  dedekind::sets::EmptyPredicate< T >
 The empty predicate: rejects every element of T. More...
struct  dedekind::sets::UnknownPredicate< T >
 The archetypal undecidable predicate: answers Unknown everywhere. More...
struct  dedekind::sets::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  dedekind::sets::Complement< T, L >
 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  dedekind::sets::InitialObjectArrow< Init, Target >
 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  dedekind::sets::SymbolicImagePredicate< U >
 Symbolic image-of-intensional-Set predicate (#602 layer 1). More...
struct  dedekind::sets::SumMembership< A, B >
 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  dedekind::sets::Restrict< K, UA, UB >
 \(\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  dedekind::sets::Inject< K, UA, UB >
 \(\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  dedekind::sets::Point< T >
struct  dedekind::sets::Finite
struct  dedekind::sets::is_extensional< T >
 Primary trait: Is a species defined by its members? More...
struct  dedekind::sets::ℵ< N >
struct  dedekind::sets::ExtensionalCardinal< W >
 Finite extensional cardinal: one machine word W. More...
struct  dedekind::sets::CardinalityEffect
 Draft writer-like cardinality effect carrier. More...
struct  dedekind::sets::SignedExtensionalCardinal< S >
 Signed one-word integer: two's complement in the signed word S. More...
struct  dedekind::sets::PositiveInfinity
struct  dedekind::sets::NegativeInfinity
struct  dedekind::sets::NaZ
struct  dedekind::sets::Env< T, R >
 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  dedekind::sets::Self< Terms >
 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  dedekind::sets::ChiTag
 The classifier under definition: χ(terms…) in a former's body is the set being formed, applied to the terms. More...
struct  dedekind::sets::Rec< S, Body >
 The recursion, closed: the base's membership, then the body evaluated with this very predicate in scope for its Self nodes. More...

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).

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.
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.
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.
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.
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.

Functions

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 A, typename Chi>
constexpr auto dedekind::category::universe (const Subobject< A, Chi > &)
template<typename A, typename Chi>
constexpr const Subobject< A, Chi > & dedekind::category::classifier (const Subobject< A, Chi > &s)
template<typename A>
requires requires(const A& a) { universe(a); }
constexpr auto dedekind::category::universe (const Not< A > &n)
template<typename A>
constexpr const Not< A > & dedekind::category::classifier (const Not< A > &n)
template<typename A, typename B>
requires requires(const A& a) { universe(a); }
constexpr auto dedekind::category::universe (const Meet< A, B > &m)
template<typename A, typename B>
constexpr const Meet< A, B > & dedekind::category::classifier (const Meet< A, B > &m)
template<typename A, typename B>
requires requires(const A& a) { universe(a); }
constexpr auto dedekind::category::universe (const Join< A, B > &j)
template<typename A, typename B>
constexpr const Join< A, B > & dedekind::category::classifier (const Join< A, B > &j)
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 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<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<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 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<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 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>
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 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<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.
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<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 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 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 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 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<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 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 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 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<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<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<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<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 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<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.

Variables

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 Projection< 1 > dedekind::sets::𝑥 {}
constexpr Projection< 2 > dedekind::sets::𝑦 {}
constexpr Projection< 3 > dedekind::sets::𝑧 {}
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 C, typename S>
constexpr bool dedekind::sets::is_sort_of_v = false
 Whether C is one of the sorts S.
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 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).
constexpr ChiTag dedekind::sets::χ {}
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.

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)

Files

file  src/main/modules/dedekind/sets/sets.cppm
 The Dedekind Set Model: Concrete Collections and Set Morphisms.
file  src/main/modules/dedekind/sets/boundaries.cppm
 The Extremal Identities: Universal (V) and Empty (∅) Sets.
file  src/main/modules/dedekind/sets/cardinality.cppm
 Cardinality types and the one-word extensional cardinal carrier.
file  src/main/modules/dedekind/sets/computability.cppm
 Decidable membership as a compile-time observable.
file  src/main/modules/dedekind/sets/expressions.cppm
 Set-builder DSL — comprehension + Boolean connectives.
file  src/main/modules/dedekind/sets/extensional.cppm
 ExtensionalSet — the canonical small-finite extensional carrier, with std::set / std::unordered_set round-trips.
file  src/main/modules/dedekind/sets/heterogeneous.cppm
 Set expressions ACROSS carriers: the product \(A \times B\), the sum \(A + B\), and the one widening the library ships, ℕ ↪ ℤ.
file  src/main/modules/dedekind/sets/quantifier.cppm
 Bounded first-order quantifiers as set operations: \(\exists\) is non-emptiness of a comprehension, \(\forall\) its \(\neg\exists\neg\) dual.
file  src/main/modules/dedekind/sets/recursion.cppm
 Inductive sets: χ, the classifier under definition, inside its own comprehension; the former closes the recursion and admits only a descent.
file  src/main/modules/dedekind/sets/singleton.cppm
 The equality atom: the point {x} as a comprehension over 𝔸<T>.
file  src/main/modules/dedekind/sets/terms.cppm
 The term grammar of comprehensions: projections, constants carried as values, arithmetic, arrows applied to terms, conditionals; the comparison atom over two terms; the pointwise connectives of relational predicates.