Constructive proofs of existence in analysis using locales
[I don't have enough points to comment; this is just a partial answer, at best]
Steve Vickers' paper https://www.cs.bham.ac.uk/~sjv/CViet.pdf has a constructive version of 1 (IVT). Theorem 41 in Section 7.3 (page 37). Broadly, the view taken there is that 'there exists $x$ such that $f(x)=0$' is interpreted as 'the inf of the modulus of $f$ is zero'. The paper also talks about a number of other issues that are being discussed in this thread.
I claim that the following result have constructive* proof:
1) Let $f : [0,1] \rightarrow \mathbb{R}$ be a uniformly continuous function such that $f(0)\leqslant 0$ and $f(1) \geqslant 0$ then (as a locale) $\{x, |f(x)=0 \}$ is not empty.
2) Let $f :D \rightarrow D$ be a uniformly continuous function then the locale $\{x | f(x)=x\}$ is not empty.
3) let $p$ be a complex polynomial, with at least one coeficient $|a_i|>0$ other than the constant coeficient, then the locale $\{x |p(x)=0 \}$ is not empty.
each time " $F$ not empty" really just mean that $F = \emptyset \Rightarrow False$
and the "*" on constructive refer to the fact that these are proof relying on Barr's theorem, cf below.
All of them follow the same scheme which I will explain below (and I will explain precesely what I mean by 'constructive' as there is a small subtleties here)
A first remark: I added "uniformly continuous" because, asking that a function from $[0,1]$ or $D$ to $\mathbb{R}$ extend to a function between the corresponding locales is the same as saying that the function is uniformly continuous. So if every time you interpret those as functions on the corresponding locale, then you can remove the uniform continuity hypothesis, and I only put it to remind of this.
Now let's move to the proof of those claim. They point is to prove them internally in a Grothendieck $T$ using Barr's covering theorem which assert that every topos $T$ admit a surjection from a topos $E \twoheadrightarrow T$ such that the internal logic of $E$ satisfies LEM and AC. (surjection mean that $f^*$ is conservative)
More precisely:
Every Grothendieck topos admit a surjection $E \twoheadrightarrow T$ where $E$ is a boolean locale. (hence its logic satisfies LEM)
Assuming AC (in the topos of set) the internal logic of every boolean locale satisifes AC.
The proof strategy for each points is the following:
You start with the problem in a topos $T$, you pull it back to a problem in $E$ where you now how to prove it because you have LEM and AC in $E$. And then you are able to deduce the result in $T$ using that $E \twoheadrightarrow T$ is a surjection. I will explain in more detail at the very end of my answer how this is done.
This gives a non constructive proof that these theorems hold in every Grothendieck topos. If you have a proof of the claims $1,2$ or $3$ that uses LEM but not AC, then you actually obtain a constructive but non predicative proof that it holds in every Grothendieck topos, and in particular in the topos of sets.
Moreover in each case you can construct a "classyfing topos for the assumption", for exemple for $(1)$ one can construct the classifying locales of all function $f:[0,1] \rightarrow \mathbb{R}$ such that $f(0) \leqslant 0$ and $f(1) \geqslant 0$ simply because $[0,1]$ is exponentiable in the category of locale and similarly. You can then apply the argument above to these classyfing topos for the assumption to deduce that the theorem holds in these specific toposes (locales). As classyfing topos have a "syntactical" description in terms of geometric logic, this actually implies that each of the claim $1$, $2$ and $3$ have a proof purely in the language of geometric logic. this puts us is the following situation:
We have given a non-constructive proof that these claim have constructive and even predicative proofs.
Whether you accept that as a constructive proof depends on your philosophical stance:
If you are interested in constructivity only because of topos theoretic interpretation (or other models of constructive mathematics) then you should accept that as a constructive proof.
If you are interested in constructivity for philosophical reason, this shouldn't be a satisfying proof.
If you are interested in "constructive proof <-> algotrithm" correspondence, then this is only partially satisfying: it says that "there exists an algorithm" that will do the corresponding task, but it does not say what the algorithm is.
And in all case, it does mean that a constructive proof do exists, so we should be able to find it. (and if those results are important to you or you plan to publish somehting that rely on them I would suggest to try to find actual construct proof for them instead of this argument, it is a lot easier to find a proof once one knows that it exists !)
Finally, let me clarify the proof that the validity of such statement in $E$ implies their Validity in $T$. I will do that for point $2$ in full detail, but this is exactly the same for all of them.
First, if we have $p:E \rightarrow T$, and interally in $T$ some function $f:D \rightarrow D$ then this can be pulled back as:
$p^{\sharp} f : p^{\sharp} D \rightarrow p^{\sharp} D$ in $E$, where $p^{\sharp}$ is how I denote the pullback of locales along a geometric morphism. And (for the locales of real numbers) $p^{\sharp} D $ is just $D$ so we have the exact same situation in $E$.
The sublocale of $D$, $\{ x \in D |f(x)=x \}$ is defined as a certain pullback so it is preserved by pullback as well:
$p^{\sharp} (\{ x \in D | x= f(x) \}) = \{ x \in p^{\sharp} D | x = p^{\sharp}(f)(x) \}$
The key point is the following: if $K$ is a locale in some topos, one can consider the proposition $``K=\emptyset"$ (which, as any proposition is a subterminal object of our topos. I claim that when $K$ is a compact locale (internally in $T$) then:
$p^*(``K=\emptyset") = `` p^{\sharp} K = \emptyset" $
intuitively, this is becasue (say when $T$ is a locale), a compact locale $K$ in $T$ is a proper geometric morphism $K \rightarrow T$, in particular, it is a closed map, hence its image is closed and the open complement of its image is the proposition in $T$, $K= \emptyset$ and this is stable under any pullback (but it only works because $K \rightarrow T$ is stably closed).
For a more precise proof, it is essentially the Beck-Chevalley condition for proper map of toposes (C3.2.6 in sketches of an elephant).
This implies that if $K$ is some locale in $T$ such that for $p : E \twoheadrightarrow T$ a surjection, if $ p^\sharp K = \emptyset \Rightarrow False $ in $E$ than $K= \emptyset \Rightarrow False$ in $T$.
Indeed $K= \emptyset \Rightarrow False$ can be written as the fact that $\emptyset \hookrightarrow `` K = \emptyset''$ is an isomorphism, and th $\emptyset \hookrightarrow `` p^{\sharp}K = \emptyset''$ is exactly the pullback of this map by $p^*$, so the conservativity of $p^*$ implies the result.