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.
TAC Home