Do strict pro-sets embed in locales?

It is well-known that the category of profinite groups (by which I mean Pro(FiniteGroups), i.e. the category of formal cofiltered limits of finite groups) is equivalent to a full subcategory of topological groups, namely those with "profinite topologies." In fact this is a specialization to groups of a more general statement: the category of pro-(finite sets) is equivalent to the category of topological spaces with profinite topologies, via the functor which says "take the limit in the category of topological spaces, where your finite sets all have the discrete topology."

It is proven in the paper "Prodiscrete groups and Galois toposes" by Moerdijk that more generally, the category of pro-groups with surjective transition maps (aka "strict" or "surjective" pro-groups) is equivalent to that of prodiscrete localic groups, i.e. groups in the category of locales which are a cofiltered limit of ordinary groups, regarded as localic groups with discrete topologies. Is there a non-group version of this? Can "strict pro-sets" be identified with "pro-discrete locales"?

Note that some hypothesis such as "surjective transition maps" is necessary. For instance, the pro-set $\cdots \xrightarrow{+1} \mathbb{N} \xrightarrow{+1} \mathbb{N} \xrightarrow{+1} \mathbb{N}$ is not isomorphic to the trivial pro-set ∅, but its limit in the category of locales is just as empty as its limit in the category of sets.

-
A word of caution. It is not true that the (2-)category of pro(finite groupoids) is equivalent to the (2-)category of groupoids in the category of profinite topologies. An example is the following. Take, for example, the circle $S$. Let $X$ be the Chech compactification of the discrete space under $S$, and $X\to S$ the canonical surjection. Then $X \times_S X \rightrightarrows X$ is a groupoid in (profinite spaces), which is not equivalent to $\hat{\mathbb Z}\rightrightarrows 1$, the profinite completion of the integers. But they represent the same functor (continued) – Theo Johnson-Freyd Dec 13 '10 at 23:58
(continuation) from finite groupoids (thought of as topological groupoids) to groupoids. I.e. they represent the same pro(finite groupoid). I learned this counterexample from Alex Chirvasitu, with whom I'm doing a joint project and we would be much happier if they were the same. (There are some old papers that seem to say the question of whether (pro(finite groupoid)) = ((profinite) groupoid) was open; I don't know if this example is new to Alex.) So the point is: there's something special about the result for groups. ((Oh, and "Chech" in my previous comment is of course "Cech".)) – Theo Johnson-Freyd Dec 14 '10 at 0:01
By the way, since StoneTop is equivalent to Pro(FinSet), it must be that Gpd(StoneTop) is equivalent to Gpd(Pro(FinSet)). I guess the point is that neither of these is equivalent to Pro(Gpd(FinSet)), in contrast to how Grp(Pro(FinSet)) is equivalent to Pro(Grp(FinSet)). It may be worth noting that in VI.2 of Stone spaces, Johnstone gives general conditions on a finitary algebraic theory T which ensure that T-Alg(Pro(FinSet)) is equivalent to Pro(T-Alg(FinSet)), along with some T for which this fails. Of course groupoids are not a finitary algebraic theory in this sense. – Mike Shulman Dec 14 '10 at 18:00
And when I say "hom of topological groupoids" I don't mean a topological functor, but a left-principal bibundle, because when I say "groupoid" I really mean "stack that it represents". – Theo Johnson-Freyd Dec 15 '10 at 7:55
Moerdijk gives examples of the same sort showing that a profinite groupoid is not the same thing as a groupoid in Stone Spaces in the AMS memoir Proper maps of toppers. He basically shows if R s a closed equivalence relation on a Stone space X which is not open, then the associated groupoid is not profinite. He argues by looking at the classifying topos, but one can see it directly. – Benjamin Steinberg Jun 28 '11 at 2:12

First note that if $(S_i)_i$ is a pro-set, which we may WLOG assume to be indexed on a directed poset, then the corresponding prodiscrete locale $\lim S_i$ is presented by the following posite. Its underlying poset is the category of elements of the diagram $(S_i)_i$, i.e. its elements are pairs $(i,x)$ with $x\in S_i$ and we have $(i,x)\le (j,y)$ if $i\le j$ and $s_{i j}(x)=y$, where $s_{i j} \colon S_i \to S_j$ is the transition map. The covers are generated by $(i,x) \lhd s_{i j}^{-1}(x)$ for any $i,j,x$.
Thus, the open sets in $\lim S_i$ are the "ideals" for this coverage, i.e. sets $A$ of pairs $(i,x)$ which are down-closed and such that if $(j,y)\in A$ for some $j$ and all $y\in s_{i j}^{-1}(x)$, then $(i,x)\in A$.
Now consider morphisms $S\to 2$, where $2=\{\bot,\top\}$, regarded as a pro-set in the trivial way, giving rise to a discrete locale. A morphism of pro-sets $S\to 2$ is determined by a partition of some $S_i = S_i^\bot \sqcup S_i^\top$ (modulo a suitable equivalence relation as we change $i$). But a morphism of locales $\lim S_i \to 2$ consists of two ideals $A^\bot$ and $A^\top$ which are disjoint and whose union generates the improper ideal (which consists of all pairs $(i,x)$). A pro-set morphism $S\to 2$ induces a locale map $\lim S_i \to 2$ where $A^\bot$ and $A^\top$ are the ideals generated by $S_i^\bot$ and $S_i^\top$, but in general not every morphism $\lim S_i \to 2$ is induced by one $S\to 2$.
Specifically, consider the following pro-set, which is indexed on the natural numbers with the inverse ordering: $$\dots \to S_i \to \dots \to S_2 \to S_1 \to S_0$$ We define $S_i = (\mathbb{N} \times \{a,b\}) / \sim_i$, where $\sim_i$ is the equivalence relation generated by $(k,a)\sim_i (k,b)$ for $k\ge i$. The transition maps are the obvious projections, which are surjective. Define $$A^\bot = \{ (i,(k,a)) | k < i \} \quad\text{and}\quad A^\top = \{ (i,(k,b) | k < i \}.$$ Then $A^\bot \cup A^\top$ generates the improper ideal, since for any $i$ we have $\{ (i+1, (i,a)), (i+1,(i,b)) \} \subset A^\bot \cup A^\top$, which covers $(i,(i,?))$, which covers $(i-1,(i,?))$, and so on down to $(0,(i,?))$. However, no $S_i$ can be partitioned as $S_i = S_i^\bot \sqcup S_i^\top$ in such a way that $S_i^\bot$ generates $A^\bot$ and $S_i^\top$ generates $A^\top$. Thus, this defines a locale map $\lim S_i \to 2$ which does not arise from a pro-set morphism $S\to 2$.