This is a self-study project of implementing ZF axioms in Coq.
ZF.vdefines the axioms of ZF.Aczel.vimplements the axioms.
The following axioms are used to implement them.
- Predicate extensionality
∀ P Q, (∀ a, P a ↔ Q a) → P = Qis used to prove set equalities. - Functional choice:
∀ R, (∀ x, ∃ y, R x y) → ∃ f, ∀ x, R x (f x)is used to implement the axiom of replacement.
See [https://www.ps.uni-saarland.de/settheory.html] for the resources I consulted.