Impredicative Definitions (CZF)

CZF is touted as the predicative and constructive variant of ZF. This is because CZF avoids the fully impredicative axioms of powerset and full separation and alternatively because CZF has an interpretation in an extension of Martin Löf’s type theory, which is predicative. One typically says the definition of an object is impredicative if it contains quantification over a collection of which the is a member. Now just as there are different versions of constructivism there are different versions of predicativism. But in many monographs that discuss predicativism among the already mentioned banned principles another hallmark definition is deemed impredicative: the least upper bound of a set. This is because for one to define the least upper bound $s$ of a subset $S$ of $X$ one must quantify over the set of upper bounds of $S$ which of course contains $s$.

Work with in CZF by both Azcel and Rathejen uses the notion of a least upper bound (or sup or join) frequently so are impredicative definitions allowed in CZF (and other predicative theories?)

Edit: It’s been established that predicativity is not a well-defined notion. I am looking for insight from people that do predicative mathematics.

According to What is predicativism? the kind of circularity that should not be forbidden occurs when one picks out an element of an existing collection. Expanding on this a bit: the definition of an element is forbidden (predicativly) if it is definable ONLY in terms of collections to which it belongs.

This is AN answer. But where does this leave the definition of least upper bound. If you are given an arbitrary non empty subset $S \subseteq X$ it seems like quantifying over the upper bounds is the same as picking out an element of an existing collection and should not be forbidden. But this seems in contrast with the claim by many predicative papers that least upper bound is a hallmark impredicative definition.