Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos. Then the translation \(Z\mapsto {\mathopen {[\negthinspace [}Z\mathclose {]\negthinspace ]}}^{X}\) from \(\mathord {\textnormal {\textsf {Sp}}}\) to \(\mathord {\textnormal {\textsf {Sh}}}(X)\) sends \(\mathcal {E}(i)\) to \(\mathcal {U}(i)\) for every \(i:\mathord {\textnormal {\textsf {Level}}}\) and preserves finite limits, products, function types whose domains are étale, finite colimits of étale types, and coproducts of étale types.