Comment by madez

   if you describe the real numbers as setoids of Cauchy sequences
   with Cauchy-equivalence as the equivalence relation, then there
   are uncountably many real numbers.

I start with computable sequences (or — if want — with turing machines), define natural numbers based on them, go to the rational numbers, define real numbers as a setoid of cauchy-sequences (note: all these sequences will be computable by the way we constructed them) of rational numbers, and end up with countably many. So, it depends on what you start your constructive world with. I see no way to start with something uncountable.

You talk about meta-theory and models. I never saw the reason to complicate things with that. Care to elaborate?