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

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

  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.

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.

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.

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.

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.

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.

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.

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.

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.

  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.

seqFo : S → Formula S 
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.

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.

  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.

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.

  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.

      , ∣ 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.

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.

        → Σ[ 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.

    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.

  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.

    (λ { (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.

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

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

  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.

  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.

  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.

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

  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.

  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.

    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.

    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.

  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.

    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.

    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.

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

    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.

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

  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.

  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.

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

  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.

  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.

    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.

  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.

    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.

    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.

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

  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.

      × ⟨ 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.

  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.

  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.

  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.

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

  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.

    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.

    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.

    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.

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

  opaque
    private
      stepFo : Formula S 
      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.

         ∧̇ (∃̇ (∃̇ (∃̇ (∃̇ (
              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.

           ∧̇ 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.

      finFo : Formula S 
      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.

      body : Formula S 
      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.

       ∧̇ 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.

    fo : Formula S 
    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.

    private
      e7 : S → S → S → S → S → S → S → S ^ 
      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.

      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.

          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.

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

      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.

          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.

      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.

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

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

    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.

    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.

        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.

              , ( 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).

      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.

        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.

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

      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.

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

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

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

    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.

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

  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.

    private
      δ : S ^ 
      δ = α ∷ 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.

      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.

      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.

      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.

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

      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.

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

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

      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.

      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.

      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.

      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.

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

      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.

      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.

    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.

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

      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.

        , (λ 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.

      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.

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

    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.

      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.

                                     × ⟨ 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.

        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.

            (λ { (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.

            (λ { (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.

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

        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.

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

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