在 L 内部构造序型

把 L 中编码的关系成员表示为小类型后，便可对良基关系作塌缩。传递性进一步保证每个塌缩值都是序数，因而属于 L。本章把这些值收集成精确值域 otL，并另行收集图 colTable；本章没有封装 otL 的序数性定理。只有再加入三歧性之后，这张图才成为从原定义域到该值域的编码单射。

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

经典假设在此显式给出，因为后文的一项存在性证明必须判定候选点是否在当前点之前。良基递归本身不需要这项判定；排中律进入之处，是按关系成立与否定义一项统一的替换函数时。

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

固定宇宙层级 ℓ，并在可构造载体所需的层级上给定排中律实例。此模块后续的构造都继承这一项经典参数；它没有被隐藏成公理。

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

塌缩将由集合论一阶语言中的公式识别。有序对的隶属与相等提供原子检验，合取、析取、蕴含、否定及无界量词则表达表的各项条件。「对每个前驱」这类看似受限的量化，通过把关系原子放在蕴含前件中表达，而不是使用有界量词构造子。

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

整个构造必须协调两种表示。为了进行良基递归，D 的成员通过一个小表示来处理；图的条目则仍是累积层级中编码为有序对的集合。表示与有序对编码的单射性，使后文能够从这些表示返回原成员和两个坐标。

open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset→isL )
open import L.Ordinal {ℓ} using ( suc-ord )

证明必须把递归定义的取值与 L 内部可满足的公式连接起来。良基递归产生塌缩，递归图把其取值与有序对收集成集合，编码公式再把这些对解释为应用。最后，层定理把每个序数塌缩值放入 L。

open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct )
open import L.Recursion.Graph {ℓ} lem
  using () renaming ( module Graph to RecursionGraph )
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; appC; appC-adequate; prʟ; prʟ-fst; svAt; domAt )

收集所得的图有两个不同层次的目标。首先，它必须把塌缩表示为 D 上全定义的单值关系；此后只有在三歧性下，它才能满足内部单射额外要求的输入唯一性条款。有序对公式表达这张图，而四项单射条件要在分别证明之后才被封装为单射码。

open import L.Coding.Expressions {ℓ} using ( module PairExpression )
open import L.Coding.Injection {ℓ} lem using ( injAt; injAt-in )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap ) renaming ( module Inj to DefinableInj )
open import L.Mostowski {ℓ} using ( module Mostowski )

后文的唯一性论证反复通过成员来比较可构造集合。外延性把逐点的隶属等价化为底层集合的相等，而取值为命题的证据使配对而成的可构造对象之相等不依赖具体证明。这也允许命题截断下的分情形以相等为目标结束，而不抽取固定选择。

open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ; isPropΣ; isSetΣSndProp )
open import Cubical.Functions.Logic using ( ⇔toPath )

累积层级同时提供外围集合及其成员的小表示。因此，D 的一个元素既可视为外围集合，也可视为小索引；隶属关系在两种视角之间传递所需的可构造性证据。层级集合上的后继运算稍后用于把序数塌缩值定位到该序数的后继层。

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

良基性提供定义并分析塌缩所需的归纳原理。空类型排除不可能的关系情形；当后续论证只需知道前驱或表项存在、而不需选定见证时，命题截断记录这种存在性。

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

以 S 表示可构造结构的载体。结构隶属 _∈ˢ_ 表达 L 的元素之间的隶属；它不同于下文用于读取外围层级集合之表示的小隶属 _∈ₛ_。

open hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )

这些公式将在 L 所承载的结构中解释。记号 S ^ n 表示由 n 个可构造集合组成的环境，而 γ ⊨ φ 表示公式 φ 在受限的可构造结构内部由环境 γ 满足。

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

底层层级载体 V ℓ 是 h-集合，而可构造性证据取值于命题。因此，依值对载体 S 也是 h-集合，即可构造集合之间的相等是命题。后文遂可把截断分情形消去到载体元素的等式中。

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

编码图在底层集合上读取：当 x 与 y 的底层元素构成的有序对属于 F 的底层集合时，记 F 对 x、y 成立。下文每条子句读取的都是这一形状。

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

固定可构造集合 D 与编码有序对的可构造集合 R。假设 Rsub 只说明 R 中每个实际出现的有序对之两个端点都属于 D。形成塌缩时另加良基性与传递性，证明单射性时才再加三歧性。本章始终没有假设关系具有外延性。

module Collapse (D R : S)
                (Rsub : (y x : S) → Holds R y x
                      → ⟨ fst y ∈ fst D ⟩ × ⟨ fst x ∈ fst D ⟩) where

D 中的隶属被陈述为载体上的一元谓词。

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

该谓词是命题，因为它是被呈现集合的底层集合中的隶属。这一命题性后文有用：某构造可以依赖于隶属证明，而不因此携带任何选择数据。

  isPropMem : (x : S) → isProp (Mem x)
  isPropMem x = snd (fst x ∈ fst D)

D 的成员由一个小类型呈现；这个小类型就是该呈现的索引类型。

  Dom : Type ℓ
  Dom = ⟪ fst D ⟫

呈现把其索引嵌入外围层级。

  ↪ : Dom → V ℓ
  ↪ = ⟪ fst D ⟫↪

索引被转回可构造集合：嵌入的成员与沿 D 的隶属、由可构造性传递性搬运而来的可构造性证明配对。

  up : Dom → S
  up m = ↪ m , isL-trans {x = fst D} {y = ↪ m} (member (fst D) m) (snd D)

重建出的可构造集合是 D 的成员，这由呈现自身的隶属记录给出。

  up-mem : (m : Dom) → Mem (up m)
  up-mem m = member (fst D) m

该表示没有重复索引：两个嵌入成员相等会迫使其索引相等。后文从已知成员 up b 恢复索引时，这一点把恢复所得索引认同为 b 本身，从而证明收集所得的图含有预期的对 (↪ b, col b)。塌缩函数的单射性是另一项结论，并且需要三歧性。

  Dom≡ : {a b : Dom} → ↪ a ≡ ↪ b → a ≡ b
  Dom≡ {a} {b} e = ↪-inj {a = fst D} {m = a} {n = b} e

反过来，D 的成员连同其隶属证明，通过取呈现在该成员处的纤维，恢复出一个呈现索引。

  toDom : (x : S) → Mem x → Dom
  toDom x mx = fst (fiber (fst D) mx)

恢复出的索引恰好呈现所给的成员：纤维携带嵌入索引与该成员的同一视。

  toDom-val : (x : S) (mx : Mem x) → ↪ (toDom x mx) ≡ fst x
  toDom-val x mx = snd (fiber (fst D) mx)

码 R 在小表示上诱导一条关系：a ≺ b 表示由被表示成员 ↪ a 与 ↪ b 组成的有序对属于 R。良基递归正沿这条关系进行。下面两条引理把它与可构造集合上的 Holds R (up a) (up b) 双向连接起来。

  opaque
    _≺_ : Dom → Dom → Type ℓ
    a ≺ b = ⟨ pr (↪ a) (↪ b) ∈ₛ fst R ⟩

对固定索引 a 与 b，关系类型 a ≺ b 是命题，因为它陈述一个层级集合中的隶属。因此，这条关系只记录边是否存在，不包含由某个特定证明携带的额外数据。这项命题性本身并不判定边是否存在；只有后文真正需要这种判定时才使用排中律。

    isProp≺ : (a b : Dom) → isProp (a ≺ b)
    isProp≺ a b = snd (pr (↪ a) (↪ b) ∈ₛ fst R)

编码关系中的隶属给出小关系：L 中记录的有序对由两种隶属关系之间的桥识别。

    ≺-in : (a b : Dom) → Holds R (up a) (up b) → a ≺ b
    ≺-in a b = ∈∈ₛ {a = pr (↪ a) (↪ b)} {b = fst R} .fst

反过来，小关系记录了 R 中真实的对，于是关系的两种读法在两个方向上一致。

    ≺-out : (a b : Dom) → a ≺ b → Holds R (up a) (up b)
    ≺-out a b = ∈∈ₛ {a = pr (↪ a) (↪ b)} {b = fst R} .snd

关系 _≺_ 的良基性提供定义 col 所需的递归与归纳。传递性承担另一项作用：它保证前驱链仍位于其上端点之下，从而可以证明每个塌缩值传递并成为序数。这两项假设尚不能保证塌缩单射，也没有把该关系封装成良序。

  module Col (wf : WellFounded _≺_)
             (≺-trans : {a b c : Dom} → a ≺ b → b ≺ c → a ≺ c) where

Mostowski 构造把 col p 定义为所有前驱 r ≺ p 的取值 col r 所成的集合。计算律 col-eq 把递归取值与这一显式前驱像认同。隶属引理从指定前驱得到 col r ∈ col p；反过来，从任意成员只得到命题截断下的前驱存在。col-ord 则证明每个单独的 col p 都是序数。

    open Mostowski Dom _≺_ wf ≺-trans public
      using ( module W; col; col-eq; col-in; col-out; col-ord )

每个塌缩值都可构造。引理 col-ord 先说明 col p 是序数；层引理随后把这个序数置于由其后继索引的层中，从而得到 col-isL p。

    opaque
      col-isL : (p : Dom) → ⟨ isL (col p) ⟩
      col-isL p = Lset→isL (sucV (col p)) (suc-ord (col-ord p)) (col p)
                    (ord∈Lset-suc (col p) (col-ord p))

每个塌缩值连同其可构造性证明被打包为可构造集合。塌缩因此产出的不只是外围集合，而是可构造宇宙的真实元素。

    colʟ : Dom → S
    colʟ p = col p , col-isL p

诸公式

若 x 的每个 R 前驱 y 都在表 F 中记录了某个取值 u，就称 F 在 x 处完备。u 的存在处于命题截断之下：完备性只保留表项存在这一事实，既不选定某个表项，也尚未断言取值唯一。

Complete : S → S → S → Type (ℓ-suc ℓ)
Complete F R x = (y : S) → Holds R y x → ∥ Σ[ u ∈ S ] Holds F y u ∥₁

谓词 Src F R x w 表示：F 在 x 的某个 R 前驱处把 w 记录为取值。该前驱及其表项都留在命题截断之下，因为后文只使用由此得到的隶属事实。

Src : S → S → S → S → Type (ℓ-suc ℓ)
Src F R x w = ∥ Σ[ y ∈ S ] (Holds R y x × Holds F y w) ∥₁

值 v 对 x 是正确的，当其成员恰为来源值：v 中的隶属给出一个来源，而每个来源都是成员。两个方向合起来说：v 就是所记录的前驱值之集，完全通过隶属读取。

ValueIs : S → S → S → S → Type (ℓ-suc ℓ)
ValueIs F R x v = (w : S) → (⟨ fst w ∈ fst v ⟩ → Src F R x w)
                          × (Src F R x w → ⟨ fst w ∈ fst v ⟩)

若一张表实际包含的每个有序对都在其输入处完备，并且输出恰由前驱取值组成，就称该表正确。这项条件没有指定定义域，因此既不要求覆盖整个 D，也不禁止在 D 之外出现条目。后文的唯一性定理只在被记录的输入属于 D 时，才把相应取值认同为塌缩值。

Correct : S → S → Type (ℓ-suc ℓ)
Correct F R = (x v : S) → Holds F x v → Complete F R x × ValueIs F R x v

公式 completeAt f R x 用无界全称量词引入候选前驱 y。蕴含只关注 R 记录有序对 (y,x) 的那些 y，其结论再用无界存在量词引入取值 u，要求 F 记录 (y,u)。进入存在量词后，u 占据新的第零槽位，原有变量相应后移。

opaque
  completeAt : ∀ {n} → Fin n → S → Fin n → Formula S n
  completeAt f R x =
    ∀̇ ( appC R zero (suc x)
      ⇒̇ ∃̇ (appAt (suc (suc f)) (suc zero) zero) )

要把该公式读成宿主层完备性，先固定前驱 y 及 R 记录 (y,x) 的证明。appC 的充分性路径把这一前提化为满足证明 h 所需的蕴含前件。应用 h 后得到命题截断下的候选取值；PT.map 保留该截断，并沿 appAt 的充分性路径把其中的图原子化为 Holds F y u。

  complete-out : ∀ {n} (f : Fin n) (R : S) (x : Fin n) (γ : S ^ n)
               → ⟨ γ ⊨ completeAt f R x ⟩
               → Complete (lookup f γ) R (lookup x γ)
  complete-out f R x γ h y p = PT.map
    (λ { (u , q) → u , subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (u ∷ y ∷ γ)) q })

这一方向的最后一次应用完成上述第一项转换：它沿 appC-adequate 搬运已给的关系事实，再把结果交给 h y。所得结果仍是对象语言语义产生的截断存在；前几行的映射只改变命题截断内部的内容。

    (h y (subst ⟨_⟩ (sym (appC-adequate R zero (suc x) (y ∷ γ))) p))

反过来，假设宿主层完备性。对满足公式前件的候选前驱，先由 appC-adequate 把该前件化为 Holds R y x。完备性给出命题截断下的取值 u，PT.map 再把伴随的 Holds F y u 搬回存在结论所需的应用原子满足证明。

  complete-in : ∀ {n} (f : Fin n) (R : S) (x : Fin n) (γ : S ^ n)
              → Complete (lookup f γ) R (lookup x γ)
              → ⟨ γ ⊨ completeAt f R x ⟩
  complete-in f R x γ h y p = PT.map
    (λ { (u , q) → u , subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (u ∷ y ∷ γ))) q })

这一行把已满足的关系原子式转换为 Holds R y x，再把 x 处的完备性施用于候选前驱 y。这次应用给出截断取值，外围的映射随后把它转换为对象语言存在量词所需的见证。

    (h y (subst ⟨_⟩ (appC-adequate R zero (suc x) (y ∷ γ)) p))

公式 srcAt f R x w 用无界存在量词断言某个 y 同时是 x 的 R 前驱，并且 F 在输入 y 处记录 w。对前驱的限制由第一个合取项表达，而不是由有界存在量词表达。

opaque
  srcAt : ∀ {n} → Fin n → S → Fin n → Fin n → Formula S n
  srcAt f R x w = ∃̇ ( appC R zero (suc x) ∧̇ appAt (suc f) zero (suc w) )

该语义存在式已经处于命题截断之下。定义 src-out 的映射保留这一截断，并转换其中每个假定见证 y：appC-adequate 把第一个合取项读成 Holds R y x，appAt-adequate 把第二个读成 Holds F y w。

  src-out : ∀ {n} (f : Fin n) (R : S) (x w : Fin n) (γ : S ^ n)
          → ⟨ γ ⊨ srcAt f R x w ⟩
          → Src (lookup f γ) R (lookup x γ) (lookup w γ)
  src-out f R x w γ = PT.map (λ { (y , (p , q)) → y
    , ( subst ⟨_⟩ (appC-adequate R zero (suc x) (y ∷ γ)) p

前驱的图隶属闭合该读取。

      , subst ⟨_⟩ (appAt-adequate (suc f) zero (suc w) (y ∷ γ)) q ) })

填充来源是其反向：把前驱引入存在量词，两个原子逆着各自充分性引理搬运。

  src-in : ∀ {n} (f : Fin n) (R : S) (x w : Fin n) (γ : S ^ n)
         → Src (lookup f γ) R (lookup x γ) (lookup w γ)
         → ⟨ γ ⊨ srcAt f R x w ⟩
  src-in f R x w γ = PT.map (λ { (y , (p , q)) → y
    , ( subst ⟨_⟩ (sym (appC-adequate R zero (suc x) (y ∷ γ))) p

图原子最后写入，填充完成。

      , subst ⟨_⟩ (sym (appAt-adequate (suc f) zero (suc w) (y ∷ γ))) q ) })

公式 valueAt f R x v 对任意集合 w 量化，并同时陈述 w ∈ v 与 srcAt f R x w 之间的两个方向。因此，它给出 v 的外延刻画：v 的成员恰是 x 的各前驱处所记录的取值。定义展开 srcAt，使这一刻画成为一条完整的一阶公式。

opaque
  unfolding srcAt
  valueAt : ∀ {n} → Fin n → S → Fin n → Fin n → Formula S n
  valueAt f R x v =
    ∀̇ ( ((var zero ∈̇ var (suc v)) ⇒̇ srcAt (suc f) R (suc x) zero)

双条件即其两个方向的合取，而来源公式在两个方向内均已展开。

      ∧̇ (srcAt (suc f) R (suc x) zero ⇒̇ (var zero ∈̇ var (suc v))) )

向外读取 valueAt 时，要在每个 w 处实例化其全称量词。正向蕴含先把 v 中的隶属转换为来源公式的满足，src-out 再把这份满足读成 Src F R x w，从而得到 ValueIs 的正向一半。

  value-out : ∀ {n} (f : Fin n) (R : S) (x v : Fin n) (γ : S ^ n)
            → ⟨ γ ⊨ valueAt f R x v ⟩
            → ValueIs (lookup f γ) R (lookup x γ) (lookup v γ)
  value-out f R x v γ h w =
      (λ w∈ → src-out (suc f) R (suc x) zero (w ∷ γ) (h w .fst w∈))

反向对称地经来源填充读取。于是该公式恰在说：v 收集来源值；这正是后文唯一性论证所消耗的读法。

    , (λ s → h w .snd (src-in (suc f) R (suc x) zero (w ∷ γ) s))

为证明 valueAt 的正向蕴含，取候选取值 v 的一个成员 w。宿主级取值方程说，在命题截断下，w 已经作为 x 的某个 R 前驱之取值出现。把这条来源陈述向内读取，便在以 w 扩展的环境中给出对象语言公式所需的存在见证。

  value-in : ∀ {n} (f : Fin n) (R : S) (x v : Fin n) (γ : S ^ n)
           → ValueIs (lookup f γ) R (lookup x γ) (lookup v γ)
           → ⟨ γ ⊨ valueAt f R x v ⟩
  value-in f R x v γ h w =
      (λ w∈ → src-in (suc f) R (suc x) zero (w ∷ γ) (h w .fst w∈))

对逆向蕴含，先把来源公式的满足读成一种命题截断的存在：某个前驱的表值是 w。随后，ValueIs 的反向一半证明 w 属于所记录的值。因此，valueAt 恰好表达相对于候选表的递归取值方程；稍后还须借助良基归纳，才能把这个值认同为 Mostowski 塌缩。

    , (λ s → h w .snd (src-out (suc f) R (suc x) zero (w ∷ γ) s))

正确性只在候选表确实含有表项之处接受检验。两层全称量词遍历实参 x 与取值 v；若表中含有有序对 (x,v)，公式便要求这个表项满足递归步骤所需的两项条件。

opaque
  unfolding completeAt valueAt
  correctAt : ∀ {n} → Fin n → S → Formula S n
  correctAt f R =
    ∀̇ (∀̇ ( appAt (suc (suc f)) (suc zero) zero

这两项条件把存在性与取值方程分开。完备性说，x 的每个 R 前驱在表中都有某个表项；取值子句则说，v 的成员恰是这些前驱表项处出现的取值。除此以外，公式并不规定表的定义域。

          ⇒̇ ( completeAt (suc (suc f)) R (suc zero)
            ∧̇ valueAt (suc (suc f)) R (suc zero) zero ) ))

向外读取公式时，先取表中一个实际表项 (x,v)。appAt 的充分性把它的隶属证明转换为公式前件所需的证明。在 x 与 v 处实例化两层量词后，便得到 x 处的完备性及相应的取值方程；本行把其中的完备性一半读回宿主级谓词。

  correct-out : ∀ {n} (f : Fin n) (R : S) (γ : S ^ n)
              → ⟨ γ ⊨ correctAt f R ⟩ → Correct (lookup f γ) R
  correct-out f R γ h x v p =
    let (c , w) = h x v (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (v ∷ x ∷ γ))) p)
    in complete-out (suc (suc f)) R (suc zero) (v ∷ x ∷ γ) c

第二分量由 value-out 读取，得到「属于 v」与「作为 x 的某个 R 前驱之取值出现」之间的等价。它与完备性配对后，证明所选表项在宿主级正确。由于该构造适用于表中每个表项，最终便得到 Correct F R。

     , value-out (suc (suc f)) R (suc zero) zero (v ∷ x ∷ γ) w

反过来，设该表在宿主级正确。选定实参 x、取值 v 与表项 (x,v) 后，appAt 的充分性把对象语言蕴含的前件转换为相应的宿主级表项。正确性随即给出该表项的完备性与取值方程；本行把其中的完备性一半填入公式。

  correct-in : ∀ {n} (f : Fin n) (R : S) (γ : S ^ n)
             → Correct (lookup f γ) R → ⟨ γ ⊨ correctAt f R ⟩
  correct-in f R γ h x v p =
    let (c , w) = h x v (subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (v ∷ x ∷ γ)) p)
    in complete-in (suc (suc f)) R (suc zero) (v ∷ x ∷ γ) c

取值方程由 value-in 填入，从而补全表项 (x,v) 所需的合取。再对选定的两个元素作抽象，便得到两层全称量词。因此，correct-in 与 correct-out 建立了 correctAt 和宿主级谓词 Correct 之间的精确对应。

     , value-in (suc (suc f)) R (suc zero) zero (v ∷ x ∷ γ) w

下一个公式固定关系 R，但仍以存在量词绑定作为见证的表。这种区分具有数学作用：在尚未构造出覆盖整个定义域的单一表之前，便可先借某张正确表局部识别一个取值。

module ColFo (R : S) where

在环境 (z ∷ p ∷ []) 中，该公式说：命题截断地存在集合 F，它对 R 正确，并含有表项 (p,z)。表由存在量词绑定，所以这里只是刻画 p 处取值的局部陈述，尚未断言有一张固定表同时适用于整个定义域。

  opaque
    unfolding correctAt
    colFo : Formula S 
    colFo = ∃̇ ( correctAt zero R
              ∧̇ appAt zero (suc (suc zero)) (suc zero) )

向外读取 colFo 时，表见证外面的命题截断仍被保留。存在量词给出表 F；在同一截断内部，合取项给出 F 对 R 正确的证据，以及表示表项 (p,z) 的对象语言应用原子式。

    colFo-out : (z p : S) → ⟨ (z ∷ p ∷ []) ⊨ colFo ⟩
              → ∥ Σ[ F ∈ S ] (Correct F R × Holds F p z) ∥₁
    colFo-out z p = PT.map (λ { (F , (hc , ha)) → F
      , ( correct-out zero R (F ∷ z ∷ p ∷ []) hc
        , subst ⟨_⟩ (appAt-adequate zero (suc (suc zero)) (suc zero)

appAt 的充分性把余下的应用原子式转换为 Holds F p z。因此，结果是在命题截断下得到一张正确表及所需表项，这正是该公式的宿主级读法。

            (F ∷ z ∷ p ∷ [])) ha ) })

对向内方向，一张明确给定且含有 (p,z) 的正确表 F 充当存在见证。正确性证明由 correct-in 转入公式；余下任务是用应用原子式表达给定的表项。

    colFo-in : (z p F : S) → Correct F R → Holds F p z
             → ⟨ (z ∷ p ∷ []) ⊨ colFo ⟩
    colFo-in z p F hc hp = ∣ F
      , ( correct-in zero R (F ∷ z ∷ p ∷ []) hc
        , subst ⟨_⟩ (sym (appAt-adequate zero (suc (suc zero)) (suc zero)

反向使用 appAt 的充分性，便把 Holds F p z 转换为该原子式的满足。随后将表见证、其正确性与这个表项一起置于存在量词的命题截断中，即得 colFo 在 (z,p) 处的满足。

            (F ∷ z ∷ p ∷ []))) hp ) ∣₁

稍后需要把 colFo 这样的逐点取值公式用于定义有序对集合。通用构造 PairFo 完成这一转换：它恰在 z 于 p 处满足给定公式时识别有序对 (p,z)。因此，局部塌缩公式能够充当下文递归构造的取值关系。

open import L.Recursion.Graph {ℓ} lem public using ( module PairFo )

唯一性、存在性与诸表

内部构造从编码定义域 D 与编码关系 R 出发。起初唯一的附加条件是：属于 R 的每个有序对，其两个坐标都属于 D。该模块边界尚未要求良基性与传递性；塌缩论证开始时才会另行给出这两项条件。

module Internal (D R : S)
                (Rsub : (y x : S) → Holds R y x
                      → ⟨ fst y ∈ fst D ⟩ × ⟨ fst x ∈ fst D ⟩) where

定义域表示及其编码关系现在成为两种公式构造的共同背景。CF 是关系 R 的局部塌缩取值公式，PF 则识别由实参与满足该公式的取值组成的有序对。此时，这两个构造都尚未断言塌缩取值存在或唯一。

  open Collapse D R Rsub public
  module CF = ColFo R using ( colFo; colFo-in; colFo-out )
  module PF = PairFo CF.colFo using ( pair-in; pair-out; pairFo )

若 q 是 D 的成员，对其成员证明解码便得到索引 toDom q mq。由 toDom-val，把该索引重新嵌入后所得元素与 q 具有相同的底层迭代集合；又因 S 的可构造性分量为命题，底层集合的相等可提升为 S 中的相等。

  up-toDom : (q : S) (mq : Mem q) → up (toDom q mq) ≡ q
  up-toDom q mq = Σ≡Prop (λ v → snd (isL v)) (toDom-val q mq)

塌缩公式通过环境的第二槽依赖实参。因此，等式 x ≡ y 允许直接在该槽中替换：若取值 v 在 x 处满足公式，它也在 y 处满足公式。稍后正是借此把典范表示 up (toDom q mq) 与原元素 q 协调起来。

  colFo-at : (v : S) {x y : S} → x ≡ y
           → ⟨ (v ∷ x ∷ []) ⊨ CF.colFo ⟩ → ⟨ (v ∷ y ∷ []) ⊨ CF.colFo ⟩
  colFo-at v e = subst (λ t → ⟨ (v ∷ t ∷ []) ⊨ CF.colFo ⟩) e

此模块现在假定小关系既良基又传递。良基性支撑 col 的递归定义以及唯一性证明中的诸次归纳；传递性则用于证明所得塌缩值为序数。这两项假设作用不同，且都不由先前对 R 的端点条件推出。

  module Graph (wf : WellFounded _≺_)
               (≺-trans : {a b c : Dom} → a ≺ b → b ≺ c → a ≺ c) where

在这两项假设下，Mostowski 递归为每个 a 指派集合 col a，其成员是诸前驱的塌缩值。相应的引入与消去引理刻画该集合的隶属，而 col-ord 证明每个单独的 col a 都是序数。这里说的是逐点塌缩值，尚不是稍后收集得到的集合 otL。

    open Col wf ≺-trans public

良基性排除了环 a ≺ a。在归纳步骤中，若有这样的环，便可把面向前驱的归纳假设施于 a 自身；同一份环证明既说明 a 比自身更小，也充当归纳假设产出矛盾时的输入。

    ≺-irrefl : (a : Dom) → a ≺ a → Empty.⊥
    ≺-irrefl = W.induction {P = λ a → a ≺ a → Empty.⊥} (λ a rec h → rec a h h)

此处的唯一性陈述以表项已经存在为条件：若正确表 F 在真实定义域点 up a 记录取值 v，则 v 的底层集合等于 col a。它并不声称每张正确表在 D 的每个成员处都有表项。证明对 a 作良基归纳，并以所示等式为归纳谓词。

    correct-val : (F : S) → Correct F R → (a : Dom) (v : S)
                → Holds F (up a) v → fst v ≡ col a
    correct-val F hc = W.induction {P = λ a → (v : S) → Holds F (up a) v → fst v ≡ col a} go
      where
      go : (a : Dom) → ((b : Dom) → b ≺ a → (v : S) → Holds F (up b) v → fst v ≡ col b)

证明化归为逐点等价：w 属于被记录取值当且仅当 w 属于塌缩。从正确性假设提取两个辅助事实：up a 处的完备性，以及取值子句。

         → (v : S) → Holds F (up a) v → fst v ≡ col a
      go a IH v hv = extensionalV {a = fst v} {b = col a} (λ w → ⇔toPath (fwd w) (bwd w))
        where
        cmp : Complete F R (up a)
        cmp = hc (up a) v hv .fst

a 处表项的正确性有两项互补后果。前面的 cmp 为所有前驱提供表项，而 val 把对 v 的隶属与作为某个前驱取值出现相互认同。接下来的外延性论证在两个方向中以相反次序使用这两项事实。

        val : ValueIs F R (up a) v
        val = hc (up a) v hv .snd

为证第一向包含，取被记录取值 v 的成员 w。由于 v 可构造，成员关系也使 w 可构造，故可将其打包为载体元素 wS。随后，val 的正向一半在命题截断下给出 a 的某个 R 前驱 y，表在该处记录 wS。

        fwd : (w : V ℓ) → ⟨ w ∈ fst v ⟩ → ⟨ w ∈ col a ⟩
        fwd w w∈ = PT.rec (snd (w ∈ col a)) read (val wS .fst w∈)
          where
          wS : S
          wS = w , isL-trans {x = fst v} {y = w} w∈ (snd v)

来源条目被转换为所需的两条事实：被载前驱与实参之间的关系，以及被载前驱处的表条目。前驱随后被解码为其内部索引。

          read : Σ[ y ∈ S ] (Holds R y (up a) × Holds F y wS) → ⟨ w ∈ col a ⟩
          read (y , (ry , fy)) = subst (λ t → ⟨ t ∈ col a ⟩) (sym e) (col-in a b b≺a)
            where
            my : Mem y
            my = Rsub y (up a) ry .fst

内部索引 b 由隶属下降而恢复，关系条目被运输为内部形式 b ≺ a。等式 e 记录 w 与 b 的塌缩的认同，下一步证明。

            b : Dom
            b = toDom y my
            b≺a : b ≺ a
            b≺a = ≺-in b a (subst (λ t → ⟨ pr t (↪ a) ∈ fst R ⟩) (sym (toDom-val y my)) ry)
            e : w ≡ col b

该等式恰是把归纳假设施于解码后的前驱：表在被载前驱处的取值等于其内部索引的塌缩，经运输即等于 w。

            e = IH b b≺a wS (subst (λ t → ⟨ pr t w ∈ fst F ⟩) (sym (toDom-val y my)) fy)

为证反向包含，设 w ∈ col a。塌缩的消去规则在命题截断下给出某个前驱 r ≺ a，并有 col r ≡ w。目标 w ∈ fst v 是命题，故可以在该截断内部推理。又因 w 属于可构造集合 col a，所以可把它连同可构造性证据打包为 wS。

        bwd : (w : V ℓ) → ⟨ w ∈ col a ⟩ → ⟨ w ∈ fst v ⟩
        bwd w w∈ = PT.rec (snd (w ∈ fst v)) read (col-out a w w∈)
          where
          wS : S
          wS = w , isL-trans {x = col a} {y = w} w∈ (col-isL a)

对 col-out 给出的前驱 r，a 处表项的完备性在命题截断下给出 up r 处的某个表值 u。由于目标 w ∈ v 是命题，可以合法地消去这个截断。接下来只须利用 r 处的正确性把 u 与 col r 比较，进而与 w 比较。

          read : Σ[ r ∈ Dom ] ((r ≺ a) × (col r ≡ w)) → ⟨ w ∈ fst v ⟩
          read (r , (ra , e)) = PT.rec (snd (w ∈ fst v)) inner (cmp (up r) (≺-out r a ra))
            where
            inner : Σ[ u ∈ S ] Holds F (up r) u → ⟨ w ∈ fst v ⟩
            inner (u , fu) = val wS .snd

取值方程的反向一半把来源见证转换为对 v 的隶属。这里的来源见证由前驱 up r、它与 up a 的关系，以及取值为 u 的表项组成；归纳假设把 u 认同为 col r，再由等式 col r ≡ w 运输该表项，使其取值成为 w。

              ∣ up r , (≺-out r a ra , subst (λ t → ⟨ pr (↪ r) t ∈ fst F ⟩) (IH r ra u fu ∙ e) fu) ∣₁

现设 q 确为 D 的成员，且 v 在 q 处满足局部塌缩公式。该公式只在命题截断下给出一张含有 (q,v) 的正确表；但所求集合等式是命题，故可以消去此截断。把表项从 q 运输到其解码表示后，correct-val 便把 fst v 认同为 col (toDom q mq)。

    colFo-val : (q : S) (mq : Mem q) (v : S) → ⟨ (v ∷ q ∷ []) ⊨ CF.colFo ⟩
              → fst v ≡ col (toDom q mq)
    colFo-val q mq v h = PT.rec (setIsSet (fst v) (col (toDom q mq)))
      (λ { (F , (hc , hv)) → correct-val F hc (toDom q mq) v
             (subst (λ t → ⟨ pr t (fst v) ∈ fst F ⟩) (sym (toDom-val q mq)) hv) })

塌缩公式的向外读法供给正确表与表条目，即唯一性引理的两个输入。

      (CF.colFo-out v q h)

局部表模块以域的实参 a 与在每个更小实参处提供塌缩公式的归纳假设为参数。它将为 a 造一张表：其实真前驱处的条目记录塌缩值，其余条目记录默认对。

    module Approx (a : Dom)
                  (IH : (b : Dom) → b ≺ a → ⟨ (colʟ b ∷ up b ∷ []) ⊨ CF.colFo ⟩) where

默认条目 ea 是被载实参与其自身塌缩组成的有序对，呈现为载体元素。

      ea : S
      ea = prʟ (up a) (colʟ a)

局部公式的体有两个析取支。左支说 q 是 a 的真前驱，且 z 把 q 与满足塌缩公式的取值配对。右支说 q 不是前驱，且 z 是默认条目。该情形分裂由排中律判定。

      Body : S → S → Type (ℓ-suc ℓ)
      Body z q =
          (Holds R q (up a)
             × ∥ Σ[ v ∈ S ] ((fst z ≡ pr (fst q) (fst v)) × ⟨ (v ∷ q ∷ []) ⊨ CF.colFo ⟩) ∥₁)
        ⊎ ((Holds R q (up a) → Empty.⊥) × (fst z ≡ fst ea))

为了在对象语言中区分前驱情形与默认情形，关系检验必须提及由变化的实参 q 与固定点 a 组成的有序对。对表达式在局部公式使用的两个自由槽位中统一给出这个词项。

      module PE = PairExpression

表达式 image 表示有序对 (q,up a)：第一坐标取自实参槽，第二坐标是表示 a 的字面载体元素。因此，image 属于 R 恰好表示 q 是 a 的 R 前驱；它并不描述局部表的表项。

      image : PE.Expr 
      image = PE.pair (PE.slot (suc zero)) (PE.literal (up a))

公式 ψ 对应 Body 的两种情形。若 q R a，第一支要求输出 z 把 q 与某个在 q 处满足 colFo 的取值配成有序对。若 q 不是 a 的前驱，第二支要求 z 等于固定的默认表项 ea。在两支之间作选择的经典判定稍后才用于函数性证明，并不是析取本身的一部分。

      opaque
        ψ : Formula S 
        ψ = (PE.member image (con R) ∧̇ PF.pairFo)
          ∨̇ ((¬̇ PE.member image (con R)) ∧̇ (var zero ≐ con ea))

向外读取 ψ 时，其析取外的命题截断仍被保留。在前驱分支中，对表达式的读式把第一合取项转换为 q R a，而 PF.pair-out 在命题截断下说明：对某个在 q 处满足 colFo 的 v，z 等于 (q,v)。在默认分支中，则须把对象语言否定转换为宿主级对 q R a 的反驳。

        ψ-out : (z q : S) → ⟨ (z ∷ q ∷ []) ⊨ ψ ⟩ → ∥ Body z q ∥₁
        ψ-out z q = PT.map
          (λ { (inl (h1 , h2)) → inl (PE.member-out image (con R) (z ∷ q ∷ []) h1
                                         , PF.pair-out z q h2)
             ; (inr (h1 , h2)) → inr

为得到这份宿主级反驳，暂设 q R a。对表达式的向内读法把该假设转换为隶属原子式的满足，而对象语言否定排除了这种满足。把 z 认同为默认表项的等式已经具有所需的宿主级形式，故原样保留。

                 ((λ k → lower (h1 (PE.member-in image (con R) (z ∷ q ∷ []) k))) , h2) })

向内读法把左支经对表达式引入与对图引入注入，并把截断取值消去到命题值的满足之中。

        ψ-in : (z q : S) → Body z q → ⟨ (z ∷ q ∷ []) ⊨ ψ ⟩
        ψ-in z q (inl (h1 , hv)) = PT.rec (snd ((z ∷ q ∷ []) ⊨ ψ))
          (λ { (v , (e , hc)) → ∣ inl (PE.member-in image (con R) (z ∷ q ∷ []) h1
                                     , PF.pair-in z q v e hc) ∣₁ }) hv
        ψ-in z q (inr (h1 , e)) =

右支把宿主侧反驳提升进对象语言并携带默认等式。两支都被注入公式的截断析取。

          ∣ inr ((λ k → lift (h1 (PE.member-out image (con R) (z ∷ q ∷ []) k))) , e) ∣₁

辅助事实 b≺a-of 把宿主侧关系隶属解码为内部比较：若 q 与 a 有关系，则 q 的内部索引低于 a。解码方式是沿隶属下降以恢复索引。

      private
        b≺a-of : (q : S) (mq : Mem q) → Holds R q (up a) → toDom q mq ≺ a
        b≺a-of q mq h = ≺-in (toDom q mq) a
          (subst (λ t → ⟨ pr t (↪ a) ∈ fst R ⟩) (sym (toDom-val q mq)) h)

归纳假设陈述在典范表示 up (toDom q mq) 处，而局部公式必须在原载体元素 q 处得到满足。往返等式认同这两种呈现，colFo-at 随之把满足证明从典范表示运输到 q。

        IHq : (q : S) (mq : Mem q) → toDom q mq ≺ a
            → ⟨ (colʟ (toDom q mq) ∷ q ∷ []) ⊨ CF.colFo ⟩
        IHq q mq k = colFo-at (colʟ (toDom q mq)) (up-toDom q mq) (IH (toDom q mq) k)

替换要求：对每个 q ∈ D，满足 ψ 的取值构成可缩纤维。证明用排中律判定是否有 q R a。无论哪种情形，它都将在命题截断下给出一个满足公式的典范输出，并证明其他任何满足公式的输出都等于它；mereFunct 再把这种命题截断的唯一存在转换为可缩性。

        fc : (q : S) → ⟨ q ∈ˢ D ⟩ → isContr (Σ[ z ∈ S ] ⟨ (z ∷ q ∷ []) ⊨ ψ ⟩)
        fc q mq = mereFunct ψ q (decide (lem (pr (fst q) (↪ a) ∈ fst R)))
          where
          b : Dom
          b = toDom q mq

在前驱分支中，典范输出为 zb = prʟ q (colʟ b)，其底层集合编码 (q,col b)；这里的 b 是从 q 解码出的内部索引。非前驱分支则使用默认输出 ea。局部判定引理将在命题截断下说明：无论哪一分支成立，都有一个满足公式的输出，且其他任何满足公式的输出都与它相等。

          zb : S
          zb = prʟ q (colʟ b)
          decide : Holds R q (up a) ⊎ (Holds R q (up a) → Empty.⊥)
                 → ∥ Σ[ z ∈ S ] (⟨ (z ∷ q ∷ []) ⊨ ψ ⟩
                                × ((z' : S) → ⟨ (z' ∷ q ∷ []) ⊨ ψ ⟩ → z' ≡ z)) ∥₁

设 q R a。归纳假设说明 col b 在 q 处满足 colFo，而 prʟ-fst 给出 fst zb 与有序对编码 pr (fst q) (col b) 之间所需的等式，故典范输出 zb 满足左支。为证唯一性，把任意满足公式的输出仍按两种情形读取：左支见证将由 colFo-val 确定，右支见证则与既有假设 q R a 矛盾。

          decide (inl h) = ∣ zb
            , ( ψ-in zb q (inl (h , ∣ colʟ b , (prʟ-fst q (colʟ b) , IHq q mq (b≺a-of q mq h)) ∣₁))
              , λ z' hz' → PT.rec (isSetS z' zb)
                  (λ { (inl (_ , hv)) → PT.rec (isSetS z' zb)
                         (λ { (v , (e , hcol)) → Σ≡Prop (λ w → snd (isL w))

对左支中的竞争见证，colFo-val 把其第二坐标认同为 col b；再与该见证的有序对等式合成，便证明整个输出等于 zb。右支中的竞争见证含有对 q R a 的否定，故不可能存在。至此，前驱情形的唯一性得证。末行另行开始非前驱情形并选择默认输出 ea；其唯一性证明将在下一代码块继续。

                                (e ∙ cong (pr (fst q)) (colFo-val q mq v hcol) ∙ sym (prʟ-fst q (colʟ b))) })
                         hv
                     ; (inr (nh , _)) → Empty.rec (nh h) })
                  (ψ-out z' q hz') ) ∣₁
          decide (inr nh) = ∣ ea

否定隶属的情形闭合了唯一性论证。默认条目 ea 满足 ψ。向外读取任意竞争见证时，要么得到一条与 nh 矛盾的肯定隶属，要么由默认支得到 fst z' ≡ fst ea。在后一种情形中，可构造性证明的命题性把这条底层集合的等式提升为 S 中所需的等式 z' ≡ ea。

            , ( ψ-in ea q (inr (nh , refl))
              , λ z' hz' → PT.rec (isSetS z' ea)
                  (λ { (inl (h , _)) → Empty.rec (nh h)
                     ; (inr (_ , e)) → Σ≡Prop (λ w → snd (isL w)) e })
                  (ψ-out z' q hz') ) ∣₁

这项局部递归的定义域是整个 D。若 q R up a，它的唯一取值是 q 与 q 所呈现索引的塌缩值组成的有序对；否则取同一个默认条目 ea。把替换应用于 ψ 及这份唯一性证明，便将所得取值收集为一个可构造集。

        module T = Of (record { dom = D ; graph = ψ ; funct = fc }) using ( table; table-in; table-out )

Fa 表示这个由替换得到的值域。下述成员关系引理将证明，它的元素恰为满足 b ≺ a 的有序对 pr(↪ b,col b)，再加上默认分支给出的顶端有序对 pr(↪ a,col a)。

      Fa : S
      Fa = T.table

Below b 陈述索引 b 至多等于当前索引：要么严格低于，要么相等。这个两分谓词驱动局部表的引入与正确性。

      Below : Dom → Type ℓ
      Below b = (b ≺ a) ⊎ (b ≡ a)

若 b 小于或等于 a，Fa-in 就把输入为 up b、取值为 colʟ b 的图条目放入 Fa。严格比较的情形用归纳假设满足 ψ 的第一个析取支；等式 b ≡ a 的情形则先把这个有序对等同于 ea，再使用默认分支。

      Fa-in : (b : Dom) → Below b → Holds Fa (up b) (colʟ b)
      Fa-in b k = subst (λ w → ⟨ w ∈ fst Fa ⟩) (prʟ-fst (up b) (colʟ b))
        (T.table-in (up b) (prʟ (up b) (colʟ b)) (up-mem b) (ψ-in _ (up b) (bodyOf k)))
        where
        bodyOf : Below b → Body (prʟ (up b) (colʟ b)) (up b)

在严格情形中，公式体包含关系见证 b ≺ a，以及归纳假设所给出的 colʟ b 在 up b 处满足塌缩公式。在相等情形中，非自反性排除 up b R up a，而沿 b ≡ a 的传输把待证有序对等同于默认有序对。

        bodyOf (inl k) = inl (≺-out b a k , ∣ colʟ b , (prʟ-fst (up b) (colʟ b) , IH b k) ∣₁)
        bodyOf (inr e) = inr
          ( (λ h → ≺-irrefl a (≺-in a a (subst (λ t → Holds R (up t) (up a)) e h)))
          , prʟ-fst (up b) (colʟ b) ∙ cong (λ t → pr (↪ t) (col t)) e ∙ sym (prʟ-fst (up a) (colʟ a)) )

反过来，属于 Fa 仅仅给出一个满足 b ≺ a 或 b ≡ a 的索引 b，以及把该成员等同于 pr(↪ b,col b) 的等式。索引仍处于命题截断之下，因此这个结论没有选定一个代表元。

      Fa-out : (y : S) → ⟨ y ∈ˢ Fa ⟩
             → ∥ Σ[ b ∈ Dom ] (Below b × (fst y ≡ pr (↪ b) (col b))) ∥₁
      Fa-out y hy = PT.rec squash₁
        (λ { (q , (mq , hψ)) → PT.rec squash₁
          (λ { (inl (h , hv)) → PT.map

在前驱分支中，colFo-val 把公式给出的取值等同于 toDom q mq 处的塌缩值，随后 q 的呈现等式把有序对改写为典范形式。在默认分支中，记录的有序对就是以 a 自身为索引的那一个。

                 (λ { (v , (e , hcol)) → toDom q mq
                    , (inl (b≺a-of q mq h)
                      , e ∙ cong₂ pr (sym (toDom-val q mq)) (colFo-val q mq v hcol)) })
                 hv
             ; (inr (_ , e)) → ∣ a , (inr refl , e ∙ prʟ-fst (up a) (colʟ a)) ∣₁ })

替换的读取引理与 ψ-out 都只返回经命题截断的见证。由于目标本身也经过命题截断，证明可以依次消去外层与内层截断，而无需在全局选定任何一个见证。

          (ψ-out y q hψ) })
        (T.table-out y hy)

把上一结论用于 x 与 v 的有序对编码，便可恢复它的两个坐标。因此，图条目 Holds Fa x v 仅仅确定某个 b ≤ a，使 fst x ≡ ↪ b 且 fst v ≡ col b。

      Fa-pair : (x v : S) → Holds Fa x v
              → ∥ Σ[ b ∈ Dom ] (Below b × (↪ b ≡ fst x) × (col b ≡ fst v)) ∥₁
      Fa-pair x v h = PT.map step
        (Fa-out (prʟ x v) (subst (λ w → ⟨ w ∈ fst Fa ⟩) (sym (prʟ-fst x v)) h))
        where

传输把等式重新指向内部对；辅助引理经有序对的单射性把它拆成索引的命名等式与塌缩值的命名等式。

        step : Σ[ b ∈ Dom ] (Below b × (fst (prʟ x v) ≡ pr (↪ b) (col b)))
             → Σ[ b ∈ Dom ] (Below b × (↪ b ≡ fst x) × (col b ≡ fst v))
        step (b , (k , e)) = b , (k , sym (fst q) , sym (snd q))
          where
          q : (fst x ≡ ↪ b) × (fst v ≡ col b)

把 pr-inj 应用于复合后的有序对等式，便得到 fst x ≡ ↪ b 与 fst v ≡ col b。Fa-pair 所需的结果把典范坐标置于等式左边，因此 step 返回前先反转这两条分量等式。

          q = pr-inj (sym (prʟ-fst x v) ∙ e)

若 c ≺ b 且 b ≺ a，传递性给出 c ≺ a。若改为 b ≡ a，把这个等式代入 c ≺ b 也得到同一结论。这正是 Below b 的两种情形。

      below-trans : {c b : Dom} → c ≺ b → Below b → c ≺ a
      below-trans cb (inl k) = ≺-trans cb k
      below-trans {c} cb (inr e) = subst (c ≺_) e cb

为证明 Correct Fa R，先固定 Fa 中一个实际条目 (x,v)。配对读取引理只给出一个经命题截断的索引来表示该条目，但 Complete Fa R x 与 ValueIs Fa R x v 都是命题。因此，可以合法地向它们的合取消去这层截断。

      Fa-correct : Correct Fa R
      Fa-correct x v hxv = PT.rec
        (isProp× (isPropΠ (λ _ → isPropΠ (λ _ → squash₁)))
                 (isPropΠ (λ w → isProp× (isPropΠ (λ _ → squash₁))
                                          (isPropΠ (λ _ → snd (fst w ∈ fst v))))))

设所选条目由某个 b ≤ a 表示，于是 x 呈现 b，而 v 的底层集合是 col b。完备性要求 x 的每个 R 前驱都在 Fa 中有取值；取值条件则要求对每个 w 证明：w ∈ v 当且仅当某个这样的前驱在 Fa 中与 w 配对。

        build (Fa-pair x v hxv)
        where
        build : Σ[ b ∈ Dom ] (Below b × (↪ b ≡ fst x) × (col b ≡ fst v))
              → Complete Fa R x × ValueIs Fa R x v
        build (b , (k , ex , ev)) = cmp , (λ w → fwd w , bwd w)

这里的关键转换，是把编码关系中的前驱 y R x 化为 Dom 中的严格比较。条目的表示把 fst x 与被表示成员 ↪ b 等同，并不把载体元素 x 与外围索引 b 等同。Rsub 先证明 y 属于 D，随后 toDom 才恢复出可与 b 比较的索引。

          where

由 y R x，端点包含假设先给出 y ∈ D，故 toDom y my 定义了一个索引 c。沿 y 与 x 的呈现等式传输关系见证，即得 c ≺ b；第二个分量则记录 ↪ c 是 y 的底层集合。

          pred : (y : S) → Holds R y x → Σ[ c ∈ Dom ] ((c ≺ b) × (↪ c ≡ fst y))
          pred y hy = c , (≺-in c b (subst2 (λ s t → ⟨ pr s t ∈ fst R ⟩)
                              (sym (toDom-val y my)) (sym ex) hy) , toDom-val y my)
            where
            my : Mem y

证明 my 正是 Rsub 给出的第一个端点成员关系，也是构造 toDom y my 所需的证据。由于属于 D 是一个命题，使用这份证据不会额外选择一种呈现。

            my = Rsub y x hy .fst
            c : Dom
            c = toDom y my

对前驱 y R x，令 c 为刚恢复的索引。完备性的取值见证是 colʟ c；Fa-in 先给出输入为 up c 的典范条目，再沿 ↪ c ≡ fst y 传输为输入在 y 处的所需条目。经由 b ≤ a 的传递性保证 c 严格低于 a。

          cmp : Complete Fa R x
          cmp y hy = ∣ colʟ c , subst (λ t → ⟨ pr t (col c) ∈ fst Fa ⟩) ec
                                 (Fa-in c (inl (below-trans cb k))) ∣₁
            where
            c = pred y hy .fst

现在把 pred y hy 的两个投影记作 cb 与 ec：cb 是严格比较 c ≺ b，ec 则把典范代表 ↪ c 等同于实际输入 y。前者提供 Fa-in 所需的界，后者负责把条目传输到 y。

            cb = pred y hy .snd .fst
            ec = pred y hy .snd .snd

为证明 ValueIs 的正向一半，先把 w ∈ v 改写为 fst w ∈ col b。塌缩的向外引理仅仅给出 r ≺ b 与 col r ≡ fst w；这些数据构造出从 up r 到 x 的一条 R 边，以及在表中把 up r 与 w 配对的条目。

          fwd : (w : S) → ⟨ fst w ∈ fst v ⟩ → Src Fa R x w
          fwd w w∈ = PT.map read (col-out b (fst w) (subst (λ t → ⟨ fst w ∈ t ⟩) (sym ev) w∈))
            where
            read : Σ[ r ∈ Dom ] ((r ≺ b) × (col r ≡ fst w)) → Σ[ y ∈ S ] (Holds R y x × Holds Fa y w)
            read (r , (rb , er)) = up r

两条隶属沿索引的等式与严格比较传输，把关系与表的隶属都落在被点名的前驱处。

              , ( subst (λ t → ⟨ pr (↪ r) t ∈ fst R ⟩) ex (≺-out r b rb)
                , subst (λ t → ⟨ pr (↪ r) t ∈ fst Fa ⟩) er (Fa-in r (inl (below-trans rb k))) )

在反向一半中，Src Fa R x w 的见证仅仅给出某个 y，满足 y R x，并且表中有从 y 到 w 的条目。目标 fst w ∈ fst v 是命题，因此可以向它依次消去来源见证与表读取结果中的命题截断。

          bwd : (w : S) → Src Fa R x w → ⟨ fst w ∈ fst v ⟩
          bwd w = PT.rec (snd (fst w ∈ fst v)) (λ { (y , (hy , fy)) →
            PT.rec (snd (fst w ∈ fst v)) (read y hy) (Fa-pair y w fy) })
            where
            read : (y : S) → Holds R y x

读取表条目得到一个索引 c、把 y 等同于 ↪ c 的等式，以及把 w 等同于 col c 的等式。把第一个等式、y R x 与 x 由 b 表示这一事实合并，便得到 c ≺ b；于是 col-in 给出 col c ∈ col b，其余等式再把这条成员关系传输为 w ∈ v。

                 → Σ[ c ∈ Dom ] (Below c × (↪ c ≡ fst y) × (col c ≡ fst w))
                 → ⟨ fst w ∈ fst v ⟩
            read y hy (c , (_ , ey , ew)) =
              subst2 (λ s t → ⟨ s ∈ t ⟩) ew ev (col-in b c cb)
              where

c 与 b 之间的严格比较由两条命名等式与关系见证填充，前驱数据随之完备。

              cb : c ≺ b
              cb = ≺-in c b (subst2 (λ s t → ⟨ pr s t ∈ fst R ⟩) (sym ey) (sym ex) hy)

局部表在顶端元素处满足图公式，默认条目见证取值子句。这是本节的归纳步。

      approx-step : ⟨ (colʟ a ∷ up a ∷ []) ⊨ CF.colFo ⟩
      approx-step = CF.colFo-in (colʟ a) (up a) Fa Fa-correct (Fa-in a (inr refl))

现在用良基归纳证明塌缩公式在每个 a : Dom 处成立。归纳假设为每个严格前驱给出该公式的满足见证，Approx.approx-step 再用这些见证在 a 处构造一张正确的局部表。结论遍及 Dom 中的每个索引，并不要求事先把 D 等同于某个序数。

    approx : (a : Dom) → ⟨ (colʟ a ∷ up a ∷ []) ⊨ CF.colFo ⟩
    approx = W.induction {P = λ a → ⟨ (colʟ a ∷ up a ∷ []) ⊨ CF.colFo ⟩}
      (λ a IH → Approx.approx-step a IH)

给定 q : S 与 mq : Mem q，前面的归纳先在典范表示 up (toDom q mq) 处给出公式。往返等式 up-toDom q mq 把该表示与 q 等同，colFo-at 再把满足证明运输到 D 的这个原成员处。

    approx-at : (q : S) (mq : Mem q) → ⟨ (colʟ (toDom q mq) ∷ q ∷ []) ⊨ CF.colFo ⟩
    approx-at q mq = colFo-at (colʟ (toDom q mq)) (up-toDom q mq) (approx (toDom q mq))

递归 otR 以 D 为定义域，以 CF.colFo 为取值关系。对成员 q ∈ D，选定的取值是小索引 toDom q mq 处的塌缩值；前面的逼近结果证明这个取值在 q 处满足公式。

    private
      otR : Recursion
      otR = record
        { dom   = D
        ; graph = CF.colFo

字段 funct 必须证明：对每个 q ∈ D，满足 CF.colFo 的取值所成纤维是可缩的。其中心由 colʟ (toDom q mq) 与 approx-at q mq 组成。对任意竞争元素 (v,hv)，colFo-val 把 v 的底层集合与同一个塌缩值等同；可构造性证明与满足证明的命题性再依次把这条等式提升到 v，最后提升到整个纤维元素。

        ; funct = λ q mq → (colʟ (toDom q mq) , approx-at q mq)
            , λ { (v , hv) → Σ≡Prop (λ w → snd ((w ∷ q ∷ []) ⊨ CF.colFo))
                (sym (Σ≡Prop (λ w → snd (isL w)) (colFo-val q mq v hv))) } }

通用的替换构造 Of 现在把这项函数性递归变成它的取值表，并给出成员关系刻画的两个方向：满足递归关系的取值进入该表，而表的每个成员都来自 D 中某个输入，并带有所需的公式见证。

      module OT = Of otR using ( table; table-in; table-out )

otL 是 otR 经替换得到的值域，因此是 L 的一个元素。它的底层集合收集所有 b : Dom 的塌缩值 col b，无需这些取值来自互不相同的索引。这里的构造只使用这一精确值域刻画；整个值域的序数性是还需进一步推出的结论。

    otL : S
    otL = OT.table

对每个 b : Dom，逼近引理证明 colʟ b 是 otR 在 up b 处的取值。因此，替换的引入方向给出 col b ∈ fst otL。

    otL-in : (b : Dom) → ⟨ col b ∈ fst otL ⟩
    otL-in b = OT.table-in (up b) (colʟ b) (up-mem b) (approx b)

反过来，每个 y ∈ fst otL 仅仅具有某个索引 b : Dom，满足 col b ≡ y。结论特意保留命题截断，因此它刻画了精确值域，却没有为每个成员选定一个原像。

    otL-out : (y : V ℓ) → ⟨ y ∈ fst otL ⟩ → ∥ Σ[ b ∈ Dom ] (col b ≡ y) ∥₁
    otL-out y hy = PT.map (λ { (q , (mq , h)) → toDom q mq , sym (colFo-val q mq yS h) })
      (OT.table-out yS hy)
      where
      yS : S

为了应用替换的读取引理，需要把外围集合 y 看作可构造论域中的元素。由 y ∈ fst otL 以及 otL 的可构造性，可构造性的向下封闭正好给出这一打包。

      yS = y , isL-trans {x = fst otL} {y = y} hy (snd otL)

把递归图构造应用于 otR，所收集的是有序对而非裸取值。它为 D 中每个输入记录该输入及其唯一确定的塌缩值，并给出相应的内向与外向读取、单值性以及精确定义域陈述。

    module CT = RecursionGraph otR using ( F; F-in; F-out; pair-out; sv; dm )

colTable 是在 L 内由 otR 构造出的函数图集合。对 b : Dom，其典范条目是 pr(↪ b,col b)：表中存储的输入是 D 的被表示成员 ↪ b，而 b 本身仍是外围小表示中的索引。

    colTable : S
    colTable = CT.F

在典范代表 up b 处，递归图最初记录的取值是 col (toDom (up b) (up-mem b))。呈现等式诱导出这个恢复索引与 b 的相等；沿该等式在 col 下的像传输第二坐标，便得到所陈述的有序对 pr(↪ b,col b)。

    colTable-in : (b : Dom) → ⟨ pr (↪ b) (col b) ∈ fst colTable ⟩
    colTable-in b = subst (λ t → ⟨ pr (↪ b) t ∈ fst colTable ⟩)
      (cong col (Dom≡ (toDom-val (up b) (up-mem b)))) (CT.F-in (up b) (up-mem b))

反过来，colTable-out 说明：对函数图的任意成员 y，仅仅存在某个 b : Dom，使 fst y ≡ pr(↪ b,col b)。该索引仍处于命题截断之下，因此这项向外读法只刻画函数图，并未为每个成员选定一个表示索引。

    colTable-out : (y : S) → ⟨ y ∈ˢ colTable ⟩
                 → ∥ Σ[ b ∈ Dom ] (fst y ≡ pr (↪ b) (col b)) ∥₁
    colTable-out y hy = PT.map (λ { (q , mq , e) → toDom q mq
      , e ∙ cong (λ t → pr t (col (toDom q mq))) (sym (toDom-val q mq)) }) (CT.F-out (fst y) hy)

纤维谓词说：与 x 配对的成员 v 是 x 所呈现索引的塌缩值，并以呈现隶属为数据。

    Fib : S → S → Type (ℓ-suc ℓ)
    Fib x v = Σ[ mx ∈ Mem x ] (fst v ≡ col (toDom x mx))

固定 x 与 v 后，Fib x v 是命题。成员关系 mx : Mem x 取值于命题；对每个这样的 mx，由于 V 是集合，等式 fst v ≡ col (toDom x mx) 也是命题。因此，这个依值和不携带额外的选择数据。

    isPropFib : (x v : S) → isProp (Fib x v)
    isPropFib x v = isPropΣ (isPropMem x) (λ mx → setIsSet (fst v) (col (toDom x mx)))

因此，x 与 v 的编码有序对属于 colTable 时，可以得到不带截断的信息：x 属于 D，且 v 的底层集合等于 x 所呈现索引处的塌缩值。正是 Fib x v 的命题性允许消去图读取结果中的截断。

    colTable-pair : (x v : S) → Holds colTable x v → Fib x v
    colTable-pair = CT.pair-out

作为编码单射的图

为研究塌缩图何时编码一条单射，固定 D、R 以及端点条件 Rsub。这个条件只说明每条被 R 记录的边，其两个端点都属于 D；良基性、传递性与三歧性仍是彼此独立的假设。

module Code (D R : S)
            (Rsub : (y x : S) → Holds R y x
                  → ⟨ fst y ∈ fst D ⟩ × ⟨ fst x ∈ fst D ⟩) where

这里沿用上文的小表示 Dom、其编码关系 _≺_，以及 D 的成员与索引之间的转换。接下来的编码论证建立在同一塌缩构造上，并不引入第二条关系。

  open Internal D R Rsub public

这些假设各有不同作用。良基性通过递归定义 col，传递性证明每个塌缩值是序数，因而可构造；局部表的装配还使用本章的经典参数 lem。这些材料共同构造出精确值域 otL 与函数图 colTable，并给出单值性、精确定义域，以及所有函数图取值都属于 otL。三歧性只在下一个模块中加入，用于证明单射性。

  module Conjuncts (wf : WellFounded _≺_)
                   (≺-trans : {a b c : Dom} → a ≺ b → b ≺ c → a ≺ c) where

固定这两个假设后，前面的图构造给出 col、otL 与 colTable，以及它们的成员关系刻画。在这一阶段，相同输入具有相同的记录取值，但尚未证明记录取值相等能够推出输入相等。

    open Graph wf ≺-trans public

在二槽位环境 γ 中，零号槽放置 colTable，一号槽放置 D。单值性与精确定义域公式因而可以通过这两个固定位置引用函数图及其预定定义域。

    γ : S ^ 
    γ = colTable ∷ D ∷ []

第一项条件是单值性：若 colTable 含有输入相同、取值分别为 y 与 y' 的两个有序对，则 fst y ≡ fst y'。这来自递归取值的唯一性，本身并不断言每个输入都有取值。

    sv : ⟨ γ ⊨ svAt zero ⟩
    sv = CT.sv

定义域条件是一条等价：一个输入在 colTable 中具有某个取值，当且仅当它属于 D。因此，它既排除定义域外的条目，也断言 D 的每个成员都有取值；后一个方向中的存在取值仍保留命题截断。

    dm : ⟨ γ ⊨ domAt zero (suc zero) ⟩
    dm = CT.dm

值域条件来自函数图的配对读取：从 x 到 y 的条目给出 x 属于定义域的见证，并把 fst y 等同于相应的塌缩值，而 otL-in 证明该塌缩值属于 otL。这里仅证明函数图的取值都落在 otL 中；colTable 的单射性仍需下一步引入的三歧性假设。

    ran : (x y : S) → Holds colTable x y → ⟨ fst y ∈ fst otL ⟩
    ran x y h = subst (λ t → ⟨ t ∈ fst otL ⟩) (sym (snd (colTable-pair x y h)))
      (otL-in (toDom x (fst (colTable-pair x y h))))

塌缩表已经在 D 上全域且单值，其取值也已落在精确值域 otL 中。要得到编码单射，只余下输入唯一性这一项条件。现在假设小定义域上的三歧性：对任意 a 与 b，或者 a ≺ b，或者 a ≡ b，或者 b ≺ a。结合外层模块已经固定的良基性与传递性，这项比较将使相等的塌缩值迫使索引相等。

    module Inj (tri : (a b : Dom) → (a ≺ b) ⊎ ((a ≡ b) ⊎ (b ≺ a))) where

为证明 col 单射，固定满足 col a ≡ col b 的 a 与 b，并按二者的三歧性分类。相等情形已经给出所需结论。两个严格情形则各自把两个塌缩值之间真实成立的隶属关系沿该等式搬运成自隶属，故只需反驳这一不可能的隶属关系。

      col-inj : (a b : Dom) → col a ≡ col b → a ≡ b
      col-inj a b e = go (tri a b)
        where
        go : (a ≺ b) ⊎ ((a ≡ b) ⊎ (b ≺ a)) → a ≡ b
        go (inl k)       = Empty.rec (∈-irrefl (col b)

左支中 a 先于 b，故 col a 属于 col b；沿取值等式运输使 col b 属于自身，被非自反性反驳。中支直接返回等式。右支对称：col a 将属于自身。

          (subst (λ t → ⟨ t ∈ col b ⟩) e (col-in b a k)))
        go (inr (inl q)) = q
        go (inr (inr k)) = Empty.rec (∈-irrefl (col a)
          (subst (λ t → ⟨ t ∈ col a ⟩) (sym e) (col-in a b k)))

对象语言子句 injAt 要求：具有同一输出的两条图表项必须具有同一输入。用 colTable-pair 读取 p 与 q，便得到两个输入属于 D 的证明 m 与 m'，以及把共同输出 y 分别认同为两个恢复所得塌缩值的等式。复合这两条等式，就得到应用 col-inj 所需的前提。

      ij : ⟨ γ ⊨ injAt zero ⟩
      ij = injAt-in zero γ (λ y x x' p q →
        let (m , e)   = colTable-pair x y p
            (m' , e') = colTable-pair x' y q
        in sym (toDom-val x m)

恢复的索引由 col-inj 相等，而往返引理把该等式搬回原载体元素的底层集合。三条等式复合成所需等式。

         ∙ cong ↪ (col-inj (toDom x m) (toDom x' m') (sym e ∙ e'))
         ∙ toDom-val x' m')

这四个字段来自不同的论证。递归图给出单值性与精确定义域子句；colTable-pair 和 otL-in 给出值域界；三歧性则补上缺少的单射性子句。把这些证明封装起来便得到 InjCode colTable D otL。因此，只有在携带 tri 的模块内部，colTable 才是编码单射；这份记录没有另行断言本章已经把 otL 封装为序数。

      code : InjCode colTable D otL
      code = sv , dm , ij , ran

反向构造只针对选定的源集 X 与目标集 Y。对每个 x ∈ X，pre 必须选出索引 b : Dom 并满足 col b ≡ fst x；它是塌缩原像，不一定是这条关系中某个固定点的前驱。第二项参数 bound 证明所表示的原输入 ↪ b 属于 Y。每次使用逆向接口时都必须另行提供这些数据，它们不能仅由 otL-out 自动得到。

      module Inverse (X Y : S)
        (pre : (x : S) → ⟨ fst x ∈ fst X ⟩ → Σ[ b ∈ Dom ] (col b ≡ fst x))
        (bound : (x : S) (mx : ⟨ fst x ∈ fst X ⟩) → ⟨ ↪ (pre x mx .fst) ∈ fst Y ⟩) where