Elementary Theory of the Category of Sets (ETCS) facade. More...

#include <algorithm>
#include <concepts>
#include <functional>
#include <memory>
#include <ranges>
#include <set>
#include <type_traits>
#include <unordered_set>
#include <utility>
import dedekind.category:logic;

Include dependency graph for etcs.cppm:

Classes
struct	dedekind::category::detail_etcs_total_witness::NonRegular
struct	dedekind::category::detail_etcs_total_witness::SetOverNonRegular
struct	dedekind::category::detail_etcs_total_witness::SetOverNonRegular::Member

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::HasAxiom1Composition
	ETCS axiom 1 witness: composition is available for ambient arrows.
concept	dedekind::category::HasAxiom2Identity
	ETCS axiom 2 witness: identity arrow acts neutrally on A.
concept	dedekind::category::HasAxiom3TerminalObject
	ETCS axiom 3 witness: terminal object 1 is present.
concept	dedekind::category::HasAxiom4WellPointedness
	ETCS axiom 4 witness: membership is evaluation through the carrier-as-characteristic-morphism. Post-#681 structural refactor: `IsSubobject` already requires the structural call shape `{` s(a) } `->` `IsΩ`, so the membership-as-evaluation reading lands on the `IsSubobject` witness itself.
concept	dedekind::category::HasAxiom5CartesianProduct
	ETCS axiom 5 witness: products exist for ambient species A.
concept	dedekind::category::HasAxiom6Exponentiation
	ETCS axiom 6 witness: exponentials B^A exist (here A^A witness). Uses the named `IsArrowExponential` refinement (#706) rather than the ad hoc `IsExponential` `&&` `IsArrow` combination that lived here previously.
concept	dedekind::category::HasAxiom7SubobjectClassifier
	ETCS axiom 7 witness: every set is represented by a subobject.
concept	dedekind::category::HasAxiom7ClassifierNaturalityWitness
	Optional naturality witness for Axiom 7 classifier behavior.
concept	dedekind::category::HasAxiom8EmptySet
	ETCS axiom 8 witness: initial object 0 is present.
concept	dedekind::category::HasAxiom9NNO
	ETCS axiom 9 witness: arithmetic species atlas exposes ℕ witness.
concept	dedekind::category::IsSplitEpicPair
	Structural witness of a split epimorphism e with section s.
concept	dedekind::category::HasAxiom10ChoiceSplitEpicWitness
	Axiom 10 (choice) support via an explicit split-epi witness shape.
concept	dedekind::category::HasAxiom10ChoiceSplitEpicLawSurface
	Axiom 10 semantic-law surface (split-epi shape + equality codomain).
concept	dedekind::category::HasAxiom7PullbackReindexingDefinitionalSurface
	Axiom 7 definitional reindexing witness surface.
concept	dedekind::category::HasAxiom10PowerObjectLattice
	ETCS axiom 10 witness: power-object lattice completeness.
concept	dedekind::category::HasETCSAxioms
	Diaconescu's classical direction (#698 Slice 9 review).
concept	dedekind::category::IsSet
	ETCS set: a carrier satisfying the 10 ETCS axioms AND admitting the canonical Set-CCC witness over its ambient species.

Typedefs
template<typename S>
using	dedekind::category::discrete_lift_t = DiscreteCategory<S>

Functions
template<typename Epi, typename Section> requires IsSplitEpicPair<Epi, Section> && std::equality_comparable<Cod<Epi>>
constexpr bool	dedekind::category::split_epi_section_law_at (const Epi &epi, const Section &section, const Cod< Epi > &b)
	Law check for split epimorphisms at a concrete codomain element.
template<typename S, IsArrow E> requires IsSubobject<S, typename S::Domain> && std::same_as<Cod<E>, typename S::Domain> && std::equality_comparable< std::invoke_result_t<S const&, typename S::Domain const&>>
constexpr bool	dedekind::category::classifier_reindexing_definitional_witness_at (const S &s, const E &embedding, const Dom< E > &x)
	Definitional witness check for Axiom 7 reindexing through embedding.
template<typename A, typename Pred> requires IsSpecies<A> && std::invocable<std::decay_t<Pred>, const A&> && IsΩ<std::invoke_result_t<std::decay_t<Pred>, const A&>>
constexpr auto	dedekind::category::ambient_set (Pred predicate)
	Construct a set object over ambient species A from a characteristic predicate.
template<typename T, typename Hash, typename Equal, typename Alloc> requires IsSpecies<T>
constexpr auto	dedekind::category::ambient_set (std::unordered_set< T, Hash, Equal, Alloc > s)
	Lift `std::unordered_set<T, ...>` into an IsSet object, by value: the container is boxed, the lifted Subobject a value. (#607 slice 1, #1061).
template<typename T, typename Compare, typename Alloc> requires IsSpecies<T>
constexpr auto	dedekind::category::ambient_set (std::set< T, Compare, Alloc > s)
	Lift `std::set<T, ...>` into an IsSet object, by value: the container is boxed, the lifted Subobject a value. (#607 slice 1, #1061).
template<std::ranges::forward_range R> requires IsSpecies<std::ranges::range_value_t<R>> && (!requires(R& r, std::ranges::range_value_t<R> x) { r.contains(x); })
constexpr auto	dedekind::category::ambient_set (R r)
	Lift any `std::ranges::input_range` (a view, span, or container) into an `IsSet` object by wrapping `std::ranges::find` as the membership test. This is the Jlt-clean reading of a set — the set is its membership test — carried down to the `std::ranges` layer: a lazy view is a first-class `IsSet`, and it is `constexpr` where `std::unordered_set` (not constexpr-constructible with contents) is not. Excludes the keyed containers above by refusing a .contains() member, so those more specific overloads still win. The range is moved into the predicate (a view is cheap to own; the lifted Subobject carries its own copy). (#607 — the range slice of the wrapper-dissolution plan.).

Detailed Description

Elementary Theory of the Category of Sets (ETCS) facade.

@partition :etcs

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

This partition lifts topoi-level subobject operations into a focused ETCS set interface. In this codebase, a "set" is represented as a subobject classified by a characteristic morphism χ: A → Ω.

etcs__ETCS_Axiom_Mapping

The following table maps each of the 10 axioms of Lawvere's ETCS to the corresponding C++23 implementation. Items marked (asp.) are aspirational.

ETCS Axiom	C++23 Implementation
1. Composition	operator>> / IsArrow
2. Identity	Identity<T> / id<T>()
3. Terminal Object (1)	One (std::monostate)
4. Well-Pointedness	s.χ(x) → Ω (global element eval)
5. Cartesian Product	std::pair / IsProduct
6. Exponentiation (B^A)	Exponential<A,B> / IsExponential
7. Subobject Classifier	Subobject<A,χ> / classify<A>(p)
8. Empty Set (∅)	Zero (std::nullptr_t)
9. NNO (ℕ)	IsNNO<Cardinality,z,s> (natural)
10. Axiom of Choice (asp.)	meet / join power-object lattice

Note: Row 9 is a witness of the NNO role, not an equality. The genuine witness (carrying a zero and a successor) is IsNNO<Cardinality, ZeroElement<Cardinality>, Successor<Cardinality>> in :numbers (natural.cppm), also reachable via :sets:cardinality (IsCountable). unsigned is only a finite carrier stand-in: SpeciesTraits<unsigned> supplies the Domain / machine_type, not a zero or successor, and it is bounded with an overflow Sollbruchstelle, whereas ℕ is countably infinite. Even Cardinality is an approximation (it carries an ℵ_0 point beyond the textbook NNO). Read "NNO (ℕ)" as the categorical role, never as "@c unsigned @c = ℕ".

etcs__What_Concreteness_Pins

:small establishes the cardinality reading of "small category": the collection of objects and the collection of arrows are each sets in the metatheory. :concrete (re-homed from this partition under #636) pins the ontological reading: each object is a set, equivalently a faithful forgetful functor U : 𝒞 → Set.

Concept-as-predicate framing (cf. paper §2.3). The chain ranges over CATEGORIES C, not over set objects: among small categories, the concrete ones (a faithful U: C→Set) contain the category Set itself, the one satisfying all 10 ETCS axioms.

IsSmallCategory<C>      ⊇    IsConcrete<C>      ⊇    C = Set (ETCS)
(size axis: small)       (ontology: objects-are-   (full ETCS
                         sets; faithful U: C→Set)   axiomatisation)

Warning: Do not read this as IsSet ⟹ IsSmallCategory . The concept IsSet is a predicate on a set OBJECT A (a carrier with a classifier), not on a category: an individual set is an object of Set (Lawvere), categorified only via the discrete embedding Disc: Set ↪ Cat. Accordingly IsSet requires the categorical axioms of CanonicalSetCCC<A::Domain> (the Set-witness over the carrier), never IsSmallCategory of the set object itself.

The IsSubobject / IsConcrete concreteness CONCEPTS live in :concrete; this partition imports it and adds the ETCS-specific axiom witnesses on top. Membership in / in_via lives in :concrete (χ-evaluation); the set-lattice operations are the operators operator& / | / ! in dedekind.sets.

See also: Lawvere, F.W. (1964) "An Elementary Theory of the Category of Sets"; McLarty, C. (1993) "Numbers can be just what they have to"

Note: "In the mathematical development of recent decades, the notion of set has not only played a fundamental role, but it has itself passed through a long process of refinement." — F. William Lawvere, "An Elementary Theory of the Category of Sets"

Classes

Namespaces

Concepts

Typedefs

Functions

Detailed Description

etcs__ETCS_Axiom_Mapping

etcs__What_Concreteness_Pins