Locales in constructive mathematics

Question

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:

1. Are these definitions reasonable in a constructive setting?
2. 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.
3. How discrete, Hausdorff, and spatial locales are related? Again, I cannot prove this, but I guess there are no implications between these notions.

Answer 1

For this type of question the first reference that comes to my mind is P.T.Johnstone Sketches of an elephant, part C.

Most of the results in this book are constructively valid: If a result is proved over an arbitrary base (either a topos or a locale), it means that it is constructive, the few non-constructive result present in the book are those that explicit refers to the category "Set".

To answer your more specific questions:

1) One generally says that a locale is discrete if its diagonal map is an open embeddings and if the map $X \rightarrow 1$ is open (in the sense of open morphisms of locales, see for example sketches section C3.1, the second condition is automatic in classical mathematics, but not in constructive mathematics). With this modification they are the standard definitions (at least equivalent to them, we generally don't invoke the Sierpinski locale to define what are open and closed subsets, they just corresponds to the element sof the defining frame).

The only things you might want to be careful about is that for a spatial locale, being Hausdorff in this sense is not exactly equivalent to the fact that the corresponding topological space is Hausdroff, but this is already the case in classical mathematics (because the products in the category of locales might differs from the product in the category of topological spaces).

2) With the modified notion, a locale is discrete if and only if it is the frame of subset of a set. (Lemma C3.1.15 of sketches of an elephant). The corresponding set is decidable if and only if the locale is Hausdorff.

3) Because of point $(2)$ one has that:

Discrete => spatial

and "Discrete => Hausdroff" is essentially equivalent to the law of excluded middle.

But there is no other implications: boolean locales are Hausdorff but not spatial nor discrete, and spatial locale can be both discrete and non discrete and both Hausdorff and non Hausdorff.

This being said, there is one more implication that will be of interest regarding your question:

If $X$ is spatial then the map $X \rightarrow 1$ is open (C3.1.16 in sketches). So with your definition of discrete what is true is that $X$ corresponds to a set if and only if $X$ is discrete and spatial.

Answer 2

PreScriptum. Having almost finished the answer below I saw the answer by Simon Henry which largely subsumes mine. I still decided to post it as it contains some details/proofs, so may be viewed as an addendum to that answer.

Concerning 2.:

First note that $f:X\to Y$ is an open embedding in your sense iff $X$ is up to isomorphism an open of $Y$.

(More precisely this means that there is an $U_X\in\operatorname{Opens}(Y)$ and an isomorphism $i:\operatorname{Opens}(X)\cong\{U\in\operatorname{Opens}(Y)\mid U\subseteq U_X\}$ such that $if^*(\_)=U_X\cap\_$ for the frame homomorphism $f^*:\operatorname{Opens}(Y)\to\operatorname{Opens}(X)$ determining $f$. Proof - if the latter holds then the needed map $Y\to$ Sierpiński corresponds to the frame homomorphism $\{\varnothing,\{o\},\{o,c\}\}\to\operatorname{Opens}(Y)$ sending $\{o\}$ to $U_X$, since the pushout of this map along the homomorphism determining the embedding of the open point into Sierpiński is the quotient of $\operatorname{Opens}(Y)$ by the smallest frame congruence identifying $U_X$ and $Y$; conversely, given such a map $f:Y\to$ Sierpiński, take $U_X=f^{-1}(o)$.)

Next observe that if $\operatorname{Opens}(Y)=\operatorname{Subsets}(S)$, then for any subset $T\subseteq S$ the frame homomorphism $T\cap\_:\operatorname{Subsets}(S)\to\operatorname{Subsets}(T)$ determines an open embedding in $Y$ of an $X$ with $\operatorname{Opens}(X)=\operatorname{Subsets}(T)$.

This in particular applies to $T\subseteq T\times T$ and we are done given that for $\operatorname{Opens}(X)=\operatorname{Subsets}(T)$ and $\operatorname{Opens}(X')=\operatorname{Subsets}(T')$ one has $\operatorname{Opens}(X\times X')=\operatorname{Subsets}(T\times T')$.

For the converse direction (and this also addresses 1. a bit), there is an additional necessary condition: if $\operatorname{Opens}(X)=\operatorname{Subsets}(T)$, then not only the diagonal $X\to X\times X$ but also $X\to\text{point}$ is open (i. e. the image of any open of $X$ under $X\to\text{point}$ is an open subset of the single point locale). Such locales are usually called $\textit{overt}$.

If the logic is not classical, there might exist non-overt locales with open diagonal. For example, if a singleton $\{*\}$ has a non-complemented subset $S\subset\{*\}$, then $S$ determines an open sublocale $U$ of the single point locale with $\operatorname{Opens}(U)=\operatorname{Subsets}(S)$; then this open sublocale has the complementary closed sublocale $C$, and if $C$ would be open too then $S$ would be complemented in $\{*\}$. Now $C$ is an example of a non-overt locale with open diagonal since ($C$ being a sublocale of the single point locale) the image of $C\to\text{point}$ is $C$ and the diagonal $C\to C\times C$ is an isomorphism.

In particular, it follows that there is no set $T$ with $\operatorname{Opens}(C)$ isomorphic to $\operatorname{Subsets}(T)$, since otherwise $C$ would be overt. (Actually $\operatorname{Opens}(C)$ is isomorphic to $\{S'\subseteq\{*\}\mid S'\supseteq S\}$.)