= Solution
<Morita equivalence of geometric theories> means equivalence of their <classifying toposes>. Equivalently, their categories of models in every <Grothendieck topos> are equivalent pseudonaturally with respect to inverse image. Agreement only of their set-based model categories, without this natural internal-model structure, is not the definition.
Suppose $\mathbf{Set}[\mathbb T]\simeq\mathbf{Set}[\mathbb S]=\mathcal E$. A property expressed intrinsically in terms of the topos is the same under either presentation. One can therefore translate a <site> or logical characterization of that property from $\mathbb T$ into one for $\mathbb S$. Examples include Booleanity, connectedness, atomicity and the structure of the <subtopos> lattice. The bridge is the common invariant $\mathcal E$, rather than an assumed literal identification of the two signatures.
The <duality between geometric quotients and subtoposes> makes this precise. A <geometric quotient theory> $\mathbb T'$ of $\mathbb T$ adds geometric axioms over the same signature. Quotients are identified when they prove the same geometric sequents. The theorem gives
$$
\boxed{\{\text{geometric quotients of }\mathbb T\}/\text{provable equivalence}
\ \longleftrightarrow\
\{\text{subtoposes of }\mathbf{Set}[\mathbb T]\}.}
$$
The <subtopos> corresponding to $\mathbb T'$ is its <classifying topos>. Stronger axioms correspond to smaller <subtoposes> under inclusion.
The <site> mechanism explains the correspondence. On $\mathcal C_{\mathbb T}$, an additional sequent requires the associated family of definable images to cover its antecedent. Adding these covering sieves produces a topology $J'\supseteq J_{\mathbb T}$ and a geometric embedding
$$
\mathbf{Sh}(\mathcal C_{\mathbb T},J')\hookrightarrow
\mathbf{Sh}(\mathcal C_{\mathbb T},J_{\mathbb T}).
$$
Conversely, <subtoposes> correspond to such larger topologies; requiring their extra definable covers gives the corresponding deductively closed quotient theory. Pulling the universal model into the <subtopos> supplies the universal model of the quotient.
Given a quotient $\mathbb T'$, transport its <subtopos> along the chosen equivalence of <classifying toposes>. Apply the duality again to obtain a quotient $\mathbb S'$ of $\mathbb S$. Their <classifying toposes> are equivalent, so
$$
\boxed{\mathbb T'\text{ and }\mathbb S'\text{ are Morita-equivalent}.}
$$
This is an explicit transfer principle for whole families of theory extensions and their order relations. Intrinsic constructions such as open, closed or Boolean <subtoposes> can likewise be described in each syntax. Different descriptions may look unrelated, but their equality is explained by the common <subtopos>. No universal translation of individual formulas is asserted without choosing the relevant equivalence and interpretations.
Back to article page
