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

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?

-

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}$.

-
What is $\mathbf{Sh}$ in the "over $\mathcal{S}$" case? Is it the $\mathcal{S}$-valued sheaves on the internal locale? – FreddieMor_12 Feb 5 '14 at 8:41
What I mean is...Given what you said, Theorem 1.4.7 reads "$\mathcal{E}$ is a localic $\mathcal{S}$-topos if and only if $\mathcal{E}\simeq \mathbf{Sh}(X)$ for some locale $X$" What is $\mathbf{Sh}(X)$ in this case? – FreddieMor_12 Feb 5 '14 at 8:58
Of course. What else could it be? All the details are in the cited book. – Zhen Lin Feb 5 '14 at 8:58
I am sorry if the question was stupid..I am not very familiar with generalizing constructive arguments, I was not sure. This is not my main area of research. Thank you very much. – FreddieMor_12 Feb 5 '14 at 9:02
Before diving into the elephant, you might want to check out the relevant nLab article. – Ingo Blechschmidt Feb 5 '14 at 16:32