**Reconsidering Pairs and Functions as Sets**-
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.

- Main Version: html version (Coq file)
- Alternative Version using the Knaster Tarski Fixed Point Theorem to justify epsilon recursion: html version (Coq file)
- Alternative Version using an inductive predicate in Coq to justify epsilon recursion: html version (Coq file)

**Three Forms of Replacement**-
Three forms of replacement (as operators) are considered:

*Map Replacement*takes a set and a meta-level function and returns the image set.*Total Replacement*takes a set and a total functional meta-level relation and returns the image set.*Partial Replacement*takes a set and a functional meta-level relation and returns the image set. (I first saw a replacement axiom in this form in Barras 2010 [Bar10].)

**Ackermann Encoding of Decidable Hereditarily Finite Sets**-
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.

**Model of ZF using a quotient of Aczel's Set Type, assuming Epsilon.**-
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.

- The first file defines a module type to make it clear what a model of ZF must satisfy: html version (Coq file)
- The second file contains the construction and the proof that it gives a module (model of ZF): html version (Coq file)

- [Ack37] Wilhelm Ackermann. Die Widerspruchsfreiheit der allgemeinen Mengenlehre. Mathematische Annalen 114: 305-315, 1937
- [Acz77] Peter Aczel. The type theoretic interpretation of constructive set theory. In A. MacIntyre, L. Pacholski, and J. Paris, editors, Logic Colloquium '77, pages 55-66. NorthHolland, 1978.
- [Bar10] Barras, B. Sets in Coq, Coq in Sets. Journal Of Formalized Reasoning, 3(1), 29-48. 2010.
- [Wer97] Benjamin Werner. Sets in types, types in sets. In Proceedings of TACS '97, pages 530-546. Springer-Verlag, 1997.