IsInitial
plain-language theorem explainer
A Peano algebra A is initial when it admits a homomorphism to every other Peano algebra B and any two such homomorphisms agree on their underlying functions. Researchers on categorical arithmetic and Recognition Science cite the structure when showing that a logic realization forces a canonical natural-number object unique up to unique isomorphism. The definition directly records the universal mapping property as data in Type.
Claim. Let $A$ be a Peano algebra (a type with zero element and successor map). Then $A$ is initial if, for every Peano algebra $B$, there exists a homomorphism $f:A→B$ (a function preserving zero and commuting with successor) and, for any two such homomorphisms $f,g$, the functions $f$ and $g$ coincide on the carriers.
background
PeanoObject consists of a carrier type together with a zero element and a step map. Hom consists of functions between two PeanoObjects that preserve zero and commute with the step map; these form the morphisms of the category of Peano algebras. The module extracts arithmetic from an abstract Law-of-Logic realization; the key point is initiality, which supplies the mechanism behind Universal Forcing by guaranteeing that the forced arithmetic object is the initial Peano algebra generated by the realization data.
proof idea
This is a structure definition encoding the initial-object property. It introduces two fields: lift, which supplies a homomorphism to an arbitrary target Peano algebra, and uniq, which asserts that any two such homomorphisms agree as functions on the carriers.
why it matters
The structure is used to build ArithmeticOf (which pairs a Peano object with its initiality witness) and appears in logicNat_initial, realization_initial, LawvereNNO, and the isInitial construction in UniversalForcing.NaturalNumberObject. It supplies the initial-object datum required by the module's account of arithmetic forced from logic realizations, thereby supporting the uniqueness-up-to-unique-isomorphism step in Universal Forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.