I've seen texts that talk about topological spaces being essentially locales, like Topology via Logic by Vickers, and texts related to homotopy theory that talk about topological spaces being essentially infinity-groupoids.
However, I've never seen any treatment of topology that combines these perspectives or talks about the relationship between locales and infinity-groupoids. Where should I be looking?
I don't think it's a good idea to mix the slogans "topological spaces are locales" and "topological spaces are $\infty$-groupoids." I think the former slogan encapsulates what we ended up defining as topological spaces while the latter slogan encapsulates what we should've defined as topological spaces, at least if we're algebraic topologists (recall that $\infty$-groupoids are only supposed to capture topological spaces up to, say, weak homotopy equivalence).
But let me make a guess anyway: the answer should be "higher sheaf theory." The story for $1$-types should be that the category of locally constant sheaves on a locale is equivalent to the category of functors from a (pro?-)groupoid to $\text{Set}$. This groupoid can be recovered by a suitable version of Tannaka reconstruction and should be regarded as the fundamental groupoid of the locale (although this won't agree with the fundamental groupoid in the ordinary sense without some local connectivity assumptions). To get the fundamental $2$-groupoid we need to consider locally constant $2$-sheaves (stacks?), whatever those are, and that should be equivalent to the category of $2$-functors from a $2$-groupoid to $\text{Gpd}$. And so forth. There are some nLab articles suggesting that someone has worked all this out.
