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( \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.$ Choose $c_m$ such that $|c-c_m| < \delta / 2$ and $(a-b)/2^m < \delta / 2$.

Claim:  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:

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 as $i$ goes from 1 to $m.$ The base case is given by $ f(a) < 0, \ f(b) > 0.$

Now assume the claim for $ i.$ In case (i), for some $ j < i,\ |f(c_j)| < \epsilon$, and the inductive step is trivial.

In case (ii), use trichotomy with either $f(c_i) < -\epsilon/2, \ |f(c_i)| < \epsilon$, or $f(c_i) > \epsilon/2.$ If $|f(c_i)| < \epsilon$, then the inductive step is again trivial. If $f(c_i) > \epsilon/2$, then $$d_i = 1$$ $$a_{i+1} = a_i, \text{ so }f(a_{i+1}) < 0$$ $$b_{i+1} = c_i,\text{ so } f(b_{i+1}) > 0$$

If $f(c_i) < - \epsilon/2$, then $$d_i = 0$$ $$a_{i+1} = c_i, \text{ so }f(a_{i+1}) < 0$$ $$b_{i+1} = b_i,\text{ so } f(b_{i+1}) > 0$$

QED (claim and theorem).

I think this one works; I look forward to seeing what MO says.

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.

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( \frac{1}{2}+ \frac{ f(c_n)}{\epsilon}, 1))$$ $$a_{n+1} = c_n - d_n (a-b)/2^n $$ $$b_{n+1} = b_n - d_n (a-b)/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.$ Choose $c_m$ such that $|c-c_m| < \delta / 2$ and $(a-b)/2^m < \delta / 2$.

Claim:  Either (i) $\exists j <= m,\ |f(c_j)| < \epsilon$ or (ii) $f(a_m) < 0 $ and$ f(b_m) > 0$.

Proof of theorem from 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 as $i$ goes from 1 to $m.$ The base case is given by $ f(a) < 0, \ f(b) > 0.$

Now assume the claim for $ i.$ In case (i), for some $ j < i,\ |f(c_j)| < \epsilon$, and the inductive step is trivial.

In case (ii), use trichotomy with either $f(c_i) < -\epsilon/2, \ |f(c_i)| < \epsilon$, or $f(c_i) > \epsilon/2.$ If $|f(c_i)| < \epsilon$, then the inductive step is again trivial. If $f(c_i) > \epsilon/2$, then $$d_i = 1$$ $$a_{i+1} = a_i, \text{ so }f(a_{i+1}) < 0$$ $$b_{i+1} = c_i,\text{ so } f(b_{i+1}) > 0$$

If $f(c_i) < - \epsilon/2$, then $$d_i = 0$$ $$a_{i+1} = c_i, \text{ so }f(a_{i+1}) < 0$$ $$b_{i+1} = b_i,\text{ so } f(b_{i+1}) > 0$$

QED (claim and theorem).

I think this one works; I look forward to seeing what MO says.

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( \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.$ Choose $c_m$ such that $|c-c_m| < \delta / 2$ and $(a-b)/2^m < \delta / 2$.

Claim:  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:

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 as $i$ goes from 1 to $m.$ The base case is given by $ f(a) < 0, \ f(b) > 0.$

Now assume the claim for $ i.$ In case (i), for some $ j < i,\ |f(c_j)| < \epsilon$, and the inductive step is trivial.

In case (ii), use trichotomy with either $f(c_i) < -\epsilon/2, \ |f(c_i)| < \epsilon$, or $f(c_i) > \epsilon/2.$ If $|f(c_i)| < \epsilon$, then the inductive step is again trivial. If $f(c_i) > \epsilon/2$, then $$d_i = 1$$ $$a_{i+1} = a_i, \text{ so }f(a_{i+1}) < 0$$ $$b_{i+1} = c_i,\text{ so } f(b_{i+1}) > 0$$

If $f(c_i) < - \epsilon/2$, then $$d_i = 0$$ $$a_{i+1} = c_i, \text{ so }f(a_{i+1}) < 0$$ $$b_{i+1} = b_i,\text{ so } f(b_{i+1}) > 0$$

QED (claim and theorem).

I think this one works; I look forward to seeing what MO says.