In classical mathematics, sequences of real numbers (or sequences of codes) are something outside the world of real numbers - they are objects of a different type. In constructive mathematics, real numbers are sequences of codes. That's why the intermediate value theorem can be proved in constructive mathematics inside the world of real numbers.
The same effect could be obtained in "set theoretical mathematics" identifying real numbers with Dedekind cuts. This means incorporating the necessary concepts of set theory into the concept of real numbers.
The point I wanted to make is: The intermediate value theorem for polynomials (to be precise: of a given degree) is a statement that uses real numbers as primitive unstructured objects and involves only addition and multiplication. It has no reference to the internal structure of real numbers. Therefore it suggests, that no knowledge on this structure is needed for a proof. This suggestion can be easily extracted from the theorem if the theorem is stated in a well-typed language and in many cases such a suggestion will be helpful, notably if automated provers are used. But there are cases - such as this one in the context of classical mathematics - where the suggestion is wrong.
In my opinion there is no contradiction between types and sets - set theory is a simple and powerful tool to define types. "Working mathematicians" (i. e. those not involved in foundational studies) do not like to care about sets though they use them. They also do not like to care about types though they use them.
Ingo Dahn