such that for any object A of E, global elementq : 1 → A, and arrow f : A → A, there exists a unique arrow u : N → A such that:
u ∘ z = q, and
u ∘ s = f ∘ u.
In other words, the triangle and square in the following diagram commute.
The pair is sometimes called the recursion data for u, given in the form of a recursive definition:
⊢ u = q
y ∈EN ⊢ u = f
The above definition is the universal property of NNOs, meaning they are defined up tocanonical isomorphism. If the arrow u as defined above merely has to exist, that is, uniqueness is not required, then N is called a weak NNO.
NNOs in cartesian closed categories or topoi are sometimes defined in the following equivalent way : for every pair of arrows g : A → B and f : B → B, there is a uniqueh : N × A → B such that the squares in the following diagram commute.
This same construction defines weak NNOs in cartesian categories that are not cartesian closed. In a category with a terminal object 1 and binary coproducts, an NNO can be defined as the initial algebra of the endofunctor that acts on objects by and on arrows by.
NNOs can be used for non-standard models of type theory in a way analogous to non-standard models of analysis. Such categories tend to have "infinitely many" non-standard natural numbers.
Freyd showed that z and s form a coproduct diagram for NNOs; also, !N : N → 1 is a coequalizer of s and 1N, i.e., every pair of global elements of N are connected by means of s; furthermore, this pair of facts characterize all NNOs.
Examples
In Set, the category of sets, the standard natural numbers are an NNO. A terminal object in Set is a singleton, and a function out of a singleton picks out a single element of a set. The natural numbers ? are an NNO where is a function from a singleton to ? whose image is zero, and is the successor function. One can prove that the diagram in the definition commutes using mathematical induction.
In the category of types of Martin-Löf type theory, the standard natural numbers type nat is an NNO. One can use the recursor for nat to show that the appropriate diagram commutes.
Assume that is a Grothendieck topos with terminal object and that for some Grothendieck topology on the category. Then if is the constant presheaf on, then the NNO in is the sheafification of and may be shown to take the form