Parametrized natural numbers object.

Question

Lambek and Scott demonstrate in Introduction to higher order categorical logic the existence of a parametrized nno when we are in a cartesian closed category (CCC) with a "simple nno" and suggest the possibility of define a parametrized nno in the context of a cartesian category (CC) with a simple nno. In which cases can it be done in the context of a CC? Could it be done only with numerals or (in the more general case of a) strong nno?

Ximo.

Answer 1

I give two examples of categories with finite products and simple NNO. In the first example the simple NNO is also a parameterized NNO, while in the second example it is not. Although it is difficult to understand your question, I believe the examples should clarify matters.

First, consider the category $\mathcal{C}$ whose objects are the finite powers of $\mathbb{N}$, namely $\mathbb{N}^0$, $\mathbb{N}^1$, $\mathbb{N}^2$, ... and morphisms are set-theoretic functions $f : \mathbb{N}^k \to \mathbb{N}^m$. This category clearly has finite products, is not cartesian-closed because there are too many morhisms $\mathbb{N} \to \mathbb{N}$, and it has a parameterized NNO, namely the obvious one.

[Updated 2022-12-07] Following Sridhar Ramesh's suggestion, we describe a category $\mathcal{D}$ which has a simple NNO but not a parameterized one. Say that a map $f : \mathbb{N}^k \to \mathbb{N}^m$ is good when for every projection $\pi_k : \mathbb{N}^m \to \mathbb{N}$ there is $f' : \mathbb{N} \to \mathbb{N}$ such that $\pi_k \circ f = f' \circ \pi_k$.

Now take as the objects of $\mathcal{D}$ powers $\mathbb{N}^0, \mathbb{N}^1, \mathbb{N}^2, \ldots$ and the morphisms are the good maps. Identity maps are obviously good because $\pi_k \circ \mathrm{id} = \mathrm{id} \circ \pi_k$. To see that the composition of good maps $f : \mathbb{N}^k \to \mathbb{N}^m$ and $g : \mathbb{N}^m \to \mathbb{N}^n$ is good, observe that $\pi_k \circ g = g' \circ \pi_k$ and $\pi_k \circ f = f' \circ \pi_k$ together apply $\pi_k \circ (h \circ f) = h' \circ \pi_k \circ f = (h' \circ f') \circ \pi_k$.

The category $\mathcal{D}$ has finite products, since projections are good, and so is the pairing of good maps.

The category $\mathcal{D}$ has a simple NNO, namely the obvious one, because the morphisms $\mathbb{N} \to \mathbb{N}$ are all set-theoretic maps. But it cannot have a parameterized NNO, for if it did, we could construct addition ${+} : \mathbb{N}^2 \to \mathbb{N}$ as a morphism in the category.

Answer 2

If I understand correctly, by a parametrized nno in a category $C$ you mean a nno $N$ which is stable under pullbacks: $N \times X$ is a nno in the slice $C/X$ for every object $X$ of $C$. The reason why a nno in a cartesian closed category is automatically a parametrized nno is that any functor with a right adjoint will preserve nnos. Cartesian closedness is precisely equivalent to saying that the pullback functor $C \to C/X$ has a right adjoint.

Sometimes (e.g. in a topos) nnos can be characterized by the two axioms

• $1 \xrightarrow{z} N \xleftarrow{s} N$ is a coproduct diagram, and

• the coequalizer of $N\xrightarrow{s} N$ and the identity on $N$ is the terminal object $1$.

These correspond more closely to the Peano axioms rather than primitive recursion. In such cases, a right exact functor between such categories will preserve nnos. This may help you relax the cartesian closedness condition a little (though, obviously, not in the case of topoi).

Answer 3

So, here are some definitions about Natural Numbers Object (nno), that is a key concept in category theory related to Computer Science. They are given in Lambek and Scott (LS) in the following form:

1. A (simple) nno is a group of three (N,z,s) where N is an object and z (as zero) and s (as successor) morphisms in a category and the diagram $1\overset{z}{\longrightarrow}N\overset{s}{\longrightarrow}N$ is initial among all the diagrams in the form $1\overset{f}{\longrightarrow}Y\overset{g}{\longrightarrow}Y$
2. A parametrized nno is a group of three as the one above where the diagram $X\overset{(z,1_X)}{\longrightarrow}N \times X\overset{s \times 1_X}{\longrightarrow}N \times X$ is initial among all the diagrams in the form $X\overset{f}{\longrightarrow}Y\overset{g}{\longrightarrow}Y$

Barr and Wells propose to say the latter simply a nno because is the only of our interest. It is closely related to a descrption of the primitive recursive functions. A nno makes an object of a category behave as the natural numbers.

With all of these my questions are: while LS demonstrate the existence of a parametrized nno when we are in a cartesian closed category (CCC) with a (simple) nno...in which cases can it be done in the context of a CC (not closed)? Could it be done only with numerals in the sense of arrows $1\longrightarrow N^{k}$ standard (built up in terms of z and s morphisms)?

To ask about weak and strong nno's I would need more definitions, so I let it here for the moment. Thank you in advance and sorry for my english.

Ximo.