In constructive mathematics without any choice at all, it is well known that the fundamental theorem of algebra cannot be proven for the Dedekind real numbers. On the other hand, Wim Ruitenberg showed in his paper Constructing Roots of Polynomials over the Complex Numbers that the fundamental theorem of algebra can be proven without choice at all for the real numbers defined as a quotient of Cauchy sequences of rational numbers. What is the status in constructive mathematics of the fundamental theorem of algebra for the locale of real numbers?

In constructive mathematics without any choice at all, it is well known that the fundamental theorem of algebra cannot be proven for the Dedekind real numbers. On the other hand, Wim Ruitenberg showed in his paper Constructing Roots of Polynomials over the Complex Numbers that the fundamental theorem of algebra can be proven without choice at all for the real numbers defined as a quotient of Cauchy sequences of rational numbers. What is the status in constructive mathematics of the fundamental theorem of algebra for the locale of real numbers? I wonder if the fact that the locale of real numbers is not spatial has any impact on the status of the fundamental theorem of algebra.