--- title: "Models of ZF and ZFC" module: FOL.ZFModel lang: en site: "Bedrock" description: "Models of ZF and ZFC" stage: "First-order logic" reading_order: 11 canonical: https://bedrock.institute/en/FOL.ZFModel.html html: FOL.ZFModel.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/ZFModel.lagda.md prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Semantics] routes: [common-foundations] translations: [https://bedrock.institute/zh/FOL.ZFModel.md, https://bedrock.institute/ja/FOL.ZFModel.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Models of ZF and ZFC A bare structure becomes a model of set theory by supplying witnesses for the ZF axioms. This chapter develops that road in stages: it says what it means for a set to realize a class, proves realizers unique from an explicit extensionality argument, introduces a description operator that reads a set back off its unique existence, and assembles the axioms into a record. It closes by extending a ZF model to ZFC with the axiom of choice. Nothing in a bare structure yet deserves the name set theory. Its membership relation need not admit an empty set, need not pair two elements, and need not gather the subsets of anything. What a universe of sets must provide is exactly what the **axioms of ZF** say, and this chapter states them. A **model of ZF** is a structure whose fields supply the axioms, so "`𝒮` satisfies ZF" means precisely that such a witness exists at `𝒮`. The setting is fixed once here: equality and membership in `𝒮` take values in `hProp ℓ`, so every such assertion is a proposition, and the module runs entirely at one universe level `ℓ` with its axioms living in `Type (ℓ-suc ℓ)`. The module signature says what kind of thing will be studied: `𝒮` is a `ZFStructure` whose truth values are propositions, that is, a structure over `hProp ℓ`. Two consequences follow immediately. First, the structure's equality `≈ˢ` and membership `∈ˢ` return propositions with underlying types, so membership claims in this chapter are things one can inhabit with proofs. Second, the parameter `{ℓ}` is a universe level, and it stays fixed throughout: the carrier `S` lives in `Type ℓ`, while statements quantifying over all subsets of `S`, such as the axioms themselves, will land in `Type (ℓ-suc ℓ)`. ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import FOL.ZFStructure using ( ZFStructure; module hPropStructure ) module FOL.ZFModel {ℓ} (𝒮 : ZFStructure ℓ) where ``` The axioms assert facts directly in `hProp`. Their constant interpretation is the canonical one from the semantics chapter: the constant domain is the carrier itself and the interpretation is `id`, so a constant appearing in a formula simply *is* the set it names. The working vocabulary for the axioms is assembled here. The syntax chapter supplies `Formula`, the membership symbol `∈̇`, and the constructors `var` and `con`; separation and replacement will take formulas as genuine inputs. The semantics chapter contributes the module `At`, which fixes a constant interpretation and exposes satisfaction for formulas at it. From the host library come `Σ≡Prop`, used to reduce a path of dependent pairs whose second components are propositions, the type `WellFounded` of well-foundedness that regularity will record, the empty type `Empty.⊥`, and propositional truncation `∥_∥₁` for the axiom of choice. ```agda open import FOL.Syntax using ( Formula; var; con; _∈̇_ ) open import FOL.Semantics 𝒮 using ( module At ) open import Cubical.Data.Sigma using ( Σ≡Prop ) open import Cubical.Induction.WellFounded using ( WellFounded ) import Cubical.Data.Empty as Empty ``` Two openings put the structure and satisfaction names into scope; the direct `hProp` operations are already supplied by the prelude. Opening `hPropStructure 𝒮` brings the structure's carrier `S`, its h-set certificate, and the two truth-valued relations `≈ˢ` and `∈ˢ`, together with the Type-valued reading `∈ᵗ` of membership. Finally, opening `At S id` instantiates the satisfaction relation `_⊨_` at the canonical constant interpretation, where a constant denotes itself, so a free variable slot in a formula is read as membership of a specific set. ```agda import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁ ) open hPropStructure 𝒮 open At S id using ( _⊨_ ) ``` ## Realizing a class as a set Nearly every axiom to come has the same shape: *there is a set whose members are exactly the so-and-so*. Pin down the "so-and-so" first. A **class** is a propositional predicate on the carrier, `S → hProp ℓ`: something whose membership can be stated, with no promise that any set collects it. (Classes have already appeared in disguise: the restriction `𝒮 ↾ M` of the structure chapter cuts along exactly such an `M`.) This section defines when a set realizes a class, observes that realization is itself a proposition, and packages the two together. The definition of realization is deliberately pointwise. `IsSetOf Q b` holds when for *every* element `x` of the carrier, the proposition `x ∈ˢ b` is equal, as an element of `hProp ℓ`, to the class value `Q x`. There is no formula, no syntax, and no reduction here: the comparison is direct equality of truth values. This type lives in `Type (ℓ-suc ℓ)` because it quantifies over all of `S`, matching where the axioms themselves will live. ```agda IsSetOf : (S → hProp ℓ) → S → Type (ℓ-suc ℓ) IsSetOf Q b = (x : S) → (x ∈ˢ b) ≡ Q x isPropIsSetOf : (Q : S → hProp ℓ) (b : S) → isProp (IsSetOf Q b) isPropIsSetOf Q b = isPropΠ (λ x → isSetHProp _ _) SetOf : (S → hProp ℓ) → Type (ℓ-suc ℓ) ``` That realization is propositional, not a heavier piece of data, is checked now. The function type `(x : S) → (x ∈ˢ b) ≡ Q x` is a proposition precisely because each fiber is: `hProp ℓ` is `hProp ℓ`, and `isSetHProp` says the type of paths between two propositions packed in `hProp` is an h-set, so its identity types are propositions; `isPropΠ` lifts the pointwise fact to the whole function type. Hence `SetOf Q`, a dependent pair of a candidate set `b` and evidence `IsSetOf Q b`, still has propositional second components, a fact used repeatedly later. ```agda SetOf Q = Σ[ b ∈ S ] IsSetOf Q b ``` How many realizers can one class have? Under **extensionality** (sets with the same members are equal; it will be the first field of the record) the answer is at most one, in the strong, structural sense: any single realizer makes the whole type of realizers contractible. The lemma takes extensionality as an explicit input, because the record that will provide it has not been defined yet. Given a realizer `(b , sp)` of the class `Q`, the contraction sends any other realizer `(b' , sp')` to a path into it. The path in the first component is extensionality applied to `λ x → sp x ∙ sym (sp' x)`: at each `x`, the two specifications give paths `x ∈ˢ b ≡ Q x` and `x ∈ˢ b' ≡ Q x`, and composing the first with the reverse of the second yields `x ∈ˢ b ≡ x ∈ˢ b'`, exactly what extensionality turns into `b ≡ b'`. The second component is disposed of by `Σ≡Prop`, which is legitimate because `isPropIsSetOf` says the specifications of any two realizers are equal. Note the argument shape: the class `Q` and one realizer are explicit inputs, so the conclusion is literally that the type `SetOf Q` is contractible with the given realizer as center. ```agda setOf-unique : ({a b : S} → ((x : S) → (x ∈ˢ a) ≡ (x ∈ˢ b)) → a ≡ b) → (Q : S → hProp ℓ) → SetOf Q → isContr (SetOf Q) setOf-unique ext Q (b , sp) = (b , sp) , λ { (b' , sp') → Σ≡Prop (isPropIsSetOf Q) (ext (λ x → sp x ∙ sym (sp' x))) } ``` ## The description operator `isContr` is the host's **unique existence**: it packages a center together with the data contracting every element to that center. So `isContr (SetOf Q)` reads: *there is exactly one set of the `Q`s*, with the center supplying a canonical witness outright. Every existence axiom below takes this form, and the payoff is immediate: given unique existence, "the set such that" is a projection. No separate classical description axiom is needed, because the center of a contraction is already data. The operator `℩` takes a contraction proof of `SetOf Q` and returns its center's first component, an element of `S`: with `isContr A` packaged as a center together with a contraction, `c .fst` is the center, and one more projection reaches the set itself. This is where a classical treatment would invoke a description axiom; here the passage from unique existence to a witness is pure data extraction, and it is why every axiom below is stated with `isContr` rather than as a truncated existence. ```agda ℩ : {Q : S → hProp ℓ} → isContr (SetOf Q) → S ℩ c = c .fst .fst ``` The extracted set would be useless without a way to read back what its members are, and that reading is again a projection: `℩-spec c` is the specification carried by the center, that is, the second component of the first component of the contraction. Together the two say: the unique set of the `Q`s exists, and `℩` hands you that set together with the certificate `x ∈ˢ (℩ c) ≡ Q x`. Every derived operation in the next sections consists of applying `℩` to an axiom field and quoting `℩-spec` as its specification. ```agda ℩-spec : {Q : S → hProp ℓ} (c : isContr (SetOf Q)) → IsSetOf Q (℩ c) ℩-spec c = c .fst .snd ``` ## Subsets One derived relation completes the vocabulary: `a ⊆ˢ b` when every member of `a` is a member of `b`. This is extensionality's defining comparison, read as a truth value rather than as a hypothesis of a theorem. Unlike the axioms, which will return sets, it lives in `hProp ℓ`, and it is stated with the direct `hProp` universal quantifier rather than a host function type. The power set field and the choice-set form of the axiom of choice are phrased with it. The definition uses the direct `hProp` quantifier `∀[ x ] P x`, to conjoin the implications `x ∈ˢ a ⇒ x ∈ˢ b` over all `x` in the carrier. Staying inside `hProp ℓ` matters: the result is a truth value of the structure, comparable and combinable with the other connectives, whereas a metalevel function type would not be. The Type-valued underlying implication is available too, since each `(x ∈ˢ a) ⇒ (x ∈ˢ b)` in `hProp` has an underlying type, but the definition keeps everything truth-valued. ```agda _⊆ˢ_ : S → S → hProp ℓ a ⊆ˢ b = ∀[ x ∶ S ] (x ∈ˢ a) ⇒ (x ∈ˢ b) ``` The notation `a ⊆ˢ b` will be used inside the power-set axiom and in later arguments. Its precedence is fixed here so formulas containing membership, equality, and subset have an unambiguous reading. ```agda infix 20 _⊆ˢ_ ``` ## The axioms, as a record Here is the heart of the chapter. The fields group into three kinds. First, extensionality and the existence axioms: empty set, pairing, union, separation, replacement, power set, each in the unique-existence form just prepared, so each yields its set through `℩` (infinity joins later). Second, the two formula schemas: separation and replacement take a `Formula S 1` or `Formula S 2` and interpret it with the satisfaction relation of the semantics chapter, so the language built in the first-order logic chapters does real work here. The restriction is explicit: these fields range over encoded first-order formulas, rather than arbitrary host predicates `S → hProp ℓ`. Thus every instance used here comes with object-language syntax and is interpreted by the satisfaction relation. Third, regularity: well-foundedness of the Type-valued membership relation, recorded as `WellFounded _∈ᵗ_` from the host library. The next section explains why this axiom is stated at the meta level while the others live inside the structure. The record is a proposition-valued structure plus the guarantees the axioms demand, and it itself lives in `Type (ℓ-suc ℓ)` because its fields quantify over all of `S`. The first two fields are not of the unique-existence form. Extensionality is the implication from pointwise agreement of membership truth values to a path `a ≡ b`, exactly the hypothesis that made `setOf-unique` work. Regularity takes `WellFounded _∈ᵗ_`, well-foundedness of the Type-valued membership: this supplies `Acc` data for every element and thereby supports recursion and induction along membership. The remaining fields each assert `isContr (SetOf Q)` for a class `Q`. ```agda record isZFModel : Type (ℓ-suc ℓ) where field extensional : {a b : S} → ((x : S) → (x ∈ˢ a) ≡ (x ∈ˢ b)) → a ≡ b regularity : WellFounded _∈ᵗ_ hasEmpty : isContr (SetOf (λ _ → ⊥)) ``` Reading each class back into words recovers the textbook statements. Nothing realizes `⊥`, so the empty set is the unique set realizing the constantly-false class. The pair of `a` and `b` realizes the class of sets structurally equal to `a` or to `b`, joined by the direct `hProp` disjunction `⊔`. The union of `a` realizes the class of sets `x` that are members of some member `y` of `a`, conjoined by `⊓` and existentially gathered by `∃[ x ] P x`. Separation, the first formula-consuming field, keeps exactly those members `x` of `a` satisfying `φ`: the class is the conjunction of membership in `a` with the satisfaction of `φ` at the one-element environment `x ∷ []`, whose single entry fills the only free-variable slot of a `Formula S 1`. ```agda hasPair : (a b : S) → isContr (SetOf (λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b))) hasUnion : (a : S) → isContr (SetOf (λ x → ∃[ y ∶ S ] (y ∈ˢ a) ⊓ (x ∈ˢ y))) hasSeparation : (a : S) (φ : Formula S 1) → isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ))) hasReplacement : (a : S) (φ : Formula S 2) ``` Replacement is the longest field and carries a hypothesis of its own. It takes a `Formula S 2`, whose two free-variable slots are read in the order given by the environment `y ∷ x ∷ []`: first the output value, then the input. The hypothesis says `φ` is *functional on `a`*: for every member `x` of `a` there is exactly one `y` satisfying `φ`, exactly-oneness being the `isContr` of the type of such `y`. Under that hypothesis the field asserts unique existence of the image, the set of `y` that stand in the relation `φ` to some member of `a`. Note what it does not assert: without the functionality hypothesis the field makes no claim at all, mirroring the classical restriction of replacement to functional formulas. Finally, the power set of `a` realizes the class of subsets, using the derived relation `⊆ˢ` from the previous section. ```agda → ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩)) → isContr (SetOf (λ y → ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ))) hasPower : (a : S) → isContr (SetOf (λ x → x ⊆ˢ a)) ``` Read each `λ` back into words and the familiar statements reappear. Nothing realizes `⊥`, so `hasEmpty` is the empty set. The pair's members are whatever equals `a` or `b`; the union's members are the members of members. Separation keeps those members of `a` that satisfy `φ` (the environment `x ∷ []` plugs the sole free variable). Replacement first asks `φ` to be functional on `a`, one output per input in the `isContr` sense, then collects the outputs. The power set's members are the subsets. ## Why regularity lives at the meta level Every other axiom speaks either the object language or plain membership; regularity alone reaches for the host's notion of well-foundedness. The classical reason is that **no first-order sentence expresses external well-foundedness**: by the **compactness theorem** of classical model theory, any sentence true in exactly the well-founded structures would also hold in a structure carrying an infinite descending ∈-chain, since every finite fragment of the extended theory (a fresh constant chain $a_{n+1} \in a_n$) has a model. The book tells this argument but does not depend on it, and compactness is not developed here. The practical reason, visible in the type `WellFounded _∈ᵗ_` itself, is what this interface buys: well-foundedness as explicit data supports recursion and induction along membership. What is surrendered is that the condition is no longer visible to first-order formulas; this chapter makes no claim about how much that matters beyond what is proved below. ## The derived operations Now `℩` turns each unique existence into an operation, and `℩-spec` turns it into its specification; every specification below is literally one projection. The union of a pair gives binary union, and binary union gives the **successor** `a ⁺ = a ∪ {a}` (the pair of `a` with itself is the singleton): this is von Neumann's step from one set to the next, the step the axiom of infinity will later use. Inside the record, each field becomes an operation by applying `℩` to it. The empty set is `℩ hasEmpty`, and the pairing operation `pair a b` applies `℩` to the pairing certificate at the specific `a` and `b`. Each such application is justified because the fields provide `isContr (SetOf _)`, which is precisely the input type of `℩`. The specification `pair-spec` is not a new proof at all: it quotes `℩-spec` at the same field, and its statement is exactly the realization assertion, that `x ∈ˢ pair a b` equals the disjunction `(x ≈ˢ a) ⊔ (x ≈ˢ b)` for every `x`. ```agda ∅ : S ∅ = ℩ hasEmpty pair : S → S → S pair a b = ℩ (hasPair a b) pair-spec : ∀ a b → IsSetOf (λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b)) (pair a b) ``` The union operation `⋃ a` extracts the union certificate of `a`, and binary union is defined from it: `a ∪ b` is the union of the pair `pair a b`, which is exactly the set whose members are the members of `a` together with the members of `b`. No separate axiom is spent on binary union; it is a composite of pairing and union. Note the definition's direction: `∪` is built from `⋃` applied to a pair, not the reverse. ```agda pair-spec a b = ℩-spec (hasPair a b) ⋃ : S → S ⋃ a = ℩ (hasUnion a) _∪_ : S → S → S a ∪ b = ⋃ (pair a b) ``` Separation becomes an operation in the formula itself: `separate a φ` applies `℩` to the separation certificate at `a` and the formula `φ`, so the resulting set depends on a piece of object-language syntax. Its specification again quotes `℩-spec` verbatim, giving `x ∈ˢ separate a φ ≡ (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)` for every `x`: membership combines belonging to `a` with satisfying `φ`. The power set operation `𝒫 a` extracts the power set certificate, and its members will be read off, via the class it realizes, as exactly the subsets of `a`. ```agda separate : (a : S) → Formula S 1 → S separate a φ = ℩ (hasSeparation a φ) separate-spec : ∀ a φ → IsSetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)) (separate a φ) separate-spec a φ = ℩-spec (hasSeparation a φ) 𝒫 : S → S ``` The trailing blank line closes this block of operations; the next sections build on them, first deriving intersection without any new axiom. ```agda 𝒫 a = ℩ (hasPower a) ``` ## Intersection derived from separation Binary intersection is deliberately **not** a field. The two-symbol formula `var zero ∈̇ con b` says "the variable is a member of `b`"; pass it to `separate` at `a` and the axioms return `a ∩ b`. Its specification is exactly the separation specification, verbatim, because satisfaction of that formula computes to `x ∈ˢ b` by the defining clauses of `⊨`. This is a worked example of the general pattern: whenever a host predicate can be named by a formula, separation turns it into a set. The definition is one line of applied syntax: `a ∩ b` separates `a` along the formula whose only content is the atomic membership statement `var zero ∈̇ con b`. Because the constant `b` denotes itself under the interpretation `id`, satisfying that formula at the environment `x ∷ []` reduces, by the defining clauses of satisfaction, to the truth value `x ∈ˢ b`. The specification theorem is then the separation specification at this particular formula, unchanged: membership in the intersection is the conjunction `x ∈ˢ a ⊓ x ∈ˢ b`. No new axiom and no new existence proof are spent; a two-symbol formula already names a host predicate that separation can realize. ```agda _∩_ : S → S → S a ∩ b = separate a (var zero ∈̇ con b) ∩-spec : ∀ a b x → (x ∈ˢ (a ∩ b)) ≡ ((x ∈ˢ a) ⊓ (x ∈ˢ b)) ∩-spec a b x = separate-spec a (var zero ∈̇ con b) x ``` ## Infinity One axiom remains, the one that forces a genuinely infinite set into existence. The **numerals** are the von Neumann naturals: `∅`, `∅ ⁺`, `(∅ ⁺) ⁺`, and so on. The record takes the chain itself as a field, pinned down by two propositional equations phrased in raw membership and equality: the zeroth numeral has no members, and the members of a successor numeral are exactly the previous numeral and its members. By extensionality the two equations yield precisely `numeral zero ≡ ∅` and `numeral (suc n) ≡ numeral n ⁺`, so this is exactly as strong as defining the chain outright. What is gained is latitude: the equations never mention the derived `∅`, so a concrete model may present the chain in whatever form is most convenient to compute with on its carrier and discharge them without ever unfolding the description operator. The chain is a function `numeral : ℕ → S`, so indexing by the host's natural numbers is explicit data. The zero case is a negative condition: any inhabitant `z` of the Type-valued membership `z ∈ˢ numeral zero` yields a contradiction, witnessed in the empty host type `Empty.⊥`. Note the reading: `∈ˢ` returns a proposition in `hProp ℓ`, `⟨_⟩` takes its underlying type, and from an inhabitant of that type the field derives absurdity. This says the zeroth numeral has no members, without mentioning the derived empty set. ```agda field numeral : ℕ → S numeral-zero : (z : S) → ⟨ z ∈ˢ numeral zero ⟩ → Empty.⊥ numeral-suc : (n : ℕ) (z : S) → (⟨ z ∈ˢ numeral (suc n) ⟩ → ⟨ (z ∈ˢ numeral n) ⊔ (z ≈ˢ numeral n) ⟩) ``` The successor case is a pair of implications, both inside the truncated-free propositional reading. The first says a member `z` of `numeral (suc n)` is a member of `numeral n` or structurally equal to it, the disjunction being the hProp `⊔`; the second says every such member of the previous numeral, or thing equal to it, is a member of the successor. Together the two directions say the members of a successor numeral are exactly the previous numeral together with its members, which is exactly the von Neumann step, stated only with `∈ˢ` and `≈ˢ`. ```agda × (⟨ (z ∈ˢ numeral n) ⊔ (z ≈ˢ numeral n) ⟩ → ⟨ z ∈ˢ numeral (suc n) ⟩) ``` `isNumeral` determines the class of objects *equal to some numeral*. The quantification runs over `ℕ` lifted to the working level, since the indexing data lives at the bottom universe. The chosen form of the **axiom of infinity** says that this exact class is a set. Consequently `ω` is characterized in both directions: every numeral belongs to it, and every member is equal to a numeral. The class `isNumeral` is an existential written directly in `hProp`: `∃[ x ] P x` quantifies over a carrier type and disjoins the family of propositions `x ≈ˢ numeral (lower n)`. The carrier must have type `Type ℓ` for `∃[ x ] P x` to apply, but `ℕ` lives at `Type ℓ-zero`; `Lift {ℓ-zero} {ℓ} ℕ` raises it to the working level, and `lower` recovers the plain index to feed to `numeral`. This is a level adjustment, not a mathematical change: the lifted type carries exactly the same elements. The field `hasInfinity` then asserts, in the now-familiar form, unique existence of a set realizing this class. ```agda isNumeral : S → hProp ℓ isNumeral x = ∃[ n ∶ Lift {ℓ-zero} {ℓ} ℕ ] x ≈ˢ numeral (lower n) field hasInfinity : isContr (SetOf isNumeral) ω : S ``` As with every other unique existence, `ω` is the centre extracted by `℩` from `hasInfinity`. Because the class realized is `isNumeral` itself, the specification `℩-spec` says every member of `ω` is equal to some numeral; that is what makes this strong form usable as the set of naturals, not merely a set into which the numerals embed. ```agda ω = ℩ hasInfinity ``` ## First theorems Extensionality upgrades the whole existence machinery once and for all: by `setOf-unique`, whenever a class has a realizer, that realizer is the unique realizer, and the realizer's type is contractible with it as center. Every derived set of this chapter therefore comes with its uniqueness. ## ZFC: choice as an extension The **axiom of choice** is taken in choice-set form: given a set `a` whose members are nonempty and pairwise disjoint, some set meets each member of `a` in exactly one point. This form is stated with membership and the derived intersection alone; its equivalence with the other formulations is model-internal mathematics, deferred until needed. Propositional truncation `∥_∥₁` appears around nonemptiness, the evidence of a shared point, and the existence of a choice set. Thus the axiom asserts existence without selecting witnesses globally. Keeping it as a separate extension rather than a field of the base record preserves the distinction between what ZF proves and what choice adds. The ZFC record extends rather than repeats: its first field is an entire ZF model, and the line `open ... public` re-exports all its fields, so anything provable for a ZF model applies verbatim to a ZFC model. Only after this opening does the record declare its own new field, keeping the added axiom cleanly separated from the base theory. ```agda record isZFCModel : Type (ℓ-suc ℓ) where field zf : isZFModel open isZFModel zf public field ``` The two hypotheses of `hasChoice` say that `a` is a family of nonempty, pairwise disjoint sets, each in the reading available here. Nonemptiness is truncated: for each member `x` of `a` there *merely* exists a `y` in it, `∥ Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ ∥₁`, with no chosen witness. Pairwise disjointness is also truncated: if `x` and `y` are two members of `a` that *merely* share a point `z`, then `x ≡ y` holds outright. Note the shape of the disjointness premise: its conclusion is a path in the host, so the truncation of the shared-point evidence is what feeds an untruncated equality. ```agda hasChoice : (a : S) → ((x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ ∥₁) → ((x y : S) → ⟨ x ∈ˢ a ⟩ → ⟨ y ∈ˢ a ⟩ → ∥ Σ[ z ∈ S ] (⟨ z ∈ˢ x ⟩ × ⟨ z ∈ˢ y ⟩) ∥₁ → x ≡ y) ``` The conclusion is likewise a truncated existence: there *merely* exists a choice set `c` such that for every member `x` of `a`, the intersection `c ∩ x` has exactly one element, expressed as `isContr` of the type of its elements. The inner `isContr` is not a truncation: for each `x`, it provides an element of `c ∩ x` and proves that every other such element equals it. The outer truncation applies to the existence of a suitable `c`, so the axiom supplies no distinguished choice set. ```agda → ∥ Σ[ c ∈ S ] ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)) ∥₁ ``` ## Recap A model of ZF is a record with three kinds of fields: extensionality, which makes realizers unique; unique-existence fields for empty set, pair, union, separation, replacement and power set, with separation and replacement restricted to the book's own formulas; and regularity, stated at the meta level as host well-foundedness of membership, so that recursion and induction along membership are available. `℩` turns fields into operations whose specifications are projections; binary union and successor are composites, and intersection was obtained from separation plus a two-symbol formula whose satisfaction computes directly. Infinity enters as the numeral chain, a function `ℕ → S` fixed by raw membership equations, and the strong form makes `ω` a set all of whose members are numerals. `isZFCModel` adds choice on top, with truncated nonemptiness and shared-point evidence, a truncated conclusion, and an untruncated `isContr` for each chosen intersection.