What locales correspond to Manifolds? I am studying the categorical equivalence between (sober) topological spaces and (spatial) locales with enough points. As the title implies, I am interested in finding localic analogues of both topological and smooth manifolds. Since an (smooth) $n$-manifold is  a paracompact, Hausdorff, locally Euclidean space equipped with an (smooth) atlas, we just need to translate all these technicalities to their lattice theoretic counterparts to find the localic version of manifolds.
I am pretty sure that somebody has work through all the details before, but couldn't find any reference for this on google. Can someone help me with this?
 A: I recently got interested in the same question. You've probably come across Picado & Pultr's Frames & Locales where they describe these technicalities but not in the context of putting them together to describe manifolds.
In particular they describe how compactness, local compactness and paracompactness have clean translations into localic language as well as regularity, complete regularity and normality. However, the Hausdorff notion doesn't translate as cleanly.
They also describe the locale of reals. We can take the localic product to obtain the locale of Cartesian spaces and since the reals are sober and locally compact, this is equivalent to the usual topology on Cartesian spaces.
One technicality to note is that sublocales of spatial locales (these are the locales that correspond to topological spaces) need not be, and mostly aren't, spatial. And another is that there is always a smallest dense sublocale. Personally, I'm curious as to what this adds to manifold theory.
Now we could attempt to translate the classical geometric description of a manifold, via atlases and charts, into locale language. But there are other approaches to smooth structure that might be more appropriate. In particular, a diffeology on a space is a concrete sheaf on the Cartesian site. Its a generalisation of smooth manifold theory where charts are replaced by plots, the distinction being that whilst charts yield the local Euclidean structure by exhibiting a homeomorphism with a Cartesian open, plots weaken this by dropping the local injectivity. Moreover, charts are based upon a single Cartesian dimension whilst plots need not be. One other important point is that with the usual manifold theory we begin with a topological space. This structure isn't neccessary here. Diffeology instead induces its own topology on the resulting smooth structure - the D-topology.
Since locales are already Grothendieck (0,1)-topoi and taking sheaves on a locale is fully faithful (unlike in Top), arguably, this seems, at least to me, to be likely the smoother approach.
