An equational variant of Lawvere's natural numbers object (Q1588078): Difference between revisions

As is well known, \textit{F. W. Lawvere}'s definition of a natural numbers object \(N\) in a cartesian closed category is equivalent to asserting that morphisms defined recursively over \(N\) exist and are unique. If one attempts to characterize recursion equationally, one can capture the existence of recursively defined morphisms but not their uniqueness (the latter requires an implication), leading to a notion that has been called a weak natural numbers object. In this paper, the author observes that one can recapture part of the uniqueness by exploiting the fact that addition and truncated subtraction enable one to define a Mal'cev operation on a natural numbers object; this leads to a notion which he calls a quasi-NNO. Morphisms defined recursively on a quasi-NNO are not unique in general, but they are unique if their codomain belongs to the class of objects which `admit enough \(N\)-valued functions to separate points' (in the internal logic of the cartesian closed category).