Let \(T_{1}\) be a base type theory and let \(T_{2}\) be a type theory internal to \(T_{1}\). We work in \(T_{1}\). Suppose that \(T_{2}\) has the unit type and coproducts. Let \(i:\mathord {\textnormal {\textsf {Level}}}\). We define a function

\(\mathord {\textnormal {\textsf {C}}}_{T_{2}}:\mathcal {U}(i)\rightarrow \mathord {\textnormal {\textsf {D}}}_{T_{2}}({}\vdash \mathord {\textnormal {\textsf {Type}}}(i))\) by \(\mathord {\textnormal {\textsf {C}}}_{T_{2}}(A)\equiv \coprod _{\_:A}\mathord {\textnormal {\textsf {1}}}\)