#
Every elementary higher topos has a natural number object

##
Nima Rasekh

We prove that every elementary (∞,1)-topos has a natural number object.
We achieve this by defining the loop space of the circle and showing that we can construct a natural number object out of it.
Part of the proof involves showing that various definitions of natural number objects (Lawvere, Freyd and Peano) agree with each other in
an elementary (∞,1)-topos.
As part of this effort we also study the internal object of contractibility in (∞,1)-categories, which is of independent interest.
Finally, we discuss various applications of natural number objects. In particular, we use it to define internal sequential
colimits in an elementary (∞,1)-topos.

Keywords:
elementary topos theory, higher category theory, natural number objects

2020 MSC:
03G30, 18B25, 18N60, 55U35

*Theory and Applications of Categories,*
Vol. 37, 2021,
No. 13, pp 337-377.

Published 2021-03-24.

http://www.tac.mta.ca/tac/volumes/37/13/37-13.pdf

TAC Home