Let \(T\) be a base type theory, and let \(X\) be a topos in \(T\). We work in \(\mathord {\textnormal {\textsf {Glob}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}(\mathord {\textnormal {\textsf {Sp}}})\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\).

• -\(\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))\) has products and coproducts indexed over any \(A:\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))\) in \(T\).
• -\(\mathcal {E}(i)\) is closed under coproducts indexed over any \(A:\mathord {\textnormal {\textsf {Type}}}(i)\) in \(T\).