[I just started here and do not have enough reputation to comment...so I´m kind of forced to give an answer.]

I believe there is a different way to eliminate countable choice in the proof of aIVT (approximate intermediate value theorem). I've described this way on the constructive-news forum https://groups.google.com/forum/#!topic/constructivenews/e3JfKk_W2jI

I'm not sure if that description is too specialist to post here. But what it boils down to is this: in Matt's first proof, using bisection, there is a hidden use of countable choice. Because to evaluate the real number $f(c_n)$, one has to pick a representative of its equivalence class. (This is brilliantly avoided in Matt's second proof).

My first attempt to avoid this involved looking at recursive mathematics. If we take $a,b$ and $f$ to be recursive, then if we pick (recursive) representatives $a', b'$ we can apply the bisection method without using countable choice. Because taking the mean is a recursive function $m(a,b)=\frac{(a+b)}{2}$, we see that every iterative construction and evaluation of $f(c_n)$ is recursive in $a', b'$.

This approach can be characterized as: `we only need countable choice because the objects that we are working with have been insufficiently specified beforehand'. In other words: we have left to much choice in $a,b$ AND $f$

However I believe there is a more general way to avoid choice in the construction of $a,b$ AND $f$. By describing R and continuous real functions in a different way, namely R as a #-quotient and continuous real functions as #-morphisms on Baire space, we can apply the bisection method without using countable choice.

The reason for this is comparable to the recursive situation. If we pick #-representatives $a'',b''$ of $a,b$ AND #-representatives $m'', f''$ of the functions $m, f$, there is no choice left in the bisection procedure using $a'', b'', m'', f''$, because composition of #-morphisms is completely deterministic.

In CLASS, INT and RUSS I believe we can prove that every continuous real function can be represented by such a #-morphism. This proof can be found in my book Natural Topology [but it really should be checked by some more people]. A preprint which I submitted to LMCS three years ago (!) is still under reviewer's consideration.

So I believe that using #-morphisms in BISH is a general way to avoid countable choice in theorems comparable to aIVT. Since #-quotient representations can be found for any Polish space, this goes a lot further than just real functions.

[I just started here and do not have enough reputation to comment...so I´m kind of forced to give an answer.]

I believe there is a different way to eliminate countable choice in the proof of aIVT (approximate intermediate value theorem). I've described this way on the constructive-news forum https://groups.google.com/forum/#!topic/constructivenews/e3JfKk_W2jI

I'm not sure if that description is too specialist to post here. But what it boils down to is this: in Matt's first proof, using bisection, there is a hidden use of countable choice. Because to evaluate the real number $f(c_n)$, one has to pick a representative of its equivalence class. (This is brilliantly avoided in Matt's second proof).

My first attempt to avoid this involved looking at recursive mathematics. If we take $a,b$ and $f$ to be recursive, then if we pick (recursive) representatives $a', b'$ we can apply the bisection method without using countable choice. Because taking the mean is a recursive function $m(a,b)=\frac{(a+b)}{2}$, we see that every iterative construction and evaluation of $f(c_n)$ is recursive in $a', b'$.

This approach can be characterized as: `we only need countable choice because the objects that we are working with have been insufficiently specified beforehand'. In other words: we have left too much choice in $a,b$ AND $f$

However I believe there is a more general way to avoid choice in the construction of $a,b$ AND $f$. By describing R and continuous real functions in a different way, namely R as a #-quotient and continuous real functions as #-morphisms on Baire space, we can apply the bisection method without using countable choice.

The reason for this is comparable to the recursive situation. If we pick #-representatives $a'',b''$ of $a,b$ AND #-representatives $m'', f''$ of the functions $m, f$, there is no choice left in the bisection procedure using $a'', b'', m'', f''$, because composition of #-morphisms is completely deterministic.

In CLASS, INT and RUSS I believe we can prove that every continuous real function can be represented by such a #-morphism. This proof can be found in my book Natural Topology [but it really should be checked by some more people]. A preprint which I submitted to LMCS three years ago (!) is still under reviewer's consideration.

So I believe that using #-morphisms in BISH is a general way to avoid countable choice in theorems comparable to aIVT. Since #-quotient representations can be found for any Polish space, this goes a lot further than just real functions.

[I just started here and do not have enough reputation to comment...so I´m kind of forced to give an answer.]

I believe there is a different way to eliminate countable choice in the proof of aIVT (approximate intermediate value theorem). I've described this way on the constructive-news forum https://groups.google.com/forum/#!topic/constructivenews/e3JfKk_W2jI

I'm not sure if that description is too specialist to post here. But what it boils down to is this: in Matt's first proof, using bisection, there is a hidden use of countable choice. Because to evaluate the real number $f(c^n)$, one has to pick a representative of its equivalence class. (This is brilliantly avoided in Matt's second proof).

My first attempt to avoid this involved looking at recursive mathematics. If we take $a,b$ and $f$ to be recursive, then if we pick (recursive) representatives $a', b'$ we can apply the bisection method without using countable choice. Because taking the mean is a recursive function $m(a,b)=\frac{(a+b)}{2}$, we see that every iterative construction and evaluation of $f(c^n)$ is recursive in $a', b'$.

This approach can be characterized as: `we only need countable choice because the objects that we are working with have been insufficiently specified beforehand'. In other words: we have left to much choice in $a,b$ AND $f$

However I believe there is a more general way to avoid choice in the construction of $a,b$ AND $f$. By describing R and continuous real functions in a different way, namely R as a #-quotient and continuous real functions as #-morphisms on Baire space, we can apply the bisection method without using countable choice.

The reason for this is comparable to the recursive situation. If we pick #-representatives $a'',b''$ of $a,b$ AND #-representatives $m'', f''$ of the functions $m, f$, there is no choice left in the bisection procedure using $a'', b'', m'', f''$, because composition of #-morphisms is completely deterministic.

In CLASS, INT and RUSS I believe we can prove that every continuous real function can be represented by such a #-morphism. This proof can be found in my book Natural Topology [but it really should be checked by some more people]. A preprint which I submitted to LMCS three years ago (!) is still under reviewer's consideration.

So I believe that using #-morphisms in BISH is a general way to avoid countable choice in theorems comparable to aIVT. Since #-quotient representations can be found for any Polish space, this goes a lot further than just real functions.

[I just started here and do not have enough reputation to comment...so I´m kind of forced to give an answer.]

I believe there is a different way to eliminate countable choice in the proof of aIVT (approximate intermediate value theorem). I've described this way on the constructive-news forum https://groups.google.com/forum/#!topic/constructivenews/e3JfKk_W2jI

I'm not sure if that description is too specialist to post here. But what it boils down to is this: in Matt's first proof, using bisection, there is a hidden use of countable choice. Because to evaluate the real number $f(c_n)$, one has to pick a representative of its equivalence class. (This is brilliantly avoided in Matt's second proof).

My first attempt to avoid this involved looking at recursive mathematics. If we take $a,b$ and $f$ to be recursive, then if we pick (recursive) representatives $a', b'$ we can apply the bisection method without using countable choice. Because taking the mean is a recursive function $m(a,b)=\frac{(a+b)}{2}$, we see that every iterative construction and evaluation of $f(c_n)$ is recursive in $a', b'$.

This approach can be characterized as: `we only need countable choice because the objects that we are working with have been insufficiently specified beforehand'. In other words: we have left to much choice in $a,b$ AND $f$

However I believe there is a more general way to avoid choice in the construction of $a,b$ AND $f$. By describing R and continuous real functions in a different way, namely R as a #-quotient and continuous real functions as #-morphisms on Baire space, we can apply the bisection method without using countable choice.

The reason for this is comparable to the recursive situation. If we pick #-representatives $a'',b''$ of $a,b$ AND #-representatives $m'', f''$ of the functions $m, f$, there is no choice left in the bisection procedure using $a'', b'', m'', f''$, because composition of #-morphisms is completely deterministic.

In CLASS, INT and RUSS I believe we can prove that every continuous real function can be represented by such a #-morphism. This proof can be found in my book Natural Topology [but it really should be checked by some more people]. A preprint which I submitted to LMCS three years ago (!) is still under reviewer's consideration.

So I believe that using #-morphisms in BISH is a general way to avoid countable choice in theorems comparable to aIVT. Since #-quotient representations can be found for any Polish space, this goes a lot further than just real functions.