Let \(T_{1}\) be a type theory and let \(T_{2}\) be a type theory internal to \(T_{1}\). We work in \(T_{2}\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\), let \(A:\mathord {\textnormal {\textsf {Type}}}(i)\) in \(T_{1}\), and let \(B(x):\mathord {\textnormal {\textsf {Type}}}(i)\) under assumption \(x:A\). We say \(T_{2}\) has the coproduct of \(B\) if the inductive type

\(\coprod _{x:A}B(x):\mathord {\textnormal {\textsf {Type}}}(i)\) with the following constructors is constructible.

• -Let \(a:A\) and let \(b:B(a)\). Then \(\mathord {\textnormal {\textsf {in}}}_{a}(b):\coprod _{x:A}B(x)\).