Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
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.