toPeano
plain-language theorem explainer
This definition extracts the Peano algebra from a Lawvere natural-number object by exposing its carrier type together with the zero element and successor map. Categorical foundation researchers and Recognition Science modelers cite it when constructing the initial object in the category of pointed endomap algebras. It is realized as a direct record projection that copies the zero and step components from the input structure.
Claim. Given a Lawvere natural-number object $(N, z, s)$ equipped with a unique recursor for every target pointed endomap, the associated Peano algebra is the triple $(N, z, s)$.
background
A Lawvere natural-number object is a triple $(N, z, s)$ such that for every pointed endomap $(X, x, f)$ there exists a unique map $h: N → X$ satisfying $h(z) = x$ and $h ∘ s = f ∘ h$. The structure IsNaturalNumberObject encodes this universal property via its recursor field together with the three axioms that enforce correct behavior at zero and successor and uniqueness of the induced map. The simpler PeanoObject record consists only of a carrier type, a zero element, and a successor function, without the recursor data. The module establishes that the arithmetic forced by the Law of Logic yields such an object in every realization, with the iteration structure identical across carriers including the two-element Boolean case.
proof idea
The definition is a direct record constructor for PeanoObject. It sets the carrier field to the underlying type of the input IsNaturalNumberObject, the zero field to the supplied z, and the step field to the supplied s.
why it matters
This definition supplies the concrete Peano algebra that isInitial consumes to establish initiality in the category of pointed endomap algebras. It thereby completes the passage from the Lawvere characterization stated in the module documentation to the algebra required for downstream forcing arguments. In the Recognition framework it ensures that the arithmetic forced by J-uniqueness and the phi fixed point is initial, closing the loop from the universal forcing chain to concrete number systems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.