  Having introduced appropriate constraints to power set and separation, we could now face a substantial objection. Constructive and intuitionistic set theories can be seen as modifications of classical ZF set theory that are obtained by: (1) replacing classical with intuitionistic logic, and (2) accurately choosing, among various classically equivalent principles, those which seem more appropriate for given purposes. For example, we might choose principles which suffice to represent a certain mathematical practice, like, for example, Bishop style mathematics. The resulting notion of set, however, might become obscure and the choice of the set-theoretic principles might appear to a certain degree as arbitrary. In the case of intuitionistic ZF, one can justify the choice of the set-theoretic principles by examining its semantical interpretations, as Heyting semantics, or by looking at its categorical models. In the case of constructive set theory, to hinder this kind of objection, Aczel has given an interpretation of CZF in a version of Martin-Löf type theory (Aczel 1978). The claim is that a clear constructive meaning is thus assigned to CZF’s notion of set by looking at its meaning in Martin-Löf type theory, since the latter is usually considered as representing an accurate and fully motivated formulation of a constructive notion of set. Aczel’s interpretation of CZF in constructive type theory is given by interpeting sets as trees in type theory. That is, in constructive type theory  the universe of sets of CZF is represented by a type, V, of iterative sets built over the universe, U, of small types (Aczel 1978; Martin-Löf 1984). This interpretation clearly highlights the (generalised) predicativity of CZF, whose sets can be seen as trees built up inductively, and whose set theoretic universe also has a clear inductive structure. 