  We formulate a definition of the existence property that works with
"structural" set theories, in the mode of ETCS (the elementary theory of the
category of sets). We show that a range of structural set theories, when
formulated using constructive logic, satisfy the disjunction, numerical
existence, and existence properties; in particular, intuitionist ETCS,
formulated with separation and Shulman's replacement of contexts axiom,
satisfies these properties. As a consequence of this, we show that, working
constructively, replacement of contexts is strictly weaker than collection.
