The predicativity of CZF and related systems is consonant with philosophical positions which are often associated with the use of intuitionistic logic. In particular, it would seem that if we construct the mathematical objects, for example, if the mathematical objects are mental constructions of some kind, then resorting to impredicative definitions would produce an undesirable form of circularity. This clearly contrasts with a view often associated to classical set theory, for which our mathematical activity can be seen as a gradual disclosure of properties of the universe of sets, whose existence is independent from us. Such a view is usually bound up with the use of classical logic and impredicativity in studying the set-theoretic universe. Predicativity is also often seen as related to the time-honoured distinction between actual and potential infinity. Predicative (and thus, in particular, constructive) theories are often seen as avoiding reference to actual infinity, and only committing to potential infinity (Dummett 2000, Fletcher 2007). This again seems particularly in harmony with those philosophical positions which highlight the human dimension of our mathematical activity, by seeing, for example, the mathematical objects and the truth of statements about them as dependent on us. Another related aspect is often seen as pertaining to predicativity: if the universe of sets is built up in stages by our own mathematical activity, then it would be natural also to see it as open ended. For this reason, in a constructive context, where the rejection of classical logic meets the requirement of predicativity, the universe of sets is often described as an open concept, a universe “in fieri”. This idea is especially well exemplified within constructive type theory, where the notion of type-theoretic universe has been deliberately left open by Per Martin-Löf (by not postulating specific elimination rules for it). The open ended nature of the universe of sets has paved the way for extensions of it by reflection principles. These have been investigated both within type theory and constructive set theory. See (Rathjen 2005a) for a survey of results and a foundational discussion, and also section 5.2.  For a formal analysis of the constructive universe of sets and a comparison with the Von Neumann hierarchy, see (Ziegler 2014). 