Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
topoi.cppm File Reference
module dedekind.category

The Internal Logic of the Topos. More...

#include <concepts>
#include <functional>
#include <type_traits>
#include <utility>
import dedekind.category:lattice;
Include dependency graph for topoi.cppm:

Classes

struct  dedekind::category::detail::topo_demo_arrow
struct  dedekind::category::detail::topo_demo_bool_arrow
struct  dedekind::category::detail::topo_demo_sieve
struct  dedekind::category::detail::topo_bad_sieve_codomain_mismatch
struct  dedekind::category::detail::topo_demo_topology
struct  dedekind::category::detail::topo_projection_arrow
struct  dedekind::category::detail::topo_bundle_witness
struct  dedekind::category::Subobject< A, Chi >
 The Subobject Species S ↣ A. More...
struct  dedekind::category::Subobject< A, Chi >::Member
 The Internal Member of the Subobject. Wraps a value from the ambient space that satisfies the classifier. More...
struct  dedekind::category::builds_lattice_nodes< Subobject< A, Chi > >
 Subobjects opt in to the lattice's | and & (:lattice): the meet and join of two subobjects of A are the pointwise meet and join of their characteristic arrows ( \(\mathrm{Sub}(A) \cong \mathrm{Hom}(A, \Omega)\)), the lattice's own nodes over them, nested terms included. A subobject is a set object too; opted in, it is the lattice's, not the set grammar's (builds_lattice_nodes). More...

Namespaces

namespace  dedekind::category

Concepts

concept  dedekind::category::IsClassifierConstant
concept  dedekind::category::IsPredicate
 The Predicate Morphism: the DSL's membership test, i.e. the characteristic arrow \(\chi_A : A \to \Omega\).
concept  dedekind::category::IsCharacteristic
 Categorical alias for a Predicate mapping to Ω: the characteristic arrow \(\chi_A : A \to \Omega\) that classifies a subobject (a set).
concept  dedekind::category::IsDecidableCharacteristic
 The Boolean refinement of IsCharacteristic: a membership test valued in the dominance Σ, i.e. \(\chi_A : A \to \Sigma\) with \(\Sigma = \Omega\)-decided \(= @c bool\).
concept  dedekind::category::IsDominanceInclusion
 The Rosolini inclusion arrow \(\iota : \Sigma \hookrightarrow \Omega\): a map between truth-objects out of the decided fragment.
concept  dedekind::category::IsSieve
 Signature-level witness for a sieve of arrows into an object.
concept  dedekind::category::IsGrothendieckTopology
 Signature-level witness for Grothendieck coverage rules over sieves.
concept  dedekind::category::IsBundleProjection
 A projection morphism π : E -> B for a bundle candidate.
concept  dedekind::category::IsFiberBundle
 Signature-level witness for a fiber bundle over a base species.
concept  dedekind::category::IsSubobject
 The categorical witness of a monomorphism ι: S ↣ A — a characteristic morphism χ: A → Ω together with its inclusion.
concept  dedekind::category::IsLSet
 An L-set: a subobject of a carrier with \(\chi : X \to L\) into a named bounded chain \(L\) (Codomain = L::Ω). The carrier is asked for copies (std::semiregular), not for a decidable ==: the equality of sets is the Rice cycle (#970), not a trait of the carrier, so the relations of a hom-set are a carrier too (𝔸<RelExpr>, #1045). An ETCS set asks decidable equality itself (IsSet, whose classifier construction needs it), as IsArrow asks an archetype of its domain rather than a value type (archetype_t). Pst is asked of the species (an Ockham algebra whose Ω is totally ordered), not of the bare Ω, so a Chain<int> set (Ω = int) qualifies while a bare int never does. The chain is the registered total order (IsTotalOrder: reflexive, transitive, antisymmetric, comparable), not the syntactic std::totally_ordered, so an Ω without certified order laws (a raw float, whose NaN breaks reflexivity) is refused honestly.
concept  dedekind::category::IsFiniteChain
 A carrier that is a finite chain by its representation: totally ordered and either a machine integer or an enumeration (both finite by construction). bool, Ternary, int qualify; Cardinality and the dense carriers do not.
concept  dedekind::category::IsFiniteLSet
 The Pst fragment: an L-set whose carrier is a finite chain (IsFiniteChain), so χ is a finite table and normalisation by evaluation is complete. Products of finite chains follow with IsProduct.
concept  dedekind::category::IsQuotient
 The categorical witness of a regular epimorphism q: A ↠ Q — the dual of IsSubobject.
concept  dedekind::category::IsPredicatePair
 Two predicates over one object, answering in one species: the operand sort of the predicate combinators below, which close on IsPredicate. Named so the set grammar's && / || (sets) can take exactly the other pairs of terms (relational fragments, mixed terms, the structured collapse) without overlapping these.

Typedefs

template<typename A, typename L = Boole>
using dedekind::category::PowerObject = Exponential<A, typename L::Ω>
 Power Object Alias.

Functions

template<typename OmegaTarget, typename L, typename Constant>
requires std::same_as<std::remove_cvref_t<Constant>, OmegaTarget> || requires(const std::remove_cvref_t<Constant>& c) { { lift_logic<L>(c) } -> std::same_as<OmegaTarget>; }
constexpr auto dedekind::category::lift_classifier_constant (Constant value)
 Lift a classifier constant into a predicate's Ω: the identity when it is already there, else the dominance lift lift_logic into the predicate's species L (true into Ternary, Ternary::Unknown into Percentage, true onto Chain<int>'s top, ...). The species is passed, not read off OmegaTarget, so a species-tagged predicate whose Ω is no truth object on its own (int) still lifts. Constrained, so a pair with no registered embedding fails the combinators' gate, not this body.
template<typename A, typename F>
requires (!IsArrow<std::remove_cvref_t<F>>) && std::invocable<std::decay_t<F>, const A&> && IsΩ<std::invoke_result_t<std::decay_t<F>, const A&>>
constexpr auto dedekind::category::classify (F f)
 Characteristic Morphism Factory (classify) Returns the Subobject Species (The Body) carrying the rule (The Arrow).
template<typename F>
requires (!IsArrow<std::remove_cvref_t<F>>) && requires { typename signature_extractor<std::decay_t<F>>::type; } && IsΩ<codomain_t<std::decay_t<F>>>
constexpr auto dedekind::category::classify (F f)
 Domain-inferring classify: deduces A from the callable's signature.
template<typename A, IsArrow F>
requires IsPredicate<F> && std::same_as<Dom<F>, A>
constexpr auto dedekind::category::classify (F f)
 Idempotent classify: Passthrough for existing Arrows.
template<typename P, typename Q>
requires IsPredicatePair<P, Q>
constexpr auto dedekind::category::operator&& (P p, Q q)
 Logical Conjunction (Intersection): Synthesizes a rule for A ∩ B.
template<IsClassifierConstant C, IsPredicate P>
requires (!IsPredicate<std::remove_cvref_t<C>>) && requires(C c) { lift_classifier_constant<Cod<P>, predicate_logic_t<P>>(c); }
constexpr auto dedekind::category::operator&& (C constant, P p)
 Conjunction of a constant logical value with a predicate.
template<IsPredicate P, IsClassifierConstant C>
requires (!IsPredicate<std::remove_cvref_t<C>>) && requires(C c) { lift_classifier_constant<Cod<P>, predicate_logic_t<P>>(c); }
constexpr auto dedekind::category::operator&& (P p, C constant)
 Conjunction of a predicate with a constant logical value.
template<typename P, typename Q>
requires IsPredicatePair<P, Q>
constexpr auto dedekind::category::operator|| (P p, Q q)
 Logical Disjunction (Union): Synthesizes a rule for A ∪ B.
template<IsClassifierConstant C, IsPredicate P>
requires (!IsPredicate<std::remove_cvref_t<C>>) && requires(C c) { lift_classifier_constant<Cod<P>, predicate_logic_t<P>>(c); }
constexpr auto dedekind::category::operator|| (C constant, P p)
 Disjunction of a constant logical value with a predicate.
template<IsPredicate P, IsClassifierConstant C>
requires (!IsPredicate<std::remove_cvref_t<C>>) && requires(C c) { lift_classifier_constant<Cod<P>, predicate_logic_t<P>>(c); }
constexpr auto dedekind::category::operator|| (P p, C constant)
 Disjunction of a predicate with a constant logical value.
template<IsPredicate P>
constexpr auto dedekind::category::operator! (P p)
 Logical Negation (Complement): Synthesizes a rule for ¬A.
template<typename A, typename P, typename Q>
requires std::invocable<const std::decay_t<P>&, const A&> && std::invocable<const std::decay_t<Q>&, const A&> && IsΩ<std::remove_cvref_t< std::invoke_result_t<const std::decay_t<P>&, const A&>>> && std::same_as< std::remove_cvref_t< std::invoke_result_t<const std::decay_t<P>&, const A&>>, std::remove_cvref_t< std::invoke_result_t<const std::decay_t<Q>&, const A&>>>
constexpr auto dedekind::category::predicate_and (P p, Q q)
 Compose two plain callable predicates over a declared domain A.
template<typename A, typename P, typename Q>
requires std::invocable<const std::decay_t<P>&, const A&> && std::invocable<const std::decay_t<Q>&, const A&> && IsΩ<std::remove_cvref_t< std::invoke_result_t<const std::decay_t<P>&, const A&>>> && std::same_as< std::remove_cvref_t< std::invoke_result_t<const std::decay_t<P>&, const A&>>, std::remove_cvref_t< std::invoke_result_t<const std::decay_t<Q>&, const A&>>>
constexpr auto dedekind::category::predicate_or (P p, Q q)
 Disjunction bridge for plain callable predicates over domain A.
template<typename A, typename P>
requires std::invocable<const std::decay_t<P>&, const A&> && IsΩ<std::remove_cvref_t< std::invoke_result_t<const std::decay_t<P>&, const A&>>>
constexpr auto dedekind::category::predicate_not (P p)
 Negation bridge for plain callable predicates over domain A.
template<typename A, typename L = Boole>
requires IsOckhamAlgebra<L>
constexpr auto dedekind::category::constant_classifier (typename L::Ω value)
 Constant classifier factory over domain A: A -> Ω.
template<typename A, typename L = Boole>
requires IsOckhamAlgebra<L>
constexpr auto dedekind::category::classifier_true ()
 The tautology / top predicate \(\top\) over domain A: the canonical always-true classifier A → Ω, constant at L::True. This is the topos truth arrow \(\top: 1 \to \Omega\) pulled back to a predicate on A (verum, "everything is a member"); use it wherever a whole-domain / unrestricted characteristic map is wanted rather than an ad-hoc [](const A&){ return true; } lambda.
template<typename A, typename L = Boole>
requires IsOckhamAlgebra<L>
constexpr auto dedekind::category::classifier_false ()
 The contradiction / bottom predicate \(\bot\) over domain A: the canonical always-false classifier A → Ω, constant at L::False (falsum, "nothing is a member"). Dual of classifier_true.
template<typename A, typename L = Kleene>
requires IsOckhamAlgebra<L> && requires { L::Unknown; }
constexpr auto dedekind::category::classifier_unknown ()
 Default unknown classifier over domain A (only for logics with Unknown).
template<typename L = Boole>
requires IsOckhamAlgebra<L>
constexpr auto dedekind::category::logical_true ()
 The 'true' morphism: 1 → Ω.
template<typename L = Boole>
requires IsOckhamAlgebra<L>
constexpr auto dedekind::category::logical_false ()
 The 'false' morphism: 1 → Ω.

Detailed Description

The Internal Logic of the Topos.

@partition :topoi

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

@quote "Grothendieck has made the category (rather than the space) the central aspect that we should explicitly axiomatise." — Myles Tierney

topoi__The_Subobject_Classifier

The Lawvere-Tierney object Ω (Omega) is the central object that classifies subobjects. Every elementary topos carries an internal logic which generalizes standard set theory into objective categorical form.

Textbook defaults in this partition:

  • operator&& models meet/intersection of characteristic predicates.
  • operator|| models join/union of characteristic predicates.
  • operator! models complement.

Wikipedia: Lawvere–Tierney topology, Subobject classifier, Topos

See also
Lawvere (1964), An elementary theory of the category of sets.
Lambek & Scott (1988), Introduction to Higher-Order Categorical Logic.
Note
"BUDOWANE JEST MNIEJ DOSKONALE OD BUDUJACEGO." ("What is built is less perfect than what builds it.") – Stanislaw Lem, GOLEM XIV