The constructible hierarchy and universe

The constructible hierarchy starts from the empty set and repeatedly applies definable power set, taking unions at limit points. The resulting stages are transitive, and the tower is monotone along membership of its indices; the sets that appear in some stage form the class L, together with the set-theoretic structure obtained by restricting the ambient one to it.

One design choice does most of the work. The tower is indexed not by a separate type of ordinals but by sets themselves, through the recursion on membership that regularity licensed: Lset α = ⋃ { Def (Lset β) ∣ β ∈ α }. This single equation covers zero, successors, and limits at once, and on von Neumann ordinals it is exactly Gödel's tower; the definition itself accepts arbitrary sets as indices, and the requirement that the index be an ordinal is imposed later, only where the class L is defined. Alongside the tower runs an inductive predicate isLayer, "being a stage", whose constructors are the tower's closure principles; the two views cooperate throughout.

The chapter works at a fixed universe level ℓ inside the cumulative hierarchy V. Its carrier S consists of sets with extensional, well-founded membership. The associated structure reads equality and membership as proposition-valued relations, so expressions such as ⟨ x ∈ˢ A ⟩ denote ordinary types of membership proofs. This is the ambient setting for the constructions below.

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

open import Base.Prelude

module L.Constructible {ℓ : Level} where

open import FOL.ZFStructure using ( ZFStructure; _↾_; module hPropStructure; Transitive )

Three mathematical ingredients drive the construction. First, well-founded recursion on membership: the hierarchy chapter's principle ∈-induction lets a function on sets be defined by recursion along ∈ˢ, which is what the tower itself will be. Second, unions of indexed families, with the two model lemmas that read membership in such a union in each direction. Third, the definability chapter's operator Def A, which collects the subsets of A definable in the inner world (A, ∈) with parameters from A; applied stage by stage, it is what pushes the hierarchy upward. The syntax of first-order formulas, in particular the type Formula, is carried over from the syntax chapter for exactly this operator.

open import FOL.Syntax using ( Formula )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; ∈-induction-compute )
open import V.Model {ℓ} using ( union-family-in; union-family-out )
open import L.Definability {ℓ} using ( module DefOf )

open import Cubical.Foundations.HLevels using ( isProp× )

A set of the hierarchy is presented by a small family, and this chapter reads its members through that presentation: for a set α, ⟪ α ⟫ is the small index type of its members, ⟪ α ⟫↪ embeds an index back into a set, and ∈ₛ⟪ α ⟫↪ m certifies that the member named by m belongs to α. The bridge ∈∈ₛ connects the hierarchy's native membership ∈ with the structural membership ∈ˢ in both directions, and sett X f forms the set whose members are the values of f over X. Alongside these, propositional truncation ∥ _ ∥₁ with its introduction ∣ _ ∣₁ gives mere existence: an inhabitant of a truncated statement asserts that a witness exists, without naming one.

import Cubical.Data.Empty as Empty
import Cubical.Data.Sum as Sum
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )

The basic constructions are available with membership characterizations: the empty set with ∅-empty, unordered pairing with pairing-ax, and binary and indexed unions with union-ax. Propositions at level ℓ-suc ℓ supply the truth values directly, and reading the ambient structure 𝒮ᵥ through hPropStructure yields the notations ⟨ _ ⟩ for the type underlying a proposition and ∈ˢ for structural membership. Every statement of this chapter is phrased in this proposition-valued setting.

open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; ⁅_,_⁆; pairing-ax; ⋃_; union-ax; _∪_ )

With the setting in place, the definable power set operator receives its working name: 𝒟 A is exactly the Def A of the definability chapter, the set of subsets of A definable over the restricted structure with finitely many parameters from A. The mathematical content of that operator, including that its members are subsets of A and that a transitive A satisfies A ⊆ 𝒟 A, was already established there; here it only takes on the short glyph used throughout.

open hPropStructure 𝒮ᵥ

𝒟 : S → S
𝒟 A = DefOf.Def A

Transitive sets

Every stage of the hierarchy is transitive: the empty set is transitive, definable power set preserves transitivity, and unions of transitive sets remain transitive. These closure facts match the constructors used to build layers.

(𝒟 is the book's short glyph for the previous chapter's Def, matching the usual script letter for the operator.)

A set A is transitive when every member of a member of A is again a member of A. The definition isTransV instantiates the structure-level closure condition Transitive 𝒮ᵥ at the class of sets equal to A, so a proof of isTransV A is literally a function taking y ∈ˢ x and x ∈ˢ A to y ∈ˢ A. Note the universe: the statement lives at ℓ-suc ℓ, since it quantifies over the carrier. Transitivity is a proposition, and isPropIsTransV shows this directly: given two proofs p and q, the conclusions y ∈ˢ A are propositions by construction, so they agree pointwise, and cubical function extensionality assembles the pointwise agreement into a path between p and q. The last line announces the first closure fact, for the empty set.

isTransV : S → Type (ℓ-suc ℓ)
isTransV A = Transitive 𝒮ᵥ (λ x → x ∈ˢ A)

isPropIsTransV : (A : S) → isProp (isTransV A)
isPropIsTransV A p q i {x} {y} y∈x x∈A = (y ∈ˢ A) .snd (p y∈x x∈A) (q y∈x x∈A) i

∅-trans : isTransV ∅

The empty set case is vacuous: from x ∈ˢ ∅ one extracts a native member of ∅ via ∈∈ₛ, and ∅-empty derives absurdity from it, so any implication into y ∈ˢ A holds. For the definable power set, two lemmas from the previous chapter combine. A member x of 𝒟 A is a definable subset, hence y ∈ x forces y ∈ A (Def∋⊆A); that is exactly the hypothesis Atr applied to a transitive A, under which A ⊆ 𝒟 A (A⊆Def) puts y into 𝒟 A. Finally ⋃-trans states the union principle: if every member of x is transitive, then so is ⋃ x, the set of all members of members of x.

∅-trans {x} y∈x x∈∅ = Empty.rec (∅-empty x (∈∈ₛ {a = x} {b = ∅} .fst x∈∅))

𝒟-trans : ∀ {A} → isTransV A → isTransV (𝒟 A)
𝒟-trans {A} Atr {x} {y} y∈x x∈𝒟A =
  DefOf.Refine.A⊆Def A Atr y (DefOf.Def∋⊆A A x x∈𝒟A y y∈x)

⋃-trans : (x : S) → ((y : S) → ⟨ y ∈ˢ x ⟩ → isTransV y) → isTransV (⋃ x)

To see a member of the union, one must first see that it is a member at all. The hypothesis u∈⋃x is membership in the ambient hierarchy; ∈∈ₛ in its second direction converts it into the truncated fiber form, and union-ax characterizes such membership: u ∈ ⋃ x holds merely if some w ∈ x has u ∈ w. The truncation is essential: the axiom does not name the intermediate w, it merely asserts that one exists. The proof therefore maps inside the truncation, and in the branch where a pair w , (w∈ₛx , u∈ₛw) is given, the two coercions ∈∈ₛ recover usable hypotheses w∈x and u∈w from the fiber data.

⋃-trans x mem {u} {v} v∈u u∈⋃x =
  ∈∈ₛ {a = v} {b = ⋃ x} .snd (union-ax x v .snd
    (PT.map
      (λ { (w , (w∈ₛx , u∈ₛw)) →
        let w∈x = ∈∈ₛ {a = w} {b = x} .snd w∈ₛx

In that branch the hypothesis mem w w∈x says w is transitive, so v ∈ u and u ∈ w give v ∈ w; coercing back with ∈∈ₛ in the first direction repackages the data as a valid fiber for union-ax, and the elimination of the truncation is legitimate because the target, membership of v in ⋃ x, is a proposition. The binary union follows: A ∪ B is defined as ⋃ ⁅ A , B ⁆, so ∪-trans applies ⋃-trans to the pair, and the remaining obligation is that every member of the pair is transitive, which the local statement prem must supply.

            u∈w = ∈∈ₛ {a = u} {b = w} .snd u∈ₛw
        in w , (w∈ₛx , ∈∈ₛ {a = v} {b = w} .fst (mem w w∈x v∈u u∈w)) })
      (union-ax x u .fst (∈∈ₛ {a = u} {b = ⋃ x} .fst u∈⋃x))))

∪-trans : ∀ {A B} → isTransV A → isTransV B → isTransV (A ∪ B)
∪-trans {A} {B} tA tB = ⋃-trans ⁅ A , B ⁆ prem

The obligation prem asks: for each y in the pair, is y transitive? Pairing characterizes membership merely: y ∈ ⁅ A , B ⁆ holds merely if y is A or y is B, given by propositional truncation rather than a chosen disjunct. The elimination runs into the proposition isTransV y, and each branch carries an equation p identifying y with A or with B; since transitivity is invariant under equality of sets, subst isTransV (sym p) transports the already-known proof tA or tB along that equation to type isTransV y.

  where
  prem : (y : S) → ⟨ y ∈ˢ ⁅ A , B ⁆ ⟩ → isTransV y
  prem y y∈ = PT.rec (isPropIsTransV y)
    (λ { (Sum.inl p) → subst isTransV (sym p) tA
       ; (Sum.inr p) → subst isTransV (sym p) tB })

The last line of prem feeds the truncated membership through pairing-ax, the case analysis is complete, and with it the binary case. The family form setUnion-trans handles a small indexed family at once: given a type X : Type ℓ and a function f : X → S, the set sett X f has as members the values f x, and each f x is transitive by hypothesis. Here too membership in the index set is truncated: the proof receives a pair x , fx≡y, an index together with a path identifying the value with y.

    (pairing-ax A B y .fst (∈∈ₛ {a = y} {b = ⁅ A , B ⁆} .fst y∈))

setUnion-trans : (X : Type ℓ) (f : X → S) → ((x : X) → isTransV (f x))
               → isTransV (⋃ (sett X f))
setUnion-trans X f hf = ⋃-trans (sett X f)
  (λ y → PT.rec (isPropIsTransV y)

Transport again does the bookkeeping: subst isTransV fx≡y (hf x) moves the transitivity proof of f x along the identification to a proof for y, and eliminating the truncation is allowed because isTransV y is a proposition. With these closure principles in place, the empty set, the definable power set, and unions in general, binary, and indexed form, the proof below that every layer is transitive becomes a one-line dispatch: each constructor is matched with the corresponding lemma proved here.

    (λ { (x , fx≡y) → subst isTransV fx≡y (hf x) }))

Ordinals, just the predicate

The indices that matter for the constructible hierarchy are the von Neumann ordinals, and inside a well-founded, extensional universe the classical definition reduces to very little: an ordinal is a transitive set of transitive sets. Well-foundedness and extensionality need not be written into the definition, since the hierarchy guarantees them everywhere; linearity is a classical theorem deferred to later chapters, not part of the notion itself. This chapter records the predicate and its propositionality; the theory of ordinals gets its own chapters when needed.

Thus IsOrd A is the conjunction of two propositions: A is transitive, and every member of A is transitive. The proof isPropIsOrd A combines the propositionality of these two components using closure under products and dependent functions. This certificate is used explicitly in the definition of isL, where (IsOrd α , isPropIsOrd α) supplies the truth value asserting that the stage index is an ordinal.

IsOrd : S → Type (ℓ-suc ℓ)
IsOrd A = isTransV A × ((x : S) → ⟨ x ∈ˢ A ⟩ → isTransV x)

isPropIsOrd : (A : S) → isProp (IsOrd A)
isPropIsOrd A = isProp× (isPropIsTransV A)
                  (isPropΠ λ x → isPropΠ λ _ → isPropIsTransV x)

Layers

isLayer A records closure of the tower by five constructors. The empty set is a layer; applying 𝒟 to a layer gives a layer; and unions are admitted in three forms, from a set all of whose members are layers, from two layers, or from a small indexed family of layers. These are the induction cases available when proving a property of every layer. In particular, each case matches one of the transitivity lemmas from the preceding section.

The predicate is an inductive family indexed by the carrier, and the constructors are read as generation rules for stages. The base case says the empty set is a stage. Closure under 𝒟 says that if A is a stage then so is its definable power set, mirroring the successor step. The general union constructor mirrors the limit step: if x is a set whose members are all, untruncatedly, stages, then ⋃ x is a stage. The binary union constructor covers A ∪ B directly from stage witnesses for A and B. Each constructor mirrors one of the transitivity lemmas of the previous section, with isTransV replaced by isLayer; this parallelism is what makes the next proof immediate.

data isLayer : S → Type (ℓ-suc ℓ) where
  ∅-layer        : isLayer ∅
  𝒟-layer        : ∀ {A} → isLayer A → isLayer (𝒟 A)
  union-layer    : (x : S) → ((y : S) → ⟨ y ∈ˢ x ⟩ → isLayer y) → isLayer (⋃ x)
  union₂-layer   : ∀ {A B} → isLayer A → isLayer B → isLayer (A ∪ B)

The small-indexed family constructor completes the picture: for a type X : Type ℓ and a family f : X → S all of whose values are stages, the union ⋃ (sett X f) is a stage. This is the constructor through which a limit stage can be assembled from the family of earlier stages. Now the induction: to prove layer-trans, that every layer is transitive, one receives the layer as an inductive argument, so the case is determined by its constructor. The empty case is ∅-trans verbatim. The 𝒟 case applies 𝒟-trans, whose premise is the induction hypothesis layer-trans lA for the sublayer.

  setUnion-layer : (X : Type ℓ) (f : X → S)
                 → ((x : X) → isLayer (f x)) → isLayer (⋃ (sett X f))

layer-trans : ∀ {A} → isLayer A → isTransV A
layer-trans ∅-layer = ∅-trans
layer-trans (𝒟-layer {A} lA) = 𝒟-trans {A} (layer-trans lA)

The three union cases dispatch just as directly. The general union case hands the memberwise induction hypothesis to ⋃-trans: the lemma wants, for each member y of x, a transitivity proof for y, and the constructor premise mem supplies exactly that, untruncated, so no elimination of truncation is needed. The binary case is ∪-trans on the two induction hypotheses. The family case is setUnion-trans with the pointwise induction hypothesis. The section thus establishes, by structural recursion alone, that every stage of the tower is a transitive set, the fact used by the transitivity of the class L later in this chapter.

layer-trans (union-layer x mem) = ⋃-trans x (λ y y∈x → layer-trans (mem y y∈x))
layer-trans (union₂-layer lA lB) = ∪-trans (layer-trans lA) (layer-trans lB)
layer-trans (setUnion-layer X f hf) = setUnion-trans X f (λ x → layer-trans (hf x))

The tower

Now the tower itself, defined by recursion on membership. Two technical measures come first. 𝒟 unfolds to a sizable sett over formulas, and the recursion machinery itself unfolds to the accessibility eliminator, so if left exposed both would enter the conversions that follow; opaque makes 𝒟ₒ and the tower opaque, opened only inside blocks that explicitly unfold them, and Lset-compute serves as the tower's declared unfolding. The step takes the union, over the members β of the index α, of 𝒟ₒ applied to the recursive values; the computation rule holds as a propositional path.

The operator is first repackaged as 𝒟ₒ inside an opaque block, so that the elaborate definition of Def stays hidden unless a lemma explicitly asks to unfold it. The step function LsetStep receives an index set α and, for each member β of α, the recursive value rec β; membership here appears through ∈ᵗ, the type-valued reading of the structural membership proposition. The body forms the family that sends a small index m : ⟪ α ⟫ to 𝒟ₒ applied to the recursive value at the member ⟪ α ⟫↪ m named by m, and takes its union. Unfolding the union over the index type, the intended reading is exactly ⋃ { 𝒟ₒ (Lset β) ∣ β ∈ α }, one equation serving zero, successors, and limits alike: for α empty the union is empty, for a successor it repeats the classical next step, and for a limit it collects all earlier stages at once.

opaque
  𝒟ₒ : S → S
  𝒟ₒ A = 𝒟 A

LsetStep : (α : S) → (∀ β → β ∈ᵗ α → S) → S
LsetStep α rec = ⋃ (sett ⟪ α ⟫ (λ m → 𝒟ₒ (rec (⟪ α ⟫↪ m) (mem m))))

The helper mem supplies the conversion the body needs: the member of α named by an index m is ⟪ α ⟫↪ m, and ∈ₛ⟪ α ⟫↪ m certifies that this set belongs to α in the small presentation; ∈∈ₛ converts that into the type-valued membership ∈ᵗ that rec expects. The tower itself is then a single call: Lset is defined as ∈-induction applied to the step. This is well-founded recursion on membership, justified once and for all by the regularity theorem of the hierarchy chapter; the recursion index is the set α itself, and ordinalhood of the index is not required by the raw definition, it will be imposed where the hierarchy is used.

  where
  mem : (m : ⟪ α ⟫) → ⟪ α ⟫↪ m ∈ᵗ α
  mem m = ∈∈ₛ {a = ⟪ α ⟫↪ m} {b = α} .snd (∈ₛ⟪ α ⟫↪ m)

opaque
  Lset : S → S

Both 𝒟ₒ and Lset are wrapped in their own opaque blocks, so the Agda term for either stays abstract during type checking; whatever unfolds inside the recursion machinery, an accessibility eliminator, cannot leak into later conversions. What replaces blind unfolding is a declared computation rule: Lset-compute states, as a propositional path, that Lset α equals the step applied to α with the recursive values λ β _ → Lset β. This is exactly the shape of ∈-induction-compute from the hierarchy chapter instantiated at the step; the equation need not hold definitionally, and stating it explicitly lets later proofs rewrite Lset α by this one controlled equation instead of opening the recursion machinery.

  Lset = ∈-induction LsetStep

opaque
  unfolding Lset
  Lset-compute : (α : S) → Lset α ≡ LsetStep α (λ β _ → Lset β)
  Lset-compute = ∈-induction-compute LsetStep

Every value of the tower is a layer: unfold once with Lset-compute, apply the inductive hypothesis to each member, raise by 𝒟ₒ-layer (the opaque definition unfolds exactly here), and conclude with setUnion-layer that the union of the family is again a layer.

The bridge from the operator to the predicate costs one line. Inside a block that unfolds 𝒟ₒ, the statement 𝒟ₒ-layer is literally the constructor 𝒟-layer, since 𝒟ₒ A computes to 𝒟 A; this is the only place in the chapter that needs to look inside the opaque wrapper, and afterwards every use of the operator can stay abstract. The goal Lset-layer then says that the tower lands entirely inside the inductive predicate: every stage Lset α is a layer. Its proof is itself an application of membership induction, the same principle that defined the tower.

opaque
  unfolding 𝒟ₒ
  𝒟ₒ-layer : ∀ {A} → isLayer A → isLayer (𝒟ₒ A)
  𝒟ₒ-layer = 𝒟-layer

Lset-layer : (α : S) → isLayer (Lset α)

The step function of this induction receives α and the inductive hypothesis IH giving a layer proof for Lset β at each member β of α. Since Lset is opaque, the goal isLayer (Lset α) is not directly matchable against a constructor; it must first be transported. The equation Lset-compute α identifies Lset α with the step's union, and subst isLayer (sym (Lset-compute α)) moves the target along that path in the right direction, so the goal becomes isLayer (⋃ (sett ⟪ α ⟫ (λ m → 𝒟ₒ (Lset (⟪ α ⟫↪ m))))), precisely the family the step function of the tower built.

Lset-layer = ∈-induction step
  where
  step : (α : S) → (∀ β → β ∈ᵗ α → isLayer (Lset β)) → isLayer (Lset α)
  step α IH = subst isLayer (sym (Lset-compute α))
    (setUnion-layer ⟪ α ⟫ (λ m → 𝒟ₒ (Lset (⟪ α ⟫↪ m)))

The remaining obligation fits the family constructor exactly: setUnion-layer wants the family and a layer proof for each of its values. For an index m, the value is 𝒟ₒ at Lset (⟪ α ⟫↪ m), and the induction hypothesis IH applied at that member, converted to type-valued membership by the local mem helper, gives isLayer (Lset (⟪ α ⟫↪ m)); 𝒟ₒ-layer raises it one definable-power-set step. The opaque wrapper of Lset opens only through the declared equation, and the opaque wrapper of 𝒟ₒ only inside 𝒟ₒ-layer, so the whole induction runs at the level of the intended reading of the tower. Combining this with the previous section, every stage is a transitive layer.

      (λ m → 𝒟ₒ-layer (IH (⟪ α ⟫↪ m) (mem m))))
    where
    mem : (m : ⟪ α ⟫) → ⟪ α ⟫↪ m ∈ᵗ α
    mem m = ∈∈ₛ {a = ⟪ α ⟫↪ m} {b = α} .snd (∈ₛ⟪ α ⟫↪ m)

Stages compared

Two more facts about the tower. The first names the operator's membership: 𝒟ₒ A is the set of definable subsets of A, so belonging to it is, by construction, "merely, is some defSet φ", and exhibiting a formula together with an extensional equation is exactly what it takes to place a set inside the operator. The second unfolds the tower once and reads the union both ways: a stage is the union, over the members of its index, of 𝒟ₒ of the earlier stages, so belonging to a stage is exactly belonging to 𝒟ₒ of some earlier stage, stated as two independent directions. Monotonicity then follows as a corollary rather than a separate construction.

Inside a block that unfolds 𝒟ₒ, membership in 𝒟ₒ A reduces to the defining property of Def: a member of 𝒟ₒ A is a subset of A picked out by a formula φ of arity one over the small members of A, with the actual set identified by a path DefOf.defSet A φ ≡ x. Since membership in the ambient hierarchy is truncated, the statement is prefixed by propositional truncation: the claim is merely that such a formula exists, not that one is chosen. The two lemmas below state this equivalence in each direction; here the introduction direction is declared, taking the truncated defining data to membership.

opaque
  unfolding 𝒟ₒ
  𝒟ₒ-intro : (A x : S)
           → ∥ Σ[ φ ∈ Formula ⟪ A ⟫  ] (DefOf.defSet A φ ≡ x) ∥₁
           → ⟨ x ∈ˢ 𝒟ₒ A ⟩

The proof body is the identity in both directions: once 𝒟ₒ is unfolded, an element of the truncated defining data already is a member, and conversely the inversion lemma 𝒟ₒ-inv returns a membership as the same truncated data. So the pair 𝒟ₒ-intro and 𝒟ₒ-inv is exactly the interface described just above: reading DefOf.defSet at a stage as a map from formulas, and recovering a member's defining formula by inversion. Both work at the level of mere existence, so no canonical formula is ever chosen; a member of 𝒟ₒ A merely is some definable subset, and that is all these two directions say.

  𝒟ₒ-intro A x p = p

  𝒟ₒ-inv : (A x : S) → ⟨ x ∈ˢ 𝒟ₒ A ⟩
         → ∥ Σ[ φ ∈ Formula ⟪ A ⟫  ] (DefOf.defSet A φ ≡ x) ∥₁
  𝒟ₒ-inv A x p = p

Two further facts make the tower usable in later arguments. The first names the operator's membership: 𝒟ₒ A is the set of definable subsets of A, so belonging to it is, by construction, "merely, is some defSet φ", and exhibiting a formula together with an extensional equation is exactly what it takes to place a set inside the operator. The second unfolds the tower once and reads the union both ways: a stage is the union, over the members of its index, of 𝒟ₒ of the earlier stages, so belonging to a stage is exactly belonging to 𝒟ₒ of some earlier stage, stated as two independent directions since that is how proofs consume it. Monotonicity then follows as a corollary rather than a separate construction.

The first lemma is the inclusion of a stage in its own definable power set: since Lset-layer β says the stage Lset β is a layer and layer-trans makes it transitive, the refinement bound A⊆Def of the definability chapter applies verbatim, giving x ∈ Lset β ⟹ x ∈ 𝒟ₒ (Lset β). Its dual 𝒟ₒ∋⊆ restates that the operator only refines: every member of 𝒟ₒ A is a subset of A, so a member of a member is still in A. Finally stageFam names the family underlying the tower's step: for an index m in the small presentation of α, the corresponding stage is 𝒟ₒ at Lset of the member named by m.

  Lset⊆𝒟ₒ : (β x : S) → ⟨ x ∈ˢ Lset β ⟩ → ⟨ x ∈ˢ 𝒟ₒ (Lset β) ⟩
  Lset⊆𝒟ₒ β x = DefOf.Refine.A⊆Def (Lset β) (layer-trans (Lset-layer β)) x

  𝒟ₒ∋⊆ : (A x : S) → ⟨ x ∈ˢ 𝒟ₒ A ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ A ⟩
  𝒟ₒ∋⊆ A = DefOf.Def∋⊆A A

stageFam : (α : S) → ⟪ α ⟫ → S

Now the characterization of stage membership from above. Lset-in says: if δ is a member of α and x lies in 𝒟ₒ (Lset δ), then x already lies in Lset α. The proof rewrites Lset α once by its computation rule, so the goal becomes membership in the union ⋃ (sett ⟪ α ⟫ (stageFam α)), and then invokes union-family-in, the model lemma which takes an index i and a member x of f i and returns a member of the indexed union. The index supplied is fib .fst, an element of ⟪ α ⟫ naming the member δ.

stageFam α m = 𝒟ₒ (Lset (⟪ α ⟫↪ m))

Lset-in : (α δ x : S) → ⟨ δ ∈ˢ α ⟩ → ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩ → ⟨ x ∈ˢ Lset α ⟩
Lset-in α δ x δ∈α x∈𝒟ₒδ =
  subst (λ w → ⟨ x ∈ˢ w ⟩) (sym (Lset-compute α))
    (union-family-in ⟪ α ⟫ (stageFam α) (fib .fst) x

The name fib abbreviates a fiber computation: the structural membership δ∈α is truncated, and ∈-asFiber converts it into a fiber of the embedding ⟪ α ⟫↪, that is, a pair of an index i with ⟪ α ⟫↪ i ≡ δ. Inside the proof this identification is transported along: x∈𝒟ₒδ speaks of Lset δ, but union-family-in needs a member of stageFam α (fib .fst), which equals 𝒟ₒ (Lset (⟪ α ⟫↪ (fib .fst))), so subst moves the hypothesis across the path sym (fib .snd). The truncated origin of δ∈α never matters here, because a fiber representation was actually constructed from it by ∈-asFiber.

      (subst (λ δ → ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩) (sym (fib .snd)) x∈𝒟ₒδ))
  where
  fib = ∈-asFiber {a = δ} {b = α} δ∈α

Lset-out : (α x : S) → ⟨ x ∈ˢ Lset α ⟩
         → ∥ Σ[ δ ∈ S ] (⟨ δ ∈ˢ α ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩) ∥₁

The downward direction Lset-out cannot avoid truncation, and states it honestly: a member x of Lset α merely comes from some predecessor, that is, merely there is a δ with δ ∈ α and x ∈ 𝒟ₒ (Lset δ). The proof again rewrites Lset α by the computation rule, applies union-family-out to get merely an index m of ⟪ α ⟫ with x in the family value at m, and maps inside the truncation: the pair (m , hx) becomes the stage ⟪ α ⟫↪ m, its structural membership in α via ∈∈ₛ, and hx. The result is a truncated witness precisely because the union axiom names no canonical predecessor; the construction of one inside the branch is local data, not a chosen function.

Lset-out α x x∈Lα = PT.map
  (λ { (m , hx) → ⟪ α ⟫↪ m
    , (∈∈ₛ {a = ⟪ α ⟫↪ m} {b = α} .snd (∈ₛ⟪ α ⟫↪ m) , hx) })
  (union-family-out ⟪ α ⟫ (stageFam α) x
    (subst (λ w → ⟨ x ∈ˢ w ⟩) (Lset-compute α) x∈Lα))

Monotonicity is now a two-line corollary of the characterization rather than a separate construction. If β ∈ α and x ∈ Lset β, then Lset⊆𝒟ₒ first lifts x into 𝒟ₒ (Lset β), using that stages are transitive, and Lset-in with the inclusion β ∈ α carries it into Lset α. Note the strict form: what monotonicity requires is that β is a member of α, not merely a subset, matching how the tower grows by taking the union over members.

Lset-mono : {α β : S} → ⟨ β ∈ˢ α ⟩ → {x : S} → ⟨ x ∈ˢ Lset β ⟩ → ⟨ x ∈ˢ Lset α ⟩
Lset-mono {α} {β} β∈α {x} x∈Lβ = Lset-in α β x β∈α (Lset⊆𝒟ₒ β x x∈Lβ)

The class L, and its structure

A set is constructible when some ordinal stage of the tower contains it. The ordinal bound is part of the definition on purpose: the later theory extracts stage ordinals, and this shape yields them by construction. Note that ordinality is imposed here, at the point of definition; the tower Lset itself accepts arbitrary sets as indices. L is a transitive class: stages are transitive, and the witnessing ordinal does not move.

The class is a truth value, not a subtype: isL x is defined as the indexed disjunction ∃[ x ] P x over all sets α of the conjunction of IsOrd α with x ∈ˢ Lset α. So an element of isL x is, by the meaning of indexed disjunction, merely a pair of an ordinal α and a membership of x in stage α; no canonical stage is attached to a constructible set. The quantifier ranges over the whole carrier, so a witness is available only in this merely-exists form; treating the class as a proposition-valued predicate is what allows it to be restricted into a structure shortly.

isL : S → hProp (ℓ-suc ℓ)
isL x = ∃[ α ∶ S ] ((IsOrd α , isPropIsOrd α) ⊓ (x ∈ˢ Lset α))

isL-trans : Transitive 𝒮ᵥ isL
isL-trans {x} {y} y∈x x∈L = PT.rec (snd (isL y))
  (λ { (α , (ordα , x∈Lα)) →

Transitivity of the class is now immediate from the closure of the stages. Given y ∈ x and an element of isL x, eliminate the truncation into the proposition isL y: the witness is a pair (α , ordα , x∈Lα), and since the stage Lset α is a transitive set by layer-trans (Lset-layer α), the two hypotheses y∈x and x∈Lα yield y ∈ Lset α. The same ordinal α re-certifies the conclusion, so the class is closed under members of members. The conclusion is re-truncated with ∣ _ ∣₁ because the target isL y is itself a truncated existential, not because any choice had to be undone.

    ∣ α , (ordα , layer-trans (Lset-layer α) y∈x x∈Lα) ∣₁ })
  x∈L

Sitting in an ordinal stage is the definition, so the bridge in that direction is the constructor itself. Giving the bridge a name simply makes it convenient to cite.

Given an ordinal witness oα for the stage α and a membership x∈Lα, the proof packages the three components, the ordinal, its ordinality, and the membership, into a single propositionally truncated pair. Nothing is computed; the content of the lemma is that the existential in the definition of isL x is witnessed by exactly the data at hand. Note the direction of trust: the lemma takes the ordinality of α as a hypothesis, since Lset as defined accepts arbitrary sets as indices and it is the caller who must know that the chosen index really is an ordinal.

Lset→isL : (α : S) → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ isL x ⟩
Lset→isL α oα x x∈Lα = ∣ α , (oα , x∈Lα) ∣₁

The final construction views the constructible class as a structure. Restricting 𝒮ᵥ to the proposition-valued class isL gives 𝒮ʟ: its elements are sets equipped with constructibility proofs, and equality and membership are inherited through the restriction. This supplies the structure in which later formulas about L are interpreted; proving that it is a model of ZFC requires the separate axiom arguments that follow.

One line suffices. The restriction _↾_ takes the ambient structure and the class isL, and forms the structure whose elements are pairs of a set with a proof that it satisfies isL; equality and membership are read along the first projection, so they agree with the ambient ones. Since isL is an hProp truth value and the class was proved transitive, the restricted structure is well-defined in the same framework. What remains open, and is the subject of the following chapters, is whether this structure satisfies the ZF and ZFC axioms; the restriction itself asserts nothing about that.

𝒮ʟ : ZFStructure (ℓ-suc ℓ)
𝒮ʟ = 𝒮ᵥ ↾ isL

Recap

The tower Lset is defined by membership recursion, and isLayer records closure under the definability operation and the three union constructions. Structural recursion with the corresponding lemmas proves layer-trans. A set is in isL when it merely belongs to Lset α for some ordinal α; this class is transitive, and restricting the ambient structure to it gives 𝒮ʟ. The remaining task is to prove, axiom by axiom, that this structure satisfies ZFC.