cartesian.cppm File Reference

Cartesian Closed Category (CCC) Foundations. More...

#include <concepts>
#include <cstddef>
#include <cstdlib>
#include <functional>
#include <memory>
#include <ranges>
#include <tuple>
#include <type_traits>
#include <utility>
#include <variant>
import dedekind.category:total;

Include dependency graph for cartesian.cppm:

Classes
struct	dedekind::category::Section< T, Op >
	A binary operation curried, with named arrows throughout (the Jlt paper, Listing 3): curry<T>(op) is \(T \to T^T\), its value at a the operator section \(b \mapsto op(a, b)\), Haskell's (a +), and uncurry takes it back to \(T \times T \to U\). A chain's end and step are such sections: curry<N>(greater_equal<N>{})(unit) stops at the unit, curry<N>(plus<N>{})(1) is the successor. More...
struct	dedekind::category::Curried< T, Op >
	\(T \to T^T\): the operation, one argument at a time. More...
struct	dedekind::category::Uncurried< T, Op >
	\(T \times T \to U\): the curried operation, taken back. More...
struct	dedekind::category::Injections< A, B >
	The injections of the coproduct std::variant<A, B> as a named operation (IsCoproduct's Op, #881): inl / inr place a value by index, so equal summands stay apart (variant<int, int>). Static members, as the concept asks for Op::inl(a) / Op::inr(b). More...
struct	dedekind::category::Injection< K, A, B >
	The injection ι_K : A → A + B as an arrow: monic (it is injective, and its image is disjoint from the other summand's), the ground of a sum's strength reduction (a set inside one injection's image pulls back along it without loss). More...
struct	dedekind::category::detail_arrows::At< T >
	The visitor that applies the active arrow to x. More...
struct	dedekind::category::Sections< T, Op >
struct	dedekind::category::is_associative< Sections< T, Op >, compose >
	Sections under composition are a monoid: composition is associative, total where the operation is, and the identity is its unit. More...
struct	dedekind::category::is_periodic< Sections< T, Op >, compose >
struct	dedekind::category::is_total_by_construction< Sections< T, Op >, compose >
struct	dedekind::category::unit_trait< Sections< T, Op >, compose >
struct	dedekind::category::Morphisms< T, Op >
struct	dedekind::category::Arrows< T, Op >
struct	dedekind::category::detail_arrows_witness::Inc
struct	dedekind::category::SetId< T >
	The Identity morphism for the category Set. More...
struct	dedekind::category::Set< T >
	The Category of C++ Types (Set). Formally reified as a Cartesian Closed Category. More...
struct	dedekind::category::arrow_as_relation< F >
	Adapter: realise an IsArrow F : A → B as a binary relation (a, b) ↦ f(a) == b. More...
struct	dedekind::category::Pairing< F, G >
	⟨f, g⟩ : A → B × C, one argument into a product. More...
struct	dedekind::category::Copairing< F, G >
	[f, g] : A + B → C, case analysis out of a sum. More...
struct	dedekind::category::is_involutive< Flip< A, A >, std::pair< A, A > >

Namespaces
namespace	dedekind::category
namespace	dedekind::category::detail_arrows
	The endomorphisms of T that have a storage class, as three coproducts, each an arrow by case analysis and a coproduct by construction (the Jlt paper, Listing 2).

Concepts
concept	dedekind::category::IsExponential
	Categorical exponential object B^A — generalised structural recogniser of "eval morphism via call expression" (#698 Slice 6).
concept	dedekind::category::IsArrowExponential
	An exponential E : A → B that also satisfies the project's morphism vocabulary (IsArrow with matching Domain / Codomain typedefs). #706.
concept	dedekind::category::IsCoproduct
	Categorification of std::variant<A, B> as the categorical coproduct (A + B).
concept	dedekind::category::detail_arrows_witness::HasSections
concept	dedekind::category::IsCartesianClosed
	A Category equipped with Terminal Objects, Products, and Exponentials.
concept	dedekind::category::IsProductCategory
	A category whose Species is a categorical product (std::pair).
concept	dedekind::category::IsBinaryRelation
	A type R is a binary relation A × B → bool if it is callable on A and B and yields a boolean.
concept	dedekind::category::IsBinaryFunction
	A binary relation R ⊆ A × B is a function when it is left-total AND right-unique.
concept	dedekind::category::IsDirectedGraph
	A homogeneous binary relation R ⊆ V × V on a vertex set V is a directed graph: each ordered pair (u, v) with R(u, v) == true is an edge.
concept	dedekind::category::IsUndirectedGraph
	A directed graph R is undirected when its relation is symmetric: R(u, v) iff R(v, u).
concept	dedekind::category::IsCongruence
	A homogeneous binary relation R on a carrier V is a congruence w.r.t. operation Op when it is an equivalence relation and respects Op.
concept	dedekind::category::HasSubscriptOperator
	Syntactic check: s[i] compiles for Seq, Idx.
concept	dedekind::category::IsEvalArrow
	Seq exposes operator[Idx] and the carrier site has declared it as the CCC eval counit (Mac Lane CWM §IV.6).

Typedefs
template<typename A, typename B>
using	dedekind::category::Exponential
	The Exponential Object B^A (Type Alias).
template<std::size_t K, typename A, typename B>
using	dedekind::category::ι = Injection<K, A, B>
	The injection by its textbook name, \(\iota_K\) (Pierce), as the projection is Π.
using	dedekind::category::detail_arrows_witness::A = Arrows<unsigned>
using	dedekind::category::detail_arrows_witness::M = Morphisms<unsigned>
using	dedekind::category::detail_arrows_witness::S = Sections<unsigned>
template<typename A>
using	dedekind::category::CanonicalSetCCC = Set<A>
	Explicit alias for the canonical ETCS CCC witness over ambient A.
template<IsArrow F, IsArrow G>
using	dedekind::category::ProductArrow
	f × g = ⟨f ∘ π₁, g ∘ π₂⟩ : A × C → B × D.
template<typename A, typename B>
using	dedekind::category::Flip = Pairing<Π<2, std::pair<A, B>>, Π<1, std::pair<A, B>>>
	flip, the symmetry of the cartesian product, \(\sigma_{A,B} : A \times B \to B \times A\): the pairing of the projections the other way round, \(\langle \pi_2, \pi_1 \rangle\). On a square an involution, so an isomorphism, its own inverse; natural in both factors, \(\sigma \circ (f \times g) = (g \times f) \circ \sigma\), the braiding of the cartesian monoidal structure, symmetric. A word of two letters flipped is the word reversed.
template<IsArrow F, IsArrow G>
using	dedekind::category::SumArrow
	f + g = [ι₁ ∘ f, ι₂ ∘ g] : A + C → B + D.
using	dedekind::category::detail_formers_witness::I = Identity<int>
using	dedekind::category::detail_formers_witness::B = Identity<bool>

Functions
template<typename F>
constexpr auto	dedekind::category::exponential (F f)
	Internal Hom Factory (Exponential).
template<typename A, typename F>
constexpr auto	dedekind::category::exponential (F f)
template<typename A, typename B, typename F>
constexpr auto	dedekind::category::exponential (F f)
template<IsArrowFromProduct F>
constexpr auto	dedekind::category::curry (F f)
	Currying: (X × A → B) ⟹ (X → B^A).
template<IsArrow F> requires IsArrow<Cod<F>>
constexpr auto	dedekind::category::uncurry (F f)
	Uncurrying: (X → B^A) ⟹ (X × A → B).
template<typename T, typename Op> requires (!IsArrow<Op>) && std::regular_invocable<const Op&, const T&, const T&>
constexpr Curried< T, Op >	dedekind::category::curry (Op op)
	The operation curried.
template<typename T, typename Op>
constexpr Uncurried< T, Op >	dedekind::category::uncurry (Curried< T, Op > c)
	The inverse of curry<T>.
template<typename A, typename B>
constexpr auto	dedekind::category::ι_1 (A value)
	Left injection ι₁: A → A + B.
template<typename A, typename B>
constexpr auto	dedekind::category::ι_2 (B value)
	Right injection ι₂: B → A + B.
constexpr void	dedekind::category::detail_arrows::refuse_deep_composite ()
	The refusal of a composite of composites: not a constant expression, so the compile-time evaluation that reaches it fails, and at run time the end of the program, since Rule 1 admits no throw.
template<typename T, typename Op>
constexpr Sections< T, Op >	dedekind::category::operator>> (const Sections< T, Op > &f, const Sections< T, Op > &g)
	f >> g on sections: the identity absorbed, two sections one, \((b \mapsto a \cdot b) ; (c \mapsto a' \cdot c) = (b \mapsto (a' \cdot a) \cdot b)\) by associativity, which Sections asks of the operation, with no state, so that both sections are of one operation.
template<typename T, typename Op>
constexpr bool	dedekind::category::detail_arrows::is_identity_tag (const Morphisms< T, Op > &m)
	Whether a morphism is the identity, read off its tags, so that composing asks no == of the carrier.
template<typename T, typename Op>
constexpr Arrows< T, Op >	dedekind::category::operator>> (const Morphisms< T, Op > &f, const Morphisms< T, Op > &g)
	f >> g on morphisms, into Arrows: the identity absorbed, two sections one, two pointers a composite.
template<typename T, typename Op>
constexpr Arrows< T, Op >	dedekind::category::operator>> (const Arrows< T, Op > &f, const Arrows< T, Op > &g)
	f >> g on arrows, restricted to one level: two morphisms compose as above, the identity is absorbed, and a composite of composites is refused.
template<IsArrow F, IsArrow G> requires std::same_as<Cod<F>, Cod<G>>
constexpr auto	dedekind::category::mediate_coproduct (F f, G g)
	Mediating morphism for Coproducts: [f, g]: (A + B) -> X.
template<typename F, typename A> requires IsExponential<F, A, std::invoke_result_t<F, A>>
constexpr auto	dedekind::category::eval (F f, A a)
	The canonical evaluation morphism for the CCC: (B^A × A) → B.
template<typename From, typename To>
constexpr To	dedekind::category::lift (From const &)
	Canonical lift From → To across the carrier lattice — discoverability alias dispatching to the registered bespoke arrow for (From, To).
template<typename A, typename B = A>
constexpr Flip< A, B >	dedekind::category::flip ()
template<IsArrow F, IsArrow G>
constexpr ProductArrow< F, G >	dedekind::category::product_arrow (const F &f, const G &g)
	f × g, built.
template<IsArrow F, IsArrow G>
constexpr SumArrow< F, G >	dedekind::category::sum_arrow (const F &f, const G &g)
	f + g, built.
template<IsArrow F, IsArrow G>
constexpr ProductArrow< F, G >	dedekind::category::operator* (const F &f, const G &g)
	f * g = f × g and f + g = f + g on arrows: the product and coproduct functors' action on arrows, as category theory writes them (Mac Lane, Awodey). A more specific overload keeps its own meaning: a set's * (its cartesian product, the classifier read through ∧), an additive hom-set's + (geometry's function spaces: the sum of parallel arrows, as in an additive category); the term grammar's * + act on terms, which are not arrows.
template<IsArrow F, IsArrow G>
constexpr SumArrow< F, G >	dedekind::category::operator+ (const F &f, const G &g)
template<typename F, typename G>
constexpr auto	dedekind::category::legs (const Pairing< F, G > &a)
	The legs of a former, for cata.
template<typename F, typename G>
constexpr auto	dedekind::category::legs (const Copairing< F, G > &a)

Variables
constexpr auto	dedekind::category::detail_sections_witness::twice = Section<unsigned, std::plus<unsigned>>{{}, 2u}
constexpr auto	dedekind::category::detail_arrows_witness::twice = Section<unsigned, std::plus<unsigned>>{{}, 2u}
constexpr auto	dedekind::category::bounded_pred = [limit = 42](int x) { return x < limit; }
template<typename R>
constexpr bool	dedekind::category::is_left_total_v = false
	User-declared left-totality witness for a binary relation.
template<typename R>
constexpr bool	dedekind::category::is_right_unique_v = false
	User-declared right-uniqueness witness for a binary relation.
template<typename R>
constexpr bool	dedekind::category::is_left_unique_v = false
	Left-uniqueness (injectivity of the relation): each b ∈ B is related to at most one a; R° right-unique. Same opt-in pattern; derived for the relational nodes by the rule table (relational:dyadic, Laws).
template<typename R>
constexpr bool	dedekind::category::is_right_total_v = false
	Right-totality (surjectivity of the relation): every b ∈ B is related to some a; R° left-total. Same opt-in pattern, derived likewise. With the other three: an isomorphism of Rel.
template<typename F>
constexpr bool	dedekind::category::is_left_total_v< arrow_as_relation< F > > = true
template<typename F>
constexpr bool	dedekind::category::is_right_unique_v< arrow_as_relation< F > > = true
template<typename F>
constexpr bool	dedekind::category::is_left_unique_v< arrow_as_relation< F > > = true
template<typename F>
constexpr bool	dedekind::category::is_right_total_v< arrow_as_relation< F > > = true
template<typename...>
constexpr bool	dedekind::category::lift_detail::dependent_false_v = false
	Dependent-false helper for the lift primary's static_assert.
template<typename R, typename T, typename Op>
constexpr bool	dedekind::category::is_congruence_v = false
	User-declared congruence witness: R respects Op on T.
template<typename R, typename V, typename Op>
constexpr bool	dedekind::category::is_congruence_v< R, V, Op > = true
template<typename Seq, typename Idx>
constexpr bool	dedekind::category::is_eval_arrow_v = false
	is_eval_arrow_v<Seq, Idx>: opt-in marker that the carrier's operator[] realises the CCC eval counit. Default false; specialise to true at the carrier site (FinitePath<T>, Vec2V<T>, …) when the subscript-as-eval reading holds.
template<typename F, typename G>
constexpr bool	dedekind::category::is_monic_arrow_v< Pairing< F, G > >
template<typename A, typename F, typename B, typename G>
constexpr bool	dedekind::category::is_monic_arrow_v< Pairing< Compose< A, F >, Compose< B, G > > >
template<typename A, typename F, typename B, typename G>
constexpr bool	dedekind::category::is_epic_arrow_v< Pairing< Compose< A, F >, Compose< B, G > > >
template<typename A, typename F, typename B, typename G, typename LeqA, typename LeqB>
constexpr bool	dedekind::category::is_monotone_v< Pairing< Compose< A, F >, Compose< B, G > >, ProductLeq< LeqA, LeqB > >
template<typename A, typename F, typename B, typename G, typename LeqA, typename LeqB>
constexpr bool	dedekind::category::is_antimonotone_v< Pairing< Compose< A, F >, Compose< B, G > >, ProductLeq< LeqA, LeqB > >
template<typename F, typename G>
constexpr bool	dedekind::category::is_epic_arrow_v< Copairing< F, G > >
template<typename F, typename G, typename X, typename Y>
constexpr bool	dedekind::category::is_monic_arrow_v< Copairing< Compose< F, Injection< 1, X, Y > >, Compose< G, Injection< 2, X, Y > > > >
template<typename F, typename G, typename X, typename Y>
constexpr bool	dedekind::category::is_epic_arrow_v< Copairing< Compose< F, Injection< 1, X, Y > >, Compose< G, Injection< 2, X, Y > > > >

Detailed Description

Cartesian Closed Category (CCC) Foundations.

@partition :cartesian

cartesian__Cartesian

This partition defines the structures required for a category to be Cartesian Closed. In the Dedekind universe, this provides the "Product" and "Function Space" (Exponential) mechanics necessary for ETCS.

cartesian__Std_Namespace_Mappings

This partition asserts bidirectional mappings between the CCC-completing categorical constructs and std types:

Concept	std representative
IsCoproduct	std::variant<A, B> (via ι₁ / ι₂)
IsExponential	std::function<B(A)>, lambdas

Note

The product side — IsProduct for std::pair<A, B>, plus IsProductProjection / IsProjectedProduct / mediate_product / IsArrowFromProduct — moved to :limit under #637, since binary products are categorical limits (limit of a discrete two-object diagram). :cartesian imports :limit, so consumers of the CCC umbrella (IsCartesianClosed) keep reaching the product machinery transitively.

Wikipedia: Cartesian closed category, Exponential object

Copyright

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

Note

"Mathematical science is in my opinion an indivisible whole, an organism whose vitality is conditioned upon the connection of its parts." – David Hilbert, Mathematical Problems (1900)

See also

#319 undergraduate graph theory (work in progress): degree, incidence and multigraphs beside IsDirectedGraph.

Variable Documentation

dependent_false_v

template<typename...>

bool dedekind::category::lift_detail::dependent_false_v = false

inlineconstexpr

Dependent-false helper for the lift primary's static_assert.

Defers false until template instantiation without requiring the parameter types to be complete (unlike sizeof(From) == 0, which would error for incomplete From before emitting the intended diagnostic).