[003D] Classifying spaces

Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos. We define a translation \(Z\mapsto {\mathopen {[\negthinspace [}Z\mathclose {]\negthinspace ]}}^{X}\) from \(\mathord {\textnormal {\textsf {Sp}}}\) to \(\mathord {\textnormal {\textsf {Sh}}}(X)\) by \({\mathopen {[\negthinspace [}Z\mathclose {]\negthinspace ]}}^{X}\equiv \mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}({X}^{*}(Z))\).

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\).

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. Then we have the following equivalences.

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.