Are constant functions continuous in constructive mathematics?

Question

The standard proof that a constant function $c: X \to Y$, $x \mapsto y_0$ is continuous proceeds as follows: if $U \subseteq Y$ is open, then either $c^{-1}(U)=X$ if $y_0 \in U$, or $c^{-1}(U)=\emptyset$ if $y_0 \notin U$. Either way, $c^{-1}(U)$ is open.

Since this proof apparently uses excluded middle, it is not valid as written in constructive mathematics. But constant functions ought to be continuous, so what is the correct proof?

Answer 1

Let $A$ be the set $\{0 : c \in U\}$. Classically, this set is empty if $c \not\in U$ and a singleton if $c \in U$, but intuitionistically, it may not be either.

Nonetheless, we can define a family of sets on $A$. For $a \in A$ let $X_a$ be $X$.

Now $c^{-1}(U) = \bigcup_{a \in A} X_a$ which is a union of open sets, so is open.

Answer 2

Let $x \in f^{-1}[O]$. Then $c=f(x) \in O$. If now $x' \in X$ is arbitrary, $c=f(x') \in O$ as well. It follows that $f^{-1}[O]=X$, which is open.

Put alternatively, for any $x \in f^{-1}[O]$ we have a neighbourhood (namely $X$) that sits inside it. So all points of $f^{-1}[O]$ are interior points. QED.