---
title: "The counting tools for infinite constructible stages"
module: L.GCH.StageCountingTools
lang: en
site: "Bedrock"
description: "The counting tools for infinite constructible stages"
stage: "Proving GCH"
reading_order: 115
canonical: https://bedrock.institute/en/L.GCH.StageCountingTools.html
html: L.GCH.StageCountingTools.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/StageCountingTools.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Presentation, V.Model, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Ordinal.Stages, L.Axioms.Basic, L.Axioms.Infinity, L.Coding.Model, L.Coding.Expressions, L.Coding.Injection, L.Coding.Environment, L.Coding.EnvironmentSet, L.Choice.NameComparison, L.Choice.StageOrders, L.Choice.OrderTable, L.Choice.InternalWellOrder, L.WellOrder.Base, L.Recursion, L.Cardinal, L.InjectionComposition, L.DefinableInjection, L.GCH.CardinalSquareLaw, L.GCH.FiniteSequenceCoding, L.Ordinal.SquareLaw, L.Choice.FiniteStageOrders, L.GCH.OrderType]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/zh/L.GCH.StageCountingTools.md, https://bedrock.institute/ja/L.GCH.StageCountingTools.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# The counting tools for infinite constructible stages

Counting the stage `Lset δ` of an infinite ordinal `δ` inside `L` rests on two ingredients: a base injection `Lω ↪ ω`, and a way of lifting injections through finite environments. This chapter supplies both, and everything here is proved for exactly the constructs named in the text.

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

The chapter works under excluded middle at the fixed universe level. This hypothesis is inherited by the constructions used throughout; its clearest local roles are to search a finite-stage tally for a name and to compare a collapse value with `ω` by ordinal trichotomy.

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

All constructions therefore share the single hypothesis `lem : LEM (ℓ-suc ℓ)`. In particular, the finite search below is a consequence of excluded middle and does not invoke a choice principle.

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

The internal graphs used below must be described by formulas that `L` itself can interpret. Equality, membership, conjunction, implication, and bounded and unbounded quantifiers provide the language for saying that a relation is a total single-valued injection and for defining its action on finite environments.

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

There are two levels of data throughout the argument. A set in the cumulative hierarchy has a small presentation whose indices name its members, while an element of `L` also carries a proof of constructibility. Moving between these levels lets an internal graph act as an ordinary function on presentation indices.

```agda
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import V.Model {ℓ} using ( ∈sucV-inl; self∈sucV )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; #mono )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset→isL )
```

Ordinal structure enters twice. Numerals identify the finite domains of environments, while the order on constructible stages later gives a canonical well order of `Lset ω`. Trichotomy will then decide how each value of its ordinal collapse sits relative to `ω`.

```agda
open import L.Ordinal {ℓ} using ( ∈#-elim; mem-ord; ω-ord; numeral-ord; #∈ω )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
```

A coded injection is represented by a set of ordered pairs. Its four obligations say that the graph is single-valued, has exactly the stated domain, is injective on inputs, and takes values in the stated target. The first part of the chapter starts from such an actual coded graph.

```agda
open import L.Coding.Model {ℓ} using ( prʟ; prʟ-fst; svAt; svAt-in; svAt-out; domAt; domAt-in; domAt-out; domAt-intro; appAt; appAt-adequate; envOverAt; envOverAt-transport )
open import L.Coding.Expressions {ℓ} using ( numL )
open import L.Coding.Injection {ℓ} lem
  using ( injAt; injAt-in; injAt-out; module Small )
open import L.Coding.Environment {ℓ} using ( env; lookup-spec )
```

For each natural number `n`, the set of environments over `A` of length `n` has a concrete presentation. The union `seqL A` ranges over every finite length. Thus an entrywise map that preserves length is exactly the operation needed to map all finite sequences over `A` into those over `B`.

```agda
open import L.Coding.EnvironmentSet {ℓ} lem
  using ( Ix; envS; envSet-in; envSet-out; envOver; module Recover )
open import L.Choice.NameComparison {ℓ} lem using ( domAt-numeral; domAt-fill )
open import L.Choice.StageOrders {ℓ} lem
  using ( carry; memOf; orderAt; orderAt-step; relOf
```

The second part orders the members of `Lset ω` first by birth stage and then, when birth stages agree, by the local step order. This distinction matters: a predecessor may have the same birth stage as its successor, although every predecessor still lies in the successor of that common stage.

```agda
        ; birth-mem; module Family )
  renaming ( Mem to MemOf )
open import L.Choice.OrderTable {ℓ} lem using ( Related; IsRel; ixRel-rep; ixRel-fill )
open import L.Choice.InternalWellOrder {ℓ} lem using ( relL; relL-spec )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
```

Collapsing this well order assigns an ordinal to each member of `Lset ω`. The task is then to prove that every collapse value belongs to `ω`. The proof will bound one predecessor segment at a time by a finite constructible stage and rule out an injection of `ω` into that stage.

```agda
  using ( SWO; lt; eq; gt ) renaming ( Tri to TriW )
open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
```

Finite-sequence coding and the collapse argument meet in later cardinal calculations. The former transports an already given coded injection coordinatewise; the latter provides the base result `Lset ω ↪ ω`. Neither statement asserts a bijection or counts arbitrary infinite sequences.

```agda
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( isL-ord )
open import L.GCH.FiniteSequenceCoding {ℓ} lem using ( seqL; seqL-in; seqL-out )
open import L.Ordinal.SquareLaw {ℓ} lem using ( module FiniteBase )
open FiniteBase using ( fromFin; fromFin-inj )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate; ω-limit; finite-excl-ω )
```

A finite stage comes with a finite tally that lists all its members. Repetitions may occur, so the tally is a surjective naming device rather than a bijection. This is enough: excluded middle permits a bounded search for one name of each given member.

```agda
open import L.Choice.FiniteStageOrders {ℓ} lem
  using ( Tally; StageOrder; stageOrder; finiteStage )  -- lint-agda: keep (StageOrder used as the projection qualifier)
open import L.GCH.OrderType {ℓ} lem using ( Holds; module Code )
```

The chosen tally index places each member of a finite stage in a finite ordinal presentation. Composing a hypothetical injection from `ω` with this naming map, and then duplicating the result on the diagonal, contradicts the finite square exclusion theorem.

```agda
open import Cubical.Data.Nat.Order using ( _<_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.FinSet using ( DecΣ )
open import Cubical.Relation.Nullary using ( decRec; yes; no )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId'; inj-toℕ )
```

Several later equalities concern dependent pairs whose second components are proofs. Since those components are propositions, equality of the underlying sets determines equality of the packaged elements. This allows the argument to move cleanly between elements of `L`, their presentations, and their graph codes.

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Sum as Sum
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ2; isPropΠ3 )
```

Numerals have a second role besides marking environment lengths. Membership in `ω` says merely that an ambient set is equal to some numeral, while the proof keeps no globally chosen natural-number representative. Later eliminations respect this propositional character.

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; ω; sucV )
```

Existence in membership and graph readings is often retained only under propositional truncation `∥_∥₁`. Such a witness may be eliminated when the target is a proposition, or when uniqueness first makes the target type a proposition; the operation does not select arbitrary representatives.

```agda
open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

The same distinction applies to the final count. `InjL A B` retains only the proposition that some constructible graph codes an injection from `A` to `B`; it does not expose a globally selected host-level function.

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

By contrast, the sequence construction begins with a particular graph `E` and the full data `InjCode E A B`. Its host-level function can therefore be read from that graph and used coordinatewise before the resulting graph is hidden again by `InjL`.

```agda
module SV = hPropStructure 𝒮ᵥ using ()
```

Every entry read from a member of a constructible set is itself constructible, by transitivity of `L`. This elementary fact is what permits finite environments and the ordered pairs in their graphs to remain objects of the internal model.

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

Satisfaction notation connects the formula-level description of a graph with these ambient membership facts. Adequacy lemmas will be used in both directions, so the proof can build an internal formula from concrete graph data and later read that formula back.

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

For a natural number `k`, `nn k` packages the numeral `# k` with its proof of constructibility. These packaged numerals serve as the finite domain objects in satisfaction environments.

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

The graph formula below introduces several nested binders. Names `i0`, `i1`, and so on abbreviate their de Bruijn positions, with `i0` always denoting the most recently bound variable.

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

As binders are added, older variables shift to the next position. The typed abbreviations record those shifts once, so the formula can display its mathematical pattern without repeating long successor expressions.

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

The positions through `i6` will suffice to relate an input environment `s`, its image `y`, a common domain `n`, an index `i`, and the two entries connected by `E`.

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

Later formulas for coded injections require a few deeper positions. Extending the same naming scheme avoids changing the convention when those additional binders are introduced.

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

The last abbreviation completes the range needed in this module. These names carry no mathematical assumptions; they only keep the variable bookkeeping legible.

```agda
  i9 = suc i8
```

## Length and extensionality of environments

The first rigidity fact compares the lengths of two coded environments. If one underlying set equals both environments `env h` and `env h'`, with every entry constructible, then the two lengths are equal: the domain of a coded environment is its length numeral, and the two readings of the same set are identified by the numeral projections.

```agda
env-len : (E : S) {n n' : ℕ} (h : Fin n → V ℓ) (h' : Fin n' → V ℓ)
        → ((i : Fin n) → ⟨ isL (h i) ⟩) → ((i : Fin n') → ⟨ isL (h' i) ⟩)
        → fst E ≡ env h → fst E ≡ env h' → n ≡ n'
env-len E {n} {n'} h h' cg cg' q q' =
  #-inj′ (domAt-numeral (suc zero) zero (nn n ∷ E ∷ []) n' h' cg' q'
```

The proof fills the domain of the first presentation with the numeral of `n`, reads the same domain back as the numeral of `n'`, and applies the injectivity of numerals. The conclusion is only the equality of lengths, not an equality of the two presenting functions.

```agda
            (domAt-fill (suc zero) zero (nn n ∷ E ∷ []) n h cg q refl))
```

The second rigidity fact assumes that two columns already have the same length and their coded graphs are equal. Looking up the numeral key for an index in both graphs then recovers equality of the corresponding entries. The converse, constructing equality of graphs from pointwise equality, is proved later at the place where it is needed.

```agda
env-pt : {n : ℕ} (h h' : Fin n → V ℓ) → env h ≡ env h' → (i : Fin n) → h i ≡ h' i
env-pt h h' q i = subst ⟨_⟩ (lookup-spec h' i (h i))
  (subst (λ w → ⟨ pr (# (toℕ i)) (h i) ∈ w ⟩) q
    (subst ⟨_⟩ (sym (lookup-spec h i (h i))) refl))
```

## Lifting a coded injection to finite sequences

The lifting module is stated for a constructible graph `E` with four data: single-valuedness, totality on `A`, injectivity on `A`, and values in `B`. These are exactly the four clauses of a coded injection from `A` into `B`.

```agda
module SeqMap (A B E : S)
              (sv : ⟨ (E ∷ A ∷ []) ⊨ svAt zero ⟩)
              (dm : ⟨ (E ∷ A ∷ []) ⊨ domAt zero (suc zero) ⟩)
              (ij : ⟨ (E ∷ A ∷ []) ⊨ injAt zero ⟩)
              (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst E ⟩
```

The final range clause says only that every value occurring in `E` belongs to `B`. It does not require every member of `B` to occur, so the data describe an injection rather than a surjection or a bijection.

```agda
                   → ⟨ fst y ∈ fst B ⟩) where
```

The extraction machinery reads the internal graph as an actual function between the presentations of `A` and `B`: single-valuedness makes the fiber of each value a proposition, so the value can be recovered without any choice principle.

```agda
  module Sm = Small E A B sv dm ij ran using ( at; fib; small; small-inj; module E )
```

The extracted function is kept opaque: later arguments use it through its graph and its injectivity.

```agda
  opaque
    f : ⟪ fst A ⟫ → ⟪ fst B ⟫
    f = Sm.small
```

The graph record states that the pair of an index's presented element and the presented image belongs to `E`; it is transported from the term algebra's own graph record along the identification of the presented value.

```agda
    f-graph : (m : ⟪ fst A ⟫)
            → ⟨ pr (⟪ fst A ⟫↪ m) (⟪ fst B ⟫↪ (f m)) ∈ fst E ⟩
    f-graph m = subst (λ w → ⟨ pr (⟪ fst A ⟫↪ m) w ∈ fst E ⟩)
      (sym (Sm.fib m .snd)) (Sm.E.toFun-graph (Sm.at m))
```

The extracted function is injective on the presentation of `A`, which is the pointwise injectivity that the sequence lifting will inherit.

```agda
    f-inj : (m n : ⟪ fst A ⟫) → f m ≡ f n → m ≡ n
    f-inj = Sm.small-inj
```

An environment entry of `A` is read as an ambient set through the embedding of the presentation.

```agda
  vA : {n : ℕ} → Ix A n → Fin n → V ℓ
  vA g i = ⟪ fst A ⟫↪ (g i)
```

Likewise for the entries of `B`-environments.

```agda
  vB : {n : ℕ} → Ix B n → Fin n → V ℓ
  vB h i = ⟪ fst B ⟫↪ (h i)
```

The lifted assignment applies the extracted function entry by entry: the image of a length-`n` environment of `A` is a length-`n` environment of `B`, so lengths never change.

```agda
  fg : {n : ℕ} → Ix A n → Ix B n
  fg g i = f (g i)
```

Every entry of an `A`-environment is constructible, by transporting the membership in `A` along the transitivity of constructibility.

```agda
  isLA : {n : ℕ} (g : Ix A n) (i : Fin n) → ⟨ isL (vA g i) ⟩
  isLA g i = isL-trans (member (fst A) (g i)) (snd A)
```

Likewise for the entries of `B`-environments.

```agda
  isLB : {n : ℕ} (h : Ix B n) (i : Fin n) → ⟨ isL (vB h i) ⟩
  isLB h i = isL-trans (member (fst B) (h i)) (snd B)
```

For an index object `i`, `Ent y s i` says merely that there are model elements `u` and `v` such that `s(i)=u`, `y(i)=v`, and the graph `E` sends `u` to `v`. The witnesses and all three graph-membership facts are kept under propositional truncation.

```agda
  Ent : (y s i : S) → Type (ℓ-suc ℓ)
  Ent y s i = ∥ Σ[ u ∈ S ] Σ[ v ∈ S ]
      ( ⟨ pr (fst i) (fst u) ∈ fst s ⟩
      × ⟨ pr (fst i) (fst v) ∈ fst y ⟩
      × ⟨ pr (fst u) (fst v) ∈ fst E ⟩ ) ∥₁
```

The host reading `Wit y s` says merely that some object `n` is the domain of `s`, that `y` is an environment over the fixed target `B` with that same domain, and that every `i∈n` satisfies `Ent y s i`. Thus `y` has the same finite shape as `s`, and its entries are the pointwise `E`-images of those of `s`.

```agda
  Wit : (y s : S) → Type (ℓ-suc ℓ)
  Wit y s = ∥ Σ[ n ∈ S ]
      ( ⟨ (n ∷ y ∷ s ∷ []) ⊨ domAt i2 i0 ⟩
      × ⟨ (B ∷ n ∷ y ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩
      × ((i : S) → ⟨ fst i ∈ fst n ⟩ → Ent y s i) ) ∥₁
```

The entry formula expresses exactly the three equations hidden in `Ent`: two existentially bound values `u` and `v` satisfy `s(i)=u`, `y(i)=v`, and `E(u)=v`. The variable positions account for the surrounding parameters and the two new witnesses.

```agda
  opaque
    private
      entFo : Formula S 5
      entFo = ∃̇ (∃̇ ( appAt i6 i2 i1 ∧̇ appAt i5 i2 i0 ∧̇ appC E i1 i0 ))
```

The full formula first binds the common domain `n`, then binds an object `b` and requires it to equal the fixed constant `B`. It says that `y` is a `b`-environment on `n` and that the entry formula holds for every `i∈n`; the equality `b=B` makes this exactly an environment over the intended target.

```agda
    fo : Formula S 2
    fo = ∃̇ ( domAt i2 i0
           ∧̇ ∃̇ ( (var i0 ≐ con B)
                ∧̇ envOverAt i2 i1 i0
                ∧̇ ∀̇∈ (var i1) entFo ) )
```

To read an entry from the formula, the proof eliminates the two nested existential witnesses `u` and `v`. This elimination is valid because `Ent y s i` is itself a proposition under propositional truncation.

```agda
    private
      entOut : (y s n b i : S) → ⟨ (i ∷ b ∷ n ∷ y ∷ s ∷ []) ⊨ entFo ⟩ → Ent y s i
      entOut y s n b i = PT.rec squash₁ (λ { (u , hv) →
        PT.rec squash₁ (λ { (v , (h1 , (h2 , h3))) →
          let γ = v ∷ u ∷ i ∷ b ∷ n ∷ y ∷ s ∷ [] in
```

The adequacy laws for the two environment applications and for application of `E` convert formula satisfaction into the three ambient memberships. Packaging the recovered `u`, `v`, and these memberships produces the required truncated entry.

```agda
          ∣ u , v
          , ( subst ⟨_⟩ (appAt-adequate i6 i2 i1 γ) h1
            , subst ⟨_⟩ (appAt-adequate i5 i2 i0 γ) h2
            , subst ⟨_⟩ (appC-adequate E i1 i0 γ) h3 ) ∣₁ }) hv })
```

The reverse direction maps a truncated entry into satisfaction of the formula. It uses the same three adequacy equalities in reverse, turning the ambient graph memberships into the two environment-application clauses and the application clause for `E`.

```agda
      entIn : (y s n i : S) → Ent y s i → ⟨ (i ∷ B ∷ n ∷ y ∷ s ∷ []) ⊨ entFo ⟩
      entIn y s n i = PT.map (λ { (u , v , (h1 , h2 , h3)) →
        let γ = v ∷ u ∷ i ∷ B ∷ n ∷ y ∷ s ∷ [] in
        u , ∣ v , ( subst ⟨_⟩ (sym (appAt-adequate i6 i2 i1 γ)) h1
                  , subst ⟨_⟩ (sym (appAt-adequate i5 i2 i0 γ)) h2
```

After both witnesses are repackaged under the nested existential quantifiers, the graph-membership clause for `E` completes satisfaction of the entry formula. Hence `entOut` and `entIn` establish the exact correspondence needed for each index.

```agda
                  , subst ⟨_⟩ (sym (appC-adequate E i1 i0 γ)) h3 ) ∣₁ })
```

The body reader receives the three components exposed by the outer formula: `n` is the domain of `s`, the auxiliary object `b` has the same underlying set as `B`, and `y` is an environment over `b` on `n` whose every index satisfies the entry formula. It must convert these data into `Wit y s`.

```agda
      bodyOut : (y s n b : S)
              → ⟨ (n ∷ y ∷ s ∷ []) ⊨ domAt i2 i0 ⟩
              → fst b ≡ fst B
              → ⟨ (b ∷ n ∷ y ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩
              → ⟨ (b ∷ n ∷ y ∷ s ∷ []) ⊨ ∀̇∈ (var i1) entFo ⟩
```

The equality between the underlying sets of `b` and `B` transports the environment-over assertion from `b` to the fixed target `B`. Each bounded instance of the entry formula is read by `entOut`, and the common domain together with these two components is then packaged under propositional truncation.

```agda
              → Wit y s
      bodyOut y s n b hd eb he hS =
        ∣ n , ( hd
              , envOverAt-transport (b ∷ n ∷ y ∷ s ∷ []) (B ∷ n ∷ y ∷ s ∷ [])
                  i2 i1 i0 i2 i1 i0 refl refl eb he
```

The bounded universal clause is used pointwise: for each `i∈n`, `entOut` turns its satisfaction proof into `Ent y s i`. Together with the domain equation and the transported environment condition, these entries form the three components of the truncated witness `Wit y s`.

```agda
              , λ i i∈n → entOut y s n b i (hS i i∈n) ) ∣₁
```

To read the whole graph formula outward, we first eliminate the truncated witness `n`, then the truncated witness `b`. Their accompanying clauses give the domain condition, the equality `fst b ≡ fst B`, the environment condition, and the bounded step condition; `bodyOut` turns exactly these data into `Wit y s`. The eliminations are legitimate because `Wit y s` is itself propositionally truncated.

```agda
    fo-out : (y s : S) → ⟨ (y ∷ s ∷ []) ⊨ fo ⟩ → Wit y s
    fo-out y s = PT.rec squash₁ (λ { (n , (hd , hb)) →
      PT.rec squash₁ (λ { (b , (eb , (he , hS))) → bodyOut y s n b hd eb he hS }) hb })
```

Conversely, a host-level witness supplies the outer existential with `n` and the inner existential with the fixed element `B`. Reflexivity proves that this element denotes the required target, while `entIn` converts every pointwise entry back into the bounded formula. Together, `fo-out` and `fo-in` establish the adequacy of `fo` for `Wit`.

```agda
    fo-in : (y s : S) → Wit y s → ⟨ (y ∷ s ∷ []) ⊨ fo ⟩
    fo-in y s = PT.rec (snd ((y ∷ s ∷ []) ⊨ fo))
      (λ { (n , (hd , he , hS)) →
        ∣ n , ( hd , ∣ B , ( refl , he , λ i i∈n → entIn y s n i (hS i i∈n) ) ∣₁ ) ∣₁ })
```

Fix a sequence `g` of length `N` over `A`, a carrier element `s`, and an equation identifying the underlying set of `s` with the environment graph of `g`. This concrete representation lets us construct the coordinatewise image and then prove that any output satisfying the same graph formula has the same underlying set.

```agda
  module AtSeq (N : ℕ) (g : Ix A N) (s : S) (e : fst s ≡ fst (envS A g)) where
```

The intended output is the environment graph of the coordinatewise image `fg g`. At index `j`, its value is `f (g j)`, so the source and target sequences have the same finite length and corresponding entries are related by the input graph `E`.

```agda
    y₀ : S
    y₀ = envS B (fg g)
```

The next lemma exposes the elementary membership fact needed to build this witness: each coordinate pair occurs in the graph of an environment. It remains local because the public result of the subsection is the existence and uniqueness of the whole image environment.

```agda
    private
```

The entry lemma says that the coded graph of a function contains the ordered pair of each natural index with its value. The proof is by the specification of the environment constructor: the pair is there by definition.

```agda
      at : {k : ℕ} (h : Fin k → V ℓ) (j : Fin k)
         → ⟨ pr (# (toℕ j)) (h j) ∈ env h ⟩
      at h j = subst ⟨_⟩ (sym (lookup-spec h j (h j))) refl
```

The canonical image satisfies the host predicate `Wit`: the numeral `nn N` records the common domain, `he` records that `y₀` is an environment over `B` of that length, and `step` verifies the relation at every index below `N`. These three clauses are then placed under propositional truncation, preserving existence without exposing a chosen decomposition later.

```agda
    wit : Wit y₀ s
    wit = ∣ nn N , ( hd , he , step ) ∣₁
      where
      hd : ⟨ (nn N ∷ y₀ ∷ s ∷ []) ⊨ domAt i2 i0 ⟩
      hd = domAt-fill i2 i0 (nn N ∷ y₀ ∷ s ∷ []) N (vA g) (isLA g) e refl
```

The fact `envOver B (fg g)` is initially stated in the shorter environment containing `B`, `nn N`, and `y₀`. The transport lemma moves this same formula to the longer assignment that also contains `s`; the three reflexivity proofs say that the slots used by the formula still contain exactly the same elements. Hence adding the unused source sequence does not change the environment-over assertion.

```agda
      he : ⟨ (B ∷ nn N ∷ y₀ ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩
      he = envOverAt-transport (B ∷ nn N ∷ y₀ ∷ []) (B ∷ nn N ∷ y₀ ∷ s ∷ [])
             i2 i1 i0 i2 i1 i0 refl refl refl (envOver B (fg g))
```

The step clause at each position is proved by eliminating the numeral membership into a bounded natural number. The eliminated data names a specific index whose value is available in both sequences.

```agda
      step : (i : S) → ⟨ fst i ∈ # N ⟩ → Ent y₀ s i
      step i i∈N = PT.map atIndex (∈#-elim N (fst i) i∈N)
        where
        atIndex : Σ[ k ∈ ℕ ] ((k < N) × (fst i ≡ # k))
                → Σ[ u ∈ S ] Σ[ v ∈ S ]
```

For the recovered finite index `j`, the required entry consists of the source value `vA g j`, the target value `vB (fg g) j`, and three graph memberships: the source environment stores the first value at `j`, the target environment stores the second there, and `E` relates the first value to the second. Constructibility proofs turn both values into elements of the carrier `S`.

```agda
                    ( ⟨ pr (fst i) (fst u) ∈ fst s ⟩
                    × ⟨ pr (fst i) (fst v) ∈ fst y₀ ⟩
                    × ⟨ pr (fst u) (fst v) ∈ fst E ⟩ )
        atIndex (k , p , ei) =
            (vA g j , isLA g j) , (vB (fg g) j , isLB (fg g) j)
```

The environment-entry lemma supplies the first two memberships, transported along the equation that identifies the given position with the numeral for `j` and, for the source, along the presentation equation `e`. The graph theorem `f-graph` supplies the third. The finite index `j` is defined immediately below from the bounded natural number obtained in the preceding step.

```agda
          , ( subst2 (λ a w → ⟨ pr a (vA g j) ∈ w ⟩) (sym qi) (sym e) (at (vA g) j)
            , subst (λ a → ⟨ pr a (vB (fg g) j) ∈ fst y₀ ⟩) (sym qi) (at (vB (fg g)) j)
            , f-graph (g j) )
          where
          j : Fin N
```

The internal index `j` is constructed from the bounded natural number by the finite decoding, and the numeral equation composes the membership transport with the recovery of the index value.

```agda
          j = fromℕ' N k p
          qi : fst i ≡ # (toℕ j)
          qi = ei ∙ cong #_ (sym (toFromId' N k p))
```

Uniqueness starts with an arbitrary candidate `y` satisfying `Wit y s` and aims to prove equality of its underlying set with that of `y₀`. The truncated witness may be eliminated because equality in the cumulative hierarchy is a proposition. Once its three clauses are exposed, the local module `Only` derives the desired equality from them.

```agda
    only : (y : S) → Wit y s → fst y ≡ fst y₀
    only y = PT.rec (setIsSet (fst y) (fst y₀))
      (λ { (n , (hd , he , hS)) → Only.final n hd he hS })
      where
      module Only (n : S)
```

The inner module collects the three clauses of the witness: the domain condition, the environment-over condition, and the step clause at every position.

```agda
                  (hd : ⟨ (n ∷ y ∷ s ∷ []) ⊨ domAt i2 i0 ⟩)
                  (he : ⟨ (B ∷ n ∷ y ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩)
                  (hS : (i : S) → ⟨ fst i ∈ fst n ⟩ → Ent y s i) where
```

The numeral equation identifies the unknown length with the known length `N`, by the adequacy of the domain coding.

```agda
        qn : fst n ≡ # N
        qn = domAt-numeral i2 i0 (n ∷ y ∷ s ∷ []) N (vA g) (isLA g) e hd
```

The environment condition and the recovered length determine an index function `gR : Ix B N` whose graph presents the candidate `y`. This definition is opaque because its construction eliminates truncated data; subsequent reasoning uses the recovered function through its stated equations rather than unfolding that elimination.

```agda
        opaque
          gR : Ix B N
          gR = Recover.g B N (B ∷ n ∷ y ∷ s ∷ []) i2 i1 i0 qn refl he
```

Recovery also proves that the underlying set of `y` is the environment graph generated by `gR`. This equation replaces the arbitrary presentation in the witness by a fixed-length coordinate presentation, so uniqueness can now be checked one coordinate at a time.

```agda
          gR-eq : fst y ≡ fst (envS B gR)
          gR-eq = Recover.recovers B N (B ∷ n ∷ y ∷ s ∷ []) i2 i1 i0 qn refl he
```

At each index `j`, the step clause yields, under propositional truncation, a source value, a candidate target value, and the three graph memberships relating them. The target equality is a proposition, so `PT.rec` may pass these data to `read`. That lemma proves equality of the represented values; injectivity of the presentation of `B` then gives `gR j ≡ fg g j`.

```agda
        pt : (j : Fin N) → gR j ≡ fg g j
        pt j = ↪-inj {a = fst B} (PT.rec (setIsSet _ _) read (hS (nn (toℕ j)) j∈n))
          where
          j∈n : ⟨ # (toℕ j) ∈ fst n ⟩
          j∈n = subst (λ w → ⟨ # (toℕ j) ∈ w ⟩) (sym qn) (#mono (toℕ j) N (toℕ<n j))
```

The reading lemma states what the step clause provides: two elements and three memberships, identifying the argument in the source sequence, the value in the unknown environment, and the relation fact connecting them through the coded pairing.

```agda
          read : Σ[ u ∈ S ] Σ[ v ∈ S ]
                   ( ⟨ pr (# (toℕ j)) (fst u) ∈ fst s ⟩
                   × ⟨ pr (# (toℕ j)) (fst v) ∈ fst y ⟩
                   × ⟨ pr (fst u) (fst v) ∈ fst E ⟩ )
               → vB gR j ≡ vB (fg g) j
```

The equation of the source argument is recovered by the lookup specification of the source environment, transported along the identifying equation.

```agda
          read (u , v , (hu , hv , hE)) = sym qv ∙ qv'
            where
            qu : fst u ≡ vA g j
            qu = subst ⟨_⟩ (lookup-spec (vA g) j (fst u))
                   (subst (λ w → ⟨ pr (# (toℕ j)) (fst u) ∈ w ⟩) e hu)
```

The candidate value `v` has two descriptions. Looking it up in the recovered environment gives `fst v ≡ vB gR j`. On the other hand, `hE` says that `E` relates the recovered source argument to `v`; after identifying that argument with `vA g j`, single-valuedness of `E` compares this edge with `f-graph (g j)` and yields `fst v ≡ vB (fg g) j`.

```agda
            qv : fst v ≡ vB gR j
            qv = subst ⟨_⟩ (lookup-spec (vB gR) j (fst v))
                   (subst (λ w → ⟨ pr (# (toℕ j)) (fst v) ∈ w ⟩) gR-eq hv)
            qv' : fst v ≡ vB (fg g) j
            qv' = svAt-out zero (E ∷ A ∷ []) sv u v (vB (fg g) j , isLB (fg g) j) hE
```

The final equation composes the function-graph fact with the reversed argument equation, completing the identification of the two image values.

```agda
                    (subst (λ w → ⟨ pr w (vB (fg g) j) ∈ fst E ⟩) (sym qu) (f-graph (g j)))
```

It remains to pass from coordinatewise agreement to equality of the two environment graphs. The desired path begins with the recovered presentation of `y` and ends at the canonical graph `y₀`.

```agda
        final : fst y ≡ fst y₀
```

Function extensionality turns `pt` into equality of the two index functions. Applying `envS B` along that path identifies their environment graphs, and composing with `gR-eq` proves `fst y ≡ fst y₀`. The path-lambda expression is the direct cubical action of the environment graph along this equality.

```agda
        final = gR-eq ∙ λ i → fst (envS B (funExt pt i))
```

Membership in the sequence set is stated as a type so that the argument can carry it alongside each element.

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem s = ⟨ fst s ∈ˢ fst (seqL A) ⟩
```

A representation is the truncated record of a length, an index function and the equation identifying the two presentations. The truncated form is what `seqL-out` supplies.

```agda
  Rep : S → Type (ℓ-suc ℓ)
  Rep s = ∥ Σ[ n ∈ ℕ ] Σ[ g ∈ Ix A n ] (fst s ≡ fst (envS A g)) ∥₁
```

Starting from membership in `seqL A`, `seqL-out` gives a propositionally truncated length `n` together with membership in the corresponding fixed-length environment set. For that `n`, `envSet-out` gives a truncated index function and presentation equation. Mapping and eliminating only into the truncated target combines the two stages without choosing a global representation.

```agda
  rep : (s : S) → Mem s → Rep s
  rep s m = PT.rec squash₁
    (λ { (n , hn) → PT.map (λ { (g , e) → n , g , e }) (envSet-out A n s hn) })
    (seqL-out A s m)
```

The recursion package uses `seqL A` as its domain and `fo` as its graph. For every member `s`, a truncated representation of `s` determines the canonical image environment; `AtSeq.wit` proves that this image satisfies the graph, while `AtSeq.only` proves that every other satisfying value has the same underlying set. Thus the graph is total and single-valued in the sense required by `mereFunct`.

```agda
  R : Recursion
  R = record
    { dom   = seqL A
    ; graph = fo
    ; funct = λ s m → mereFunct fo s (PT.map (λ { (n , g , e) →
```

For a concrete representation `(n , g , e)`, the functionality witness consists of the canonical image `AtSeq.y₀`, its proof of satisfying `fo`, and the proof that every other satisfying carrier element is equal to it. `Σ≡Prop` lifts equality of underlying sets to equality in `S`, since constructibility proofs form proposition-valued fibres. `PT.map` then keeps the whole construction under truncation.

```agda
        AtSeq.y₀ n g s e
        , ( fo-in (AtSeq.y₀ n g s e) s (AtSeq.wit n g s e)
          , λ y' h → Σ≡Prop (λ v → snd (isL v)) (AtSeq.only n g s e y' (fo-out y' s h)) ) })
        (rep s m)) }
```

The recursion table machinery is opened, supplying the actual function, its values, and the uniqueness of values.

```agda
  module T = Of R using ( funct; val; val-uniq )
```

The resulting value `fn s m` is the unique carrier element satisfying `fo` at `s`; although its construction starts from a truncated representation of `s`, uniqueness makes the value independent of which length and index function represent that sequence.

```agda
  fn : (s : S) → Mem s → S
  fn = T.val
```

Whenever `s` is presented by a length `n` and an index function `g`, the computed value `fn s m` equals the canonical coordinatewise image `AtSeq.y₀ n g s e`. Both values satisfy the recursion graph at `s`, so the uniqueness theorem `T.val-uniq` supplies the equality. This equation will let later proofs reason from any available presentation of `s`.

```agda
  fn-code : (s : S) (m : Mem s) (n : ℕ) (g : Ix A n) (e : fst s ≡ fst (envS A g))
          → fn s m ≡ AtSeq.y₀ n g s e
  fn-code s m n g e =
    T.val-uniq s m (AtSeq.y₀ n g s e) (fo-in (AtSeq.y₀ n g s e) s (AtSeq.wit n g s e))
```

Membership in the target sequence set is proved by transporting along the code equation and applying the inward reading of the target sequence set.

```agda
  into : (s : S) (m : Mem s) → ⟨ fst (fn s m) ∈ˢ fst (seqL B) ⟩
  into s m = PT.rec (snd (fst (fn s m) ∈ˢ fst (seqL B)))
    (λ { (n , g , e) → subst (λ w → ⟨ fst w ∈ˢ fst (seqL B) ⟩) (sym (fn-code s m n g e))
           (seqL-in B n (envS B (fg g)) (envSet-in B (fg g))) })
    (rep s m)
```

These facts define a map from `seqL A` to `seqL B`: `fo` gives its graph, `fn` gives its unique value at each source member, and `into` proves that this value is again a finite sequence over `B`. The remaining task is to show that equality of two values forces equality of their source sequences.

```agda
  D : DefinableMap
  D = record
    { dom = seqL A ; cod = seqL B ; fn = fn ; into = into ; graph = fo
    ; defines = λ s m → T.funct s m .fst .snd
    ; only    = λ s m y h → sym (T.val-uniq s m y h) }
```

To prove injectivity, it suffices first to compare canonical presentations. Suppose two coordinatewise image environments are equal, although their displayed lengths may differ. The helper `same` recovers equality of the lengths, transports the second source sequence to the common finite index type, and then uses injectivity of `f` at every coordinate to prove equality of the source environment graphs.

```agda
  private
    same : (n : ℕ) (g : Ix A n) (n' : ℕ) (g' : Ix A n')
         → fst (envS B (fg g)) ≡ fst (envS B (fg g'))
         → fst (envS A g) ≡ fst (envS A g')
    same n g n' g' q =
```

The equality of the two target environment graphs determines equality of their finite lengths by `env-len`, because the coded domain of an environment is its numeral length. Substitution along that equality reduces the problem to two sequences indexed by the same `Fin n`; the local family `P` records the statement that remains after this alignment.

```agda
      subst P (env-len (envS B (fg g)) (vB (fg g)) (vB (fg g')) (isLB (fg g)) (isLB (fg g')) refl q)
        base g' q
      where
      P : ℕ → Type (ℓ-suc ℓ)
      P k = (h : Ix A k) → fst (envS B (fg g)) ≡ fst (envS B (fg h))
```

With a common length, `env-pt` reads equality of the target graphs as equality of their values at each index. Injectivity of the presentation of `B` turns this into equality `f (g j) ≡ f (h j)`, and `f-inj` recovers `g j ≡ h j`. Function extensionality then identifies the source index functions, hence their environment graphs.

```agda
          → fst (envS A g) ≡ fst (envS A h)
      base : P n
      base h q' = λ i → fst (envS A (funExt (λ j →
        f-inj (g j) (h j) (↪-inj {a = fst B} (env-pt (vB (fg g)) (vB (fg h)) q' j))) i))
```

For arbitrary members `s` and `s'`, their representations are available only under propositional truncation. The desired equality `fst s ≡ fst s'` is a proposition because cumulative-hierarchy values form a set, so `PT.rec2` may expose one representation of each input locally and pass them to the canonical comparison.

```agda
  inj : (s : S) (m : Mem s) (s' : S) (m' : Mem s')
      → fst (fn s m) ≡ fst (fn s' m') → fst s ≡ fst s'
  inj s m s' m' q = PT.rec2 (setIsSet (fst s) (fst s'))
    (λ { (n , g , e) (n' , g' , e') →
        e
```

The code equations identify the actual outputs `fn s m` and `fn s' m'` with their respective canonical image environments. Composing these identifications with the assumed output equality gives the hypothesis required by `same`; finally, the presentation equations `e` and `e'` transfer the resulting equality of source environment graphs back to `fst s ≡ fst s'`.

```agda
      ∙ same n g n' g'
          (sym (cong fst (fn-code s m n g e)) ∙ q ∙ cong fst (fn-code s' m' n' g' e'))
      ∙ sym e' })
    (rep s m) (rep s' m')
```

The injectivity just proved upgrades the definable map to an internal coded injection `seqL A ↪ seqL B`. Its graph still records the same coordinatewise action; the conclusion retains only the propositional existence of a suitable code.

```agda
  injL : InjL (seqL A) (seqL B)
  injL = Inj.injL D inj
```

The exported theorem starts from an actual code `E` witnessing an injection from `A` to `B`: it is single-valued, has domain `A`, is injective, and has range contained in `B`. Passing these four components to `SeqMap` yields the propositionally truncated existence of a coded injection from `seqL A` to `seqL B`. The result concerns finite sequences of arbitrary length, not infinite sequences.

```agda
seq-map : (A B E : S) → InjCode E A B → InjL (seqL A) (seqL B)
seq-map A B E (sv , dm , ij , ran) = SeqMap.injL A B E sv dm ij ran
```

## Pinning a quantified variable to a constant

The pinning formula binds one existential to fix a free slot to a chosen constant: it says merely that some value equals the constant and satisfies the inner formula.

```agda
pinAt : ∀ {n} → S → Formula S (suc n) → Formula S n
pinAt c φ = ∃̇ ((var zero ≐ con c) ∧̇ φ)
```

The inward reading exhibits the constant as the witness and the body satisfaction at the extended environment.

```agda
pin-in : ∀ {n} (c : S) (φ : Formula S (suc n)) (γ : S ^ n)
       → ⟨ (c ∷ γ) ⊨ φ ⟩ → ⟨ γ ⊨ pinAt c φ ⟩
pin-in c φ γ h = ∣ c , (refl , h) ∣₁
```

For the outward direction, the existential supplies a carrier element `z`, an equality of its underlying set with that of `c`, and a proof of the body at `z`. Since constructibility is proposition-valued, `Σ≡Prop` lifts the underlying-set equality to an equality `z ≡ c` in `S`; transport along it gives satisfaction at the pinned environment. Elimination from propositional truncation is valid because formula satisfaction is a proposition.

```agda
pin-out : ∀ {n} (c : S) (φ : Formula S (suc n)) (γ : S ^ n)
        → ⟨ γ ⊨ pinAt c φ ⟩ → ⟨ (c ∷ γ) ⊨ φ ⟩
pin-out c φ γ = PT.rec (snd ((c ∷ γ) ⊨ φ))
  (λ { (z , (ez , h)) → subst (λ v → ⟨ (v ∷ γ) ⊨ φ ⟩) (Σ≡Prop (λ v → snd (isL v)) ez) h })
```

## A formula for coded injections into a fixed target

An `InjCode F a b` consists of four proposition-valued conditions: single-valuedness of `F`, the assertion that its domain is `a`, injectivity of its graph, and containment of its values in `b`. Formula satisfaction is proposition-valued, and the last condition is a dependent function into membership propositions, so their nested product is again a proposition.

```agda
isPropInjCode : (F a b : S) → isProp (InjCode F a b)
isPropInjCode F a b =
  isProp× (snd ((F ∷ a ∷ []) ⊨ svAt zero))
    (isProp× (snd ((F ∷ a ∷ []) ⊨ domAt zero (suc zero)))
      (isProp× (snd ((F ∷ a ∷ []) ⊨ injAt zero))
```

The remaining range condition quantifies over an argument, a value, and a proof that the graph relates them. Its conclusion is membership of the value in `b`, which is a proposition; repeated dependent products therefore preserve propositionality and complete the proof for `InjCode`.

```agda
        (isPropΠ3 (λ _ y _ → snd (fst y ∈ fst b)))))
```

Only the underlying sets represented by the graph and domain arguments matter to `InjCode`. Because constructibility proofs are propositions, equalities `fst F ≡ fst F'` and `fst a ≡ fst a'` lift uniquely to equalities in `S`; two-variable substitution then transports an injection code from `(F , a)` to `(F' , a')`, while the target `b` remains fixed.

```agda
injcode-resp : (F F' a a' b : S) → fst F ≡ fst F' → fst a ≡ fst a'
             → InjCode F a b → InjCode F' a' b
injcode-resp F F' a a' b qF qa = subst2 {x = F} {y = F'} {z = a} {w = a'}
  (λ E A → InjCode E A b)
  (Σ≡Prop (λ v → snd (isL v)) qF) (Σ≡Prop (λ v → snd (isL v)) qa)
```

The formula `injFo b f B` expresses the four conditions of an injection code using the graph in slot `f` and the domain in slot `B`. The graph is single-valued, has exactly that domain, and is injective; moreover, whenever it relates an argument to a value, that value belongs to the fixed target `b`. The last clause gives range containment, rather than surjectivity onto `b`.

```agda
injFo : ∀ {n} → S → Fin n → Fin n → Formula S n
injFo b f B = svAt f ∧̇ domAt f B ∧̇ injAt f
            ∧̇ ∀̇ (∀̇ (appAt (suc (suc f)) i1 i0 ⇒̇ (var i0 ∈̇ con b)))
```

To prove the reading laws for `injFo`, fix the target `b`, the two relevant slots `f` and `B`, and an assignment `γ`. The local names `F` and `A` denote the carrier elements found in those slots. The following arguments can then state the result directly as an `InjCode F A b`, keeping the bookkeeping of variable lookup out of the mathematical statement.

```agda
module InjFo {n : ℕ} (b : S) (f B : Fin n) (γ : S ^ n) where
  private
    F A : S
    F = lookup f γ
    A = lookup B γ
```

The reading lemma turns satisfaction of the injection formula into the four clauses of an injection code. For the domain clause, a graph witness for an input is eliminated from propositional truncation into the proposition that the input belongs to `A`; conversely, membership in `A` produces the required domain witness.

```agda
  read : ⟨ γ ⊨ injFo b f B ⟩ → InjCode F A b
  read (sv , dm , ij , ran) =
      svAt-in zero (F ∷ A ∷ []) (λ x y y' p q → svAt-out f γ sv x y y' p q)
    , domAt-intro zero (suc zero) (F ∷ A ∷ []) (λ x →
          (λ h → PT.rec (snd (fst x ∈ fst A))
```

Single-valuedness and injectivity are transferred by reading their semantic clauses at `γ` and rebuilding the corresponding clauses for the two-entry environment `(F,A)`. The range condition uses adequacy of application to turn graph membership in `F` into the application atom expected by the formula, after which its last clause yields membership of the value in the fixed target `b`.

```agda
                   (λ { (y , p) → domAt-out f B γ dm x y p }) h)
        , (λ hx → domAt-in f B γ dm x hx))
    , injAt-in zero (F ∷ A ∷ []) (λ y x x' p q → injAt-out f γ ij y x x' p q)
    , λ x y p → ran x y (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) i1 i0 (y ∷ x ∷ γ))) p)
```

The filling lemma is the converse construction: from the four data of a coded injection it builds the satisfaction of the injection formula, this time reading all atoms over the structure in which the formula is stated.

```agda
  fill : InjCode F A b → ⟨ γ ⊨ injFo b f B ⟩
  fill (sv , dm , ij , ran) =
      svAt-in f γ (λ x y y' p q → svAt-out zero (F ∷ A ∷ []) sv x y y' p q)
    , domAt-intro f B γ (λ x →
          (λ h → PT.rec (snd (fst x ∈ fst A))
```

For totality, a truncated graph witness is eliminated only into the proposition that the input lies in `A`, while membership in `A` supplies a witness in the other direction. The remaining clauses rebuild single-valuedness and injectivity at `γ`, and application adequacy converts the range hypothesis into the final formula clause. Together, `read` and `fill` give both directions between formula satisfaction and the four injection-code conditions.

```agda
                   (λ { (y , p) → domAt-out zero (suc zero) (F ∷ A ∷ []) dm x y p }) h)
        , (λ hx → domAt-in zero (suc zero) (F ∷ A ∷ []) dm x hx))
    , injAt-in f γ (λ y x x' p q → injAt-out zero (F ∷ A ∷ []) ij y x x' p q)
    , λ x y p → ran x y (subst ⟨_⟩ (appAt-adequate (suc (suc f)) i1 i0 (y ∷ x ∷ γ)) p)
```

## Reducing the infinite-stage count to `L_ω`

The stage at the infinite ordinal `ω` is presented as a constructible set: the ordinal stage `Lset ω` together with its ordinalness is packaged by the stage presentation.

```agda
Lω : S
Lω = LsetS ω ω-ord
```

The goal of the section is then stated as a type: an internal coded injection from the constructible presentation of `Lset ω` into the internal `ω`. This is the base case on which the counting of larger stages is built.

```agda
LimitStageCounted : Type (ℓ-suc ℓ)
LimitStageCounted = InjL Lω ωʟ
```

The move lemma transports a coded internal injection along equalities of the underlying source and target sets. The source equality gives an inclusion from the new source `a'` into the old source `a`; after the given injection is applied, the target equality gives an inclusion from the old target `b` into the new target `b'`. Composing these three injections yields `InjL a' b'`.

```agda
move : (a a' b b' : S) → fst a ≡ fst a' → fst b ≡ fst b' → InjL a b → InjL a' b'
move a a' b b' qa qb h =
  injl-trans a' a b' (inclusion-coded a' a (λ z hz → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym qa) hz))
    (injl-trans a b b' h (inclusion-coded b b' (λ z hz → subst (λ w → ⟨ z ∈ˢ w ⟩) qb hz)))
```

## The base count: `L_ω` injects into `ω`

The exclusion argument works with finite stages of the form `Lset (# n)`, and begins by taking the tally of such a finite stage: an indexed enumeration of its members.

```agda
private
  module FinNo (n : ℕ) where
    t : Tally (finiteStage n)
    t = StageOrder.tally (stageOrder n)
```

The tally supplies its size, its member at each index, and the covering fact that every member appears at some index.

```agda
    open Tally t using ( size; item; onto )
```

The search lemma names a member: for each member `x` of the finite stage it runs a decidable search through the finitely many indices, comparing each entry with `x` by excluded middle, and returns an index whose entry is `x`. The search returns some index; it does not claim that index to be unique, and it is a finitary decision on a finite family rather than an appeal to any choice principle.

```agda
    named : (x : V ℓ) → ⟨ x ∈ˢ finiteStage n ⟩ → Σ[ i ∈ Fin size ] (item i ≡ x)
    named x hx = decRec (λ q → q) (λ nq → Empty.rec (PT.rec Empty.isProp⊥ nq (onto x hx)))
      (DecΣ size (λ i → item i ≡ x)
        (λ i → Sum.rec yes no (lem ((item i ≡ x) , setIsSet (item i) x))))
```

Suppose that `f` injected the presentation of `ω` into a finite stage. Each value `f x` can be assigned a tally index `q x`; duplicating that index gives the map `x ↦ (q x,q x)` required by the finite exclusion theorem. Equality of these pairs forces equality of the corresponding values of `f`, and then injectivity of `f` forces equality of the original inputs.

```agda
    noinj : (f : ⟪ ω ⟫ → ⟪ Lset (# n) ⟫)
          → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → Empty.⊥
    noinj f finj = finite-excl-ω (# size) (numeral-ord size) (#∈ω size)
      (λ x → q x , q x) (λ x y e → finj x y (qq x y (cong fst e)))
      where
```

The auxiliary map reads each value of `f` as an ambient element, certifies that it belongs to the finite stage, and names it by the finite index found above.

```agda
      vl : ⟪ ω ⟫ → V ℓ
      vl x = ⟪ Lset (# n) ⟫↪ (f x)
      mm : (x : ⟪ ω ⟫) → ⟨ vl x ∈ˢ finiteStage n ⟩
      mm x = member (Lset (# n)) (f x)
      q : ⟪ ω ⟫ → ⟪ # size ⟫
```

The map `q` converts the chosen tally index into the corresponding element of the finite ordinal presentation `⟪# size⟫`. If two such names agree, injectivity of that presentation makes their natural-number indices equal, so the two tally entries agree. The presentation of `Lset (# n)` then turns this ambient equality back into equality of the two values of `f`.

```agda
      q x = fromFin size (toℕ (named (vl x) (mm x) .fst) , toℕ<n (named (vl x) (mm x) .fst))
      qq : (x y : ⟪ ω ⟫) → q x ≡ q y → f x ≡ f y
      qq x y e = ↪-inj {a = Lset (# n)}
        (sym (named (vl x) (mm x) .snd)
          ∙ cong item (inj-toℕ (cong fst (fromFin-inj size _ _ e)))
```

The chain of identifications is closed by the named entry of the second point, completing the proof that equal names force equal values.

```agda
          ∙ named (vl y) (mm y) .snd)
```

For an arbitrary index `w`, `NoInto w` is the proposition that no host-level injection exists from the presentation of `ω` into the presentation of `Lset w`. The next lemma will establish this proposition under the additional hypothesis that `w` belongs to `ω`.

```agda
  NoInto : V ℓ → Type ℓ
  NoInto w = (f : ⟪ ω ⟫ → ⟪ Lset w ⟫)
           → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → Empty.⊥
```

The general form follows by transporting the finite case along the membership of `g` in `ω`: a member of `ω` is, merely, a numeral, and the transport moves the whole exclusion statement to the stage of that numeral. The elimination is legitimate because the target is a contradiction.

```agda
  no-inj-fin : (g : V ℓ) → ⟨ g ∈ˢ ω ⟩ → NoInto g
  no-inj-fin g g∈ω = PT.rec (isPropΠ2 (λ _ _ → Empty.isProp⊥))
    (λ { (k , e) → subst NoInto e (FinNo.noinj (lower k)) }) g∈ω
```

The infinite ordinal `ω` is constructible: its ordinalness feeds the ordinal stage construction.

```agda
hω : ⟨ isL ω ⟩
hω = isL-ord ω ω-ord
```

The stage order of `Lset ω` is implemented as a constructible set `Rω` of coded pairs inside `L`.

```agda
Rω : SL.S
Rω = relL ω hω ω-ord
```

The relation specification says that the coded pairs of `Rω` are exactly the ordered pairs of `L`-elements related by the stage order.

```agda
specω : IsRel ω Rω
specω = relL-spec ω hω ω-ord
```

The endpoint condition recovers stage membership for both endpoints of every related pair. Unfolding the coded pair yields two members of `Lset ω`, and the component equations identify their underlying sets with the endpoints `y` and `x`.

```agda
Rsub : (y x : SL.S) → Holds Rω y x
     → ⟨ fst y ∈ˢ Lset ω ⟩ × ⟨ fst x ∈ˢ Lset ω ⟩
Rsub y x h = PT.rec isP
  (λ { (_ , h₁) → PT.rec isP
    (λ { (a , h₂) → PT.rec isP
```

Both memberships are transported along the two component equations supplied by the injectivity of the ordered-pair coding.

```agda
      (λ { (b , (q , _)) →
             subst (λ w → ⟨ w ∈ˢ Lset ω ⟩) (sym (pr-inj q .fst)) (a .snd)
           , subst (λ w → ⟨ w ∈ˢ Lset ω ⟩) (sym (pr-inj q .snd)) (b .snd) })
      h₂ })
    h₁ })
```

The conjunction of the two memberships is a proposition, and the relatedness of the coded pair is produced from the relation specification at the constructible ordered pair.

```agda
  rel
  where
  isP : isProp (⟨ fst y ∈ˢ Lset ω ⟩ × ⟨ fst x ∈ˢ Lset ω ⟩)
  isP = isProp× (snd (fst y ∈ˢ Lset ω)) (snd (fst x ∈ˢ Lset ω))
  rel : ⟨ Related ω (pr (fst y) (fst x)) ⟩
```

The relatedness is transported along the identification of the coded pair with the plain ordered pair of the two underlying sets.

```agda
  rel = subst (λ w → ⟨ Related ω w ⟩) (prʟ-fst y x)
    (specω (prʟ y x) .fst
      (subst (λ w → ⟨ w ∈ˢ fst Rω ⟩) (sym (prʟ-fst y x)) h))
```

The order-type machinery is instantiated at the stage `Lset ω` with the internal relation and its endpoint condition: this fixes the small domain, the internal relation, and the collapse construction of the previous chapter.

```agda
module OT = Code Lω Rω Rsub using ( module Conjuncts; Dom; _≺_; isProp≺; ≺-in; ≺-out )
```

The host well order is the stage order carried to the presentation of `Lset ω`, so the abstract well-order machinery can be used on the small index type.

```agda
Wω : SWO ⟪ Lset ω ⟫
Wω = carry (Lset ω) (orderAt ω ω-ord)
```

Write `a <ω b` for the strict comparison supplied by this well order on the presentation of `Lset ω`. The next two lemmas show that this relation and the internally coded predecessor relation `a OT.≺ b` express the same comparison.

```agda
open SWO Wω using () renaming ( _<∙_ to _<ω_ )
```

The internal relation and the host stage order agree on the common presentation. The first direction reads an internal predecessor proof `a OT.≺ b` as the host-order comparison `a <ω b`, using the representation theorem for the coded relation.

```agda
≺→< : (a b : OT.Dom) → a OT.≺ b → a <ω b
≺→< a b k = ixRel-rep ω ω-ord Rω specω a b (OT.≺-out a b k)
```

Conversely, the filling theorem for the coded relation turns a host-order comparison `a <ω b` into the internal predecessor proof `a OT.≺ b`. These two conversions let the order-theoretic properties of the host relation be transferred to the internal one.

```agda
<→≺ : (a b : OT.Dom) → a <ω b → a OT.≺ b
<→≺ a b k = OT.≺-in a b (ixRel-fill ω ω-ord Rω specω a b k)
```

Well-foundedness of the internal relation follows from well-foundedness of the host order. Accessibility is transported point by point: each predecessor inside the internal relation is first converted into a host predecessor.

```agda
wfω : WellFounded OT._≺_
wfω m = go (SWO.wf∙ Wω m)
  where
  go : {n : OT.Dom} → Acc _<ω_ n → Acc OT._≺_ n
  go {n} (acc r) = acc (λ n' k → go (r n' (≺→< n' n k)))
```

Transitivity of the internal relation is likewise transported through the host order: two consecutive internal steps are converted, composed, and converted back.

```agda
transω : {a b c : OT.Dom} → a OT.≺ b → b OT.≺ c → a OT.≺ c
transω {a} {b} {c} k k' =
  <→≺ a c (SWO.trans∙ Wω a b c (≺→< a b k) (≺→< b c k'))
```

For any `a` and `b`, trichotomy of the host well order gives exactly one of three forms: `a <ω b`, equality, or `b <ω a`. The result is expressed as a nested sum so that each comparison can be converted into the matching case for the internal relation.

```agda
triω : (a b : OT.Dom) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
triω a b = go (SWO.tri∙ Wω a b)
  where
  go : TriW (a <ω b) (a ≡ b) (b <ω a)
     → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
```

Each host case is converted back into the corresponding internal case: less-than, equality, or greater-than.

```agda
  go (lt h) = inl (<→≺ a b h)
  go (eq e) = inr (inl e)
  go (gt h) = inr (inr (<→≺ b a h))
```

Well-foundedness and transitivity now define the collapse values and their ordinal image `otL`. Trichotomy proves that distinct points have distinct collapse values, so the collapse graph `colTable` satisfies the injectivity clause and yields the code used below.

```agda
module C = OT.Conjuncts wfω transω using ( module Inj; col; col-ord; col-out; colTable; otL; otL-out )
module I = C.Inj triω using ( code; col-inj )
```

The birth-stage family is instantiated at the internal `ω`: every presented member of `Lset ω` has a birth stage in `ω`, ordered by a family relation.

```agda
private
  module F = Family ω (λ δ _ → orderAt δ) ω-ord using ( _≺_; bornAt )
```

The unfolded reading of the family relation is proved: at `ω`, the abstractly stated order equals the concrete birth-stage-then-step order.

```agda
  unfoldω : (a b : MemOf (Lset ω))
          → relOf (orderAt ω ω-ord) a b ≡ F._≺_ a b
  unfoldω a b = cong (λ z → relOf (z ω-ord) a b) (orderAt-step ω)
```

The birth stage of a member is read as an ambient set.

```agda
  bAt : MemOf (Lset ω) → V ℓ
  bAt a = F.bornAt a .fst
```

Every birth stage belongs to the internal `ω`, since the whole family lives below `ω`.

```agda
  bAt∈ω : (a : MemOf (Lset ω)) → ⟨ bAt a ∈ˢ ω ⟩
  bAt∈ω a = F.bornAt a .snd
```

Every birth stage is an ordinal: it is a member of the ordinal `ω`, and members of ordinals are ordinals.

```agda
  bAt-ord : (a : MemOf (Lset ω)) → IsOrd (bAt a)
  bAt-ord a = mem-ord {A = ω} ω-ord (bAt a) (bAt∈ω a)
```

Every presented member of `Lset ω` belongs to the stage indexed by its own birth stage raised by one: the member's constructibility is transported into that successor stage.

```agda
  self-at : (a : MemOf (Lset ω)) → ⟨ a .fst ∈ˢ Lset (sucV (bAt a)) ⟩
  self-at a = birth-mem (a .fst) (Lset→isL ω ω-ord (a .fst) (a .snd))
```

The step bound says: if `a` precedes `b` in the family order, then the underlying set of `a` belongs to the stage indexed by one plus the birth stage of `b`. In the strictly earlier birth case, the successor comparison is decided by ordinal linearity.

```agda
  step-bound : (a b : MemOf (Lset ω)) → F._≺_ a b
             → ⟨ a .fst ∈ˢ Lset (sucV (bAt b)) ⟩
  step-bound a b (inl h) =
    raise (suc∈or≡ (bAt a) (bAt b) (bAt-ord a) (bAt-ord b) h)
    where
```

In the strictly earlier-birth branch, ordinal discreteness compares `sucV (bAt a)` directly with `bAt b`. If the successor still lies below `bAt b`, or is equal to it, stage monotonicity carries the known membership of `a` in `Lset (sucV (bAt a))` into `Lset (sucV (bAt b))`.

```agda
    raise : ⟨ sucV (bAt a) ∈ˢ bAt b ⟩ ⊎ (sucV (bAt a) ≡ bAt b)
          → ⟨ a .fst ∈ˢ Lset (sucV (bAt b)) ⟩
    raise (inl k) = Lset-mono {α = sucV (bAt b)} {β = sucV (bAt a)}
      (∈sucV-inl {A = bAt b} {x = sucV (bAt a)} k) (self-at a)
    raise (inr e) = Lset-mono {α = sucV (bAt b)} {β = sucV (bAt a)}
```

In the equality subcase `sucV (bAt a) ≡ bAt b`, the proof first places this ordinal in the successor of `bAt b` and then applies stage monotonicity. The other main branch has equal birth stages; there the step-order witness itself contains membership of `a` in the successor stage of their common birth stage, and transport along the equality gives the stated bound.

```agda
      (subst (λ w → ⟨ sucV (bAt a) ∈ˢ sucV w ⟩) e (self∈sucV (sucV (bAt a))))
      (self-at a)
  step-bound a b (inr (e , u)) =
    subst (λ w → ⟨ a .fst ∈ˢ Lset (sucV w) ⟩) (sym e) (u .fst)
```

Every point of the internal collapse domain is read as a presented member of `Lset ω`.

```agda
  atIx : OT.Dom → MemOf (Lset ω)
  atIx m = ⟪ Lset ω ⟫↪ m , memOf (Lset ω) m
```

For a collapse-domain point `p`, the guard index `gOf p` is the successor of the birth stage of the member represented by `p`. The finite stage `Lset (gOf p)` will contain every predecessor of `p`.

```agda
  gOf : OT.Dom → V ℓ
  gOf p = sucV (bAt (atIx p))
```

Every guard belongs to the internal `ω`, since it is the successor of a member of `ω`.

```agda
  gOf∈ω : (p : OT.Dom) → ⟨ gOf p ∈ˢ ω ⟩
  gOf∈ω p = ω-limit (bAt (atIx p)) (bAt∈ω (atIx p))
```

The predecessor bound says that every predecessor `r` of a point `p` presents an ambient element of the finite stage guarded by `p`. The proof transports the step bound through the unfolded reading of the family order.

```agda
  seg-bound : (p r : OT.Dom) → r OT.≺ p
            → ⟨ ⟪ Lset ω ⟫↪ r ∈ˢ Lset (gOf p) ⟩
  seg-bound p r k =
    step-bound (atIx r) (atIx p) (transport (unfoldω (atIx r) (atIx p)) (≺→< r p k))
```

A predecessor segment records a predecessor `r` of `p` together with the identification of its collapse value with a given set.

```agda
private
  Seg : OT.Dom → V ℓ → Type (ℓ-suc ℓ)
  Seg p b = Σ[ r ∈ OT.Dom ] ((r OT.≺ p) × (C.col r ≡ b))
```

Predecessor segments are propositions: two records with the same collapse value are identified because the collapse is injective on the small domain, the relation is proposition-valued, and the underlying sets form an h-set.

```agda
  isPropSeg : (p : OT.Dom) (b : V ℓ) → isProp (Seg p b)
  isPropSeg p b (r , _ , e) (r' , _ , e') =
    Σ≡Prop (λ z → isProp× (OT.isProp≺ z p) (setIsSet _ _))
      (I.col-inj r r' (e ∙ sym e'))
```

Every membership in a collapse value yields a predecessor segment: the truncated reading of the collapse is eliminated into the proposition-valued segment.

```agda
  seg : (p : OT.Dom) (b : V ℓ) → ⟨ b ∈ˢ C.col p ⟩ → Seg p b
  seg p b h = PT.rec (isPropSeg p b) (λ z → z) (C.col-out p b h)
```

It remains to show that each ordinal `C.col p` lies below `ω`. Ordinal trichotomy leaves two obstructing possibilities, equality with `ω` and membership of `ω` in the collapse. Both will imply the same inclusion `ω ⊆ C.col p`, so we first prove that such an inclusion would force an impossible injection into the finite stage `Lset (gOf p)`.

```agda
col-fin : (p : OT.Dom) → ⟨ C.col p ∈ˢ ω ⟩
col-fin p = go (ord-tri (C.col p) (C.col-ord p) ω ω-ord)
  where
  refute : ((z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ C.col p ⟩) → Empty.⊥
  refute sub = no-inj-fin (gOf p) (gOf∈ω p) f f-inj
```

Assume for contradiction that every element of `ω` belongs to `C.col p`. For a presented element `x` of `ω`, membership in the collapse yields a predecessor `r ≺ p` whose collapse value is the set presented by `x`. The type `Seg` of such predecessors is a proposition, so `seg` may eliminate the truncated membership evidence and `s x` records this uniquely determined predecessor. The bound on the segment places the set represented by `r`, rather than its collapse value, in `Lset (gOf p)`; `fb x` chooses its canonical presentation there.

```agda
    where
    s : (x : ⟪ ω ⟫) → Seg p (⟪ ω ⟫↪ x)
    s x = seg p (⟪ ω ⟫↪ x) (sub (⟪ ω ⟫↪ x) (member ω x))
    fb : (x : ⟪ ω ⟫)
       → Σ[ m ∈ ⟪ Lset (gOf p) ⟫ ] (⟪ Lset (gOf p) ⟫↪ m ≡ ⟪ Lset ω ⟫↪ (s x .fst))
```

Thus `f` sends each presented element of `ω` to the presentation, in the common finite stage, of its recovered predecessor. To prove this map injective, suppose `f x = f y`. Equality of these finite-stage indices first gives equality of the sets represented by the two predecessors. The remaining path calculation then recovers equality of the original elements `x` and `y`.

```agda
    fb x = fiber (Lset (gOf p)) (seg-bound p (s x .fst) (s x .snd .fst))
    f : ⟪ ω ⟫ → ⟪ Lset (gOf p) ⟫
    f x = fb x .fst
    f-inj : (x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y
    f-inj x y e = ↪-inj {a = ω}
```

Presentation injectivity turns equality of the two values of `f` into equality `rr` of the recovered predecessor indices in `Lset ω`. Applying the collapse function to `rr`, and composing with the equations stored in `s x` and `s y`, shows that the sets presented by `x` and `y` are equal. Injectivity of the presentation of `ω` then gives `x = y`. Hence the assumed inclusion `ω ⊆ C.col p` would produce an injection from `ω` into the finite stage `Lset (gOf p)`.

```agda
      (sym (s x .snd .snd) ∙ cong C.col rr ∙ s y .snd .snd)
      where
      rr : s x .fst ≡ s y .fst
      rr = ↪-inj {a = Lset ω}
        (sym (fb x .snd) ∙ cong ⟪ Lset (gOf p) ⟫↪ e ∙ fb y .snd)
```

Ordinal trichotomy compares `C.col p` with `ω`. If the collapse is already a member of `ω`, the desired conclusion is immediate. If `C.col p = ω`, transport along that equality makes every element of `ω` an element of the collapse. This is precisely the inclusion refuted above, since it would yield the impossible injection into `Lset (gOf p)`.

```agda
  go : ⟨ C.col p ∈ˢ ω ⟩ ⊎ ((C.col p ≡ ω) ⊎ ⟨ ω ∈ˢ C.col p ⟩) → ⟨ C.col p ∈ˢ ω ⟩
  go (inl k) = k
  go (inr (inl e)) =
    Empty.rec (refute (λ z z∈ω → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈ω))
  go (inr (inr ω∈c)) =
```

In the remaining case `ω ∈ C.col p`. Since `C.col p` is an ordinal and therefore transitive, every element of `ω` then belongs to `C.col p`. This again supplies the forbidden inclusion and closes the last trichotomy branch. Consequently every collapse value `C.col p` is a member of `ω`.

```agda
    Empty.rec (refute (λ z z∈ω → C.col-ord p .fst z∈ω ω∈c))
```

The order-type image is therefore contained in `ω`. Its outward reading supplies, under propositional truncation, an index `b` and an equation identifying a given image member `z` with `C.col b`. Because the target assertion `z∈ω` is a proposition, this witness may be eliminated there; transport of `col-fin b` along the equation proves the required membership. This establishes only `C.otL ⊆ ω`, not the reverse inclusion.

```agda
otL⊆ω : (z : V ℓ) → ⟨ z ∈ˢ fst C.otL ⟩ → ⟨ z ∈ˢ ω ⟩
otL⊆ω z h = PT.rec (snd (z ∈ˢ ω))
  (λ { (b , e) → subst (λ w → ⟨ w ∈ˢ ω ⟩) e (col-fin b) })
  (C.otL-out z h)
```

The collapse table gives a coded injection from `L_ω` into its image `C.otL`, and the proved containment gives a coded inclusion from `C.otL` into `ωʟ`. Their composition yields `limit-stage-counted : InjL Lω ωʟ`. Thus the formal conclusion is the propositionally retained existence of an internal injection `L_ω ↪ ω`; no surjection, bijection, or equality `C.otL=ω` is asserted. Later stage counts use this result as their base injection.

```agda
limit-stage-counted : LimitStageCounted
limit-stage-counted =
  injl-trans Lω C.otL ωʟ ∣ C.colTable , I.code ∣₁
    (inclusion-coded C.otL ωʟ otL⊆ω)
```