The intermediate value theorem in constructive mathematics without choice

In Bishop’s constructive mathematics without choice axioms, it seems that in order to construct an object you require it to satisfy some (strong) uniqueness property. As a consequence, it seems unlikely that the standard constructive version of the intermediate value theorem—requiring only the additional hypothesis that the function is locally nonzero—carries over to the setting of Bishop’s constructive mathematics without choice. We give a weaker version of the intermediate value theorem which does hold without choice; the uniqueness of the root constructed follows from it being minimal.