We start from axioms for intuitionistic (well-founded) Zermelo-Fraenkel set theory without an axiom of infinity. An epsilon recursion principle is proven. Using this ordered pairs and functions are defined in such a way that ordered pairs are the same as functions from the finite ordinal 2. This is written up in an article that has been submitted to a journal, with a technical report version available here.
Three forms of replacement (as operators) are considered:
Following Ackermann 1937 [Ack37], a membership relation can be defined on the natural numbers and the Zermelo-Fraenkel axioms except infinity can be proven. Separation is limited to decidable predicates. Choice should also be provable, but is not considered in the file.
In the 1970s, Aczel gave an inductive type of trees on which an equivalence relation can be recursively defined [Acz77].
The trees behave as sets relative to the equivalence relation.
In this Coq development, we assume classical logic, epsilon (a form of choice) and extensionality.
After defining the Aczel type and the equivalence relation (following Werner's 1997 description [Wer97]),
we use the choice operator to obtain canonical representatives.
We then define the quotient using sigma types and canonical representatives.
The Zermelo-Fraenkel axioms are proven.
We do not consider the choice axiom, though it should be provable as well.