singleton.cppm File Reference

The equality atom: the point {x} as a comprehension over 𝔸<T>. More...

#include <compare>
#include <concepts>
#include <functional>
#include <optional>
#include <type_traits>
#include <utility>
import dedekind.sets:heterogeneous;
import dedekind.category;

Include dependency graph for singleton.cppm:

Classes
struct	dedekind::sets::Point< T >

Namespaces
namespace	dedekind::sets

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

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

Functions
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 > &)

Detailed Description

The equality atom: the point {x} as a comprehension over 𝔸<T>.

@partition :singleton

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

@dependency dedekind.ontology

singleton__The_Singleton_Atom

In the Dedekind universe, the Singleton is the "Unit of Presence." It serves as the canonical implementation of a Pointed Set and provides the concrete singleton constructor used in sets-level monadic workflows.

This structure bridges Level 0a (Species) and Level 1 (Mereology):

• It is Extensional: It exists in memory as a single 'pivot' element.
• It is a Monad: It supports the Kleisli Highway (>>=) via direct application.
• It is a Comonad: It supports the Co-Kleisli Pull (<<=) via extraction (ε).

Category-level η/ε specializations for Singleton are currently deferred while dedekind.sets is being retargeted to the updated functor interfaces in dedekind.category.

singleton__Structural_Role

The Singleton provides the baseline proof for the Unified Highway Bridge. Its sets-layer operations (constructor, bind, extend) are available now; category-layer η/ε and the functor's action F(f) are intentionally postponed to a follow-up integration pass.

Template Parameters

T	The underlying Species of the pivot element.
L	The Subobject Classifier (Ω) governing the set's logic. Defaults to Boole {True, False}.

Wikipedia: Singleton (mathematics), Unit element, Monad (category theory)

Copyright

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

Note

"What is clear and easily comprehended attracts, the complicated repels us." – David Hilbert, Mathematical Problems (1900)