Is there a good theory of 2-locales?

Question

Topological spaces and locales are two closely related notions meant to capture the concept of an abstract space, the latter of which admits a certain "noncommutative" generalisation known as a quantale. Out of these three notions, topological spaces and quantales admit clear 1-categorical analogues, coming from viewing powersets $\mathcal{P}(X)=\mathsf{Set}(X,\{\mathrm{true},\mathrm{false}\})$ as the 0-categorical analogue of presheaf categories $\mathsf{PSh}(\mathcal{C})=\mathsf{Cat}(\mathcal{C}^\mathsf{op},\mathsf{Set})$:

• The 1-categorical analogue of a topological space is a Grothendieck topos, since:
  • A Grothendieck topos is a left exact reflective subcategory of $\mathsf{PSh}(\mathcal{C})$;
  • A topology on a set $X$ is a left exact reflective subcategory of the powerset $\mathcal{P}(X)$ of $X$, viewed as a poset; (see Edit)
• The 1-categorical analogue of a quantale is a "compatibly monoidal cocomplete category", since:
  • A quantale is a monoid in suplattices, the algebras for the powerset monad;
  • A compatibly monoidal cocomplete category is a pseudomonoid in cocomplete categories, the algebras for the presheaf category relative monad.

We have thus assembled the following table:

Topological Spaces	Locales	Quantales
Grothendieck Topoi	?	Compatibly Monoidal Cocomplete Categories

Question 1: What would be the appropriate notion filling the "?" spot in the table above?

It seems to me that one plausible definition of a "2-locale" would be that of a "Cartesian compatibly monoidal cocomplete category", much like locales are quantales whose product is given by the meet (Cartesian product).

Question 2: Has anyone tried developing such a "theory of 2-locales" in this sense?

---

Edit: I've just realised that a left exact reflective subcategory of $\mathcal{P}(X)$ is actually a different structure (although similar) to that of a topological space. See these two other questions: [1] [2].

Answer 1

A standard answer is in fact that Grothendieck toposes are categorified locales, with the argument that a Grothendieck topos that lacks enough points is not a tight generalization of a topological space, noting that the set $X$ of points has no analogue in your analogy between a Grothendieck topos and a space. Seen another way, if you look at the left exact reflective subcategories of presheaves on a poset, i.e. $(0,1)$-categories, then you've got locales.

According to Garner, a categorified topological space should instead by an ionad, which under an accessibility condition is closely related to a Grothendieck topos with enough points. One reason your proposal for a 2-locale might be questioned is that your conditions don't imply any adjoint functor theorem, so that your 2-locales need not be complete, though locales always are.