Michael Shulman
NNO in a 2-category

If KK is a 2-category with finite limits, a successor algebra in KK is an object XX equipped with morphisms o:1Xo:1\to X and s:XXs:X\to X. A morphism of successor algebras is a morphism f:XYf:X\to Y with isomorphisms fo Xo Yf o_X \cong o_Y and fs Xs Yff s_X \cong s_Y f. Likewise a 2-cell of successor algebras is a 2-cell α:fg\alpha: f\to g commuting with the above isomorphisms in an obvious way.

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

If KK 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 KK has coproducts, then [o,s]:1+NN[o,s]:1+N \to N is an equivalence, since NN is an initial algebra for the endofunctor 1+()1+(-).
  • Therefore, if KK is extensive, then o:1No:1\to N and s:NNs:N\to N are disjoint subobjects of NN.
  • NN satisfies the fifth Peano axiom: if NN' is a subobject of NN containing oo and closed under ss, then N=NN'=N.

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

Theorem

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

Proof

First note that since N1+NN\simeq 1+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 SNS\hookrightarrow N described in the internal logic as determined by those y:Ny:N for which the above sequents remain true when oo is replaced by yy. (This requires universal quantification over x,f,gx,f,g.) The above observation shows that oSo\in S. Suppose that ySy\in S, x:Nx:N, and f:hom N(sy,x)f:hom_N(s y, x), g:hom N(sy,x)g:hom_N(s y,x). If x=ox=o then f=gf=g and is an isomorphism; otherwise x=szx = s z; but ss is ff, so we have f:hom N(y,z)f':hom_N(y,z) and g:hom N(y,z)g':hom_N(y,z) which are equal and isomorphisms; hence so are f=s(f)f= s(f') and g=s(g)g=s(g'). Thus, SS is closed under ss, so it is all of NN. Therefore, NN is discrete.

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