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.