I am a little aware of various attempts to axiomize set theory within a theorem prover. Is there a standard kind of encoding of sets? An organic model to interpret set theories into? I would like to be sure my axioms have reasonable interpretations.
Something like this page on pure sets on nlab seems close but also seems a bit hairy.
It feels like these sort of encodings would be easiest with some hairy uses of functional or propositional extensionality which is mildly inconvenient.
You also have classical or choice principle issues. Something like CZF feels like it would be easiest to model in type theory (but hairier to axiomize.)
From what I grasp of the pure set page you want something like
Inductive pregraph :=
| sup X (f: X -> pregraph).
Fixpoint monic p :=
let 'sup X f := p in
f x == f y -> x = y
/\ forall x, monic (f x).
Existing Class monic.
Definition graph := { p: graph | monic p }.
Definition member P '(sup X ps) :=
exists x. ps x == P.
But you need to define equivalence of pregraphs or assume some flavor of extensionality. Then you need to carve out well-founded sets. I feel like there ought to be an easier way.
Maybe it would be nicer to first model proper classes and then model pure sets as classes which are members of other classes?