I am looking for constructively valid references for the following two related facts:
discrete topological spaces are sober,
the points of a locale coproduct are the disjoint union of the points of the cofactors.
Neither is difficult, but nor are they so trivial that a reference might be dispensed with.
Item (1) is, of course, classically contained in the statement that Hausdorff spaces are sober, but, constructively, “sober” is a fairly strong notion (e.g., $\mathbb{Q}$ may fail to be sober even though it is Hausdorff in any reasonable sense of the word). Concerning (2), I am surprised not to find the statement anywhere (e.g., I couldn't find it in Picado & Pultr's book Frames and Locales: Topology without points).
For completeness of MathOverflow, here is a full proof of (1):
Let $X$ be a set: to say that $X$ with the discrete topology $\mathscr{P}(X)$ is sober amounts to saying that frame homomorphisms $\Omega^X \to \Omega$ (where $\Omega := \mathscr{P}(1)$ is the frame of truth values, i.e., the powerset of a singleton $1 = \{\bullet\}$ and of course $\Omega^X$ is isomorphic to $\mathscr{P}(X)$) correspond bijectively to evaluation maps $\hat x\colon \Omega^X \to \Omega, v \mapsto v(x)$ for $x \in X$. It is obvious that $\hat x = \hat y$ implies $x=y$ (just evaluate at $e_x$ defined below), so the real question is whether every frame homomorphism $\Omega^X \to \Omega$ is of this form.
So, consider $\varphi\colon \Omega^X \to \Omega$ a frame homomorphisms. Denote by $e_x \in \Omega^X$ the element given by the map $X \to \Omega$ that is the characteristic function of a singleton, that is, $z \mapsto \{\bullet : z=x\}$, and let $\check\varphi\colon X\to \Omega$ be $x \mapsto \varphi(e_x)$. Since $e_x \wedge e_y \leq \bigvee\{\top : x=y\}$ in $\Omega^X$, we have (a) $\check\varphi(x) \wedge \check\varphi(y) \leq \{\bullet : x=y\}$ in $\Omega$, and since $\bigvee\{e_x : x\in X\} = \top$ in $\Omega^X$, we have (b) $\bigvee\{\check\varphi(x) : x\in X\} = \top$ in $\Omega$. These two facts tell us of the set $S := \{x\in X : \check\varphi(x)\} \subseteq X$ whose characteristic function is $\check\varphi$ that (a) any two elements of $S$ are equal, and (b) $S$ is inhabited (it has an element); so $S$ is a singleton, say $S = \{s\}$. We then have $\check\varphi(x) = \{\bullet : x=s\}$, and more generally, $\varphi(v) = \varphi(\bigvee\{e_x : v(x)\}) = \bigvee\{\check\varphi(x) : v(x)\} = v(s)$ so that $\varphi = \hat s$ is the evaluation at $s$. ∎
(This, of course, uses the principle of unique choice to select $s$ in $S$, so, just to be clear, when I say “constructively”, the principle of unique choice is permissible.)
A proof of (2) can be obtained similarly by analysing frame homomorphisms $\varphi \colon \prod_{i\in I} L_i \to \Omega$ where $(L_i)_{i\in I}$ is a family of frames and $\prod_{i\in I} L_i$ denotes their product (which is the frame of opens of the coproduct locale). As a matter of fact, I believe we can deduce (2) from (1) by considering the composite map $\Omega^I \to L \to \Omega$ of $\varphi$ with the product $\Omega^I \to L := \prod_{i\in I} L_i$ of all morphisms $\Omega \to L_i$ (given by $p \mapsto \bigvee\{\top_{L_i} : p\}$): according to (1), this composite $\Omega^I \to \Omega$ is of the form $\hat\imath$ for some uniquely defined $i\in I$, and then it's easy to see that $\varphi$ factors through the $L_i$ factor (I'm not sure this is much simpler than actually rewriting the proof, though).
I may have been a bit uselessly verbose in the above proof, but I don't think it's entirely trivial either. So, does this already appear somewhere in the literature?
