The Natural Numbers Object — Lawvere's ETCS Axiom 9 — and the upstream home of Peano recursion / primitive recursion / the Peano successor (categorical idiom + textbook synonyms below). More...

#include <algorithm>
#include <concepts>
#include <cstddef>
#include <cstdint>
#include <functional>
#include <limits>
#include <optional>
#include <type_traits>
#include <utility>
import dedekind.category:morphism;

Include dependency graph for nno.cppm:

Classes
struct	dedekind::category::Successor< N >
	The successor \(S : N \to N\) as an arrow, over any carrier with the NNO step: the one spelling of the Peano successor where an `IsArrow` is needed (`image`, `graph`, the NNO witness), in place of a struct per site. More...
struct	dedekind::category::ZeroElement< N >
	The zero element \(Z : 1 \to N\), the nullary `IsNNO` witness: the carrier's default value, which is the NNO's zero for the integrals and for `Cardinality`. Nullary, so not an `IsArrow` (that concept asks for a `Domain`); a composable \(1 \to N\) arrow is not needed here. More...
struct	dedekind::category::Predecessor< N >
	The predecessor \(P : N \to N\) as an arrow, in the carrier's own posture at ⊥: the monus on ℕ (0 a fixpoint), `−1` on ℤ. More...
struct	dedekind::category::In< N >
	The NNO's structure map \([Z, S] : 1 + N \to N\) as an arrow: zero, or the successor of the element given. `std::optional<N>` is \(1 + N\), the NNO's own functor \(F(X) = 1 + X\). More...
struct	dedekind::category::Prior< N >
	The destructor \(\langle \text{is}\;Z?,\, P\rangle : N \to 1 + N\): nothing at zero, else the predecessor. More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsNNO
	Structural shape: (N, Z, S) is a Natural Numbers Object — `Z` is the zero element `1` `→` `N`, `S` is the successor map `N` `→` `N`.
concept	dedekind::category::HasNNOStep
	A carrier with both NNO steps available: the shape a value-determined point collapse needs (`succ(lo)` `==` `pred(hi)`).

Functions
template<std::integral T>
constexpr T	dedekind::category::successor (T n) noexcept
	The successor arrow as a free customization point: `successor(n)` for an NNO carrier, and its partial dual `predecessor(n)`.
template<std::integral T>
constexpr T	dedekind::category::predecessor (T n) noexcept
template<typename T> requires requires(const T& n) { { T::successor(n) } -> std::convertible_to<T>; }
constexpr T	dedekind::category::successor (const T &n)
	Bridge to the :morphologies static-member convention.
constexpr bool	dedekind::category::predecessor (bool) noexcept
constexpr std::byte	dedekind::category::successor (std::byte b) noexcept
	The octets' covering step: `std::byte's` order read as a chain, the next byte, saturating at the top. No arithmetic, only the step, so a byte chain is a chain and no integer chain.
constexpr std::byte	dedekind::category::predecessor (std::byte b) noexcept
template<HasNNOStep N> requires std::equality_comparable<N>
constexpr std::optional< N >	dedekind::category::cover (const N &n)
	The cover \(S^{+} : N \to 1 + N\) (y covers x: x < y, nothing between, Davey and Priestley [3], ch. 1): the successor read partially, `nullopt` at a fixpoint of `S`, which on a saturating bounded chain is its top (ℵ₀ on `Cardinality`, `True` on K₃), and at a machine word's greatest value, where `S` has no value (signed) or wraps (unsigned: the ring ℤ/2^w under `S`, the chain 0 < 1 < … < 2^w − 1 under its cover); total on an unbounded chain. Whether the step itself is monotone is the arrow's fact (`IsMonotone<Successor<N>>`, registered in `order:completeness` from the carrier's periodicity), not the carrier's. `std::optional<N>` is \(1 + N\), the NNO's own functor \(F(X) = 1 + X\).
template<HasNNOStep N> requires std::equality_comparable<N>
constexpr std::optional< N >	dedekind::category::lower_cover (const N &n)
	The lower cover \(P^{+} : N \to 1 + N\), dual to cover: the predecessor read partially, `nullopt` at the least element (a fixpoint of `P`, or a machine word's least value). Not the destructor `Prior`, which is nothing at zero.
template<typename A, typename G> requires std::regular_invocable<const G&, const A&> && std::convertible_to<std::invoke_result_t<const G&, const A&>, A> && std::copyable<A>
constexpr A	dedekind::category::nno_iterate (A a0, G g, std::size_t n)
	Recursion-via-universal-property (operational discharge).

Detailed Description

The Natural Numbers Object — Lawvere's ETCS Axiom 9 — and the upstream home of Peano recursion / primitive recursion / the Peano successor (categorical idiom + textbook synonyms below).

@partition :nno

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

nno__Vocabulary

The categorical and textbook idioms are interchangeable on this partition — they name the same Form under different names:

NNO universal property ≡ Peano recursion (a.k.a. primitive recursion).
The arrow s : N → N (categorical idiom) ≡ the Peano successor.
The arrow z : 1 → N (categorical idiom) ≡ the zero axiom.
A morphism f : N → A determined by (a₀, g) (categorical idiom) ≡ a function defined by Peano recursion with base case a₀ and recursive step g.

The categorical idiom is what the IsNNO concept below pins structurally. The textbook idiom is recorded here so that a search for "Peano" lands at this upstream Form, not at one of the downstream witness sites where the carrier-level successor member API is named on a specific carrier (morphologies:archimedean for the IsCyclic shape; numbers:natural for Cardinality's NNO witness). See the layering note in §nno__Layering_audit.

nno__NNO_Universal_Property

In Lawvere's ETCS the natural numbers are not constructed — they are defined by a universal property. An NNO consists of an object N together with two arrows

z : 1 → N (the zero element) s : N → N (the successor map)

such that for any object A together with arrows a₀ : 1 → A and g : A → A there exists a unique arrow f : N → A making the recursion diagram commute:

f ∘ z = a₀ (initial-value clause) f ∘ s = g ∘ f (step clause)

Existence + uniqueness of f for any (A, a₀, g) is the universal property; equivalently, "every Peano-recursion specification has a unique total function realising it" — the engineer's honesty obligation in this codebase, since C++ concepts cannot quantify over the functorial content. The structural shape ( z and s as arrows of the stated signatures) is what the type system can pin.

nno__Layering_audit

Audited 2026-05-07: the upstream home of Peano recursion / Peano successor / primitive recursion is this partition (:category:nno). The downstream files that mention "Peano" surface the carrier-level witness, not the categorical Form:

morphologies:archimedean — has a T::successor(x) member API on IsCyclic carriers (Modular<N> etc.). The numerically-coinciding-with \(S(x) = x + 1\) remark there is about the carrier's API, not about NNO universality.
numbers:natural — registers Cardinality as the canonical IsNNO witness. This is a (z, s) pair on a specific carrier; the universal property it claims-to-witness is what this partition defines.

The layering is correct: Form upstream (:category:nno), witnesses downstream. The textbook-vocabulary section above is the cross-reference that prevents the "Peano keeps appearing in prose but is buried downstream" misreading a search-by-vocabulary naturally invites.

nno__This_Partition

Lifts ETCS Axiom 9 from the :etcs facade-level mention (where it was previously cross-referenced as SpeciesTraits<unsigned>) to a first-class concept that any carrier can witness. Closes part of #445. Concrete carrier witnesses ( Cardinality from sets:cardinality, Modular<N> from morphologies:cyclic) are registered downstream where the carriers are available. Dedekind's chain over the step, as a range, is :chain's.

nno__Form_Bias_NNO_Cardinality_ℕ

Per the project's Platonist stance ("Forms precede carriers"), the architecture is a three-layer chain:

NNO → Cardinality → ℕ

NNO is the Form — the universal property defined in this partition. Multiple carriers may witness it.
Cardinality (variant ℕ-proxy in sets:cardinality) is the canonical carrier inhabiting the NNO Form, certified by the IsNNO witness in numbers:natural. Saturating semantics ( ℵ_0 escalation) is the carrier's extra behaviour beyond the textbook NNO — the abstract NNO is purely the Peano-style universal property over a bounded / finite presentation; Cardinality adds ℵ_0 as an overflow sentinel so a machine implementation can stay honest about values that exceed its representable range.
ℕ (textbook symbol, in sets:boundaries post-#427) is an alias that refers to Cardinality — the symbol practitioners use. The chain reads "NNO supplies the Form; Cardinality is the canonical witness; ℕ is the name."

Sibling carrier witnesses ( Modular<2^w> as the bounded NNO, the textbook ℤ/2^wℤ; unsigned int with the bounded-NNO caveat that closure under successor only holds away from numeric_limits<unsigned>::max() ) are downstream candidates.

Note: "Die Zahlen sind freie Schöpfungen des menschlichen Geistes; sie dienen als ein Mittel, um die Verschiedenheit der Dinge leichter und schärfer aufzufassen."

[Trans: "Numbers are free creations of the human mind; they serve as a means of apprehending more easily and more sharply the difference of things."] — Richard Dedekind, Was sind und was sollen die Zahlen? (1888), preface.

Classes

Namespaces