limit.cppm File Reference

Universal Limits: boundary objects (Initial and Terminal) and binary products. More...

#include <concepts>
#include <cstddef>
#include <exception>
#include <functional>
#include <tuple>
#include <type_traits>
#include <utility>
#include <variant>
import dedekind.category:morphism;

Include dependency graph for limit.cppm:

Classes
struct	dedekind::category::Projection< K >
	The projection π_k: the k-th component of a product. More...
struct	dedekind::category::Projection< 0 >
	The projection out of the one-fold product A¹ ≅ A: the identity arrow (Identity), read at the point's own type. More...
struct	dedekind::category::detail_limit::ProjectionAt< K, P >
struct	dedekind::category::detail_limit::projection_arrow< K, P >
struct	dedekind::category::detail_limit::projection_arrow< 0, P >
struct	dedekind::category::AnyOperation
	Base-case sentinel for the operation parameter of IsProduct / IsCoproduct. More...
struct	dedekind::category::SpeciesTraits< std::pair< A, B > >
struct	dedekind::category::SpeciesTraits< std::tuple< Ts... > >
struct	dedekind::category::detail::TerminalEnvelope
struct	dedekind::category::detail::InitialEnvelope
struct	dedekind::category::detail::DrillDown
	The opt-in operator-> drill-down policy: the projector the projected-object concepts take, by name rather than as a lambda. More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsMorphicTotal
	A Morphism whose Codomain is the Terminal Object (One).
concept	dedekind::category::IsTerminalMorphism
	A morphism that maps into the Terminal Object (One).
concept	dedekind::category::IsTerminalObject
	A type that plays the role of a terminal object — either the canonical global One (std::monostate, the unique terminal of the ambient category of sets) or an opt-in structural witness via the is_terminal_object_tag typedef.
concept	dedekind::category::IsBoundaryProjection
	Projection witness from an owning/wrapper whole to a boundary object.
concept	dedekind::category::IsProjectedTerminalObject
	Terminal-object witness through an optional projection policy.
concept	dedekind::category::HasUniqueMorphismTo
	Asserts that there exists a unique morphism from T to U = One.
concept	dedekind::category::HasUniqueMorphismFrom
	Asserts that there exists a unique (unreachable) morphism from Z = Zero to T.
concept	dedekind::category::IsInitialObject
	A type that plays the role of an initial object — either the canonical global Zero (std::nullptr_t, the unique initial of the ambient category of sets) or an opt-in structural witness via the is_initial_object_tag typedef.
concept	dedekind::category::IsBoundaryObject
	A type at a lattice / category bound: an initial object (⊥) or a terminal object (⊤).
concept	dedekind::category::IsProjectedInitialObject
	Initial-object witness through an optional projection policy.
concept	dedekind::category::TupleLike
concept	dedekind::category::detail_limit::HasIndependentComponents
	A point whose components are stored independently, every value of one beside every value of the others: a tuple, a pair-like product, or a carrier that says so. Not a fibred product's point, whose components are read off one value.
concept	dedekind::category::IsPairProjection
	Whether F is the projection \(\pi_K\) out of a pair: the recogniser the law readers (:cartesian, a product's defining form) and the hyperdoctrine (relational:graph) read. A genuine std::pair only: a pair-like carrier with more state is no product of its two members.
concept	dedekind::category::IsProduct
	Categorification of std::pair<A, B> as the categorical product (A × B).
concept	dedekind::category::IsArrowProduct
	An IsProduct whose projections are genuine MORPHISMS (arrows), not merely the structural callables IsProduct checks.
concept	dedekind::category::IsProductProjection
	Functional-part projection witness from a product whole to one part.
concept	dedekind::category::IsProjectedProduct
	Product witness through an optional whole-projection policy.
concept	dedekind::category::IsArrowFromProduct
	Matches an Arrow whose Domain is a categorical Product (std::pair).
concept	dedekind::category::IsProductParthood
	Bridge: a product P with parts A and B IS a mereological parthood in the projection-access reading.
concept	dedekind::category::IsCartesian
	A small category equipped with a terminal object 1 and binary products × — a "cartesian category" in the textbook sense (Pierce, Basic Category Theory for Computer Scientists §1.4; Awodey).

Typedefs
using	dedekind::category::One = std::monostate
	The Terminal Object (1): the unique sink of every morphism.
using	dedekind::category::Zero = std::nullptr_t
	The Initial Object (0): the unique source of every morphism.
template<std::size_t K>
using	dedekind::category::At = std::integral_constant<std::size_t, K>
	The projections π_k out of a product, one family: π_1, π_2 (Pierce, Basic Category Theory for Computer Scientists §1.4), π_3 and π_<k> for a flat n-ary product, and π for the one-fold product A¹ ≅ A, whose projection is the identity.
template<std::size_t K, typename P>
using	dedekind::category::Π = typename detail_limit::projection_arrow<K, P>::type
	π_k read at the product P, as a MORPHISM (Domain = P, Codomain the k-th part): the building block of IsArrowProduct. Π<0, P> is Identity
using	dedekind::category::TerminalCategory = DiscreteCategory<One>
using	dedekind::category::InitialCategory = DiscreteCategory<Zero>

Functions
template<typename T>
constexpr auto	dedekind::category::bang ()
	The terminal map factory: produces the unique arrow !: T → One.
template<typename T>
constexpr auto	dedekind::category::zero ()
	The zero morphism factory: produces the unique (unreachable) arrow ?: Zero → T.
template<typename P, std::size_t K> requires TupleLike<P> && (K >= 1) && (K <= std::tuple_size_v<P>)
constexpr auto	dedekind::category::component (const P &p, At< K >)
	The k-th component of a tuple-like product, by reference: a projection reads its point without copying it (a string or vector carrier stays where it is). π_k returns a temporary's component by value.
template<typename P> requires (!TupleLike<P>) && requires(const P& p) { p.first; }
constexpr auto	dedekind::category::component (const P &p, At< 1 >)
	The components of a pair-like product that is not tuple-like.
template<typename P> requires (!TupleLike<P>) && requires(const P& p) { p.second; }
constexpr auto	dedekind::category::component (const P &p, At< 2 >)
template<IsArrow F, IsArrow G> requires std::same_as<Dom<F>, Dom<G>>
constexpr auto	dedekind::category::mediate_product (F f, G g)
	Mediating morphism for Products: ⟨f, g⟩: X -> (A × B).

Variables
constexpr Projection< 0 >	dedekind::category::π {}
	The unary projection, the identity: the variable of a comprehension over one carrier.
constexpr Projection< 1 >	dedekind::category::π_1 {}
	The projections of a pair (and the first three of a tuple).
constexpr Projection< 2 >	dedekind::category::π_2 {}
constexpr Projection< 3 >	dedekind::category::π_3 {}
template<std::size_t K>
constexpr Projection< K >	dedekind::category::π_ {}
	The family: π_<k> is the k-th projection of a flat product.
template<std::size_t K, typename P>
constexpr bool	dedekind::category::is_epic_arrow_v< detail_limit::ProjectionAt< K, P > > = true
	A projection of a product is epic, inferred from the point's shape: with independent components, every value of the component is attained, the others being any value of their types, which are inhabited (semiregular). It is not monic, since it forgets the others; the Jlt paper's Listing 1 shows it beside its section.
template<std::size_t K, typename P>
constexpr bool	dedekind::category::is_monic_arrow_v< detail_limit::ProjectionAt< K, P > > = true
	A projection whose components are inclusions is monic: the point is one value, each component that value seen in a part, as a pullback apex's legs are (:pullback). Inferred from the point's own declaration.

Detailed Description

Universal Limits: boundary objects (Initial and Terminal) and binary products.

@partition :limit

Copyright

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

@quote "The progress of mathematics can be viewed as progress from the infinite to the finite." — Gian-Carlo Rota, Indiscrete Thoughts

limit__Limits

In the Dedekind topos, the Initial (0) and Terminal (1) objects represent the finite "anchors" of a system of otherwise infinite potential relations. They are the unique sinks and sources through which the structure of every other species is measured and made finite.

limit__Std_Namespace_Mappings

This partition asserts bidirectional mappings between categorical limit constructions and std types:

Concept / Alias	std representative	Categorical role
One (Terminal)	std::monostate	Unique sink (1)
Zero (Initial)	std::nullptr_t	Unique source (0)
IsProduct	std::pair<A, B>	Binary product (A × B)

Note

"This conviction of the solvability of every mathematical problem is a powerful incentive to the worker. We hear within us the perpetual call: There is the problem. Seek its solution." – David Hilbert, Mathematical Problems (1900)