Every elementary higher topos has a natural number object
Theory and applications of categories, Tome 37 (2021), pp. 337-377
Cet article a éte moissonné depuis la source Theory and Applications of Categories website
We prove that every elementary (∞,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 (∞,1)-topos. As part of this effort we also study the internal object of contractibility in (∞,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 (∞,1)-topos.
Publié le :
Classification :
03G30, 18B25, 18N60, 55U35
Keywords: elementary topos theory, higher category theory, natural number objects
Keywords: elementary topos theory, higher category theory, natural number objects
@article{TAC_2021_37_a12,
author = {Nima Rasekh},
title = {Every elementary higher topos has a natural number object},
journal = {Theory and applications of categories},
pages = {337--377},
year = {2021},
volume = {37},
language = {en},
url = {http://geodesic.mathdoc.fr/item/TAC_2021_37_a12/}
}
Nima Rasekh. Every elementary higher topos has a natural number object. Theory and applications of categories, Tome 37 (2021), pp. 337-377. http://geodesic.mathdoc.fr/item/TAC_2021_37_a12/