Let \(T\) be a type theory. We work in the type theory of spaces in \(T\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\).

• -A univalent universe \(\mathcal {E}(i)\) in \(\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))\) of étale types is constructed.
• -\(\mathcal {E}(i)\) is closed under the unit type, pair types, identity types, finite colimits, and coproducts indexed over any \(A:\mathord {\textnormal {\textsf {Type}}}(i)\).