A Theory of Elementary Higher Toposes

Abstract

We define an elementary $\infty$-topos that simultaneously generalizes an elementary topos and Grothendieck $\infty$-topos. We then prove it satisfies the expected topos theoretic properties, such as descent, local Cartesian closure, locality and classification of univalent morphisms, generalizing results by Lurie and Gepner-Kock. We also define $\infty$-logical functors and show the resulting $\infty$-category is closed under limits and filtered colimits, generalizing the analogous result for elementary toposes and Grothendieck $\infty$-toposes. Moreover, we give an alternative characterization of elementary $\infty$-toposes and their $\infty$-logical functors via their ind-completions. Finally we generalize these results by discussing the case of elementary (n,1)-toposes and give various examples and non-examples.