Defining function by overlapping cases in constructive logic Is it possible to define a function by cases in intuitionistic logic where the cases possibly overlap and the function values disagree in the overlapping area? In particular, if I am working with real values, then I might have proof of $\forall x \in \mathbb{R}, x > 2 \lor x < 3$. Is it valid to define a function as follows?
$$
 f : \mathbb{R} \to \mathbb{N},\quad x \mapsto 
\begin{cases} 
 1 & \text{if } x > 2 \\
 0 & \text{if } x < 3
\end{cases}
$$
On the one hand, if I am thinking in terms of the Brouwer-Heyting-Kolmogorov interpretation, then the statement $\forall x \in \mathbb{R}, x > 2 \lor x < 3$ gives me a pair $(0, p(x))$ or $(1, q(x))$ (where $p(x)$ is a proof of $x > 2$ and $q(x)$ is a proof of $x < 3$), which I could then use to decide between the two cases. On the other hand, the function above is not classically well-defined: for $x = 2.5$, then $f(x) = 1$ and $f(x) = 0$, which breaks extensionality. Classically, I could repair the above definition by writing
$$
\tilde{f} : \mathbb{R} \to \mathbb{N}, \quad x \mapsto \begin{cases}
 1 & \text{if } x > 2 \\
 0 & \text{if } \neg(x > 2) \land x < 3
\end{cases},
$$
essentially by asserting that the cases were exclusive. This trick doesn't work constructively though, since I don't necessarily have a proof that $\forall x \in \mathbb{R}, x > 2 \lor \neg(x > 2)$.
Is such a definition valid in a constructive setting, then? If not, what modifications can I make to obtain a similar result?
 A: I've seen two constructs in such a context with a finite set of exhaustive cases, and a function for each case that takes the case as its domain:
>When all of the functions agree on the overlap of their domains, the construction pans out well, as you point out. That is to say, the functions are compatible, and the resulting function is the gluing of these functions—this is standard stuff you see in, for instance, sheafs of continuous functions.
>When it is not known whether the functions are compatible, I've seen the following type of workaround, which is usually phrased like this:

If $X=X_1\cup\cdots\cup X_n$, then given any $x\in X$, there is a way to effectively find an integer $k$ with $1\leq k\leq n$ and $x\in X_k$. This effective procedure can be described as a function $h:X\to\lbrace 1,\cdots, n\rbrace$ such that $x\in X_{h(x)}$ for all $x\in X$. Hence, if $f_k:X_k\to Y$ for each natural $k$ with $1\leq k\leq n$, one may define $$f(x)=f_{h(x)}(x).$$

As you may be aware, the "procedure" being symbolized as $h$ here may not be functional—for example, if $X$ were the natural numbers, then $h(2+2)$ and $h(4)$ could yield different results. So the assertion that such a functional $h$ exists is a form of choice principle; as it turns out, you will only see this type of argument in use when $X$ is countable, and this is due to a lot of constructivist schools tending to accept countable choice. Hence, this construct depends on if you accept countable choice or not—and of course it depends on whether $X$ is countable or not.
In general, it's important to consider the topology of the sets being involved, as that is intimately related to the ways in which you can probe the space, its regions and its points. Thus, the method that is most reliable and natural with this outlook is, evidently, the gluing of compatible maps.

Post scriptum. Some people also take care, in the case of map gluing, to mention that this also utilizes a choice principle: the principle of unique choice. I do not know much about the specifics of math without this principle, and most constructivists I know are fine with using it. It looks like the MathOverflow post is a good start, though.
