Hello, all!
Is this meaningful way to do ZFC set theory “from inside” in Coq? https://pastebin.com/cauVSRf1
Also, I can’t find a way to prove last theorem named ‘subset_of_singleton’. Is it because I’m not clever enough or maybe I have made a mistake somewhere before? Thanks in advance.
There are antecedents.
You can have a look at GitHub - coq-contribs/cats-in-zfc: Category theory in ZFC (the first files are in order axioms.v tactics.v and set_theory.v, read tactics.v just to know what the tactics in the others mean). The pdf in that repo looks like it’s broken, get it from [math/0410224] Formalized proof, computation, and the construction problem in algebraic geometry instead.
Years ago I played around with it and made it more axiomatic (eg instead of Definition E := Type. for the type of sets I have Axiom E : Type., so you have to use the ZF axioms on it instead of inductive types etc), you can have a look at GitHub - SkySkimmer/ZF: Playing around with axiomatic set theory in Coq (quality not guaranteed, doesn’t compile with current Coq).
Also, I can’t find a way to prove last theorem named ‘subset_of_singleton’. Is it because I’m not clever enough or maybe I have made a mistake somewhere before? Thanks in advance.
You have excluded middle (classical logic) so you can ask whether {a} belongs to x. The answer lets you know if x is supposed to be empty or {{a}}. Proceed from there.
BTW consider using more informative theorem names than E1214 or T3.
There’s a formalization in HoTT, most of this (quotients, …) should also work if you use classical logic.
The main idea is to encode sets-as-trees using W-types.
The approach is described in the HoTT book.
Another overview:
https://www.ps.uni-saarland.de/settheory.html
There’s also http://www.lix.polytechnique.fr/~barras/proofs/sets/ (https://doi.org/10.6092/issn.1972-5787/1695)
Thank you all for the answers!
Thank you, it helped!
Definitely will make better theorem names in future. It was the first iteration with exercises and theorems taken from some book (E were exercises, T - some theorems).
Hi! 
Just a remark that the natural axiomatisation of ZFC in a dependent type theory you follow is in fact stronger than the usual formulation as a first-order theory. Since your replacement axiom quantifies over all relations and not only the first-order definable ones, it only admits the standard models V_\kappa for \kappa inaccessible.
That the models of this higher-order axiomatisation only differ in height has been observed by Zermelo in his 1930 paper “Über Grenzzahlen und Mengenbereiche” and we have formalised the result in Coq (https://link.springer.com/article/10.1007%2Fs10817-018-9480-6). Our development also contains model constructions a la Aczel/Werner/Barras for the first \omega inaccessibles.
If you are interested in the first-order model theory of ZFC, I guess you’ll have to make the syntax explicit and weaken the replacement axiom accordingly. This has for instance been done in Lean to get a model contradicting the axiom of choice (https://arxiv.org/abs/1904.10570).
The abstract says the paper is about the Continuum Hypothesis.
Forcing can naturally be presented using higher order logic (toposes) and it even works for higher toposes (“models of HoTT”), so another route is also available. In fact, this is related to the various “translations” of type theory studied in Nantes.
I saw that one more development on axiomatic set theory in Coq (8.9) appeared recently:
The main novelties claimed are that it’s the Morse-Kelley extended axiomatic set theory, and there are proofs of the Hausdorff maximal principle and the Schroeder-Bernstein theorem.
There is an accompanying paper as well.