Every Elementary Higher Topos Has A Natural Number Object
We prove that every elementary (infinity, 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 (infinity, 1)-topos. As part of this effort we also study the internal object of contractibility in (infinity, 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 (infinity, 1)-topos.
WOS:000674967700013
2021-01-01
37
337
377
Link to the fulltext
REVIEWED