CZF is an intuitionistic set theory that does not contain Power Set, substituting instead a weaker version, Subset Collection. In this paper a Kripke model of CZF is presented in which Power Set is false. In addition, another Kripke model is presented of CZF with Subset Collection replaced by Exponentiation, in which Subset Collection fails.

In constructive mathematics it is of interest to consider a more general, but classically equivalent, notion of linear order, a so-called pseudo-order. The prime example is the order of the constructive real numbers. We examine two kinds of constructive completions of pseudo-orders: order completions of pseudo-orders and Cauchy completions of ordered groups and fields. It is shown how these can be predicatively defined in type theory, also when the underlying set is non-discrete. Provable choice principles, in particular a generalisation of (...) dependent choice, are used for showing set-representability of cuts. (shrink)

A constructive definition of the continuum based on formal topology is given and its basic properties studied. A natural notion of Cauchy sequence is introduced and Cauchy completeness is proved. Other results include elementary proofs of the Baire and Cantor theorems. From a classical standpoint, formal reals are seen to be equivalent to the usual reals. Lastly, the relation of real numbers as a formal space to other approaches to constructive real numbers is determined.