Synthetic topos theory
[0029] Rule

Let \(T\) be a type theory. We work in the type theory of spaces in \(T\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\). Then \(\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))\) has the unit type, pair types, identity types, function types, inductive types, and products and coproducts indexed over any \(A:\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))\) in \(T\). Moreover, \(\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))\) is represented by a univalent universe \(\mathcal {V}(\mathord {\textnormal {\textsf {succ}}}(i)):\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(\mathord {\textnormal {\textsf {succ}}}(i)))\).