Synthetic topos theory
[0018] Definition

Let \(U\) be a universe. We define \(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U)\) to be the \(1\)-categorical core of \(\mathord {\textnormal {\textsf {Topos}}}(U)\).