Is there a "standard" encoding or model of material set theory in type theory?

Question

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?

Answer 1

(Building on comments by Pedro Sánchez Terraf) As for encoding ZFC in dependent type theory their seems to be the following progression of work

• Aczel's encoding of ZFC into DTT as an inductive structure
• Werner's implementation of Aczel's encoding in Coq in Sets in Coq, Coq in Sets. I believe you can find the code in the coq-zfc opam package and coq-contribs/zfc github repo.
• Mario Carneiro implemented the Werner-Aczel's encoding in Lean's mathlib. Here is the current state of ZFC in Lean's mathlib, and here is some additional set theory built on top of it. (Also Mario's masters thesis The Type Theory of Lean has some pen and paper proofs showing the relation between Lean's type theory and ZFC (plus large cardinals).)
• As part of the Jesse Michael Han and Floris van Doorn's Flypitch project to formalize the independence of continuum hypothesis in Lean, they extended the Aczel-Werner encoding to Boolean valued models (paper, repo).

Also, here is a quote from the Flypitch paper which I think captures the essence of both the Aczel-Werner encoding and its extension in that paper.

As with Coq, Lean is able to encode extremely complex objects and reason about their specifications using inductive types. However, the user must be careful to choose the encoding so that properties they wish to reason about are accessible by structural induction, which is the most natural mode of reasoning in the proof assistant. After observing (1) that the Aczel-Werner encoding of ZFC as an inductive type is essentially a special case of the recursive name construction from forcing (c.f. Section 3), and (2) that the automatically-generated induction principle for that inductive type is $\in$-induction, it is easy to see that this encoding can be modified to produce a Boolean-valued model of set theory where, again, $\in$-induction comes for free.

Answer 2

Depends on which type theory :-)

ZF set theory has been formalised in Isabelle as Isabelle/ZF by directly assuming the ZF axioms (and optionally AC). For those who prefer higher-order logic (also known as simple type theory), it's been done many times.

Details here and an application here. See also an impressive application of Isabelle/ZF.