categoryInterfaceOfLawvere
plain-language theorem explainer
The definition constructs a CategoryNNOInterface from any LawvereNNO by collapsing the object type to Unit and routing all morphisms through the identity Peano homomorphism on the underlying carrier. Foundation researchers building categorical realizations of arithmetic cite it as the explicit bridge from initial Peano objects to Lawvere-style NNO data. It proceeds by direct structural assignment that populates each interface field from the supplied Peano homomorphisms and the trivial initiality proposition.
Claim. Let $N$ be a Lawvere natural-number object whose underlying Peano algebra is initial. The categorical interface is the structure whose object type is the singleton, whose hom-sets are the Peano homomorphisms on the carrier of $N$, whose terminal object and natural-number object are both the singleton, whose zero and successor morphisms are both the identity homomorphism on that carrier, and whose initiality field is the proposition True.
background
The CategoricalLogicRealization module packages the natural-number object using the initial-Peano-algebra language of ArithmeticOf. A PeanoObject consists of a carrier type together with a zero element and a successor map. A LawvereNNO is the structure that augments such a PeanoObject with a proof that it is initial, a decidable equality on the carrier, and a witness of nontriviality. The CategoryNNOInterface is the explicit record that names the data a categorical realization must supply: an object type, hom-sets, a terminal object, an NNO object, zero and successor morphisms, and an initiality proposition. This avoids importing Mathlib's full category-theory library while still naming the required pieces.
proof idea
Direct structural definition. The object type is set to Unit, the hom-sets are taken from PeanoObject.Hom applied to the underlying object of the input LawvereNNO, the terminal and NNO fields are both the unit element, the zero and successor morphisms are both the identity homomorphism supplied by PeanoObject.Hom.id, and the initiality field is the proposition True.
why it matters
The definition is the concrete hook required by the downstream theorem logicNatNNO_has_category_interface, which shows that the canonical logicNatNNO produces a nonempty initiality field. It advances the module's goal of supplying a Lawvere-style realization for the Universal Forcing program while remaining inside the Peano-algebra language. In the larger Recognition framework it supplies the first explicit link between the arithmetic foundation and the categorical data needed for later steps that derive the eight-tick octave and spatial dimension from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.