Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
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.
,