Editing Natural numbers object (section)

In [[category theory]], a '''natural numbers object''' ('''NNO''') is an object endowed with a [[Recursion (computer science)|recursive]] [[Mathematical structure|structure]] similar to [[natural number]]s. More precisely, in a [[Category (mathematics)|category]] '''E''' with a [[terminal object]] 1, an NNO ''N'' is given by:

# a [[global element]] ''z'' : 1 → ''N'', and
# an [[morphism|arrow]] ''s'' : ''N'' → ''N'',

such that for any object ''A'' of '''E''', global element ''q'' : 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''.{{sfn|Johnstone|2002|loc=A2.5.1}}{{sfn|Lawvere|2005|p=14}}<ref>{{Cite journal|last=Leinster|first=Tom|date=2014|title=Rethinking set theory|journal=American Mathematical Monthly |volume=121|issue=5|pages=403–415|arxiv=1212.6543|bibcode=2012arXiv1212.6543L|doi=10.4169/amer.math.monthly.121.05.403|s2cid=5732995 }}</ref>

In other words, the triangle and square in the following diagram commute.

<div style="margin-left: 2em">[[Image:Natural numbers object definition.svg|250px|A commutative diagram expressing the equations in the definition of an NNO]]</div>

The pair (''q'', ''f'') is sometimes called the ''recursion data'' for ''u'', given in the form of a [[recursive definition]]:

# ⊢ ''u'' (''z'') = ''q''
# ''y'' ∈<sub>'''E'''</sub> ''N'' ⊢ ''u'' (''s'' ''y'') = ''f'' (''u'' (''y''))

The above definition is the [[universal property]] of NNOs, meaning they are defined [[up to]] [[List of mathematical jargon#canonical|canonical]] [[morphism|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.