those surjective functions with . Of course, there are no such surjective functions , and this is not a spatial locale. The theory of locales We have seen that we have a functor from the category of topological spaces and continuous maps to the category of locales. If we restrict this functor to the full subcategory of sober spaces, we obtain a full embedding of the category of sober spaces and continuous maps into the category of locales. In this sense, locales are generalizations of sober spaces. It is possible to translate most concepts of point-set topology into the context of locales, and prove analogous theorems. Some important facts of classical topology depending on choice principles become choice-free (that is, constructive, which is, in particular, appealing for computer science). Thus for instance, arbitrary products of compact locales are compact constructively (this is Tychonoff's theorem in point-set topology), or completions of uniform locales are constructive. This can be useful if one works in a topos that does not have the axiom of choice. Other advantages include the much better behaviour of paracompactness, with arbitrary products of paracompact locales being paracompact, which is not true for paracompact spaces, or the fact that subgroups of localic groups are always closed. Another point where topology and locale theory diverge strongly is the concepts of subspaces versus sublocales, and density: given any collection of dense sublocales of a locale , their intersection is also dense in . This leads to Isbell's density theorem: every locale has a smallest dense sublocale. These results have no equivalent in the realm of topological spaces. See also Heyting algebra. Frames turn out to be the same as complete Heyting algebras (even though frame homomorphisms need not be Heyting algebra homomorphisms.) Complete Boolean algebra. Any complete Boolean algebra is a frame (it is a spatial frame if and only if it is atomic). Details on the relationship between the category of topological spaces and the category of locales, including the explicit construction of the equivalence between sober spaces and spatial locales, can be found in the article on Stone duality. Whitehead's point-free geometry. Mereotopology. Citations Bibliography A general introduction to pointless topology is This is, in its own words, to be read as the trailer for Johnstone's monograph (which appeared already in 1982 and can still be used for basic reference): Johnstone, Peter T. (1982). Stone Spaces. Cambridge University Press,