BedrockThe basic axioms
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapHow does a set-producing operation lift into the constructible universe? A set belongs to L when it can be presented as a definable subset of an ordinal stage Lset σ. The chapter repeatedly finds one ordinal stage containing the needed inputs, writes a formula over that stage whose extension is the desired set, and proves the extensional equation in the surrounding hierarchy.
The closure lemma defSet→isL completes this pattern. Given an ordinal σ and the mere existence of a unary formula whose extension is x, 𝒟ₒ-intro recognizes x as a definable subset of Lset σ, and 𝒟ₒ→isL places it in L. The identity Lset (sucV σ) ≡ 𝒟ₒ (Lset σ) explains the stage calculation: the next stage consists exactly of the definable subsets of the present one. The packaged sets LsetS and 𝒟ₒS provide these two sets as elements of the carrier S.
This method constructs the empty set, unordered pairs, and unions inside L. Extensionality follows by using transitivity to extend agreement from constructible members to all surrounding members; regularity instead restricts the hierarchy's accessibility proof recursively. When two inputs need a common stage, bound2 supplies a common strict upper bound without comparing their original stages.
The setting fixes one universe level ℓ and works in the cumulative hierarchy V at that level. Everything in this chapter is constructive: no excluded middle, no resizing, no choice. The carrier on which the axioms will be proved is the type of sets of V together with a constructibility certificate isL, and every claim below is established from the ambient hierarchy alone.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module L.Axioms.Basic {ℓ : Level} where open import FOL.Syntax using ( Formula; var; con; _≐_; _∈̇_; _∨̇_; ⊤̇; ⊥̇; ∃̇∈ )
The defining step of the closure pattern is expressed in a first-order language. Its formulas sit over a structure's small index type, with equality and membership as the atomic predicates, and with disjunction and bounded existential quantification available; these are the operations used to form definable subsets. Two ambient facts about passing from a structure to a substructure will matter: a path between two elements of a restriction is already a path between their underlying sets, and that is the direction the inherited axioms will exploit.
open import FOL.ZFStructure using ( ↾-reflects; module hPropStructure ) import FOL.ZFModel open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV ) open import V.Model {ℓ} using ( empty-spec; pair-spec; union-spec; self∈sucV; ∈sucV-elim
Each construction to be lifted already satisfies its membership law in the ambient hierarchy: the empty set has no members, every member of an unordered pair is one of its two entries, and union has its exact two-way classification. These ambient laws, proved once in the hierarchy, serve as the standards against which the formulas carved below are checked by extensionality; they are inherited, not re-derived. Two further ambient facts enter the computations: membership in the successor sucV σ splits into members of σ and σ itself, and the singleton is identified with the pair ⁅ x , x ⁆. The Kuratowski code pr of an ordered pair will have its stage placement computed from unordered pairs.
; pair-singleton ) open import V.Coding {ℓ} using ( pr ) open import L.Definability {ℓ} using ( module DefOf ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-layer
On the constructible side, Lset indexes stages by sets, IsOrd records which indices are ordinals, and isL is the class of constructible sets, transitive by isL-trans. The definable powerset of a stage is 𝒟ₒ; 𝒟ₒ-intro recognizes a definable subset from a formula and an extensional equation, and Lset-in, Lset-out, Lset⊆𝒟ₒ, Lset-mono and Lset→isL let membership in a stage be converted, carried upward along a larger stage, and read as a constructibility certificate. Stage transitivity is layer-trans.
; layer-trans; 𝒟ₒ; 𝒟ₒ-intro; Lset-in; Lset-out; Lset⊆𝒟ₒ ; Lset-mono; Lset→isL ) open import L.Ordinal {ℓ} using ( ∅-ord; suc-ord; bound2 ) open import Cubical.Data.FinData using ( zero; suc ) open import Cubical.Data.Sum using ( inl; inr )
Three ordinal facts control the stages: the empty set is an ordinal, the successor of an ordinal is an ordinal, and bound2 returns an ordinal strictly containing each of two given ordinals. Pairing uses the last result to place two constructible arguments in one common stage without comparing their original stages or choosing a maximum. Finite index types then describe finite images inside that stage, while binary sums express the disjunctions that define them.
open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.Foundations.Prelude using ( isPropIsContr ) open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded ) import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT
Membership in the ambient hierarchy is proposition-valued, but the presentation embedding has propositional fibers. Consequently ∈-asFiber converts a given membership proof into an actual index of the small presentation together with a path back to the member. Thus from ⟨ x ∈ Lset σ ⟩ one obtains m : ⟪ Lset σ ⟫ with ⟪ Lset σ ⟫↪ m ≡ x, allowing the formula to name that member by a constant. The output is data because the corresponding fiber is itself a proposition; there is no additional outer truncation to eliminate at this step.
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; sett ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( _∈ₛ_; ∈∈ₛ; ∈-asFiber; extensionality; _⊆_; ⟪_⟫; ⟪_⟫↪ ) open import Cubical.HITs.CumulativeHierarchy.Constructions
The ambient sets this chapter needs come with their exact membership characterizations: ∅-empty for the empty set, pairing-ax for the unordered pair ⁅_,_⁆ and its singleton variant, and union-ax and ⋃_ for the union. These are the hierarchy's own classification results, and they supply both directions of each membership law, so the definable subsets carved below can be checked against them by extensionality. The successor operation sucV supplies the next stage's index.
using ( ∅; ∅-empty; ⁅_,_⁆; ⁅_⁆s; pairing-ax; ⋃_; union-ax ; module InfinitySet ) open InfinitySet using ( sucV ) open hPropStructure 𝒮ʟ
The semantic side is fixed once. Truth values are the propositions at level ℓ-suc ℓ, so a formula's interpretation lands in an ordinary type former, and reading the restricted structure through the proposition-valued semantics gives the structural membership ∈ˢ and the bracket notation ⟨_⟩ for the type underlying a proposition. A realizing set is then an element of the carrier S, a set with its constructibility certificate, together with the equation stating which specification its membership realizes; this is the type SetOf Q. The principle setOf-unique, which turns one realizing set into contractibility data, is what reduces every remaining axiom field in this chapter to a bare existence problem.
module ModelL = FOL.ZFModel 𝒮ʟ open ModelL using ( SetOf; setOf-unique )
Definable subsets are constructible
The stage Lset (sucV σ) is a union indexed by δ ∈ sucV σ. Since σ ∈ sucV σ, the set 𝒟ₒ (Lset σ) is one of the sets being unioned. Therefore every element of 𝒟ₒ (Lset σ) belongs to Lset (sucV σ). When σ is ordinal, so is its successor, and this stage membership yields an isL certificate.
The lemma 𝒟ₒ→isL takes an ordinal σ with its ordinality certificate oσ, a set x, and a proof that x belongs to the definable power set of the stage at σ; it concludes that x is constructible. The proof places x one level up. Because σ is a member of its own successor sucV σ, the inclusion Lset-in carries membership in 𝒟ₒ (Lset σ) into membership in the stage Lset (sucV σ), whose index is an ordinal by suc-ord oσ. One application of Lset→isL then converts that stage membership into the certificate isL x. The truncated hypothesis is used as given: it is passed straight into Lset-in, whose conclusion is truncated in the same way, so no witness of constructibility is ever extracted or chosen.
𝒟ₒ→isL : (σ : V ℓ) → IsOrd σ → (x : V ℓ) → ⟨ x ∈ 𝒟ₒ (Lset σ) ⟩ → ⟨ isL x ⟩ 𝒟ₒ→isL σ oσ x x∈𝒟ₒσ = Lset→isL (sucV σ) (suc-ord oσ) x (Lset-in (sucV σ) σ x (self∈sucV σ) x∈𝒟ₒσ)
Composing the closure lemma with the recognition principle for the operator gives the form every construction in this chapter uses: to put a set in L, exhibit an ordinal stage, a formula, and an extensional equation saying that the formula defines exactly that set. The exhibit is merely existential, a truncated pair of a formula and an equation, and that is already enough. The empty set, pairing, and union below are its first three instances.
The hypothesis of defSet→isL is a truncated existential: merely some formula φ of arity one over the stage's members satisfies defSet (Lset σ) φ ≡ x. The recognition principle 𝒟ₒ-intro turns exactly such data into membership of x in 𝒟ₒ (Lset σ). That membership is a proposition, so eliminating the truncation into it is legitimate and no formula is ever chosen; the one-line composition with 𝒟ₒ→isL then delivers isL x. The shape of the displayed certificate, an ordinal stage, a defining formula, and an extensional equation, is the pattern the rest of the chapter instantiates.
defSet→isL : (σ : V ℓ) → IsOrd σ → (x : V ℓ) → ∥ Σ[ φ ∈ Formula ⟪ Lset σ ⟫ 1 ] (DefOf.defSet (Lset σ) φ ≡ x) ∥₁ → ⟨ isL x ⟩ defSet→isL σ oσ x p = 𝒟ₒ→isL σ oσ x (𝒟ₒ-intro (Lset σ) x p)
The zeroth instance of the pattern is the stage itself. The formula "true" defines the whole of a set, so every stage is a definable subset of itself, and therefore constructible one stage later. This is what lets a stage be named by a formula, the fact on which any construction that bounds a quantifier by a stage rests. Together with the packaging LsetS, which pairs a stage with its constructibility certificate, it makes the stage itself an element of the carrier of L.
The proof of isL-Lset is a direct instance of 𝒟ₒ→isL at x = Lset β. The witness formula is the constant-true formula ⊤̇, and defSet⊤≡A identifies its extension with the whole of the carrier set, here the stage Lset β itself. Wrapping the pair of formula and equation in a single truncation gives a member of 𝒟ₒ (Lset β), and the closure lemma lifts it to ⟨ isL (Lset β) ⟩. Nothing about the stage's internal structure is inspected; only the ordinality of β enters, through suc-ord.
opaque isL-Lset : (β : V ℓ) → IsOrd β → ⟨ isL (Lset β) ⟩ isL-Lset β oβ = 𝒟ₒ→isL β oβ (Lset β) (𝒟ₒ-intro (Lset β) (Lset β) ∣ ⊤̇ , DefOf.defSet⊤≡A (Lset β) ∣₁) LsetS : (β : V ℓ) → IsOrd β → S
The carrier S of the restricted structure consists of a set together with a proof that it lies in the class; LsetS supplies exactly that pairing for an ordinal stage: the underlying set Lset β with the certificate just built. Through this element the stage enters the constructible structure as an ordinary carrier point.
LsetS β oβ = Lset β , isL-Lset β oβ
The successor stage
The tower's step is the definable power set, and at a successor index the step is all there is: Lset (sucV σ) is 𝒟ₒ (Lset σ) exactly. The identity is proved as two inclusions. For one direction, σ is a member of its own successor, so every element of 𝒟ₒ (Lset σ), one of the sets being unioned, lies in the next stage. For the other, a member of Lset (sucV σ) lies in 𝒟ₒ (Lset δ) for some δ in sucV σ; either δ is a member of σ, and then the set is already in Lset σ and so among its definable subsets, or δ is σ and the inclusion is immediate. Neither half relativizes anything, and neither needs the operator to be monotone; no ordinality hypothesis on σ is used.
With the identity in hand, constructibility of the definable power set follows at once: a stage is constructible one stage later, and the definable power set of a stage is that very next stage.
The two sets are compared by ambient extensionality, which reduces the path to a pair of inclusions. The harder inclusion needs a bridge lemma: from a member x of the next stage, merely some earlier stage's definable power set contains x, with the witness δ a member of sucV σ. Since the members of sucV σ are, by its construction, either members of σ or σ itself, the witness is exactly the information the argument can case on.
Lset-suc : (σ : V ℓ) → Lset (sucV σ) ≡ 𝒟ₒ (Lset σ) Lset-suc σ = extensionality (Lset (sucV σ)) (𝒟ₒ (Lset σ)) (sub₁ , sub₂) where fromEarlier : (x : V ℓ) → Σ[ δ ∈ V ℓ ] (⟨ δ ∈ sucV σ ⟩ × ⟨ x ∈ 𝒟ₒ (Lset δ) ⟩)
The elimination of the witness uses exactly that dichotomy. ∈sucV-elim takes the proof that δ lies in sucV σ and two branches. In the first branch δ is a member of σ, so Lset-in places x inside Lset σ, and the lemma Lset⊆𝒟ₒ says that every member of a stage is one of its definable subsets, lifting x into 𝒟ₒ (Lset σ). In the second branch δ is σ itself, and subst transports the given membership across the path δ ≡ σ, changing the index of the stage. The whole target x ∈ 𝒟ₒ (Lset σ) is a proposition, which is what allows the truncated witness to be eliminated here at all.
→ ⟨ x ∈ 𝒟ₒ (Lset σ) ⟩ fromEarlier x (δ , (δ∈suc , x∈𝒟ₒδ)) = ∈sucV-elim {A = σ} {x = δ} (snd (x ∈ 𝒟ₒ (Lset σ))) δ∈suc (λ δ∈σ → Lset⊆𝒟ₒ σ x (Lset-in σ δ x δ∈σ x∈𝒟ₒδ)) (λ δ≡σ → subst (λ w → ⟨ x ∈ 𝒟ₒ (Lset w) ⟩) δ≡σ x∈𝒟ₒδ)
The first inclusion applies the bridge in its forward direction. A structural member of Lset (sucV σ) is converted by ∈∈ₛ into membership in the surrounding hierarchy, the stage characterization Lset-out returns the truncated earlier-stage witness, and fromEarlier maps it into 𝒟ₒ (Lset σ); the elimination lands in the proposition x ∈ 𝒟ₒ (Lset σ), which is what licenses discarding the choice of δ. The reverse inclusion needs only that σ belongs to its own successor: after ∈∈ₛ converts the structural membership into the ambient form, Lset-in with the witness self∈sucV σ places any member of 𝒟ₒ (Lset σ) directly into the stage at sucV σ. The two inclusions assemble into the identity as a path.
sub₁ : ⟨ Lset (sucV σ) ⊆ 𝒟ₒ (Lset σ) ⟩ sub₁ x x∈ₛ = ∈∈ₛ {a = x} {b = 𝒟ₒ (Lset σ)} .fst (PT.rec (snd (x ∈ 𝒟ₒ (Lset σ))) (fromEarlier x) (Lset-out (sucV σ) x (∈∈ₛ {a = x} {b = Lset (sucV σ)} .snd x∈ₛ))) sub₂ : ⟨ 𝒟ₒ (Lset σ) ⊆ Lset (sucV σ) ⟩
For the other inclusion, self∈sucV σ selects 𝒟ₒ (Lset σ) as one of the sets being unioned in the definition of Lset (sucV σ). Thus Lset-in sends each element of that definable power set into the successor stage. Together with the first inclusion, surrounding extensionality gives the path Lset (sucV σ) ≡ 𝒟ₒ (Lset σ); no ordinality hypothesis on σ occurs in this identity.
sub₂ x x∈ₛ = ∈∈ₛ {a = x} {b = Lset (sucV σ)} .fst (Lset-in (sucV σ) σ x (self∈sucV σ) (∈∈ₛ {a = x} {b = 𝒟ₒ (Lset σ)} .snd x∈ₛ))
The successor identity converts the statement that a stage is constructible one stage later into a statement about the definable power set itself: since Lset (sucV σ) is exactly 𝒟ₒ (Lset σ), and Lset (sucV σ) is constructible by the earlier lemma, the definable power set of any ordinal stage is constructible. It can then be packaged as an element of the carrier, a set of L with its constructibility certificate attached.
The proof is a transport along the successor identity. isL-Lset at the successor, whose ordinality is suc-ord oσ, proves ⟨ isL (Lset (sucV σ)) ⟩; rewriting the target along the path Lset-suc σ turns that into ⟨ isL (𝒟ₒ (Lset σ)) ⟩. No property of the operator beyond the identity is used.
opaque isL-𝒟ₒ : (σ : V ℓ) → IsOrd σ → ⟨ isL (𝒟ₒ (Lset σ)) ⟩ isL-𝒟ₒ σ oσ = subst (λ w → ⟨ isL w ⟩) (Lset-suc σ) (isL-Lset (sucV σ) (suc-ord oσ)) 𝒟ₒS : (σ : V ℓ) → IsOrd σ → S
The packaging 𝒟ₒS pairs the definable power set of the stage with its constructibility certificate, giving a carrier element that denotes exactly 𝒟ₒ (Lset σ). Where the previous section packaged a stage itself, this one packages the totality of definable subsets of a stage.
𝒟ₒS σ oσ = 𝒟ₒ (Lset σ) , isL-𝒟ₒ σ oσ
Finite families
The closure pattern is easiest to see on a finite family. Fix a stage Lset σ and a family of n members of it. Their image is the set finSet n h, and the finite disjunction of "equals this one" carves exactly that image out of the stage: at length zero the formula is falsity, and at each later length one more constant is compared against the free variable. The family may repeat a member; distinct positions may name the same set.
The whole content is one induction identifying satisfaction of the disjunction with being hit by the family, each direction stated for the embedded representatives of the named members. With both directions in hand, an ambient extensionality proves defSet≡, the equation saying the definable subset is exactly the image; finSet∈𝒟ₒ records the image as a member of 𝒟ₒ (Lset σ), and finSetL passes from the hypothesis that every family member lies in the stage to the certificate isL (finSet n h), via the closure lemma defSet→isL.
The image set is defined directly: finSet n h is the set presented by the index type Fin n lifted into the hierarchy's universe and the indexing map that applies h after lowering. Membership is characterized in the truncated form appropriate to the hierarchy: y belongs to finSet n h precisely when some index i merely satisfies h i ≡ y. Each direction of finSet-in and finSet-out is a single map inside the truncation, since membership in a presented set is by construction the truncated existence of an index.
finSet : (n : ℕ) → (Fin n → V ℓ) → V ℓ finSet n h = sett (Lift {ℓ-zero} {ℓ} (Fin n)) (λ i → h (lower i)) finSet-in : (n : ℕ) (h : Fin n → V ℓ) (y : V ℓ) → ∥ Σ[ i ∈ Fin n ] (h i ≡ y) ∥₁ → ⟨ y ∈ finSet n h ⟩ finSet-in n h y = PT.map (λ { (i , q) → lift i , q })
The reverse membership lemma finSet-out is the same map read backwards, from a lifted index back down to Fin n. The definability work then happens at an ordinal stage σ: working inside DefOf (Lset σ) fixes the alphabet of constants to be the small index type ⟪ Lset σ ⟫ of that stage, so a member of the stage can be named by a constant, and the definable subsets at issue are those carved from Lset σ.
finSet-out : (n : ℕ) (h : Fin n → V ℓ) (y : V ℓ) → ⟨ y ∈ finSet n h ⟩ → ∥ Σ[ i ∈ Fin n ] (h i ≡ y) ∥₁ finSet-out n h y = PT.map (λ { (i , q) → lower i , q }) module FinOf (σ : V ℓ) (oσ : IsOrd σ) where module DefC = DefOf (Lset σ)
The formula is the finite disjunction of equalities. At length zero there is nothing to be equal to, so the formula is falsity; at the successor of a length, the free variable is compared against the constant naming the first family member, and the remaining members are handled by the recursive call with the family shifted. The arity is one throughout: a single free-variable slot serves the whole disjunction, and the function g need not be injective, distinct positions may name the same member.
finDisj : (n : ℕ) → (Fin n → ⟪ Lset σ ⟫) → Formula ⟪ Lset σ ⟫ 1 finDisj zero g = ⊥̇ finDisj (suc n) g = (var zero ≐ con (g zero)) ∨̇ finDisj n (λ i → g (suc i)) private
The bridge statement Hits says that the member named by the environment is merely hit by the family, with the path written against the embedded representative ⟪ Lset σ ⟫↪ (g i) of the named member. The two directions connect satisfaction of the disjunction, which is what the definable subset sees, with being hit by the family, which is what the image set sees.
Hits : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫) (y : V ℓ) → Type (ℓ-suc ℓ) Hits n g y = ∥ Σ[ i ∈ Fin n ] (⟪ Lset σ ⟫↪ (g i) ≡ y) ∥₁ sat→hits : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫) (m : ⟪ Lset σ ⟫) → ⟨ (DefC.ι m ∷ []) DefC.⊨ᵐ finDisj n g ⟩ → Hits n g (⟪ Lset σ ⟫↪ m)
From satisfaction to hits proceeds by recursion on the length. At zero the formula is falsity, and a proof of it is absurd. At a successor, satisfaction is a truncated disjunction: in the left branch the environment equals the first constant, giving the index zero; in the right branch the recursive call returns a hit for the shifted family, whose index is promoted by one. Each branch returns its witness inside a truncation, and the outer elimination is legitimate because the target Hits is proposition-valued.
sat→hits zero g m bot = Empty.rec* bot sat→hits (suc n) g m = PT.rec squash₁ (λ { (inl e) → ∣ zero , sym e ∣₁ ; (inr sat) → PT.map (λ { (i , q) → suc i , q }) (sat→hits n (λ i → g (suc i)) m sat) })
The reverse direction turns a hit into satisfaction, again by recursion on the length. At length zero there is no index of type Fin 0, so a hit there can be refuted by matching against the empty index type; this matches the formula being falsity at zero. Since the statement of hits→sat is quantified over all lengths at once, the recursive call in the successor case is available without any hypothesis being carried along.
hits→sat : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫) (m : ⟪ Lset σ ⟫)
→ Hits n g (⟪ Lset σ ⟫↪ m)
→ ⟨ (DefC.ι m ∷ []) DefC.⊨ᵐ finDisj n g ⟩
hits→sat zero g m =
PT.rec (snd ((DefC.ι m ∷ []) DefC.⊨ᵐ finDisj zero g)) (λ { (() , _) })
At a successor length, the hit is a truncated pair whose index is either zero or a successor suc i. In the first case the path identifies the member with the first constant, and the left disjunct of the formula is satisfied. In the second, the recursive call applied to the shifted family produces satisfaction of the tail disjunction, which becomes the right disjunct. Both cases return their answer inside a truncation, so the proof never depends on which index a hit happened to carry.
hits→sat (suc n) g m = PT.rec (snd ((DefC.ι m ∷ []) DefC.⊨ᵐ finDisj (suc n) g)) (λ { (zero , q) → ∣ inl (sym q) ∣₁ ; (suc i , q) → ∣ inr (hits→sat n (λ j → g (suc j)) m ∣ i , q ∣₁) ∣₁ })
The two directions of the bridge are exactly the two inclusions that the identity defSet≡ needs. It is proved by ambient extensionality, which reduces the path of sets to a pair of inclusions, and the image set is abbreviated F. It remains to translate between membership in the structured presentation and membership in the surrounding hierarchy.
defSet≡ : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫) → DefC.defSet (finDisj n g) ≡ finSet n (λ i → ⟪ Lset σ ⟫↪ (g i)) defSet≡ n g = extensionality _ _ (sub₁ , sub₂) where F = finSet n (λ i → ⟪ Lset σ ⟫↪ (g i))
The first inclusion starts from a structural member y of the definable subset. The conversion ∈∈ₛ turns it into ambient membership, whose reading lemma supplies the truncated defining data: an environment m with a satisfaction certificate, together with a path q identifying y with the member named by m. The goal being proved at that point is the proposition ⟨ y ∈ F ⟩, which is what licenses eliminating the truncation.
sub₁ : ⟨ DefC.defSet (finDisj n g) ⊆ F ⟩ sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = F} .fst (PT.rec (snd (y ∈ F)) (λ { ((m , h) , q) → subst (λ v → ⟨ v ∈ F ⟩) q (finSet-in n (λ i → ⟪ Lset σ ⟫↪ (g i)) (⟪ Lset σ ⟫↪ m)
The satisfaction certificate is converted, by the computation rule defSet-mem for membership in a definable subset, into a satisfaction of the disjunction at the environment m. The bridge lemma sat→hits then produces a hit, and finSet-in reads the hit as membership of the embedded element in the image. The transport along q finally relocates that membership from the named member to y itself.
(sat→hits n g m (subst ⟨_⟩ (DefC.defSet-mem (finDisj n g) m) ∣ (m , h) , refl ∣₁))) }) (∈∈ₛ {a = y} {b = DefC.defSet (finDisj n g)} .snd y∈ₛ)) sub₂ : ⟨ F ⊆ DefC.defSet (finDisj n g) ⟩
The reverse inclusion starts from y ∈ F. The elimination rule finSet-out merely supplies an index i : Fin n and a path q : ⟪ Lset σ ⟫↪ (g i) ≡ y. At the representative g i, the truncated witness ∣ i , refl ∣₁ proves Hits n g (⟪ Lset σ ⟫↪ (g i)); hits→sat converts it into satisfaction of the finite disjunction there. The following transport along q then yields membership of y in the definable subset.
sub₂ y y∈ₛ = PT.rec (snd (y ∈ₛ DefC.defSet (finDisj n g))) (λ { (i , q) → subst (λ v → ⟨ v ∈ₛ DefC.defSet (finDisj n g) ⟩) q (∈∈ₛ {a = ⟪ Lset σ ⟫↪ (g i)} {b = DefC.defSet (finDisj n g)} .fst (subst ⟨_⟩ (sym (DefC.defSet-mem (finDisj n g) (g i)))
The satisfaction is read, through the membership reading of defSet used in reverse, as structural membership of the embedded g i in the definable subset, and the transport along the hit's path moves it onto y. With both inclusions assembled, defSet≡ states the equality as a path of sets: the subset carved by the finite disjunction is the image of the family, repetitions in the family included, since equal members are named by several constants without affecting the image.
(hits→sat n g (g i) ∣ i , refl ∣₁))) }) (finSet-out n (λ i → ⟪ Lset σ ⟫↪ (g i)) y (∈∈ₛ {a = y} {b = F} .snd y∈ₛ)) finSet∈𝒟ₒ : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫) → ⟨ finSet n (λ i → ⟪ Lset σ ⟫↪ (g i)) ∈ 𝒟ₒ (Lset σ) ⟩
Two packaging steps finish the section. First, finSet∈𝒟ₒ supplies the disjunction and the identity just proved to 𝒟ₒ-intro, recording the image set as a member of the definable power set of the stage; the certificate is truncated, so the particular formula is not part of the data retained. Second, finSetL starts from a family of arbitrary sets, each of which is given as lying in the stage by a membership proof. For each member, ∈-asFiber converts that membership proof into an index of the stage's presentation together with a path back to the member; collecting these paths and rewriting the image set along them by cong (finSet n) (funExt qg) identifies it with the embedded family that defSet≡ speaks about. The closure lemma defSet→isL then delivers the constructibility of finSet n h.
finSet∈𝒟ₒ n g = 𝒟ₒ-intro (Lset σ) _ ∣ finDisj n g , defSet≡ n g ∣₁ finSetL : (n : ℕ) (h : Fin n → V ℓ) → ((i : Fin n) → ⟨ h i ∈ Lset σ ⟩) → ⟨ isL (finSet n h) ⟩ finSetL n h hσ = defSet→isL σ oσ (finSet n h) ∣ finDisj n g , (defSet≡ n g ∙ cong (finSet n) (funExt qg)) ∣₁
The hypothesis hσ i states merely that h i lies in the stage. Membership in a hierarchy set is a truncated fiber of the embedding ⟪ Lset σ ⟫↪, and because that map is an embedding its fiber types are propositions, so eliminating the truncation into a fiber type is legitimate and ∈-asFiber performs exactly that conversion. Thus g i is a chosen index whose embedded element has the path qg i back to h i. The certificate handed to defSet→isL pairs the finite disjunction in the representatives g with defSet≡ n g followed by the rewriting funExt qg, carrying the identification from the embedded family finSet n (λ i → ⟪ Lset σ ⟫↪ (g i)) to the original family finSet n h.
where g : Fin n → ⟪ Lset σ ⟫ g i = ∈-asFiber {a = h i} {b = Lset σ} (hσ i) .fst qg : (i : Fin n) → ⟪ Lset σ ⟫↪ (g i) ≡ h i qg i = ∈-asFiber {a = h i} {b = Lset σ} (hσ i) .snd
Two sets, one stage
isL-directed places any two constructible sets in one common ordinal stage.
Each constructible set has a stage of its own, given merely by its truncated certificate of constructibility. The conclusion combines the two: merely, there is an ordinal σ whose stage contains both sets. The ordinal bound2 produces one that contains both given ordinals, and monotonicity of stages carries each set from its own stage up into the stage at the bound. The result is stated truncated, so no stage is ever exhibited to the outside; locally the two certificates are opened far enough to read off the two stages they name.
The statement takes two constructible sets as truncated certificates: ⟨ isL x ⟩ and ⟨ isL y ⟩ say merely that each lies in L, without naming a stage. The conclusion is likewise truncated, so the two certificates are eliminated only into a truncated existence statement, and no stage is ever chosen for the outside world. Locally the target content is packaged as Bound: an ordinal σ, its ordinality, and the two memberships in Lset σ.
isL-directed : (x y : V ℓ) → ⟨ isL x ⟩ → ⟨ isL y ⟩ → ∥ Σ[ σ ∈ V ℓ ] (IsOrd σ × (⟨ x ∈ Lset σ ⟩ × ⟨ y ∈ Lset σ ⟩)) ∥₁ isL-directed x y px py = PT.rec2 squash₁ go px py where Bound : Type (ℓ-suc ℓ)
The two truncations are eliminated at once by PT.rec2, whose target is the truncation ∥ Bound ∥₁. Its working part go receives the explicit data that the certificates conceal: a stage α, ordinal, with x in Lset α, and a stage β, ordinal, with y in Lset β. Merging them is not a comparison of sizes; bound2 α β oα oβ returns a single ordinal bound that contains both α and β, together with its ordinality and the two memberships.
Bound = Σ[ σ ∈ V ℓ ] (IsOrd σ × (⟨ x ∈ Lset σ ⟩ × ⟨ y ∈ Lset σ ⟩)) go : Σ[ α ∈ V ℓ ] (IsOrd α × ⟨ x ∈ Lset α ⟩) → Σ[ β ∈ V ℓ ] (IsOrd β × ⟨ y ∈ Lset β ⟩) → ∥ Bound ∥₁ go (α , (oα , x∈Lα)) (β , (oβ , y∈Lβ)) = ∣ bnd .fst , (bnd .snd .fst , ( Lset-mono (bnd .snd .snd .fst) x∈Lα
The bound comes with memberships α ∈ σ₀ and β ∈ σ₀, so monotonicity Lset-mono lifts x ∈ Lset α into the stage Lset σ₀ at the bound, and likewise for y from β. Wrapping the assembled triple in ∣_∣₁ completes go, and with it the whole statement: any two constructible sets merely have a common ordinal stage. This is what the pairing field will consume, since it needs both arguments visible at one stage.
, Lset-mono (bnd .snd .snd .snd) y∈Lβ )) ∣₁ where bnd = bound2 α β oα oβ
The two inherited axioms
Extensionality and regularity both restrict from the ambient hierarchy, but by different arguments. For extensionality, isL-trans turns an ambient member of either constructible set into a carrier element, so the assumed agreement on carrier members applies; ambient extensionality then equates the underlying sets and restriction reflection gives a carrier path. Regularity does not use isL-trans: ambient accessibility is restricted recursively to pairs already carrying their constructibility certificates.
Extensionality inside L has the shape: if two carrier elements agree on membership at every carrier element, they are equal as paths. The proof reduces to the underlying hierarchy. The carrier consists of pairs of a set with a constructibility certificate, and ↾-reflects is the principle that such pairs are determined by their first projections: a path between the underlying sets fst a and fst b already gives a path a ≡ b. Everything therefore rests on producing that underlying path, which extensionalV supplies given vwise.
extensionalL : {a b : S} → ((x : S) → (x ∈ˢ a) ≡ (x ∈ˢ b)) → a ≡ b extensionalL {a} {b} h = ↾-reflects {𝒮 = 𝒮ᵥ} {M = isL} (extensionalV {a = fst a} {b = fst b} vwise) where vwise : (v : V ℓ) → (v ∈ fst a) ≡ (v ∈ fst b)
The hypothesis h only speaks about carrier elements, that is, about constructible pairs. To extend it to an arbitrary v of the hierarchy, transitivity does the work: from v ∈ fst a and the certificate carried by a, isL-trans yields that v is itself constructible; pairing that certificate with v presents it as a carrier element, and h at that element gives a path of restricted memberships. Transporting v∈a along that path lands in ⟨ v ∈ fst b ⟩, so fwd is a plain implication. Joining the two implications with ⇔toPath yields the pointwise path of ambient membership that extensionalV demands.
vwise v = ⇔toPath fwd bwd where fwd : ⟨ v ∈ fst a ⟩ → ⟨ v ∈ fst b ⟩ fwd v∈a = subst ⟨_⟩ (h (v , isL-trans v∈a (a .snd))) v∈a bwd : ⟨ v ∈ fst b ⟩ → ⟨ v ∈ fst a ⟩
The backward direction is the same argument read from b, with sym because h points from a to b. This closes extensionalL. Regularity asks for something else: well-foundedness of the carrier's membership relation, as explicit accessibility data. For a pair (v , p), meaning the set v together with its constructibility certificate, the ambient hierarchy already provides Acc for v; the task is to lift that data through the certificate.
bwd v∈b = subst ⟨_⟩ (sym (h (v , isL-trans v∈b (b .snd)))) v∈b regularityL : WellFounded _∈ᵗ_ regularityL (v , p) = accL v (regularityV v) p where module Vmem = hPropStructure 𝒮ᵥ
The lifting is a recursion on the ambient accessibility data. If u is accessible, then by definition every ambient member y of u is accessible, and the clause rec packages exactly that. A member (y , r) of the restricted element (u , q) projects to an ambient member y of u, so accL may recurse on rec y y∈ and attach the certificate r to the result. The restricted membership y ∈ᵗ (u , q) is inherited solely from the underlying relation y ∈ u; the certificate r belongs to the predecessor carrier element (y , r), rather than to the membership proof. Thus accessibility transfers member by member along the underlying set.
accL : (u : V ℓ) → Acc Vmem._∈ᵗ_ u → (q : u ∈ᶜ isL) → Acc _∈ᵗ_ (u , q) accL u (acc rec) q = acc (λ { (y , r) y∈ → accL y (rec y y∈) r })
Uniqueness from extensionality
uniqueL derives uniqueness from extensionality: any set realizing a fixed membership specification is unique, so the axiom fields still ahead need only a witness that merely exists.
The argument is the extensionality of the carrier applied to realizers. Two sets realizing the same predicate Q agree, at every carrier element, on the same truth value, namely Q x, so extensionalL equates them. Uniqueness in the form needed here is contractibility, and contractibility is a proposition, which is exactly what lets a merely existing realizer be turned into the contractibility data itself.
Uniqueness of a realizer is contractibility data: a center, namely any realizing set, together with a path from the center to every realizing set. The path-producing part is extensionalL, since two realizing sets carry the same membership specification and hence coincide; the assembly of center and paths is setOf-unique applied to extensionalL. The second statement passes from mere existence: PT.rec may eliminate the truncated hypothesis because its target isContr (SetOf Q) is a proposition, and returns the same contractibility data. From here on, each remaining axiom field is proved by exhibiting one witness, supplied truncated.
uniqueL : (Q : S → hProp (ℓ-suc ℓ)) → SetOf Q → isContr (SetOf Q) uniqueL = setOf-unique extensionalL mere→uniqueL : (Q : S → hProp (ℓ-suc ℓ)) → ∥ SetOf Q ∥₁ → isContr (SetOf Q) mere→uniqueL Q = PT.rec isPropIsContr (uniqueL Q)
The empty set
The false object-language formula carves the ambient empty set as a definable subset, and hasEmptyL packages its constructibility and empty-membership specification.
The falsehood of the object language carves nothing out of any stage: a member of defSet ⊥̇ would carry a proof of falsehood at its index. So defSet ⊥̇ is the empty set, one extensionality apart, and the empty set is therefore constructible. Its specification comes from the hierarchy, since membership in L is membership in the hierarchy, and the uniqueness principle of the previous section turns the witness into the contractibility the model demands.
The empty set is the first constructed set, and it needs no bounding at all: the argument σ ranges over arbitrary stages, with no ordinality hypothesis, because a formula defining the empty set can be read at any stage whatsoever. The certificate is the pairing of the object-language falsity ⊥̇ with the equation defSet⊥≡∅, and it is supplied truncated, as 𝒟ₒ-intro expects.
∅∈𝒟ₒ : (σ : V ℓ) → ⟨ ∅ ∈ 𝒟ₒ (Lset σ) ⟩ ∅∈𝒟ₒ σ = 𝒟ₒ-intro (Lset σ) ∅ ∣ ⊥̇ , defSet⊥≡∅ ∣₁ where module DefC = DefOf (Lset σ) defSet⊥≡∅ : DefC.defSet ⊥̇ ≡ ∅
The equation is one extensionality against the ambient empty set, in two inclusions. The first is the substantive direction: a member y of the definable subset comes, by the reading lemma for defSet, as a truncated pair of an index m and a satisfaction proof h for ⊥̇. Satisfaction of falsity is an empty host type, so Empty.rec* h refutes any such member. Since inclusion is stated as a proposition-valued statement, eliminating the truncation into it is legitimate.
defSet⊥≡∅ = extensionality (DefC.defSet ⊥̇) ∅ (sub₁ , sub₂) where sub₁ : ⟨ DefC.defSet ⊥̇ ⊆ ∅ ⟩ sub₁ y y∈ₛ = PT.rec (snd (y ∈ₛ ∅)) (λ { ((m , h) , q) → Empty.rec* h })
The second inclusion is vacuous: ∅-empty turns any would-be member of the ambient empty set directly into a refutation. With both directions in hand, defSet ⊥̇ and ∅ are equal as sets, and ∅∈𝒟ₒ records that the empty set is a definable subset of an arbitrary stage. The closure lemma then applies one last time, at the stage ∅ itself, whose ordinality is the lemma ∅-ord: the empty set is constructible, one successor above itself.
(∈∈ₛ {a = y} {b = DefC.defSet ⊥̇} .snd y∈ₛ) sub₂ : ⟨ ∅ ⊆ DefC.defSet ⊥̇ ⟩ sub₂ y y∈ₛ = Empty.rec (∅-empty y y∈ₛ) ∅∈L : ⟨ isL ∅ ⟩ ∅∈L = 𝒟ₒ→isL ∅ ∅-ord ∅ (∅∈𝒟ₒ ∅)
Packaging mirrors the underlying set: ∅ʟ is the pair of ∅ with its constructibility certificate, an element of the carrier S. The model's existence statement requires a unique set with no members. The witness offered is ∅ʟ together with the specification taken from the hierarchy, empty-spec read at the underlying set of any candidate; uniqueness then follows by uniqueL. This is the first field, and the pattern of the next two is already visible in it: bound, carve, close.
∅ʟ : S ∅ʟ = ∅ , ∅∈L hasEmptyL : isContr (SetOf (λ _ → ⊥)) hasEmptyL = uniqueL _ (∅ʟ , (λ x → empty-spec (fst x)))
Pairing, bounded by a stage
For two members of one stage, a two-constant disjunction carves their unordered pair as a definable subset, and the derived statements place the singleton one stage up and the Kuratowski ordered-pair code two stages up.
The unordered pair of two members of a stage is a definable subset of that stage: each of them is ⟪ Lset σ ⟫↪ of some index, and the formula naming those two indices carves out exactly the pair. Checking that takes one extensionality against the hierarchy's own pairing axiom, in both directions: a member of the definable subset satisfies the disjunction, hence is one of the two; and each of the two satisfies it, hence is a member.
Nothing in the argument concerns the model. What it says is a fact about the tower, and it is stated as one: an ordered pair in Kuratowski's encoding is two unordered pairs deep, so it sits two stages above its entries.
Ordinality is not asked for, exactly as the successor identity does not ask for it, and for the same reason: carving is not comparison. The singleton is the degenerate pair, and the ordered pair is the pair of a singleton with a pair.
The statement assumes only that x and y lie in the stage Lset σ; no ordinality of σ is required, because carving a subset needs no comparison of stages. The certificate is assembled by 𝒟ₒ-intro: a formula φ together with the equation defSet≡ saying that φ's extension inside the stage is exactly ⁅ x , y ⁆, supplied merely, as the definability operator's interface expects.
pair∈𝒟ₒ : (σ x y : V ℓ) → ⟨ x ∈ Lset σ ⟩ → ⟨ y ∈ Lset σ ⟩ → ⟨ ⁅ x , y ⁆ ∈ 𝒟ₒ (Lset σ) ⟩ pair∈𝒟ₒ σ x y x∈ y∈ = 𝒟ₒ-intro (Lset σ) ⁅ x , y ⁆ ∣ φ , defSet≡ ∣₁ where module DefC = DefOf (Lset σ)
The formula must name constants drawn from the small presentation ⟪ Lset σ ⟫ of the stage. Applying ∈-asFiber to the two membership proofs gives actual indices mₓ and mᵧ, together with paths qₓ : ⟪ Lset σ ⟫↪ mₓ ≡ x and qᵧ : ⟪ Lset σ ⟫↪ mᵧ ≡ y. This direct recovery is available because the presentation embedding has propositional fibers; the membership hypotheses are not treated as an outer truncation here.
mₓ = ∈-asFiber {a = x} {b = Lset σ} x∈ .fst qₓ : ⟪ Lset σ ⟫↪ mₓ ≡ x qₓ = ∈-asFiber {a = x} {b = Lset σ} x∈ .snd mᵧ = ∈-asFiber {a = y} {b = Lset σ} y∈ .fst qᵧ : ⟪ Lset σ ⟫↪ mᵧ ≡ y
The formula has one free-variable slot and reads: the variable equals the constant mₓ, or it equals the constant mᵧ. Its claimed extension is the unordered pair of x and y. The proof does not identify the extension with that pair directly; it first identifies it with the pair of the embedded representatives, where the constants actually live, and then transports the whole equation along qₓ and qᵧ by congruence under ⁅_,_⁆.
qᵧ = ∈-asFiber {a = y} {b = Lset σ} y∈ .snd φ : Formula ⟪ Lset σ ⟫ 1 φ = (var zero ≐ con mₓ) ∨̇ (var zero ≐ con mᵧ) defSet≡ : DefC.defSet φ ≡ ⁅ x , y ⁆ defSet≡ =
The first half of the identification is one extensionality, from the definable subset to the pair of embedded representatives, split into two inclusions. The direction shown here says: whatever satisfies φ is one of the two named elements.
extensionality (DefC.defSet φ) ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆ (sub₁ , sub₂) ∙ cong₂ ⁅_,_⁆ qₓ qᵧ where sub₁ : ⟨ DefC.defSet φ ⊆ ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆ ⟩
A member w of the definable subset is presented, by the reading lemma, as a truncated pair of an index m and a satisfaction proof for φ at the environment naming m. The satisfaction of a disjunction of equalities records, merely, that the element named by m equals one of the two constants. That truncated disjunction is exactly the hypothesis the hierarchy's pairing characterization requires in its right-to-left direction, so pairing-ax places the embedded element ⟪ Lset σ ⟫↪ m inside the pair of embedded representatives. The transport along the path q identifying w with the embedded index then finishes the inclusion.
sub₁ w w∈ₛ = PT.rec (snd (w ∈ₛ ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆)) (λ { ((m , h) , q) → subst (λ v → ⟨ v ∈ₛ ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆ ⟩) q (pairing-ax (⟪ Lset σ ⟫↪ mₓ) (⟪ Lset σ ⟫↪ mᵧ) (⟪ Lset σ ⟫↪ m) .snd (subst ⟨_⟩ (DefC.defSet-mem φ m) ∣ (m , h) , refl ∣₁)) })
The reverse inclusion reads the hierarchy's pairing characterization in its other direction. A member w of the pair of embedded representatives is, merely, equal to one of the two entries. Each of the two branches supplies the same helper with the corresponding representative: knowing which representative w equals, one shows w satisfies φ at that representative's constant, and is therefore a member of the definable subset.
(∈∈ₛ {a = w} {b = DefC.defSet φ} .snd w∈ₛ) sub₂ : ⟨ ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆ ⊆ DefC.defSet φ ⟩ sub₂ w w∈ₛ = PT.rec (snd (w ∈ₛ DefC.defSet φ)) (λ { (inl p) → memOf mₓ ∣ inl refl ∣₁ p ; (inr p) → memOf mᵧ ∣ inr refl ∣₁ p })
The helper memOf takes a representative mᵢ, a satisfaction proof for φ at the constant naming mᵢ, and a path identifying w with the embedded element of mᵢ. The membership reading of defSet turns satisfaction at the constant into membership of the embedded element in the definable subset; transporting along the path, in the direction sym p, moves that membership to w. With both inclusions proved, the extensionality yields the equation with the pair of embedded representatives, and the congruence step under ⁅_,_⁆ rewrites that pair into ⁅ x , y ⁆ along the paths qₓ and qᵧ.
(pairing-ax (⟪ Lset σ ⟫↪ mₓ) (⟪ Lset σ ⟫↪ mᵧ) w .fst w∈ₛ) where memOf : (mᵢ : ⟪ Lset σ ⟫) → ⟨ (DefC.ι mᵢ ∷ []) DefC.⊨ᵐ φ ⟩ → w ≡ ⟪ Lset σ ⟫↪ mᵢ → ⟨ w ∈ₛ DefC.defSet φ ⟩ memOf mᵢ sat p = subst (λ v → ⟨ v ∈ₛ DefC.defSet φ ⟩) (sym p)
The first derived result converts the definability statement into membership in a stage. The successor identity proved earlier in this chapter says that Lset (sucV σ) is exactly 𝒟ₒ (Lset σ), so transporting the conclusion of pair∈𝒟ₒ along that identity, in the direction sym, yields ⟨ ⁅ x , y ⁆ ∈ Lset (sucV σ) ⟩: the unordered pair of two members of a stage is contained in the displayed next-stage bound.
(∈∈ₛ {a = ⟪ Lset σ ⟫↪ mᵢ} {b = DefC.defSet φ} .fst (subst ⟨_⟩ (sym (DefC.defSet-mem φ mᵢ)) sat)) pair∈Lset-suc : (σ x y : V ℓ) → ⟨ x ∈ Lset σ ⟩ → ⟨ y ∈ Lset σ ⟩ → ⟨ ⁅ x , y ⁆ ∈ Lset (sucV σ) ⟩ pair∈Lset-suc σ x y x∈ y∈ =
The singleton is the degenerate case. Applying the pair placement to x twice gives the pair ⁅ x , x ⁆ in the next stage, and the hierarchy's identification pair-singleton of ⁅ x , x ⁆ with ⁅ x ⁆s transports that membership onto the singleton ⁅ x ⁆s.
subst (λ w → ⟨ ⁅ x , y ⁆ ∈ w ⟩) (sym (Lset-suc σ)) (pair∈𝒟ₒ σ x y x∈ y∈) sgl∈Lset-suc : (σ x : V ℓ) → ⟨ x ∈ Lset σ ⟩ → ⟨ ⁅ x ⁆s ∈ Lset (sucV σ) ⟩ sgl∈Lset-suc σ x x∈ = subst (λ w → ⟨ w ∈ Lset (sucV σ) ⟩) (pair-singleton x) (pair∈Lset-suc σ x x x∈ x∈) pr∈Lset-suc : (σ x y : V ℓ) → ⟨ x ∈ Lset σ ⟩ → ⟨ y ∈ Lset σ ⟩
The ordered pair code pr x y is the pair whose two entries are the singleton ⁅ x ⁆s and the unordered pair ⁅ x , y ⁆. Both entries lie in Lset (sucV σ), the first by the singleton result and the second by the pair result, so the outer unordered pair can be placed at the stage one further up: pr x y lies in Lset (sucV (sucV σ)). Because the Kuratowski code nests one unordered pair inside another, two applications of pair closure give the displayed two-successor upper bound for the ordered-pair code; this does not assert that the code first appears there.
→ ⟨ pr x y ∈ Lset (sucV (sucV σ)) ⟩ pr∈Lset-suc σ x y x∈ y∈ = pair∈Lset-suc (sucV σ) ⁅ x ⁆s ⁅ x , y ⁆ (sgl∈Lset-suc σ x x∈) (pair∈Lset-suc σ x y x∈ y∈)
Pairing
hasPairL first places two arbitrary constructible sets in a common stage, then applies the bounded pair construction and the uniqueness principle.
The witness for the axiom is the unordered pair of the two arguments at a common ordinal stage, proved constructible by the lemma of the previous section; the specification is the hierarchy's own classification of the unordered pair, read at the underlying sets. Uniqueness then comes from extensionality.
The pairing field is stated over two arguments. Its predicate Q x says that an element x is equal to a or to b, with the disjunction interpreted in the model's truth values. A set realizes the field when its elements are exactly those satisfying Q. The construction mkPair assumes a common ordinal stage containing the underlying sets of both arguments, which is precisely what the bounding step supplies.
module PairOf (a b : S) where Q : S → hProp (ℓ-suc ℓ) Q x = (x ≈ˢ a) ⊔ (x ≈ˢ b) mkPair : (σ : V ℓ) → IsOrd σ → ⟨ fst a ∈ Lset σ ⟩ → ⟨ fst b ∈ Lset σ ⟩ → SetOf Q
The witness is the ambient unordered pair of the underlying sets, packaged with its constructibility certificate. That certificate comes from the bounded construction: the pair of two members of Lset σ is a definable subset there, and the lemma 𝒟ₒ→isL lifts a definable subset of an ordinal stage into L. The specification is the hierarchy's own classification of the unordered pair, pair-spec, read at the underlying sets; restricted membership is ambient membership on carriers, so the model's reading of the field coincides with the hierarchy's classification.
mkPair σ oσ fa∈ fb∈ = pairElt , (λ z → pair-spec (fst a) (fst b) (fst z)) where pairElt : S pairElt = ⁅ fst a , fst b ⁆ , 𝒟ₒ→isL σ oσ ⁅ fst a , fst b ⁆ (pair∈𝒟ₒ σ (fst a) (fst b) fa∈ fb∈)
The construction is not yet the field: it needs a stage, and only its mere existence is available. build eliminates the truncation from isL-directed with PT.rec, whose target ∥ SetOf Q ∥₁ is itself truncated, so the two certificates of constructibility for a and b may be opened just far enough to read off the common stage and the two memberships, and mkPair runs there. No stage is chosen for the outside world.
build : ∥ SetOf Q ∥₁ build = PT.rec squash₁ (λ { (σ , (oσ , (fa∈ , fb∈))) → ∣ mkPair σ oσ fa∈ fb∈ ∣₁ }) (isL-directed (fst a) (fst b) (a .snd) (b .snd)) hasPairL : (a b : S) → isContr (SetOf (λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b)))
The field hasPairL asks for contractibility of the type of realizers: a canonical realizer together with a path from it to every other realizer. The truncated common-stage bound is eliminated only into the truncated existence ∥ SetOf Q ∥₁; within that elimination, mkPair constructs a realizer from the stage and its two membership proofs. Then mere→uniqueL, using uniqueL and extensionality, turns mere existence plus uniqueness into an explicit center of contraction. Thus the proof makes no arbitrary choice of a common stage, while its final result does contain the definite canonical realizer required by isContr.
hasPairL a b = mere→uniqueL (PairOf.Q a b) (PairOf.build a b)
Union
Union needs no bounding search: a single stage containing the argument already suffices. Because the stage Lset σ is transitive, every member of a member of fst a is again in the stage, so a bounded existential formula, "some member of the argument has me as a member", carves out exactly the ambient union ⋃ (fst a).
The extensional equation is proved by two inclusions. One direction reads the formula's satisfaction: a witness v with y a member of v is exactly what the hierarchy's union classification asks for. The other direction starts from the union classification and must first pull the intermediate member v into the stage, which is precisely what stage transitivity does, applied twice. The final specification compares two quantifiers: the constructible condition quantifies over carrier witnesses only, while the hierarchy's union law quantifies over all of V, and isL-trans identifies the two ranges in both directions. With union in place, this chapter has proved five axioms: extensionality, regularity, the empty set, pairing, and union.
The membership condition Q is an indexed disjunction inside the model's truth values: x realizes the union when, for some y that is a member of a, x is a member of y. The construction mkUnion carries a single hypothesis, that one ordinal stage σ contains the underlying set of a. There is no second argument to house, so unlike pairing no bounding ordinal is needed; the stage that a itself already has is enough.
module UnionOf (a : S) where Q : S → hProp (ℓ-suc ℓ) Q x = ∃[ y ∶ S ] (y ∈ˢ a) ⊓ (x ∈ˢ y) mkUnion : (σ : V ℓ) → IsOrd σ → ⟨ fst a ∈ Lset σ ⟩ → SetOf Q mkUnion σ oσ fa∈ = unionElt , spec
At the stage Lset σ, formulas range over its small presentation. Its transitivity, obtained from Lset-layer σ and layer-trans, says that a member of a member of the stage lies in the stage again. Applying ∈-asFiber to the given membership of fst a produces the representative mₐ and path qₐ : ⟪ Lset σ ⟫↪ mₐ ≡ fst a; as above, this is direct fiber data rather than elimination of an outer truncation.
where module DefA = DefOf (Lset σ) Atrans = layer-trans (Lset-layer σ) mₐ = ∈-asFiber {a = fst a} {b = Lset σ} fa∈ .fst qₐ : ⟪ Lset σ ⟫↪ mₐ ≡ fst a
The formula has one free-variable slot and is a bounded existential: the variable ranges over the members of the constant mₐ, that is, over the members of a as presented inside the stage, and the matrix says that the bound variable has the outer variable as a member. Since the bound variable occupies the first slot inside the quantifier body, the outer variable sits in the successor slot. The claimed extension is the ambient union ⋃ (fst a), and the equation defSet≡ is one extensionality, split into two inclusions.
qₐ = ∈-asFiber {a = fst a} {b = Lset σ} fa∈ .snd φ : Formula ⟪ Lset σ ⟫ 1 φ = ∃̇∈ (con mₐ) (var (suc zero) ∈̇ var zero) defSet≡ : DefA.defSet φ ≡ ⋃ (fst a) defSet≡ = extensionality (DefA.defSet φ) (⋃ (fst a)) (sub₁ , sub₂)
The first inclusion says: everything satisfying the formula lies in the ambient union. A member y of the definable subset arrives, by the reading lemma for defSet, as a truncated pair of an index m and a satisfaction proof, together with a path q identifying y with the embedded element ⟪ Lset σ ⟫↪ m. The satisfaction hypothesis names members by their indices, so it can only be consumed for the embedded element; transporting along q moves the goal from y to that element, and the elimination into the proposition y ∈ₛ ⋃ (fst a) is what keeps the whole step legitimate.
where sub₁ : ⟨ DefA.defSet φ ⊆ ⋃ (fst a) ⟩ sub₁ y y∈ₛ = PT.rec (snd (y ∈ₛ ⋃ (fst a))) (λ { ((m , h) , q) → subst (λ w → ⟨ w ∈ₛ ⋃ (fst a) ⟩) q
The satisfaction proof for the bounded existential yields, merely, a witness v from the range together with the two matrix memberships: fst v is a member of the embedded mₐ, and the embedded m is a member of fst v. These are exactly the two memberships the hierarchy's union classification requires in its introduction direction: to place ⟪ Lset σ ⟫↪ m inside ⋃ (fst a) it suffices to exhibit some member of fst a having it as a member.
(PT.rec (snd (⟪ Lset σ ⟫↪ m ∈ₛ ⋃ (fst a))) (λ { (v , (fstv∈mₐ , m∈fstv)) → union-ax (fst a) (⟪ Lset σ ⟫↪ m) .snd ∣ fst v , ( ∈∈ₛ {a = fst v} {b = fst a} .fst
The two matrix memberships, however, speak the restricted presentation's language and must become ambient ones. ∈∈ₛ performs the conversion, and the path qₐ already in hand rewrites the range from the embedded mₐ to fst a, so the witness fst v is presented as a member of fst a; the second conjunct is used as it stands, since it is already a membership of the embedded m in fst v. With both memberships in ambient form, the union classification applies and the first inclusion closes.
(subst (λ w → ⟨ fst v ∈ w ⟩) qₐ fstv∈mₐ) , ∈∈ₛ {a = ⟪ Lset σ ⟫↪ m} {b = fst v} .fst m∈fstv ) ∣₁ }) (subst ⟨_⟩ (DefA.defSet-mem φ m) ∣ (m , h) , refl ∣₁)) }) (∈∈ₛ {a = y} {b = DefA.defSet φ} .snd y∈ₛ) sub₂ : ⟨ ⋃ (fst a) ⊆ DefA.defSet φ ⟩
The reverse inclusion reads the same classification in its other direction: membership of y in the ambient union is, merely, a member v of fst a with y a member of v. The helper member must then exhibit y inside the definable subset for this particular v. This is the half where the stage hypothesis does the work, because nothing so far guarantees that the intermediate v is visible in the stage at all.
sub₂ y y∈ₛ = PT.rec (snd (y ∈ₛ DefA.defSet φ)) (λ { (v , (v∈ₛfa , y∈ₛv)) → member v v∈ₛfa y∈ₛv }) (union-ax (fst a) y .fst y∈ₛ) where member : (v : V ℓ) → ⟨ v ∈ₛ fst a ⟩ → ⟨ y ∈ₛ v ⟩
The helper first converts y into a representative m' of the stage with its identifying path q', and uses the membership reading of defSet backward: satisfaction of φ at the constant naming m' becomes membership of the embedded m', and the transport along q' moves that membership to y. All that remains is the satisfaction proof sat, which is assembled from the two memberships v ∈ₛ fst a and y ∈ₛ v: transitivity of the stage, applied through Atrans, certifies first that v lies in Lset σ and then that y does as well, and the two conjuncts are transported to the embedded presentation along the paths sym qₐ and sym q'.
→ ⟨ y ∈ₛ DefA.defSet φ ⟩ member v v∈ₛfa y∈ₛv = subst (λ w → ⟨ w ∈ₛ DefA.defSet φ ⟩) q' (∈∈ₛ {a = ⟪ Lset σ ⟫↪ m'} {b = DefA.defSet φ} .fst (subst ⟨_⟩ (sym (DefA.defSet-mem φ m')) sat))
This block is where the stage hypothesis earns its keep, and it is the one step pairing did not need. The two ambient memberships are first read back out of their structural form by ∈∈ₛ: v is a member of the underlying set of a, and y is a member of v. Transitivity of the stage is then applied twice. Since fst a lies in Lset σ and the stage is transitive, its member v lies in Lset σ too; applying the same reasoning to the membership of y in v certifies y itself as a member of the stage. So a member of a member of a is pulled into the stage, which is precisely what lets the formula's quantifier see it.
where v∈fa = ∈∈ₛ {a = v} {b = fst a} .snd v∈ₛfa y∈v = ∈∈ₛ {a = y} {b = v} .snd y∈ₛv v∈A = Atrans {x = fst a} {y = v} v∈fa fa∈ y∈A = Atrans {x = v} {y = y} y∈v v∈A
With y certified to lie in the stage, the fiber conversion ∈-asFiber supplies the representative m' and its identifying path q' from the embedded element back to y. The satisfaction proof for φ at that representative is then assembled inside the truncation: the witness is the pair of v together with its own membership v∈A in the stage, and the two matrix conjuncts are transported to the embedded presentation, v into the embedded mₐ along sym qₐ and the embedded m' into v along sym q'. This is exactly the data the bounded existential asks for.
fib = ∈-asFiber {a = y} {b = Lset σ} y∈A m' = fib .fst q' = fib .snd sat : ⟨ (DefA.ι m' ∷ []) DefA.⊨ᵐ φ ⟩ sat = ∣ (v , v∈A)
The two inclusions assemble into the equation defSet≡, and the recognition principle 𝒟ₒ-intro turns formula and equation into membership of ⋃ (fst a) in 𝒟ₒ (Lset σ). One application of the closure lemma 𝒟ₒ→isL finishes the construction: since σ is an ordinal, a definable subset of Lset σ is constructible, so ⋃ (fst a) enters L packaged as a carrier element together with its certificate. This packaging is what the next block classifies.
, ( subst (λ w → ⟨ v ∈ w ⟩) (sym qₐ) v∈fa , subst (λ w → ⟨ w ∈ v ⟩) (sym q') y∈v ) ∣₁ union∈𝒟ₒ : ⟨ ⋃ (fst a) ∈ 𝒟ₒ (Lset σ) ⟩ union∈𝒟ₒ = 𝒟ₒ-intro (Lset σ) (⋃ (fst a)) ∣ φ , defSet≡ ∣₁ unionElt : S
The specification is a path of truth values, and it is composed from two pieces. The hierarchy's own union law union-spec classifies membership of fst z in the ambient union as an indexed disjunction over all of the hierarchy: some y in fst a with fst z in y. What remains is to turn that ambient indexed disjunction into Q z, which quantifies over the carrier S, that is, over constructible witnesses only. The two quantifier ranges differ, and the bridge of the next block identifies the two truncated disjunctions.
unionElt = ⋃ (fst a) , 𝒟ₒ→isL σ oσ (⋃ (fst a)) union∈𝒟ₒ spec : (z : S) → (z ∈ˢ unionElt) ≡ Q z spec z = union-spec (fst a) (fst z) ∙ bridge where bridge : (∃[ y ∶ (V ℓ) ] (y ∈ fst a) ⊓ (fst z ∈ y)) ≡ Q z
The bridge is a pair of maps between the two truncated disjunctions, joined into a path by ⇔toPath. Forward: an ambient witness y with its two memberships gains a constructibility certificate, precisely because y is a member of fst a, whose own certificate a .snd is in hand; transitivity of the class, here isL-trans applied to the membership of y and the certificate of a, certifies y itself, so the witness may be presented as a carrier element while keeping the memberships. Backward: a carrier witness is projected down to its underlying set, discarding the certificate but keeping the memberships. Neither direction inspects how the truth values are built; both act on abstract Ω values. With the bridge in place, spec is the composite path, and the union field of the model is thereby supplied.
bridge = ⇔toPath (PT.map (λ { (y , py) → (y , isL-trans {x = fst a} {y = y} (py .fst) (a .snd)) , py })) (PT.map (λ { (y , py) → fst y , py })) build : ∥ SetOf Q ∥₁
The assembly mirrors the pairing field. The argument's own certificate a .snd is truncated, and build eliminates it with PT.rec into the truncated existence of a realizing set: at the stage the certificate names, mkUnion runs and produces a witness. The field itself is then one application of the uniqueness principle, mere→uniqueL, which turns a merely existing witness into contractibility data, the form every existence field of the model record takes.
build = PT.rec squash₁ (λ { (σ , (oσ , fa∈)) → ∣ mkUnion σ oσ fa∈ ∣₁ }) (a .snd) hasUnionL : (a : S) → isContr (SetOf (λ x → ∃[ y ∶ S ] (y ∈ˢ a) ⊓ (x ∈ˢ y))) hasUnionL a = mere→uniqueL (UnionOf.Q a) (UnionOf.build a)
Recap
This chapter supplies five axioms for the constructible universe. Extensionality and regularity are inherited: extensionality uses transitivity to reach ambient members, whereas regularity directly restricts ambient accessibility, and once extensionality is available inside the carrier, each remaining axiom reduces to exhibiting a witness, because a set realizing a fixed membership condition is unique. The empty set, pairing, and union are constructed: each is carved from a single stage by a single formula, with the bounding ordinal supplying that stage where two arguments had to meet. The union specification also shows transitivity at work a second time: an ambient witness for membership in the union gains its constructibility certificate exactly by isL-trans, which identifies the restricted witnesses of the model with all witnesses of the ambient union. Alongside the axioms, the chapter records the corresponding placement facts about the tower itself: pair∈Lset-suc puts the unordered pair of two members of a stage in the next stage, sgl∈Lset-suc the singleton, and pr∈Lset-suc the ordered pair two stages up, which is what places anything written with ordered pairs at a stage at all.