regular, coherent, geometric) theory over a signature $\Sigma$. We denote by ${\cal C}_{\mathbb T}^{\textrm{cart}}$ (resp. ${\cal C}_{\mathbb T}^{\textrm{reg}}$, ${\cal C}_{\mathbb T}^{\textrm{coh}}$, ${\cal C}_{\mathbb T}^{\textrm{geom}}$) the cartesian (resp. regular, coherent, geometric) syntactic category of $\mathbb T$ and by $J^{\textrm{reg}}_{\mathbb T}$ the regular (resp. coherent, geometric) topology on ${\cal C}_{\mathbb T}^{\textrm{reg}}$ (resp. ${\cal C}_{\mathbb T}^{\textrm{coh}}$, ${\cal C}_{\mathbb T}^{\textrm{geom}}$). Recall from [@El2] that if $\mathbb T$ is cartesian (resp. regular, coherent, geometric) then $[{{\cal C}_{\mathbb T}^{\textrm{cart}}}^{\textrm{op}}, {{\bf Set }}]$ (resp. ${{\bf Sh}}({\cal C}_{\mathbb T}^{\textrm{reg}}, J^{\textrm{reg}}_{\mathbb T})$, ${{\bf Sh}}({\cal C}_{\mathbb T}^{\textrm{coh}}, J^{\textrm{coh}}_{\mathbb T})$, ${{\bf Sh}}({\cal C}_{\mathbb T}^{\textrm{geom}}, J^{\textrm{geom}}_{\mathbb T})$) is a classifying topos for $\mathbb T$. Let us denote by $y^{\textrm{cart}}_{\mathbb T}:{\cal C}^{\textrm{cart}}_{\mathbb T}\to [{{\cal C}_{\mathbb T}^{\textrm{cart}}}^{\textrm{op}}, {{\bf Set }}]$ (resp. $y^{\textrm{reg}}_{\mathbb T}:{\cal C}^{\textrm{reg}}_{\mathbb T}\to {{\bf Sh}}({\cal C}_{\mathbb T}^{\textrm{reg}}, J^{\textrm{reg}}_{\mathbb T})$, $y^{\textrm{coh}}_{\mathbb T}:{\cal C}^{\textrm{coh}}_{\mathbb T}\to {{\bf Sh}}({\cal C}_{\mathbb T}^{\textrm{coh}}, J^{\textrm{coh}}_{\mathbb T})$, $y^{\textrm{geom}}_{\mathbb T}:{\cal C}^{\textrm{geom}}_{\mathbb T}\to {{\bf Sh}}({\cal C}_{\mathbb T}^{\textrm{geom}}, J^{\textrm{geom}}_{\mathbb T})$) the Yoneda embeddings.

Let us introduce the following notions. Below, by a $\mathbb T$-provably functional geometric formula from $\{\vec{x}. \phi\}$ to $\{\vec{y}. \psi\}$ we mean a geometric formula $\theta(\vec{x}, \vec{y})$ such that the sequents $(\phi \vdash_{\vec{x}} (\exists \vec{y})\theta)$, $(\theta \vdash_{\vec{y}, \vec{x}} \phi \wedge \psi)$ and $(\theta \wedge \theta[\vec{z}\slash \vec{y}] \vdash_{\vec{x}, \vec{y}, \vec{z}} \vec{y}=\vec{z})$ 