Added proof that the “simpler” notion of parametrized NNO is equivalent to the more obviously correct one.

]]>added pointer to:

- Nima Rasekh,
*Every Elementary Higher Topos has a Natural Number Object*, (arXiv:1809.01734)

Yes, you seem to be correct. Good catch.

]]>please doublecheck my correction. but it seems like the second pair is backwards. if we identify (\pi_1 \circ a, \pi_2 \circ b) and (\pi_2 \circ a, \pi_1 \circ b), that means we’re declaring i-l = j-k for i+j = k+l, whereas we actually want i-l = k-j. So we want to identify (\pi_1 \circ b, \pi_2 \circ a)

]]>Why is it that a parameterized NNO is the same as being preserved by all the functors to the coKelisli categories for the comonad $A\times -$? I’m trying to see how this works as I’d like to think of an NNO as being an initial algebra for a polynomial endofunctor (arising from 1←1→1+1→1) and these two pictures aren’t meshing.

]]>Oops, quite right. I suppose $ZFC + \neg Con(ZFC)$, with the “function” that verifies proofs of inconsistency of ZFC, is what I meant.

]]>But wait: ZFC proves that PA is consistent (since one can establish ordinal induction up to $\epsilon_0$ in ZFC).

Edit: Well, I think the conclusion must still hold anyway: in the initial structure, it cannot be established that $G = 0$, since that would amount to provability of that statement within primitive recursive arithmetic. So $G$ and $0$ are distinct there.

]]>Ah yes, that certainly seems to work. Nice!

]]>Hmmm. Well, consider the primitive recursive “function” $G$ defined by $G(n) = 1$ if $n$ codes the proof of a contradiction in Peano arithmetic, and $G(n) = 0$ otherwise. (This is primitive recursive because no unbounded searches are required to verify the validity of a proof.) In the standard model of arithmetic, $G$ is the constant $0$ function, but we could equally consider the elementary topos corresponding to a model of $ZFC + \neg Con(PA)$, in which $G$ is *not* the constant $0$ function. Thus $G$ and the constant $0$ function must be distinct in the category $F$.

Maybe, but I’d really like to see a specific example of that.

]]>Perhaps it’s a question of extensionality? The morphisms $N^k \to N$ are surely constructed by syntactic means, and it’s conceivable that two such morphisms describe the same primitive recursive function in the standard model of arithmetic while not being provably equal (in whatever system of arithmetic corresponds to $F$).

]]>I added an explicit definition of parametrized NNO to natural numbers object.

I have a question: there is mention in that article of a categories with finite products and a parametrized NNO, and the initial such structure $F$, and it is written that the canonical maps

$\hom_F(N^k, N) \to \hom_{Set}(\mathbb{N}^k, \mathbb{N})$surject onto the primitive recursive maps. Why couldn’t “surject” be replaced by “biject”?

]]>I have expanded a little at *Transfer of NNOs along inverse images*.

Yes, of course, since it has a universal property.

]]>started an Examples-section at natural numbers object

btw, the natural numbers objects of a topos is unique, up to isomorphism, right? if so, we should say that

]]>