# Is there a classifying topos for locales?

Is there a Grothendieck topos $$F$$ such that, for any Grothendieck topos $$E$$, the category of geometric morphisms $$E\rightarrow F$$ is equivalent to the category of locales internal to $$F$$?

I suspect that such an $$F$$ doesn't exist, because the definition of locale doesn't look to me like it can be formalised as a geometric theory. But it would be nice if there was such a classifying space, since the locales internal to a topos are interesting objects. In particular, if $$X$$ is a locale then the locales internal to $$\mathrm{Sh}(X)$$ correspond bijectively with bundles over $$X$$, i.e. pairs $$(Y,f)$$ where $$Y$$ is a locale and $$f:Y\to X$$.

• Excellent question. I too suspect that such an $F$ doesn't exist. If you're satisfied with essential surjectivity instead of equivalence, and if you're okay with switching to the dual category, then I can propose a substitute: the classifying topos of frame presentations. Every frame arises from a frame presentation, though not uniquely so. Details in frame presentations are for instance in a fine paper by Steve Vickers on the double powerlocale, Section 5, there called GRD system and cast in the language of geometric logic. – Ingo Blechschmidt Sep 28 '18 at 8:04
• @IngoBlechschmidt The following occurred to me, I guess it must be well known. The internal locales do respect pullback: if $E\to F$ is a geometric morphism then we get a canonical functor from the category of locales internal to F to the category of locales internal to E. In other words we have a functor $\mathrm{Locale}:\mathbf{Topos}^\text{op}\to\mathbf{Cat}$. – Oscar Cunningham Oct 3 '18 at 11:09
• @IngoBlechschmidt But $\mathbf{Topos}^\text{op}\to\mathbf{Cat}$ is the free cocompletion of $\mathbf{Topos}$, and $\mathbf{Topos}$ is already cocomplete. So there should be some sort of canonical "geometriztation" of $\mathrm{Locale}$ achieved by applying the functor $(\mathbf{Topos}^\text{op}\to\mathbf{Cat})\to\mathbf{Topos}$. Can we describe what this is? – Oscar Cunningham Oct 3 '18 at 11:09
• Maybe there are size issues... – Oscar Cunningham Oct 4 '18 at 10:43
• Ah, I see. The problem is that since $\mathbf{Topos}$ is large, it's free small-cocompletion isn't $\mathbf{Topos}^\text{op}\to\mathbf{Cat}$. – Oscar Cunningham Oct 5 '18 at 14:36