BedrockV ⊨ ZF(C)
Time to settle the account. The model record demands twelve fields; two are banked (extensionality and regularity, from the hierarchy chapter), and the smallness chapter's free tier covers separation only for Δ₀ witnesses, while the record wants it for every formula. This chapter delivers the rest: the stock sets that the library simply has (empty, pair, union), replacement and strong infinity, which turn out to cost nothing, and then the two genuine debts, full separation and power set, whose exact price is a resizing assumption. With that assumption paid, the record is assembled: V is a model of ZF, the relative-consistency theorem this part exists to prove. Choice then enters as a second, independent assumption, and upgrades the model to ZFC.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth module V.Model {ℓ : Level} where open import Base.Impredicativity using ( HPropSmallness; Impredicativity ) open import Base.Classical using ( LEM; lem→impredicativity ) open import Base.Choice using ( SetChoice; choice→lem; lowerSetChoice ) open import FOL.ZFStructure using ( ZFStructure ) open import FOL.Syntax using ( Formula ) import FOL.Semantics import FOL.ZFModel open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV ) open import V.Smallness {ℓ} using ( separateFromSmall ) open import Cubical.Foundations.Equiv using ( equivFun; invEq; secEq ) open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.Functions.Embedding using ( Embedding-into-isSet→isSet; isEmbedding→Inj ) open import Cubical.Data.Sigma using ( Σ≡Prop ) import Cubical.Data.Sum as Sum import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( sett; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber ; identityPrinciple; _⊆_; extensionality ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; ∅-empty; ⁅_,_⁆; pairing-ax; ⋃_; union-ax; ⁅_⁆s; _∪_ ; SingletonPackage; module InfinitySet ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( SetPackage ) -- lint-agda: keep (used qualified: SetPackage.classification) open InfinitySet using ( sucV; #_; ω ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open ZFStructure 𝒮ᵥ module Model = FOL.ZFModel 𝒮ᵥ open Model using ( SetOf; _⊆ˢ_; setOf-unique; isZFModel; isZFCModel ) module SemanticsV = FOL.Semantics (hPropAlgebra (ℓ-suc ℓ)) 𝒮ᵥ open SemanticsV.At S id using ( _⊨_ )
The stock sets
Empty set, pair, and union sit in the library ready-made, each with its axiom. Only the shape needs converting, and the recipe is the same three moves every time: the library states its axiom in small form (∈ₛ), ∈∈ₛ reshapes membership pointwise, and ⇔toPath lands the bi-implication as the path the record's field wants. For the pair the fit is even closer: the library's "equal to a or to b" is the field's (x ≈ˢ a) ⊔ (x ≈ˢ b) definitionally, so the glue is one layer of ∈∈ₛ and nothing else.
empty-spec : (x : S) → (x ∈ˢ ∅) ≡ ⊥ empty-spec x = ⇔toPath (λ x∈ → Empty.rec (∅-empty x (∈∈ₛ {a = x} {b = ∅} .fst x∈))) (λ ()) pair-spec : (a b x : S) → (x ∈ˢ ⁅ a , b ⁆) ≡ ((x ≈ˢ a) ⊔ (x ≈ˢ b)) pair-spec a b x = ⇔toPath (λ x∈ → pairing-ax a b x .fst (∈∈ₛ {a = x} {b = ⁅ a , b ⁆} .fst x∈)) (λ h → ∈∈ₛ {a = x} {b = ⁅ a , b ⁆} .snd (pairing-ax a b x .snd h)) union-spec : (a x : S) → (x ∈ˢ (⋃ a)) ≡ ⋁ S (λ y → (y ∈ˢ a) ⊓ (x ∈ˢ y)) union-spec a x = ⇔toPath (λ x∈ → PT.map (λ { (v , va , xv) → v , ∈∈ₛ {a = v} {b = a} .snd va , ∈∈ₛ {a = x} {b = v} .snd xv }) (union-ax a x .fst (∈∈ₛ {a = x} {b = ⋃ a} .fst x∈))) (λ h → ∈∈ₛ {a = x} {b = ⋃ a} .snd (union-ax a x .snd (PT.map (λ { (v , va , xv) → v , ∈∈ₛ {a = v} {b = a} .fst va , ∈∈ₛ {a = x} {b = v} .fst xv }) h)))
Replacement, for free
Replacement is the first surprise of the chapter: a schema that costs nothing. The reason is sett itself. Given φ functional on a, index the image by the small member type ⟪ a ⟫ and write the image set down directly; no axiom is consulted. The delicate direction is recovering an index from a membership fact, and it is the smallness chapter's refrain once more: the fibers of ∈-asFiber are untruncated, so "member to index" is a function, not a choice.
private memb : (a : S) (m : ⟪ a ⟫) → ⟨ ⟪ a ⟫↪ m ∈ˢ a ⟩ memb a m = ∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m) module _ (a : S) (φ : Formula S 2) (fc : (x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩)) where replaceImage : S replaceImage = sett ⟪ a ⟫ (λ m → fc (⟪ a ⟫↪ m) (memb a m) .fst .fst) replaceImage-spec : ∀ y → (y ∈ˢ replaceImage) ≡ ⋁ S (λ x → (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ)) replaceImage-spec y = ⇔toPath fwd bwd where fwd : ⟨ y ∈ˢ replaceImage ⟩ → ⟨ ⋁ S (λ x → (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ)) ⟩ fwd = PT.map λ { (m , q) → ⟪ a ⟫↪ m , memb a m , subst (λ v → ⟨ (v ∷ ⟪ a ⟫↪ m ∷ []) ⊨ φ ⟩) q (fc (⟪ a ⟫↪ m) (memb a m) .fst .snd) } bwd : ⟨ ⋁ S (λ x → (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ)) ⟩ → ⟨ y ∈ˢ replaceImage ⟩ bwd = PT.map λ { (x , x∈a , hφ) → let mf = ∈-asFiber {a = x} {b = a} x∈a hφ' = subst (λ v → ⟨ (y ∷ v ∷ []) ⊨ φ ⟩) (sym (mf .snd)) hφ in mf .fst , cong fst (fc (⟪ a ⟫↪ (mf .fst)) (memb a (mf .fst)) .snd (y , hφ')) }
The numeral chain and ω
The library's ω is sett over Lift ℕ with the library numerals # as the family, so its membership is definitionally "merely hit by some #": strong infinity in exactly the record's sense, before any proof is written. What remains is bookkeeping in two steps. First, the model's chain must align with the library's: numeralV steps by a ∪ ⁅ a , a ⁆ while # steps by sucV a = a ∪ ⁅ a ⁆s, and the only genuine gap is ⁅ a , a ⁆ ≡ ⁅ a ⁆s, one appeal to extensionality (the two families differ only in index type).
pair-singleton : (a : S) → ⁅ a , a ⁆ ≡ ⁅ a ⁆s pair-singleton a = extensionality ⁅ a , a ⁆ ⁅ a ⁆s (s1 , s2) where singl-cls = SetPackage.classification (SingletonPackage a) s1 : ⟨ ⁅ a , a ⁆ ⊆ ⁅ a ⁆s ⟩ s1 x x∈ₛ = singl-cls x .snd (PT.rec (setIsSet x a) (λ { (Sum.inl e) → e ; (Sum.inr e) → e }) (pairing-ax a a x .fst x∈ₛ)) s2 : ⟨ ⁅ a ⁆s ⊆ ⁅ a , a ⁆ ⟩ s2 x x∈ₛ = pairing-ax a a x .snd ∣ Sum.inl (singl-cls x .fst x∈ₛ) ∣₁ numeralV : ℕ → S numeralV zero = ∅ numeralV (suc n) = numeralV n ∪ ⁅ numeralV n , numeralV n ⁆ numeralV≡# : (n : ℕ) → numeralV n ≡ # n numeralV≡# zero = refl numeralV≡# (suc n) = cong₂ (λ u v → ⋃ ⁅ u , v ⁆) (numeralV≡# n) (cong (λ u → ⁅ u , u ⁆) (numeralV≡# n) ∙ pair-singleton (# n)) ω-specV : (x : S) → (x ∈ˢ ω) ≡ ⋁ (Lift {ℓ-zero} {ℓ-suc ℓ} ℕ) (λ n → x ≈ˢ numeralV (lower n)) ω-specV x = ⇔toPath (PT.map (λ { (i , p) → lift (lower i) , sym p ∙ sym (numeralV≡# (lower i)) })) (PT.map (λ { (n , q) → lift (lower n) , sym (q ∙ numeralV≡# (lower n)) }))
Second, the record's two pinning equations speak of membership in a successor, so the chapter needs the case analysis for sucV: a member of sucV A is merely a member of A or equal to A, and both inclusions back. The proofs unfold sucV through the union and pairing axioms once, with the singleton's classification closing the second disjunct.
private singl≡ : (A x : S) → ⟨ x ∈ₛ ⁅ A ⁆s ⟩ → x ≡ A singl≡ A x = SetPackage.classification (SingletonPackage A) x .fst ∈sucV-elim : {A x : S} {P : Type (ℓ-suc ℓ)} → isProp P → ⟨ x ∈ˢ sucV A ⟩ → (⟨ x ∈ˢ A ⟩ → P) → (x ≡ A → P) → P ∈sucV-elim {A} {x} pP x∈ kA k≡ = PT.rec pP (λ { (v , (v∈₂ , x∈v)) → PT.rec pP (λ { (Sum.inl v≡A) → kA (∈∈ₛ {a = x} {b = A} .snd (subst (λ w → ⟨ x ∈ₛ w ⟩) v≡A x∈v)) ; (Sum.inr v≡s) → k≡ (singl≡ A x (subst (λ w → ⟨ x ∈ₛ w ⟩) v≡s x∈v)) }) (pairing-ax A ⁅ A ⁆s v .fst v∈₂) }) (union-ax ⁅ A , ⁅ A ⁆s ⁆ x .fst (∈∈ₛ {a = x} {b = sucV A} .fst x∈)) ∈sucV-inl : {A x : S} → ⟨ x ∈ˢ A ⟩ → ⟨ x ∈ˢ sucV A ⟩ ∈sucV-inl {A} {x} x∈A = ∈∈ₛ {a = x} {b = sucV A} .snd (union-ax ⁅ A , ⁅ A ⁆s ⁆ x .snd ∣ A , (pairing-ax A ⁅ A ⁆s A .snd ∣ Sum.inl refl ∣₁ , ∈∈ₛ {a = x} {b = A} .fst x∈A) ∣₁) self∈sucV : (a : S) → ⟨ a ∈ˢ sucV a ⟩ self∈sucV a = ∈∈ₛ {a = a} {b = sucV a} .snd (union-ax ⁅ a , ⁅ a ⁆s ⁆ a .snd ∣ ⁅ a ⁆s , (pairing-ax a ⁅ a ⁆s ⁅ a ⁆s .snd ∣ Sum.inr refl ∣₁ , SetPackage.classification (SingletonPackage a) a .snd refl) ∣₁)
The price of the rest
Two fields remain, full separation and power set, and neither is free: both need truth values brought down a universe with no Δ₀ witness to pay the fare. The price is exactly Part 0's impredicativity packing: resizing compresses any proposition, and hPropSmallness is the small classifier the power set will be indexed by. Nothing here is an axiom; the assembly takes the packing as a parameter, and the classical reader rides free through
lem→impredicativity, which is what the dividends were saved for.
Power set
The power set is the one construction the library's own header disclaims, and the small classifier is precisely what builds it. Index the candidate subsets by small characteristic functions ⟪ a ⟫ → Ω'; realizing one as a set is a sett over the members it selects. The delicate direction again runs through untruncated fibers: from an actual subset s, the characteristic function m ↦ encode (⟪ a ⟫↪ m ∈ₛ s) is recovered as a function, and extensionality closes the loop.
module Power (sΩ : HPropSmallness ℓ) where private decode : sΩ .fst → hProp ℓ decode = equivFun (sΩ .snd) encode : hProp ℓ → sΩ .fst encode = invEq (sΩ .snd) decode∘encode : (P : hProp ℓ) → decode (encode P) ≡ P decode∘encode = secEq (sΩ .snd) F : (a : S) → (⟪ a ⟫ → sΩ .fst) → S F a χ = sett (Σ[ m ∈ ⟪ a ⟫ ] ⟨ decode (χ m) ⟩) (λ p → ⟪ a ⟫↪ (p .fst)) 𝒫V : S → S 𝒫V a = sett (⟪ a ⟫ → sΩ .fst) (F a) private fwd : (a x : S) → ⟨ x ∈ˢ 𝒫V a ⟩ → ⟨ x ⊆ a ⟩ fwd a x = PT.rec ((x ⊆ a) .snd) λ { (χ , p) y y∈ₛx → PT.rec ((y ∈ₛ a) .snd) (λ { ((m , _) , q) → subst (λ v → ⟨ v ∈ₛ a ⟩) q (∈ₛ⟪ a ⟫↪ m) }) (∈∈ₛ {a = y} {b = F a χ} .snd (subst (λ v → ⟨ y ∈ₛ v ⟩) (sym p) y∈ₛx)) } bwd : (a x : S) → ⟨ x ⊆ a ⟩ → ⟨ x ∈ˢ 𝒫V a ⟩ bwd a x sub = ∣ χₓ , extensionality (F a χₓ) x (s1 , s2) ∣₁ where χₓ : ⟪ a ⟫ → sΩ .fst χₓ m = encode (⟪ a ⟫↪ m ∈ₛ x) s1 : ⟨ F a χₓ ⊆ x ⟩ s1 y y∈ₛF = PT.rec ((y ∈ₛ x) .snd) (λ { ((m , h) , q) → subst (λ v → ⟨ v ∈ₛ x ⟩) q (subst ⟨_⟩ (decode∘encode (⟪ a ⟫↪ m ∈ₛ x)) h) }) (∈∈ₛ {a = y} {b = F a χₓ} .snd y∈ₛF) s2 : ⟨ x ⊆ F a χₓ ⟩ s2 y y∈ₛx = ∈∈ₛ {a = y} {b = F a χₓ} .fst ∣ (m₀ , h) , q ∣₁ where m₀ = sub y y∈ₛx .fst q : ⟪ a ⟫↪ m₀ ≡ y q = equivFun identityPrinciple (sub y y∈ₛx .snd) h : ⟨ decode (χₓ m₀) ⟩ h = subst ⟨_⟩ (sym (decode∘encode (⟪ a ⟫↪ m₀ ∈ₛ x))) (subst (λ v → ⟨ v ∈ₛ x ⟩) (sym q) y∈ₛx) power-spec : (a x : S) → (x ∈ˢ 𝒫V a) ≡ (x ⊆ˢ a) power-spec a x = ⇔toPath {P = x ∈ˢ 𝒫V a} {Q = x ⊆ a} (fwd a x) (bwd a x) ∙ ⇔toPath {P = x ⊆ a} {Q = x ⊆ˢ a} (λ s y y∈x → ∈∈ₛ {a = y} {b = a} .snd (s y (∈∈ₛ {a = y} {b = x} .fst y∈x))) (λ f y y∈ₛx → ∈∈ₛ {a = y} {b = a} .fst (f y (∈∈ₛ {a = y} {b = x} .snd y∈ₛx)))
Assembly: V ⊨ ZF
Given the impredicativity parameter, full separation is the smallness chapter's pipe with the fare paid by resizing instead of a Δ₀ witness, and every field is on the table. One discipline governs the assembly: each unique-existence field takes a library set as its centre, so that the description operator's projections compute back to the stock sets by definition. The two pinning equations for the numeral chain are discharged through the sucV case analysis, riding numeralV≡# between the model's chain and the library's.
module VModel (imp : Impredicativity ℓ) where open Impredicativity imp open Power hPropSmallness public separateFull : (a : S) (φ : Formula S 1) → Σ[ s ∈ S ] (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ ((y ∷ []) ⊨ φ))) separateFull a φ = separateFromSmall a (λ y → (y ∷ []) ⊨ φ) (λ y → resizing ((y ∷ []) ⊨ φ)) V⊨ZF-impredicative : isZFModel V⊨ZF-impredicative = record { extensional = extensionalV ; regularity = regularityV ; hasEmpty = one _ (∅ , empty-spec) ; hasPair = λ a b → one _ (⁅ a , b ⁆ , pair-spec a b) ; hasUnion = λ a → one _ (⋃ a , union-spec a) ; hasSeparation = λ a φ → one _ (separateFull a φ) ; hasReplacement = λ a φ fc → one _ (replaceImage a φ fc , replaceImage-spec a φ fc) ; hasPower = λ a → one _ (𝒫V a , power-spec a) ; numeral = numeralV ; numeral-zero = pin0 ; numeral-suc = pinS ; hasInfinity = one _ (ω , ω-specV) } where pin0 : (z : S) → ⟨ z ∈ˢ numeralV zero ⟩ → Empty.⊥ pin0 z z∈ = ∅-empty z (∈∈ₛ {a = z} {b = ∅} .fst z∈) pinS : (n : ℕ) (z : S) → (⟨ z ∈ˢ numeralV (suc n) ⟩ → ⟨ (z ∈ˢ numeralV n) ⊔ (z ≈ˢ numeralV n) ⟩) × (⟨ (z ∈ˢ numeralV n) ⊔ (z ≈ˢ numeralV n) ⟩ → ⟨ z ∈ˢ numeralV (suc n) ⟩) pinS n z = fwd , bwd where fwd : ⟨ z ∈ˢ numeralV (suc n) ⟩ → ⟨ (z ∈ˢ numeralV n) ⊔ (z ≈ˢ numeralV n) ⟩ fwd z∈ = ∈sucV-elim {A = # n} {x = z} (snd ((z ∈ˢ numeralV n) ⊔ (z ≈ˢ numeralV n))) (subst (λ w → ⟨ z ∈ˢ w ⟩) (numeralV≡# (suc n)) z∈) (λ z∈#n → ∣ Sum.inl (subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (numeralV≡# n)) z∈#n) ∣₁) (λ z≡#n → ∣ Sum.inr (z≡#n ∙ sym (numeralV≡# n)) ∣₁) bwd : ⟨ (z ∈ˢ numeralV n) ⊔ (z ≈ˢ numeralV n) ⟩ → ⟨ z ∈ˢ numeralV (suc n) ⟩ bwd = PT.rec (snd (z ∈ˢ numeralV (suc n))) (λ { (Sum.inl z∈n) → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (numeralV≡# (suc n))) (∈sucV-inl {A = # n} (subst (λ w → ⟨ z ∈ˢ w ⟩) (numeralV≡# n) z∈n)) ; (Sum.inr z≡n) → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (numeralV≡# (suc n))) (subst (λ w → ⟨ w ∈ˢ sucV (# n) ⟩) (sym (z≡n ∙ numeralV≡# n)) (self∈sucV (# n))) }) one : (Q : S → hProp (ℓ-suc ℓ)) → SetOf Q → isContr (SetOf Q) one = setOf-unique extensionalV
This is the semantic relative-consistency theorem this part promised: within cubical Agda and its universes, granted impredicativity, the cumulative hierarchy is a model of ZF. The schemas are honoured for all formulas at once; the deep embedding of Part 1 takes its first full load here. The name carries the exact hypothesis as a suffix, and the unsuffixed headline is the classical redemption:
V⊨ZF : LEM (ℓ-suc ℓ) → isZFModel V⊨ZF lem = VModel.V⊨ZF-impredicative (lem→impredicativity lem)
Choice, independently
The excluded middle does not prove choice, so upgrading to ZFC costs a genuinely new assumption: the choice chapter's SetChoice. (Recall that the dependence runs the other way, choice→lem; the section after this one cashes exactly that.) Choice is applied only at small member types, asserting the choice of indices, the lowest level at which the statement makes sense. From it, the model's choice-set axiom follows for any ZF model on this carrier, not just the one assembled above: the proof consumes nothing about how the model was built, only its ∩ and extensionality, which is worth savouring, choice here is a structural fact about ZF models on V, not a constructional accident. The choice set is sett over the chosen indices, and disjointness plus the embedding property pin its intersection with each member to exactly one point.
private isSet⟪_⟫ : (a : S) → isSet ⟪ a ⟫ isSet⟪ a ⟫ = Embedding-into-isSet→isSet (⟪ a ⟫↪ , isEmb⟪ a ⟫↪) setIsSet isContrΣ-fromCenter : {P : S → hProp (ℓ-suc ℓ)} (z₀ : S) (p₀ : z₀ ∈ᶜ P) → ((z : S) → z ∈ᶜ P → z₀ ≡ z) → isContr (Σ[ z ∈ S ] (z ∈ᶜ P)) isContrΣ-fromCenter {P} z₀ p₀ u = (z₀ , p₀) , λ w → Σ≡Prop (λ v → snd (P v)) (u (w .fst) (w .snd)) module ChoiceLemma (zf : isZFModel) (ac : SetChoice ℓ) where open Model.isZFModel zf using ( _∩_; ∩-spec ) choice : (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) → ∥ Σ[ c ∈ S ] ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)) ∥₁ choice a inh disj = PT.map mk (ac ⟪ a ⟫ isSet⟪ a ⟫ (λ m → ⟪ ⟪ a ⟫↪ m ⟫) pick) where pick : (m : ⟪ a ⟫) → ∥ ⟪ ⟪ a ⟫↪ m ⟫ ∥₁ pick m = PT.map (λ { (y , y∈) → ∈-asFiber {a = y} {b = ⟪ a ⟫↪ m} y∈ .fst }) (inh (⟪ a ⟫↪ m) (memb a m)) mk : ((m : ⟪ a ⟫) → ⟪ ⟪ a ⟫↪ m ⟫) → Σ[ c ∈ S ] ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)) mk g = c , uniq where chosen : ⟪ a ⟫ → S chosen m = ⟪ ⟪ a ⟫↪ m ⟫↪ (g m) c : S c = sett ⟪ a ⟫ chosen chosen∈ : (m : ⟪ a ⟫) → ⟨ chosen m ∈ˢ ⟪ a ⟫↪ m ⟩ chosen∈ m = ∈∈ₛ {a = chosen m} {b = ⟪ a ⟫↪ m} .snd (∈ₛ⟪ ⟪ a ⟫↪ m ⟫↪ (g m)) uniq : (x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩) uniq x x∈a = isContrΣ-fromCenter {P = λ z → z ∈ˢ (c ∩ x)} z₀ pf₀ uniqz where mf = ∈-asFiber {a = x} {b = a} x∈a m₀ = mf .fst z₀ = chosen m₀ pf₀ : ⟨ z₀ ∈ˢ (c ∩ x) ⟩ pf₀ = subst ⟨_⟩ (sym (∩-spec c x z₀)) ( ∣ m₀ , refl ∣₁ , subst (λ w → ⟨ z₀ ∈ˢ w ⟩) (mf .snd) (chosen∈ m₀) ) uniqz : (z : S) → ⟨ z ∈ˢ (c ∩ x) ⟩ → z₀ ≡ z uniqz z pf = PT.rec (setIsSet z₀ z) (λ { (m , q) → let z∈m : ⟨ z ∈ˢ ⟪ a ⟫↪ m ⟩ z∈m = subst (λ w → ⟨ w ∈ˢ ⟪ a ⟫↪ m ⟩) q (chosen∈ m) x≡m : x ≡ ⟪ a ⟫↪ m x≡m = disj x (⟪ a ⟫↪ m) x∈a (memb a m) ∣ z , zcx .snd , z∈m ∣₁ m≡m₀ : m ≡ m₀ m≡m₀ = isEmbedding→Inj isEmb⟪ a ⟫↪ m m₀ (sym x≡m ∙ sym (mf .snd)) in sym (cong chosen m≡m₀) ∙ q }) (zcx .fst) where zcx : ⟨ z ∈ˢ c ⟩ × ⟨ z ∈ˢ x ⟩ zcx = subst ⟨_⟩ (∩-spec c x z) pf
V ⊨ ZFC, on choice alone
The ZFC theorem now assembles from one hypothesis, one instance, with Diaconescu's theorem paying every other bill. Choice at the truth level ℓ-suc ℓ decides that level's propositions, funding the whole impredicativity packing; and the same instance, lowered one universe, feeds the choice set. One choice, at the model's own truth level, is the entire price of V ⊨ ZFC. (The finer accounting stays visible in the pieces: VModel charges exactly impredicativity, ChoiceLemma exactly one level of choice; only their sum is stated here.)
V⊨ZFC : SetChoice (ℓ-suc ℓ) → isZFCModel V⊨ZFC ac = record { zf = base ; hasChoice = ChoiceLemma.choice base (lowerSetChoice ac) } where base : isZFModel base = V⊨ZF (choice→lem ac)
Recap
The account closes balanced. Empty set, pair, and union were library stock reshaped by ∈∈ₛ and ⇔toPath; replacement came free through sett over untruncated fibers; strong infinity was ω's definition plus one chain alignment (numeralV≡#). The two debts, full separation and power set, cost exactly Part 0's Impredicativity packing: assembly gives
V⊨ZF-impredicative at that exact price, the excluded middle redeems it into the headline V⊨ZF, and by Diaconescu the choice interface alone funds V⊨ZFC. The universe that Part 4 will dig inside now exists.