IsInitial
plain-language theorem explainer
IsInitial equips a Peano algebra A with a homomorphism to every other Peano algebra B together with uniqueness of the underlying map. Researchers on categorical logic or universal forcing cite it to certify that an arithmetic object extracted from a logic realization is the initial one. The declaration is a bare structure with two fields and no proof body.
Claim. A Peano algebra $A$ (carrier type with zero element and successor map) is initial when, for every Peano algebra $B$, there exists a homomorphism $A$ to $B$ (function preserving zero and successor) and any two such homomorphisms agree on their underlying functions.
background
PeanoObject is a structure with a carrier type, zero element, and step map. Hom is the structure of maps between two PeanoObjects that send zero to zero and commute with the step operation. The module extracts arithmetic from an abstract Law-of-Logic realization; the key point is initiality: once a realization supplies identity and step data, the forced arithmetic object is the initial Peano algebra generated by that data. Initial objects are unique up to unique isomorphism; this is the mechanism behind Universal Forcing.
proof idea
This is a structure definition with no proof body. It directly records the initiality property by declaring the lift field (existence of homomorphisms to any target) and the uniq field (agreement of underlying functions).
why it matters
The definition is instantiated in ArithmeticOf (which pairs a PeanoObject with its IsInitial datum), in logicNat_initial, and in realization_initial. It is also required by LawvereNNO and by isInitial in UniversalForcing.NaturalNumberObject. In the Recognition framework it supplies the initiality that forces arithmetic from logic realizations and thereby realizes the universal forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.