An open problem in choiceless constructivism is to prove that if a function $f:\mathbb R \to \mathbb R$ is pointwise differentiable everywhere, with $f'=0$, then $f$ is constant. See In choiceless constructivism: If $f'=0$ then is $f$ constant?.
I'm proposing a route to a negative answer to the above conjecture.
Cantor's staircase is a continuous function whose derivative is $0$ almost everywhere, but which is non-constant. The function is constant over intervals $[a/3^n, (a+1)/3^n]$.
What I'm proposing is to construct a function by exploiting the classical countability of the computable numbers $\mathbb R^c$. Let $(u_i)_{i \in \mathbb N} \in (\mathbb R^c)^{\mathbb N}$ be a sequence enumerating the computable numbers. Construct $F:\mathbb R^c \to \mathbb R^c$ as $\lim_{n \to \infty}F_n$ where $(F_n)_{n \in \mathbb N}$ is recursively defined by:
Let $l < u$ be a pair of uncomputable reals in $[0,1]$. Then let: $F_0:[0,l] \cup [u,1] \to \mathbb R^c, x \mapsto \begin{cases}0, & x \in [0,l] \\ 1, & x \in [u,1]. \end{cases}$
$F_{n+1}$ by the following rule: If $u_{n}$ is in the domain of the function $F_n$, then define $F_{n+1} = F_n$. If $u_{n}$ is not in the domain of $F_n$, then pick two uncomputable numbers $l < u$ such that $[l,u]$ is not in the domain of $F_n$ and $l < u_{n} < u$; then define
$$\begin{align} F_{n+1}&:\operatorname{dom}(F_n) \cup [l,u] \to \mathbb R^c,\\ x& \mapsto \begin{cases} \frac{1}{2}(F_n(\sup(\operatorname{dom}(F_n) \cap [0,l])) + F_n(\inf(\operatorname{dom}(F_n) \cap [u,1]))), &x \in [l,u] \\ F_n(x), &x \not \in [l,u]. \end{cases} \end{align}$$
I don't see how an uncomputable number can be obtained from such a function, and therefore how an $x$ can be exhibited for which $F'(x)$ does not exist.
I suppose I'm suggesting that in the sentence $\forall x \in \mathbb R. f'(x)=0$, we mean to quantify only over the computable numbers. So we would need a topos in which $\mathbb R$ is just the computable numbers, perhaps. Maybe externally, the morphisms $\mathbb R \to \mathbb R$ need to correspond to all the continuous functions $\mathbb R^c \to \mathbb R^c$, including the one above.
Notice that in classical logic, the space of computable numbers with the Euclidean topology is totally disconnected. The failure of $f'=0$ to imply that $f$ is constant is then due to total disconnectivity.
Can this be used to settle the conjecture in the negative?
