What is the category of internal locales in a topos equivalent to?

Question

I (think) have heard in a conference, in passing, the sentence ''there is an equivalence between internal locales in a topos $\mathbb{S}$ and localic $\mathbb{S}$-topoi''. Is this true in any sense? If yes, there is an inclusion $\mathbf{Loc}(\mathbb{S})\to \mathbf{Topos}/\mathbb{S}$ between the cat. of internal locales in $\mathbb{S}$ and topoi over $\mathbb{S}$...How is it realized - do we take sheaves of some kind? Can someone say a bit more about this?

Answer 1

The 2-category of internal locales in $\mathcal{S}$ is indeed (bi)equivalent to the 2-category of localic $\mathcal{S}$-toposes via the pseudofunctor $L \mapsto \mathbf{Sh}(L)$. This is proved for $\mathcal{S} = \mathbf{Set}$ as Proposition 1.4.4 + 1.4.5 + Theorem 1.4.7 in [Sketches of an elephant, Part C] (see also Corollary 3.3.5 in [Sketches of an elepehant, Part B]), but the arguments are constructive and can be generalised for any base topos $\mathcal{S}$.