It is well known that locales are much more well behaved in a constructive setting than topological spaces. Nevertheless, many authors develop the theory of locales in classical mathematics. Are there any textbooks in which the theory is treated constructively?

I'm actually interested in specific questions. First, let us define a map of locales to be an open (resp., closed) embedding if it is a pullback of the open (resp., closed) point of the Sierpiński locale. We say that a locale $X$ is discrete if the diagonal $X \to X \times X$ is open. We say that $X$ is Hausdorff if the diagonal is closed. Now, my questions are:

- Are these definitions reasonable in a constructive setting?
- Is it true that the locale corresponding to the frame of subsets of a set is discrete? I think I can prove this for discrete sets (that is, sets with decidable equality). Also, are there some implications in the converse direction? My guess is that the answer to both questions is "no", but I don't have any counterexamples.
- How discrete, Hausdorff, and spatial locales are related? Again, I cannot prove this, but I guess there are no implications between these notions.

3more comments