An equational variant of Lawvere's natural numbers object
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).
- Adjointness in Foundations
- AN ELEMENTARY THEORY OF THE CATEGORY OF SETS
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- Least fixpoints of endofunctors of cartesian closed categories
- Pre-recursive categories
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
This page was built for publication: An equational variant of Lawvere's natural numbers object
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1588078)
