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?
Best Answer
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.