Characterization of 'canonical' natural numbers objects

Question

Canonicity is a useful property satisfied by some type theories, saying that every element of natural number type is propositional equal to an element of the form $s^n(0)$, where $s$ is the successor operation. For certain type theories, this can be proven by gluing techniques, as done by Lambek and Scott. The categorical translation of canonicity then becomes that every arrow $1\to \mathbb{N}$, where $\mathbb{N}$ is the natural numbers object, is of the form $S^n(0)$. These gluing arguments use certain syntactic topoi of the relevant type theory.

I was wondering if there are categorical results on canonicity in categories. That is, if there are necessary or sufficient properties a category $\mathcal{C}$ with a natural numbers object $\mathbb{N}$ should have in order to enjoy canonicity. Or, does anyone have an insightful counterexample why not every natural numbers object satisfies canonicity?

Thanks!

Edit: I am not necessarily looking out for a 'canonicity' in the type theoretic, constructivistic sense. I'll also be very happy with natural number objects satisfying that every map $1\to \mathbb{N}$ is of the forn $s^n(0)$, not necessarily in the canonicity sense. I don't really know the terminology for this.

Answer 1

I suspect there is no good answer to the question:

The type theoretic results you are mentioning definitely have a category theoretic interpretation in fact their proof using gluing is already very category theoretic.

But these results say that for example the "free topos with NNO", or the "free (locally) cartesian closed category with NNO" satisfies canonicity as you defined it (Here "free" means "initial").

To me the intuitive understanding of these results is that if the initial category with some structure was failing canonicity, there would be a map $1 \to N$ witnessing it, and by initiality this map would appear in all other category with the same structure, for example you'll get some "non-canonical integer" existing in all elementary toposes. Playing around with some model where we know there is no such terms (and using gluing) on can arrive with some work at a contradiction.

But in any case the essential assumption is this "Free" or "initial". These results of course do not say that "all topos satisfies canonicity" or "all locally cartesian closed category satisfies canonicity".

So you can get a purely category theoretic approaches to these, and never even mention type theory. But at the end of the day, type theory is really just a description of the initial category with "such and such" structure, so because these results are about these initial categories, even if you don't mention type theory explicitely at all, it will be there.

I do not know any general results about canonicity that is not of this kind. But of course, I cannot prove that these do not exists, and maybe someone will know some other kind of examples.

To some extent, Zhen Lin comment is an example: if your category has countable coproduct and $Hom(1,\_)$ preserve them, then you have canonicity. But this is far more elementary than the sort of result you were mentioning.

Answer 2

My comment (2) was:

That the logical results apply to initial or term models is clearly important, and somewhere in that we're using recursion over that model. This must be a stronger form of recursion than whatever the object theory includes, because it's proving consistency of that theory. This means that we must be invoking some form of the Axiom-scheme of Replacement. That is, in the case where the object logic is set-like higher order logic, although I propose that the term Replacement be generalised to mean recursion over the term model of whatever object logic.

Simon Henry replied:

These proofs of canonicity do not prove consistency: they assume consistency. Indeed they glue the initial model to some other concrete model that we understand well (usually $\mathbf{Set}$), but, having this concrete model already implies consistency.

Quick answer:

I'm a categorist, not a logician, so I'm not sure about the "official" names for these things. I would say that the "canonicity" in this Question is a version of consistency, in particular it says $0\neq 1$. The other corollaries of the gluing contruction (or "logical relations", as it's known in theoretical computer science) are similar.

For this to work, the "concrete model that we know well (usually $\mathbf{Set}$)" must be more than a model of the theory under discussion. This is because the gluing results in an internal model inside the concrete one. Also, we may do type-valued recursion within this concrete model over the term model.

This is what I mean by a version of the Axiom-Scheme of Replacement.

I said this is a "quick answer" because I would like to come back to it (and invite Simon and others to contribute comments in the mean time). I am in the final stages of selling a house, so I cannot think clearly about mathematics at the moment.