Michael Shulman
NNO in a 2-category

If K is a 2-category with finite limits, a successor algebra in K is an object X equipped with morphisms o:1X and s:XX. A morphism of successor algebras is a morphism f:XY with isomorphisms fo Xo Y and fs Xs Yf. Likewise a 2-cell of successor algebras is a 2-cell α:fg commuting with the above isomorphisms in an obvious way.

Finally, a natural numbers object in K is an initial object N in the 2-category SuccAlg(K) of successor algebras. This means that for any successor algebra X there is a morphism NX of successor algebras, unique up to unique isomorphism. Clearly any NNO in K is also an NNO, in the usual sense, in disc(K).

If K doesn’t have enough exponentials, then perhaps this definition should be augmented with some parametricity, as in the 1-categorical case.

As in a 1-category, we can prove that:

  • If K has coproducts, then [o,s]:1+NN is an equivalence, since N is an initial algebra for the endofunctor 1+().
  • Therefore, if K is extensive, then o:1N and s:NN are disjoint subobjects of N.
  • N satisfies the fifth Peano axiom: if N is a subobject of N containing o and closed under s, then N=N.

This enables us to show the following, using the internal logic.

Theorem

If K is a positive Heyting coherent 2-category with an NNO N, then N is discrete.

Proof

First note that since N1+N and coproducts are disjoint, we have

x:N,f:hom N(o,x),g:hom N(x,o) f=gand is an isomorphism x:N,f:hom N(x,o),g:hom N(o,x) f=gand is an isomorphism\begin{aligned} x:N, f:hom_N(o,x), g:hom_N(x,o) &\vdash f=g\;\text{and is an isomorphism}\\ x:N, f:hom_N(x,o), g:hom_N(o,x) &\vdash f=g\;\text{and is an isomorphism} \end{aligned}

Now consider the subobject SN described in the internal logic as determined by those y:N for which the above sequents remain true when o is replaced by y. (This requires universal quantification over x,f,g.) The above observation shows that oS. Suppose that yS, x:N, and f:hom N(sy,x), g:hom N(sy,x). If x=o then f=g and is an isomorphism; otherwise x=sz; but s is ff, so we have f:hom N(y,z) and g:hom N(y,z) which are equal and isomorphisms; hence so are f=s(f) and g=s(g). Thus, S is closed under s, so it is all of N. Therefore, N is discrete.

Revised on February 13, 2009 05:28:19 by Mike Shulman (75.3.140.11)