Constructive Set Theory with operations

We present an extension of Aczel's constructive Zermelo–Fraenkel set theory. Constructive sets are endowed with an applicative structure, which allows us to express several set theoretic constructs uniformly and explicitly. From the proof theoretic point of view, the addition is shown to be conservative. In particular, we single out a theory of constructive sets with operations which has the same strength as Peano arithmetic.