is irreducible in ${{\bf Sh}}({\cal C}_{\mathbb T}^{\textrm{geom}}, J^{\textrm{geom}}_{\mathbb T})$ then, denoted by $\cal G$ the full subcategory of ${\cal C}_{\mathbb T}^{\textrm{geom}}$ on the cartesian formulae, equivalently the cartesian syntactic category ${{\cal C}_{{\mathbb T}'}^{\textrm{cart}}}$ of the cartesianization ${\mathbb T}'$ of $\mathbb T$ (i.e. the theory axiomatized by all the cartesian sequents over $\Sigma$ which are provable in $\mathbb T$), we have that $\cal G$ is $J^{\textrm{geom}}_{\mathbb T}$-dense (by Lemma D1.3.8 [@El2]) and $J^{\textrm{geom}}_{\mathbb T}|_{\cal G}$ is the trivial Grothendieck topology. Thus the Comparison Lemma yields an equivalence ${{\bf Sh}}({\cal C}_{\mathbb T}^{\textrm{geom}}, J^{\textrm{geom}}_{\mathbb T})\simeq [{{\cal C}_{{\mathbb T}'}^{\textrm{cart}}}^{\textrm{op}}, {{\bf Set }}]$. Clearly, this equivalence sends the universal model of $\mathbb T$ in ${{\bf Sh}}({\cal C}_{\mathbb T}^{\textrm{geom}}, J^{\textrm{geom}}_{\mathbb T})$ to the universal model of ${\mathbb T}'$ in $[{{\cal C}_{{\mathbb T}'}^{\textrm{cart}}}^{\textrm{op}}, {{\bf Set }}]$, and hence, universal models being conservative, $\mathbb T$ and ${\mathbb T}'$ prove exactly the same geometric sequents over $\Sigma$ i.e. they are equivalent, as required.

The ‘only if’ direction in the following result extends Lemma D3.3.11 [@El2].

\[Onetoposmany\_regcrit\] Let $\mathbb T$ be a geometric theory over a signature $\Sigma$. Then $\mathbb T$ is equivalent to a regular theory if and only if for any regular formula $\{\vec{x}. \phi\}$ over $\Sigma$, for 