Here's a constructive proof of the approximate Intermediate Value Theorem from pointwise continuity, not relying on Dependent Choice and not relying on a setoid construction of the reals.
Theorem: If $f$ is pointwise continuous with $f(a)<0, \ f(b)>0,\ \epsilon>0$ then there is some $x$ with $|f(x)|<\epsilon$.
Proof: Define the following inductively:
$$a_1 = a$$
$$b_1 = b$$
$$c_n = (a_n+b_n) / 2$$
$$d_n = \max( 0, \min( \textstyle\frac{1}{2}+ \frac{ f(c_n)}{\epsilon}, 1))$$
$$a_{n+1} = c_n - d_n (b-a)/2^n $$
$$b_{n+1} = b_n - d_n (b-a)/2^n$$
Then $b_n - a_n = (b-a)/2^{n-1}.$
So the $c_n$'s converge to some $c.$
By pointwise continuity at $c$,
let $\delta$ be such that $ |x-c|<\delta$
implies $|f(x)-f(c)| < \epsilon.$
Claim:
For any $m\in\mathbb{N}$, either (i) $\exists j \le m,\ |f(c_j)| < \epsilon$
or (ii) $f(a_m) < 0 $ and$ f(b_m) > 0$.
Proof of theorem from claim:
Choose $c_m$ such that $|c-c_m| < \delta / 2$ and $(a-b)/2^m < \delta / 2$, and apply the claim.
In the first case of the claim, the theorem is immediate.
In the second case of the claim,
$$ |c-a_m| \le |c-c_m| + |c_m-a_m| < \delta, \text{ so }|f(c)-f(a_m)| < \epsilon$$
$$ |c-b_m| \le |c-c_m| + |c_m-b_m| < \delta, \text{ so }|f(c)-f(b_m)| < \epsilon$$
So $f(c)$ is within $\epsilon$ of both a negative and a positive number, and $|
f(c)| < \epsilon$, QED.
Proof of claim by induction on $m$.
The base case is given by $ f(a) < 0, \ f(b) > 0.$
Now assume the claim for $m$. In case (i), for some $ j < m,\ |f(c_j)| < \epsilon$, and the inductive step is trivial.
In case (ii), use trichotomy with either
$f(c_m) < -\epsilon/2, \ |f(c_m)| < \epsilon$, or $f(c_m) > \epsilon/2.$
If $|f(c_m)| < \epsilon$, then the inductive step is again trivial.
If $f(c_m) > \epsilon/2$, then
$$d_m = 1$$
$$a_{m+1} = a_m, \text{ so }f(a_{m+1}) < 0$$
$$b_{m+1} = c_m,\text{ so } f(b_{m+1}) > 0$$
If $f(c_m) < - \epsilon/2$, then
$$d_m = 0$$
$$a_{m+1} = c_m, \text{ so }f(a_{m+1}) < 0$$
$$b_{m+1} = b_m,\text{ so } f(b_{m+1}) > 0$$
QED (claim and theorem).
I think this one works; I look forward to seeing what MO says.
Best Answer
Suppose you have a classical classification theorem saying
Then you cannot exhibit constructively a $C$ which is neither $A$ nor $B$ because every constructive proof is also classical, and so that would contradict the classical classification.
What happens instead is that the classical meaning of “$p$ or $q$” corresponds to the constructive “not ($\neg p$ and $\neg q$)“ so the constructive reading of the classical classification theorem is
To give you an idea on how to play tricks with excluded middle in constructive mathematics, consider any proposition $p$ and define $$K_p = \{ z \in \mathbb{C} \mid p \Rightarrow z \in \mathbb{R} \}.$$ It is easy to check, regardless of what $p$ is, that $K_p$ is a subfield of $\mathbb{C}$.
Moreover, if $p$ holds then $K_p = \mathbb{R}$, and if $\neg p$ holds then $K_p = \mathbb{C}$. But stating that $K_p$ is either $\mathbb{R}$ or $\mathbb{C}$ implies $\neg \neg p \lor \neg p$, which lets us decide $\neg p$, which is not generally possible in constructive mathematics. It is still the case that $K_p$ cannot be different from both $\mathbb{R}$ and $\mathbb{C}$, because that amounts to $\neg (\neg p \land \neg\neg p)$, which is constructively true (obviously).
Consequently, if Solèr’s theorem were true constructively (in the version that says that every structure is either this or that), we could decide $\neg p$: just ask the theorem to classify $K_p$ for you.
The usual solution to the conundrum is to strengthen the assumptions to something that does not matter classically. For example, you might want to assume that the vector space $E$ featuring in the definition of a Hermitian form has a given basis, and that the basis has size which is either a natural number or is countably infinite (this cannot be shown to hold for $K_p$ above seen as a real vector space). But that is only the first step, there will be further complications, and one would have to dig into the details of the classification theorem. Unfortunately, I do not know whether anyone has done so.