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.