Synthetic topos theory
[0005] Definition

Let \(U\) be a universe. The \(2\)-category \(\mathord {\textnormal {\textsf {Topos}}}(U)\) of \(U\)-toposes is defined to be \({(\mathord {\textnormal {\textsf {Logos}}}(U))}^{\mathord {\textnormal {\textsf {op}}}}\).