---
title: "The cumulative hierarchy models ZF and ZFC"
module: V.Model
lang: en
site: "Bedrock"
description: "The cumulative hierarchy models ZF and ZFC"
stage: "The ambient hierarchy"
reading_order: 22
canonical: https://bedrock.institute/en/V.Model.html
html: V.Model.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/Model.lagda.md
prerequisites: [Base.Prelude, Base.Impredicativity, Base.Classical, Base.Choice, FOL.ZFStructure, FOL.Syntax, FOL.Semantics, FOL.ZFModel, V.Hierarchy, V.Smallness]
routes: [ambient-model]
translations: [https://bedrock.institute/zh/V.Model.md, https://bedrock.institute/ja/V.Model.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

```agda
{-# 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.

```agda
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.

```agda
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.

```agda
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.

```agda
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 `_∪_`.

```agda
  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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
  (λ 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.

```agda
    (λ { (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.

```agda
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.

```agda
                 → ⟨ 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.

```agda
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
```

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.

```agda
  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.

```agda
    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.

```agda
              (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.

```agda
      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.

```agda
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.

```agda
  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.

```agda
  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.

```agda
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.

```agda
ω-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.

```agda
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.

```agda
∈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`.

```agda
         ; (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`.

```agda
∈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.

```agda
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.

```agda
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.

```agda
         → (⟨ 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.

```agda
    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.

```agda
    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.

```agda
             (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.

```agda
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.

```agda
    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.

```agda
  𝒫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`.

```agda
      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`.

```agda
    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`.

```agda
      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.

```agda
      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.

```agda
        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.

```agda
  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.

```agda
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 ∷ []) ⊨ φ)))
```

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.

```agda
  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.

```agda
    ; 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.

```agda
    ; 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.

```agda
    ; 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.

```agda
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.

```agda
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 ℓ`.

```agda
                      → 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.

```agda
  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.

```agda
              → 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.

```agda
        (λ { (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.

```agda
      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.

```agda
        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.

```agda
          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`.

```agda
          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.

```agda
              (λ { (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.

```agda
                            ∣ 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.

```agda
              (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.

```agda
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.

```agda
  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.