Quoting Paul Taylor <pt09@PaulTaylor.EU>:
Toby has also said a lot of interesting things about many different systems. These illustrate my point that it is essential to state which system, or which notion of "constructivity" you intend.
He has said, for example * The Dedekind reals can also be constructed in CZF (Peter Aczel's predicative constructive set theory) even if you remove countable choice, using subset collection aka fullness. * Similarly, if you remove identity types from intensional type theory (so breaking the justification of countable choice), you can still justify the fullness axiom and so construct the Dedekind reals (albeit not literally as sets of rational numbers). * The Cauchy reals exist an a Pi-W-pretopos (equivalently, in a constructive set or type theory with exponentiation but no power sets or even fullness and with infinity but no countable choice). * But the Dedekind reals, as far as [he] can tell, do not; excluded middle, power sets, fullness, or countable choice would each do the job, but you need ~something~.
I would challenge someone to consider the last of these questions seriously, maybe taking a hint from the second. ASD provides another, as it uses lambda term over a special object instead of talking about "sets" of rational numbers.
A note concerning the possibility of constructing the Dedekind reals without fullness, etc: the Dedekind reals can be defined in constructive set theory even without excluded middle, power sets, fullness, or countable choice. The point is that they then form a class and not a set. Class-sized objects are however the norm in a constructive predicative setting. For instance, a (non-trivial) locale is carried by a class that is never a set; in general a formal space or formal topology is a large object too, so that one often deals with superlarge "categories" with large homsets. Giovanni Curi Dipartimento di Matematica Pura ed Applicata Universita' degli Studi di Padova www.math.unipd.it