---
title: "Counting a Skolem hull from a counted start"
module: L.GCH.HullCounting
lang: en
site: "Bedrock"
description: "Counting a Skolem hull from a counted start"
stage: "Proving GCH"
reading_order: 117
canonical: https://bedrock.institute/en/L.GCH.HullCounting.html
html: L.GCH.HullCounting.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/HullCounting.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Axioms.Full, L.Axioms.Infinity, L.Axioms.Numerals, L.Coding.Model, L.Coding.Expressions, L.Coding.CodeConstructibility, L.Coding.Injection, L.Cardinal, L.InjectionComposition, L.DefinableInjection, L.GCH.LeastWitnessMap, L.GCH.CardinalSquareLaw, L.Stage, L.Coding.EnvironmentSet, L.GCH.AdequateStages, L.Coding.SatisfactionGraphSet, L.GCH.SkolemHull, L.GCH.ConstructibleHull, L.GCH.StageCountingTools, L.GCH.FiniteSequenceCoding]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/zh/L.GCH.HullCounting.md, https://bedrock.institute/ja/L.GCH.HullCounting.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
Closing a small set under definable least witnesses should preserve an infinite cardinal bound. This chapter proves inside `L` that if the starting set injects into an infinite cardinal, then so does its Skolem hull.

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

Excluded middle supplies local decisions such as whether a member of a union lies in its left summand. Classical reasoning enters through one explicit hypothesis, so the resulting bound records exactly that assumption.

```agda
open import Base.Prelude
open import Base.Classical using ( LEM )
```

Fix a universe level `ℓ` and excluded middle for propositions at level `ℓ-suc ℓ`. The internal sets, coded graphs, and truncated witnesses are all formed relative to this fixed instance.

```agda
module L.GCH.HullCounting {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

Coded graphs are expressed in the first-order language of equality and membership. Conjunction, disjunction, negation, and existential quantification describe their cases, while satisfaction is interpreted over the ambient cumulative hierarchy.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ¬̇_; ∃̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

The argument moves between ordinal stages and their constructible members. Transitivity keeps members inside `L`, while ordinal membership and stage cumulativity place each object in a stage large enough for definable selection.

```agda
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-layer; layer-trans )
open import L.Ordinal {ℓ} using ( mem-ord; #∈ω )
open import L.Ordinal.Stages {ℓ} lem using ( Lset-cumul; ord∈Lset-suc )
```

The counting maps must themselves be sets of `L`. Separation constructs subgraphs, pairing and union build their codes, and adequacy connects the internal formulas for application, single-valuedness, and domains with their set-theoretic meanings.

```agda
open import L.Axioms.Basic {ℓ} using ( LsetS; ∅ʟ )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Axioms.Numerals {ℓ} using ( pairʟ; unionʟ )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; appAt; appAt-adequate; svAt-out; domAt-in )
```

An internal injection is witnessed by a constructible graph with exact domain, single-valuedness, injectivity, and a range bound. `InjCode` retains a particular graph, whereas `InjL` retains only the proposition that one exists.

```agda
open import L.Coding.Expressions {ℓ} using ( numL; tagAtL; tagAtL-adequate )
open import L.Coding.CodeConstructibility {ℓ}
  using ( sglʟ; sglʟ-in; sglʟ-out; cupʟ; cupʟ-inl; cupʟ-inr; cupʟ-out )
open import L.Coding.Injection {ℓ} lem using ( injAt-out; module Extract )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
```

The counting proof composes internal injections. Definable maps turn formulas with unique values into constructible graphs, least-witness selection supplies such maps for Skolem closure, and the internal product provides room for tagged pairs.

```agda
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
open import L.GCH.LeastWitnessMap {ℓ} lem using ( module Least )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( prodL; prodL-in; module Relation )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )
```

Least witnesses are selected inside a common constructible stage. Bounding ordinals collect the parameters there, superadequacy stabilizes satisfaction, and the satisfaction graph records the choices as a set of `L`.

```agda
open import L.Stage {ℓ} lem using ( LeastOrd; isPropLeastOrd; leastOrd; stage; stage-ord; stage-mem )
open import L.Ordinal using ( boundingOrd )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet; envSet-in )
open import L.GCH.AdequateStages {ℓ} lem using ( Superadequate )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )
```

The Skolem hull is obtained by iterating least-witness closure from the starting set. Its constructible presentation supplies stage bounds for selection, while condensation identifies the hull with the corresponding constructible structure.

```agda
open import L.GCH.SkolemHull {ℓ} lem using ( module Frame; module HullStage )
open import L.GCH.ConstructibleHull {ℓ} lem using ( module Condense′; module Telescope )
open import L.GCH.StageCountingTools {ℓ} lem
  using ( isPropInjCode; injcode-resp; injFo; module InjFo; pinAt; pin-in; pin-out; seq-map; Lω
        ; limit-stage-counted )
```

Each closure step is indexed by a formula code and a finite parameter sequence. Formula shapes are countable, finite sequences over an infinite cardinal are bounded by the square law, and well-founded induction supplies that law for the internal cardinals in the count.

```agda
open import L.GCH.FiniteSequenceCoding {ℓ} lem using ( seqL; seqL-in; seq-count )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( prod-inj; ω⊆; Goal; module Step )
open import L.Cardinal {ℓ} lem using ( IsCardinalL )
open import V.Hierarchy {ℓ} using ( regularityV )
import Cubical.Induction.WellFounded as WF
```

When both arguments of a graph are identified by equalities, two-place transport moves a graph-membership proof across both identifications at once. Thus equality replacement remains compatible with the coded relation.

```agda
open import Cubical.Foundations.Prelude using ( subst2 )
```

The tags `0` and `1` are distinct, making the two branches of a tagged injection disjoint. Equality of dependent pairs with proposition-valued fibers reduces to equality of their first components, so constructibility proofs do not affect the count.

```agda
open import Cubical.Data.Nat.Properties using ( znots; snotz )
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.HLevels using ( isProp×; isSetΣSndProp )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
```

Von Neumann numerals provide the tags, `ω` collects them, and successor describes their finite progression. The empty set serves as the value of a singleton injection, while propositional truncation records existence without choosing a representative.

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; ω; sucV )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅ )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
```

Existence of a coded injection is propositionally truncated because the count depends only on whether a witnessing graph exists. Elimination is therefore made only into propositions, preserving independence from the choice of graph.

```agda
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

For ambient sets, `x ∈ˢ y` is the proposition that `x` belongs to `y`. The domain and range clauses of coded functions ultimately reduce to this relation on underlying sets.

```agda
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
```

Write `S` for the carrier of the constructible model. Its elements are ambient sets paired with proofs of membership in `L`; since those proofs are propositions, the underlying set determines the constructible element up to equality.

```agda
module SL = hPropStructure 𝒮ʟ using ( S )
open SL using ( S )
```

A formula with constructible constants can be evaluated inside `L` and projected to the ambient hierarchy. Transitivity makes the two readings agree, so an internally proved graph statement can be used as ordinary membership between underlying sets.

```agda
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
```

`Holds F x y` means that the ordered pair of the underlying sets of `x` and `y` belongs to the underlying graph `F`. This is the ambient relation represented by every coded application formula in the argument.

```agda
Holds : S → S → S → Type (ℓ-suc ℓ)
Holds F x y = ⟨ pr (fst x) (fst y) ∈ fst F ⟩
```

The element `nn k : S` is the ambient von Neumann numeral `# k` together with its constructibility proof. In particular, `nn 0` and `nn 1` serve as internal tags without leaving `L`.

```agda
nn : ℕ → S
nn k = # k , numL k
```

If two elements of `S` have equal underlying sets, then the elements themselves are equal. The second components contain only constructibility proofs, so proof irrelevance lifts equality of the first components to equality of the dependent pairs.

```agda
S≡ : {x y : S} → fst x ≡ fst y → x ≡ y
S≡ = Σ≡Prop (λ v → snd (isL v))
```

The carrier `S` is an h-set. Its first component lies in the cumulative hierarchy, which is an h-set, and each fiber of constructibility proofs is a proposition; hence every equality type in `S` is a proposition.

```agda
isSetS : isSet S
isSetS = isSetΣSndProp setIsSet (λ v → snd (isL v))
```

De Bruijn indices for the first two variable slots are named, since the coded formulas of this chapter never mention more than eight slots at once.

```agda
private
  i0 : ∀ {k} → Fin (suc k)
  i0 = zero
  i1 : ∀ {k} → Fin (suc (suc k))
  i1 = suc i0
```

The names `i2`, `i3`, and `i4` denote variable positions two, three, and four. Each is one successor beyond the preceding index, with a polymorphic tail `k` keeping the position valid when more variables are available.

```agda
  i2 : ∀ {k} → Fin (suc (suc (suc k)))
  i2 = suc i1
  i3 : ∀ {k} → Fin (suc (suc (suc (suc k))))
  i3 = suc i2
  i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))
```

After the defining equation for `i4`, the same successor pattern defines positions five and six. These names make the shifts caused by nested binders visible in the types of coded formulas.

```agda
  i4 = suc i3
  i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k))))))
  i5 = suc i4
  i6 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc k)))))))
  i6 = suc i5
```

Slot seven is the last, and the eight indices cover every variable position used in this chapter.

```agda
  i7 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc k))))))))
  i7 = suc i6
```

An ordinal is contained in its own stage: each member of an ordinal is itself an ordinal, and the cumulative construction places every member of the ordinal into the stage indexed by that ordinal.

```agda
ord⊆Lset : (α : V ℓ) → IsOrd α → (z : V ℓ) → ⟨ z ∈ α ⟩ → ⟨ z ∈ Lset α ⟩
ord⊆Lset α oα z z∈α =
  Lset-cumul z α oz oα z∈α (ord∈Lset-suc z oz)
  where
  oz : IsOrd z
```

Since `z ∈ α` and `α` is an ordinal, `z` is itself an ordinal. This places `z` in its successor stage; cumulativity along `z ∈ α` then gives `z ∈ Lset α`.

```agda
  oz = mem-ord {A = α} oα z z∈α
```

Fix constructible sets `D₁` and `D₂`. Their internal binary union is the common domain for combining two injections; its membership principle gives both inclusions and a truncated case split.

```agda
module Union2 (D₁ D₂ : S) where
```

The union is the internal union of the two sets.

```agda
  D : S
  D = cupʟ D₁ D₂
```

Left members are included by the left rule of the union.

```agda
  in₁ : (z : S) → ⟨ fst z ∈ fst D₁ ⟩ → ⟨ fst z ∈ fst D ⟩
  in₁ z = cupʟ-inl D₁ D₂ (fst z)
```

Right members are included symmetrically.

```agda
  in₂ : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → ⟨ fst z ∈ fst D ⟩
  in₂ z = cupʟ-inr D₁ D₂ (fst z)
```

If `z ∈ D₁ ∪ D₂`, then it merely belongs to the left side or the right side. The disjunction is propositionally truncated because membership retains that some presentation index names `z`, but not which index supplied it.

```agda
  out : (z : S) → ⟨ fst z ∈ fst D ⟩ → ∥ ⟨ fst z ∈ fst D₁ ⟩ ⊎ ⟨ fst z ∈ fst D₂ ⟩ ∥₁
  out z = cupʟ-out D₁ D₂ (fst z)
```

Let `κ` be a constructible set containing the tags `0` and `1`, and let `E₁` and `E₂` code injections from `D₁` and `D₂` into `κ`. Tagging their values combines them into an injection from `D₁ ∪ D₂` into `κ × κ`. This construction requires no ordinal hypothesis on `κ`.

```agda
module TagUnion (κ : S) (0∈κ : ⟨ # 0 ∈ fst κ ⟩) (1∈κ : ⟨ # 1 ∈ fst κ ⟩)
                (D₁ D₂ E₁ E₂ : S) (c₁ : InjCode E₁ D₁ κ) (c₂ : InjCode E₂ D₂ κ) where
```

Write `D = D₁ ∪ D₂`. A member of either summand belongs to `D`, and every member of `D` yields a truncated proof that it comes from one of the two summands.

```agda
  open Union2 D₁ D₂ public using ( D; in₁; in₂; out )
```

Each coded injection extracts its underlying function together with the proof that its graph holds exactly when the coding says so.

```agda
  module X₁ = Extract E₁ D₁ (fst c₁) (fst (snd c₁)) using ( toFun; toFun-graph )
  module X₂ = Extract E₂ D₂ (fst c₂) (fst (snd c₂)) using ( toFun; toFun-graph )
```

`Mem z` is the proposition that `z` belongs to the union domain `D`. Carrying this proof with an input supplies exactly the domain evidence needed to evaluate the piecewise function.

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem z = ⟨ fst z ∈ fst D ⟩
```

Membership in the left domain is decidable by excluded middle, and the decision is the case split the tagged injection is built on.

```agda
  Case : S → Type (ℓ-suc ℓ)
  Case z = ⟨ fst z ∈ fst D₁ ⟩ ⊎ (⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥)
```

Excluded middle decides, for every member of the union, whether it came from the left domain.

```agda
  decide : (z : S) → Case z
  decide z = lem (fst z ∈ fst D₁)
```

A member outside the left domain must lie in the right domain: the union membership splits into the two sides, and the left side contradicts the assumed failure.

```agda
  off : (z : S) → Mem z → (⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥) → ⟨ fst z ∈ fst D₂ ⟩
  off z m no = PT.rec (snd (fst z ∈ fst D₂))
    (λ { (inl h) → Empty.rec (no h) ; (inr h) → h }) (out z m)
```

The value on each side is the tagged image: the numeral tag zero or one paired with the extracted function value, so the two injections land in disjoint tagged ranges.

```agda
  val : (z : S) → Mem z → Case z → S
  val z m (inl h)  = prʟ (nn 0) (X₁.toFun (z , h))
  val z m (inr no) = prʟ (nn 1) (X₂.toFun (z , off z m no))
```

For `z ∈ D`, the function `fn` decides whether `z ∈ D₁`. It returns `(0,E₁(z))` in the left case and `(1,E₂(z))` in the complementary right case.

```agda
  fn : (z : S) → Mem z → S
  fn z m = val z m (decide z)
```

The ambient meaning `Wit y z` has two branches. In the left branch, `z ∈ D₁`, and there merely exists `v` with `(z,v) ∈ E₁` such that the underlying set of `y` is `(0,v)`.

```agda
  Wit : (y z : S) → Type (ℓ-suc ℓ)
  Wit y z =
      (⟨ fst z ∈ fst D₁ ⟩
        × ∥ Σ[ v ∈ S ] (Holds E₁ z v × (fst y ≡ pr (# 0) (fst v))) ∥₁)
    ⊎ ((⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥)
```

In the right branch, `z ∉ D₁`, and there merely exists `v` with `(z,v) ∈ E₂` such that `y = (1,v)` on underlying sets. The distinct tags rule out equality between outputs from opposite branches.

```agda
        × ∥ Σ[ v ∈ S ] (Holds E₂ z v × (fst y ≡ pr (# 1) (fst v))) ∥₁)
```

The graph is written as a two-slot formula: membership in `D₁` conjoined with an existential over the first code, or the negation of that membership conjoined with an existential over the second code. Inside the existential, the injected value and the tag equation are atoms of the coding.

```agda
  opaque
    fo : Formula S 2
    fo = ((var i1 ∈̇ con D₁) ∧̇ ∃̇ (appC E₁ i2 i0 ∧̇ tagAtL i1 0 i0))
       ∨̇ ((¬̇ (var i1 ∈̇ con D₁)) ∧̇ ∃̇ (appC E₂ i2 i0 ∧̇ tagAtL i1 1 i0))
```

Reading the two coding atoms uses their adequacy lemmas: satisfaction of the application atom becomes a membership `Holds E z v`, and satisfaction of the tag atom becomes the equation between `y` and the tagged pair.

```agda
    private
      rd : (E : S) (k : ℕ) (y z v : S)
         → ⟨ (v ∷ y ∷ z ∷ []) ⊨ appC E i2 i0 ⟩ → ⟨ (v ∷ y ∷ z ∷ []) ⊨ tagAtL i1 k i0 ⟩
         → Holds E z v × (fst y ≡ pr (# k) (fst v))
      rd E k y z v ha ht =
```

After transport along the two adequacy equivalences, the satisfaction witnesses become the components required by `Wit`: graph membership `Holds E z v` and the equality identifying `y` with the pair tagged by `k`.

```agda
          subst ⟨_⟩ (appC-adequate E i2 i0 (v ∷ y ∷ z ∷ [])) ha
        , subst ⟨_⟩ (tagAtL-adequate i1 k i0 (v ∷ y ∷ z ∷ [])) ht
```

Conversely, from `Holds E z v` and the underlying equality `y = (k,v)`, transport backward along adequacy produces satisfaction of the application atom.

```agda
      wr : (E : S) (k : ℕ) (y z v : S)
         → Holds E z v → fst y ≡ pr (# k) (fst v)
         → ⟨ (v ∷ y ∷ z ∷ []) ⊨ appC E i2 i0 ⟩ × ⟨ (v ∷ y ∷ z ∷ []) ⊨ tagAtL i1 k i0 ⟩
      wr E k y z v ha ht =
          subst ⟨_⟩ (sym (appC-adequate E i2 i0 (v ∷ y ∷ z ∷ []))) ha
```

The same backward transport turns the tagged-pair equality into satisfaction of the tag atom. Together the two proofs reconstruct the conjunction under the existential quantifier.

```agda
        , subst ⟨_⟩ (sym (tagAtL-adequate i1 k i0 (v ∷ y ∷ z ∷ []))) ht
```

Reading a satisfaction proof of `fo` proceeds by its two disjuncts. The left yields `z ∈ D₁` and a truncated `E₁` witness tagged by zero; the right yields `z ∉ D₁` and the corresponding `E₂` witness tagged by one. Applying `rd` inside each truncation gives a truncated inhabitant of `Wit y z`.

```agda
    fo-out : (y z : S) → ⟨ (y ∷ z ∷ []) ⊨ fo ⟩ → ∥ Wit y z ∥₁
    fo-out y z = PT.map
      (λ { (inl (h , hv)) → inl (h , PT.map (λ { (v , (ha , ht)) → v , rd E₁ 0 y z v ha ht }) hv)
         ; (inr (h , hv)) → inr ((λ z∈ → lower (h z∈))
             , PT.map (λ { (v , (ha , ht)) → v , rd E₂ 1 y z v ha ht }) hv) })
```

The inward reading of the graph turns the host-side witness into satisfaction, case by case. In the left case the membership and the truncated entry are transported through the adequacy equations of the application and tag codings; the right case does the same after lifting the refutation of membership into the object-language negation.

```agda
    fo-in : (y z : S) → Wit y z → ⟨ (y ∷ z ∷ []) ⊨ fo ⟩
    fo-in y z (inl (h , hv)) =
      ∣ inl (h , PT.map (λ { (v , (ha , ht)) → v , wr E₁ 0 y z v ha ht }) hv) ∣₁
    fo-in y z (inr (h , hv)) =
      ∣ inr ((λ z∈ → lift (h z∈))
```

The tail of the right case completes the second disjunct: the entry of `E₂` is transported exactly as in the left, with the tag `1` in place of `0`. Both disjuncts are then injected into the truncated existence, and the introduction is finished.

```agda
          , PT.map (λ { (v , (ha , ht)) → v , wr E₂ 1 y z v ha ht }) hv) ∣₁
```

Each coded relation is single-valued: two entries with the same first component have the same second component. This is the first conjunct of the injection code, read out through the adequacy of the application coding.

```agda
  private
    sv₁ : (x y y' : S) → Holds E₁ x y → Holds E₁ x y' → fst y ≡ fst y'
    sv₁ = svAt-out zero (E₁ ∷ D₁ ∷ []) (fst c₁)
    sv₂ : (x y y' : S) → Holds E₂ x y → Holds E₂ x y' → fst y ≡ fst y'
    sv₂ = svAt-out zero (E₂ ∷ D₂ ∷ []) (fst c₂)
```

Each coded relation is also injective: two entries with the same second component have first components with equal underlying sets. The range clause begins the list: every value of the relation lies in the cardinal.

```agda
    ij₁ : (y x x' : S) → Holds E₁ x y → Holds E₁ x' y → fst x ≡ fst x'
    ij₁ = injAt-out zero (E₁ ∷ D₁ ∷ []) (fst (snd (snd c₁)))
    ij₂ : (y x x' : S) → Holds E₂ x y → Holds E₂ x' y → fst x ≡ fst x'
    ij₂ = injAt-out zero (E₂ ∷ D₂ ∷ []) (fst (snd (snd c₂)))
    ran₁ : (x y : S) → Holds E₁ x y → ⟨ fst y ∈ fst κ ⟩
```

The second range clause completes the data extracted from the two injection codes. For each relation we now have single-valuedness, injectivity, and the fact that every value lies in `κ`; these are the properties used to build the tagged map.

```agda
    ran₁ = snd (snd (snd c₁))
    ran₂ : (x y : S) → Holds E₂ x y → ⟨ fst y ∈ fst κ ⟩
    ran₂ = snd (snd (snd c₂))
```

The witness is constructed from the two cases for a member. If `z ∈ D₁`, its value uses the function extracted from `E₁`; otherwise it uses the function extracted from `E₂` at the resulting member of `D₂`. In either case the extraction supplies both the graph entry and the equation identifying the tagged pair with the chosen value.

```agda
  wit : (z : S) (m : Mem z) (c : Case z) → Wit (val z m c) z
  wit z m (inl h)  = inl (h , ∣ X₁.toFun (z , h)
    , (X₁.toFun-graph (z , h) , prʟ-fst (nn 0) (X₁.toFun (z , h))) ∣₁)
  wit z m (inr no) = inr (no , ∣ X₂.toFun (z , off z m no)
    , (X₂.toFun-graph (z , off z m no) , prʟ-fst (nn 1) (X₂.toFun (z , off z m no))) ∣₁)
```

Uniqueness in the left case composes three equations: the entry's second component equals the value named by the truncated witness; single-valuedness of `E₁` identifies the two function values; and the pair's first-projection equation says the value is exactly the tagged entry.

```agda
  only : (z : S) (m : Mem z) (c : Case z) (y : S) → Wit y z → fst y ≡ fst (val z m c)
  only z m (inl h) y (inl (_ , hv)) = PT.rec (setIsSet _ _)
    (λ { (v , (hg , hy)) →
       hy ∙ cong (pr (# 0)) (sv₁ z v (X₁.toFun (z , h)) hg (X₁.toFun-graph (z , h)))
          ∙ sym (prʟ-fst (nn 0) (X₁.toFun (z , h))) }) hv
```

The mixed cases are refuted outright: a member inside `D₁` cannot carry a witness recorded off `D₁`, and conversely. The right-right case is then handled exactly as the left, with `E₂`, the tag `1`, and the off-set function value.

```agda
  only z m (inl h) y (inr (no , _)) = Empty.rec (no h)
  only z m (inr no) y (inl (h , _)) = Empty.rec (no h)
  only z m (inr no) y (inr (_ , hv)) = PT.rec (setIsSet _ _)
    (λ { (v , (hg , hy)) →
       hy ∙ cong (pr (# 1)) (sv₂ z v (X₂.toFun (z , off z m no)) hg (X₂.toFun-graph (z , off z m no)))
```

The final equation composes the tag identification with the pair's first-projection equation, completing uniqueness. The witness thus determines its value in both cases.

```agda
          ∙ sym (prʟ-fst (nn 1) (X₂.toFun (z , off z m no))) }) hv
```

The value lands in the internal product: the pair of the numeral `0` or `1` with the function value is presented through its first projection equation, and `prodL-in` admits it because both numerals lie in `κ` and the function value lies in `κ` by the range clause.

```agda
  into : (z : S) (m : Mem z) (c : Case z) → ⟨ fst (val z m c) ∈ˢ fst (prodL κ) ⟩
  into z m (inl h) = subst (λ w → ⟨ w ∈ˢ fst (prodL κ) ⟩) (sym (prʟ-fst (nn 0) (X₁.toFun (z , h))))
    (prodL-in κ (nn 0) (X₁.toFun (z , h)) 0∈κ (ran₁ z (X₁.toFun (z , h)) (X₁.toFun-graph (z , h))))
  into z m (inr no) = subst (λ w → ⟨ w ∈ˢ fst (prodL κ) ⟩) (sym (prʟ-fst (nn 1) (X₂.toFun (z , off z m no))))
    (prodL-in κ (nn 1) (X₂.toFun (z , off z m no)) 1∈κ
```

The right case supplies the range fact from `E₂` and the numeral `1`, completing the membership of both tagged values in the product.

```agda
      (ran₂ z (X₂.toFun (z , off z m no)) (X₂.toFun-graph (z , off z m no))))
```

These ingredients define a map from the ordinary union `D` to the internal product `prodL κ`. Its value is chosen by the left-biased case distinction, and `into` proves that this tagged value belongs to the product.

```agda
  Dmap : DefinableMap
  Dmap = record
    { dom = D ; cod = prodL κ ; fn = fn
    ; into = λ z m → into z m (decide z)
    ; graph = fo
```

The defining clause feeds the witness into the graph introduction, and uniqueness converts every graph entry into the value at the decided case, transported along the carrier equality. The definable map is complete.

```agda
    ; defines = λ z m → fo-in (fn z m) z (wit z m (decide z))
    ; only = λ z m y h → S≡ (PT.rec (setIsSet _ _) (only z m (decide z) y) (fo-out y z h)) }
```

Injectivity of the tagged map is proved by comparing the decided cases of two inputs. The case analysis has four combinations, and the tagged pair structure separates them cleanly.

```agda
  inj : (z : S) (m : Mem z) (z' : S) (m' : Mem z') → fst (fn z m) ≡ fst (fn z' m') → fst z ≡ fst z'
  inj z m z' m' = go (decide z) (decide z')
    where
    go : (c : Case z) (c' : Case z') → fst (val z m c) ≡ fst (val z' m' c') → fst z ≡ fst z'
    go (inl h) (inl h') q = ij₁ (X₁.toFun (z , h)) z z' (X₁.toFun-graph (z , h))
```

In the same-tag case, the pair equation is inverted by `pr-inj`: the tags agree, so the equation of the values identifies the two function values, which is exactly the argument the injectivity clause consumes.

```agda
      (subst (λ w → ⟨ pr (fst z') w ∈ fst E₁ ⟩) (sym (snd p)) (X₁.toFun-graph (z' , h')))
      where
      p : (# 0 ≡ # 0) × (fst (X₁.toFun (z , h)) ≡ fst (X₁.toFun (z' , h')))
      p = pr-inj (sym (prʟ-fst (nn 0) (X₁.toFun (z , h))) ∙ q ∙ prʟ-fst (nn 0) (X₁.toFun (z' , h')))
    go (inl h) (inr no') q = Empty.rec (znots (#-inj 0 1 (fst
```

The mixed-tag cases are impossible: equality of the two values would force the numeral `0` to equal the numeral `1`, contradicted in the two orientations by `znots` and `snotz`. When both inputs take the right branch, injectivity of `E₂` identifies them.

```agda
      (pr-inj (sym (prʟ-fst (nn 0) (X₁.toFun (z , h))) ∙ q ∙ prʟ-fst (nn 1) (X₂.toFun (z' , off z' m' no')))))))
    go (inr no) (inl h') q = Empty.rec (snotz (#-inj 1 0 (fst
      (pr-inj (sym (prʟ-fst (nn 1) (X₂.toFun (z , off z m no))) ∙ q ∙ prʟ-fst (nn 0) (X₁.toFun (z' , h')))))))
    go (inr no) (inr no') q = ij₂ (X₂.toFun (z , off z m no)) z z' (X₂.toFun-graph (z , off z m no))
      (subst (λ w → ⟨ pr (fst z') w ∈ fst E₂ ⟩) (sym (snd p)) (X₂.toFun-graph (z' , off z' m' no')))
```

The pair equation for the right-right case splits into the agreement of the tags and of the function values, the latter being what injectivity consumes.

```agda
      where
      p : (# 1 ≡ # 1) × (fst (X₂.toFun (z , off z m no)) ≡ fst (X₂.toFun (z' , off z' m' no')))
      p = pr-inj (sym (prʟ-fst (nn 1) (X₂.toFun (z , off z m no))) ∙ q
                  ∙ prʟ-fst (nn 1) (X₂.toFun (z' , off z' m' no')))
```

The resulting graph is a coded injection from the ordinary union `D₁ ∪ D₂` into `prodL κ`. The map uses tags in its values to distinguish the two branches, and resolves an element in the overlap through the first branch.

```agda
  injL : InjL D (prodL κ)
  injL = Inj.injL Dmap inj
```

The two premises expose their injection graphs only under propositional truncation. Eliminating both truncations into the proposition `InjL (D₁ ∪ D₂) (prodL κ)` lets the tagged construction be applied to any witnessing pair of graphs, yielding the required mere coded injection.

```agda
tag-union : (κ : S) → ⟨ # 0 ∈ fst κ ⟩ → ⟨ # 1 ∈ fst κ ⟩
          → (D₁ D₂ : S) → InjL D₁ κ → InjL D₂ κ
          → InjL (unionʟ (pairʟ D₁ D₂)) (prodL κ)
tag-union κ h0 h1 D₁ D₂ = PT.rec2 squash₁
  (λ { (E₁ , c₁) (E₂ , c₂) → TagUnion.injL κ h0 h1 D₁ D₂ E₁ E₂ c₁ c₂ })
```

The least-predecessor construction is stated generically. It takes an ordinal `γ`, a relation `G`, a domain `D`, and a set `P` of predecessors bounded by the stage `γ`, such that every member of `D` merely has some `G`-predecessor in `P`; the task is to choose one canonically.

```agda
module LeastPre (γ : V ℓ) (oγ : IsOrd γ) (G D P : S)
  (inP : (p z : S) → Holds G p z → ⟨ fst p ∈ fst P ⟩)
  (P⊆L : (p : S) → ⟨ fst p ∈ fst P ⟩ → ⟨ fst p ∈ Lset γ ⟩)
  (have : (z : S) → ⟨ fst z ∈ fst D ⟩ → ∥ Σ[ p ∈ S ] Holds G p z ∥₁) where
```

Membership in the domain is recorded as a type, so that the argument can carry it alongside the elements.

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem z = ⟨ fst z ∈ fst D ⟩
```

The graph formula is the application clause of the constant `G`: holding at a pair means exactly that the pair belongs to the relation.

```agda
  private
    graphFo : Formula S 2
    graphFo = appC G i0 i1
```

The existence hypothesis is moved to the common stage without choosing a predecessor globally. Each truncated predecessor lies in `P`, hence in `Lset γ`, and the adequacy equation turns its relation membership into satisfaction of the graph formula.

```agda
    have-γ : (z : S) → Mem z
           → ∥ Σ[ p ∈ S ] (⟨ fst p ∈ Lset γ ⟩ × ⟨ (p ∷ z ∷ []) ⊨ graphFo ⟩) ∥₁
    have-γ z m = PT.map
      (λ { (p , h) → p , P⊆L p (inP p z h)
                       , subst ⟨_⟩ (sym (appC-adequate G i0 i1 (p ∷ z ∷ []))) h })
```

The original truncated existence supplies the witness that the transport consumes.

```agda
      (have z m)
```

The stage-order construction now selects, for every member of the domain, the least `G`-predecessor in `Lset γ`. It also supplies a definable graph and the membership readings that identify each input with its selected value.

```agda
    module Ls = Least γ oγ D graphFo have-γ using ( fn; fn-holds; Dmap; T; T-in; T-out )
```

The selected least predecessor is the value function of the construction.

```agda
  fn : (z : S) → Mem z → S
  fn = Ls.fn
```

The value satisfies the relation at its input: the internal satisfaction is transported back to the application clause at the environment pairing the value with the input.

```agda
  fn-holds : (z : S) (m : Mem z) → Holds G (fn z m) z
  fn-holds z m = subst ⟨_⟩ (appC-adequate G i0 i1 (fn z m ∷ z ∷ [])) (Ls.fn-holds z m)
```

The definable map is recorded with codomain `P`, the membership of the value being guaranteed by the inward direction of the standing hypothesis.

```agda
  Dmap : DefinableMap
  Dmap = record Ls.Dmap { cod = P ; into = λ z m → inP (fn z m) z (fn-holds z m) }
```

The graph of the least-predecessor function is an element of `L`, as the stage machinery returns it with its membership description.

```agda
  T : S
  T = Ls.T
```

The inward reading exhibits the pair of an input with its selected value as an entry of the graph.

```agda
  T-in : (z : S) (m : Mem z) → ⟨ pr (fst z) (fst (fn z m)) ∈ fst T ⟩
  T-in = Ls.T-in
```

The outward reading recovers, from every entry, the input together with the equation identifying the second component with the selected value; this is what later arguments use to compare candidates.

```agda
  T-out : (z e : S) → ⟨ pr (fst z) (fst e) ∈ fst T ⟩
        → Σ[ m ∈ Mem z ] (fst e ≡ fst (fn z m))
  T-out = Ls.T-out
```

Under the additional hypothesis that the relation is functional, the least-predecessor function becomes injective: the module carries that single assumption.

```agda
  module Functional
    (funct : (p z z' : S) → Holds G p z → Holds G p z' → fst z ≡ fst z') where
```

If two inputs share a value, the value satisfies the relation at both inputs; the second satisfaction is transported along the equation of the values, and functionality then identifies the two inputs.

```agda
    inj : (z : S) (m : Mem z) (z' : S) (m' : Mem z')
        → fst (fn z m) ≡ fst (fn z' m') → fst z ≡ fst z'
    inj z m z' m' q = funct (fn z m) z z' (fn-holds z m)
      (subst (λ w → ⟨ pr w (fst z') ∈ fst G ⟩) (sym q) (fn-holds z' m'))
```

The injectivity is packaged into a coded injection from the domain into the predecessor set.

```agda
    injL : InjL D P
    injL = Inj.injL Dmap inj
```

The point construction handles an at-most-singleton domain. Given only `0 ∈ κ`, it sends every member of the singleton generated by `a` to the zeroth numeral and obtains a coded injection into `κ`.

```agda
module Point (κ : S) (0∈κ : ⟨ # 0 ∈ fst κ ⟩) (a : S) where
```

Let `Y` be the constructible singleton generated by `a`. The argument will use only its membership introduction and elimination laws.

```agda
  Y : S
  Y = sglʟ a
```

The member `a` belongs to its own singleton, by the introduction reading of the singleton construction.

```agda
  Y-in : ⟨ fst a ∈ fst Y ⟩
  Y-in = sglʟ-in a (fst a) refl
```

The elimination reading says the singleton contains nothing else: any member has `a` as its underlying set.

```agda
  Y-out : (z : S) → ⟨ fst z ∈ fst Y ⟩ → fst z ≡ fst a
  Y-out z = sglʟ-out a (fst z)
```

The graph is described by the atomic formula with two free slots that equates the value slot with the internal empty set, whose underlying set is the numeral `0`.

```agda
  fo : Formula S 2
  fo = var i0 ≐ con ∅ʟ
```

The definable map sends the unique input to the zeroth numeral; the codomain membership is the standing fact `0∈κ`.

```agda
  Dmap : DefinableMap
  Dmap = record
    { dom = Y ; cod = κ ; fn = λ _ _ → nn 0
    ; into = λ _ _ → 0∈κ
    ; graph = fo
```

The graph holds definitionally, since the atomic sentence equates the numeral with itself; uniqueness holds because both members of the singleton present the same underlying set.

```agda
    ; defines = λ z m → refl
    ; only = λ z m y h → S≡ h }
```

Injectivity composes the two outward readings: both inputs present the same underlying set as `a`, hence they are equal as carrier elements.

```agda
  inj : (z : S) (m : ⟨ fst z ∈ fst Y ⟩) (z' : S) (m' : ⟨ fst z' ∈ fst Y ⟩)
      → fst (nn 0) ≡ fst (nn 0) → fst z ≡ fst z'
  inj z m z' m' _ = Y-out z m ∙ sym (Y-out z' m')
```

The singleton-to-cardinal injection is packaged in the same form as every other counting piece.

```agda
  injL : InjL Y κ
  injL = Inj.injL Dmap inj
```

## Counting every finite closure step

The counting theorem fixes an ordinal `lam` closed under successor, a start set `X` contained in `Lset lam`, and a proof that `X` is constructible. The elementarity and superadequacy hypotheses provide the closure and least-witness facts for the Skolem hull generated from `X`.

```agda
module Count (lam : V ℓ) (ordλ : IsOrd lam)
  (succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : V ℓ) (X⊆L : (x : V ℓ) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
  (elem : Frame.A.Elementary lam ordλ succλ X X⊆L ∅∈λ)
```

The counting target is an internal cardinal `κ` outside `ω`, together with a coded injection of the start into it. The task is to count the whole hull by the same cardinal.

```agda
  (sup : Superadequate lam)
  (X-isL : ⟨ isL X ⟩)
  (κ : S) (oκ : IsOrd (fst κ)) (cκ : IsCardinalL κ) (κ∉ω : ⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
  (base : InjL (X , X-isL) κ) where
```

The hull is presented as the union of its finite iterates `hullStep n`. One closure step is governed by `Φ`, whose nontrivial branch records a least witness for a formula key and a finite parameter environment over the current iterate.

```agda
  module Cn = Condense′ lam ordλ succλ X X⊆L ∅∈λ elem sup X-isL
    using ( hullStep; hullL; hullStep⊆Hull )
  module B = Telescope.Build lam ordλ succλ X X⊆L ∅∈λ
    using ( A; Body
          ; LeastWitness; leastWitnessFo; leastWitness-in; leastWitness-out
```

For a least witness, the accompanying data recover a natural length, a finite assignment into the current set, the encoded environment, and membership of the formula key in `Lset ω`. Uniqueness holds after the key and environment have been fixed.

```agda
          ; LeastWitnessData; leastWitness-data; leastWitness-unique; witFo-leastWitness
          ; Φ; Φ-out; λ-isL; ω-num; pack )
  module SM = SatGraph B.A using ( pairs; pairs-out; valOf )
```

The finite iterates come with introduction and elimination rules, and every iterate lies in the full hull. The full hull itself is contained in `Lset lam`; these inclusions keep every set used by the counting construction inside the fixed ambient stage.

```agda
  module It = Telescope.HullIter.It lam ordλ succλ X X⊆L ∅∈λ X-isL B.pack
    using ( Num; iter; iter-in; iter-out; iterUnion-out; ω-num )
  module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ using ( Hull⊆L )
  open Cn using ( hullStep; hullL )
```

Because `κ` is an ordinal and does not belong to `ω`, it contains every finite numeral. Internal cardinality is not used for this conclusion; it is needed separately for the square law.

```agda
  num∈κ : (k : ℕ) → ⟨ # k ∈ fst κ ⟩
  num∈κ k = ω⊆ (fst κ) oκ κ∉ω (# k) (#∈ω k)
```

The infinite-cardinal square argument gives the coded injection `pairκ : InjL (prodL κ) κ`. It uses all three relevant hypotheses on `κ`: ordinality, internal cardinality, and non-membership in `ω`; the result is an injection, not a bijection.

```agda
  pairκ : InjL (prodL κ) κ
  pairκ = WF.WFI.induction regularityV {P = Goal} Step.result (fst κ) (snd κ) oκ cκ κ∉ω
```

The stage `Lω = Lset ω` injects into `κ` by composition. Limit-stage counting first gives `Lω ↪ ωʟ`, and the inclusion `ω ⊆ κ`, obtained from the ordinality and non-finiteness of `κ`, gives `ωʟ ↪ κ`.

```agda
  Lω↪κ : InjL Lω κ
  Lω↪κ = injl-trans Lω ωʟ κ limit-stage-counted
    (inclusion-coded ωʟ κ (λ z hz → ω⊆ (fst κ) oκ κ∉ω z hz))
```

For one closure step, fix a constructible `Z` contained in `Lset lam` and an actual graph `E` satisfying `InjCode E Z κ`. The goal is to turn this chosen stage injection into the mere coded injection `InjL (Φ Z) κ`.

```agda
  module OneStep (Z : S) (Z⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
                 (E : S) (cE : InjCode E Z κ) where
```

`ΦZ = Φ Z` is one closure step. Its membership description has three branches: an old member of `Z`, the empty-set fallback, or a least witness determined by a formula key and a finite parameter environment over `Z`.

```agda
    ΦZ : S
    ΦZ = B.Φ Z
```

The new part is separated first: `D₂` collects the members of `ΦZ` that are not members of `Z`. Separation inside `L` keeps the new part constructible.

```agda
    opaque
      D₂ : S
      D₂ = hasSeparationL ΦZ (¬̇ (var i0 ∈̇ con Z)) .fst .fst
```

Its membership specification says exactly what separation computed: belonging to `D₂` is belonging to `ΦZ` together with the refutation of belonging to `Z`.

```agda
      D₂-spec : (z : S) → (fst z ∈ fst D₂)
              ≡ ((fst z ∈ fst ΦZ) ⊓ ((z ∷ []) ⊨ ¬̇ (var i0 ∈̇ con Z)))
      D₂-spec z = hasSeparationL ΦZ (¬̇ (var i0 ∈̇ con Z)) .fst .snd z
```

The introduction rule lifts the refutation of membership into the object level, so an element of `ΦZ` together with a proof that it is not in `Z` enters `D₂`.

```agda
    opaque
      D₂-in : (z : S) → ⟨ fst z ∈ fst ΦZ ⟩ → (⟨ fst z ∈ fst Z ⟩ → Empty.⊥) → ⟨ fst z ∈ fst D₂ ⟩
      D₂-in z h no = subst ⟨_⟩ (sym (D₂-spec z)) (h , λ z∈ → lift (no z∈))
```

The elimination rule unpacks membership in `D₂` through the specification, and lowers the object-level refutation back to an ordinary implication.

```agda
      D₂-out : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → ⟨ fst z ∈ fst ΦZ ⟩ × (⟨ fst z ∈ fst Z ⟩ → Empty.⊥)
      D₂-out z h = r .fst , λ z∈ → lower (r .snd z∈)
        where
        r : ⟨ fst z ∈ fst ΦZ ⟩
          × ⟨ (z ∷ []) ⊨ ¬̇ (var i0 ∈̇ con Z) ⟩
```

The unpacked statement is a pair: membership in `ΦZ` and satisfaction of the negated atom.

```agda
        r = subst ⟨_⟩ (D₂-spec z) h
```

Inside the new part, the elements equal to the empty set are separated out as `D∅`.

```agda
    opaque
      D∅ : S
      D∅ = hasSeparationL D₂ (var i0 ≐ con ∅ʟ) .fst .fst
```

Its specification is the same two-fold pattern: membership in `D₂` together with the equation to the empty set.

```agda
      D∅-spec : (z : S) → (fst z ∈ fst D∅)
              ≡ ((fst z ∈ fst D₂) ⊓ ((z ∷ []) ⊨ var i0 ≐ con ∅ʟ))
      D∅-spec z = hasSeparationL D₂ (var i0 ≐ con ∅ʟ) .fst .snd z
```

An element of `D₂` that equals the empty set enters `D∅` with both data.

```agda
    opaque
      D∅-in : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → fst z ≡ ∅ → ⟨ fst z ∈ fst D∅ ⟩
      D∅-in z h e = subst ⟨_⟩ (sym (D∅-spec z)) (h , e)
```

Its elimination is the specification read directly: membership in `D₂` and the equation to the empty set.

```agda
      D∅-out : (z : S) → ⟨ fst z ∈ fst D∅ ⟩ → ⟨ fst z ∈ fst D₂ ⟩ × (fst z ≡ ∅)
      D∅-out z h = subst ⟨_⟩ (D∅-spec z) h
```

The remainder `Dw` collects the elements of `D₂` that differ from the empty set.

```agda
    opaque
      Dw : S
      Dw = hasSeparationL D₂ (¬̇ (var i0 ≐ con ∅ʟ)) .fst .fst
```

Its specification mirrors the previous one, with the negated equation in place of the equation.

```agda
      Dw-spec : (z : S) → (fst z ∈ fst Dw)
              ≡ ((fst z ∈ fst D₂) ⊓ ((z ∷ []) ⊨ ¬̇ (var i0 ≐ con ∅ʟ)))
      Dw-spec z = hasSeparationL D₂ (¬̇ (var i0 ≐ con ∅ʟ)) .fst .snd z
```

Introduction requires membership in `D₂` and a refutation of equality with the empty set.

```agda
    opaque
      Dw-in : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → (fst z ≡ ∅ → Empty.⊥) → ⟨ fst z ∈ fst Dw ⟩
      Dw-in z h ne = subst ⟨_⟩ (sym (Dw-spec z)) (h , λ q → lift (ne q))
```

Elimination returns membership in `D₂` and the refutation, lowered from the object level.

```agda
      Dw-out : (z : S) → ⟨ fst z ∈ fst Dw ⟩ → ⟨ fst z ∈ fst D₂ ⟩ × (fst z ≡ ∅ → Empty.⊥)
      Dw-out z h = r .fst , λ q → lower (r .snd q)
        where
        r : ⟨ fst z ∈ fst D₂ ⟩
          × ⟨ (z ∷ []) ⊨ ¬̇ (var i0 ≐ con ∅ʟ) ⟩
```

Two unions provide the bounds needed later. `U₁` contains `Z` and the genuinely new part `D₂`, while `U₃` contains the empty-valued part `D∅` and the nonempty witness part `Dw`. The next lemmas prove the required inclusions into these unions.

```agda
        r = subst ⟨_⟩ (Dw-spec z) h
    module U₁ = Union2 Z D₂ using ( D; in₁; in₂ )
    module U₃ = Union2 D∅ Dw using ( D; in₁; in₂ )
```

The closure step is covered by the first union. Each member `z` of `ΦZ` either belongs to `Z` or does not, decided by excluded middle; in both cases `z` is constructible, because `ΦZ` is.

```agda
    ΦZ⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst ΦZ ⟩ → ⟨ z ∈ˢ fst U₁.D ⟩
    ΦZ⊆ z h = go (lem (z ∈ fst Z))
      where
      zS : S
      zS = z , isL-trans {x = fst ΦZ} {y = z} h (snd ΦZ)
```

The two cases enter `U₁` through its two union inclusions. A member already in `Z` uses the first inclusion; otherwise `D₂-in` first proves that it belongs to the new part, after which the second inclusion applies.

```agda
      go : ⟨ z ∈ fst Z ⟩ ⊎ (⟨ z ∈ fst Z ⟩ → Empty.⊥) → ⟨ z ∈ fst U₁.D ⟩
      go (inl hz) = U₁.in₁ zS hz
      go (inr no) = U₁.in₂ zS (D₂-in zS h no)
```

The new part is covered by the second union, by the same excluded-middle argument on the equation with the empty set.

```agda
    D₂⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst D₂ ⟩ → ⟨ z ∈ˢ fst U₃.D ⟩
    D₂⊆ z h = go (lem ((z ≡ ∅) , setIsSet z ∅))
      where
      zS : S
      zS = z , isL-trans {x = fst D₂} {y = z} h (snd D₂)
```

An element equal to the empty set enters through `D∅`; an element distinct from it enters through `Dw`.

```agda
      go : (z ≡ ∅) ⊎ (z ≡ ∅ → Empty.⊥) → ⟨ z ∈ fst U₃.D ⟩
      go (inl e)  = U₃.in₁ zS (D∅-in zS h e)
      go (inr ne) = U₃.in₂ zS (Dw-in zS h ne)
```

Every member of `D∅` equals `∅`, although `D∅` itself may be empty. Since the numeral `0` belongs to `κ`, inclusion coding therefore gives `D∅ ↪ κ` inside `L`.

```agda
    D∅↪κ : InjL D∅ κ
    D∅↪κ = inclusion-coded D∅ κ
      (λ z hz → subst (λ w → ⟨ w ∈ fst κ ⟩)
        (sym (D∅-out (z , isL-trans {x = fst D∅} {y = z} hz (snd D∅)) hz .snd)) (num∈κ 0))
```

A second union prepares the coding of witnesses: `U₂` joins the elements born by stage `ω` with the finite sequences of members of `Z`.

```agda
    module U₂ = Union2 Lω (seqL Z) using ( D; in₁; in₂ )
```

Let `PB` be the square of `U₂ = Lω ∪ seqL Z`. Every actual witness code `(s,e)`, with `s ∈ Lω` and `e ∈ seqL Z`, lies in `PB`; `PB` is a homogeneous upper bound and also contains pairs that are not valid witness codes.

```agda
    PB : S
    PB = prodL U₂.D
```

The least-witness formula is pinned at the fixed base `Z`. The resulting five-variable formula `pin₅` is satisfied at the frame `(e,s,z,p,q)` exactly when `z` is the least witness determined by the environment `e` and key `s`; the last two slots are carried by the surrounding frame.

```agda
    opaque
      pin₅ : Formula S 5
      pin₅ = pinAt Z B.leastWitnessFo
```

Inward, a least witness for `z` at the parameter environment `e` with key `s` yields the satisfaction of the pinned formula at the five-slot context.

```agda
      pin₅-in : (e s z p q : S) → B.LeastWitness Z e s z
              → ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩
      pin₅-in e s z p q h =
        pin-in Z B.leastWitnessFo (e ∷ s ∷ z ∷ p ∷ q ∷ [])
          (B.leastWitness-in Z e s z p q h)
```

Outward, satisfaction of the pinned formula unpacks to a least witness, the pinning being inverted by the pinning lemma.

```agda
      pin₅-out : (e s z p q : S) → ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩
               → B.LeastWitness Z e s z
      pin₅-out e s z p q h =
        B.leastWitness-out Z e s z p q
          (pin-out Z B.leastWitnessFo (e ∷ s ∷ z ∷ p ∷ q ∷ []) h)
```

The relation to be counted is propositionally truncated. `GW p z` says merely that there are a key `s` and an environment `e` such that `p = (s,e)` and `z` is their least witness.

```agda
    GW : (p z : S) → Type (ℓ-suc ℓ)
    GW p z = ∥ Σ[ s ∈ S ] Σ[ e ∈ S ]
               ((fst p ≡ pr (fst s) (fst e)) × B.LeastWitness Z e s z) ∥₁
```

The same relation is written as a formula: two existentials bind the key and the environment, the pairing atom identifies `p`, and the pinned formula carries the witness condition.

```agda
    opaque
      se₃ : Formula S 3
      se₃ = ∃̇ (∃̇ (prAtL i3 i1 i0 ∧̇ pin₅))
```

Inward: given the pair equation and a least witness, the two witnesses are entered and the pair atom is transported along its adequacy into the object language.

```agda
      se₃-in : (z p q s e : S) → fst p ≡ pr (fst s) (fst e)
             → B.LeastWitness Z e s z → ⟨ (z ∷ p ∷ q ∷ []) ⊨ se₃ ⟩
      se₃-in z p q s e qp h =
        ∣ s , ∣ e , ( subst ⟨_⟩ (sym (prAtL-adequate i3 i1 i0 (e ∷ s ∷ z ∷ p ∷ q ∷ []))) qp
                    , pin₅-in e s z p q h ) ∣₁ ∣₁
```

Outward, the two existentials are consumed one at a time; the first step strips the outer quantifier and keeps the entry `s` with the truncated remainder.

```agda
      se₃-out : (z p q : S) → ⟨ (z ∷ p ∷ q ∷ []) ⊨ se₃ ⟩ → GW p z
      se₃-out z p q = PT.rec squash₁ at₁
        where
        at₂ : (s : S) → Σ[ e ∈ S ] ( ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ prAtL i3 i1 i0 ⟩
                                   × ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩ ) → GW p z
```

After the second existential is opened, adequacy of the pairing atom recovers `p = (s,e)`, and the outward reading of the pinned formula recovers the least-witness condition. These witnesses are then placed back under the propositional truncation defining `GW`.

```agda
        at₂ s (e , (qp , h)) = ∣ s , e
          , ( subst ⟨_⟩ (prAtL-adequate i3 i1 i0 (e ∷ s ∷ z ∷ p ∷ q ∷ [])) qp
            , pin₅-out e s z p q h ) ∣₁
        at₁ : Σ[ s ∈ S ] ∥ Σ[ e ∈ S ] ( ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ prAtL i3 i1 i0 ⟩
                                      × ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩ ) ∥₁ → GW p z
```

Because `GW p z` is a proposition, the remaining outer truncation can be eliminated into it. Together, `se₃-in` and `se₃-out` give the two implications between the host relation `GW` and satisfaction of its object-language formula.

```agda
        at₁ (s , h) = PT.rec squash₁ (at₂ s) h
```

Bounded separation constructs a relation `G` inside `L` whose entries are ordered pairs `(p,z)` with `p ∈ PB`, `z ∈ Dw`, and `GW p z`. Thus `G` restricts the least-witness relation to the chosen code pool and the nonempty new part.

```agda
    private
      module WitnessGraph = Relation PB Dw ((var i1 ∈̇ con PB) ∧̇ se₃)
        (λ p z → (fst p ∈ fst PB) ⊓ (GW p z , squash₁))
        (λ p z q h → h .fst , se₃-out z p q (h .snd))
        (λ p z q h → h .fst , PT.rec (snd ((z ∷ p ∷ q ∷ []) ⊨ se₃))
```

The outward reading of the describing condition is the formula's own outward reading, which returns exactly the data of `GW`.

```agda
          (λ { (s , e , qp , hw) → se₃-in z p q s e qp hw }) (h .snd))
```

`G` is the resulting constructible relation, represented as a set of ordered pairs `(p,z)`. It relates a candidate code in `PB` to an element of `Dw` when that code carries least-witness data for the element.

```agda
    G : S
    G = WitnessGraph.rel
```

Inward: a code `p` in `PB` that, together with `z`, names a least witness through some key and environment, belongs to `G`.

```agda
    G-in : (p z : S) → ⟨ fst p ∈ fst PB ⟩ → ⟨ fst z ∈ fst Dw ⟩
         → (s e : S) → fst p ≡ pr (fst s) (fst e)
         → B.LeastWitness Z e s z → Holds G p z
    G-in p z hp hz s e qp h =
      WitnessGraph.into p z hp hz (hp , ∣ s , e , qp , h ∣₁)
```

Conversely, `Holds G p z` yields both `p ∈ PB` and the propositionally truncated witness data `GW p z`. It does not choose a key and environment outside that truncation.

```agda
    G-out : (p z : S) → Holds G p z → ⟨ fst p ∈ fst PB ⟩ × GW p z
    G-out = WitnessGraph.pair-out
```

The relation is total on `Dw` only in the truncated sense: every `z ∈ Dw` merely has some `p` with `Holds G p z`. Reading membership in `ΦZ` exposes the three possible reasons why `z` entered the closure step.

```agda
    have : (z : S) → ⟨ fst z ∈ fst Dw ⟩ → ∥ Σ[ p ∈ S ] Holds G p z ∥₁
    have z hz = PT.rec squash₁ body (B.Φ-out Z z (D₂-out z (Dw-out z hz .fst) .fst))
      where
      body : B.Body Z z → ∥ Σ[ p ∈ S ] Holds G p z ∥₁
      body (inl h) = Empty.rec (D₂-out z (Dw-out z hz .fst) .snd h)
```

Two of them are already excluded by the separators: `z` cannot be an old member of `Z`, nor the empty set. What remains is the witness case, read through the outward lemma of the witness formula.

```agda
      body (inr (inl e)) = Empty.rec (Dw-out z hz .snd e)
      body (inr (inr hw)) = PT.rec squash₁ read (B.witFo-leastWitness z Z hw)
        where
        read : Σ[ e ∈ S ] Σ[ s ∈ S ] B.LeastWitness Z e s z
             → ∥ Σ[ p ∈ S ] Holds G p z ∥₁
```

The witness branch supplies an environment `e`, a key `s`, and a least witness. Its data lemma then gives a natural length `n`, a meta-level assignment `g : Fin n → ⟪Z⟫`, an equation identifying `e` with the encoded environment of `g`, and the membership `s ∈ Lset ω`.

```agda
        read (e , s , hw') = PT.map at (B.leastWitness-data Z e s z hw')
          where
          at : B.LeastWitnessData Z e s → Σ[ p ∈ S ] Holds G p z
          at (n , g , qe , hs) = prʟ s e
            , G-in (prʟ s e) z
```

The code `p` is the internal pair of the key and the environment. Its membership in `PB` is built entry by entry: the key enters through `Lω` because it lies in `Lset ω`, and the environment enters through the finite sequences of `Z`, being the environment of a length-`n` assignment into `Z`. The relation then accepts the pair.

```agda
                (subst (λ w → ⟨ w ∈ fst PB ⟩) (sym (prʟ-fst s e))
                  (prodL-in U₂.D s e (U₂.in₁ s hs)
                    (U₂.in₂ e (seqL-in Z n e
                      (subst (λ w → ⟨ w ∈ˢ fst (envSet Z n) ⟩) (sym qe) (envSet-in Z g))))))
                hz s e (prʟ-fst s e) hw'
```

## Uniqueness for a witness key

The required functionality has the reverse orientation needed for counting: if one fixed code `p` is related both to `z` and to `z'`, then `z` and `z'` have equal underlying sets. Different codes for the same element are still allowed.

```agda
    funct : (p z z' : S) → Holds G p z → Holds G p z' → fst z ≡ fst z'
    funct p z z' h h' = PT.rec2 (setIsSet (fst z) (fst z')) read (G-out p z h .snd) (G-out p z' h' .snd)
      where
      read : Σ[ s ∈ S ] Σ[ e ∈ S ]
               ((fst p ≡ pr (fst s) (fst e)) × B.LeastWitness Z e s z)
```

Both relations are read outward, each returning a key, an environment, the pair equation, and a least witness.

```agda
           → Σ[ s₂ ∈ S ] Σ[ e₂ ∈ S ]
               ((fst p ≡ pr (fst s₂) (fst e₂)) × B.LeastWitness Z e₂ s₂ z')
           → fst z ≡ fst z'
      read (s , e , q , hw) (s₂ , e₂ , q₂ , hw₂) =
        B.leastWitness-unique Z e s z z' hw hw₂'
```

Both readings express the same fixed `p` as `(s,e)` and `(s₂,e₂)`. Injectivity of ordered-pair coding identifies the two keys and the two environments at the level of underlying sets, and proof irrelevance lifts those equalities to the corresponding elements of `S`.

```agda
        where
        ee : (fst s₂ ≡ fst s) × (fst e₂ ≡ fst e)
        ee = pr-inj (sym q₂ ∙ q)
        hw₂' : B.LeastWitness Z e s z'
        hw₂' = subst2 (λ e' s' → B.LeastWitness Z e' s' z')
```

After transporting the second least-witness proof along those identifications, both proofs concern the same key and environment. Least-witness uniqueness then gives `fst z ≡ fst z'`.

```agda
          (S≡ {x = e₂} {y = e} (snd ee)) (S≡ {x = s₂} {y = s} (fst ee)) hw₂
```

The code pool has a birth stage: `γG` is the stage at which `PB` appears in the hierarchy.

```agda
    γG : V ℓ
    γG = stage (fst PB) (snd PB)
```

That stage is indexed by an ordinal, which is what the counting lemma requires of it.

```agda
    oγG : IsOrd γG
    oγG = stage-ord (fst PB) (snd PB)
```

The pool is contained in its birth stage, by the transitivity of the stages: a member of a set born at `γG` belongs to `Lset γG`.

```agda
    PB⊆Lγ : (p : S) → ⟨ fst p ∈ fst PB ⟩ → ⟨ fst p ∈ Lset γG ⟩
    PB⊆Lγ p hp = layer-trans (Lset-layer γG) {x = fst PB} {y = fst p} hp (stage-mem (fst PB) (snd PB))
```

The hypotheses now instantiate `LeastPre`: every `z ∈ Dw` merely has a related code in `PB`, and a fixed code determines at most one such `z`. Least selection chooses one code for each element and yields `InjL Dw PB`. It does not assert that witness codes were unique beforehand, and this is only the count of the nonempty new part, not yet the full one-step result.

```agda
    module LP = LeastPre γG oγG G Dw PB (λ p z h → G-out p z h .fst) PB⊆Lγ have
      using ( module Functional )
```

The least-preimage construction injects the genuinely new witnesses into `PB`. Each `z ∈ Dw` merely has some related code, and the stage order selects the least such code. Codes need not be unique before selection; injectivity follows instead because a fixed code can represent only one witness.

```agda
    Dw↪PB : InjL Dw PB
    Dw↪PB = LP.Functional.injL funct
```

The injection `Z ↪ κ` acts coordinatewise on finite sequences, giving `seqL Z ↪ seqL κ`. Composing with finite-sequence counting yields `seqL Z ↪ κ`; this second map requires only that `κ` be an infinite ordinal, not that it be an internal cardinal.

```agda
    seq↪κ : InjL (seqL Z) κ
    seq↪κ = injl-trans (seqL Z) (seqL κ) κ (seq-map Z κ E cE) (seq-count κ oκ κ∉ω)
```

First count `U₂.D = Lω ∪ seqL Z`: tagging its two summands gives an injection into `κ × κ`, and `pairκ` folds that product into `κ`. Since `PB = U₂.D × U₂.D`, `prod-inj` lifts this injection to `PB ↪ κ × κ`; a second use of `pairκ` then gives `PB ↪ κ`. The two folds are the steps that use the square law and hence internal cardinality.

```agda
    PB↪κ : InjL PB κ
    PB↪κ = injl-trans PB (prodL κ) κ
      (prod-inj U₂.D κ
        (injl-trans U₂.D (prodL κ) κ (tag-union κ (num∈κ 0) (num∈κ 1) Lω (seqL Z) Lω↪κ seq↪κ) pairκ))
      pairκ
```

Composing the two injections gives the count of the genuinely new witnesses: every such witness is coded by some `p ∈ PB`, and `PB` injects into `κ`, so `Dw` injects into `κ`.

```agda
    Dw↪κ : InjL Dw κ
    Dw↪κ = injl-trans Dw PB κ Dw↪PB PB↪κ
```

The new part `D₂` is included in `D∅ ∪ Dw`. Here `D∅` contains precisely the new members equal to the empty set and may itself be empty, while `Dw` contains the nonempty witness members. Their two counts are tagged into `κ × κ` and folded by `pairκ`, giving `D₂ ↪ κ`.

```agda
    D₂↪κ : InjL D₂ κ
    D₂↪κ = injl-trans D₂ U₃.D κ (inclusion-coded D₂ U₃.D D₂⊆)
      (injl-trans U₃.D (prodL κ) κ (tag-union κ (num∈κ 0) (num∈κ 1) D∅ Dw D∅↪κ Dw↪κ) pairκ)
```

Every member of `ΦZ` lies in `Z ∪ D₂`. The given graph `E` counts `Z`, while the preceding construction counts `D₂`; tagging these injections gives a map into `κ × κ`, and `pairκ` completes the injection `ΦZ ↪ κ`.

```agda
    result : InjL ΦZ κ
    result = injl-trans ΦZ U₁.D κ (inclusion-coded ΦZ U₁.D ΦZ⊆)
      (injl-trans U₁.D (prodL κ) κ (tag-union κ (num∈κ 0) (num∈κ 1) Z D₂ ∣ E , cE ∣₁ D₂↪κ) pairκ)
```

`step-count` eliminates the truncated witness of `Z ↪ κ` into the proposition `ΦZ ↪ κ`. It therefore proves a cardinal bound by `κ`, rather than countability, and it does not select a graph witnessing the output injection.

```agda
  step-count : (Z : S) → ((z : V ℓ) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
             → InjL Z κ → InjL (B.Φ Z) κ
  step-count Z Z⊆ = PT.rec squash₁ (λ { (E , cE) → OneStep.result Z Z⊆ E cE })
```

Every member of every finite closure iterate lies in the ambient stage `Lset lam`: this follows from the iterates being contained in the hull, whose members all lie in the stage.

```agda
  iter⊆L : (n : ℕ) (z : V ℓ) → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ Lset lam ⟩
  iter⊆L n z hz = HSH.Hull⊆L z (Cn.hullStep⊆Hull n z hz)
```

Natural-number induction gives a separate internal injection for every finite iterate. The base case is the assumed injection of the starting set, and the successor case applies `step-count`. These witnesses remain propositionally truncated, so they cannot simply be chosen simultaneously to count the union.

```agda
  counted : (n : ℕ) → InjL (hullStep n) κ
  counted zero    = base
  counted (suc n) = step-count (hullStep n) (iter⊆L n) (counted n)
```

`HoldsAt n σ` is the propositionally truncated assertion that some constructible graph `F ∈ Lset σ` codes an injection `hullStep n ↪ κ`. It records both the stage containing the code and the exact iterate that the code counts.

```agda
  HoldsAt : ℕ → V ℓ → hProp (ℓ-suc ℓ)
  HoldsAt n σ = ∥ Σ[ F ∈ S ] (⟨ fst F ∈ Lset σ ⟩ × InjCode F (hullStep n) κ) ∥₁ , squash₁
```

For each `n`, let `ls n` be the least ordinal stage satisfying `HoldsAt n`. The truncated injection supplied by `counted n` provides existence, and least-ordinal selection is valid because the resulting leastness statement is a proposition.

```agda
  opaque
    ls : (n : ℕ) → LeastOrd (HoldsAt n)
    ls n = PT.rec (isPropLeastOrd (HoldsAt n)) from (counted n)
      where
      from : Σ[ F ∈ S ] InjCode F (hullStep n) κ → LeastOrd (HoldsAt n)
```

Given a graph `F` coding `hullStep n ↪ κ`, the canonical stage containing `F` is an ordinal and witnesses `HoldsAt n` there. Thus the class of candidate stages is inhabited, and `leastOrd` returns its least member.

```agda
      from (F , code) = leastOrd (HoldsAt n)
        ∣ stage (fst F) (snd F) , stage-ord (fst F) (snd F)
        , ∣ F , stage-mem (fst F) (snd F) , code ∣₁ ∣₁
```

The family of least stages `n ↦ ls n`, indexed by the meta-level natural numbers, has a single ordinal bound `γ`. The bounding theorem places every `ls n` strictly below this common ordinal.

```agda
  opaque
    γ : V ℓ
    γ = boundingOrd (Lift {ℓ-zero} {ℓ} ℕ) (λ n → ls (lower n) .fst) (λ n → ls (lower n) .snd .fst) .fst
```

The bound `γ` is itself an ordinal. Hence `Lset γ` is a legitimate constructible stage in which the separate injection codes can be collected.

```agda
    oγ : IsOrd γ
    oγ = boundingOrd (Lift {ℓ-zero} {ℓ} ℕ) (λ n → ls (lower n) .fst) (λ n → ls (lower n) .snd .fst) .snd .fst
```

For every natural number `n`, the least stage `ls n` belongs to the common upper bound `γ`. This strict bound is the input needed for monotonicity of the constructible hierarchy.

```agda
    bnd-in : (n : ℕ) → ⟨ ls n .fst ∈ γ ⟩
    bnd-in n = boundingOrd (Lift {ℓ-zero} {ℓ} ℕ) (λ n → ls (lower n) .fst) (λ n → ls (lower n) .snd .fst)
                 .snd .snd (lift n)
```

A code at a smaller stage becomes a code at the common stage: the iterate's coding is transported into `Lset γ` by stage monotonicity.

```agda
  code-at-γ : (n : ℕ) → ⟨ HoldsAt n γ ⟩
  code-at-γ n = PT.map raise (ls n .snd .snd .fst)
    where
    raise : Σ[ F ∈ S ] (⟨ fst F ∈ Lset (ls n .fst) ⟩ × InjCode F (hullStep n) κ)
          → Σ[ F ∈ S ] (⟨ fst F ∈ Lset γ ⟩ × InjCode F (hullStep n) κ)
```

The transport pairs the code with its membership in the larger stage, leaving the code itself untouched; only the stage witness moves.

```agda
    raise (F , h , code) = F , Lset-mono {α = γ} {β = ls n .fst} (bnd-in n) h , code
```

Let `Lγ` be the constructible set whose underlying set is the common stage `Lset γ`. It serves as one internal domain containing an injection code for every finite iterate.

```agda
  opaque
    Lγ : S
    Lγ = LsetS γ oγ
```

Its underlying set is the stage `Lset γ`, definitionally.

```agda
    Lγ-fst : fst Lγ ≡ Lset γ
    Lγ-fst = refl
```

The iterates themselves are collected into one constructible set: `Iter` pairs each internal numeral with the closure iterate it indexes.

```agda
    Iter : S
    Iter = It.iter
```

Each pair of a numeral and its iterate is a member, by the iterated-set introduction.

```agda
    Iter-in : (n : ℕ) → ⟨ pr (# n) (fst (hullStep n)) ∈ fst Iter ⟩
    Iter-in = It.iter-in
```

Conversely, every member is, merely, such a pair, so membership in `Iter` identifies exactly the counted iterates and nothing else.

```agda
    Iter-out : (y : S) → ⟨ fst y ∈ fst Iter ⟩ → ∥ Σ[ n ∈ ℕ ] (fst y ≡ pr (# n) (fst (hullStep n))) ∥₁
    Iter-out = It.iter-out
```

A table witness for a constructible code `F` at an internal numeral `n` consists of two facts: `F` lies in the common stage, and, merely, there is an iterate recorded at `n` for which `F` codes an injection into `κ`.

```agda
  TabWit : (F n : S) → Type (ℓ-suc ℓ)
  TabWit F n = ⟨ fst F ∈ Lset γ ⟩ × ∥ Σ[ Zn ∈ S ] (Holds Iter n Zn × InjCode F Zn κ) ∥₁
```

`tabBody` has three free slots for a code `F`, an internal numeral `n`, and an unused relation parameter. It asserts `F ∈ Lset γ` and existentially binds an iterate `Zn` such that `Iter(n,Zn)` and `F` codes an injection `Zn ↪ κ`. The existential quantifier is unbounded over `S`.

```agda
  opaque
    tabBody : Formula S 3
    tabBody = (var i1 ∈̇ con Lγ) ∧̇ ∃̇ (appC Iter i1 i0 ∧̇ injFo κ i2 i0)
```

Reading the table body back uses the adequacy of the application atom and the reading of the injection formula, converting satisfaction into the two-component table witness.

```agda
    tab-read : (F n q : S) → ⟨ (n ∷ F ∷ q ∷ []) ⊨ tabBody ⟩ → TabWit F n
    tab-read F n q (hF , h) = subst (λ w → ⟨ fst F ∈ w ⟩) Lγ-fst hF
      , PT.map (λ { (Zn , hI , hc) → Zn
          , subst ⟨_⟩ (appC-adequate Iter i1 i0 (Zn ∷ n ∷ F ∷ q ∷ [])) hI
          , InjFo.read κ i2 i0 (Zn ∷ n ∷ F ∷ q ∷ []) hc }) h
```

Conversely, a `TabWit F n` witness supplies satisfaction of `tabBody`. Stage membership is transported to membership in `Lγ`, and the iterate relation and injection code are converted back through the adequacy of application and the injection formula.

```agda
    tab-fill : (F n q : S) → TabWit F n → ⟨ (n ∷ F ∷ q ∷ []) ⊨ tabBody ⟩
    tab-fill F n q (hF , h) = subst (λ w → ⟨ fst F ∈ w ⟩) (sym Lγ-fst) hF
      , PT.map (λ { (Zn , hI , hc) → Zn
          , subst ⟨_⟩ (sym (appC-adequate Iter i1 i0 (Zn ∷ n ∷ F ∷ q ∷ []))) hI
          , InjFo.fill κ i2 i0 (Zn ∷ n ∷ F ∷ q ∷ []) hc }) h
```

The relation defined by `tabBody` is collected as a constructible subset of `Lγ × ω`. Its members are pairs `(F,n)` satisfying the table witness condition; separation may use `tabBody` even though its displayed existential is unbounded, because the available separation principle is full separation.

```agda
  private
    module TableGraph = Relation Lγ ωʟ tabBody
      (λ F n → TabWit F n , isProp× (snd (fst F ∈ Lset γ)) squash₁) tab-read tab-fill
```

Write `Gt` for this constructible relation. A pair `(F,n)` belongs to it exactly when `F ∈ Lset γ` and there merely exists an iterate `Zn` recorded at `n` for which `F` codes an injection into `κ`.

```agda
  Gt : S
  Gt = TableGraph.rel
```

If `F ∈ Lset γ`, `n ∈ ω`, `Iter(n,Zn)`, and `F` codes `Zn ↪ κ`, then the pair `(F,n)` belongs to `Gt`. The iterate `Zn` is retained only under propositional truncation in the relation's specification.

```agda
  Gt-in : (F n Zn : S) → ⟨ fst F ∈ Lset γ ⟩ → ⟨ fst n ∈ fst ωʟ ⟩
        → Holds Iter n Zn → InjCode F Zn κ → Holds Gt F n
  Gt-in F n Zn hF hn hI code = TableGraph.into F n
    (subst (λ w → ⟨ fst F ∈ w ⟩) (sym Lγ-fst) hF) hn (hF , ∣ Zn , hI , code ∣₁)
```

Elimination reads a table entry back into the two-component witness.

```agda
  Gt-out : (F n : S) → Holds Gt F n → TabWit F n
  Gt-out = TableGraph.pair-out
```

Every internal numeral in `ω` carries an entry: the iterate it records is some finite closure stage, whose code exists in the common stage by the transport above.

```agda
  have-code : (n : S) → ⟨ fst n ∈ fst ωʟ ⟩ → ∥ Σ[ F ∈ S ] Holds Gt F n ∥₁
  have-code n hn = PT.rec squash₁ at (It.ω-num n hn)
    where
    at : It.Num n → ∥ Σ[ F ∈ S ] Holds Gt F n ∥₁
    at (k , qk) = PT.map
```

The code is then introduced into the table: the iterate identification is transported along the numeral equation, so the entry records the numeral paired with its own iterate.

```agda
      (λ { (F , hF , code) → F
         , Gt-in F n (hullStep k) hF hn
             (subst (λ w → ⟨ pr w (fst (hullStep k)) ∈ fst Iter ⟩) (cong fst qk) (Iter-in k)) code })
      (code-at-γ k)
```

Apply least-preimage selection to `Gt` with domain `ω` and code bound `Lγ`. For every internal numeral it selects the stage-order-least related injection code and collects the pairs `(n,eS(n))` into a constructible table `Te`. This definable selection inside one common stage avoids choosing representatives directly from the truncated family `counted n`.

```agda
  module Tb = LeastPre γ oγ Gt ωʟ Lγ
    (λ F n h → subst (λ w → ⟨ fst F ∈ w ⟩) (sym Lγ-fst) (Gt-out F n h .fst))
    (λ F hF → subst (λ w → ⟨ fst F ∈ w ⟩) Lγ-fst hF)
    have-code
    using ( T; fn; T-in; T-out; fn-holds )
```

`Te` is the constructible graph of the selected entries. Its domain is the internal `ω`, and its value at each numeral is the least code related to that numeral by `Gt`.

```agda
  Te : S
  Te = Tb.T
```

The least-entry function assigns to each internal numeral in `ω` the least table entry coding an injection for the iterate recorded there.

```agda
  eS : (n : S) → ⟨ fst n ∈ fst ωʟ ⟩ → S
  eS = Tb.fn
```

For every `n ∈ ω`, the ordered pair `(n,eS(n))` belongs to `Te`. Thus `Te` records the selected code as the value at the numeral `n`.

```agda
  Te-in : (n : S) (m : ⟨ fst n ∈ fst ωʟ ⟩) → ⟨ pr (fst n) (fst (eS n m)) ∈ fst Te ⟩
  Te-in = Tb.T-in
```

Conversely, if `(n,F) ∈ Te`, then `n ∈ ω` and the underlying set of `F` equals that of the selected entry `eS(n)`. The membership proof of `n ∈ ω` is proposition-valued, so it does not create additional table values.

```agda
  Te-out : (n F : S) → ⟨ pr (fst n) (fst F) ∈ fst Te ⟩
         → Σ[ m ∈ ⟨ fst n ∈ fst ωʟ ⟩ ] (fst F ≡ fst (eS n m))
  Te-out = Tb.T-out
```

The selected entry `eS(n)` satisfies the second component of `TabWit`: merely some iterate `Zn` is recorded at `n`, and `eS(n)` codes an injection `Zn ↪ κ`. The existential remains truncated because only its existence is part of the table specification.

```agda
  e-wit : (n : S) (m : ⟨ fst n ∈ fst ωʟ ⟩)
        → ∥ Σ[ Zn ∈ S ] (Holds Iter n Zn × InjCode (eS n m) Zn κ) ∥₁
  e-wit n m = Gt-out (eS n m) n (Tb.fn-holds n m) .snd
```

For the canonical numeral of a natural number `k`, the truncation is eliminated. The table entry at that numeral codes an injection of the iterate `hullStep k` into `κ`; the elimination is legitimate because `InjCode` is a proposition.

```agda
  e-code : (k : ℕ) → InjCode (eS (nn k) (#∈ω k)) (hullStep k) κ
  e-code k = PT.rec (isPropInjCode (eS (nn k) (#∈ω k)) (hullStep k) κ) read (e-wit (nn k) (#∈ω k))
    where
    F : S
    F = eS (nn k) (#∈ω k)
```

The recorded iterate is identified first: a member of the iterate set is, merely, a pair whose numeral component and iterate component can both be read off, and the pairing equations identify the recorded iterate.

```agda
    read : Σ[ Zn ∈ S ] (Holds Iter (nn k) Zn × InjCode F Zn κ) → InjCode F (hullStep k) κ
    read (Zn , hI , code) = PT.rec (isPropInjCode F (hullStep k) κ) at
      (Iter-out (prʟ (nn k) Zn) (subst (λ w → ⟨ w ∈ fst Iter ⟩) (sym (prʟ-fst (nn k) Zn)) hI))
      where
      at : Σ[ k' ∈ ℕ ] (fst (prʟ (nn k) Zn) ≡ pr (# k') (fst (hullStep k'))) → InjCode F (hullStep k) κ
```

The numeral equation forces `k'` to be `k`, and the code is transported along the identification of the two iterates, which does not change the code itself.

```agda
      at (k' , q) = injcode-resp F F Zn (hullStep k) κ refl
        (snd ee ∙ cong (λ j → fst (hullStep j)) (sym (#-inj k k' (fst ee)))) code
        where
        ee : (# k ≡ # k') × (fst Zn ≡ fst (hullStep k'))
        ee = pr-inj (sym (prʟ-fst (nn k) Zn) ∙ q)
```

`FinWit p z` merely records an internal numeral `n ∈ ω`, a value `v`, and a table entry `F`. Its equations say `p=(n,v)`, `Te(n)=F`, and `F(z)=v`. Thus `p`, rather than `F`, is the pair code used to count `z`.

```agda
  FinWit : (p z : S) → Type (ℓ-suc ℓ)
  FinWit p z = ∥ Σ[ n ∈ S ] Σ[ v ∈ S ] Σ[ F ∈ S ]
      ((fst p ≡ pr (fst n) (fst v)) × ⟨ fst n ∈ fst ωʟ ⟩ × Holds Te n F × Holds F z v) ∥₁
```

`inner₆` is the conjunction of two application statements: the table `Te` maps `n` to the entry `F`, and that entry maps `z` to `v`. With environment `F,v,n,z,p,q`, these are exactly `Holds Te n F` and `Holds F z v`.

```agda
  opaque
    inner₆ : Formula S 6
    inner₆ = appC Te i2 i0 ∧̇ appAt i0 i3 i1
```

Filling the two atoms uses their adequacy lemmas, so a witness record produces the satisfaction of the two application atoms in one environment.

```agda
    inner₆-in : (F v n z p q : S) → Holds Te n F → Holds F z v
              → ⟨ (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []) ⊨ inner₆ ⟩
    inner₆-in F v n z p q ht hv =
        subst ⟨_⟩ (sym (appC-adequate Te i2 i0 (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []))) ht
      , subst ⟨_⟩ (sym (appAt-adequate i0 i3 i1 (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []))) hv
```

Reading the two atoms uses the same adequacy lemmas in the forward direction, recovering the table satisfaction and the graph membership.

```agda
    inner₆-out : (F v n z p q : S) → ⟨ (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []) ⊨ inner₆ ⟩
               → Holds Te n F × Holds F z v
    inner₆-out F v n z p q (ht , hv) =
        subst ⟨_⟩ (appC-adequate Te i2 i0 (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ [])) ht
      , subst ⟨_⟩ (appAt-adequate i0 i3 i1 (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ [])) hv
```

`nv₃` has free variables `z,p,q` and existentially binds `n`, then `v`, then `F`. Its body states `p=(n,v)`, `n ∈ ω`, `Te(n)=F`, and `F(z)=v`; the free variable `q` is unused.

```agda
  opaque
    nv₃ : Formula S 3
    nv₃ = ∃̇ (∃̇ (prAtL i3 i1 i0 ∧̇ ((var i1 ∈̇ con ωʟ) ∧̇ ∃̇ inner₆)))
```

Given `p=(n,v)`, `n ∈ ω`, `Te(n)=F`, and `F(z)=v`, the three witnesses `n`, `v`, and `F` fill the nested existential quantifiers. Pairing adequacy supplies the pair atom, and `inner₆-in` supplies the two application atoms.

```agda
    nv₃-in : (z p q n v F : S) → fst p ≡ pr (fst n) (fst v) → ⟨ fst n ∈ fst ωʟ ⟩
           → Holds Te n F → Holds F z v → ⟨ (z ∷ p ∷ q ∷ []) ⊨ nv₃ ⟩
    nv₃-in z p q n v F qp hn ht hv =
      ∣ n , ∣ v , ( subst ⟨_⟩ (sym (prAtL-adequate i3 i1 i0 (v ∷ n ∷ z ∷ p ∷ q ∷ []))) qp
                  , ( hn , ∣ F , inner₆-in F v n z p q ht hv ∣₁ ) ) ∣₁ ∣₁
```

To read `nv₃`, first eliminate the truncated witness for `n`, then the truncated witness for `v`. For fixed `n` and `v`, `Inner n v` retains the pairing atom, membership `n ∈ ω`, and a third truncated existence of an entry `F` satisfying `inner₆`.

```agda
    nv₃-out : (z p q : S) → ⟨ (z ∷ p ∷ q ∷ []) ⊨ nv₃ ⟩ → FinWit p z
    nv₃-out z p q = PT.rec squash₁ at₁
      where
      Inner : (n v : S) → Type (ℓ-suc ℓ)
      Inner n v = ⟨ (v ∷ n ∷ z ∷ p ∷ q ∷ []) ⊨ prAtL i3 i1 i0 ⟩
```

The innermost truncated existence supplies the table entry `F`, not the value `v`, which is already fixed. Pairing adequacy converts the pair atom to `p=(n,v)`, while `inner₆-out` recovers `Te(n)=F` and `F(z)=v`; these data form `FinWit p z`.

```agda
                × ( ⟨ fst n ∈ fst ωʟ ⟩ × ∥ Σ[ F ∈ S ] ⟨ (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []) ⊨ inner₆ ⟩ ∥₁ )
      at₃ : (n v : S) → Inner n v → FinWit p z
      at₃ n v (qp , (hn , h)) = PT.map
        (λ { (F , hi) → n , v , F
           , ( subst ⟨_⟩ (prAtL-adequate i3 i1 i0 (v ∷ n ∷ z ∷ p ∷ q ∷ [])) qp
```

For fixed `n` and `v`, the innermost conversion produces `FinWit p z`; the two outer eliminations then discharge the truncated choices of `v` and `n`. Thus satisfaction of `nv₃` yields exactly the truncated tuple required by the ambient relation.

```agda
             , hn , inner₆-out F v n z p q hi ) }) h
      at₂ : (n : S) → Σ[ v ∈ S ] Inner n v → FinWit p z
      at₂ n (v , h) = at₃ n v h
      at₁ : Σ[ n ∈ S ] ∥ Σ[ v ∈ S ] Inner n v ∥₁ → FinWit p z
      at₁ (n , h) = PT.rec squash₁ (at₂ n) h
```

The final relation is obtained by separation inside the Cartesian product of `prodL κ` and `hullL`. Its defining formula is `nv₃`, whose three existential witnesses are an internal natural `n`, a value `v`, and a table entry `F`. The relation connects `p` to `z` exactly when `p = (n,v)`, `n ∈ ω`, the table records `F` at `n`, and `F` records `v` at `z`.

```agda
  private
    module FinalGraph = Relation (prodL κ) hullL nv₃ (λ p z → FinWit p z , squash₁)
      (λ p z q → nv₃-out z p q)
      (λ p z q → PT.rec (snd ((z ∷ p ∷ q ∷ []) ⊨ nv₃))
        (λ { (n , v , F , qp , hn , ht , hv) → nv₃-in z p q n v F qp hn ht hv }))
```

The separated set is named `Gf` and is the constructible carrier of the final graph.

```agda
  Gf : S
  Gf = FinalGraph.rel
```

To introduce membership in `Gf`, take `p ∈ prodL κ`, `z ∈ hullL`, an internal natural `n ∈ ω`, a value `v`, and a table entry `F`. An equation `p = (n,v)`, together with the graph memberships saying that `Te` records `F` at `n` and `F` records `v` at `z`, supplies exactly the witness required by the defining relation.

```agda
  Gf-in : (p z n v F : S) → ⟨ fst p ∈ fst (prodL κ) ⟩ → ⟨ fst z ∈ fst hullL ⟩
        → fst p ≡ pr (fst n) (fst v) → ⟨ fst n ∈ fst ωʟ ⟩ → Holds Te n F → Holds F z v
        → Holds Gf p z
  Gf-in p z n v F hp hz qp hn ht hv = FinalGraph.into p z hp hz ∣ n , v , F , qp , hn , ht , hv ∣₁
```

Conversely, `Gf-out` turns a graph membership into the propositionally truncated record `FinWit p z`. This record may be eliminated when proving proposition-valued consequences, such as membership in a set or equality of sets.

```agda
  Gf-out : (p z : S) → Holds Gf p z → FinWit p z
  Gf-out = FinalGraph.pair-out
```

Every value recorded by a table entry lies in `κ`. From `Te(n,F)`, the table reading identifies `F` with the selected entry at `n`; `e-wit` supplies an iterate `Zn` and an injection code from `Zn` into `κ` for that selected entry. Transporting `F(z)=v` across the table identification lets the range clause of this code prove `v ∈ κ`.

```agda
  entry-ran : (n F z v : S) → Holds Te n F → Holds F z v → ⟨ fst v ∈ fst κ ⟩
  entry-ran n F z v ht hv = PT.rec (snd (fst v ∈ fst κ))
    (λ { (Zn , _ , code) → snd (snd (snd code)) z v
          (subst (λ w → ⟨ pr (fst z) (fst v) ∈ w ⟩) (Te-out n F ht .snd) hv) })
    (e-wit n (Te-out n F ht .fst))
```

Every first component related by `Gf` belongs to `prodL κ`. A record for such a component writes it as `(n,v)` with `n ∈ ω` and `v ∈ κ`. Since the non-finite ordinal `κ` contains `ω`, also `n ∈ κ`; hence both coordinates lie in `κ`, so `(n,v) ∈ prodL κ`.

```agda
  inPκ : (p z : S) → Holds Gf p z → ⟨ fst p ∈ fst (prodL κ) ⟩
  inPκ p z h = PT.rec (snd (fst p ∈ fst (prodL κ)))
    (λ { (n , v , F , (qp , hn , ht , hv)) →
       subst (λ w → ⟨ w ∈ fst (prodL κ) ⟩) (sym qp)
         (prodL-in κ n v (ω⊆ (fst κ) oκ κ∉ω (fst n) hn) (entry-ran n F z v ht hv)) })
```

Applying this argument to the truncated record returned by `Gf-out` proves `inPκ`: whenever `Gf(p,z)` holds, its first component `p` belongs to `prodL κ`.

```agda
    (Gf-out p z h)
```

Every hull member merely has a related code. The characterization of the iterate union places `z` in some finite stage `hullStep n`. For the selected graph `F = eS (# n)`, the exact code `e-code n` has domain `hullStep n`; its totality clause therefore gives, merely, a value `v` with `F(z)=v`.

```agda
  have-fin : (z : S) → ⟨ fst z ∈ fst hullL ⟩ → ∥ Σ[ p ∈ S ] Holds Gf p z ∥₁
  have-fin z hz = PT.rec squash₁ at (It.iterUnion-out z hz)
    where
    at : Σ[ n ∈ ℕ ] ⟨ fst z ∈ fst (hullStep n) ⟩ → ∥ Σ[ p ∈ S ] Holds Gf p z ∥₁
    at (n , hn) = PT.map val (domAt-in zero (suc zero) (F ∷ hullStep n ∷ []) (fst (snd (e-code n))) z hn)
```

The totality clause of `e-code n` supplies the value `v` together with the graph membership `F(z)=v`. Pairing the canonical numeral `# n` with this value produces the candidate code `p = (# n,v)`.

```agda
      where
      F : S
      F = eS (nn n) (#∈ω n)
      val : Σ[ v ∈ S ] Holds F z v → Σ[ p ∈ S ] Holds Gf p z
      val (v , hv) = prʟ (nn n) v
```

The introduction assembles the whole record: the pair lies in the product by the numeral membership and the code's range clause, and the graph relates it to `z` by the table's own membership.

```agda
        , Gf-in (prʟ (nn n) v) z (nn n) v F
            (subst (λ w → ⟨ w ∈ fst (prodL κ) ⟩) (sym (prʟ-fst (nn n) v))
              (prodL-in κ (nn n) v (num∈κ n) (snd (snd (snd (e-code n))) z v hv)))
            hz (prʟ-fst (nn n) v) (#∈ω n) (Te-in (nn n) (#∈ω n)) hv
```

The functionality needed for least-preimage selection runs from a candidate code back to the hull: if the same `p` is related to both `z` and `z'`, then `z = z'`. This property makes the selected map from hull members to their least codes injective. Both relation witnesses are truncated records, and they can be eliminated here because equality of sets is a proposition.

```agda
  funct-fin : (p z z' : S) → Holds Gf p z → Holds Gf p z' → fst z ≡ fst z'
  funct-fin p z z' h h' = PT.rec2 (setIsSet (fst z) (fst z')) read (Gf-out p z h) (Gf-out p z' h')
    where
    read : Σ[ n ∈ S ] Σ[ v ∈ S ] Σ[ F ∈ S ]
             ((fst p ≡ pr (fst n) (fst v)) × ⟨ fst n ∈ fst ωʟ ⟩ × Holds Te n F × Holds F z v)
```

Unpacking the two records gives `n,v,F` and `n',v',F'`. Each record contains one pair equation, respectively `p=(n,v)` and `p=(n',v')`, together with three facts: its index belongs to `ω`, the table records its entry at that index, and the entry records the displayed value at the corresponding hull member.

```agda
         → Σ[ n' ∈ S ] Σ[ v' ∈ S ] Σ[ F' ∈ S ]
             ((fst p ≡ pr (fst n') (fst v')) × ⟨ fst n' ∈ fst ωʟ ⟩ × Holds Te n' F' × Holds F' z' v')
         → fst z ≡ fst z'
    read (n , v , F , (qp , hn , ht , hv)) (n' , v' , F' , (qp' , hn' , ht' , hv')) =
      PT.rec (setIsSet (fst z) (fst z'))
```

The two pair equations first give `n=n'` and `v=v'`. The table readings then align `F` and `F'` with the same selected entry `eS n m`. The witness `e-wit n m` supplies an iterate `Zn` and an injection code for this entry. After transporting both graph memberships to that common entry, and the second value along `v'=v`, the injectivity clause yields `z=z'`.

```agda
        (λ { (Zn , _ , code) →
           injAt-out zero (eS n m ∷ Zn ∷ []) (fst (snd (snd code))) v z z'
             (subst (λ w → ⟨ pr (fst z) (fst v) ∈ w ⟩) (Te-out n F ht .snd) hv)
             (subst2 (λ u w → ⟨ pr (fst z') u ∈ w ⟩) (sym (snd ee)) qF hv') })
        (e-wit n m)
```

Injectivity of the ordered pair splits the identification into the numeral and the value component, and the table reading certifies that the numeral lies in `ω`.

```agda
      where
      ee : (fst n ≡ fst n') × (fst v ≡ fst v')
      ee = pr-inj (sym qp ∙ qp')
      m : ⟨ fst n ∈ fst ωʟ ⟩
      m = Te-out n F ht .fst
```

The two pairs, numeral together with ω-membership, are equal because ω-membership is propositional and the numeral equation is an equality of underlying sets.

```agda
      pth : _≡_ {A = Σ[ c ∈ S ] ⟨ fst c ∈ fst ωʟ ⟩} (n' , Te-out n' F' ht' .fst) (n , m)
      pth = Σ≡Prop (λ c → snd (fst c ∈ fst ωʟ)) (S≡ {x = n'} {y = n} (sym (fst ee)))
```

Transporting the table reading for `F'` along the equality of the two internal-natural indices identifies `F'` with the selected entry `eS n m`. Together with the corresponding reading for `F`, this puts both graph memberships in the same injection graph.

```agda
      qF : fst F' ≡ fst (eS n m)
      qF = Te-out n' F' ht' .snd ∙ (λ i → fst (eS (fst (pth i)) (snd (pth i))))
```

Let `γf` be the ordinal stage assigned to the constructible set `prodL κ`. It provides a common stage `Lset γf` containing every candidate code, so the canonical stage order can compare their preimages.

```agda
  γf : V ℓ
  γf = stage (fst (prodL κ)) (snd (prodL κ))
```

That stage is an ordinal, as every stage is.

```agda
  oγf : IsOrd γf
  oγf = stage-ord (fst (prodL κ)) (snd (prodL κ))
```

The set `prodL κ` belongs to `Lset γf` by the defining property of its stage. Since `Lset γf` is transitive, every member of `prodL κ` also belongs to `Lset γf`; hence `prodL κ ⊆ Lset γf`.

```agda
  prodκ⊆Lγ : (p : S) → ⟨ fst p ∈ fst (prodL κ) ⟩ → ⟨ fst p ∈ Lset γf ⟩
  prodκ⊆Lγ p hp =
    layer-trans (Lset-layer γf) {x = fst (prodL κ)} {y = fst p} hp (stage-mem (fst (prodL κ)) (snd (prodL κ)))
```

For each `z ∈ hullL`, choose the stage-order-least `p ∈ prodL κ` with `Gf(p,z)`. The three required facts are exactly those proved above: every related `p` lies in `prodL κ`, this carrier is contained in `Lset γf`, and every hull member merely has a related `p`. Since `funct-fin` says that one `p` cannot be related to two different hull members, the resulting least-preimage map is an internal coded injection `hullL ↪ prodL κ`.

```agda
  module LF = LeastPre γf oγf Gf hullL (prodL κ) inPκ prodκ⊆Lγ have-fin using ( module Functional )
```

The least-preimage construction gives a coded injection from the hull into `prodL κ`, and the square law gives a coded injection from `prodL κ` into `κ`. Their composition proves the propositionally truncated statement `InjL hullL κ`. This is an internal coded injection; it asserts neither surjectivity nor equality of cardinals, and it makes no claim about a collapse image. Thus the constructible hull has distinct internal `κ`-codes for all of its members.

```agda
  hull↪κ : InjL hullL κ
  hull↪κ = injl-trans hullL (prodL κ) κ (LF.Functional.injL funct-fin) pairκ
```