Let \(T\) be a type theory. We work in the type theory of spaces in \(T\).

• -A univalent universe \(\mathcal {T}:\mathord {\textnormal {\textsf {Type}}}(1)\) of toposes is constructed.
• -\(\mathcal {E}(0)\) is in \(\mathcal {T}\).
• -Let \(A:\mathcal {E}(0)\). Then \(A\) is in \(\mathcal {T}\).
• -\(\mathcal {T}\) is closed under the unit type, pair types, identity types, products indexed over any \(A:\mathord {\textnormal {\textsf {Type}}}(0)\), and function types whose domains are in \(\mathcal {E}(0)\).