---
title: "The basic axioms"
module: L.Axioms.Basic
lang: en
site: "Bedrock"
description: "The basic axioms"
stage: "Constructible stages and the axioms"
reading_order: 31
canonical: https://bedrock.institute/en/L.Axioms.Basic.html
html: L.Axioms.Basic.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Axioms/Basic.lagda.md
prerequisites: [Base.Prelude, FOL.Syntax, FOL.ZFStructure, FOL.ZFModel, V.Hierarchy, V.Model, V.Coding, L.Definability, L.Constructible, L.Ordinal]
routes: [constructible-axioms]
translations: [https://bedrock.institute/zh/L.Axioms.Basic.md, https://bedrock.institute/ja/L.Axioms.Basic.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# The basic axioms

How 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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

```agda
∅∈𝒟ₒ : (σ : 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.

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

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

```agda
∅ʟ : 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.

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

```agda
  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 `⁅_,_⁆`.

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

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

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

```agda
      (∈∈ₛ {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ᵧ`.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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