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. Then \(\mathord {\textnormal {\textsf {C}}}_{T_{2}}\) is a “left adjoint” of \(\mathord {\textnormal {\textsf {GS}}}_{T_{2}}\).