---
title: "在无穷序数以下编码有限序列"
module: L.GCH.FiniteSequenceCoding
lang: zh
site: "Bedrock"
description: "在无穷序数以下编码有限序列"
stage: "证明 GCH"
reading_order: 114
canonical: https://bedrock.institute/zh/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/en/L.GCH.FiniteSequenceCoding.md, https://bedrock.institute/ja/L.GCH.FiniteSequenceCoding.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 在无穷序数以下编码有限序列

有限参数表必须由 `L` 内部存在的集合来计数。本章先把一个可构造集合上的全部有限序列收集成一个可构造集合。随后对无穷序数 `α`，借助从 `α × α` 到 `α` 的内部编码单射逐项折叠序列，再以长度作最终标签，并证明从序列集到 `α` 的内部单射。这个结论只给出上界：它既不覆盖 `α` 的每个元素，也不定义 `α` 全域上的解码器。

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

这项构造的经典性只来自一条显式的排中律假设。尤其是，命题截断的见证始终保持截断，除非唯一性使见证类型本身成为命题；证明不借助选择公理来任意选取序列表示或单射图。

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

固定宇宙层级 `ℓ`，并假设层级 `ℓ-suc ℓ` 上的排中律。下文从分离到末尾所用平方律的每项构造都相对于这一条具名假设，因此最终的序列界恰好承载同一假设。

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

下文始终交替使用同一对象的两种描述。在对象语言层面，相等、合取以及有界或无界量化描述 `L` 内部的序列图与递归轨迹。在宿主层面，呈现把集合成员化为小索引，而正则性稍后支撑平方律背后的良基论证。

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

编码依赖两类具有刚性的集合码。有序对码的单射性可从对码相等恢复两个坐标，冯·诺伊曼数码则在 `ω` 内忠实记录自然数及其顺序。可构造性的传递性保证可构造序数的每个成员仍在 `L` 中，因而这些外围码可作为可构造模型的元素使用。

```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 ( ωʟ )
```

这里使用的集合论图必须能由 `L` 内部的一阶推理识别。分离构成准确的子集合，而配对、图应用、定义域与环境的充分性把每条对象语言子句同底层集合之间的预期关系认同起来。这座桥梁稍后会把宿主层的递归折叠转化为内部可定义图。

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

有限序列表示为以数码为准确规定义域的环境图。对每个固定长度，环境集构造恰好收集这些图，而从成员反向读取表示时只得到命题截断的结果。尽管如此，一旦图公式的输出唯一，递归机制仍可产出实际取值；编码单射的复合则把所得的界在可构造集合之间传递。

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

最终的计数论证无需假设给定的无穷序数本身已是基数。证明先转到一个基数代表，在那里用平方律压缩有序对，再复合回原序数。本章随后把这项对压缩构造成有限序列的可定义单射。

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

长度以自然数表示，位置以 `Fin n` 的元素表示，内部定义域标记则以数码表示。在这三种视角之间转换，需要 `toℕ i < n` 之类的顺序事实，以及从小于 `n` 的自然数反向构造有穷索引。由于随附的隶属证明是命题，依值对的相等由其数据分量控制。

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

单射性证明反复区分后继以下索引的两种情形：它小于前驱，或者正是末索引。命题外延性随后把两个隶属蕴含化为集合相等，累积层级则提供承载这些论证的集合及其典范呈现。

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

冯·诺伊曼数码及其后继运算把有限长度同内部集合 `ω` 联系起来。不可能的有限界由空类型表示；良基归纳只在稍后借平方律构造对压缩时出现，并不参与折叠一条给定有限序列的初等递归。

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

命题截断记录某个表示存在，同时刻意忘却所给的是哪一个表示。只有当目标本身是命题时，例如集合的隶属或相等，才使用它的消去原则。这项限制保证本章能够证明存在性与单射性，而不会暗中选取长度、赋值或内部图。

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

在外围层面，隶属是命题值的。每当把截断见证消去到隶属断言中，这一点都至关重要：没有数据被选出，留下的只有隶属为真。

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

以 `SV` 表示外围累积层级上的命题值结构。它提供外围隶属概念，用来比较有序对码、数码与集合论图，随后再把这些对象视为可构造对象。

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

以 `S` 表示可构造结构 `SL` 的载体。`S` 的元素由外围集合及其属于 `L` 的证据组成；因此内部单射所用的每个序列集、图与序数都有实际的可构造代表。

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

带有 `S` 中常元的公式在可构造结构中求值，其原子内容也可投影到底层外围集合后读取。`L` 的传递性使两种读法一致，从而对象语言中的图条件能够证成折叠所用的外围隶属等式。

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

数码 `nn k` 把外围的冯·诺伊曼数码与其可构造性证明打包在一起。数码标记有限环境的准确定义域；数码零还充当折叠的初始累积值与 `ext` 在界外的无关紧要默认值；长度数码则为完成的折叠加上标签。借助这些用途，有限索引在可构造模型内部仍可被识别。

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

## 收集一个集合上的全部有限序列

`A` 上的序列在宿主层面是从有限序数到 `A` 的呈现的函数；小索引类型收集一个长度与这样一个函数。这是宿主层面的概念；其集合编码的对应物在下文定义。

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

小定义域原理给出一个可构造集合，它包含 `A` 上一切有限长度的环境图。这只是公共容器：精确的集合由下文的分离刻出，且不主张该容器恰为这些图的像。

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

对特定长度 `n` 与赋值 `g`，图 `envS A g` 属于这个公共容器。这条包含提供分离隶属的外围一半；定义公式则提供准确的有限环境条件。

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

这个一元公式断言：候选对象 `x` 是 `A` 上的环境图，其定义域是内部 `ω` 的某个成员。因此起初只知道这个有界见证属于 `ω`；从中恢复实际的自然数长度要到稍后进行，而且结果仍在命题截断之内。

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

现在用分离去除公共容器中的多余元素。所得集合 `seqL A` 恰好包含容器中满足有限环境描述的元素。保持定义不透明只影响归一化；其数学内容由随后给出的隶属等式完全确定。

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

一个元素属于 `seqL A`，当且仅当它既属于公共容器，又满足 `seqFo A`。因此容器保证这批对象组成集合，公式保证其准确性；任何一部分都不能单独刻画全部有限序列之集。

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

长度为 `n` 的环境集的每个成员都属于 `seqL A`。证明先读取该成员的截断呈现，再把它引入分离所得的集合。

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

该成员先被搬运到图形式。界定记录表明这个图属于容器，随后典范条目便满足相应描述。

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

描述的见证由长度的数码、其在内部 `ω` 中的隶属，以及该环境在 `A` 上的图关系组成，全部打包进截断存在。

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

反过来，属于 `seqL A` 只给出经过命题截断的断言：存在某个自然数长度 `n`，使该成员属于 `envSet A n`。论证舍去分离等式中的容器分量，从定义公式读取存在信息；它并未为所有成员一致地选取长度。

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

在截断见证的一个分支内，设定义域对象 `d` 已与数码 `# k` 等同，底对象 `b` 已与 `A` 等同，且 `x` 满足环境条件。对这些固定见证，恢复过程构造长度为 `k` 的赋值，并把 `x` 与其图等同。外层结果随即再次截断，所以这项局部构造并不定义全局解码器。

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

在固定长度 `k` 下，环境的各项条件唯一确定每个条目：准确的定义域给出仅有的存在性，单值性使条目纤维成为命题，取值限制则把恢复出的值放入 `A` 的呈现。随后外延性还使用「图的每个成员都具有对形」这一条，把整个集合 `x` 与典范环境图等同。

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

剩余步骤消去定义域在 `ω` 中的隶属：`ω` 的成员仅仅是某个数码。

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

数码被喂入转换步骤，读取方向完成。注意其强度：长度与环境只在截断之内被恢复，并未产出从 `seqL A` 到赋值的全局解码器。

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

## 把有限序列折叠成一个序数码

编码模块固定配对函数的数据。其参数包括序数 `α`、`α` 不属于 `ω` 的证明，以及可构造图 `F` 连同三条子句：单值性、在乘积上的全域性和单射性。这里以 `α ∉ ω` 表述所需的无穷性。

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

最后一条假设是元层形式的值域条件：图记录的每个值都属于 `α`。四条条款合起来说：`F` 是从乘积 `α × α` 到 `α` 的内部编码单射。

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

输入与值的载体是「可构造集合连同属于 `α` 的证明」这一类型：乘积的条目必须落在 `α` 中，每个值也一样。

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

数码成为载体的元素：由于 `α` 不属于 `ω`，`α` 的无穷性把每个数码放入 `α` 之内。这是无穷性假设在折叠中的唯一用场。

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

`α` 的呈现索引也成为载体元素：可构造性沿 `α` 的隶属搬运，而隶属由呈现见证。

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

单值性与准确的定义域子句共同把图 `F` 读成 `prodL α` 成员上的实际宿主函数。定义域隶属起初只给出截断的输出，但可能输出所成的纤维是命题，故可提取其中的唯一取值。要从输出相等推出输入相等，仍须另用假设 `ij`。

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

两个载体元素的编码对属于乘积：两个坐标都在 `α` 中，配对运算把这一点转化为对 `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))
```

对已经知道属于 `prodL α` 的输入 `x`，定义 `val x` 为 `F` 在 `x` 处记录的唯一输出。隶属证明是输入数据的一部分，因为图只被要求恰好在该乘积上全域，而非在每个可构造集合上全域。

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

图记录陈述：输入与值构成的有序对属于 `F`；这正是后文同一视引理所消耗的数据。

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

图在乘积上单射：值相等的两点底层集合相等。与提取合在一起，这是配对函数的单射一半。

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

二元运算 `app a u` 在 `a` 与 `u` 的内部有序对处求图 `F` 的值。这个取值来自图纤维，因而已经是可构造集合；值域子句再提供它属于 `α` 的证明。因此 `app` 在载体 `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))
```

求值并未失去与内部图的联系。定理 `app-graph` 记录：以 `(a,u)` 的外围对码为输入、以 `app a u` 为输出的有序对属于 `F`。可构造有序对的投影等式提供两种输入码之间所需的等同。

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

若两次应用的输出相等，`F` 的单射性先认同它们的编码对输入。有序对码的单射性再把这条相等拆成两个第一坐标相等与两个第二坐标相等。因此可以剥去一层应用，而无需构造 `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
```

对输入对的比较先从可构造对码转到外围 Kuratowski 对码，再转回去。完成这些搬运后，有序对的单射性恰好给出 `app-inj` 所需的两条分量相等；无需比较随附的隶属证明。

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

配套的唯一性事实沿正向使用图。若 `F` 在输入对 `(a,u)` 处记录某个取值 `w`，则 `w` 必须等于已经提取的取值 `app a u`。这是图的单值性，与不同输入之间的单射性无关。

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

为应用单值性，先把给定的隶属从外围对码搬运到 `val` 所用的可构造对。随后将它与 `val-graph` 给出的典范图隶属比较。此时两条记录具有相同输入，单值性子句便认同它们的输出。

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

环境读取被延拓为数码上的全函数：在序列范围之外它返回数码零。这个垃圾值不携带数学含义；后文的一切使用都只在长度以下的索引处读取该延拓。

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

由对索引的递归，在长度以下的每个索引处，延拓读回的恰是序列的该条目。

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

固定长度 `n` 与序列 `g` 后，`chain n g k` 按步数参数 `k` 递归定义。初值为数码零；在每个满足 `k<n` 的步骤中，配对函数作用于下一条目 `g(k)` 与此前的累积值。因此 `chain n g n` 恰好消耗序列的 `n` 个条目；超过此界后的行为只依赖 `ext` 给出的无意义默认值，不属于序列码的数学内容。

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

对长度为 `n` 的序列，折叠终止于 `vₙ = chain n g n`。其码定义为 `F(n,vₙ)`：最终配对的第一坐标是长度数码，第二坐标是折叠值。给定 `n` 与 `g` 后，这一定义产出实际取值；它既不声称 `α` 的每个元素都是码，也不定义 `α` 全域上的解码器。

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

设两条折叠链在 `k` 步后相等，则它们在每个位置 `j<k` 的条目都相等。归纳沿链反向进行：第 `k+1` 阶段的相等经 `F` 的单射性分解为第 `k` 阶段所用条目的相等，以及此前链值的相等。

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

在后继阶段，`app-inj` 给出这两条相等。若 `j=k`，第一条正是所需的条目相等；若 `j<k`，第二条使归纳假设可用于更短的链。这是在两条已知合法折叠之间作消去，并不是把 `α` 的任意元素变成序列的过程。

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

长度标签在此发挥作用。若两个码相等，外层应用的单射性先恢复长度数码的相等，继而得到自然数长度相等。把两条序列传输到同一长度后，沿折叠反向消去便得到逐项相等，因而两个环境图的底层集合相等。这里仅断言这一方向。

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

成对的结论 `q` 把码等式分成数码坐标的相等与终端折叠值的相等。族 `P m` 准确记录长度为 `m` 时尚待证明的结论，使数码单射性能够把第二条序列及其折叠等式传输到原长度 `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)
```

长度一致后，环境图的相等由函数外延性推出。对每个有穷索引 `i`，证明比较 `α` 的两个相应呈现成员；呈现嵌入的单射性把成员相等化为从两条链恢复的底层集合相等。

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

位置 `i` 处的比较先用 `ext-at` 把有界全域函数 `ext n g` 的取值认同为真正条目 `g i`。由于 `toℕ i<n`，链消去引理给出两个全域取值的相等；再次使用 `ext-at`，便把另一端认同为 `h i`。`ext` 在此界之外的取值不具数学作用。

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

为在语义层描述一次递归转移，固定索引对象 `i`。`StepAt s C i` 仅记录对象 `j,a,u,w`，满足：`j` 是 `i` 的后继，序列图给出 `s(i)=a`，轨迹给出 `C(i)=u` 与 `C(j)=w`，而图 `F` 给出 `F(a,u)=w`。整组数据经过命题截断。

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

最后一条隶属断言把递推等式写成图事实：输入是有序对 `(a,u)`，输出是 `w`。因此 `StepAt` 是稍后的一阶步进公式所要表达的宿主层含义；它尚未加入任何解码器，也未选择一条全局轨迹。

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

`DomIs s n` 表示 `n` 恰是序列图 `s` 的定义域。每个 `x∈n` 都有某个 `y` 使 `(x,y)∈s`，而每个 `(x,y)∈s` 的第一坐标 `x` 都属于 `n`。取值的存在性只以命题截断保留；需要唯一性时，则由另行给出的环境条件保证。

```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` 表示 `C` 是取值于 `α`、定义域恰为 `m` 的环境。通过 `envOverAt`，这同时包含单值性、定义域条件、所有取值均属于 `α`，以及 `C` 的每个成员都是有序对。这里 `m` 将是序列长度的后继，因此轨迹具有从 `0` 到 `n` 的各个位置。

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

完整的语义见证先给出数码 `n∈ω`、其后继 `m` 与轨迹环境 `C`。它要求 `s` 的定义域为 `n`，`C` 的定义域为 `m` 且取值于 `α`，并以 `C(0)=0` 开始。随后对每个 `i∈n` 给出一次转移，最后给出 `C(n)` 处的取值，使它与 `n` 配对后得到 `y`。这项见证经过命题截断。

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

最后一个分量把终端轨迹值与长度标签分开记录。它给出某个 `v`，满足 `(n,v)∈C` 且 `F(n,v)=y`。转移子句把 `v` 确定为 `n` 次折叠后的结果；最后这次 `F` 的应用再记录长度，使不同长度的序列不能具有相同码。

```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 ⟩ ) ∥₁ ) ∥₁
```

嵌套量词会移动此前各变元的 de Bruijn 位置。缩写 `i0,i1,…` 统一命名这些位置：`i0` 是最新约束的变元，每取一次后继便向外移动一位。借助这套记号，下列公式能够陈述有限轨迹等式，并保持每次出现所指对象清楚可辨。

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

从 `i0` 到 `i4` 的名称覆盖轨迹公式的浅层部分，包括当前索引、其后继，以及一次递推步骤中新引入的邻近取值。它们的长度参数是多态的，因此增加更多约束后仍可复用同一位置名称。

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

接下来的位置在引入若干存在见证后，仍能指向轨迹环境与原有自由变元。因此同一公式可以同时指称旧轨迹值、新轨迹值，以及把二者联系起来的序列条目。

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

步进公式总共引入五个见证：后继索引 `j`、取值 `a,u,w`，以及 `(a,u)` 的对码。在这五层约束之下，原序列变元移动到位置 `i12`；这个较深索引来自约束深度，并不表示新增数学假设。

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

具体而言，`i12` 是在 `i8` 上再取四次后继。位置名称固定后，阅读下列定义时便可追踪各变元的数学角色，而无须逐层数后继构造子。

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

公式 `stepFo` 是 `StepAt` 的对象语言版本。它先选取 `j`，并断言 `j` 是当前索引 `i` 的后继；随后选取序列取值 `a`、新旧轨迹值 `u,w`，以及有序对 `(a,u)` 的码。

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

内层四个存在量词约束 `a,u,w` 及其对码。前三个应用子句分别表示 `s(i)=a`、`C(i)=u` 与 `C(j)=w`；配对子句把辅助码认同为 `(a,u)`。这些事实共同准备公式核心处的一条递推断言。

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

最内层合取项是递推的图事实：把 `F` 作用于辅助输入码，产出新值 `w`。前一条配对子句把该辅助码认同为有序对 `(a,u)`。两项合在一起，才在对象语言中表达折叠等式 `F(a,u)=w`。

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

最终长度公式说：编码环境中数码槽位处存在取值，且编码配对施于数码与该取值产出输出。

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

公式体在陈述轨迹条件前先显式保留两个辅助参数。它把 `b` 认同为固定字母表 `α`，把 `z` 认同为零数码，再断言 `m` 是所选长度 `n` 的后继。这些等式使后续通用的环境与应用公式能够特化到 `α` 与 `0`。

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

其余合取项依次施加定义域条件、环境覆盖条件、零条目等式、`n` 以下的全部转移，以及最终长度子句。对当前已经命名的对象而言，这些条件说明 `C` 是一条经编码配对从初始零连到输出的有限轨迹。随后 `fo` 的外层量词才断言这样的长度与轨迹存在。

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

完整图公式先用 `ωʟ` 上的有界量词绑定数码，再以嵌套存在量词绑定四个辅助对象，产出关于输出与序列的二元公式。

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

环境 `e7` 包含进入 `stepFo` 与 `finFo` 的内部量词前已有的七个对象。按 de Bruijn 次序，它们是 `z,b,C,m,n,y,s`，所以第零位是辅助零，而原输出与序列占据最外侧两位。后续约束会从环境前端继续扩张。

```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 ∷ []
```

为向外读取 `stepFo`，证明把其中经过命题截断的见证消去到命题 `StepAt s C i`。由此得到 `j,a,u,w` 与辅助对码，并取得后继子句、三个图应用子句、配对子句和 `F` 应用子句。辅助对码在其等式使用后便不再保留。

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

每条充分性等式都把一项满足判断传输为其预期的等式或图隶属。所得事实把 `j` 认作 `i` 的后继，从 `s` 读出 `a`，并从 `C` 读出 `u,w`；连同关于 `F` 的最后一条图事实，它们恰好组成 `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
```

配对充分性等式把辅助对象认同为有序对 `(a,u)`。沿这条等式传输 `F` 的应用事实，便得到递推所需的隶属 `((a,u),w)∈F`。至此完成从一阶步进公式到一次语义转移的向外读取。

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

向外读取 `finFo` 时，先取得终端轨迹值 `v` 与辅助对象 `q`。三个子句分别表示 `C(n)=v`、`q=(n,v)` 与 `F(q)=y`。由于目标经过命题截断，可以消去两个存在见证，只保留 `Wit` 所需的 `v` 及两条图事实。

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

充分性把三个子句分别化为表示 `C(n)=v` 与 `F(q)=y` 的隶属，以及等式 `q=(n,v)`。沿最后这条等式传输 `F` 中的隶属，便以 `(n,v)` 替换 `q`，得到图形式的 `F(n,v)=y`。

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

公式体含有八个合取项。前两项认同辅助对象 `b=α` 与 `z=0`；其余六项断言 `m=n+1`、`s` 的准确规定义域、`C` 的环境条件、`C(0)=0`、`n` 以下的全部转移，以及最终带长度标签的取值。再加上另行给出的 `n∈ω`，这些数据构成 `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∈ω
```

后继公式的充分性等式给出 `m=n+1`，而 `domAt` 的两个读法给出 `s` 的准确定义域隶属的两个方向。再利用 `b=α`，把环境公式从辅助基集 `b` 传输到固定的 `α`；这里不需要证明两条完整轨迹相等。

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

等式 `z=0` 把公式体中的子句 `C(z)=z` 化为初始条件 `C(0)=0`。有界全称子句由 `stepOut` 逐点读取，`finOut` 则给出带标签的终端取值。这些就是命题截断见证余下的各个分量。

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

完整公式的向外读法逐一消去五层嵌套存在量词，每层喂给体读取，直至装配出完整见证。

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

反向构造从一项经过命题截断的 `StepAt` 见证出发，把它映到 `stepFo` 的满足。对代表 `j,a,u,w`，先以其对码及这四个取值扩张环境；随后的子句再以对象语言形式重建后继断言与各条图断言。

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

各见证按 `stepFo` 约束它们的次序引入。反向使用后继与应用的充分性等式，把语义事实 `j=i+1`、`s(i)=a`、`C(i)=u` 与 `C(j)=w` 化为相应的满足判断。这里只是引入已有见证，并未从命题截断中作出选择，因此各层截断均得到保留。

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

典范可构造对 `prʟ a u` 充当辅助对变元的见证。配对充分性把其底层集合认同为 `(a,u)`，再传输隶属 `((a,u),w)∈F`，便得到所需的对象语言应用子句。一次转移的向内读取至此完成。

```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) )))) ∣₁ ∣₁ ∣₁ ∣₁ ) })
```

向内读取 `finFo` 时，从经过命题截断的终端取值 `v` 出发，其中 `C(n)=v` 且 `F(n,v)=y`。构造把这项见证映过 `finFo` 的两个存在量词：一个约束 `v`，另一个约束有序对 `(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)) →
```

以 `v` 与典范对 `prʟ n v` 扩张环境。反向使用应用充分性可表达 `C(n)=v`，反向使用配对充分性可认同对见证，再反向使用常元图 `F` 的应用充分性即可表达 `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 γ))
```

最后一次传输把以外围有序对 `(n,v)` 为输入的图隶属，化为使用可构造代表 `prʟ n v` 的满足。因此，终端子句得以重建，而没有在命题截断已携带的见证之外再作选择。

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

为重建公式体，假设六项实质性的轨迹条件：`m=n+1`、`s` 的准确规定义域、`C` 的环境条件、初始值、全部有界转移，以及带标签的终端取值。公式体余下两个合取项是固定的认同 `b=α` 与 `z=0`，无需额外假设。

```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 ⟩ ) ∥₁
```

在所选的七对象环境中，两个辅助条目按定义就是 `α` 与 `0`，所以公式体前两个合取项均由自反性证明。余下证明把已给的六项语义条件化为其余六个对象语言合取项。

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

反向使用后继充分性，便得到表示 `m=n+1` 的合取项。`domAt` 的引入读法组合 `DomIs` 的两个方向：由于图取值的存在经过命题截断，其中一个方向使用命题消去，另一方向本来就是直接蕴含。随后把环境条件传输到所选变元位置。

```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 ∷ []) γ
```

初始隶属 `C(0)=0` 经应用充分性给出第六个合取项。`n` 以下的每次转移由 `stepIn` 向内送入，`finIn` 则重建最终带标签的取值子句。连同此前五项事实，这些内容补全有限轨迹公式体的全部八个合取项。

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

完整公式的向内读法消去截断见证，并把五个对象沿五层嵌套存在量词注入，装配图公式的对象语言满足。

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

五个见证是 `n,m,C,α,0`：第一个通过 `ω` 上的有界存在量词引入，其余四个通过普通存在量词引入。固定选择 `α` 与 `0` 使公式体前两条等式由自反性成立，而 `bodyIn` 则提供后继、定义域、环境、初始、转移与终端子句。因此 `fo-in` 重建完整满足，而没有从命题截断见证中作出全局代表选择。

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

接下来要在一条真正的有限序列上检验该语义公式。固定长度 `N`、赋值 `g : Fin N → α`、可构造集合 `s`，以及一条把 `s` 的底层集合认同为环境图 `envS α g` 的等式。下列构造将证明这条已表示序列的公式输出存在且唯一。

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

对标准环境图，调用通用环境公式只需三个对象：基集 `α`、长度数码 `N` 与 `envS α g`。它们在 `δ` 中的 de Bruijn 次序使环境图位于第二位，数码位于第一位，基集位于第零位。

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

标准图 `envS α g` 已知是取值于 `α`、定义域为 `N` 的环境。从这项环境事实中投影定义域子句，便证明其准确定义域是数码 `#N`。稍后，这项事实将迫使同一序列的任何其他见证使用相同的有限长度。

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

为使用环境的查表定理，先要把赋值看成 `V` 中的一族集合。映射 `gV` 把每个有穷索引送到呈现元素 `g i` 所指名的底层集合；由于 `g i` 呈现 `α` 的一个成员，这正是该索引处记录的取值。

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

若 `k < N`，则典范环境包含一个有序对，其第一坐标是数码 `# k`，第二坐标是序列的第 `k` 项。证明先把 `k` 转为 `Fin N` 的元素，在该处应用查表规格，再把所得隶属证明运输回自然数索引。

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

等式 `ext-at` 把全域化查找 `ext N g (toℕ i)` 与真正的条目 `g i` 等同。随后，有界自然数与 `Fin N` 之间的往返恒等式把索引及所展示的取值都还原到原来的 `k`。

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

反向查表陈述表达每个合法索引处的单值性。若环境在 `k < N` 时包含 `(# k,a)`，则 `a` 的底层集合必等于真正第 `k` 项的底层集合；该索引处不能记录第二个不同的取值。

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

这一等同先在相应的 `Fin N` 索引处建立。查表等式首先确定 `a`，`ext-at` 再把全域化条目换回原赋值条目，最后由转换恒等式把结论运输回 `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
```

这里 `i = fromℕ' N k p` 是由界 `p : k < N` 保证存在的有穷索引。显式保留这个界十分关键，因为全域函数 `ext` 在该范围之外没有序列意义。

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

折叠共有 `N + 1` 个状态，从初值一直到处理完全部 `N` 个条目后的状态。每个状态已经带有属于 `α` 的证明；`fiber` 把这份隶属证明转成呈现元素，从而得到由 `Fin (suc N)` 索引的赋值 `h`。

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

族 `hV` 忘去呈现索引，回到它们所指名的 `V` 中底层集合。下文使用的纤维等式说明，这些集合恰是构造 `h` 时所取的折叠状态。

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

令 `C` 为这族状态的环境图。它的定义域长度为 `N + 1`，在 `k` 处记录处理完前 `k` 个序列条目后的折叠状态，其中包括 `k = 0` 处的初值与 `k = N` 处的终值。

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

对每个 `k < N + 1`，`chainMem` 给出预期图条目 `(# k, chain N g k)` 属于 `C` 的证明。与原序列相同，证明先转到 `Fin (suc N)` 中对应的元素，再调用环境的查表规格。

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

纤维等式把 `h i` 所指名的取值与实际折叠状态等同，而 `toFromId'` 还原原来的自然数索引。这两项等同完成图隶属证明，并未对 `N + 1` 之外的索引作任何断言。

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

固定等式 `e : fst s ≡ fst (envS α g)` 使我们能够把典范环境的事实用于被表示的序列 `s`。映射 `inS` 把 `envS α g` 中的典范图条目运输到 `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)
```

反向运输 `outS` 把 `s` 的任意图条目移回 `envS α g`。唯一性论证将使用这一方向，把任意见证链给出的条目与实际赋值条目比较。

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

现在验证典范码满足图公式。见证取有限长度数码 `# N`、它的后继 `#(N+1)` 以及状态环境 `C`；其余各项依次证明 `s` 的定义域、取值于 `α` 的状态链、零初值、每一步转移与最后一次配对图应用。

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

最后的存在子句由状态 `chain N g N` 见证。它在 `C` 的索引 `N` 处出现，而把配对图 `F` 应用于长度数码与该状态组成的有序对，所得正是 `code N g`；整个存在陈述仍经过命题截断。

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

为证明 `s` 的定义域是 `# N`，先取 `# N` 中的一个索引。典范环境在该索引处给出一个仅保持存在性的取值，再沿 `e` 运输其图隶属，便得到该有序对属于 `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))
```

反过来，若 `s` 包含第一坐标为 `x` 的有序对，运输会把它送回典范环境。该环境的已知定义域于是推出 `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))
```

对集合论索引 `i ∈ # N`，数码消去给出一个自然数 `k < N`，其数码与 `i` 相等。转移见证随后选取后继数码、序列真正的第 `k` 项以及折叠在 `k` 与 `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)
```

所需的转移事实现由两个典范环境与折叠的定义等式给出。序列条目属于 `s`，相邻的两个状态都属于 `C`，而 `app-graph` 记录 `F` 把该条目与旧状态组成的有序对送到新状态；各次运输只负责把 `# k` 换回原先给定的索引 `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)
```

仅有存在性还不足以使 `fo` 成为函数图。定理 `only` 证明：凡由 `Wit y s` 接受的输出 `y`，其底层集合都等于典范码。由于该等式是命题，可以先消去经过命题截断的见证，再开始唯一性论证。

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

固定一个任意见证，其中长度对象为 `n`，其后继为 `m`，状态环境为 `C'`。各项假设说明：`s` 的定义域是 `n`，`C'` 是长度为 `m` 且取值于 `α` 的环境，其初始条目为零，它在 `n` 以下遵守每一步折叠规则，并且终止状态与 `n` 配对后产生 `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' ⟩
```

终止子句 `hF` 只断言存在一个状态 `v`：它由 `C'` 记录在索引 `n` 处，并与 `n` 一同经 `F` 映到 `y`。它并未全局选取终止状态；下文只把它消去到表达输出唯一性的集合等式中。

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

见证中的长度 `n` 作为集合必等于典范数码 `# N`。二者都描述同一序列 `s` 的定义域：`hd` 给出任意见证中的描述，`dom0` 则经所选表示 `s = envS α g` 给出描述。外延性把该等式化为两个隶属蕴涵。

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

对向前蕴涵，由 `x ∈ n` 与 `hd` 可得 `s` 中仅保持存在性的一个有序对，其第一坐标为 `x`。把该有序对运输到典范环境，再读取其已知定义域，便得 `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))
```

对反向蕴涵，`x ∈ # N` 给出典范环境中的一个条目。把它运输到 `s` 后，`hd` 的反向部分推出 `x ∈ n`。因此，长度由序列的定义域恢复，而无须为每个序列选定一种表示。

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

由于 `C'` 满足环境条件，它是单值的。因此，`C'` 中第一坐标相同的两个有序对，其第二坐标的底层集合必相等。这个事实将用于比较 `C'` 记录的任意状态与折叠等式所强制的状态。

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

核心归纳断言：对每个 `k < N + 1`，`C'` 在索引 `k` 处记录的任何取值都等于典范折叠状态 `chain N g k`。在 `k = 0` 时，初始子句与 `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)) →
```

在后继情形，转移见证给出序列条目 `a`、旧状态 `u` 与新状态 `w`。典范序列的查表性质把 `a` 等同于第 `k` 个输入，归纳假设把 `u` 等同于典范旧状态，而 `F` 的功能性随后把 `w` 等同于典范新状态。

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

由后继索引的界可得 `k < N`，因而可以调用步进子句。该子句把 `w` 放在 `C'` 的后继索引处；单值性先把原先给定的取值 `v` 与 `w` 等同，前述应用论证再把 `w` 与 `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')))
```

前驱界是归纳所需的小型算术事实：由 `suc k < suc N` 得到 `k < N`。它保证第 `k` 个输入条目确实存在，并且 `k` 处的折叠步骤位于序列范围内。

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

最后还需确定所给输出 `y`。消去经过命题截断的终止见证后，得到见证长度 `n` 处记录的状态 `v`；底层集合等式 `n≡ : fst n ≡ # N` 把该隶属运输到索引 `N`，归纳结论便把 `v` 与典范折叠的最终状态等同。

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

终止子句还说明，`F` 把由 `fst n` 与 `fst v` 组成的有序对映到底层集合 `fst y`。把这两个输入换成 `# N` 与典范终态后，`F` 的功能性给出 `fst y ≡ fst (fst (code N g))`。这只证明满足图公式的输出具有唯一性，并未在 `α` 的任意元素上定义解码函数。

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

谓词 `Mem s` 就是 `s` 属于 `seqL α`。因此，后续构造只作用于取值于 `α` 的有穷环境图，而不是外围宇宙中的任意元素。

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

`s` 的一种表示只保留如下存在性：某个自然数长度 `n`、某个赋值 `g : Ix α n`，以及 `s` 与 `g` 的环境图相等。命题截断刻意忘去究竟是哪一种表示提供这些数据；这里没有全局选取长度或赋值。

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

由 `s ∈ seqL α`，`seqL-out` 首先给出仅保持存在性的某个有限长度，使 `s` 属于相应环境集。再读取该环境集的反向刻画，便得到仅保持存在性的赋值及所需图等式，从而建立 `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)
```

现在可以把图公式化为 `seqL α` 上的函数。每个具体表示 `(n,g,e)` 都给出候选值 `fst (code n g)`，并证明它唯一地占据 `s` 上的图纤维。把经过命题截断的表示映到这条同样经过命题截断的唯一存在陈述后，便可将其交给 `mereFunct`；后者把它转成所需的可缩性，而不选取首选表示。

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

对每一种表示，`fo-in` 证明典范码属于相应图纤维。若另一个 `y'` 也属于该纤维，`fo-out` 把其满足性证明转成见证，`AtSeq.only` 再把它与典范码等同。由于可构造性证明是命题，底层集合的相等即可给出带证明元素的相等。

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

关于可定义函数关系的一般定理现在给出其唯一取值运算。这里保留函数值，以及任何满足 `fo` 的输出都等于该值的原理；构造内部单射只需要这两项事实。

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

把 `fn s m` 定义为序列成员 `s` 的这个唯一取值。虽然记号中包含隶属证明 `m`，但隶属关系取值于命题，因此数学上的取值不依赖于在不同证明之间作选择。

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

只要 `s` 由长度为 `n` 的赋值 `g` 表示，作为 `S` 元素的编码值 `fst (code n g)` 就满足 `fo`；图取值的唯一性因而给出 `fn s m ≡ fst (code n g)`。这个比较对每个给定表示都成立，所以无须选取首选表示。

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

`fn` 的取值仍位于 `α` 中。由于目标隶属陈述是命题，可以消去经过命题截断的表示；对每个代表 `(n,g)`，`code n g` 的第二分量证明它属于 `α`，再由 `fn-code` 把该事实运输到 `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)
```

这些事实组成一个从 `seqL α` 到 `α` 的 `DefinableMap`。该记录把宿主层函数、函数值落在陪域中的证明与一阶公式 `fo` 一同保存：`defines` 证明所取之值满足该公式，`only` 则证明每个满足公式的输出都是这个值。下文证明单射性后，`Inj` 构造再用这些可定义性数据在 `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) }
```

为证明单射性，设两个序列成员的 `fn` 取值相等。它们的表示都经过命题截断，但所求的底层集合等式本身是命题，因此可以同时消去两份截断，比较任意代表 `(n,g)` 与 `(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
```

等式 `fn-code` 把两个 `fn` 取值的相等转为两个典范码的相等。先前证明的 `code-inj` 随即给出相应环境图相等；再与两条表示等式复合，便得 `fst s ≡ fst s'`。这是对合法码进行比较的证明，而不是定义在 `α` 全域上的解码运算。

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

该可定义映射与前述单射性证明共同给出从 `seqL α` 到 `α` 的内部单射。结论 `InjL` 是 `L` 中存在合适函数图的命题截断；它既不声称该映射满射，也不声称 `α` 的任意元素都能解码为有穷序列。

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

## 有限序列单射到无穷序数

最终定理去掉先前临时采用的假设，即已经给定 `α` 上的配对单射。构造出内部单射 `prodL α ↪ α` 后，其经过命题截断的图见证提供折叠构造所需的单值性、准确的定义域、单射性与值域事实，从而在 `L` 内得到 `seqL α ↪ α`。

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

为构造配对单射，只在局部取 `cardOf α oα` 给出的基数代表 `μ`。这个代表经过命题截断才可得，但目标 `InjL (prodL α) α` 本身也是命题，所以可以对任意代表完成构造，而不作全局选择。

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

代表 `μ` 是序数也是内部基数，并且 `α` 与 `μ` 之间各有一条内部单射；`cardOf` 还给出包含 `μ ⊆ α`，不过本构造没有使用它。两条单射从两个方向比较基数大小，但并不把 `μ` 与 `α` 定义性地等同。

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

所需配对单射是复合 `α² ↪ μ² ↪ μ ↪ α`。第一条箭头把 `α ↪ μ` 逐坐标应用，居中的箭头是无穷内部基数 `μ` 的平方律，最后一条箭头回到 `α`。因此，平方律施用于基数代表，而不是直接施用于任意无穷序数。

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

最后还要证明 `μ` 具有平方律所需的无穷性。若 `μ ∈ ω`，则 `μ` 是有穷序数，而已有的内部单射 `α ↪ μ` 会把无穷序数 `α` 单射到其中；`no-fin` 利用 `α`、`μ` 的序数性与 `α` 的无穷性排除这种情形。

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