The disjunction and related properties for constructive Zermelo-Fraenkel set theory

This paper proves that the disjunction property,. the numerical existence property, Church's rule. and several other metamathematical properties hold true for Constructive Zermelo-Fraenkel Set Theory. CZF. and also for the theory CZF augmented by the Regular Extension Axiom. As regards the proof technique, it features a self-validating semantics for CZF that combines realizability for extensional set theory and truth.