Constructing coproducts in locally Cartesian closed \(\infty\)-categories (Q6039222)

Elementary toposes were defined by Lawvere and Tierney as a generalization of Grothendieck toposes, which always admit limits and colimits. The first definitions of elementary topos assumed the existence of both finite limits and finite colimits [\textit{F. W. Lawvere}, in: Actes Congr. internat. Math. 1970, 1, 329--334 (1971; Zbl 0261.18010); \textit{M. Tierney}, Lect. Notes Math. 274, 13--42 (1972; Zbl 0244.18005)]. However, it was soon realized that the existence of finite colimits could in fact be deduced from the other axioms [\textit{R. Pare}, Bull. Am. Math. Soc. 80, 556--561 (1974; Zbl 0288.18002); \textit{R. Pare}, Rev. Roum. Math. Pures Appl. 22, 335--340 (1977; Zbl 0359.18001); \textit{C. J. Mikkelsen}, Lattice theoretic and logical aspects of elementary topoi. Aarhus: Aarhus Universitet (1976; Zbl 0345.18006)]. The theory of Grothendieck toposes has successfully been generalized to the higher categorical setting, both in the context of model categories [\url{https://faculty.math.illinois.edu/~rezk/homotopy-topos-sketch.pdf}] and \(\infty\)-categories [\textit{J. Lurie}, Higher topos theory. Princeton, NJ: Princeton University Press (2009; Zbl 1175.18001)]. At the same time, categorical logicians have devised a homotopy invariant interpretation of Martin-Löf type theory [\textit{P. Martin-Löf}, Intuitionistic type theory. Napoli: Bibliopolis (1984; Zbl 0571.03030)], known as homotopy type theory [\textit{The Univalent Foundations Program}, Homotopy type theory. Univalent foundations of mathematics. Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press (2013; Zbl 1298.03002)], which was quickly conjectured to generalize from homotopy types to arbitrary \(\infty\)-toposes, which was completely established in [\textit{M. Shulman}, ``All \((\infty,1)\)-toposes have strict univalent universes'', Preprint, \url{arXiv:1904.07004}]. Just as the interpretation of higher order logic in \(1\)-toposes, the interpretation of type theory in \(\infty\)-toposes does not rely on the (co)completeness of the topos, which suggests to formulate a notion of ``finitary'' or ``elementary'' \(\infty\)-topos as natural target for the interpretation of type theory, analogous to Lawvere and Tierney's elementary \(1\)-toposes. Concrete proposals for a definition of elementary \(1\)-topos were given in [\url{https://golem.ph.utexas.edu/category/2017/04/elementary_1topoi.html}, \textit{N. Rasekh}, ``A theory of elementary higher toposes'', Preprint, \url{arXiv:1805.03805}], explicitly postulating the existence of finite colimits. This paper gives a partial answer to the question whether we can recover finite colimits from the remaining axioms just as in the \(1\)-dimensional case. The synopsis of the paper goes as follows. \begin{itemize} \item[\S 2] recalls basic facts about locally Cartesian closed \(\infty \)-categories, including the Beck-Chevalley condition (Lemma 2.1), truncation levels (\S 2.1) and the \textit{object of contractibility}, which is a technique allowing of reducing contractibility questions to contractibilitysubterminals. \item[\S 3] addresses subobject lattices and subobject classifiers, showing that if a locally Cartesian closed \(\infty\)-category has a subobject classifier, then its subobject lattices have finite joins (Theorem 3.4). \item[\S 4] shows that any locally Cartesian closed \(\infty\)-category with a subobject classifier has an initial object (Corollary 4.4). \item[\S 5] shows that any locally Cartesian closed \(\infty\)-category with a subobject classifier has binary coproducts (Theorem 5.4). \item[\S 6] discusses the relevance of Theorem 5.4 to the notion of elementary \(\infty\)-topos. \end{itemize}