The Artin-gluing conjecture for replacing an open subtopos

Let $\mathbb{T}$ be a geometric theory, let $\phi$ be a closed formula of $\mathbb{T}$, and let $\mathbb{E}$ be an extension of $\mathbb{T}+\phi$. Write $\mathrm{Set}[\mathbb{T}]$ for the classifying topos of $\mathbb{T}$, and let $\pi_{\phi+\mathbb{E}}$ and $\pi_{\lnot\phi}$ denote the geometric morphisms induced by the corresponding theory extensions. For a left exact functor $G$, write $\operatorname{Gl}(G)$ for its Artin gluing.

Artin-gluing conjecture. The theory $\mathbb{T}+\mathbb{E}/\phi$ is classified by the topos

$$\operatorname{Gl}\Bigl( \mathrm{Set}[\mathbb{T}+\phi+\mathbb{E}] \xrightarrow{{\pi_{\phi+\mathbb{E}}}_*} \mathrm{Set}[\mathbb{T}] \xrightarrow{{\pi_{\lnot\phi}}^*} \mathrm{Set}[\mathbb{T}+\lnot\phi] \Bigr).$$

Equivalently, this asserts that $\mathrm{Set}[\mathbb{T}+\mathbb{E}/\phi]$ is obtained by replacing the open subtopos $\mathrm{Set}[\mathbb{T}+\phi]$ of $\mathrm{Set}[\mathbb{T}]$ with $\mathrm{Set}[\mathbb{T}+\phi+\mathbb{E}]$ in the canonical Artin-gluing construction, using the geometric morphism induced by $\mathbb{E}$.