The cumulative hierarchy models ZF and ZFC

This chapter realizes each axiom of ZF inside the cumulative hierarchy at one fixed universe level ℓ. For each axiom asserting the existence of a set, the task is to exhibit that set together with a proof that its membership relation is, as a path of truth values, exactly the required description. The assumptions involved are worth separating at the outset. The stock constructions, namely the empty set, pairing, and union, cost nothing beyond the hierarchy's own set former, and the same is true of replacement, which is read directly off the membership rule of that former. Full separation needs propositional resizing, so that each satisfaction proposition gets a representative one universe down. Power set needs a small classifier for propositions, HPropSmallness. Resizing and the classifier are packaged together as Impredicativity, and the assembled ZF theorem V⊨ZF assumes exactly LEM (ℓ-suc ℓ), from which the package follows. For its ZFC part, the theorem V⊨ZFC separately assumes set-level choice at ℓ-suc ℓ; by Diaconescu's theorem it implies the excluded middle used for the ZF part, and, lowered one universe, it supplies the choice-set axiom. The chapter builds up to these two theorems by converting, one axiom at a time, the constructions the hierarchy already provides into the exact shape the axioms demand.

The universe accounting is exact and should be read once. The carrier of the model is the hierarchy S at level ℓ, itself an inhabitant of Type (ℓ-suc ℓ). The truth values serving as the model's equality and membership live in hProp (ℓ-suc ℓ). The package Impredicativity ℓ couples the two smallness principles used below: resizing at that truth level, and the small classifier HPropSmallness ℓ, a small type equivalent to all of hProp ℓ. The choice lemma consumes set-level choice at level ℓ, and the final corollaries assume LEM (ℓ-suc ℓ) and SetChoice (ℓ-suc ℓ) respectively. So no single uniform level governs every assumption; each principle is taken exactly where its statement makes sense.

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude

module V.Model {ℓ : Level} where

open import Base.Impredicativity using ( HPropSmallness; Impredicativity )

Formally, what does it mean for the hierarchy to satisfy an axiom? The first-order logic chapters supply the vocabulary. A structure is a carrier that is an h-set, whose equality and membership take truth values, not booleans of a fixed two-element type. A formula is an element of the object language's syntax, and the axiom schemas quantify over its free-variable slots. Satisfaction is a relation that reads a formula at an environment of carrier elements and returns a truth value. The ZF axioms are re-derived one by one in exactly these terms below.

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

The hierarchy contributes the structure 𝒮ᵥ: its equality is the path type of the higher inductive type V ℓ, and its membership is the hierarchy's native ∈. Extensionality and regularity for this structure were proved in the chapter on the hierarchy itself and are quoted here rather than reproved. One further tool is carried over from the smallness chapter: the adapter that builds a set from a predicate each of whose values is small. It becomes full separation as soon as resizing supplies the smallness. Throughout, a bi-implication of propositions is converted into the path between their truth values by the standard rewriting ⇔toPath; almost every specification below ends with that step.

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 )

Three general cubical facts shape the proofs to come. An embedding into a type whose equality types are propositions is injective, which matters whenever a recovered index must be shown to be the only possible one. A path between dependent pairs whose second components are propositions is fixed by the paths between first projections. And membership statements about image sets are typically truncated existentials: they are introduced by ∣_∣₁ and eliminated with PT.rec into proposition-valued targets, while contradictions are handled by the empty type.

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

The central construction is the set former sett: from a small index type X and a family X → S it forms the image set, and y ∈ sett X ix holds exactly when some index presents y, merely. Replacement is read directly off this membership rule. That the hierarchy is an h-set, recorded by setIsSet, is what makes the path type x ≡ y a proposition and hence a legitimate truth value for the structure's equality.

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base
  using ( sett; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties

Membership comes in two shapes, and the whole chapter moves between them. Every set a has a small type of indices ⟪ a ⟫ with an embedding ⟪ a ⟫↪ whose image is a; the small membership x ∈ₛ a says that some index presents x. The equivalence ∈∈ₛ converts between small and ordinary membership pointwise in both directions, and ∈-asFiber does more: from a proof of x ∈ a it returns an actual, untruncated pair of an index and a presenting path. That untruncatedness is what lets index recovery be a function rather than a choice. The stock sets are also ready-made: the empty set with its refutation ∅-empty, the pair ⁅ a , b ⁆ with pairing-ax, the union ⋃ a with union-ax, the singleton ⁅ a ⁆s with its classification, and the binary union _∪_.

  using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber
        ; identityPrinciple; _⊆_; extensionality )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; ⁅_,_⁆; pairing-ax; ⋃_; union-ax; ⁅_⁆s; _∪_
        ; SingletonPackage; module InfinitySet )

A worked conversion shows the method that every specification proof uses. For the pair, the library's pairing-ax states a bi-implication between x ∈ₛ ⁅ a , b ⁆ and the disjunction x ≡ₕ a ⊔ x ≡ₕ b; for this structure ≡ₕ u v is the path type u ≡ v, which is definitionally what the structure's ≈ˢ u v is. So the pairing specification, proved in the next section, is just ⇔toPath applied to pairing-ax with one layer of ∈∈ₛ threaded through each direction: forward turns the ordinary membership into the small one the classification consumes, backward turns the resulting disjunction back into an ordinary membership. The same three moves convert the empty set, the union, and, with one more truncation layer, membership in the union of an indexed family.

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( SetPackage )  -- lint-agda: keep (used qualified: SetPackage.classification)
open InfinitySet using ( sucV; #_; ω )

open ZFStructure 𝒮ᵥ

The target of all these conversions is the record isZFModel, whose fields are the ZF axioms: extensionality, regularity, empty set, pairing, union, separation, replacement, power set, and strong infinity through a numeral chain with two pinning equations. Each existence field asks for an isContr (SetOf Q): a set realizing the class Q together with uniqueness data, which extensionality supplies; isZFCModel adds the choice-set field. Satisfaction for the deep-embedded formulas is instantiated at this structure: (y ∷ x ∷ []) ⊨ φ reads a formula φ of arity two at the environment that assigns y to the first free-variable slot and x to the second. The axiom schemas are each supplied as functions of their parameters, so every instance, for every formula, holds at once.

module Model = FOL.ZFModel 𝒮ᵥ
open Model using ( SetOf; _⊆ˢ_; setOf-unique; isZFModel; isZFCModel )

module SemanticsV = FOL.Semantics 𝒮ᵥ
open SemanticsV.At S id using ( _⊨_ )

The basic sets

The empty set, pairing, and union are the easiest fields to discharge, because the constructions and their classifications already exist in the hierarchy library. What remains is to change the shape of the statements. A specification for the model record is an equality of truth values, and indeed a path: for every carrier element x, the truth value x ∈ˢ b must be equal, as a path, to the class description Q x. The library states its axioms through the small membership ∈ₛ, so each conversion applies the same three moves: ∈∈ₛ trades small membership for ordinary membership pointwise, the library's classification supplies the corresponding bi-implication, and ⇔toPath rewrites that bi-implication into the required path. For pairing the correspondence is closest: the library's "equal to a or to b" is definitionally the field's (x ≈ˢ a) ⊔ (x ≈ˢ b), so only the layer of ∈∈ₛ is genuinely work.

The empty-set specification asks that, for every carrier element x, the truth value of x ∈ˢ ∅ be the path-equal image of the falsity ⊥. This is the chapter's basic conversion in miniature. What the library proves is that ∅ has no members in the small membership ∈ₛ, so the two membership notions must be exchanged pointwise first. Forward, ∈∈ₛ turns a proof of x ∈ˢ ∅ into the small membership that ∅-empty refutes, and from the contradiction the empty type is inhabited, which is exactly what the implication demands. Backward there is nothing to build, since no element of ⊥ can be supplied. ⇔toPath then converts the resulting bi-implication of propositions into the path of truth values the specification requires.

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))

Pairing asks that membership in ⁅ a , b ⁆ equal the disjunction of being equal to a and being equal to b, where the equalities are read as the structure's ≈ˢ. The library's pairing-ax states a bi-implication between the small membership x ∈ₛ ⁅ a , b ⁆ and the corresponding disjunction of small equality with a or b, and the propositional part of the statement already matches the target. Forward, one application of ∈∈ₛ converts the ordinary membership x ∈ˢ ⁅ a , b ⁆ into the small form that pairing-ax consumes, and its first direction returns the disjunction. Backward, the second direction of pairing-ax produces the small membership, and the other half of ∈∈ₛ lifts it back to ordinary membership. Each direction is a single application of the library result wrapped in one exchange of membership notation.

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)) ≡ (∃[ y ∶ S ] (y ∈ˢ a) ⊓ (x ∈ˢ y))
union-spec a x = ⇔toPath

Union is the first specification with an existential shape: membership in ⋃ a should equal the truncated statement that some y lies in a with x in y. Forward, union-ax yields such a truncated triple (v , v in a , x in v), but with both memberships in small form. The rewriting happens inside a propositional truncation with a propositional target, so PT.map transforms the witness in place: ∈∈ₛ turns v ∈ₛ a into an ordinary member of a, and x ∈ₛ v into an ordinary member of v. The outcome is a witness of the indexed disjunction ∃[ x ] P x, the direct hProp` mere-existence statement over the carrier, and no member is chosen.

  (λ 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

Backward runs the same exchange in reverse. From a truncated witness of the indexed disjunction, PT.map takes each case (v , v in a , x in v) and, using the other direction of ∈∈ₛ, rebuilds the small-form triple that union-ax consumes; its second direction then returns small membership in ⋃ a, which the remaining half of ∈∈ₛ lifts to ordinary membership. Together the two directions give the path of truth values the specification requires, both derived from the one library classification plus the pointwise exchange of membership notation.

    (λ { (v , va , xv) → v , ∈∈ₛ {a = v} {b = a} .fst va
                           , ∈∈ₛ {a = x} {b = v} .fst xv })
    h)))

The goal of this chapter is to realize each axiom of ZF inside the cumulative hierarchy, at one fixed universe level ℓ: the structure 𝒮ᵥ has a carrier S with truth-valued equality and membership, and a model record demands, for each axiom, a set whose membership is path-equal to the prescribed description. The assumptions are uneven, and it pays to separate them. The stock constructions, namely the empty set, pair, union, and infinity, and the whole replacement argument need no extra assumption at all. Full separation needs propositional resizing, so that the satisfaction of each formula becomes a small proposition pointwise. Power set needs a small classifier HPropSmallness, a small type equivalent to all of hProp ℓ. The packaged corollaries record the combined cost: V⊨ZF assumes exactly LEM (ℓ-suc ℓ), and V⊨ZFC assumes exactly SetChoice (ℓ-suc ℓ). This section stays on the assumption-free side. It develops the basic membership specifications for the union of a set and then for the union of an indexed family f : X → S. The set ⋃ (sett X f) collects the values of the family through an intermediate set, and it is worth reading membership in that union directly as membership in some family member. Unfolding union-spec gives a truncated existential over members v of the union, and since each such v is itself presented by an index of the sett, a second truncated layer sits on top. The two lemmas below compose the layers into one, in each direction.

The inward lemma turns one concrete membership x ∈ f i into membership in the whole union. The witness is written down rather than searched for: the intermediate element is f i itself, presented by the index i through the reflexive path, with h certifying that x lies in it. Since union-spec is an equality of truth values, subst ⟨_⟩ transports this witness across the reversed specification, so the truncated triple is consumed exactly in the shape the union characterization expects. Nothing enters beyond union-spec itself.

union-family-in : (X : Type ℓ) (f : X → S) (i : X) (x : S)
                → ⟨ x ∈ˢ f i ⟩ → ⟨ x ∈ˢ (⋃ (sett X f)) ⟩
union-family-in X f i x h = subst ⟨_⟩ (sym (union-spec (sett X f) x))
  ∣ f i , ∣ i , refl ∣₁ , h ∣₁

union-family-out : (X : Type ℓ) (f : X → S) (x : S)

The outward lemma recovers, from membership in the union, merely some family member containing x. Unfolding union-spec gives a truncated triple (v , v in the union , x in v); the second component says v is presented by an index, so a further PT.map inside the truncation extracts a pair (i , q) with f i ≡ v. The membership of x in v is then transported along the reverse of q to land in f i. The target keeps its truncation, so the eliminator is PT.rec into ∥ Σ[ i ] ⟨ x ∈ˢ f i ⟩ ∥₁ with squash₁ as the propositionhood evidence. The conclusion stays a mere existence: some family member contains x, and no member is chosen.

                 → ⟨ x ∈ˢ (⋃ (sett X f)) ⟩ → ∥ Σ[ i ∈ X ] ⟨ x ∈ˢ f i ⟩ ∥₁
union-family-out X f x h = PT.rec PT.squash₁
  (λ { (v , hv , hx) → PT.map
    (λ { (i , q) → i , subst (λ w → ⟨ x ∈ˢ w ⟩) (sym q) hx }) hv })
  (subst ⟨_⟩ (union-spec (sett X f) x) h)

Replacement without an additional axiom

Replacement is a schema, and in ordinary set theory it is a genuine axiom: for each set a and each formula φ functional on a, the existence of the image must be postulated. Here the hierarchy itself supplies a construction, and no choice principle is invoked. The functionality hypothesis is stated as contractibility: for every member x of a, the type of values y with (y ∷ x ∷ []) ⊨ φ is contractible, so a center value comes with proofs that every other value is identified with it. Because contractibility provides actual data, that center value can be read off and used to build the image. The members of a, however, are given only through their small presentation: each member appears as ⟪ a ⟫↪ m for some index m of the type ⟪ a ⟫. The construction therefore indexes the image by ⟪ a ⟫ itself, and the potentially delicate step, recovering an index from a membership fact, is a function rather than a choice, because the presentation fibers of ∈-asFiber are untruncated. What must be checked is that membership in the resulting set has exactly the truth value the schema demands. The forward direction only reads off the data the image provides; the backward direction recovers an index from an external membership and then uses the contraction of the functionality hypothesis once, to identify the externally given value with the value the construction chose at the recovered index.

One preliminary fact runs through everything below: if m is an index of the presentation of a, then the element ⟪ a ⟫↪ m it presents really is a member of a. The small membership ⟪ a ⟫↪ m ∈ₛ a holds by definition of the presentation, and ∈∈ₛ lifts it to the structural membership. The section then takes its data: a set a, a formula φ with two free-variable slots, and the functionality hypothesis fc, which asserts for each x ∈ a that the type of values y satisfying (y ∷ x ∷ []) ⊨ φ is contractible. Contractibility is data, a center together with a contraction, so the center value for each member of a is available for computation without any choice principle.

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 )
         (fc : (x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩)) where

The image is then a direct assembly: replaceImage is sett over the index type ⟪ a ⟫, sending each index m to the center value that fc provides for the member ⟪ a ⟫↪ m. Its specification says that membership in replaceImage equals the truth value obtained by disjoining (x ∈ a) ⊓ φ(y, x) over all x, which is the replacement schema in semantic form: y belongs to the image exactly when it arises as the value of φ at some member of a. As elsewhere in the chapter, ⇔toPath converts the two implications into the path of truth values the specification asks for.

  replaceImage : S
  replaceImage = sett ⟪ a ⟫ (λ m → fc (⟪ a ⟫↪ m) (memb a m) .fst .fst)

  replaceImage-spec : ∀ y → (y ∈ˢ replaceImage)
                    ≡ (∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ))
  replaceImage-spec y = ⇔toPath fwd bwd

The forward direction of the specification starts from a membership in the image. Because replaceImage is a sett indexed by the presentation type of a, such a membership carries an index m of ⟪ a ⟫ together with a path q from the presented element ⟪ a ⟫↪ m to y. The witness for the right-hand side is then assembled from this one index. First, the presented element is a member of a, by the preliminary fact memb. Second, fc provides the value at that member together with the proof that φ holds of it and that member; transporting that proof along q moves the second free-variable slot from the presented element to y. This direction uses none of the uniqueness content of fc: however the image presents y, some member of a is produced at which φ(y, x) holds.

    where
    fwd : ⟨ y ∈ˢ replaceImage ⟩ → ⟨ ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ) ⟩
    fwd = PT.map λ { (m , q) →
        ⟪ a ⟫↪ m , memb a m
      , subst (λ v → ⟨ (v ∷ ⟪ a ⟫↪ m ∷ []) ⊨ φ ⟩) q

The backward direction is where a choice principle would seem unavoidable. It receives a truncated witness (x , x∈a , hφ) and must produce an index into the image, an index that presents the very member x of a at which φ(y, x) holds. So the fact that x is a member must be turned into an index presenting it. The smallness chapter supplies exactly this: ∈-asFiber returns, as ordinary untruncated data, an actual pair mf of an index and a path from the presented element back to x. No choice among possible indices is made, because the recovery is a function. The satisfaction proof hφ is then transported along the reverse of the path mf .snd, moving the second free-variable slot from x to the presented element, which is the shape in which the hypothesis fc was stated.

              (fc (⟪ a ⟫↪ m) (memb a m) .fst .snd) }
    bwd : ⟨ ∃[ x ∶ S ] (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φ

The recovered index still has to become membership in the image, and this is the one place where uniqueness enters. At the index mf .fst, the functionality hypothesis says the type of suitable values is contractible, so the externally supplied pair (y , hφ') is compared with the chosen center: the contraction yields the center together with a path to it, and the first projection of that path identifies y with the value the construction assigned to the presented member, which is an index into replaceImage. Uniqueness is thus used exactly once, to recognize the externally given value y as one of the internally chosen image values. Combined with the presenting index mf .fst, this gives membership of y in the image.

      in mf .fst
       , cong fst (fc (⟪ a ⟫↪ (mf .fst)) (memb a (mf .fst)) .snd (y , hφ')) }

The numeral chain and ω

Strong infinity is the field the library supplies nearly complete. Its ω is a sett over Lift ℕ with the numerals # as the family, so membership in ω holds precisely when x is merely hit by some #. What the record demands, however, is phrased through the model's own numeral chain: zero must be empty, and each successor's members must be exactly the members of the predecessor together with the predecessor itself. The work is therefore to align two chains that step differently. The model's chain takes a ∪ ⁅ a , a ⁆ as its successor, the library's takes sucV a = a ∪ ⁅ a ⁆s. The pair ⁅ a , a ⁆ with a repeated entry and the singleton ⁅ a ⁆s have the same elements, and extensionality turns that into a path; with this one identification the two chains agree stage by stage, and ω's membership characterization becomes the record's strong infinity.

The identification ⁅ a , a ⁆ ≡ ⁅ a ⁆s is a path between sets, so extensionality reduces it to the two membership inclusions. The first inclusion says every element of the pair with a repeated entry is an element of the singleton. Its input is a membership in ⁅ a , a ⁆, and the pairing axiom unfolds such a membership into a truncated disjunction: the element equals a through the left entry of the pair or through the right one.

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 ⟩

Both disjuncts ask for the same thing, membership in ⁅ a ⁆s, so after the truncated disjunction is eliminated into the proposition x ≡ a, whose propositionhood follows from the hierarchy being an h-set, each branch supplies its path and the results agree by that very propositionhood. What is consumed here is the backward direction of the singleton's classification, running from the path x ≡ a to the small membership x ∈ₛ ⁅ a ⁆s; note that it is the opposite direction from the one the reverse inclusion will use.

  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 ⁆ ⟩

The reverse inclusion runs in the other direction: the classification's forward component turns the membership x ∈ₛ ⁅ a ⁆s into the path x ≡ a, and this path, injected as the left disjunct, is converted by the pairing axiom into membership in ⁅ a , a ⁆. With the two sets identified, the model's numeral chain is defined by recursion on ℕ: numeralV zero is the empty set, and numeralV (suc n) unions onto stage n a pair whose two entries are both that stage. After the identification this is exactly the von Neumann successor step n ∪ ⁅ n ⁆s, since a pair with equal entries and a singleton have the same members.

  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

That the two chains agree is proved by induction on ℕ. At zero both sides reduce to the empty set, so the path is refl. At the successor step, congruence under the same union-of-pair shape rewrites both sides, and inside the pair the identification pair-singleton is applied, which is the step where the extensionality result is consumed. With the chains aligned, the remaining task is to read ω's membership in the model's vocabulary. The statement ω-specV says that membership in ω equals the indexed disjunction "x is equal to some numeralV", the index ranging over Lift ℕ, whose elements are lifted natural numbers. The equality on the right is ≈ˢ, the extensional equality of sets of the structure, so the statement is about the set x, not about a chosen presentation.

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 ∈ˢ ω) ≡ (∃[ n ∶ Lift {ℓ-zero} {ℓ-suc ℓ} ℕ ] x ≈ˢ numeralV (lower n))

The proof converts the two descriptions of membership into a path with ⇔toPath. Forward, a witness (i , p) is a lifted index together with a path p from x to the library numeral # (lower i); composing p with the reverses of the alignment paths turns it into a path from x to numeralV (lower i). Backward, the same path algebra runs in the opposite direction: a path from x to numeralV is rewritten, via the alignment, into a path to the matching #. The lift and lower conversions only move the natural number across the Lift; the mathematical content of both directions is the alignment numeralV≡# and the path algebra around it.

ω-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)) }))

The record's two pinning equations speak of membership in a successor stage, so the chapter needs the case analysis for sucV itself: a member of sucV A is, merely, a member of A or equal to A, and both inclusions hold. This is what lets any numeral chain aligned with the library inherit the pinning equations, since the library numerals step by sucV. The analysis unfolds sucV A once through the union and pairing axioms; the second disjunct, membership in the singleton ⁅ A ⁆s, is closed by the singleton's classification.

The analysis starts from a piece of the previous section that is worth extracting: membership of x in the singleton ⁅ A ⁆s forces the path x ≡ A. This is the first half of the singleton's classification, recorded here as singl≡. The elimination principle ∈sucV-elim then turns the case analysis into a usable form: given a proposition P, a proof of P from membership in A, a proof of P from equality with A, and a member of sucV A, it produces a proof of P. That P is required to be a proposition is exactly what licenses eliminating the truncated case analysis into it.

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

Mathematically, sucV A is the union of the pair ⁅ A , ⁅ A ⁆s ⁆, so a member of it is a member of one of the two components. The analysis therefore runs in two steps. The union axiom first produces, merely, a component v of the pair with x a member of v; the pairing axiom then splits membership of v in the pair into the truncated disjunction v ≡ A or v ≡ ⁅ A ⁆s. In the left branch, transporting x ∈ v along v ≡ A gives ordinary membership in A, exactly what the first premise expects.

∈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))

In the right branch, transporting along v ≡ ⁅ A ⁆s yields membership in the singleton, and singl≡ converts that into the path x ≡ A, which is what the second premise expects. Both truncated eliminations land in the proposition P, so they are legitimate, and the two cases together discharge the analysis. The first inclusion is also recorded on its own: ∈sucV-inl states that a member of A is a member of sucV A.

         ; (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 ⟩

The proof of ∈sucV-inl builds rather than analyzes: from the assumed membership of x in A, it assembles a witness for membership in the union. Inside the truncation, the component A of the pair is presented through the pairing axiom via the left disjunct with the reflexive path, and the membership of x in A is converted into the small form the union axiom consumes. The outer exchange then lifts the whole small-form witness to membership in 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 ⟩

The companion self∈sucV proves the second inclusion: every set a is a member of its own successor. The witness is now the other component ⁅ a ⁆s of the pair, presented via the right disjunct; the fact that it contains a is the second half of the singleton classification applied to the reflexive path. Together the two lemmas give the content the pinning equations need: the members of sucV A are, merely, the members of A together with A itself.

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 two pinning equations, for any chain aligned with the library's. The record asks that the zeroth numeral have no members and that the members of each successor numeral be exactly the members of the predecessor together with the predecessor itself. Both statements are about membership in the given chain, while the case analysis of the previous section speaks of membership in sucV; the alignment q : a n ≡ # n is the bridge, and every statement about membership in the chain transports along q to the corresponding statement about the library numerals. The module takes the chain and the alignment as parameters, so the same lemmas serve the model's chain and any other.

The zero equation is the easier one. If z were a member of the chain's zeroth stage, transporting along q zero makes it a member of the library's empty set; after the exchange by ∈∈ₛ, ∅-empty refutes that membership in its small form, and the result is an inhabitant of the empty type. Note what is not claimed: no freestanding emptiness of the model's numeral is proved, only that membership in it implies a contradiction, which is all the pinning equation demands.

module NumPin (a : ℕ → S) (q : (n : ℕ) → a n ≡ # n) where
  pinZero : (z : S) → ⟨ z ∈ˢ a zero ⟩ → Empty.⊥
  pinZero z z∈ = ∅-empty z
    (∈∈ₛ {a = z} {b = ∅} .fst (subst (λ w → ⟨ z ∈ˢ w ⟩) (q zero) z∈))

  pinSuc : (n : ℕ) (z : S)

The successor equation is a pair of conversions between membership in a (suc n) and the truncated disjunction of membership in a n with equality to it, which is the shape the record's field prescribes. The equality in the second disjunct is ≈ˢ, the structure's equality, so the alignment paths apply to it directly. The propositionhood of the disjunction is supplied explicitly in the proof, since the eliminator of a truncated statement needs it.

         → (⟨ z ∈ˢ a (suc n) ⟩ → ⟨ (z ∈ˢ a n) ⊔ (z ≈ˢ a n) ⟩)
         × (⟨ (z ∈ˢ a n) ⊔ (z ≈ˢ a n) ⟩ → ⟨ z ∈ˢ a (suc n) ⟩)
  pinSuc n z = fwd , bwd
    where
    fwd : ⟨ z ∈ˢ a (suc n) ⟩ → ⟨ (z ∈ˢ a n) ⊔ (z ≈ˢ a n) ⟩

Forward, the membership in the chain is first transported to membership in # (suc n), and from there the sucV analysis applies, eliminating into the disjunction of the conclusion. In the first branch, membership in # n is transported back along the alignment at stage n to membership in a n, and the truncated disjunction is introduced with the left injection. In the second branch, the path from z to # n is composed with the reverse alignment to give a path from z to a n, taking the right injection. Both branches produce truncated witnesses, so the result remains a mere disjunction, never a decided case.

    fwd z∈ = ∈sucV-elim {A = # n} {x = z}
      (snd ((z ∈ˢ a n) ⊔ (z ≈ˢ a n)))
      (subst (λ w → ⟨ z ∈ˢ w ⟩) (q (suc n)) z∈)
      (λ z∈#n → ∣ Sum.inl (subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (q n)) z∈#n) ∣₁)
      (λ z≡#n → ∣ Sum.inr (z≡#n ∙ sym (q n)) ∣₁)

Backward has two truncated cases to handle, so the eliminator runs into the membership proposition of a (suc n). In the first case, the member of a n is transported to # n, the lemma ∈sucV-inl puts it into the library successor, and the result is transported back along the alignment at the successor stage. The alignment is used in both directions at every step, which is why it was taken as a hypothesis for all n at once.

    bwd : ⟨ (z ∈ˢ a n) ⊔ (z ≈ˢ a n) ⟩ → ⟨ z ∈ˢ a (suc n) ⟩
    bwd = PT.rec (snd (z ∈ˢ a (suc n)))
      (λ { (Sum.inl z∈n) → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (q (suc n)))
             (∈sucV-inl {A = # n} (subst (λ w → ⟨ z ∈ˢ w ⟩) (q n) z∈n))
         ; (Sum.inr z≡n) → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (q (suc n)))

The second case handles the right disjunct, and this is where the fact that a successor contains itself enters. The hypothesis is a path z ≡ a n from z to the model's predecessor; composing it with the alignment q n yields a path z ≡ # n. That path transports the stored fact self∈sucV (# n), that # n lies in its own library successor, into the statement that z lies in sucV (# n), and the final transport along the alignment at the successor stage returns to the chain. Together the two branches deliver the full backward conversion, completing the successor pinning equation for every aligned chain.

             (subst (λ w → ⟨ w ∈ˢ sucV (# n) ⟩) (sym (z≡n ∙ q n))
               (self∈sucV (# n))) })

Assumptions for the remaining axioms

Two fields remain, full separation and power set, and they pose two different smallness problems. Full separation must turn an arbitrary satisfaction proposition (y ∷ []) ⊨ φ, which lives in Type (ℓ-suc ℓ), into a small one, and no Δ₀ witness is available to do this by hand; what is needed is the resizing component of impredicativity, which produces a small representative for each such proposition pointwise, so that the smallness adapter separateFromSmall applies. Power set poses the other problem: a candidate subset of a is a family of membership propositions indexed by ⟪ a ⟫, and to form a set from it, each proposition must be encoded in one fixed small type. The hPropSmallness component supplies exactly this: a small type Ω' equivalent to all of hProp ℓ, serving as a classifier for propositions. Neither construction uses the whole Impredicativity packing; each consumes one of its two components, and the later assembly takes the packing as a parameter, deriving it in the classical case through lem→impredicativity.

Power set

The power set is the one construction the library's own header disclaims, and the small classifier is what builds it. A candidate subset of a is described by a characteristic function ⟪ a ⟫ → Ω' into the classifier's small carrier; decoding each value χ m yields a proposition on the index m, and the elements presented by indices where that proposition holds are gathered into a set by sett. The proof establishes two inclusions: everything the function selects lies in the given subset, and every member of the subset is selected, the second direction using the round trip decode after encode on propositions, together with extensionality.

The power-set construction assumes exactly one component of the packing: a witness sΩ of HPropSmallness ℓ, that is, a small type Ω' in Type ℓ together with an equivalence onto hProp ℓ. Nothing else is assumed. From the equivalence two readings are extracted. The forward map decode turns a small truth value into an ordinary proposition packaged in hProp ℓ; this is the direction that lets a characteristic function be read as a predicate on indices.

module Power (sΩ : HPropSmallness ℓ) where

  private
    decode : sΩ .fst → hProp ℓ
    decode = equivFun (sΩ .snd)

    encode : hProp ℓ → sΩ .fst

The backward map encode sends an hProp ℓ proposition into the small carrier, and the round trip decode∘encode is the secEq leg of the equivalence: decoding the encoding of a proposition returns a path to exactly that proposition. With the classifier in place, the realizing family F is direct. For a characteristic function χ, take the pairs of an index m with a proof that decode (χ m) holds, and form the sett of the elements they present. The selected members are exactly those whose encoded truth value decodes to a proposition with a proof.

    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))

The power set operation is itself a sett: the index type is the function type from ⟪ a ⟫ into the small carrier Ω', and the family realizes each characteristic function as the set selected above. Membership in 𝒫V a is therefore, merely, membership in one of the realized sets: a member arrives as a truncated pair of a characteristic function and a path from the set it selects to x. The forward direction of the specification shows that such an x is a subset of a in the ambient sense, the inclusion ⊆ of the hierarchy library rather than the structure's relation ⊆ˢ; the passage between the two is kept separate and handled at the end.

  𝒫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 →

The proof of x ⊆ a proceeds member by member, first eliminating the truncated membership in the power set. After transporting the membership of y in x back along the presenting path, it becomes small membership in the selected set F a χ; converting that through ∈∈ₛ yields a presenting fiber, an index m together with a proof that decode (χ m) holds and a path identifying y with the presented element ⟪ a ⟫↪ m.

      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 ⟩

The remaining work is to turn that fiber into membership of y in a, which the transport along the path accomplishes, since the presented elements of a are members of a by construction. The target stays proposition-valued throughout, so both truncation eliminations are legitimate. Thus any member of the power set, however it is presented, collects only members of a.

Backward builds the witness for membership in the power set, and it needs no choice. The characteristic function χₓ is recovered explicitly: the index m is sent to the encoding encode of the small membership of the presented element ⟪ a ⟫↪ m in x, a function because the small membership fiber of the embedding is untruncated. The truncated pair then packages χₓ with the assertion, proved by extensionality from the two inclusions s1 and s2, that the set χₓ selects equals x.

    bwd a x sub = ∣ χₓ , extensionality (F a χₓ) x (s1 , s2) ∣₁
      where
      χₓ : ⟪ a ⟫ → sΩ .fst
      χₓ m = encode (⟪ a ⟫↪ m ∈ₛ x)
      s1 : ⟨ F a χₓ ⊆ x ⟩

The first inclusion shows that the set selected by χₓ adds nothing beyond x. A small member of F a χₓ carries an index m, a proof that decode (χₓ m) holds, and a presenting path. Since χₓ m was defined as the encoding of the membership ⟪ a ⟫↪ m ∈ₛ x, the round trip decode∘encode rewrites the decoded proof back into exactly that membership, and the presenting path transports it onto y. So every member of the selected set is a member of 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)

The second inclusion must go the other way: from an arbitrary member y of x, produce a small member of F a χₓ. The inclusion hypothesis sub first gives a presenting fiber for y in a, and its second component certifies that the presented element and y have the same members. The embedding's presentation is used in both directions here, so nothing needs to be chosen: the fiber is untruncated data, and the path q extracting ⟪ a ⟫↪ m₀ ≡ y will be available as an ordinary term.

      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

The path q is obtained by applying identityPrinciple to the equal-members data of the inclusion hypothesis, so the presented element ⟪ a ⟫↪ m₀ equals y. Transporting the membership of y in x backwards along q lands it at the presented element, and that is precisely the proposition that decode (χₓ m₀) decodes to, by the round trip again: χₓ m₀ was defined as the encoding of exactly this membership. So the pair (m₀ , h) of the index with the transported proof inhabits the type defining F a χₓ, and it witnesses y in the selected set. With both inclusions in place, power-spec composes this equivalence with the pointwise exchange between the ambient inclusion ⊆ and the structure's subset relation ⊆ˢ, giving the field hasPower a set whose membership is, as truth values, the subset relation the record states.

        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)

The specification power-spec composes two equalities of truth values. The first is the equivalence just proved: membership in 𝒫V a equals the ambient inclusion x ⊆ a, which quantifies over actual members and is not truncated. The second converts the ambient inclusion into the structure's own subset relation x ⊆ˢ a, stated through the structure's membership ∈ˢ: given a function sending each ordinary member of x to an ordinary member of a, the two directions of ∈∈ₛ exchange the membership notations pointwise in both directions. The composite is the power-set field's data: a set 𝒫V a whose membership, as a truth value, is exactly the subset relation the record states. Note where each smallness input entered: separation consumed resizing pointwise, while the power set was built from hPropSmallness alone.

  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)))

Establishing V ⊨ ZF

Every field of the model record now has its witness, and this section assembles them into a single mathematical theorem: the cumulative hierarchy satisfies ZF. The axioms group by how they were obtained. Empty set, pairing, and union are the stock sets converted at the start of the chapter. Full separation and power set are the two smallness results, each consuming one component of the impredicativity packing: separation uses resizing to make each satisfaction proposition small so that separateFromSmall applies, and power set uses the small classifier alone. Replacement is the image built from untruncated fibers, and infinity is the library's ω together with the numeral alignment. What remains is a packaging step with one genuine mathematical input. A field of isZFModel asks for isContr (SetOf Q): a realizing set together with a contraction of all realizers to it, and extensionality supplies exactly that contraction, via setOf-unique. The theorem V⊨ZF-impredicative assumes the packing Impredicativity ℓ; the theorem V⊨ZF assumes instead LEM (ℓ-suc ℓ) and derives the packing through lem→impredicativity.

The assembly takes the packing Impredicativity ℓ as a parameter, and its two fields feed the two smallness constructions separately: hPropSmallness goes to the power-set construction of the previous section, which uses the classifier alone, and resizing is what separation uses. Full separation is stated directly: given a set a and a formula φ with one free-variable slot, produce a set s such that, for every y, the truth value y ∈ˢ s is the path equal to the conjunction of y ∈ˢ a and the satisfaction of φ at the one-point environment y ∷ []. This is precisely the shape of the separation specification the model record demands.

module VModel (imp : Impredicativity ℓ) where
  open Impredicativity imp
  open Power hPropSmallness public

  separateFull : (a : S) (φ : Formula S )
               → Σ[ s ∈ S ] (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ ((y ∷ []) ⊨ φ)))

Separation is one application of the adapter from the smallness chapter. separateFromSmall takes a predicate P : S → hProp (ℓ-suc ℓ) on a, a smallness witness for each value, and returns a set s with the path specification y ∈ˢ s ≡ (y ∈ˢ a) ⊓ P y. Here the predicate is λ y → (y ∷ []) ⊨ φ, the satisfaction of φ at each one-point environment, and its smallness at each point is resizing applied there. No hypothesis on the shape of φ is needed: resizing assigns a small representative to every satisfaction proposition, whatever formula produces it. With separateFull in hand, the theorem V⊨ZF-impredicative of type isZFModel can be assembled from the witnesses already proved.

  separateFull a φ =
    separateFromSmall a (λ y → (y ∷ []) ⊨ φ) (λ y → resizing ((y ∷ []) ⊨ φ))

  V⊨ZF-impredicative : isZFModel
  V⊨ZF-impredicative = record
    { extensional    = extensionalV

The first group of entries reuses the chapter's opening conversions. For the empty set, the pair, and the union, the explicit realizer is the library set ∅, ⁅ a , b ⁆, or ⋃ a, together with the specification proved there; the entries extensional and regularity quote the witnesses proved in the hierarchy chapter. Separation's realizer is separateFull a φ, the pair of the separated set and its specification, already in the shape the field asks for. Each field is a function of its parameters, so every instance of the schema, for every formula, is supplied at once.

    ; 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 φ)

The next two entries consume the middle constructions. The replacement field receives the functionality hypothesis fc and takes as realizer the image replaceImage with its specification; the power-set field takes 𝒫V a with power-spec, the construction built from the small classifier alone. The numeral chain then occupies three entries: the operation numeralV itself, and the two pinning equations, numeral-zero saying that nothing inhabits numeralV zero, and numeral-suc giving the member-or-predecessor dichotomy for numeralV (suc n). Both equations come from the NumPin lemmas applied to the alignment numeralV≡#, so they carry exactly the content of that alignment plus the sucV case analysis.

    ; hasReplacement = λ a φ fc → one _ (replaceImage a φ fc , replaceImage-spec a φ fc)
    ; hasPower       = λ a → one _ (𝒫V a , power-spec a)
    ; numeral        = numeralV
    ; numeral-zero   = NumPin.pinZero numeralV numeralV≡#
    ; numeral-suc    = NumPin.pinSuc numeralV numeralV≡#

The last field is strong infinity, realized by ω with its specification: every member of ω is merely a model numeral, which is what the record demands. The auxiliary one records the general principle that closes every existence field. For any class Q : S → hProp (ℓ-suc ℓ), an element of SetOf Q, that is a realizing set with its specification, already determines an element of isContr (SetOf Q), because setOf-unique applied to extensionality contracts all realizers to the given one. So every explicit realizer above becomes the contractibility data its field requires, and extensionality is quoted once in one rather than repeated in each entry.

    ; hasInfinity    = one _ (ω , ω-specV) }
    where
    one : (Q : S → hProp (ℓ-suc ℓ)) → SetOf Q → isContr (SetOf Q)
    one = setOf-unique extensionalV

The theorem V⊨ZF-impredicative states that the cumulative hierarchy satisfies ZF under the single hypothesis Impredicativity ℓ. Both schema fields are functions that accept every formula, so separation and replacement hold for all formulas at once, through the deep embedding of the object language in the first-order logic chapters. The second theorem replaces the packing with the standard classical assumption: V⊨ZF takes LEM (ℓ-suc ℓ) and derives the packing from it. What is proved is a model construction under the stated hypothesis, not an unconditional consistency claim.

The definition of V⊨ZF is one composition: the excluded middle instance is converted into the packing by lem→impredicativity, and the result is fed to VModel.V⊨ZF-impredicative. In that conversion, from the classical chapter, the resizing field uses lem at its own level, while the classifier field first lowers the instance one successor step with lowerLEM and then builds the equivalence presenting hProp ℓ by Lift Bool. One assumption at the successor level therefore reaches both fields the model consumes: separation through resizing, power set through the classifier.

V⊨ZF : LEM (ℓ-suc ℓ) → isZFModel
V⊨ZF lem = VModel.V⊨ZF-impredicative (lem→impredicativity lem)

Choice as a separate assumption

Excluded middle does not yield choice, so the last axiom of ZFC is taken as a separate assumption and the choice-set axiom is proved from it. The interface is SetChoice: for an h-set X : Type ℓ and a family B : X → Type ℓ each of whose fibers is merely inhabited, there is a choice function on the whole of X, given as a truncated inhabitant. The lemma below assumes a level-ℓ instance of this interface together with an isZFModel for the fixed hierarchy structure 𝒮ᵥ, from which it uses the intersection ∩ and its specification. The family whose choice is taken is a small presentation: the index type is ⟪ a ⟫, an h-set, and the fiber over an index m is the set ⟪ ⟪ a ⟫↪ m ⟫ presented by m. So choice selects presentation indices, not elements of sets. From the chosen indices a set c is formed by one application of sett; the pairwise disjointness hypothesis disj then shows, through the model's intersection, that c meets each member of a in a contractible, hence unique, set of points. The truncation is asymmetric by design: the choice set itself is merely existential, while each intersection carries explicit isContr data. The final theorem consumes one instance of SetChoice (ℓ-suc ℓ) twice: choice→lem converts it into LEM (ℓ-suc ℓ) for the ZF part, and lowerSetChoice lowers it to SetChoice ℓ for the choice lemma. So V⊨ZFC is proved from choice alone; excluded middle is recovered from choice by Diaconescu's theorem, not the other way round.

Two preliminary facts feed the choice-set construction. The first concerns the index type at which choice will be applied. Each presentation type ⟪ a ⟫ is an h-set: it embeds into the hierarchy through ⟪ a ⟫↪, whose embedding property isEmb⟪ a ⟫↪ was recorded when the presentation was introduced, and the hierarchy itself is an h-set by setIsSet. A general cubical result, Embedding-into-isSet→isSet, transfers the h-set condition back along an embedding, so isSet⟪ a ⟫ holds for every set a. Equality types between indices are therefore propositions, which is precisely the condition SetChoice places on the type it chooses from.

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)

The second fact turns a uniqueness argument into contractibility data. For a class P on the carrier, suppose a centre z₀ with a realization p₀, together with a contraction sending every realizing z to a path z₀ ≡ z. Then the type of pairs of a set and a realization of P is contractible, with centre (z₀ , p₀). The contraction between pairs is built with Σ≡Prop: it suffices to give the path between first components, because each P v is a proposition and so fixes the second component. The choice-set conclusion has exactly this shape: one meeting point, unique in the isContr sense. The lemma then takes its hypotheses. It assumes an arbitrary isZFModel for the fixed structure 𝒮ᵥ, from which it uses only the model's intersection ∩ and its specification ∩-spec, together with an instance of SetChoice ℓ.

                      → 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 )

The lemma choice states the classical choice-set situation. Its hypotheses: inh says each member x of a is merely inhabited, so the family consists of nonempty sets; disj says that two members of a sharing any element, even merely, are already equal, so the family is pairwise disjoint. The conclusion is a merely existing set c such that for each member x of a the type of points meeting c ∩ x is contractible. The truncation is asymmetric: the choice set itself is not given as data, only its truncation is inhabited, while the uniqueness of each meeting point is explicit isContr data.

  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 ⟩

The proof applies the choice instance at the small presentation of the family, not at the family itself. The index type is ⟪ a ⟫, an h-set by the first preliminary fact; the family is λ m → ⟪ ⟪ a ⟫↪ m ⟫, the set presented by each index. What remains is to show each fiber merely inhabited, which is the role of pick: for each index m, a member of the presented set ⟪ a ⟫↪ m merely exists by inh at the member that memb a m certifies, and ∈-asFiber extracts from that membership an actual index into the presentation of ⟪ a ⟫↪ m. The truncation on the input is preserved throughout, so pick never claims to choose a point inside a member of a; it only re-indexes the mere existence.

              → 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

The choice function then returns, for each index m, an actual element g m of the presented set: choice on the h-set of indices yields untruncated data, an element of the presentation of ⟪ a ⟫↪ m. The remainder mk packages this into the conclusion: a set c together with, for each member x of a, contractibility data for the type of points meeting c ∩ x. Because the choice function already produced untruncated data at the index level, mk is an ordinary function; the truncation reappears only when the whole package is wrapped by PT.map. This is exactly why the choice set itself is merely existential while each intersection carries explicit isContr data.

        (λ { (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) ⟩))

Inside mk, the chosen data is interpreted. The function g m returns an index into the presentation of ⟪ a ⟫↪ m, so composing with that presentation yields an actual set chosen m, a member of the member indexed by m. The choice set is then c = sett ⟪ a ⟫ chosen: the sets picked for each index, gathered by one application of the hierarchy's set former.

      mk g = c , uniq
        where
        chosen : ⟪ a ⟫ → S
        chosen m = ⟪ ⟪ a ⟫↪ m ⟫↪ (g m)
        c : S

One fact about c is recorded before uniqueness: each chosen set really is a member of the member it came from. This follows from the presentation: an index g m into the presentation of a set is, by ∈ₛ⟪ ⟫↪, a small membership, and ∈∈ₛ lifts it to the structural membership ⟨ chosen m ∈ˢ ⟪ a ⟫↪ m ⟩. With the uniqueness helper of the second preliminary fact available, uniq becomes a three-part argument: a centre, a proof that the centre lies in the intersection, and a contraction of every other meeting point to the centre.

        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

The centre is computed as follows. The member x of a has an untruncated presenting fiber: ∈-asFiber gives an index m₀ together with a path mf .snd presenting x. The meeting point is the set chosen at that index, z₀ = chosen m₀. This is where the untruncated fibers pay off again: recovering the index from membership is a function, not a choice, so the centre is well defined without any appeal to the choice instance.

          where
          mf = ∈-asFiber {a = x} {b = a} x∈a
          m₀ = mf .fst
          z₀ = chosen m₀
          pf₀ : ⟨ z₀ ∈ˢ (c ∩ x) ⟩

The centre must lie in the intersection c ∩ x. By the model's ∩-spec, membership in an intersection is a truth value equal to the conjunction of membership in c and in x, and the proof transports along the symmetrized specification. Membership in c merely witnesses that z₀ was chosen at index m₀, with the reflexive path, and m₀ presents x; membership in x follows by transporting chosen∈ m₀ along that presenting path. The two halves are conjoined as a truncated pair. The remaining duty is the contraction uniqz, which must send every z meeting c ∩ x to a path z₀ ≡ z.

          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)

The contraction is the delicate half. Take any z meeting c ∩ x; membership in the intersection transports through ∩-spec into the truncated conjunction zcx. The first component says, merely, that z lies in some chosen set: an index m together with a path q from z to chosen m as members of c. Since chosen m is a member of ⟪ a ⟫↪ m by chosen∈, transporting along q shows z is a member of that member too. So z is a shared element of the members x and ⟪ a ⟫↪ m of a, and disjointness applies: disj yields the path x ≡ ⟪ a ⟫↪ m. The two members present the same set, so their presenting indices agree: the presentation is an embedding, hence injective on indices, and isEmbedding→Inj applied to the composed paths gives m ≡ m₀. Therefore chosen m ≡ chosen m₀ = z₀, and composing with q yields the contraction path z₀ ≡ z. The target is a path between elements of an h-set, hence a proposition, which licenses eliminating the truncation here.

The accounting of the chapter's final theorem is exact. One instance of SetChoice (ℓ-suc ℓ) is used twice: choice→lem converts it into LEM (ℓ-suc ℓ), which drives the ZF part through V⊨ZF, and lowerSetChoice lowers the same instance to SetChoice ℓ, which feeds ChoiceLemma for the choice-set part. The choice set exists merely, while each intersection is uniquely determined by explicit contractibility data.

              (λ { (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)

Disjointness is applied to the two members x and ⟪ a ⟫↪ m of a, with the shared element z as the witness of their overlap; the hypothesis disj returns the path x ≡ ⟪ a ⟫↪ m. The two indices therefore present the same member, and the presentation ⟪ a ⟫↪ is an embedding, hence injective on indices: isEmbedding→Inj, applied to the composition sym x≡m ∙ sym (mf .snd), yields m ≡ m₀. Applying chosen to that path and composing with q produces z₀ ≡ z, the path the contraction requires. The target z₀ ≡ z is a path between elements of the h-set V, hence a proposition, which licenses eliminating the truncation of the case analysis here.

                            ∣ 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 })

The conjunction zcx is produced by transporting pf along the path ∩-spec c x z, which rewrites membership in c ∩ x as a plain pair of the two membership propositions. Its components are then used separately: the first feeds the disjointness witness of the previous step, and the second enters the transport z∈m of the membership of z. With the centre and the contraction in place, uniq supplies the isContr data for each member x of a, and mk returns the set c together with those data. The choice set itself exists only merely, as an inhabitant of a propositional truncation; the uniqueness of each intersection, by contrast, is explicit, untruncated isContr data.

              (zcx .fst)
            where
            zcx : ⟨ z ∈ˢ c ⟩ × ⟨ z ∈ˢ x ⟩
            zcx = subst ⟨_⟩ (∩-spec c x z) pf

V ⊨ ZFC, on choice alone

The lemma of the previous section and the ZF theorem meet here. The construction ChoiceLemma.choice is proved for the fixed hierarchy structure under two stated hypotheses: an arbitrary isZFModel for that structure, and an instance of SetChoice ℓ. Its index type is the small presentation ⟪ a ⟫, an h-set, so choice selects presentation indices of the family; disjointness then proves each intersection contractible. The choice set therefore exists merely, while each meeting point is unique as explicit isContr data. The theorem V⊨ZFC states the exact combined cost: SetChoice (ℓ-suc ℓ) yields LEM (ℓ-suc ℓ) for the ZF part via choice→lem, and the same instance, lowered by lowerSetChoice to SetChoice ℓ, drives the choice-set lemma. What is proved is a model construction under the stated hypothesis, not an unconditional proof.

The theorem's hypothesis is a single instance, SetChoice (ℓ-suc ℓ): set-level choice at the successor of the model's truth level. The conclusion isZFCModel packages a ZF model together with an internal choice-set witness, so the proof supplies both components. The ZF part is named base, since the choice-set lemma takes a ZF model as an input.

V⊨ZFC : SetChoice (ℓ-suc ℓ) → isZFCModel
V⊨ZFC ac = record
  { zf = base ; hasChoice = ChoiceLemma.choice base (lowerSetChoice ac) }
  where
  base : isZFModel

The single instance is used for two conclusions. choice→lem converts it into excluded middle at level ℓ-suc ℓ, which is exactly the hypothesis V⊨ZF expects; this gives base. For the choice-set part, lowerSetChoice lowers the same instance to SetChoice ℓ, which is what ChoiceLemma.choice requires, and the lemma is applied to base. Thus one instance of choice at the successor level yields the ZF model through excluded middle, and its one-level lowering yields the choice-set axiom.

  base = V⊨ZF (choice→lem ac)

Recap

The chapter's accounting is now complete. Empty set, pair, and union were converted from existing constructions by ∈∈ₛ and ⇔toPath; replacement follows directly through sett over untruncated fibers; strong infinity is ω's definition plus one chain alignment (numeralV≡#). The two remaining fields, full separation and power set, need exactly the Impredicativity packing of Base.Impredicativity: assembly gives V⊨ZF-impredicative at that exact cost, and excluded middle upgrades it to the headline V⊨ZF. One further, independent instance of set-level choice supplies the final theorem: SetChoice (ℓ-suc ℓ) yields LEM (ℓ-suc ℓ) for the ZF part and, lowered one level to SetChoice ℓ, drives the choice-set lemma, giving V⊨ZFC. The universe that the constructible-universe chapters will examine from within now exists.