**Are you an EPFL student looking for a semester project?**

Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.

Concept# Natural numbers object

Summary

In , a natural numbers object (NNO) is an object endowed with a recursive structure similar to natural numbers. More precisely, in a E with a terminal object 1, an NNO N is given by:
a global element z : 1 → N, and
an 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.
In other words, the triangle and square in the following diagram commute.
The pair (q, f) is sometimes called the recursion data for u, given in the form of a recursive definition:
⊢ u (z) = q
y ∈E N ⊢ u (s y) = f (u (y))
The above definition is the universal property of NNOs, meaning they are defined up to canonical 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 (CCCs) or topoi are sometimes defined in the following equivalent way (due to Lawvere): for every pair of arrows g : A → B and f : B → B, there is a unique h : 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 (denoted by +), an NNO can be defined as the initial algebra of the endofunctor that acts on objects by ↦ 1 + and on arrows by ↦ id1 + .
Every NNO is an initial object of the category of of the form
If a cartesian closed category has weak NNOs, then every of it also has a weak NNO.
NNOs can be used for non-standard models of type theory in a way analogous to non-standard models of analysis. Such categories (or topoi) tend to have "infinitely many" non-standard natural numbers. (Like always, there are simple ways to get non-standard NNOs; for example, if z = s z, in which case the category or topos E is trivial.)
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.

Official source

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications

Loading

Related people

Loading

Related units

Loading

Related concepts

Loading

Related courses

Loading

Related lectures

Loading

Related MOOCs

Loading

Related concepts

Related units

Related courses

Related publications

Related lectures

No results

Related MOOCs

Related people

No results

No results

No results

No results

No results

No results