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}}}$