Let \(T\) be a base type theory. We work in \(T\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\), let \(A:\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sp}}}}({}\vdash \mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i)))\), and let \(X\) be a topos. We define \(\mathord {\textnormal {\textsf {Model}}}^{X}(A)\equiv \mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}({}\vdash {\mathopen {[\negthinspace [}A\mathclose {]\negthinspace ]}}^{X})\). Elements of \(\mathord {\textnormal {\textsf {Model}}}^{X}(A)\) are called models of \(A\) in \(X\).