discrete.cppm File Reference

The Discrete Infrastructure (Points as Arrows). More...

#include <algorithm>
#include <concepts>
#include <functional>
import dedekind.category:species;

Include dependency graph for discrete.cppm:

Classes
struct	dedekind::category::ConstantMorphism< A, B >
	The Constant Morphism f: A -> B. More...
struct	dedekind::category::Equals< A >
	The equality test against one value as an arrow \(A \to 2\), the characteristic map of the point x: the condition a guard asks of a state (the Jlt paper's Listing 3, until(equals(1), step)). More...
struct	dedekind::category::DiscreteCategory< T >
	DiscreteCategory realization using the Identity Morphism. Lifts a species T into a category where every arrow is the Identity<T>. More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsDiscreteCategory

Typedefs
template<typename X, typename Y = X>
using	dedekind::category::Constant = ConstantMorphism<X, Y>
	The constant arrow by its short name, the paper's spelling.
using	dedekind::category::IntCat = DiscreteCategory<int>

Functions
template<typename A, typename B>
constexpr auto	dedekind::category::constant (B y)
	The constant arrow's factory, beside id<A>() and endo<A>(f): the domain named, the codomain the value's.
template<std::equality_comparable A>
constexpr Equals< A >	dedekind::category::equals (A x)
	The equality test's factory.

Variables
template<typename A, typename B, typename Op>
constexpr bool	dedekind::category::is_associative_v< ConstantMorphism< A, B >, Op > = true
template<typename A, typename B>
constexpr bool	dedekind::category::is_constant_arrow_v< ConstantMorphism< A, B > > = true

Detailed Description

The Discrete Infrastructure (Points as Arrows).

@partition :discrete

Copyright

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

This partition reifies the simplest possible categorical structure: the Discrete Category, where the only morphisms are identities. In our structuralist framework, this provides the "Point" (1) and the "Empty" (0) objects, as well as the means to treat any species element as a constant mapping.

discrete__The_Discrete_Duality

While Level 0 (:morphism) provides the syntax of the Arrow, Level 0.25 provides the "Discrete Points" that populate the objects:

• One (1) : The Terminal Object; the categorical "Atom" of Truth.
• Zero (0) : The Initial Object; the categorical "Atom" of Falsehood.
• ConstantMorphism : A mapping that factors through the Terminal Object, collapsing the domain into a single point.

discrete__Role_in_the_Fractal

By establishing the Discrete Floor here, we enable Level 0.5 (:limit) to define universal properties (Initiality/Terminality) and Level 1 (:total) to define algebraic identities (Zero/Unit) without circular dependencies.

Note

「三十輻，共一轂，當其無，有車之用。」 (Thirty spokes meet at a single hub; it is the empty space (the relation) that makes the wheel useful.) — 老子 (Laozi)

See also

#275 nLab algebra/category hierarchy (work in progress): the groupoid beside IsDiscreteCategory.