Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::category::IsNNO Concept Referenceexport

Structural shape: (N, Z, S) is a Natural Numbers Object — Z is the zero element 1 → N, S is the successor map N → N. More...

Concept definition

template<typename N, typename Z, typename S>
concept dedekind::category::IsNNO = requires(Z z, S s, N n) {
{ z() } -> std::convertible_to<N>;
{ s(n) } -> std::convertible_to<N>;
}
Structural shape: (N, Z, S) is a Natural Numbers Object — Z is the zero element 1 → N,...
Definition nno.cppm:183

Detailed Description

Structural shape: (N, Z, S) is a Natural Numbers Object — Z is the zero element 1 → N, S is the successor map N → N.

C++ concepts cannot quantify over the universal property (existence + uniqueness of f : N → A for arbitrary (A, a₀, g)); that is the engineer's honesty obligation. The structural shape pinned here is the operational signatures — Z is callable with no arguments and yields an N (the zero element); S is callable on an N and yields an N (the successor). Together they generate the NNO's iterated presentation: Z(), S(Z()), S(S(Z())), ...

The dual shape concept on the Functor side (NNOs as initial F-algebras of F(X) = 1 + X) is reified in the sibling partition :f_algebra (closes the universal-property layer for #449; Pierce §5.4, Mac Lane III–VI). The two readings are operationally equivalent — the (z, s) pair pinned here induces the structure map [z, s] : 1 + N → N via coproduct copairing on the standard injections inl : 1 → 1 + N and inr : N → 1 + N. This partition focuses on the (z, s) shape since it is the more directly recognisable one to a working mathematician.

Template Parameters
NThe carrier object.
ZA nullary callable Z : 1 → N (the zero element).
SA unary callable S : N → N (the successor).
See also
Dedekind [4], the naturals as the chain of one element under a map into itself; Peano [9], the same as axioms.