By Nima Rasekh
One key aspect of elementary topos theory is the existence of a natural number object. While it does not exist in every elementary topos (such as finite sets) we often need it to study more advanced aspects of topos theory (such as free monoids). In this talk we see how in the higher categorical setting, the existence of a natural number object can in fact be deduced from a small list of axioms that any reasonable definition of elementary higher topos should satisfy, hence proving that every elementary higher topos has a natural number object. We will observe how the proof involves ideas from algebraic topology, elementary topos theory and homotopy type theory.
By Dustin Clausen
By Riccardo Zanfa
By Jean-Claude Belfiore
By Daniel Bennequin
By Samson Abramsky
By Jens Hemelaer
By Francesco Genovese
By Vasudevan Srinivas
By Marc Levine
