We can prove the approximate intermediate value theorem constructively using only pointwise continuity. The proof has the same feel as $\forall x \in \mathbf{R}\ \exists n \in \mathbf{N} \ n > r$, which is constructively valid but with $n$ chosen in a way that depends on the particular rational sequence defining $x$.

A real number $x$ is defined to be a sequence of rationals $x^n$ such that $|x^m-x^n|\le 1/m+1/n$. (Since there are no positive exponents in this proof, all positive superscripts will be these rational approximations.) So $|x-x^n| \le 1/n$ and, e.g. we can choose the $n$ above to be $\lceil x^1 \rceil + 2.$

Now we are given $a,\ b,\ \epsilon,\ f$ as in the question. Let $a_1=a$, $b_1=b$.

$$\text{Let }c_n = (a_n+b_n)/2.$$ $$\text{If }f(c_n)^n < 0,\text{ then let }a_{n+1} = c_n,\ b_{n+1}=b_n.$$ $$\text{If }f(c_n)^n \ge 0,\text{ then let }a_{n+1} = a_n,\ b_{n+1}=c_n.$$

Unlike the version referenced in the 11/16 comment, this is deterministic at each stage, so the construction of the $c$'s requires only unique choice and not dependent choice. (If there's a hidden use of dependent choice, please let me know!)

The intervals $[a_n,b_n]$ have lengths decreasing by halves with intersection $c$. Furthermore, $f(a_n)^n < 1/n$ and $f(b_n)^n \ge 1/n$ for all $n$.

By pointwise continuity of $f$, choose $\delta$ such that $|x-c|<\delta$ implies $|f(x)-f(c)|<\epsilon/3$.

Choose $m$ with $(a-b)2^{-m} < \delta$ and $1/m < \epsilon/3$. Then

$$|a_m-c|<(a-b)2^{-m} < \delta, \ \text{ and }\ f(c) \le f(a_m) + \epsilon/3 \le f(a_m)^m + 1/m + \epsilon/3 \le \epsilon.$$ By similar comparison with the $b$'s, $f(c) \ge -\epsilon$. So $c$ is as desired to prove the approximate intermediate value theorem, QED.

Update: this answer was before the edit to the question rejecting this setoid approach.

We can prove the approximate intermediate value theorem constructively using only pointwise continuity. The proof has the same feel as $\forall x \in \mathbf{R}\ \exists n \in \mathbf{N} \ n > r$, which is constructively valid but with $n$ chosen in a way that depends on the particular rational sequence defining $x$.

A real number $x$ is defined to be a sequence of rationals $x^n$ such that $|x^m-x^n|\le 1/m+1/n$. (Since there are no positive exponents in this proof, all positive superscripts will be these rational approximations.) So $|x-x^n| \le 1/n$ and, e.g. we can choose the $n$ above to be $\lceil x^1 \rceil + 2.$

Now we are given $a,\ b,\ \epsilon,\ f$ as in the question. Let $a_1=a$, $b_1=b$.

$$\text{Let }c_n = (a_n+b_n)/2.$$ $$\text{If }f(c_n)^n < 0,\text{ then let }a_{n+1} = c_n,\ b_{n+1}=b_n.$$ $$\text{If }f(c_n)^n \ge 0,\text{ then let }a_{n+1} = a_n,\ b_{n+1}=c_n.$$

Unlike the version referenced in the 11/16 comment, this is deterministic at each stage, so the construction of the $c$'s requires only unique choice and not dependent choice. (If there's a hidden use of dependent choice, please let me know!)

The intervals $[a_n,b_n]$ have lengths decreasing by halves with intersection $c$. Furthermore, $f(a_n)^n < 1/n$ and $f(b_n)^n \ge -1/n$ for all $n$.

By pointwise continuity of $f$, choose $\delta$ such that $|x-c|<\delta$ implies $|f(x)-f(c)|<\epsilon/3$.

Choose $m$ with $(a-b)2^{-m} < \delta$ and $1/m < \epsilon/3$. Then

$$|a_m-c|<(a-b)2^{-m} < \delta, \ \text{ and }\ f(c) \le f(a_m) + \epsilon/3 \le f(a_m)^m + 1/m + \epsilon/3 \le \epsilon.$$ By similar comparison with the $b$'s, $f(c) \ge -\epsilon$. So $c$ is as desired to prove the approximate intermediate value theorem, QED.

We can prove the approximate intermediate value theorem constructively using only pointwise continuity. The proof has the same feel as $\forall x \in \mathbf{R}\ \exists n \in \mathbf{N} \ n > r$, which is constructively valid but with $n$ chosen in a way that depends on the particular rational sequence defining $x$.

A real number $x$ is defined to be a sequence of rationals $x^n$ such that $|x^m-x^n|\le 1/m+1/n$. (Since there are no positive exponents in this proof, all positive superscripts will be these rational approximations.) So $|x-x^n| \le 1/n$ and, e.g. we can choose the $n$ above to be $\lceil x^1 \rceil + 2.$

Now we are given $a,\ b,\ \epsilon,\ f$ as in the question. Let $a_1=a$, $b_1=b$.

$$\text{Let }c_n = (a_n+b_n)/2.$$ $$\text{If }(c_n)^n < 0,\text{ then let }a_{n+1} = c_n,\ b_{n+1}=b_n.$$ $$\text{If }(c_n)^n \ge 0,\text{ then let }a_{n+1} = a_n,\ b_{n+1}=c_n.$$

Unlike the version referenced in the 11/16 comment, this is deterministic at each stage, so the construction of the $c$'s requires only unique choice and not dependent choice. (If there's a hidden use of dependent choice, please let me know!)

The intervals $[a_n,b_n]$ have lengths decreasing by halves with intersection $c$. Furthermore, $f(a_n)^n < 1/n$ and $f(b_n)^n \ge 1/n$ for all $n$.

By pointwise continuity of $f$, choose $\delta$ such that $|x-c|<\delta$ implies $|f(x)-f(c)|<\epsilon/3$.

Choose $m$ with $(a-b)2^{-m} < \delta$ and $1/m < \epsilon/3$. Then

$$|a_m-c|<(a-b)2^{-m} < \delta, \ \text{ and }\ f(c) \le f(a_m) + \epsilon/3 \le f(a_m)^m + 1/m + \epsilon/3 \le \epsilon.$$ By similar comparison with the $b$'s, $f(c) \ge -\epsilon$. So $c$ is as desired to prove the approximate intermediate value theorem, QED.

We can prove the approximate intermediate value theorem constructively using only pointwise continuity. The proof has the same feel as $\forall x \in \mathbf{R}\ \exists n \in \mathbf{N} \ n > r$, which is constructively valid but with $n$ chosen in a way that depends on the particular rational sequence defining $x$.

A real number $x$ is defined to be a sequence of rationals $x^n$ such that $|x^m-x^n|\le 1/m+1/n$. (Since there are no positive exponents in this proof, all positive superscripts will be these rational approximations.) So $|x-x^n| \le 1/n$ and, e.g. we can choose the $n$ above to be $\lceil x^1 \rceil + 2.$

Now we are given $a,\ b,\ \epsilon,\ f$ as in the question. Let $a_1=a$, $b_1=b$.

$$\text{Let }c_n = (a_n+b_n)/2.$$ $$\text{If }f(c_n)^n < 0,\text{ then let }a_{n+1} = c_n,\ b_{n+1}=b_n.$$ $$\text{If }f(c_n)^n \ge 0,\text{ then let }a_{n+1} = a_n,\ b_{n+1}=c_n.$$

Unlike the version referenced in the 11/16 comment, this is deterministic at each stage, so the construction of the $c$'s requires only unique choice and not dependent choice. (If there's a hidden use of dependent choice, please let me know!)

The intervals $[a_n,b_n]$ have lengths decreasing by halves with intersection $c$. Furthermore, $f(a_n)^n < 1/n$ and $f(b_n)^n \ge 1/n$ for all $n$.

By pointwise continuity of $f$, choose $\delta$ such that $|x-c|<\delta$ implies $|f(x)-f(c)|<\epsilon/3$.

Choose $m$ with $(a-b)2^{-m} < \delta$ and $1/m < \epsilon/3$. Then

$$|a_m-c|<(a-b)2^{-m} < \delta, \ \text{ and }\ f(c) \le f(a_m) + \epsilon/3 \le f(a_m)^m + 1/m + \epsilon/3 \le \epsilon.$$ By similar comparison with the $b$'s, $f(c) \ge -\epsilon$. So $c$ is as desired to prove the approximate intermediate value theorem, QED.