---
title: "Coding finite sequences below an infinite ordinal"
module: L.GCH.FiniteSequenceCoding
lang: en
site: "Bedrock"
description: "Coding finite sequences below an infinite ordinal"
stage: "Proving GCH"
reading_order: 114
canonical: https://bedrock.institute/en/L.GCH.FiniteSequenceCoding.html
html: L.GCH.FiniteSequenceCoding.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/FiniteSequenceCoding.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Presentation, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Infinity, L.Axioms.Full, L.Coding.Model, L.Coding.Expressions, L.Coding.Injection, L.Coding.Environment, L.Coding.EnvironmentSet, L.Recursion, L.Cardinal, L.InjectionComposition, L.GCH.CardinalRepresentative, L.DefinableInjection, L.GCH.CardinalSquareLaw]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/zh/L.GCH.FiniteSequenceCoding.md, https://bedrock.institute/ja/L.GCH.FiniteSequenceCoding.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Coding finite sequences below an infinite ordinal

Finite parameter lists must be counted by sets that exist inside `L`. This chapter first collects all finite sequences over a constructible set as one constructible set. For an infinite ordinal `α`, it then folds each sequence through an internal injection from `α × α` to `α`, attaches the length as a final tag, and proves an internal injection from the sequence set into `α`. The result is an upper bound only: it neither covers every element of `α` nor defines a decoder on all of `α`.

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

The construction is classical only through an explicit excluded-middle hypothesis. In particular, propositionally truncated witnesses remain truncated unless uniqueness makes their witness type a proposition; no choice principle is used to select arbitrary sequence representations or injection graphs.

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

Fix a universe level `ℓ` and excluded middle at level `ℓ-suc ℓ`. Every construction below, from separation to the cardinal square law used at the end, is relative to this one named hypothesis, so the final sequence bound carries exactly the same assumption.

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

Two descriptions of the same objects will be used throughout. At the object-language level, equality, conjunction, and bounded or unbounded quantification describe sequence graphs and recursive traces inside `L`. At the host level, presentations turn membership in a set into small indices, while regularity later supports the well-founded argument behind the square law.

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

The coding relies on two rigid families of set codes. Ordered-pair injectivity recovers both coordinates from an equality of pair codes, and von Neumann numerals faithfully record natural numbers and their order inside `ω`. Transitivity of constructibility keeps every member of a constructible ordinal inside `L`, so these ambient codes can be used as elements of the constructible model.

```agda
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; #mono )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd )
open import L.Ordinal {ℓ} using ( #∈ω; ∈#-elim )
open import L.Axioms.Basic {ℓ} using ( extensionalL )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
```

The set-theoretic graphs used here must be visible to first-order reasoning in `L`. Separation forms the exact subcollections, while adequacy for pairs, graph application, domains, and environments identifies each object-language clause with its intended relation between underlying sets. This bridge will later turn a host recursive fold into an internal definable graph.

```agda
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-out; domAt; domAt-in; domAt-out; domAt-intro; appAt; appAt-adequate; envOverAt; envOver-sv; envOver-dom; envOverAt-transport )
open import L.Coding.Expressions {ℓ} using ( numL; sucAtL; sucAtL-adequate )
open import L.Coding.Injection {ℓ} lem using ( injAt; module Extract )
open import L.Coding.Environment {ℓ} using ( lookup-spec )
```

A finite sequence is represented by an environment graph with a numeral as its exact domain. For each fixed length, the environment-set construction collects precisely those graphs and reads a member back only under propositional truncation. The recursion machinery will nevertheless produce an actual value once the graph formula has a unique output, and coded-injection composition will carry the resulting bounds between constructible sets.

```agda
open import L.Coding.EnvironmentSet {ℓ} lem
  using ( Ix; envS; envOver; envSet; envSet-in; envSet-out; module Recover )
open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct; smallDom )
open import L.Cardinal {ℓ} lem using ( InjL; IsCardinalL )
open import L.InjectionComposition {ℓ} lem using ( injl-trans )
```

The final counting argument need not assume that the given infinite ordinal is already a cardinal. It first passes to a cardinal representative, uses the square law there to compress pairs, and composes back into the original ordinal. The present chapter then turns that pair compression into a definable injection for finite sequences.

```agda
open import L.GCH.CardinalRepresentative {ℓ} lem using ( cardOf )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
open import L.GCH.CardinalSquareLaw {ℓ} lem
  using ( prodL; prodL-in; Goal; module Step; prod-inj; no-fin; ω⊆ )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )
```

Lengths live as natural numbers, positions as elements of `Fin n`, and internal domain markers as numerals. Moving between these three views requires order facts such as `toℕ i < n` and the inverse conversion from a number below `n` to a finite index. Equality of dependent pairs is controlled by their data component because the accompanying membership proofs are propositions.

```agda
open import Cubical.Data.Nat.Order
  using ( _<_; ≤-refl; ≤-suc; suc-≤-suc; pred-≤-pred; ¬-<-zero; <-split; zero-≤ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )
open import Cubical.Data.Sigma using ( Σ≡Prop )
```

The injectivity proof repeatedly separates two possibilities for an index below a successor: it lies below the predecessor, or it is the last index. Propositional extensionality then converts two membership implications into equality of sets, and the cumulative hierarchy supplies the sets and their canonical presentations on which these arguments run.

```agda
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
```

Von Neumann numerals and their successor operation connect finite lengths with the internal set `ω`. An impossible finite bound is expressed by the empty type, while well-founded induction enters only in the later construction of pair compression from the cardinal square law, not in the elementary recursion that folds a given finite sequence.

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

Propositional truncation records that a representation exists while deliberately forgetting which representation was supplied. Its eliminator is used only when the target is itself a proposition, such as membership or equality of sets. This restriction is the reason the chapter can prove existence and injectivity without silently choosing a length, an assignment, or an internal graph.

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

At the ambient level, membership is proposition-valued. This matters whenever a truncated witness is eliminated into a membership claim: no data are selected, and only the truth of membership survives.

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

Write `SV` for the proposition-valued structure on the ambient cumulative hierarchy. It provides the outer notion of membership used to compare pair codes, numerals, and set-theoretic graphs before they are regarded as constructible objects.

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

Write `S` for the carrier of the constructible structure `SL`. An element of `S` is an ambient set together with evidence that it lies in `L`; consequently every sequence set, graph, and ordinal used by the internal injection has an actual constructible representative.

```agda
module SL = hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )
open SL using ( S )
```

Formulas with constants from `S` are evaluated in the constructible structure, while their atomic content can also be read after projection to ambient sets. Transitivity of `L` makes these readings agree, allowing an object-language graph condition to justify the ambient membership equations used in the fold.

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

The numeral `nn k` packages the ambient von Neumann numeral together with its constructibility proof. Numerals mark the exact domains of finite environments; zero also supplies the initial accumulator and the harmless out-of-range value of `ext`; and the length numeral tags the completed fold. These roles keep finite indices visible inside the constructible model.

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

## Collecting all finite sequences over a set

A sequence over `A` is, at the host level, a function from a finite ordinal into the presentation of `A`; the small index type collects a length and such a function. This is the host-level notion; its set-coded counterpart is defined below.

```agda
SeqIx : S → Type ℓ
SeqIx A = Σ[ n ∈ ℕ ] Ix A n
```

The small-domain principle gives one constructible set that contains every environment graph over `A`, of every finite length. This is only a common container: the exact collection is carved out by separation below, and nothing is claimed about the container being precisely the image.

```agda
private
  amb : (A : S) → S
  amb A = smallDom (SeqIx A) (λ p → envS A (snd p)) .fst
```

For a particular length `n` and assignment `g`, the graph `envS A g` lies in the common container. This inclusion supplies the ambient half of separation membership; the defining formula will supply the exact finite-environment condition.

```agda
  amb-in : (A : S) (p : SeqIx A) → ⟨ fst (envS A (snd p)) ∈ˢ fst (amb A) ⟩
  amb-in A = smallDom (SeqIx A) (λ p → envS A (snd p)) .snd
```

The one-variable formula says that the candidate `x` is an environment graph over `A` whose domain is some member of the internal `ω`. The bounded witness is therefore only known at first to be an element of `ω`; recovering an actual natural length from it is a later, propositionally truncated step.

```agda
seqFo : S → Formula S 1
seqFo A = ∃̇∈ (con ωʟ) (∃̇ ( (var zero ≐ con A)
                        ∧̇ envOverAt (suc (suc zero)) (suc zero) zero ))
```

Separation now removes the surplus elements of the common container. The resulting set `seqL A` contains exactly those container elements satisfying the finite-environment description. Keeping the definition opaque affects normalization only; the mathematical content is fixed by the membership equation that follows.

```agda
opaque
  seqL : S → S
  seqL A = hasSeparationL (amb A) (seqFo A) .fst .fst
```

An element belongs to `seqL A` precisely when it both lies in the common container and satisfies `seqFo A`. Thus the container establishes set-sizedness, while the formula establishes exactness; neither part alone characterizes the set of all finite sequences.

```agda
  seqL-spec : (A x : S) → (x SL.∈ˢ seqL A)
            ≡ ((x SL.∈ˢ amb A) ⊓ ((x ∷ []) ⊨ seqFo A))
  seqL-spec A = hasSeparationL (amb A) (seqFo A) .fst .snd
```

Every member of an environment set of length `n` belongs to `seqL A`. The proof reads the truncated presentation of the member and then introduces it into the separated set.

```agda
seqL-in : (A : S) (n : ℕ) (x : S)
        → ⟨ fst x ∈ˢ fst (envSet A n) ⟩ → ⟨ fst x ∈ˢ fst (seqL A) ⟩
seqL-in A n x hx = PT.rec (snd (fst x ∈ˢ fst (seqL A))) from (envSet-out A n x hx)
  where
  from : Σ[ g ∈ Ix A n ] (fst x ≡ fst (envS A g)) → ⟨ fst x ∈ˢ fst (seqL A) ⟩
```

The member is transported to its graph form, which is a member of the container by the bounding record; the description is then satisfied by the canonical entry.

```agda
  from (g , e) = subst (λ w → ⟨ w ∈ˢ fst (seqL A) ⟩) (sym e) canonical
    where
    canonical : ⟨ fst (envS A g) ∈ˢ fst (seqL A) ⟩
    canonical = subst ⟨_⟩ (sym (seqL-spec A (envS A g)))
      ( amb-in A (n , g)
```

The description's witness consists of the numeral of the length, its membership in the internal `ω`, and the graph relation of the environment over `A`, all packaged in the truncated existential.

```agda
      , ∣ nn n , (#∈ω n , ∣ A , (refl , envOver A g) ∣₁) ∣₁ )
```

Conversely, membership in `seqL A` yields only the propositionally truncated assertion that some natural length `n` makes the member an element of `envSet A n`. The argument discards the container component of the separation equation and reads the existential information from the defining formula; it does not choose a length uniformly for all members.

```agda
seqL-out : (A x : S) → ⟨ fst x ∈ˢ fst (seqL A) ⟩
         → ∥ Σ[ n ∈ ℕ ] ⟨ fst x ∈ˢ fst (envSet A n) ⟩ ∥₁
seqL-out A x hx = PT.rec squash₁ step1 (subst ⟨_⟩ (seqL-spec A x) hx .snd)
  where
  step2 : (d : S) (k : ℕ) → # k ≡ fst d
```

Inside one branch of the truncated witnesses, suppose the domain object `d` has been identified with the numeral `# k`, the base object `b` with `A`, and `x` satisfies the environment condition. For these fixed witnesses, recovery produces an assignment of length `k` and identifies `x` with its graph. The outer result is truncated again, so this local construction does not define a global decoder.

```agda
        → Σ[ b ∈ S ] ((fst b ≡ fst A)
             × ⟨ (b ∷ d ∷ x ∷ []) ⊨ envOverAt (suc (suc zero)) (suc zero) zero ⟩)
        → ∥ Σ[ n ∈ ℕ ] ⟨ fst x ∈ˢ fst (envSet A n) ⟩ ∥₁
  step2 d k q (b , eb , hov) =
    ∣ k , subst (λ w → ⟨ w ∈ˢ fst (envSet A k) ⟩) (sym R.recovers) (envSet-in A R.g) ∣₁
```

For the fixed length `k`, the environment clauses determine each entry uniquely: exactness of the domain gives mere existence, single-valuedness makes the entry fiber a proposition, and the value restriction places the recovered value in the presentation of `A`. Extensionality, using also the clause that every graph member has pair shape, then identifies the whole set `x` with the canonical environment graph.

```agda
    where
    module R = Recover A k (b ∷ d ∷ x ∷ []) (suc (suc zero)) (suc zero) zero
                 (sym q) eb hov using ( g; recovers )
```

The remaining step eliminates the membership of the domain in `ω`: a member of `ω` is, merely, a numeral.

```agda
  step1 : Σ[ d ∈ S ] (⟨ fst d ∈ˢ ω ⟩
            × ∥ Σ[ b ∈ S ] ((fst b ≡ fst A)
                 × ⟨ (b ∷ d ∷ x ∷ []) ⊨ envOverAt (suc (suc zero)) (suc zero) zero ⟩) ∥₁)
        → ∥ Σ[ n ∈ ℕ ] ⟨ fst x ∈ˢ fst (envSet A n) ⟩ ∥₁
  step1 (d , d∈ω , h) = PT.rec squash₁
```

The numeral is fed into the conversion step, completing the reading direction. Note the strength: the length and the environment are recovered only within the truncation, and no global decoder from `seqL A` to assignments is produced.

```agda
    (λ { (k , q) → PT.rec squash₁ (step2 d (lower k) q) h }) d∈ω
```

## Folding a finite sequence into one ordinal code

The coding module fixes the data of the pairing function. Its parameters are an ordinal `α`, a proof that `α` is not a member of `ω` (the form of infinitude used here), and a constructible graph `F` together with three clauses: single-valuedness, totality on the product, and injectivity.

```agda
module Code (α : S) (oα : IsOrd (fst α)) (α∉ω : ⟨ fst α ∈ˢ ω ⟩ → Empty.⊥)
            (F : S)
            (sv : ⟨ (F ∷ prodL α ∷ []) ⊨ svAt zero ⟩)
            (dm : ⟨ (F ∷ prodL α ∷ []) ⊨ domAt zero (suc zero) ⟩)
            (ij : ⟨ (F ∷ prodL α ∷ []) ⊨ injAt zero ⟩)
```

The last hypothesis is the range condition in meta-level form: every value recorded by the graph belongs to `α`. Together the four clauses say that `F` is an internal coded injection from the product `α × α` into `α`.

```agda
            (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩
                 → ⟨ fst y ∈ fst α ⟩) where
```

The carrier of inputs and values is the type of constructible sets together with membership in `α`: an entry of the product must lie in `α`, and so must every value.

```agda
  M : Type (ℓ-suc ℓ)
  M = Σ[ v ∈ S ] ⟨ fst v ∈ˢ fst α ⟩
```

Numerals become elements of the carrier: since `α` is not in `ω`, the infinitude of `α` places every numeral inside `α`. This is the only use of the infinitude hypothesis in the fold.

```agda
  num : ℕ → M
  num k = nn k , ω⊆ (fst α) oα α∉ω (# k) (#∈ω k)
```

Presentation indices of `α` also become elements of the carrier, with constructibility transported along the membership of `α` and membership witnessed by the presentation.

```agda
  up : ⟪ fst α ⟫ → M
  up m = (⟪ fst α ⟫↪ m , isL-trans (member (fst α) m) (snd α)) , member (fst α) m
```

Single-valuedness together with the exact-domain clause turns the graph `F` into an actual host function on members of `prodL α`. Domain membership initially gives only a truncated output, but the fiber of possible outputs is a proposition, so its unique value can be extracted. The separate hypothesis `ij` is still needed to conclude that equal outputs have equal inputs.

```agda
  module E = Extract F (prodL α) sv dm using ( toFun; toFun-graph; toFun-inj )
```

The coded pair of two carrier elements belongs to the product: both coordinates are in `α`, and the pair operation transports this into membership in `prodL α`.

```agda
  opaque
    pairMem : (a u : M) → ⟨ fst (prʟ (fst a) (fst u)) ∈ˢ fst (prodL α) ⟩
    pairMem a u = subst (λ w → ⟨ w ∈ˢ fst (prodL α) ⟩) (sym (prʟ-fst (fst a) (fst u)))
                    (prodL-in α (fst a) (fst u) (snd a) (snd u))
```

For an input `x` already known to belong to `prodL α`, define `val x` to be the unique output recorded by `F` at `x`. The membership proof is part of the input because the graph is required to be total exactly on the product, not on every constructible set.

```agda
  opaque
    val : (x : S) → ⟨ fst x ∈ˢ fst (prodL α) ⟩ → S
    val x mx = E.toFun (x , mx)
```

The graph record states that the pair of the input and the value belongs to `F`, which is the data the later identification lemmas consume.

```agda
    val-graph : (x : S) (mx : ⟨ fst x ∈ˢ fst (prodL α) ⟩)
              → ⟨ pr (fst x) (fst (val x mx)) ∈ fst F ⟩
    val-graph x mx = E.toFun-graph (x , mx)
```

The graph is injective on the product: two points with equal values have equal underlying sets. Together with the extraction, this is the injectivity half of the pairing function.

```agda
    val-inj : (x : S) (mx : ⟨ fst x ∈ˢ fst (prodL α) ⟩)
              (x' : S) (mx' : ⟨ fst x' ∈ˢ fst (prodL α) ⟩)
            → fst (val x mx) ≡ fst (val x' mx') → fst x ≡ fst x'
    val-inj x mx x' mx' = E.toFun-inj ij (x , mx) (x' , mx')
```

The binary operation `app a u` evaluates `F` at the internal ordered pair of `a` and `u`. Its value is already a constructible set because it comes from the graph fiber, and the range clause supplies the additional proof that this value lies in `α`. Hence `app` is closed on the carrier `M`.

```agda
  opaque
    app : M → M → M
    app a u = val (prʟ (fst a) (fst u)) (pairMem a u)
            , ran (prʟ (fst a) (fst u)) (val (prʟ (fst a) (fst u)) (pairMem a u))
                (val-graph (prʟ (fst a) (fst u)) (pairMem a u))
```

Evaluation does not lose contact with the internal graph. The theorem `app-graph` records that the pair whose input is the ambient code of `(a,u)` and whose output is `app a u` belongs to `F`. The projection equation for the constructible pair supplies the needed identification of the two input codes.

```agda
    app-graph : (a u : M)
              → ⟨ pr (pr (fst (fst a)) (fst (fst u))) (fst (fst (app a u))) ∈ fst F ⟩
    app-graph a u = subst (λ w → ⟨ pr w (fst (fst (app a u))) ∈ fst F ⟩)
                      (prʟ-fst (fst a) (fst u))
                      (val-graph (prʟ (fst a) (fst u)) (pairMem a u))
```

If two applications have equal outputs, injectivity of `F` first identifies their encoded pair inputs. Injectivity of the ordered-pair code then separates this equality into equality of the two first coordinates and equality of the two second coordinates. Thus one application layer can be peeled off without constructing an inverse to `F`.

```agda
    app-inj : (a u a' u' : M) → fst (fst (app a u)) ≡ fst (fst (app a' u'))
            → (fst (fst a) ≡ fst (fst a')) × (fst (fst u) ≡ fst (fst u'))
    app-inj a u a' u' e = pr-inj
      (sym (prʟ-fst (fst a) (fst u))
       ∙ val-inj (prʟ (fst a) (fst u)) (pairMem a u) (prʟ (fst a') (fst u')) (pairMem a' u') e
```

The comparison of pair inputs passes from constructible pair codes to their ambient Kuratowski codes and back. After these transports, pair injectivity yields exactly the two component equalities required by `app-inj`; no equality of the accompanying membership proofs is needed.

```agda
       ∙ prʟ-fst (fst a') (fst u'))
```

The companion uniqueness fact runs in the forward direction. If `F` records some value `w` at the pair `(a,u)`, then `w` must equal the already extracted value `app a u`. This is functionality of the graph, independent of its injectivity across different inputs.

```agda
    app-uniq : (a u : M) (w : S)
             → ⟨ pr (pr (fst (fst a)) (fst (fst u))) (fst w) ∈ fst F ⟩
             → fst w ≡ fst (fst (app a u))
    app-uniq a u w h =
      svAt-out zero (F ∷ prodL α ∷ []) sv (prʟ (fst a) (fst u)) w (fst (app a u))
```

To apply single-valuedness, the supplied membership is first transported from the ambient pair code to the constructible pair used by `val`. It is then compared with `val-graph`, the canonical membership for the extracted value. Since both entries now have the same input, the single-valuedness clause identifies their outputs.

```agda
        (subst (λ z → ⟨ pr z (fst w) ∈ fst F ⟩) (sym (prʟ-fst (fst a) (fst u))) h)
        (val-graph (prʟ (fst a) (fst u)) (pairMem a u))
```

The environment reader is extended to a total function on the numerals: outside the range of the sequence it returns the numeral zero. This junk value carries no mathematical meaning; every later use reads the extension only at indices below the length.

```agda
  ext : (n : ℕ) → (Fin n → ⟪ fst α ⟫) → ℕ → M
  ext zero    g k       = num zero
  ext (suc n) g zero    = up (g zero)
  ext (suc n) g (suc k) = ext n (λ i → g (suc i)) k
```

At every index below the length, the extension reads back exactly the entry of the sequence, by a recursion on the index.

```agda
  ext-at : (n : ℕ) (g : Fin n → ⟪ fst α ⟫) (i : Fin n) → ext n g (toℕ i) ≡ up (g i)
  ext-at (suc n) g zero    = refl
  ext-at (suc n) g (suc i) = ext-at n (λ j → g (suc j)) i
```

With the length `n` and sequence `g` fixed, `chain n g k` is defined by recursion on the step counter `k`. It starts at the numeral zero, and each step with `k<n` applies the pairing function to the next entry `g(k)` and the value accumulated so far. Thus `chain n g n` has consumed exactly the `n` entries of the sequence; behavior after that bound depends only on the meaningless default supplied by `ext` and is not part of the sequence code.

```agda
  chain : (n : ℕ) → (Fin n → ⟪ fst α ⟫) → ℕ → M
  chain n g zero    = num zero
  chain n g (suc k) = app (ext n g k) (chain n g k)
```

For a sequence of length `n`, the fold ends at `vₙ = chain n g n`. Its code is then `F(n,vₙ)`: the length numeral is the first coordinate of the final pairing, and the folded value is the second. This gives an actual value once `n` and `g` are given. It neither says that every element of `α` is a code nor defines a decoder on all of `α`.

```agda
  code : (n : ℕ) → (Fin n → ⟪ fst α ⟫) → M
  code n g = app (num n) (chain n g n)
```

Suppose two fold chains agree after `k` steps. Then their entries agree at every position `j<k`. The induction runs backward through the chain: equality at stage `k+1` is split by injectivity of `F` into equality of the entries used at stage `k` and equality of the preceding chain values.

```agda
  chain-inj : (n : ℕ) (g g' : Fin n → ⟪ fst α ⟫) (k : ℕ)
            → fst (fst (chain n g k)) ≡ fst (fst (chain n g' k))
            → (j : ℕ) → j < k → fst (fst (ext n g j)) ≡ fst (fst (ext n g' j))
  chain-inj n g g' zero    e j j<0  = Empty.rec (¬-<-zero j<0)
  chain-inj n g g' (suc k) e j j<sk = go (<-split j<sk)
```

At a successor stage, `app-inj` supplies those two equalities. If `j=k`, the first one is the desired entry equality; if `j<k`, the second one lets the induction hypothesis continue with the shorter chain. This is a cancellation argument between two known valid folds, not a procedure that turns an arbitrary element of `α` into a sequence.

```agda
    where
    q = app-inj (ext n g k) (chain n g k) (ext n g' k) (chain n g' k) e
    go : (j < k) ⊎ (j ≡ k) → fst (fst (ext n g j)) ≡ fst (fst (ext n g' j))
    go (inl j<k) = chain-inj n g g' k (snd q) j j<k
    go (inr j≡k) = subst (λ j → fst (fst (ext n g j)) ≡ fst (fst (ext n g' j))) (sym j≡k) (fst q)
```

The length tag now proves its purpose. If two codes are equal, injectivity of the outer application first recovers equality of their length numerals and hence equality of their natural-number lengths. After transporting to one common length, backward cancellation of the fold gives entrywise equality, so the two environment graphs have equal underlying sets. Only this implication is asserted.

```agda
  code-inj : (n : ℕ) (g : Fin n → ⟪ fst α ⟫) (n' : ℕ) (g' : Fin n' → ⟪ fst α ⟫)
           → fst (fst (code n g)) ≡ fst (fst (code n' g'))
           → fst (envS α g) ≡ fst (envS α g')
  code-inj n g n' g' e = subst P (#-inj′ (fst q)) same g' (snd q)
    where
```

The pair `q` separates the code equation into equality of the numeral coordinates and equality of the terminal fold values. The family `P m` records exactly what remains to prove for a sequence of length `m`, allowing numeral injectivity to transport the second sequence and its fold equation to the original length `n`.

```agda
    q = app-inj (num n) (chain n g n) (num n') (chain n' g' n') e
    P : ℕ → Type (ℓ-suc ℓ)
    P m = (h : Fin m → ⟪ fst α ⟫)
        → fst (fst (chain n g n)) ≡ fst (fst (chain m h m))
        → fst (envS α g) ≡ fst (envS α h)
```

Once the lengths coincide, equality of the environment graphs follows from function extensionality. For each finite index `i`, the proof compares the corresponding presented members of `α`; injectivity of the presentation embedding reduces their equality to equality of the underlying sets recovered from the two chains.

```agda
    same : P n
    same h e' = cong (λ (f : Fin n → ⟪ fst α ⟫) → fst (envS α f)) (funExt pt)
      where
      pt : (i : Fin n) → g i ≡ h i
      pt i = ↪-inj {a = fst α}
```

The comparison at `i` begins by using `ext-at` to identify the bounded total function `ext n g` with the genuine entry `g i`. The chain-cancellation lemma supplies equality of the two extended entries because `toℕ i<n`, and a second use of `ext-at` identifies the other side with `h i`. Values of `ext` outside this bound play no mathematical role.

```agda
        ( sym (cong (λ z → fst (fst z)) (ext-at n g i))
        ∙ chain-inj n g h n e' (toℕ i) (toℕ<n i)
        ∙ cong (λ z → fst (fst z)) (ext-at n h i) )
```

To describe one recursive transition semantically, fix an index object `i`. A `StepAt s C i` merely records objects `j,a,u,w` such that `j` is the successor of `i`, the sequence graph gives `s(i)=a`, the trace gives `C(i)=u` and `C(j)=w`, and the graph `F` gives `F(a,u)=w`. The whole package is propositionally truncated.

```agda
  StepAt : (s C i : S) → Type (ℓ-suc ℓ)
  StepAt s C i = ∥ Σ[ j ∈ S ] Σ[ a ∈ S ] Σ[ u ∈ S ] Σ[ w ∈ S ]
      ( (fst j ≡ sucV (fst i))
      × ⟨ pr (fst i) (fst a) ∈ fst s ⟩
      × ⟨ pr (fst i) (fst u) ∈ fst C ⟩
```

The last membership assertion is the recurrence equation written as a graph fact. Its input is the ordered pair `(a,u)`, and its output is `w`. Thus `StepAt` is the host-level meaning that the later first-order step formula must express; it does not yet add any decoder or choice of a global trace.

```agda
      × ⟨ pr (fst j) (fst w) ∈ fst C ⟩
      × ⟨ pr (pr (fst a) (fst u)) (fst w) ∈ fst F ⟩ ) ∥₁
```

`DomIs s n` says that `n` is exactly the domain of the sequence graph `s`. Every `x∈n` has some value `y` with `(x,y)∈s`, while every pair `(x,y)∈s` has its first coordinate `x` in `n`. Existence of a value is retained only propositionally; uniqueness comes from the separate environment conditions when it is needed.

```agda
  DomIs : (s n : S) → Type (ℓ-suc ℓ)
  DomIs s n = (x : S)
    → (⟨ fst x ∈ fst n ⟩ → ∥ Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst s ⟩ ∥₁)
    × ((y : S) → ⟨ pr (fst x) (fst y) ∈ fst s ⟩ → ⟨ fst x ∈ fst n ⟩)
```

`EnvC m C` says that `C` is an environment over `α` with exact domain `m`. Through `envOverAt`, this includes single-valuedness, the domain condition, the requirement that all values lie in `α`, and the requirement that every member of `C` is an ordered pair. Here `m` will be the successor of the sequence length, so the trace has positions from `0` through `n`.

```agda
  EnvC : (m C : S) → Type (ℓ-suc ℓ)
  EnvC m C = ⟨ (α ∷ m ∷ C ∷ []) ⊨ envOverAt (suc (suc zero)) (suc zero) zero ⟩
```

The complete semantic witness begins with a numeral `n∈ω`, its successor `m`, and a trace environment `C`. It requires `s` to have domain `n`, `C` to have domain `m` and values in `α`, and the trace to start at `C(0)=0`. A transition is supplied for each `i∈n`, followed by a final value at `C(n)` whose pairing with `n` yields `y`. This witness is propositionally truncated.

```agda
  Wit : (y s : S) → Type (ℓ-suc ℓ)
  Wit y s = ∥ Σ[ n ∈ S ] Σ[ m ∈ S ] Σ[ C ∈ S ]
      ( ⟨ fst n ∈ ω ⟩
      × (fst m ≡ sucV (fst n))
      × DomIs s n
```

The last component separates the terminal trace value from the length tag. It gives some `v` with `(n,v)∈C` and `F(n,v)=y`. The transition clauses determine `v` as the result after `n` folds; this final application of `F` then records the length and prevents sequences of different lengths from sharing a code.

```agda
      × EnvC m C
      × ⟨ pr (# zero) (# zero) ∈ fst C ⟩
      × ((i : S) → ⟨ fst i ∈ fst n ⟩ → StepAt s C i)
      × ∥ Σ[ v ∈ S ] ( ⟨ pr (fst n) (fst v) ∈ fst C ⟩
                     × ⟨ pr (pr (fst n) (fst v)) (fst y) ∈ fst F ⟩ ) ∥₁ ) ∥₁
```

Nested quantifiers shift the de Bruijn positions of every previously available variable. The abbreviations `i0,i1,…` name these positions uniformly: `i0` is the newest bound variable, and each successor moves one place outward. This bookkeeping lets the formulas below state the finite-trace equations without obscuring which object each occurrence denotes.

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

The names through `i4` cover the shallow part of the trace formulas: the current index, its successor, and the nearby values introduced for one recurrence step. Their polymorphic lengths allow the same position name to be reused after further binders have been added.

```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 next positions reach the trace environment and the original free variables after several existential witnesses have been introduced. In particular, the same formula can still refer simultaneously to the old trace value, the new trace value, and the sequence entry that relates them.

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

The step formula introduces five witnesses in all: the successor index `j`, the values `a,u,w`, and the pair code for `(a,u)`. Beneath all five binders, the original sequence variable has moved to position `i12`; the long index is therefore forced by the binding depth, not by an additional mathematical assumption.

```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
    i12 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc k)))))))))))))
```

Concretely, `i12` is four successors beyond `i8`. With the index names fixed, the next definitions can be read by following the mathematical roles of the variables rather than recounting nested successor constructors.

```agda
    i12 = suc (suc (suc (suc i8)))
```

The formula `stepFo` is the object-language counterpart of `StepAt`. It first chooses `j` and asserts that `j` is the successor of the current index `i`. It then chooses the sequence value `a`, the old and new trace values `u,w`, and a code for the ordered pair `(a,u)`.

```agda
  opaque
    private
      stepFo : Formula S 8
      stepFo = ∃̇ (
            sucAtL i1 i0
```

The four inner existential quantifiers bind `a,u,w` and their pair code. The first three application clauses state `s(i)=a`, `C(i)=u`, and `C(j)=w`; the pair clause identifies the auxiliary code with `(a,u)`. These facts prepare the single recurrence assertion at the center of the formula.

```agda
         ∧̇ (∃̇ (∃̇ (∃̇ (∃̇ (
              appAt i12 i5 i3
           ∧̇ appAt i8 i5 i2
           ∧̇ appAt i8 i4 i1
           ∧̇ prAtL i0 i3 i2
```

The innermost conjunct is the recurrence graph fact: applying `F` to the auxiliary input code produces the new value `w`. The preceding pair conjunct identifies that auxiliary code with the ordered pair `(a,u)`. Together the two conjuncts express the folding equation `F(a,u)=w` in the object language.

```agda
           ∧̇ appC F i0 i1 ))))))
```

The final-length formula says: there exists a value in the coded environment at the numeral slot, and the coded pairing applied to the numeral and this value produces the output.

```agda
      finFo : Formula S 7
      finFo = ∃̇ (∃̇ (
            appAt i4 i6 i1
         ∧̇ prAtL i0 i6 i1
         ∧̇ appC F i0 i7 ))
```

The body keeps two auxiliary parameters explicit before stating the trace conditions. It identifies `b` with the fixed alphabet `α` and `z` with the zero numeral, then asserts that `m` is the successor of the chosen length `n`. The equalities let later generic environment and application formulas be specialized to `α` and `0`.

```agda
      body : Formula S 7
      body =
          (var i1 ≐ con α)
       ∧̇ (var i0 ≐ con (nn zero))
       ∧̇ sucAtL i4 i3
```

The remaining conjuncts impose the domain condition, the environment-over condition, the zero-entry equation, every transition below `n`, and the final-length clause. For the currently named objects, they say that `C` is a finite trace connecting the initial zero to the output through the coded pairing. The outer quantifiers in `fo` will then assert that such a length and trace exist.

```agda
       ∧̇ domAt i6 i4
       ∧̇ envOverAt i2 i3 i1
       ∧̇ appAt i2 i0 i0
       ∧̇ ∀̇∈ (var i4) stepFo
       ∧̇ finFo
```

The full graph formula binds the numeral by the bounded quantifier over `ωʟ` and then the four auxiliary objects by nested existentials, producing a two-place formula over the output and the sequence.

```agda
    fo : Formula S 2
    fo = ∃̇∈ (con ωʟ) (∃̇ (∃̇ (∃̇ (∃̇ body))))
```

The environment `e7` contains the seven objects available before the quantifiers inside `stepFo` and `finFo` are opened. In de Bruijn order they are `z,b,C,m,n,y,s`, so slot zero is the auxiliary zero, while the original output and sequence occupy the two outermost slots. Later binders extend this environment at the front.

```agda
    private
      e7 : S → S → S → S → S → S → S → S ^ 7
      e7 y s n m C b z = z ∷ b ∷ C ∷ m ∷ n ∷ y ∷ s ∷ []
```

To read `stepFo` outward, the proof eliminates its propositionally truncated witnesses into the proposition `StepAt s C i`. It obtains `j,a,u,w` and the auxiliary pair code, together with the successor, three graph-application, pair, and `F`-application clauses. The auxiliary pair code will disappear after its equality is used.

```agda
      stepOut : (y s n m C b z i : S)
              → ⟨ (i ∷ e7 y s n m C b z) ⊨ stepFo ⟩ → StepAt s C i
      stepOut y s n m C b z i = PT.rec squash₁ (λ { (j , (ej , ha)) →
        PT.rec squash₁ (λ { (a , hu) → PT.rec squash₁ (λ { (u , hw) →
        PT.rec squash₁ (λ { (w , hp) → PT.rec squash₁ (λ { (p , (h1 , (h2 , (h3 , (h4 , h5))))) →
```

Each adequacy equation changes one satisfaction judgment into its intended equality or graph membership. The resulting facts identify `j` as the successor of `i`, read `a` from `s`, and read `u,w` from `C`. Together with the final graph fact for `F`, they have exactly the semantic shape required by `StepAt`.

```agda
          let γ = p ∷ w ∷ u ∷ a ∷ j ∷ i ∷ e7 y s n m C b z in
          ∣ j , a , u , w
          , ( subst ⟨_⟩ (sucAtL-adequate i1 i0 (j ∷ i ∷ e7 y s n m C b z)) ej
            , subst ⟨_⟩ (appAt-adequate i12 i5 i3 γ) h1
            , subst ⟨_⟩ (appAt-adequate i8 i5 i2 γ) h2
```

The pair-adequacy equation identifies the auxiliary object with the ordered pair `(a,u)`. Transporting the `F`-application fact along that equality yields the recurrence membership `((a,u),w)∈F`. This completes the outward passage from the first-order step formula to one semantic transition.

```agda
            , subst ⟨_⟩ (appAt-adequate i8 i4 i1 γ) h3
            , subst (λ q → ⟨ pr q (fst w) ∈ fst F ⟩)
                (subst ⟨_⟩ (prAtL-adequate i0 i3 i2 γ) h4)
                (subst ⟨_⟩ (appC-adequate F i0 i1 γ) h5) ) ∣₁ }) hp }) hw }) hu }) ha })
```

The outward reading of `finFo` first obtains a terminal trace value `v` and an auxiliary object `q`. Its clauses say `C(n)=v`, `q=(n,v)`, and `F(q)=y`. Because the target is propositionally truncated, both existential witnesses can be eliminated while retaining only `v` and the two graph facts needed by `Wit`.

```agda
      finOut : (y s n m C b z : S) → ⟨ e7 y s n m C b z ⊨ finFo ⟩
             → ∥ Σ[ v ∈ S ] ( ⟨ pr (fst n) (fst v) ∈ fst C ⟩
                            × ⟨ pr (pr (fst n) (fst v)) (fst y) ∈ fst F ⟩ ) ∥₁
      finOut y s n m C b z = PT.rec squash₁ (λ { (v , hq) →
        PT.rec squash₁ (λ { (q , (h1 , (h2 , h3))) →
```

Adequacy turns the three clauses into the memberships expressing `C(n)=v` and `F(q)=y`, together with the equality `q=(n,v)`. Transport along the last equality replaces `q` in the `F`-membership, producing exactly `F(n,v)=y` in graph form.

```agda
          let γ = q ∷ v ∷ e7 y s n m C b z in
          ∣ v , ( subst ⟨_⟩ (appAt-adequate i4 i6 i1 γ) h1
                , subst (λ r → ⟨ pr r (fst y) ∈ fst F ⟩)
                    (subst ⟨_⟩ (prAtL-adequate i0 i6 i1 γ) h2)
                    (subst ⟨_⟩ (appC-adequate F i0 i7 γ) h3) ) ∣₁ }) hq })
```

The body has eight conjuncts. The first two identify the auxiliaries `b=α` and `z=0`; the remaining six assert `m=n+1`, the exact domain of `s`, the environment conditions on `C`, `C(0)=0`, all transitions below `n`, and the final tagged value. Together with the separately supplied fact `n∈ω`, these data form `Wit y s`.

```agda
      bodyOut : (y s n m C b z : S) → ⟨ fst n ∈ ω ⟩
              → ⟨ e7 y s n m C b z ⊨ body ⟩ → Wit y s
      bodyOut y s n m C b z n∈ω (eb , (ez , (em , (hd , (hE , (h0 , (hS , hF))))))) =
        ∣ n , m , C
        , ( n∈ω
```

The successor adequacy equation supplies `m=n+1`, while the two readings of `domAt` give both directions of exact-domain membership for `s`. The environment formula is transported from the auxiliary base `b` to the fixed `α` using `b=α`; no equality between complete traces is required.

```agda
          , subst ⟨_⟩ (sucAtL-adequate i4 i3 (e7 y s n m C b z)) em
          , (λ x → domAt-in i6 i4 (e7 y s n m C b z) hd x
                 , domAt-out i6 i4 (e7 y s n m C b z) hd x)
          , envOverAt-transport (e7 y s n m C b z) (α ∷ m ∷ C ∷ [])
              i2 i3 i1 (suc (suc zero)) (suc zero) zero refl refl eb hE
```

The equality `z=0` converts the body clause `C(z)=z` into the initial condition `C(0)=0`. The bounded universal clause is read pointwise by `stepOut`, and `finOut` supplies the terminal tagged value. These are the remaining components of the propositionally truncated witness.

```agda
          , subst (λ w → ⟨ pr w w ∈ fst C ⟩) ez
              (subst ⟨_⟩ (appAt-adequate i2 i0 i0 (e7 y s n m C b z)) h0)
          , (λ i i∈n → stepOut y s n m C b z i (hS i i∈n))
          , finOut y s n m C b z hF ) ∣₁
```

The outward reading of the full formula eliminates the five nested existentials one by one, feeding each into the body reading until the complete witness is assembled.

```agda
    fo-out : (y s : S) → ⟨ (y ∷ s ∷ []) ⊨ fo ⟩ → Wit y s
    fo-out y s = PT.rec squash₁ (λ { (n , (n∈ω , hm)) →
      PT.rec squash₁ (λ { (m , hC) → PT.rec squash₁ (λ { (C , hb) →
      PT.rec squash₁ (λ { (b , hz) → PT.rec squash₁ (λ { (z , hbody) →
        bodyOut y s n m C b z n∈ω hbody }) hz }) hb }) hC }) hm })
```

The converse direction begins with one propositionally truncated `StepAt` witness and maps it to a satisfaction of `stepFo`. For representatives `j,a,u,w`, the environment is extended by their pair code and by the four values themselves. The following clauses then rebuild the successor and graph assertions in object-language form.

```agda
    private
      stepIn : (y s n m C i : S) → StepAt s C i
             → ⟨ (i ∷ e7 y s n m C α (nn zero)) ⊨ stepFo ⟩
      stepIn y s n m C i = PT.map (λ { (j , a , u , w , (ej , ha , hu , hw , hF)) →
        let γ = prʟ a u ∷ w ∷ u ∷ a ∷ j ∷ i ∷ e7 y s n m C α (nn zero) in
```

The witnesses are inserted in the same order in which `stepFo` binds them. Reversing the successor and application adequacy equations turns the semantic facts `j=i+1`, `s(i)=a`, `C(i)=u`, and `C(j)=w` into the corresponding satisfaction judgments. The nested truncations are preserved by introducing, rather than selecting, these witnesses.

```agda
        j , ( subst ⟨_⟩ (sym (sucAtL-adequate i1 i0 (j ∷ i ∷ e7 y s n m C α (nn zero)))) ej
            , ∣ a , ∣ u , ∣ w , ∣ prʟ a u
            , ( subst ⟨_⟩ (sym (appAt-adequate i12 i5 i3 γ)) ha
              , ( subst ⟨_⟩ (sym (appAt-adequate i8 i5 i2 γ)) hu
              , ( subst ⟨_⟩ (sym (appAt-adequate i8 i4 i1 γ)) hw
```

The canonical constructible pair `prʟ a u` witnesses the auxiliary pair variable. Pair adequacy identifies its underlying set with `(a,u)`, and transport of the membership `((a,u),w)∈F` gives the required object-language application clause. This completes the inward reading of one transition.

```agda
              , ( subst ⟨_⟩ (sym (prAtL-adequate i0 i3 i2 γ)) (prʟ-fst a u)
                , subst ⟨_⟩ (sym (appC-adequate F i0 i1 γ))
                    (subst (λ q → ⟨ pr q (fst w) ∈ fst F ⟩) (sym (prʟ-fst a u)) hF) )))) ∣₁ ∣₁ ∣₁ ∣₁ ) })
```

The inward reading of `finFo` starts from a propositionally truncated terminal value `v` with `C(n)=v` and `F(n,v)=y`. It maps this witness through the two existential quantifiers of `finFo`: one binds `v`, and the other binds an explicit code for the ordered pair `(n,v)`.

```agda
      finIn : (y s n m C : S)
            → ∥ Σ[ v ∈ S ] ( ⟨ pr (fst n) (fst v) ∈ fst C ⟩
                           × ⟨ pr (pr (fst n) (fst v)) (fst y) ∈ fst F ⟩ ) ∥₁
            → ⟨ e7 y s n m C α (nn zero) ⊨ finFo ⟩
      finIn y s n m C = PT.map (λ { (v , (hv , hy)) →
```

Extend the environment by `v` and the canonical pair `prʟ n v`. Reversing application adequacy expresses `C(n)=v`; reversing pair adequacy identifies the pair witness; and reversing the adequacy of application to the constant graph `F` expresses `F(n,v)=y`.

```agda
        let γ = prʟ n v ∷ v ∷ e7 y s n m C α (nn zero) in
        v , ∣ prʟ n v
            , ( subst ⟨_⟩ (sym (appAt-adequate i4 i6 i1 γ)) hv
              , ( subst ⟨_⟩ (sym (prAtL-adequate i0 i6 i1 γ)) (prʟ-fst n v)
                , subst ⟨_⟩ (sym (appC-adequate F i0 i7 γ))
```

The final transport changes the graph membership whose input is the ambient pair `(n,v)` into satisfaction using the constructible representative `prʟ n v`. The terminal clause is therefore rebuilt without choosing anything beyond the witness already carried by the propositional truncation.

```agda
                    (subst (λ q → ⟨ pr q (fst y) ∈ fst F ⟩) (sym (prʟ-fst n v)) hy) )) ∣₁ })
```

To rebuild the body, assume the six substantive trace conditions: `m=n+1`, the exact domain of `s`, the environment conditions for `C`, the initial value, all bounded transitions, and the terminal tagged value. The two remaining body conjuncts are the fixed identifications `b=α` and `z=0`, which need no additional hypotheses.

```agda
      bodyIn : (y s n m C : S) → fst m ≡ sucV (fst n) → DomIs s n → EnvC m C
             → ⟨ pr (# zero) (# zero) ∈ fst C ⟩
             → ((i : S) → ⟨ fst i ∈ fst n ⟩ → StepAt s C i)
             → ∥ Σ[ v ∈ S ] ( ⟨ pr (fst n) (fst v) ∈ fst C ⟩
                            × ⟨ pr (pr (fst n) (fst v)) (fst y) ∈ fst F ⟩ ) ∥₁
```

In the chosen seven-object environment, the auxiliary entries are literally `α` and `0`. Consequently the first two conjuncts of the body are witnessed by reflexivity. The rest of the proof converts the six supplied semantic conditions into the remaining six object-language conjuncts.

```agda
             → ⟨ e7 y s n m C α (nn zero) ⊨ body ⟩
      bodyIn y s n m C em hd hE h0 hS hF =
        let γ = e7 y s n m C α (nn zero) in
          refl
        , ( refl
```

Reversing successor adequacy supplies the conjunct for `m=n+1`. The introduction reading of `domAt` combines the two directions in `DomIs`: one direction uses propositional elimination because the existence of a graph value is truncated, and the other is already a direct implication. The environment condition is then transported into the selected variable positions.

```agda
        , ( subst ⟨_⟩ (sym (sucAtL-adequate i4 i3 γ)) em
        , ( domAt-intro i6 i4 γ (λ x →
              PT.rec (snd (fst x ∈ fst n)) (λ { (yy , p) → hd x .snd yy p })
            , hd x .fst)
        , ( envOverAt-transport (α ∷ m ∷ C ∷ []) γ
```

The initial membership `C(0)=0` gives the sixth conjunct through application adequacy. Each transition below `n` is sent inward by `stepIn`, and `finIn` rebuilds the final tagged-value clause. Along with the preceding five facts, these complete all eight conjuncts of the finite-trace body.

```agda
              (suc (suc zero)) (suc zero) zero i2 i3 i1 refl refl refl hE
        , ( subst ⟨_⟩ (sym (appAt-adequate i2 i0 i0 γ)) h0
        , ( (λ i i∈n → stepIn y s n m C i (hS i i∈n))
        , finIn y s n m C hF ))))))
```

The inward reading of the full formula eliminates the truncated witness and injects the five objects through the five nested existentials, assembling the object-language satisfaction of the graph formula.

```agda
    fo-in : (y s : S) → Wit y s → ⟨ (y ∷ s ∷ []) ⊨ fo ⟩
    fo-in y s = PT.rec (snd ((y ∷ s ∷ []) ⊨ fo))
      (λ { (n , m , C , (n∈ω , em , hd , hE , h0 , hS , hF)) →
        ∣ n , ( n∈ω
              , ∣ m , ∣ C , ∣ α , ∣ nn zero
```

The five witnesses are `n,m,C,α,0`: the first is introduced through the bounded existential over `ω`, and the remaining four through ordinary existentials. The fixed choices `α` and `0` make the first two body equalities reflexive, while `bodyIn` supplies the successor, domain, environment, initial, transition, and terminal clauses. Thus `fo-in` reconstructs the complete satisfaction without selecting a representative from the truncated witness globally.

```agda
              , bodyIn y s n m C em hd hE h0 hS hF ∣₁ ∣₁ ∣₁ ∣₁ ) ∣₁ })
```

It remains to test the semantic formula on a genuine finite sequence. Fix a length `N`, an assignment `g : Fin N → α`, a constructible set `s`, and an equality identifying the underlying set of `s` with the environment graph `envS α g`. The following construction proves existence and uniqueness of the formula's output for this represented sequence.

```agda
  module AtSeq (N : ℕ) (g : Fin N → ⟪ fst α ⟫) (s : S) (e : fst s ≡ fst (envS α g)) where
```

For the standard environment graph, three objects suffice to invoke the generic environment formulas: the base set `α`, the length numeral `N`, and `envS α g`. Their de Bruijn order in `δ` places the graph at slot two, the numeral at slot one, and the base at slot zero.

```agda
    private
      δ : S ^ 3
      δ = α ∷ nn N ∷ envS α g ∷ []
```

The standard graph `envS α g` is already known to be an environment over `α` with domain `N`. Projecting the domain clause from this environment fact proves that its exact domain is the numeral `#N`. This fact will later force every competing witness for the same sequence to use that same finite length.

```agda
      dom0 : ⟨ δ ⊨ domAt (suc (suc zero)) (suc zero) ⟩
      dom0 = envOver-dom (suc (suc zero)) (suc zero) zero δ (envOver α g)
```

To use the environment lookup theorem, the assignment must first be viewed as a family of sets in `V`. The map `gV` sends each finite index to the underlying set named by the corresponding presentation element `g i`; because `g i` presents a member of `α`, this is exactly the value recorded at that index.

```agda
      gV : Fin N → V ℓ
      gV i = ⟪ fst α ⟫↪ (g i)
```

If `k < N`, then the canonical environment contains the pair whose first coordinate is the numeral `# k` and whose second coordinate is the `k`-th sequence entry. The proof converts `k` to an element of `Fin N`, applies the lookup specification there, and transports the resulting membership back to the natural-number index.

```agda
      extMem : (k : ℕ) (p : k < N)
             → ⟨ pr (# k) (fst (fst (ext N g k))) ∈ fst (envS α g) ⟩
      extMem k p = subst (λ k → ⟨ pr (# k) (fst (fst (ext N g k))) ∈ fst (envS α g) ⟩)
        (toFromId' N k p)
        (subst ⟨_⟩ (sym (lookup-spec gV i (fst (fst (ext N g (toℕ i))))))
```

The comparison `ext-at` identifies the totalized lookup `ext N g (toℕ i)` with the genuine entry `g i`. The identities for conversion between bounded natural numbers and `Fin N` then return both the index and the displayed value to the original `k`.

```agda
          (cong (λ z → fst (fst z)) (ext-at N g i)))
        where
        i : Fin N
        i = fromℕ' N k p
```

The converse lookup statement expresses single-valuedness at every valid index. If the environment contains `(# k,a)` with `k < N`, then the underlying set of `a` must be the underlying set of the actual `k`-th entry; no second value can be recorded at that index.

```agda
      s-uniq : (k : ℕ) (p : k < N) (a : S)
             → ⟨ pr (# k) (fst a) ∈ fst (envS α g) ⟩
             → fst a ≡ fst (fst (ext N g k))
      s-uniq k p a ha =
          subst ⟨_⟩ (lookup-spec gV i (fst a))
```

This identification is made at the corresponding `Fin N` index. The lookup equation first determines `a`, `ext-at` replaces the totalized entry by the original assignment entry, and the conversion identity transports the result back to `k`.

```agda
            (subst (λ k → ⟨ pr (# k) (fst a) ∈ fst (envS α g) ⟩) (sym (toFromId' N k p)) ha)
        ∙ sym (cong (λ z → fst (fst z)) (ext-at N g i))
        ∙ cong (λ k → fst (fst (ext N g k))) (toFromId' N k p)
        where
        i : Fin N
```

Here `i = fromℕ' N k p` is the finite index justified by the bound `p : k < N`. Keeping the bound explicit is essential: the total function `ext` has no sequence meaning outside this range.

```agda
        i = fromℕ' N k p
```

The fold has `N + 1` states, from the initial value through the state after all `N` entries have been processed. Each state already comes with a proof that it belongs to `α`; `fiber` turns that membership into a presentation element, producing an assignment `h` indexed by `Fin (suc N)`.

```agda
      h : Fin (suc N) → ⟪ fst α ⟫
      h i = fiber (fst α) (snd (chain N g (toℕ i))) .fst
```

The family `hV` forgets the presentation indices and returns to their underlying `V`-sets. The fiber equation used below shows that these sets are precisely the fold states from which `h` was obtained.

```agda
      hV : Fin (suc N) → V ℓ
      hV i = ⟪ fst α ⟫↪ (h i)
```

Let `C` be the environment graph of this state assignment. Its domain has length `N + 1`, and its entry at `k` records the fold state after the first `k` sequence entries, including the initial state at `k = 0` and the final state at `k = N`.

```agda
      C : S
      C = envS α h
```

For every `k < N + 1`, `chainMem` exhibits the expected graph entry `(# k, chain N g k)` in `C`. As for the original sequence, the proof passes through the corresponding element of `Fin (suc N)` and invokes the environment lookup specification.

```agda
      chainMem : (k : ℕ) (p : k < suc N)
               → ⟨ pr (# k) (fst (fst (chain N g k))) ∈ fst C ⟩
      chainMem k p = subst (λ k → ⟨ pr (# k) (fst (fst (chain N g k))) ∈ fst C ⟩)
        (toFromId' (suc N) k p)
        (subst ⟨_⟩ (sym (lookup-spec hV i (fst (fst (chain N g (toℕ i))))))
```

The fiber equation identifies the value named by `h i` with the actual fold state, while `toFromId'` restores the original natural-number index. These two identifications complete the graph-membership proof without asserting anything about indices outside `N + 1`.

```agda
          (sym (fiber (fst α) (snd (chain N g (toℕ i))) .snd)))
        where
        i : Fin (suc N)
        i = fromℕ' (suc N) k p
```

The fixed equation `e : fst s ≡ fst (envS α g)` lets us use the canonical environment facts for the represented sequence `s`. The map `inS` transports a canonical graph entry from `envS α g` into `s`.

```agda
      inS : (k : ℕ) (a : S) → ⟨ pr (# k) (fst a) ∈ fst (envS α g) ⟩ → ⟨ pr (# k) (fst a) ∈ fst s ⟩
      inS k a = subst (λ w → ⟨ pr (# k) (fst a) ∈ w ⟩) (sym e)
```

The reverse transport `outS` moves any graph entry of `s` back to `envS α g`. This direction will be used in the uniqueness argument, where an entry supplied by an arbitrary witness chain must be compared with the actual assignment entry.

```agda
      outS : (k : ℕ) (a : S) → ⟨ pr (# k) (fst a) ∈ fst s ⟩ → ⟨ pr (# k) (fst a) ∈ fst (envS α g) ⟩
      outS k a = subst (λ w → ⟨ pr (# k) (fst a) ∈ w ⟩) e
```

We now verify that the canonical code satisfies the graph formula. The witnesses choose the finite length numeral `# N`, its successor `#(N+1)`, and the state environment `C`; the remaining fields establish the domain of `s`, the `α`-valued state chain, its zero initial state, every transition, and the final application of the pairing graph.

```agda
    wit : Wit (fst (code N g)) s
    wit = ∣ nn N , nn (suc N) , C
          , ( #∈ω N
            , refl
            , domIs
```

The last existential clause is witnessed by the state `chain N g N`. It occurs in `C` at index `N`, and applying `F` to the pair consisting of the length numeral and that state gives `code N g`; the whole existence statement remains propositionally truncated.

```agda
            , envOver α h
            , chainMem zero (suc-≤-suc zero-≤)
            , step
            , ∣ fst (chain N g N)
              , ( chainMem N ≤-refl , app-graph (num N) (chain N g N) ) ∣₁ ) ∣₁
```

To prove that `s` has domain `# N`, start with an index in `# N`. The canonical environment supplies a merely existing value at that index, and transport along `e` turns its graph membership into membership in `s`.

```agda
      where
      domIs : DomIs s (nn N)
      domIs x =
          (λ m → PT.map (λ { (yy , p) → yy , subst (λ w → ⟨ pr (fst x) (fst yy) ∈ w ⟩) (sym e) p })
                   (domAt-in (suc (suc zero)) (suc zero) δ dom0 x m))
```

Conversely, if `s` contains a pair with first coordinate `x`, transport sends it back to the canonical environment. The known domain of that environment then implies `x ∈ # N`, completing the two directions of the domain characterization.

```agda
        , (λ yy p → domAt-out (suc (suc zero)) (suc zero) δ dom0 x yy
                      (subst (λ w → ⟨ pr (fst x) (fst yy) ∈ w ⟩) e p))
```

For a set-theoretic index `i ∈ # N`, numeral elimination supplies a natural number `k < N` whose numeral is `i`. The transition witness then chooses the successor numeral, the actual `k`-th sequence entry, and the fold states at `k` and `k+1`.

```agda
      step : (i : S) → ⟨ fst i ∈ # N ⟩ → StepAt s C i
      step i i∈N = PT.rec squash₁ (λ { (k , p , ei) →
        ∣ nn (suc k) , fst (ext N g k) , fst (chain N g k) , fst (chain N g (suc k))
        , ( cong sucV (sym ei)
          , subst (λ w → ⟨ pr w (fst (fst (ext N g k))) ∈ fst s ⟩) (sym ei)
```

The required transition facts now follow from the two canonical environments and the defining equation of the fold. The sequence entry lies in `s`, both adjacent states lie in `C`, and `app-graph` records that `F` sends the pair of the entry and the old state to the new state; transports only replace `# k` by the originally given index `i`.

```agda
              (inS k (fst (ext N g k)) (extMem k p))
          , subst (λ w → ⟨ pr w (fst (fst (chain N g k))) ∈ fst C ⟩) (sym ei)
              (chainMem k (≤-suc p))
          , chainMem (suc k) (suc-≤-suc p)
          , app-graph (ext N g k) (chain N g k) ) ∣₁ }) (∈#-elim N (fst i) i∈N)
```

Existence alone does not yet make `fo` a function graph. The theorem `only` proves that every output `y` admitted by a `Wit y s` has the same underlying set as the canonical code. Since this equality is a proposition, the propositionally truncated witness may be eliminated before the uniqueness argument begins.

```agda
    only : (y : S) → Wit y s → fst y ≡ fst (fst (code N g))
    only y = PT.rec (setIsSet (fst y) (fst (fst (code N g))))
      (λ { (n , m , C' , (n∈ω , em , hd , hE , h0 , hS , hF)) →
        Only.final n m C' n∈ω em hd hE h0 hS hF })
      where
```

Fix an arbitrary witness with length object `n`, successor `m`, and state environment `C'`. Its hypotheses say that `s` has domain `n`, that `C'` is an `α`-valued environment of length `m`, that its initial entry is zero, that it obeys every fold step below `n`, and that its terminal state is paired with `n` to produce `y`.

```agda
      module Only (n m C' : S) (n∈ω : ⟨ fst n ∈ ω ⟩) (em : fst m ≡ sucV (fst n))
                  (hd : DomIs s n) (hE : EnvC m C')
                  (h0 : ⟨ pr (# zero) (# zero) ∈ fst C' ⟩)
                  (hS : (i : S) → ⟨ fst i ∈ fst n ⟩ → StepAt s C' i)
                  (hF : ∥ Σ[ v ∈ S ] ( ⟨ pr (fst n) (fst v) ∈ fst C' ⟩
```

The terminal clause `hF` merely asserts the existence of a state `v` recorded by `C'` at index `n` and mapped by `F` together with `n` to `y`. It does not choose a terminal state globally; later it is eliminated only into the set equality that states uniqueness of the output.

```agda
                                     × ⟨ pr (pr (fst n) (fst v)) (fst y) ∈ fst F ⟩ ) ∥₁)
                  where
```

The witness length `n` must equal the canonical numeral `# N` as a set. Both describe the domain of the same sequence `s`: `hd` gives the description through the arbitrary witness, while `dom0` gives it through the chosen representation `s = envS α g`. Extensionality reduces the equality to the two membership implications.

```agda
        n≡ : fst n ≡ # N
        n≡ = cong fst (extensionalL {a = n} {b = nn N} (λ x → ⇔toPath (fwd x) (bwd x)))
          where
          fwd : (x : S) → ⟨ fst x ∈ fst n ⟩ → ⟨ fst x ∈ # N ⟩
          fwd x x∈n = PT.rec (snd (fst x ∈ # N))
```

For the forward implication, an element `x ∈ n` yields, by `hd`, a merely existing pair in `s` with first coordinate `x`. Transporting that pair to the canonical environment and reading its known domain proves `x ∈ # N`.

```agda
            (λ { (yy , p) → domAt-out (suc (suc zero)) (suc zero) δ dom0 x yy
                              (subst (λ w → ⟨ pr (fst x) (fst yy) ∈ w ⟩) e p) })
            (hd x .fst x∈n)
          bwd : (x : S) → ⟨ fst x ∈ # N ⟩ → ⟨ fst x ∈ fst n ⟩
          bwd x x∈N = PT.rec (snd (fst x ∈ fst n))
```

For the reverse implication, `x ∈ # N` gives an entry of the canonical environment. After transport to `s`, the converse half of `hd` shows `x ∈ n`. Thus the length is recovered from the sequence domain, without selecting a representation for every sequence.

```agda
            (λ { (yy , p) → hd x .snd yy (subst (λ w → ⟨ pr (fst x) (fst yy) ∈ w ⟩) (sym e) p) })
            (domAt-in (suc (suc zero)) (suc zero) δ dom0 x x∈N)
```

Because `C'` satisfies the environment condition, it is single-valued. Hence two pairs in `C'` with the same first coordinate must have equal second coordinates as underlying sets. This fact will compare the arbitrary state recorded by `C'` with the state forced by the fold equations.

```agda
        svC : (x v v' : S) → ⟨ pr (fst x) (fst v) ∈ fst C' ⟩ → ⟨ pr (fst x) (fst v') ∈ fst C' ⟩
            → fst v ≡ fst v'
        svC = svAt-out (suc (suc zero)) (α ∷ m ∷ C' ∷ [])
                (envOver-sv (suc (suc zero)) (suc zero) zero (α ∷ m ∷ C' ∷ []) hE)
```

The central induction states that every value recorded by `C'` at an index `k < N + 1` equals the canonical fold state `chain N g k`. At `k = 0`, both values are forced to be zero by the initial clause and single-valuedness of `C'`.

```agda
        entry : (k : ℕ) → k < suc N → (v : S)
              → ⟨ pr (# k) (fst v) ∈ fst C' ⟩ → fst v ≡ fst (fst (chain N g k))
        entry zero    p v hv = svC (nn zero) v (nn zero) hv h0
        entry (suc k) p v hv = PT.rec (setIsSet (fst v) (fst (fst (chain N g (suc k)))))
          (λ { (j , a , u , w , (ej , ha , hu , hw , hFw)) →
```

In the successor case, a transition witness supplies an entry `a` of the sequence, an old state `u`, and a new state `w`. The canonical sequence lookup identifies `a` with the `k`-th input, the induction hypothesis identifies `u` with the canonical old state, and functionality of `F` then identifies `w` with the canonical new state.

```agda
            let ea : fst a ≡ fst (fst (ext N g k))
                ea = s-uniq k p' a (outS k a ha)
                eu : fst u ≡ fst (fst (chain N g k))
                eu = entry k (≤-suc p') u hu
                ew : fst w ≡ fst (fst (chain N g (suc k)))
```

The step clause is available because `k < N`, obtained from the successor bound. It places `w` in `C'` at the successor index; single-valuedness first equates the originally given value `v` with `w`, and the preceding application argument then equates `w` with `chain N g (suc k)`.

```agda
                ew = app-uniq (ext N g k) (chain N g k) w
                       (subst (λ q → ⟨ pr q (fst w) ∈ fst F ⟩) (cong₂ pr ea eu) hFw)
            in svC (nn (suc k)) v w hv
                 (subst (λ z → ⟨ pr z (fst w) ∈ fst C' ⟩) ej hw) ∙ ew })
          (hS (nn k) (subst (λ z → ⟨ # k ∈ z ⟩) (sym n≡) (#mono k N p')))
```

The predecessor bound is the small arithmetic fact needed by the induction: from `suc k < suc N` one obtains `k < N`. It ensures that the `k`-th input entry is genuine and that the fold step at `k` lies within the sequence.

```agda
          where
          p' : k < N
          p' = pred-≤-pred p
```

It remains to determine the candidate output `y`. Eliminating the propositionally truncated terminal witness gives a state `v` recorded at the witness length `n`; the underlying-set equality `n≡ : fst n ≡ # N` transports this membership to index `N`, where the induction identifies `v` with the canonical final fold state.

```agda
        final : fst y ≡ fst (fst (code N g))
        final = PT.rec (setIsSet (fst y) (fst (fst (code N g))))
          (λ { (v , (hv , hy)) →
            let hv' : ⟨ pr (# N) (fst v) ∈ fst C' ⟩
                hv' = subst (λ z → ⟨ pr z (fst v) ∈ fst C' ⟩) n≡ hv
```

The terminal clause also says that `F` maps the pair formed from `fst n` and `fst v` to the underlying set of `y`. After replacing these inputs by `# N` and the canonical final state, functionality of `F` gives `fst y ≡ fst (fst (code N g))`. This proves uniqueness only for outputs satisfying the graph formula; it does not define a decoder on arbitrary elements of `α`.

```agda
                ev : fst v ≡ fst (fst (chain N g N))
                ev = entry N ≤-refl v hv'
            in app-uniq (num N) (chain N g N) y
                 (subst (λ q → ⟨ pr q (fst y) ∈ fst F ⟩) (cong₂ pr n≡ ev) hy) })
          hF
```

The predicate `Mem s` is simply membership of `s` in `seqL α`. Thus every later construction is restricted to sets that are finite `α`-valued environment graphs, rather than arbitrary elements of the ambient universe.

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

A representation of `s` consists merely of a natural length `n`, an assignment `g : Ix α n`, and equality of `s` with the environment graph of `g`. The propositional truncation deliberately forgets which representation supplied these data; no global choice of lengths or assignments is made.

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

Membership in `seqL α` first yields, through `seqL-out`, a merely existing finite length at which `s` belongs to an environment set. The converse description of that environment set then supplies a merely existing assignment and the required graph equality, establishing `Rep s`.

```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 α n s hn) })
    (seqL-out α s m)
```

The graph formula can now be turned into a function on `seqL α`. Each concrete representation `(n,g,e)` yields the candidate `fst (code n g)` together with a proof that it uniquely fills the graph fiber over `s`. Mapping the truncated representation into this propositionally truncated unique-existence statement makes it a valid input to `mereFunct`, which converts it into the required contractibility without selecting a preferred representation.

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

For each representation, `fo-in` proves that the canonical code lies in the graph fiber. If another `y'` lies in that fiber, `fo-out` turns its satisfaction proof into a witness and `AtSeq.only` identifies it with the canonical code. Since constructibility proofs are propositional, equality of the underlying sets gives equality of the packaged elements.

```agda
        fst (code n g)
        , ( fo-in (fst (code n g)) 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 general theorem for a functional definable relation now supplies its unique value operation. We retain the function value and the principle that any output satisfying `fo` is equal to that value; these are the two facts needed to construct the internal injection.

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

Define `fn s m` to be this unique value for the sequence member `s`. Although the notation includes the membership proof `m`, membership is proposition-valued, so the mathematical value does not depend on a choice among distinct proofs.

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

Whenever `s` is represented by an assignment `g` of length `n`, the underlying `S`-value `fst (code n g)` satisfies `fo`; uniqueness of the graph value therefore gives `fn s m ≡ fst (code n g)`. This comparison holds for every supplied representation and so does not require choosing a preferred one.

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

The value of `fn` remains inside `α`. A truncated representation may be eliminated into this membership proposition; for each representative `(n,g)`, the second component of `code n g` proves membership in `α`, and `fn-code` transports that fact to `fn s m`.

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

These facts form a `DefinableMap` from `seqL α` to `α`. The record stores the host-level function and the proof that its values lie in the codomain together with the first-order formula `fo`: `defines` proves that the selected value satisfies the formula, while `only` proves that every satisfying output is that selected value. After injectivity is established, the following `Inj` construction uses this definability data to build the actual graph set in `L`.

```agda
  D : DefinableMap
  D = record
    { dom = seqL α ; cod = α ; 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, suppose two sequence members have equal `fn` values. Their representations are propositionally truncated, but the desired equality of underlying sets is itself a proposition, so both truncations may be eliminated to compare arbitrary representatives `(n,g)` and `(n',g')`.

```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' e = PT.rec2 (setIsSet (fst s) (fst s'))
    (λ { (n , g , es) (n' , g' , es') →
        es
```

The equations `fn-code` turn equality of the two `fn` values into equality of the two canonical codes. The previously proved `code-inj` then gives equality of their environment graphs; composing with the two representation equations yields `fst s ≡ fst s'`. This is a proof by comparison of valid codes, not a total decoding operation on `α`.

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

The definable map and the preceding injectivity proof determine an internal injection from `seqL α` into `α`. The conclusion `InjL` is propositionally truncated existence of a suitable graph in `L`; it asserts neither that the map is surjective nor that arbitrary elements of `α` can be decoded as finite sequences.

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

## Finite sequences inject into an infinite ordinal

The final theorem removes the temporary assumption that a pairing injection on `α` has already been supplied. Once an internal injection `prodL α ↪ α` is constructed, its truncated graph witness provides the single-valuedness, exact domain, injectivity, and range facts required by the fold construction, yielding `seqL α ↪ α` inside `L`.

```agda
seq-count :
    (α : SL.S) → IsOrd (fst α) → (⟨ fst α ∈ˢ ω ⟩ → Empty.⊥)
  → InjL (seqL α) α
seq-count α oα α∉ω = PT.rec squash₁
  (λ { (F , sv , dm , ij , ran) → Code.injL α oα α∉ω F sv dm ij ran }) pairing
```

To build the pairing injection, choose only locally a cardinal representative `μ` supplied by `cardOf α oα`. This representative is available under propositional truncation, but the target `InjL (prodL α) α` is also a proposition, so the construction may be carried out for an arbitrary representative without making a global choice.

```agda
  where
  pairing : InjL (prodL α) α
  pairing = PT.rec squash₁ build (cardOf α oα)
    where
    build : Σ[ μ ∈ S ]
```

The representative `μ` is an ordinal and an internal cardinal, with internal injections in both directions between `α` and `μ`; `cardOf` also supplies an inclusion `μ ⊆ α`, although this construction does not use it. The two injections compare cardinality in both directions without identifying `μ` and `α` definitionally.

```agda
              ( IsOrd (fst μ) × IsCardinalL μ
              × ((z : V ℓ) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst α ⟩)
              × InjL α μ × InjL μ α )
          → InjL (prodL α) α
    build (μ , oμ , cardμ , _ , α↪μ , μ↪α) =
```

The desired pairing is the composite `α² ↪ μ² ↪ μ ↪ α`. The first arrow applies `α ↪ μ` to both coordinates, the middle arrow is the square law for the infinite internal cardinal `μ`, and the last arrow returns to `α`. The square law is therefore used at the cardinal representative, not directly at an arbitrary infinite ordinal.

```agda
      injl-trans (prodL α) (prodL μ) α (prod-inj α μ α↪μ)
        (injl-trans (prodL μ) μ α
          (WF.WFI.induction regularityV {P = Goal} Step.result (fst μ) (snd μ) oμ cardμ μ∉ω)
          μ↪α)
      where
```

It remains to show that `μ` is infinite in the sense required by the square law. If `μ ∈ ω`, then `μ` would be a finite ordinal, while the supplied internal injection `α ↪ μ` would inject the infinite ordinal `α` into it; `no-fin` rules this out using the ordinality and infinitude hypotheses on `α` and `μ`.

```agda
      μ∉ω : ⟨ fst μ ∈ˢ ω ⟩ → Empty.⊥
      μ∉ω h = no-fin α μ oα α∉ω oμ h α↪μ
```