Solution (source code)

= Solution

Use the order on <locale> maps in which $f\leq g$ means $f^*(a)\leq g^*(a)$ for every open $a$. A <Hausdorff locale> has a closed diagonal in its localic square. A <totally unordered locale>, or $T_U$ <locale>, has discretely ordered hom-sets: every comparable pair of maps with any common domain is equal.

In the localic square of $Y$, let
$$
N=\bigvee_{a\wedge b=0}a\times b.
$$
This is the largest open disjoint from the diagonal: inverse image along the diagonal sends the rectangle $a\times b$ to $a\wedge b$. Hence $N$ is the <complement> of its closure. If $f\leq g$, then
$$
(f,g)^*(a\times b)=f^*(a)\wedge g^*(b)\leq g^*(a)\wedge g^*(b)=0
$$
for every summand of $N$. Thus $(f,g)$ factors through the closure of the diagonal. For a <Hausdorff locale> that closure is the diagonal itself, so $f=g$. This proof of \b[Hausdorff implies $T_U$] does not require classical logic.

Here is an explicit classical counterexample to the converse implication from spatial Hausdorffness. Give $\mathbb R$ the <topology> generated by the usual opens and by $\mathbb Q$. Every open has the form $U=V\cup(W\cap\mathbb Q)$, where $V,W$ are usual open sets and we may arrange $V\subseteq W$. The <topology> is finer than the usual one, so the space is <Hausdorff>. Put $B=\operatorname{RO}(\mathbb R)$, the <complete Boolean algebra> of ordinary <regular open elements>, and write $\rho(V)=\operatorname{int}\overline V$. Restriction from this space to its rational and irrational subspaces, followed by Booleanization, gives <frame homomorphisms>
$$
f^*(U)=\rho(V),\qquad g^*(U)=\rho(W),\qquad\mathcal O(X)\longrightarrow B.
$$
To justify these formulas, each subspace has its ordinary <subspace topology> and is dense in the ordinary real line. Regular-open algebras of a space and a dense subspace are isomorphic: restrict a regular open and take its interior-closure, with inverse obtained by taking interior-closure in the ambient space. Restriction is a <frame homomorphism>, and double negation is a <frame homomorphism> into its fixed-element <frame>. These observations also show independence of the chosen representation of $U$. Since $V\subseteq W$, we have $f^*\leq g^*$, but $f^*(\mathbb Q)=0$ and $g^*(\mathbb Q)=1$. Thus \b[this Hausdorff space fails $T_U$ as a <locale>].

For the remaining arguments about <connected locales>, use the classical-logic option: <positive opens of a locale> are exactly the nonzero opens. There is a necessary positivity qualification. The empty <locale> has no positive opens, so the printed condition on those opens holds vacuously, although no point $1\to\varnothing$ exists. The point assertions therefore require $X$ to be positive. This qualification is automatic if “totally connected” includes nonemptiness; otherwise it must be added explicitly.

Let $X$ be positive and satisfy the condition on its <positive opens of a locale>. Put $F=\{a\in\mathcal O(X):a\ne0\}$. It contains $1$, excludes $0$, and is upward closed. If $a,b\in F$ had $a\wedge b=0$, their union would be a <positive open of a locale> with a decomposition into two disjoint nonzero opens, contradicting its being a <connected locale>. Thus $a\wedge b\in F$. If $\bigvee_i a_i\ne0$, not all $a_i$ can be zero; classical logic supplies a nonzero summand. Hence \b[$F$ is a <completely prime filter>], and its characteristic <frame homomorphism> defines a point $p:1\to X$.

The point is dense. Indeed $p^*(a)=0$ implies $a=0$ by the definition of $F$. In nucleus language the image of $p$ has nucleus $p_*p^*$; its value at $0$ is $p_*(0)=0$, so the image is a <dense sublocale>.

Conversely suppose an <open locale> has a dense point $p$. Density means $p^*(a)=0$ only if $a=0$, and classically this implies $p^*(a)=1$ for every <positive open of a locale>. If a positive open $u$ split as $a\vee b=u$ with $a\wedge b=0$ and both summands nonzero, then $p^*(a)=p^*(b)=1$, contradicting preservation of their <meet>. Thus every <positive open of a locale> is a <connected locale>, proving the converse under the declared logical convention.

Let $x:X\to1$ be the terminal map. For a positive <totally connected locale> $X$, the point above satisfies
$$
a\leq x^*p^*(a)\quad(a\in\mathcal O(X)),
$$
because the right side is $1$ when $a\ne0$ and both sides are $0$ otherwise. Hence $1_X\leq px$. If $f:X\to Y$ and $Y$ is a <totally unordered locale>, composition gives $f\leq fpx$, so $f=fpx$. Therefore
$$
\boxed{f=(fp)\circ x,}
$$
which is the required constant factorization. For the empty source the factorization need not exist: the unique map $\varnothing\to\varnothing$ does not factor through $1$. Thus the positivity qualification matters for this assertion too.