boundaries.cppm File Reference

The Extremal Identities: Universal (V) and Empty (∅) Sets. More...

#include <algorithm>
#include <compare>
#include <concepts>
#include <cstddef>
#include <cstdint>
#include <functional>
#include <limits>
#include <ranges>
#include <type_traits>
#include <utility>
import dedekind.sets:cardinality;
import dedekind.category;

Include dependency graph for boundaries.cppm:

Classes
struct	dedekind::sets::Ø< T, L >
	∅: The Initial Object. Extensional (Size 0). More...
struct	dedekind::sets::Ø< T, L >::Member
	Member-shape mirror of Subobject's. Vacuously inhabited (Ø has no members) — but the wrapper type is still required so the IsSubobject contract has a Member-to-T projection to read through ι. More...
struct	dedekind::sets::default_cardinality< T >
	Trait behind default_cardinality_t: ℵ_0 for every carrier (the countable fiction of #680) ... More...
struct	dedekind::sets::default_cardinality< bool >
	... except bool, which is Finite by its representation. 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::𝔸< T, L, C >::Member
	Member-shape mirror of Subobject's: every element of T is a member of U via the always-True classifier; the wrapper carries the T-value the IsSubobject contract reads back through ι. More...
struct	dedekind::sets::SetObjectLeaf
	A leaf that is a set object, the property over_nodes lifts. More...
struct	dedekind::sets::is_set_object< T >
	A set object: a leaf, or a node over set objects on one domain, by category's over_nodes, the rule its opt-in | and & follow too. More...
struct	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::codomain_reduce< R >
	The codomain leg of the two-axis reduce (#894). More...
struct	dedekind::sets::codomain_reduce< Ø< T, L > >
struct	dedekind::sets::codomain_reduce< 𝔸< T, L, C > >
struct	dedekind::sets::is_extensional< 𝔸< T, L, C > >
struct	dedekind::category::is_transfinite< dedekind::sets::𝔸< T, L, C > >
struct	dedekind::category::is_lattice_bottom_for< dedekind::sets::Ø< T, L >, dedekind::sets::subobject_order< L > >
struct	dedekind::category::is_lattice_top_for< dedekind::sets::𝔸< T, L, C >, dedekind::sets::subobject_order< L > >

Namespaces
namespace	dedekind::sets
namespace	dedekind::category

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::IsSetObjectLeaf
	The leaf case: a set object that carries the subobject surface itself (Definition Lwv) together with its two legs.
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.

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.

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 T, typename L>
constexpr Ø< T, L >	dedekind::sets::materialize_bounds (LatticeBottom< T, subobject_order< L > >)
template<typename T, typename L>
constexpr 𝔸< T, L >	dedekind::sets::materialize_bounds (LatticeTop< T, subobject_order< L > >)
template<typename R>
constexpr R	dedekind::sets::materialize_bounds (R r)
template<typename L = Boole, typename Combine = no_leaf_combine, IsSetObject Node>
constexpr auto	dedekind::sets::subobject_reduce (const Node &node)
	The domain reduce: fold a subobject lattice Node value (a Meet / Join / Not over Sub(T), or a leaf) to its normal-form value under subobject_order<L> through the one reducer (category::Reduce under cata), make an abstract bound concrete, then finalize the codomain leg. The same fold at compile time names the type subobject_reduce_t; at run time it preserves a runtime-stateful operand (a Singleton holding a value) where the normal form is that operand, so it is the entry the Python surface calls. The four Ø / 𝔸 meet & join operators and the free & / | / ~ over IsSetObject (:expressions) all route through here.
template<typename T, typename L, typename S> requires (IsLSet<S> && std::same_as<typename S::Domain, T>)
constexpr auto	dedekind::sets::operator& (const Ø< T, L > &, const S &s)
	Ø & S / Ø | S: Ø is the ⊥ of Sub(T) meeting / joining any set. Free operators (the Ø-LHS members were retired); overload resolution pins them by the Ø operand.
template<typename T, typename L, typename S> requires (IsLSet<S> && std::same_as<typename S::Domain, T>)
constexpr auto	dedekind::sets::operator| (const Ø< T, L > &, const S &s)
	Ø | S = S (⊥ is the join unit); see operator&.
template<typename T, typename L, typename C, typename S> requires (IsLSet<S> && std::same_as<typename S::Domain, T>)
constexpr auto	dedekind::sets::operator& (const 𝔸< T, L, C > &, const S &s)
	𝔸 & S / 𝔸 | S: 𝔸 is the ⊤ of Sub(T) meeting / joining any set. Free operators (the 𝔸-LHS members were retired); pinned by the 𝔸 operand.
template<typename T, typename L, typename C, typename S> requires (IsLSet<S> && std::same_as<typename S::Domain, T>)
constexpr auto	dedekind::sets::operator| (const 𝔸< T, L, C > &, const S &s)
	𝔸 | S = 𝔸 (⊤ is the join annihilator); see operator&.
template<typename S1, typename S2>
constexpr std::size_t	dedekind::sets::bound_meet (const S1 &lhs, const S2 &rhs)
template<typename S1, typename S2>
constexpr std::size_t	dedekind::sets::bound_join (const S1 &lhs, const S2 &rhs)
	ETCS-aligned upper bound for join/union cardinality.

Variables
template<typename T, typename L>
const Ø< T, L >	dedekind::sets::Ø< T, L >::χ {}
template<typename T, IsOckhamAlgebra L, IsCardinality C>
const 𝔸< T, L, C >	dedekind::sets::𝔸< T, L, C >::χ {}
constexpr auto	dedekind::sets::ℕ = 𝔸<Cardinality>{}
	The canonical Natural-numbers universe ℕ = 𝔸<Cardinality> (post-#559).
constexpr auto	dedekind::sets::𝔹 = 𝔸<bool>{}
	𝔹 — the canonical Boolean universe 𝔸<bool>{}, the finite set \(\{\mathtt{false},\mathtt{true}\}\). This is the one symbol downstream code refers to (no partition re-exports or re-aliases it); the carrier is bool and is spelled directly in type positions. Companion to ℕ for the point-free set-builder surface 𝔹 | π == true.
constexpr auto	dedekind::sets::U64 = 𝔸<u64, Boole, Finite>{}
	U64 — the universe over the word, 𝔸<u64>{}: finite by representation, the twin of Python's U64 (A(u64)).
template<typename T, typename L>
constexpr bool	dedekind::category::is_distributive_lattice_for_v< T, dedekind::sets::subobject_order< L > > = true
	The subobject lattice Sub(T) is a distributive lattice under subobject_order<L>, for every carrier T and classifier L. In a topos Sub(T) is a Heyting algebra (meet distributes over join), and the classical (Boole) case is the Boolean specialisation of that. The DNF rewrite, however, acts on the pointwise L::AND / L::OR of the predicates, so its soundness needs those operations to distribute, which the IsOckhamAlgebra shape gate does not certify. So the marker is gated on a species-level distributivity certificate: IsBoundedDeMorganChain<L>. A bounded De Morgan chain is (by chain-normality) a distributive lattice, so its L::AND / L::OR distribute; every shipped species (Boole, Kleene, Chain<T>, Percent) satisfies it, while an unconstrained / non-distributive custom L is excluded (fail-closed). When gated, it licenses the reducer's meet_distributivity_law to rewrite a genuinely non-collapsing Sub(T) meet-over-join into disjunctive normal form (X∧(P∨Q)→(X∧P)∨(X∧Q)). FIXME(#907/#923): replace IsBoundedDeMorganChain with a dedicated species-level distributivity certificate (via the :species-trait bridge) so non-chain distributive logics can also opt in.
template<typename L>
constexpr bool	dedekind::category::is_complemented_lattice_for_v< bool, dedekind::sets::subobject_order< L > >

Detailed Description

The Extremal Identities: Universal (V) and Empty (∅) Sets.

@partition :boundaries

Copyright 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

@dependency dedekind.ontology

boundaries__The_Structural_Limits

In the Dedekind topos, the boundaries of a Species define the 'North and South poles' of the set-lattice. This partition implements the identities required for a Bounded Lattice over any Species:

• 𝔸 (V): The 'Top' (⊤). The extensional whole of a Species.
• EmptySet (∅): The 'Bottom' (⊥). The mereological remainder of the whole.

These sets are the 'First-Class Citizens' of the Mereological System:

1. Self-Awareness: Each boundary knows its 'Ambient Species' (The context).
2. Duality: Each is the other's complement.
3. Identity: They serve as the unit elements for Union (|) and Intersection (&).

boundaries__Semantic_Role

While a Singleton represents an 'Atomic Part', the boundaries represent the 'Absolute State' of the Species. In a 'Family' (A Set of Sets), these objects serve as the terminal bounds of the collection.

Template Parameters

Species	The underlying domain (e.g., Integers, Booleans).
L	The Subobject Classifier (Ω) governing the truth logic.

Wikipedia: Universal set, Empty set, Bounded lattice, Identity element

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

Note

"For us there is no ignorabimus." – David Hilbert, Konigsberg address (1930)