Every Elementary Higher Topos has a Natural Number Object

Abstract

We prove that every elementary $(\infty ,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 $(\infty ,1)$-topos. As part of this effort we also study the internal object of contractibility in $(\infty ,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 $(\infty ,1)$-topos.

arXiv comment32 Pages, final version, published in Theory and Applications of Categories

Cited by in corpus (2)

• Filter Quotients and Non-Presentable $(\infty ,1)$-Toposes
• Univalence in Higher Category Theory