---
title: "L 中无穷基数的平方律"
module: L.GCH.CardinalSquareLaw
lang: zh
site: "Bedrock"
description: "L 中无穷基数的平方律"
stage: "证明 GCH"
reading_order: 111
canonical: https://bedrock.institute/zh/L.GCH.CardinalSquareLaw.html
html: L.GCH.CardinalSquareLaw.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/CardinalSquareLaw.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, L.Choice.FirstIntersectionStage, V.Model, V.Presentation, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Ordinal.Linear, L.Ordinal.SquareLaw, L.WellOrder.Base, L.Axioms.Basic, L.Axioms.Infinity, L.Axioms.Numerals, L.Coding.Model, L.Coding.Expressions, L.Coding.Injection, L.Cardinal, L.InjectionComposition, L.GCH.CardinalRepresentative, L.DefinableInjection, L.GCH.OrderType]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.CardinalSquareLaw.md, https://bedrock.institute/ja/L.GCH.CardinalSquareLaw.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# L 中无穷基数的平方律

对 `L` 中的无穷基数 `κ`，其成员的有序对所成之集可经 `L` 内部的编码单射注入 `κ` 自身。本章构造这个单射。路线经由对上的 Gödel 序：把这条序写成第一阶对象语言的公式，在序数 `κ` 处读作外部的 Gödel 序，再塌缩到序型，由计数引理与 `κ` 比较。本章在固定的宇宙层级 `ℓ` 上工作，使用高一层的排中律，即下文所有序数比较所依赖的唯一经典假设。

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

这一构造并非处处构造性的，其原因在数学而不在形式化。要为序数的有序对排序，就必须对两个序数 `a` 与 `b` 判定 `a` 是否属于 `b`；本章的每个经典判定都是这同一个问题的实例。模块因此以显式数据接收层级 `ℓ-suc ℓ` 上的排中律，那正是被判定隶属命题所在的层级。

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

模块参数一次性固定这个实例，本章的每个经典步骤消耗的恰是它。

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

将被内在化的序用一阶对象语言写出：由隶属与相等两种原子经联结词、否定和无界存在量词生成的公式，在外围层级上解释。层级自身还有两条事实伴随其侧，二者都用于收束论证：隶属是良基的，故序数允许沿 `∈` 作归纳；并且没有集合属于自身，故不可能的比较可被直接反驳。

```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; ∈-irrefl )
```

读取编码对的坐标并以其计数，依赖三个事实。序数的后继运算是单射的，故相等的后继有相同的前驱。序数的每个成员都由其小呈现的一个索引指名，该命名单射，且可构造集的成员自身可构造。有序对 `pr` 在两个坐标上都是单射的，故编码对确定其两个分量。

```agda
open import L.Choice.FirstIntersectionStage {ℓ} lem using ( ord-suc-inj )
open import V.Model {ℓ} using ( ∈sucV-elim; ∈sucV-inl; self∈sucV )
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ}
```

在可构造一侧，内层结构 `𝒮ʟ` 把层级限制到可构造集这个传递类。全章使用的序数事实都是封闭性事实：序数的成员是序数，序数的后继是序数，`ω` 的成员是序数，且任意两个序数经三歧性可比。与它们并列的，是本章所要内在化的、对上的外部 Gödel 序。

```agda
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset→isL )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; ω-ord; #∈ω; ω-mem-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
import L.Ordinal.SquareLaw {ℓ} lem as SQ
```

两个序数的比较被打包成三歧数据而非真值，因为下文的证明必须检查出现了哪种情形：严格小于、相等、或严格大于。空集与 `ω` 都可作为 `L` 的元素使用，内部的后继数码则带有对其底层集合的等同，使数码槽位能读作外围自然数。

```agda
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
  using ( lt; eq; gt ) renaming ( Tri to TriW )
open import L.Axioms.Basic {ℓ} using ( ∅ʟ )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Axioms.Numerals {ℓ} using ( sucʟ; sucʟ-fst )
```

在 `L` 内部，有序对与图条件由具有内外两种读法的一阶公式表达。配对充分性把编码对等同于其两个分量组成的外围有序对；图的读法则表达单值性、定义域、单射性及取值属于陪域。合在一起，这些条件刻画内部编码单射。

```agda
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-out; domAt )
open import L.Coding.Expressions {ℓ} using ( sucAtL; sucAtL-adequate )
open import L.Coding.Injection {ℓ} lem using ( injAt; module Extract; module Small )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL; IsCardinalL; _↪_ )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
```

构造由三个数学转换推动。首先，以包含于原序数且在内部与之等势的内部基数代表替代该序数；其次，可定义单射函数给出编码单射；最后，把良基且传递的关系塌缩为序数序型，并由三歧性证明塌缩映射单射。

```agda
open import L.GCH.CardinalRepresentative {ℓ} lem using ( cardOf )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
open import L.GCH.OrderType {ℓ} lem using ( Holds; module Code )
open import L.InjectionComposition {ℓ} lem
  using ( appC; appC-adequate; ω-limit; finite-excl-ω )
```

两个编码对的比较携带六个相互依赖的见证：四个坐标及其两个最大值。积保存同时成立的等式与次序条件，不交和保存不同的比较情形。由于证明分量都是命题，它们不会在所得序数据中引入额外选择。

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

编码对的坐标是 `κ` 底层集合的成员，须借助该集合的小呈现读取。与呈现并列的还有外围隶属、带空虚性证明的空集，以及 `ω` 与后继运算，坐标的比较与计数正是在这些概念中进行。

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

三种逻辑形式反复出现。良基性表述为每个元素的可及性数据，正是它使塌缩能沿序下降。反驳居住在空类型中。而只断言见证存在的条件在截断之下陈述，这已经足够，因为消费这些条件的目标本身就是命题或截断。

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

两个载体被命名并保持区分。外围载体承载层级自身的隶属；内层载体 `S` 由可构造集组成，每个元素是一个外围集合连同其可构造性证明，其隶属就是在外围集合上读取的外围隶属。

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

绝对性实例固定在可构造集这个传递类上：有界公式在 `L` 内外的含义相同，环境经投影读取，内层满足关系被改名为朴素的 `_⊨_`。

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

内层载体是 h-集合，这使其元素的相等易于处理。其元素是第二分量为命题的对，所以两个元素恰在其底层集合相等时相等；对路径引理则由各分量的等式构造两个对的等式。

```agda
isSetS : isSet S
isSetS = isSetΣSndProp setIsSet (λ v → snd (isL v))
opaque
  pair≡ : {A : Type ℓ} {B : Type ℓ} {a a' : A} {b b' : B}
        → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
```

对路径正是这一构造：由 `a ≡ a'` 与 `b ≡ b'` 逐点得到路径 `(a , b) ≡ (a' , b')`。序数是可构造的，理由直接：序数 `x` 属于它自己的后继，而那个层是 `L` 的集合，属于层即是可构造。该陈述是命题，故其证明在事实之外不携带任何信息。

```agda
  pair≡ e1 e2 = λ i → e1 i , e2 i
opaque
  isL-ord : (x : V ℓ) → IsOrd x → ⟨ isL x ⟩
  isL-ord x ox = Lset→isL (sucV x) (suc-ord ox) x (ord∈Lset-suc x ox)
```

因此，序数 `x` 可连同其可构造性证明视为可构造载体的元素 `ordL x ox`。再对「两个坐标都属于 `K`」这一关系施行可定义分离，便得到由这些有序对组成的可构造集合 `prodL K`。

```agda
ordL : (x : V ℓ) → IsOrd x → S
ordL x ox = x , isL-ord x ox
open import L.InjectionComposition {ℓ} lem public using ( module Relation )
private
  module Product (K : S) = Relation K K
```

乘积的描述条件说：两个坐标都是 `K` 的成员。其在宿主一侧的读法，是两个投影在 `K` 的底层集合中的外围隶属，且该读法的两个方向都已给出。

```agda
    ((var (suc zero) ∈̇ con K) ∧̇ (var zero ∈̇ con K))
    (λ x y → (fst x ∈ˢ fst K) ⊓ (fst y ∈ˢ fst K))
    (λ x y e h → h) (λ x y e h → h)
```

于是 `prodL K` 就是由 `K` 的两个成员组成的有序对之集，在 `L` 内部从约束它们的层中分离而来。

```agda
prodL : S → S
prodL = Product.rel
```

乘积中的隶属由一条截断的存在陈述刻画：存在 `K` 的两个成员 `a` 与 `b`，使该成员等于它们的有序对。截断如实记录条件所断言的内容，即见证存在，而在此处没有任何东西能区分一对见证与另一对；只有先证明见证唯一，才谈得上消去截断。

```agda
InProd : S → V ℓ → Type (ℓ-suc ℓ)
InProd K e = ∥ Σ[ a ∈ S ] Σ[ b ∈ S ]
               (⟨ fst a ∈ˢ fst K ⟩ × ⟨ fst b ∈ˢ fst K ⟩
                × (e ≡ pr (fst a) (fst b))) ∥₁
```

向内：`K` 的任意两个成员的有序对属于 `prodL K`；这正是那条被分离关系自身的引入规则。

```agda
prodL-in : (K a b : S) → ⟨ fst a ∈ˢ fst K ⟩ → ⟨ fst b ∈ˢ fst K ⟩
         → ⟨ pr (fst a) (fst b) ∈ˢ fst (prodL K) ⟩
prodL-in K a b ma mb = Product.into K a b ma mb (ma , mb)
```

向外：`prodL K` 的成员以截断的形式来自 `K` 的两个成员与那条对等式。对照 `K` 的小呈现，更强而不截断的陈述也可用：乘积的每个成员都是 `K` 的两个索引所指名元素组成的有序对。

```agda
prodL-out : (K e : S) → ⟨ fst e ∈ˢ fst (prodL K) ⟩ → InProd K (fst e)
prodL-out K e h = PT.map (λ { (a , b , q , ma , mb) → a , b , ma , mb , q }) (Product.out K e h)
prodL-fst : (K e : S) → ⟨ fst e ∈ˢ fst (prodL K) ⟩
          → Σ[ a ∈ ⟪ fst K ⟫ ] Σ[ b ∈ ⟪ fst K ⟫ ]
              (fst e ≡ pr (⟪ fst K ⟫↪ a) (⟪ fst K ⟫↪ b))
```

证明把截断的见证转换为 `K` 的索引的纤维，并沿纤维自身的等同，即「`K` 的每个成员恰是其索引所指名的集合」，修复那条对等式。

```agda
prodL-fst K e h = PT.rec isPropFib
  (λ { (a , b , ma , mb , q) →
     fiber (fst K) ma .fst , fiber (fst K) mb .fst
     , q ∙ cong₂ pr (sym (fiber (fst K) ma .snd)) (sym (fiber (fst K) mb .snd)) })
  (prodL-out K e h)
```

第二分量是唯一的：有序对的单射性提取出所指名集合的等式，而 `K` 的索引的单射性把它变成索引的等式。

```agda
  where
  inner : (a : ⟪ fst K ⟫)
        → isProp (Σ[ b ∈ ⟪ fst K ⟫ ] (fst e ≡ pr (⟪ fst K ⟫↪ a) (⟪ fst K ⟫↪ b)))
  inner a (b , q) (b' , q') = Σ≡Prop (λ _ → setIsSet _ _)
    (↪-inj {a = fst K} (pr-inj (sym q ∙ q') .snd))
```

第一分量基于同样的理由唯一，于是整条纤维陈述是一个命题：不截断的读法不依赖任何选取。

```agda
  isPropFib : isProp (Σ[ a ∈ ⟪ fst K ⟫ ] Σ[ b ∈ ⟪ fst K ⟫ ]
                        (fst e ≡ pr (⟪ fst K ⟫↪ a) (⟪ fst K ⟫↪ b)))
  isPropFib (a , b , q) (a' , b' , q') = Σ≡Prop inner
    (↪-inj {a = fst K} (pr-inj (sym q ∙ q') .fst))
```

## 作为公式的 Gödel 序

乘积到手之后，序登场：当 `a` 与 `b` 为序数时，`MaxIs` 说 `m` 是它们的最大值。

```agda
MaxIs : S → S → S → Type (ℓ-suc ℓ)
```

定义给出两个选项：要么 `a` 属于 `b` 且 `m` 是 `b`，要么「`a` 属于 `b`」被反驳且 `m` 是 `a`。被截断的只是这个析取，因为定义只断言两个选项之一成立而不判定是哪一个；在序数上，排中律将选出分支，被选出的 `m` 便是 `a` 与 `b` 的最大值。

```agda
MaxIs m a b =
  ∥ (⟨ fst a ∈ˢ fst b ⟩ × (fst m ≡ fst b))
  ⊎ ((⟨ fst a ∈ˢ fst b ⟩ → Empty.⊥) × (fst m ≡ fst a)) ∥₁
```

两个对的 Gödel 比较同样是截断之下的数据：要么第一对的最大值 `m` 属于第二对的最大值 `n`，要么两个最大值相等，此时按字典序比较，先比第一坐标，再比第二坐标。

```agda
OrdIs : S → S → S → S → S → S → Type (ℓ-suc ℓ)
OrdIs m n a b c d =
  ∥ ⟨ fst m ∈ˢ fst n ⟩
  ⊎ ((fst m ≡ fst n)
     × ∥ ⟨ fst a ∈ˢ fst c ⟩ ⊎ ((fst a ≡ fst c) × ⟨ fst b ∈ˢ fst d ⟩) ∥₁) ∥₁
```

最大值可写成一条有界公式：当 `a` 属于 `b` 时 `m` 等于 `b`，当 `a` 属于 `b` 被反驳时等于 `a`；否定词使第二个选项成为受守卫的分支。当 `a` 与 `b` 为序数时，这条公式说的恰是 `m` 是它们的最大值。

```agda
maxAt : ∀ {k} → Fin k → Fin k → Fin k → Formula S k
maxAt m a b = ((var a ∈̇ var b) ∧̇ (var m ≐ var b))
            ∨̇ ((¬̇ (var a ∈̇ var b)) ∧̇ (var m ≐ var a))
```

Gödel 比较也可同样写出，且其优先级是显式的：先比较两个最大值；最大值相等时比较第一坐标；第一坐标也相等时再比较第二坐标。

```agda
ordAt : ∀ {k} → Fin k → Fin k → Fin k → Fin k → Fin k → Fin k → Formula S k
ordAt m n a b c d =
    (var m ∈̇ var n)
  ∨̇ ((var m ≐ var n)
     ∧̇ ((var a ∈̇ var c) ∨̇ ((var a ≐ var c) ∧̇ (var b ∈̇ var d))))
```

把各部分合起来，`Lt p q` 说：`p` 与 `q` 是编码对，分别由成员 `a`、`b` 与成员 `c`、`d` 组成，其最大值 `m` 与 `n` 满足最大值条件，其比较满足 Gödel 条件。六个见证在截断之下记录：这些条件只断言见证存在，而经典情形分析是随后才在诸选项间作出选择。

```agda
Lt : V ℓ → V ℓ → Type (ℓ-suc ℓ)
Lt p q = ∥ Σ[ a ∈ S ] Σ[ b ∈ S ] Σ[ c ∈ S ] Σ[ d ∈ S ] Σ[ m ∈ S ] Σ[ n ∈ S ]
           ( (p ≡ pr (fst a) (fst b)) × (q ≡ pr (fst c) (fst d))
           × MaxIs m a b × MaxIs n c d × OrdIs m n a b c d ) ∥₁
```

六个约束子需要超出调用者环境的六个槽位，`↑6` 恰好把索引移动这么多位置。

```agda
private
  ↑6 : ∀ {k} → Fin k → Fin (suc (suc (suc (suc (suc (suc k))))))
  ↑6 i = suc (suc (suc (suc (suc (suc i)))))
```

六个槽位被命名为 `i0` 到 `i5`，每个量化见证一个。前三条别名绑定第零、第一、第二位置，它们将容纳第二对的最大值、第一对的最大值、以及第二对的第二坐标。

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

别名继续：第二位由第二对的第二坐标填充，第三位由其第一坐标填充，第四位由第一对的第二坐标填充。

```agda
  i2 = suc (suc zero)
  i3 : ∀ {k} → Fin (suc (suc (suc (suc k))))
  i3 = suc (suc (suc zero))
  i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))
  i4 = suc (suc (suc (suc zero)))
```

第五位是第一对的第一坐标，六个至此齐备。序公式随之开始：它将依次绑定六个见证，并就 `p` 与 `q` 说出 Gödel 比较所要求的内容。

```agda
  i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k))))))
  i5 = suc (suc (suc (suc (suc zero))))
opaque
  ltAt : ∀ {k} → Fin k → Fin k → Formula S k
  ltAt p q = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (
```

公式体依次绑定六个见证，并合取五个原子：`p` 是第五、第四槽位组成的有序对，`q` 是第三、第二槽位组成的有序对，第一个最大值原子约束 `p` 的两个坐标，第二个最大值原子约束 `q` 的两个坐标，序原子则先比较两个最大值、再比较坐标。在六槽位语境中读出，这恰好说：`p` 在 Gödel 序下低于 `q`。

```agda
        prAtL (↑6 p) i5 i4
     ∧̇ (prAtL (↑6 q) i3 i2
     ∧̇ (maxAt i1 i5 i4
     ∧̇ (maxAt i0 i3 i2
     ∧̇ ordAt i1 i0 i5 i4 i3 i2)))))))))
```

充分性对照一个具体的六条目语境检验。该语境把六个见证以最新在前的方式添加到调用者的环境：`n`、`m`、`d`、`c`、`b`、`a`，于是第零槽位是 `n`、第五槽位是 `a`，与那些别名一致。

```agda
  private
    env : ∀ {k} → S ^ k → S → S → S → S → S → S
        → S ^ (suc (suc (suc (suc (suc (suc k))))))
    env γ a b c d m n = n ∷ m ∷ d ∷ c ∷ b ∷ a ∷ γ
```

第一条充分性引理在该语境读取配对原子：配对原子的满足，就是调用者的 `p` 与 `a`、`b` 的有序对之间的等式。

```agda
    atP : ∀ {k} (p : Fin k) (γ : S ^ k) (a b c d m n : S)
        → ⟨ env γ a b c d m n ⊨ prAtL (↑6 p) i5 i4 ⟩
        ≡ (fst (lookup p γ) ≡ pr (fst a) (fst b))
    atP p γ a b c d m n = cong ⟨_⟩ (prAtL-adequate (↑6 p) i5 i4 (env γ a b c d m n))
```

第二条对 `q` 与 `c`、`d` 的有序对做同样的事。有了这两条等同，公式的满足与 `Lt` 的六见证数据便可互换。

```agda
    atQ : ∀ {k} (q : Fin k) (γ : S ^ k) (a b c d m n : S)
        → ⟨ env γ a b c d m n ⊨ prAtL (↑6 q) i3 i2 ⟩
        ≡ (fst (lookup q γ) ≡ pr (fst c) (fst d))
    atQ q γ a b c d m n = cong ⟨_⟩ (prAtL-adequate (↑6 q) i3 i2 (env γ a b c d m n))
```

向外方向依次消耗六层嵌套的截断：`ltAt p q` 在 `γ` 处的满足给出见证 `a` 至 `n`，连同两条对等式、两份最大值数据与一份序数据。

```agda
  lt-out : ∀ {k} (p q : Fin k) (γ : S ^ k) → ⟨ γ ⊨ ltAt p q ⟩
         → Lt (fst (lookup p γ)) (fst (lookup q γ))
  lt-out p q γ = PT.rec squash₁ (λ { (a , ha) → PT.rec squash₁ (λ { (b , hb) →
    PT.rec squash₁ (λ { (c , hc) → PT.rec squash₁ (λ { (d , hd) →
    PT.rec squash₁ (λ { (m , hm) → PT.rec squash₁ (λ { (n , (hp , (hq , (hM , (hN , hO))))) →
```

两条对等式沿充分性路径传输；第一份最大值数据被搬运到外围层级。六个存在见证处于被提升的语义层，因此肯定的情形原样保留，反驳的情形则被从提升中降出。

```agda
      ∣ a , b , c , d , m , n
      , ( transport (atP p γ a b c d m n) hp
        , transport (atQ q γ a b c d m n) hq
        , PT.map (λ { (inl h) → inl h
                    ; (inr (n , e)) → inr ((λ k → lower (n k)) , e) }) hM
```

第二份最大值数据以同样方式映射，从而在调用者的 `p` 与 `q` 处补全 `Lt` 的见证。

```agda
        , PT.map (λ { (inl h) → inl h
                    ; (inr (n , e)) → inr ((λ k → lower (n k)) , e) }) hN
        , hO ) ∣₁ }) hm }) hd }) hc }) hb }) ha })
```

向内方向把 `Lt` 转为满足陈述，而后者是命题。

```agda
  lt-in : ∀ {k} (p q : Fin k) (γ : S ^ k)
        → Lt (fst (lookup p γ)) (fst (lookup q γ)) → ⟨ γ ⊨ ltAt p q ⟩
  lt-in p q γ = PT.rec (snd (γ ⊨ ltAt p q))
    (λ { (a , b , c , d , m , n , (ep , eq' , hM , hN , hO)) →
      ∣ a , ∣ b , ∣ c , ∣ d , ∣ m , ∣ n
```

六个见证作为嵌套的存在见证被重新填入，两条对等式则沿充分性路径反方向传输。

```agda
      , ( transport (sym (atP p γ a b c d m n)) ep
        , ( transport (sym (atQ q γ a b c d m n)) eq'
        , ( PT.map (λ { (inl h) → inl h
                      ; (inr (n , e)) → inr ((λ k → lift (n k)) , e) }) hM
          , ( PT.map (λ { (inl h) → inl h
```

两份最大值数据被映射回去，这次提升为对象层带守卫的原子，序数据随之封闭整条公式。Gödel 模块随后为集合 `P` 打包这条序：其描述条件要求两个坐标都是 `P` 的成员，并以序公式关联它们。

```agda
                        ; (inr (n , e)) → inr ((λ k → lift (n k)) , e) }) hN
            , hO )))) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ })
private
  module Godel (P : S) = Relation P P
    ((var (suc zero) ∈̇ con P) ∧̇ ((var zero ∈̇ con P) ∧̇ ltAt (suc zero) zero))
```

宿主读法在两侧加上对 `P` 的隶属，与序关系合取；两个方向在两个约束子所占的槽位处引用向外与向内引理：第一坐标在外层槽位，第二坐标在内层槽位。

```agda
    (λ p q → (fst p ∈ˢ fst P) ⊓ ((fst q ∈ˢ fst P) ⊓ (Lt (fst p) (fst q) , squash₁)))
    (λ p q e h → h .fst , h .snd .fst , lt-out (suc zero) zero (q ∷ p ∷ e ∷ []) (h .snd .snd))
    (λ p q e h → h .fst , h .snd .fst , lt-in (suc zero) zero (q ∷ p ∷ e ∷ []) (h .snd .snd))
```

`godel P` 就是那条被分离的关系：在 `L` 内部，由 `P` 的成员组成的、在 Gödel 序下相互低于的有序对之集。

```agda
godel : S → S
godel = Godel.rel
```

向内：对 `P` 的两个成员 `p`、`q`，若 `p` 低于 `q`，则它们的有序对属于 `godel P`。

```agda
godel-in : (P p q : S) → ⟨ fst p ∈ˢ fst P ⟩ → ⟨ fst q ∈ˢ fst P ⟩
         → Lt (fst p) (fst q) → ⟨ pr (fst p) (fst q) ∈ˢ fst (godel P) ⟩
godel-in P p q mp mq l = Godel.into P p q mp mq (mp , mq , l)
```

向外：`godel P` 的成员带有两个成员及其间的序数据。

```agda
godel-out : (P p q : S) → ⟨ pr (fst p) (fst q) ∈ˢ fst (godel P) ⟩
          → ⟨ fst p ∈ˢ fst P ⟩ × ⟨ fst q ∈ˢ fst P ⟩ × Lt (fst p) (fst q)
godel-out = Godel.pair-out
```

## 到宿主序的搬运

序模块随后固定一个序数 `κ`，即平方律所陈述的情形。

```agda
module Order (κ : S) (oκ : IsOrd (fst κ)) where
```

`K` 是序数 `κ` 的底层集合；平方律所展开的载体正是这个由 `κ` 以下序数组成的集合。

```agda
  K : V ℓ
  K = fst κ
```

`↑` 借助小呈现的嵌入，在外围点名 `K` 的成员：每个索引指称它所呈现的那个序数。

```agda
  ↑ : ⟪ K ⟫ → V ℓ
  ↑ = ⟪ K ⟫↪
```

索引 `m : ⟪ K ⟫` 指名外围集合 `↑ m`，并带有它属于 `κ` 的证明。可构造性向成员传递，因此 `upK m` 把这个被指名的序数打包为 `L` 的元素。

```agda
  upK : ⟪ K ⟫ → S
  upK m = ↑ m , isL-trans {x = K} {y = ↑ m} (member K m) (snd κ)
```

待比较的序的载体是 `Pair`，即 `κ` 的两个索引组成的类型：宿主一侧的有序对，每个坐标都指名一个低于 `κ` 的序数。

```agda
  Pair : Type ℓ
  Pair = ⟪ K ⟫ × ⟪ K ⟫
```

坐标自身之上立着坐标序 `≺₁`，引自外部的平方律构造：低于 `κ` 的序数按其所指名外围集合之间的隶属作严格比较。

```agda
  _≺₁_ : ⟪ K ⟫ → ⟪ K ⟫ → Type (ℓ-suc ℓ)
  _≺₁_ = SQ._≺₁_ K oκ
```

有序对之上立着 Gödel 序 `≺ₚ`：先比最大值，再比第一坐标，最后比第二坐标。这正是内部公式必须复现的那条外部序。

```agda
  _≺ₚ_ : Pair → Pair → Type (ℓ-suc ℓ)
  _≺ₚ_ = SQ._≺_ K oκ
```

最大值运算 `maxOrd` 对低于 `κ` 的两个序数返回其中较大者，同样引自外部构造，也同样只因条目是序数才读作最大值。

```agda
  maxOrd : ⟪ K ⟫ → ⟪ K ⟫ → ⟪ K ⟫
  maxOrd = SQ.maxOrd K oκ
```

两个小事实为两侧的比较做准备。其一，序数 `κ` 的每个成员自身也是序数，故被点名的序数携带序数性证书。其二，`max-out` 陈述：在底层集合指名 `a'` 与 `b'` 的元素处读取的内部最大值条件，迫使内部最大值恰为 `a'` 与 `b'` 的宿主最大值；证明按宿主序的三歧数据展开。

```agda
  ord↑ : (m : ⟪ K ⟫) → IsOrd (↑ m)
  ord↑ m = mem-ord {A = K} oκ (↑ m) (member K m)
  max-out : (a b m : S) (a' b' : ⟪ K ⟫) → fst a ≡ ↑ a' → fst b ≡ ↑ b'
          → MaxIs m a b → fst m ≡ ↑ (maxOrd a' b')
  max-out a b m a' b' ea eb = PT.rec (setIsSet _ _) (go (SQ.tri₁ K oκ a' b'))
```

情形函数固定了该论证的形状：宿主三歧分成低于、相等、高于；内部数据分成肯定分支 (`m` 即 `b`) 与反驳分支 (`m` 即 `a`)。把两种分裂逐项配上，就是全部内容。

```agda
    where
    go : (t : TriW (a' ≺₁ b') (a' ≡ b') (b' ≺₁ a'))
       → (⟨ fst a ∈ˢ fst b ⟩ × (fst m ≡ fst b))
         ⊎ ((⟨ fst a ∈ˢ fst b ⟩ → Empty.⊥) × (fst m ≡ fst a))
       → fst m ≡ ↑ (SQ.maxGo K oκ a' b' t)
```

低于情形中，肯定分支把 `m` 与 `b` 的等式同 `b` 的命名复合，给出宿主最大值。其反驳分支不可能：它所反驳的隶属恰是三歧的见证，只须经两次命名传输即得。

```agda
    go (lt h) (inl (_ , e))   = e ∙ eb
    go (lt h) (inr (na , _))  =
      Empty.rec (na (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) (sym ea) (sym eb) h))
    go (eq p) (inl (a∈b , _)) =
      Empty.rec (∈-irrefl (↑ b')
```

相等情形中，肯定分支会断言 `a` 属于 `b`，而宿主宣布二者相等，这与被点名序数 `b` 处隶属的非自反性矛盾；反驳分支随即把最大值命名为 `a`，并沿 `a` 的命名传输。

```agda
        (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) (ea ∙ cong ↑ p) eb a∈b))
    go (eq p) (inr (_ , e))   = e ∙ ea
    go (gt h) (inl (a∈b , _)) =
      Empty.rec (∈-irrefl (↑ a')
        (ord↑ a' .fst {x = ↑ b'} {y = ↑ a'}
```

高于情形中，宿主见证给出 `b ∈ a`；若内部仍取肯定分支，还会有 `a ∈ b`，传递性便在 `a` 处违背非自反性。

```agda
          (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) ea eb a∈b) h))
    go (gt h) (inr (_ , e))   = e ∙ ea
```

逆向的 `max-in` 把宿主最大值写进内部谓词：对每一对索引，由 `maxOrd` 指名的被提升元素在两个被提升坐标处满足 `MaxIs`。

```agda
  max-in : (a' b' : ⟪ K ⟫) → MaxIs (upK (maxOrd a' b')) (upK a') (upK b')
  max-in a' b' = go (SQ.tri₁ K oκ a' b')
    where
    go : (t : TriW (a' ≺₁ b') (a' ≡ b') (b' ≺₁ a'))
       → MaxIs (upK (SQ.maxGo K oκ a' b' t)) (upK a') (upK b')
```

其三种情形由宿主比较直接得出：低于给出肯定分支且等式定义性成立；相等以非自反性反驳隶属；高于则借该坐标自身的序数性反驳。同一块中还定义了 `code`，即宿主对的两个被点名序数的外围有序对。

```agda
    go (lt h) = ∣ inl (h , refl) ∣₁
    go (eq p) = ∣ inr ((λ h → ∈-irrefl (↑ b') (subst (λ w → ⟨ ↑ w ∈ˢ ↑ b' ⟩) p h)) , refl) ∣₁
    go (gt h) = ∣ inr ((λ h' → ∈-irrefl (↑ a') (ord↑ a' .fst {x = ↑ b'} {y = ↑ a'} h' h)) , refl) ∣₁
  code : Pair → V ℓ
  code p = pr (↑ (fst p)) (↑ (snd p))
```

搬运的核心是一条反驳引理。它假设一对形状即矛盾的数据：`Lt` 在 `p` 与 `q` 的编码对上成立，而宿主序却拒绝比较它们。这种假设下的 `Lt` 的六个见证被收拢为一条荒谬性陈述。

```agda
  private
    refute : (p q : Pair) → (p ≺ₚ q → Empty.⊥)
           → Σ[ a ∈ S ] Σ[ b ∈ S ] Σ[ c ∈ S ] Σ[ d ∈ S ] Σ[ m ∈ S ] Σ[ n ∈ S ]
               ( (code p ≡ pr (fst a) (fst b)) × (code q ≡ pr (fst c) (fst d))
               × MaxIs m a b × MaxIs n c d × OrdIs m n a b c d )
```

结论是空类型：被假设的序数据与被拒绝的比较不能并存。证明拆开六个见证，在其所指名的底层集合上工作。

```agda
           → Empty.⊥
    refute (a' , b') (c' , d') nk (a , b , c , d , m , n , (ep , eq' , hM , hN , hO)) =
      PT.rec Empty.isProp⊥ outer hO
      where
      ea : fst a ≡ ↑ a'
```

有序对的单射性从每条编码等式中提取出：每个见证的底层集合与相应被点名序数的等同。这四条等式为后文所有比较提供了锚点。

```agda
      ea = sym (pr-inj ep .fst)
      eb : fst b ≡ ↑ b'
      eb = sym (pr-inj ep .snd)
      ec : fst c ≡ ↑ c'
      ec = sym (pr-inj eq' .fst)
```

两个最大值再经 `max-out` 施于两份最大值数据，而与宿主最大值等同。至此整个构形的内部读法与外部读法在全部六个坐标上一致。

```agda
      ed : fst d ≡ ↑ d'
      ed = sym (pr-inj eq' .snd)
      em : fst m ≡ ↑ (maxOrd a' b')
      em = max-out a b m a' b' ea eb hM
      en : fst n ≡ ↑ (maxOrd c' d')
```

等式 `en` 为第二个对给出同样的等同，于是现在可把 `OrdIs` 完整传输到宿主最大值与坐标上。

```agda
      en = max-out c d n c' d' ec ed hN
```

内层引理传递坐标比较：被点名第一坐标之间的外围隶属，沿两次命名的等同传输后，变成宿主序中的低于关系。

```agda
      inner : ⟨ fst a ∈ˢ fst c ⟩ ⊎ ((fst a ≡ fst c) × ⟨ fst b ∈ˢ fst d ⟩)
            → (a' ≺₁ c') ⊎ ((a' ≡ c') × (b' ≺₁ d'))
      inner (inl h)       = inl (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) ea ec h)
      inner (inr (e , h)) =
        inr ( ↪-inj {a = K} (sym ea ∙ e ∙ ec)
```

相等情形同样传递：被点名集合的等式经两次命名的循环改写后，由 `K` 的命名的单射性变成索引的等式，而第二坐标照旧比较。

```agda
            , subst2 (λ x y → ⟨ x ∈ˢ y ⟩) eb ed h )
```

若第一个最大值属于第二个，沿 `em` 与 `en` 传输这份隶属，便得到 `p ≺ₚ q` 的严格最大值分支，与 `nk` 矛盾。

```agda
      outer : ⟨ fst m ∈ˢ fst n ⟩
            ⊎ ((fst m ≡ fst n)
               × ∥ ⟨ fst a ∈ˢ fst c ⟩ ⊎ ((fst a ≡ fst c) × ⟨ fst b ∈ˢ fst d ⟩) ∥₁)
            → Empty.⊥
      outer (inl h)       = nk (inl (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) em en h))
```

若两个最大值相等，底层集合的等式经命名单射性变成索引的等式，内层引理随后在宿主序内比较两对，再次反驳拒绝。

```agda
      outer (inr (e , h)) = PT.rec Empty.isProp⊥
        (λ w → nk (inr (↪-inj {a = K} (sym em ∙ e ∙ en) , inner w))) h
```

证明 `lt→≺` 时，宿主对的三歧性给出三种可能。所需的严格分支可直接返回；在相等或反向严格的分支中，若拒绝 `p ≺ₚ q`，`refute` 会使之与已假设的 `Lt` 矛盾，因而仍得到所需比较。

```agda
  lt→≺ : (p q : Pair) → Lt (code p) (code q) → p ≺ₚ q
  lt→≺ p q l = go (SQ.tri≺ K oκ p q)
    where
    refuted : ((p ≺ₚ q) → Empty.⊥) → p ≺ₚ q
    refuted nk = Empty.rec (PT.rec Empty.isProp⊥ (refute p q nk) l)
```

相等情形中，假设的 `p ≺ₚ q` 可传输为 `q ≺ₚ q`，违背非自反性；反向严格情形中，把这份假设比较与 `q ≺ₚ p` 复合会得到 `p ≺ₚ p`，同样不可能。

```agda
    go : TriW (p ≺ₚ q) (p ≡ q) (q ≺ₚ p) → p ≺ₚ q
    go (lt k) = k
    go (eq e) = refuted (λ k → SQ.irr≺ K oκ q (subst (λ w → w ≺ₚ q) e k))
    go (gt h) = refuted (λ k → SQ.irr≺ K oκ p (SQ.trans≺ K oκ p q p k h))
```

逆向的 `≺→lt` 把宿主比较写进对象语言。其六个见证是被提升的坐标与两个被提升的最大值，两条对等式定义性成立，最大值数据来自 `max-in`，序数据来自宿主比较本身。

```agda
  ≺→lt : (p q : Pair) → p ≺ₚ q → Lt (code p) (code q)
  ≺→lt (a' , b') (c' , d') k =
    ∣ upK a' , upK b' , upK c' , upK d' , upK (maxOrd a' b') , upK (maxOrd c' d')
    , ( refl , refl , max-in a' b' , max-in c' d' , ord k ) ∣₁
    where
```

序数据按情形逐条读取：严格隶属原样通过；两种相等情形分别沿最大值的命名与坐标的命名传输。

```agda
    ord : (a' , b') ≺ₚ (c' , d')
        → OrdIs (upK (maxOrd a' b')) (upK (maxOrd c' d')) (upK a') (upK b') (upK c') (upK d')
    ord (inl h)                 = ∣ inl h ∣₁
    ord (inr (e , inl h))       = ∣ inr (cong ↑ e , ∣ inl h ∣₁) ∣₁
    ord (inr (e , inr (f , h))) = ∣ inr (cong ↑ e , ∣ inr (cong ↑ f , h) ∣₁) ∣₁
```

若 `x < y`，与 `y < z` 传递即得 `x < z`；若 `x = y`，则沿该等式传输已有的 `y < z`。

```agda
  private
    ≤→≺ : (x y z : ⟪ K ⟫) → SQ._≤₁_ K oκ x y → y ≺₁ z → x ≺₁ z
    ≤→≺ x y z (inl h) h' = SQ.trans₁ K oκ x y z h h'
    ≤→≺ x y z (inr e) h' = subst (λ w → w ≺₁ z) (sym e) h'
```

配套引理由 `x ≤ y` 与 `y = y'` 得出 `x` 属于 `y'` 的后继。严格情形中，`x ∈ y'` 直接给出后继隶属；相等情形中，把 `x` 与 `y'` 等同后，目标化为 `y'` 属于自身后继。

```agda
    ≤→∈suc : (x y y' : ⟪ K ⟫) → SQ._≤₁_ K oκ x y → y ≡ y'
           → ⟨ ↑ x ∈ˢ sucV (↑ y') ⟩
    ≤→∈suc x y y' (inl h) e = ∈sucV-inl (subst (λ w → x ≺₁ w) e h)
    ≤→∈suc x y y' (inr q) e =
      subst (λ w → ⟨ ↑ w ∈ˢ sucV (↑ y') ⟩) (sym (q ∙ e)) (self∈sucV (↑ y'))
```

节段引理现在从序中读出：若对 `r` 低于对 `p`，则 `r` 的第一坐标属于 `p` 的最大值的后继；在最大值严格比较的情形，这是先「至多」再严格比较。

```agda
  fst∈suc : (r p : Pair) → r ≺ₚ p
          → ⟨ ↑ (fst r) ∈ˢ sucV (↑ (maxOrd (fst p) (snd p))) ⟩
  fst∈suc (a , b) (c , d) (inl h) =
    ∈sucV-inl (≤→≺ a (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .fst) h)
  fst∈suc (a , b) (c , d) (inr (e , _)) =
```

最大值相等的情形中，第一坐标至多为共同的最大值，而两个最大值被等同，故隶属由「最大值属于自身后继」得出。

```agda
    ≤→∈suc a (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .fst) e
```

把同一论证施于第二坐标，即得 `snd∈suc`：`r` 的第二坐标同样落入 `p` 的最大值的后继，无论两个最大值严格比较还是相等。

```agda
  snd∈suc : (r p : Pair) → r ≺ₚ p
          → ⟨ ↑ (snd r) ∈ˢ sucV (↑ (maxOrd (fst p) (snd p))) ⟩
  snd∈suc (a , b) (c , d) (inl h) =
    ∈sucV-inl (≤→≺ b (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .snd) h)
  snd∈suc (a , b) (c , d) (inr (e , _)) =
```

这两个界说明，对 `(c, d)` 的每个前驱，其两个坐标都属于 `suc(max(c, d))`。

```agda
    ≤→∈suc b (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .snd) e
module Coll (κ : S) (oκ : IsOrd (fst κ)) where
```

这些界控制 Gödel 序的每个前驱节段。结合良基性与传递性，它们使 `prodL κ` 上的关系处于可塌缩为序数序型的情形。

```agda
  open Order κ oκ
```

将要被塌缩成序型的集合是 `P`，即乘积：序数 `κ` 的成员的有序对之集，已在 `L` 内部分离而来。

```agda
  P : S
  P = prodL κ
```

塌缩所用关系是 `R`，即该乘积上的 Gödel 序：`P` 的两个成员恰好在其一低于另一个时相关。

```agda
  R : S
  R = godel P
```

对 Gödel 关系这可直接读出：只要 `y R x`，`y` 与 `x` 都是该乘积的成员。

```agda
  Rsub : (y x : S) → Holds R y x → ⟨ fst y ∈ fst P ⟩ × ⟨ fst x ∈ fst P ⟩
  Rsub y x h = godel-out P y x h .fst , godel-out P y x h .snd .fst
```

序型机制针对这个乘积一次性实例化。其定义域是塌缩的一个索引集，而 `φ` 为每个索引读出乘积中相应成员所呈现的宿主对：两个坐标由乘积的呈现读式无截断地恢复。

```agda
  module OT = Code P R Rsub using (Dom; Dom≡; isProp≺; toDom; up; up-mem; up-toDom; ↪; _≺_; ≺-in; ≺-out; module Conjuncts)
  φ : OT.Dom → Pair
  φ m = prodL-fst κ (OT.up m) (OT.up-mem m) .fst
      , prodL-fst κ (OT.up m) (OT.up-mem m) .snd .fst
```

该读式随附一条等式：索引的内部编码等于两个坐标的外围有序对。这条等式是内部序与外部序之间每一次比较所依赖的枢纽。

```agda
  φ-eq : (m : OT.Dom) → OT.↪ m ≡ code (φ m)
  φ-eq m = prodL-fst κ (OT.up m) (OT.up-mem m) .snd .snd
```

`φ` 是单射的：若两个索引指名同一宿主对，则它们的编码一致，而定义域自身的判据「编码相等」即返回索引相等。因此两个不同的乘积索引不可能被送到同一个宿主对。

```agda
  φ-inj : (m n : OT.Dom) → φ m ≡ φ n → m ≡ n
  φ-inj m n e = OT.Dom≡ (φ-eq m ∙ cong code e ∙ sym (φ-eq n))
```

向前传递把内部序向外读：若两个索引在 `L` 内部可比较，则它们的宿主对在 Gödel 序下可比较。证明引用定义等式与公式的外向读式，然后在两个宿主对上施用传递 `lt→≺`。

```agda
  ≺-fwd : (m n : OT.Dom) → m OT.≺ n → φ m ≺ₚ φ n
  ≺-fwd m n k = lt→≺ (φ m) (φ n)
    (subst2 Lt (φ-eq m) (φ-eq n) (godel-out P (OT.up m) (OT.up n) (OT.≺-out m n k) .snd .snd))
```

向后传递把宿主序向内读，引用公式的向内读式与同一对上的传递 `≺→lt`。两个方向合起来说：塌缩索引上的内部关系，恰是经 `φ` 读出的宿主 Gödel 序。

```agda
  ≺-bwd : (m n : OT.Dom) → φ m ≺ₚ φ n → m OT.≺ n
  ≺-bwd m n k = OT.≺-in m n
    (godel-in P (OT.up m) (OT.up n) (OT.up-mem m) (OT.up-mem n)
      (subst2 Lt (sym (φ-eq m)) (sym (φ-eq n)) (≺→lt (φ m) (φ n) k)))
```

良基性随索引传递。宿主对的可及性给出相应索引的可及性，其前驱向前映到严格更小的对所对应的宿主对。于是沿外部序的归纳成为沿内部序的归纳。

```agda
  wf : WellFounded OT._≺_
  wf m = go (SQ.wf≺ K oκ (φ m))
    where
    go : {n : OT.Dom} → Acc _≺ₚ_ (φ n) → Acc OT._≺_ n
    go {n} (acc r) = acc (λ n' k → go (r (φ n') (≺-fwd n' n k)))
```

传递性同样传递：内部的两步先向外读出，由宿主序的传递性复合，再向内读回为从 `a` 直达 `c` 的一步。

```agda
  ≺-trans : {a b c : OT.Dom} → a OT.≺ b → b OT.≺ c → a OT.≺ c
  ≺-trans {a} {b} {c} k k' =
    ≺-bwd a c (SQ.trans≺ K oκ (φ a) (φ b) (φ c) (≺-fwd a b k) (≺-fwd b c k'))
```

三歧性补全所传递的整套结构。对任意两个索引，宿主三歧比较它们的对；该陈述是内部比较的三向和。

```agda
  tri : (a b : OT.Dom) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
  tri a b = go (SQ.tri≺ K oκ (φ a) (φ b))
    where
    go : TriW (φ a ≺ₚ φ b) (φ a ≡ φ b) (φ b ≺ₚ φ a)
       → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
```

三种情形分别读回：两个严格情形经向后传递，相等情形经 `φ` 的单射性，指名同一宿主对的索引相等。

```agda
    go (lt h) = inl (≺-bwd a b h)
    go (eq e) = inr (inl (φ-inj a b e))
    go (gt h) = inr (inr (≺-bwd b a h))
```

良基性与传递性构造出塌缩及其序型；

```agda
  module C = OT.Conjuncts wf ≺-trans using (module Inj; col; col-ord; col-out; colTable; colTable-in; colTable-pair; colʟ; otL; otL-out)
  module I = C.Inj tri using (code; col-inj; module Inverse)
  injL-ot : InjL P C.otL
  injL-ot = ∣ C.colTable , I.code ∣₁
```

## 三条计数事实

三歧性随后证明塌缩映射单射，因此其图见证内部单射 `P ↪ C.otL`。

```agda
incl : (a b : V ℓ) → ((z : V ℓ) → ⟨ z ∈ˢ a ⟩ → ⟨ z ∈ˢ b ⟩) → ⟪ a ⟫ ↪ ⟪ b ⟫
```

计数引理从外围一侧开始。两个外围集合之间的包含作用于小呈现：子集的每个索引指名较大集合的一个成员，而该成员在较大呈现中的纤维则指名相应的索引。

```agda
incl a b sub = ι , ι-inj
  where
  ι : ⟪ a ⟫ → ⟪ b ⟫
  ι m = fiber b (sub (⟪ a ⟫↪ m) (member a m)) .fst
  ι-inj : (m n : ⟪ a ⟫) → ι m ≡ ι n → m ≡ n
```

诱导出的索引映射是单射的：若子集的两个索引所指名的成员在较大呈现中被同一索引指名，则命名的等式迫使被指名成员相等，而子集自身的单射性返回索引的相等。

```agda
  ι-inj m n e = ↪-inj {a = a}
    (sym (fiber b (sub (⟪ a ⟫↪ m) (member a m)) .snd)
     ∙ cong ⟪ b ⟫↪ e
     ∙ fiber b (sub (⟪ a ⟫↪ n) (member a n)) .snd)
opaque
```

`L` 中的编码单射可在外围读出：图的各项条件确定其定义域与值域的小呈现之间的单射。再结合每个无穷序数 `a` 都满足 `ω ⊆ a`，便把内部单射同通常的基数比较连接起来。

```agda
  coded→ambient : (a b : S) → Σ[ F ∈ S ] InjCode F a b → ⟪ fst a ⟫ ↪ ⟪ fst b ⟫
  coded→ambient a b (F , sv , dm , ij , ran) = Sm.small , Sm.small-inj
    where module Sm = Small F a b sv dm ij ran
ω⊆ : (a : V ℓ) → IsOrd a → (⟨ a ∈ˢ ω ⟩ → Empty.⊥)
   → (z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ a ⟩
```

`ω` 的包含由序数 `a` 处的三歧性得出：由无穷性假设 `a` 不属于 `ω`；`a` 等于 `ω` 时传输该隶属；`ω` 在 `a` 之内时由传递性转发每一份隶属。

```agda
ω⊆ a oa a∉ω z z∈ω = go (ord-tri a oa ω ω-ord)
  where
  go : ⟨ a ∈ˢ ω ⟩ ⊎ ((a ≡ ω) ⊎ ⟨ ω ∈ˢ a ⟩) → ⟨ z ∈ˢ a ⟩
  go (inl h)         = Empty.rec (a∉ω h)
  go (inr (inl e))   = subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈ω
```

其最后一种情形是把传递性施于 `z ∈ ω` 与 `ω ∈ a`。包含到手之后，第二条计数事实是排除：无穷序数不容许到 `ω` 之成员 (即有限序数) 的内部单射。

```agda
  go (inr (inr ω∈a)) = oa .fst z∈ω ω∈a
no-fin : (a b : S) → IsOrd (fst a) → (⟨ fst a ∈ˢ ω ⟩ → Empty.⊥)
       → IsOrd (fst b) → ⟨ fst b ∈ˢ ω ⟩ → InjL a b → Empty.⊥
no-fin a b oa a∉ω ob b∈ω = PT.rec Empty.isProp⊥ (λ c →
  finite-excl-ω (fst b) ob b∈ω (λ x → h c x , h c x)
```

反驳的最后一步引用 `ω` 含于 `a` 的事实：由于 `ω ⊆ a`，两条引理得以复合，于是「`ω` 单射入 `b`」经过 `a` 中转就成了「`ω` 单射入有限集 `b`」。包含映射 `ι` 在 where 子句中一次性确定。

```agda
    (λ x y e → ι .snd x y
       (coded→ambient a b c .snd (ι .fst x) (ι .fst y) (cong fst e))))
  where
  ι : ⟪ ω ⟫ ↪ ⟪ fst a ⟫
  ι = incl ω (fst a) (ω⊆ (fst a) oa a∉ω)
```

映射 `h` 在包含 `ω ↪ a` 之后求值编码单射。

```agda
  h : Σ[ F ∈ S ] InjCode F a b → ⟪ ω ⟫ → ⟪ fst b ⟫
  h c x = coded→ambient a b c .fst (ι .fst x)
```

## 编码单射提升到乘积

为构造乘积上的映射，固定一个图 `F`：它在 `a` 上单值、定义域为 `a`、具有单射性，且取值落在 `b` 中；这四项正是编码单射 `a ↪ b` 的条件。

```agda
module ProdMap (a b F : S)
               (sv : ⟨ (F ∷ a ∷ []) ⊨ svAt zero ⟩)
               (dm : ⟨ (F ∷ a ∷ []) ⊨ domAt zero (suc zero) ⟩)
```

映射 `h` 在包含 `ω ↪ a` 之后求值编码单射。为构造乘积上的映射，固定一个图 `F`：它在 `a` 上单值、定义域为 `a`、具有单射性，且取值落在 `b` 中；这四项正是编码单射 `a ↪ b` 的条件。

```agda
               (ij : ⟨ (F ∷ a ∷ []) ⊨ injAt zero ⟩)
               (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩
                    → ⟨ fst y ∈ fst b ⟩) where
```

提取模块从图中读出真正的函数：`toFun` 在每个定义域元素处计算取值，`toFun-graph` 证明相应的对属于图，`toFun-inj` 把图的单射性转移到函数上。

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

两个谓词刻画所涉对象。`Mem p` 说 `p` 是乘积 `prodL a` 的成员；`Comp p` 说 `p` 可分解为 `a` 的两个成员 `x` 与 `y`，且其有序对恰是 `p` 的底层集合。

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem p = ⟨ fst p ∈ˢ fst (prodL a) ⟩
  Comp : S → Type (ℓ-suc ℓ)
  Comp p = Σ[ x ∈ S ] Σ[ y ∈ S ]
             (⟨ fst x ∈ˢ fst a ⟩ × ⟨ fst y ∈ˢ fst a ⟩ × (fst p ≡ pr (fst x) (fst y)))
```

乘积成员的分量唯一，`isPropComp` 证明这一点。第一投影由有序对的单射性等同；第二投影随后在内层引理中比较。

```agda
  isPropComp : (p : S) → isProp (Comp p)
  isPropComp p (x , y , _ , _ , e) (x' , y' , _ , _ , e') =
    Σ≡Prop inner (Σ≡Prop (λ v → snd (isL v)) (pr-inj (sym e ∙ e') .fst))
    where
    inner : (x : S)
```

内层引理比较第二分量：与同一第一坐标配对的两个候选 `y` 与 `y'` 相等，因为对等式把它们的底层集合与同一个集合等同，而可构造性与隶属分量都是命题。

```agda
          → isProp (Σ[ y ∈ S ] (⟨ fst x ∈ˢ fst a ⟩ × ⟨ fst y ∈ˢ fst a ⟩
                                × (fst p ≡ pr (fst x) (fst y))))
    inner x (y , _ , _ , e) (y' , _ , _ , e') =
      Σ≡Prop (λ w → isProp× (snd (fst x ∈ˢ fst a))
                      (isProp× (snd (fst w ∈ˢ fst a)) (setIsSet _ _)))
```

最后一个分量由底层集合的相等消解，唯一性随之完成：`Comp p` 是命题，故其截断的存在可以消去为一份真实的分解。

```agda
        (Σ≡Prop (λ v → snd (isL v)) (pr-inj (sym e ∙ e') .snd))
```

读式 `comp` 把乘积的截断隶属变成真实的分解，而刚刚证明的唯一性正是这一消去的许可。取值映射 `val` 随后在 `a` 的每个成员 `x` 处计算编码单射 `F` 指派给它的元素。

```agda
  comp : (p : S) → Mem p → Comp p
  comp p mp = PT.rec (isPropComp p) (λ z → z) (prodL-out a p mp)
  opaque
    val : (x : S) → ⟨ fst x ∈ˢ fst a ⟩ → S
    val x mx = E.toFun (x , mx)
```

图引理证明：计算出的取值与其输入在图中配对，即 `x` 与 `val x` 的有序对属于 `F`。这就是赋值的记录，对 `a` 的每个成员都予保留。

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

单射性引理把图的单射性转移到计算出的取值上：若 `a` 的两个成员被指派的取值有相同的底层集合，则这两个成员本身相等。这正是使对上的提升映射成为单射的关键。

```agda
    val-inj : (x : S) (mx : ⟨ fst x ∈ˢ fst a ⟩) (x' : S) (mx' : ⟨ fst x' ∈ˢ fst a ⟩)
            → 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')
```

提升映射 `fn` 作用于乘积成员的方式是按坐标施用 `F`：即第一坐标的像与第二坐标的像组成的内部有序对。

```agda
  fn : (p : S) → Mem p → S
  fn p mp = prʟ (val (comp p mp .fst) (comp p mp .snd .snd .fst))
                (val (comp p mp .snd .fst) (comp p mp .snd .snd .snd .fst))
```

像落入 `b` 之上的乘积：由值域子句，两个分量取值都是 `b` 的成员，故其内部对属于 `prodL b`。内部对与外围对的等同则沿其第一投影引理传输。

```agda
  into : (p : S) (mp : Mem p) → ⟨ fst (fn p mp) ∈ˢ fst (prodL b) ⟩
  into p mp =
    subst (λ w → ⟨ w ∈ˢ fst (prodL b) ⟩) (sym (prʟ-fst (val x mx) (val y my)))
      (prodL-in b (val x mx) (val y my)
        (ran x (val x mx) (val-graph x mx)) (ran y (val y my) (val-graph y my)))
```

`p` 的分解给出坐标 `x,y`，并同时给出 `x ∈ a` 与 `y ∈ a` 的证明。这些隶属证明是数据的一部分，因为 `val` 只在 `a` 的成员上定义。

```agda
    where
    x = comp p mp .fst
    y = comp p mp .snd .fst
    mx = comp p mp .snd .snd .fst
    my = comp p mp .snd .snd .snd .fst
```

链类型汇集图公式须见证的全部内容：`p` 是 `x` 与 `y` 的对，`q` 是 `x'` 与 `y'` 的对，且 `F` 的图包含两个第一坐标的对与两个第二坐标的对。

```agda
  Chain : S → S → S → S → S → S → Type (ℓ-suc ℓ)
  Chain q p x y x' y' =
      (fst p ≡ pr (fst x) (fst y)) × (fst q ≡ pr (fst x') (fst y'))
    × ⟨ pr (fst x) (fst x') ∈ fst F ⟩ × ⟨ pr (fst y) (fst y') ∈ fst F ⟩
```

图公式 `mapFo` 以存在量词选取 `x,y,x',y'`，并合取四项断言：`p=(x,y)`、`q=(x',y')`，以及 `F` 的两次应用。

```agda
  opaque
    mapFo : Formula S 2
    mapFo = ∃̇ (∃̇ (∃̇ (∃̇ (
          prAtL i5 i3 i2
       ∧̇ (prAtL i4 i1 i0
```

最后两个原子是应用子句：`F` 的图包含两个第一坐标的对与两个第二坐标的对，这恰是「`F` 把 `x` 映到 `x'`、把 `y` 映到 `y'`」的陈述。

```agda
       ∧̇ (appC F i3 i1
       ∧̇ appC F i2 i0))))))
```

充分性对照一个具体的六条目语境检验：该语境先加入四个见证 (最新在前)，再接对 `q` 与对 `p`，于是第零槽位是 `y'`、第五槽位是 `p`，与四个原子的索引一致。

```agda
    private
      env₄ : S → S → S → S → S → S → S ^ 6
      env₄ q p x y x' y' = y' ∷ x' ∷ y ∷ x ∷ q ∷ p ∷ []
```

第一条充分性引理读取 `p` 的配对原子：该原子在语境中的满足，就是 `p` 的底层集合与 `x`、`y` 的有序对之间的等式。

```agda
      at1 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ prAtL i5 i3 i2 ⟩ ≡ (fst p ≡ pr (fst x) (fst y))
      at1 q p x y x' y' = cong ⟨_⟩ (prAtL-adequate i5 i3 i2 (env₄ q p x y x' y'))
```

第二条充分性引理对 `q` 与见证 `x'`、`y'` 做同样的事。这两条等式为链的对部分提供了锚点。

```agda
      at2 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ prAtL i4 i1 i0 ⟩ ≡ (fst q ≡ pr (fst x') (fst y'))
      at2 q p x y x' y' = cong ⟨_⟩ (prAtL-adequate i4 i1 i0 (env₄ q p x y x' y'))
```

第三条充分性引理读取第一个应用原子：其在 `L` 中的满足，被等同于两个第一坐标组成的对在 `F` 图中的外围隶属。

```agda
      at3 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ appC F i3 i1 ⟩ ≡ ⟨ pr (fst x) (fst x') ∈ fst F ⟩
      at3 q p x y x' y' = cong ⟨_⟩ (appC-adequate F i3 i1 (env₄ q p x y x' y'))
```

第四条对第二坐标做同样的事，四个原子由此全部翻译为关于集合成员的普通陈述。

```agda
      at4 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ appC F i2 i0 ⟩ ≡ ⟨ pr (fst y) (fst y') ∈ fst F ⟩
      at4 q p x y x' y' = cong ⟨_⟩ (appC-adequate F i2 i0 (env₄ q p x y x' y'))
```

向外方向依次消耗四层嵌套的存在量词，组装出截断的链：四个见证连同全部四个原子都传输到其外围读法。

```agda
    mapFo-out : (q p : S) → ⟨ (q ∷ p ∷ []) ⊨ mapFo ⟩
              → ∥ Σ[ x ∈ S ] Σ[ y ∈ S ] Σ[ x' ∈ S ] Σ[ y' ∈ S ] Chain q p x y x' y' ∥₁
    mapFo-out q p = PT.rec squash₁ (λ { (x , hx) → PT.rec squash₁ (λ { (y , hy) →
      PT.rec squash₁ (λ { (x' , hx') → PT.map (λ { (y' , (h1 , (h2 , (h3 , h4)))) →
        x , y , x' , y'
```

每个原子都沿其自身的充分性路径传输，因此链所记录的是普通的等式与普通的隶属，而非满足判断。

```agda
        , ( transport (at1 q p x y x' y') h1 , transport (at2 q p x y x' y') h2
          , transport (at3 q p x y x' y') h3 , transport (at4 q p x y x' y') h4 ) })
        hx' }) hy }) hx })
```

向内方向从链重建公式：四个见证作为嵌套存在量词的见证填入，四个原子沿充分性路径反方向传输。

```agda
    mapFo-in : (q p x y x' y' : S) → Chain q p x y x' y' → ⟨ (q ∷ p ∷ []) ⊨ mapFo ⟩
    mapFo-in q p x y x' y' (h1 , h2 , h3 , h4) =
      ∣ x , ∣ y , ∣ x' , ∣ y'
      , ( transport (sym (at1 q p x y x' y')) h1
        , ( transport (sym (at2 q p x y x' y')) h2
```

最后两个应用原子补全由四项断言组成的嵌套合取，从而完成 `mapFo` 的见证。

```agda
        , ( transport (sym (at3 q p x y x' y')) h3
          , transport (sym (at4 q p x y x' y')) h4 ))) ∣₁ ∣₁ ∣₁ ∣₁
```

唯一性说图公式确定取值：任何在图中与 `p` 配对的 `q` 都等于典范像 `fn p mp`。证明把截断的链消耗进对等式，而目标正是 h-集合中的等式。

```agda
  only : (p : S) (mp : Mem p) (q : S) → ⟨ (q ∷ p ∷ []) ⊨ mapFo ⟩ → q ≡ fn p mp
  only p mp q h = PT.rec (isSetS q (fn p mp)) step (mapFo-out q p h)
    where
    x = comp p mp .fst
    y = comp p mp .snd .fst
```

成员 `p` 的四个分量像在像引理中那样一次性命名，使唯一性的计算可以直接引用它们。

```agda
    mx = comp p mp .snd .snd .fst
    my = comp p mp .snd .snd .snd .fst
    e = comp p mp .snd .snd .snd .snd
```

链中的等式把 `q` 写成 `(x₁',y₁')`，而固定的分解把 `p` 写成 `(x,y)`。单值性分别把 `x₁'`、`y₁'` 认同为 `val x`、`val y`，故 `q` 就是典范像 `(val x,val y)`。

```agda
    step : Σ[ x₁ ∈ S ] Σ[ y₁ ∈ S ] Σ[ x₁' ∈ S ] Σ[ y₁' ∈ S ] Chain q p x₁ y₁ x₁' y₁'
         → q ≡ fn p mp
    step (x₁ , y₁ , x₁' , y₁' , (e₁ , e₂ , h3 , h4)) =
      Σ≡Prop (λ v → snd (isL v))
        (e₂ ∙ cong₂ pr ex ey ∙ sym (prʟ-fst (val x mx) (val y my)))
```

有序对的单射性把对等式拆成两条：`x₁` 的底层集合等于 `x` 的，`y₁` 的底层集合等于 `y` 的。

```agda
      where
      x₁≡x : fst x₁ ≡ fst x
      x₁≡x = pr-inj (sym e₁ ∙ e) .fst
      y₁≡y : fst y₁ ≡ fst y
      y₁≡y = pr-inj (sym e₁ ∙ e) .snd
```

两条图隶属随后经 `F` 的单值性读出：一旦知道 `x₁` 指名 `x`，与 `x₁` 配对的条目在其第一投影上必与已记录的取值 `val x mx` 一致。

```agda
      ex : fst x₁' ≡ fst (val x mx)
      ex = svAt-out zero (F ∷ a ∷ []) sv x x₁' (val x mx)
             (subst (λ w → ⟨ pr w (fst x₁') ∈ fst F ⟩) x₁≡x h3) (val-graph x mx)
      ey : fst y₁' ≡ fst (val y my)
      ey = svAt-out zero (F ∷ a ∷ []) sv y y₁' (val y my)
```

第二坐标以完全相同的方式处理，使用它自己的隶属与它自己被记录的取值。

```agda
             (subst (λ w → ⟨ pr w (fst y₁') ∈ fst F ⟩) y₁≡y h4) (val-graph y my)
```

因此 `mapFo` 定义逐坐标像 `fn`：每个乘积成员都具有这一图取值，而 `into` 把该取值置于 `prodL b` 中。

```agda
  M : DefinableMap
  M = record
    { dom = prodL a ; cod = prodL b ; fn = fn ; into = into ; graph = mapFo
    ; defines = λ p mp →
        mapFo-in (fn p mp) p (comp p mp .fst) (comp p mp .snd .fst)
```

定义子句就是那条链，在 `p` 的典范像处实例化：两个取值、乘积成员的对等式，以及两条图引理，共同证明图对像及其输入成立。

```agda
          (val (comp p mp .fst) (comp p mp .snd .snd .fst))
          (val (comp p mp .snd .fst) (comp p mp .snd .snd .snd .fst))
          ( comp p mp .snd .snd .snd .snd
          , prʟ-fst _ _
          , val-graph (comp p mp .fst) (comp p mp .snd .snd .fst)
```

唯一性定理排除了第二个图取值，因此该公式确实表示 `prodL a` 上的函数。

```agda
          , val-graph (comp p mp .snd .fst) (comp p mp .snd .snd .snd .fst) )
    ; only = only }
```

提升映射的单射性被直接证明：若两个乘积成员的像作为底层集合相等，则这两个成员本身相等。证明把每个成员从其分量重新组装。

```agda
  inj : (p : S) (mp : Mem p) (p' : S) (mp' : Mem p')
      → fst (fn p mp) ≡ fst (fn p' mp') → fst p ≡ fst p'
  inj p mp p' mp' e = e₀ ∙ cong₂ pr ex ey ∙ sym e₀'
    where
    x = comp p mp .fst
```

两个成员的分量各一次性命名，使两份分解可以逐坐标比较。

```agda
    y = comp p mp .snd .fst
    mx = comp p mp .snd .snd .fst
    my = comp p mp .snd .snd .snd .fst
    e₀ = comp p mp .snd .snd .snd .snd
    x' = comp p' mp' .fst
```

所假设的像相等是内部对的相等；其单射性把它拆成两个第一像的相等与两个第二像的相等。

```agda
    y' = comp p' mp' .snd .fst
    mx' = comp p' mp' .snd .snd .fst
    my' = comp p' mp' .snd .snd .snd .fst
    e₀' = comp p' mp' .snd .snd .snd .snd
    q : (fst (val x mx) ≡ fst (val x' mx')) × (fst (val y my) ≡ fst (val y' my'))
```

每个分量的等式都被喂给取值映射的单射性，得到第一坐标相等与第二坐标相等；对等式的两个坐标再沿它们传输。

```agda
    q = pr-inj (sym (prʟ-fst (val x mx) (val y my)) ∙ e ∙ prʟ-fst (val x' mx') (val y' my'))
    ex : fst x ≡ fst x'
    ex = val-inj x mx x' mx' (fst q)
    ey : fst y ≡ fst y'
    ey = val-inj y my y' my' (snd q)
```

可定义映射与其单射性装配成内部单射：在 `L` 内部，`prodL a` 单射入 `prodL b`。

```agda
  injL : InjL (prodL a) (prodL b)
  injL = Inj.injL M inj
```

由于 `InjL` 是命题截断的，提升编码单射 `a ↪ b` 无须全局选定其图。

```agda
prod-inj : (a b : S) → InjL a b → InjL (prodL a) (prodL b)
prod-inj a b = PT.rec squash₁
  (λ { (F , sv , dm , ij , ran) → ProdMap.injL a b F sv dm ij ran })
```

## 定理

为吸收无穷序数新增的顶端元素，还须把该序数的后继单射回序数本身。

```agda
module Shift (mL : S) (om : IsOrd (fst mL)) (m∉ω : ⟨ fst mL ∈ˢ ω ⟩ → Empty.⊥) where
```

记 `mL` 的底层序数为 `m`。隶属与有限性判定针对这个集合，而 `mL` 保留它属于 `L` 的证据。

```agda
  private
    m : V ℓ
    m = fst mL
```

移位的定义域是内部后继 `D = sucʟ mL`：即 `L` 内该序数的后继，它既包含 `m` 的成员，也包含 `m` 自身。

```agda
    D : S
    D = sucʟ mL
```

`L` 中两个元素的相等就是其底层集合的相等，因为可构造性分量是命题。这条小等式在移位内部的每一处等同都要用到。

```agda
    S≡ : {x y : S} → fst x ≡ fst y → x ≡ y
    S≡ = Σ≡Prop (λ v → snd (isL v))
```

由于 `m` 无穷，`ω` 的每个成员都属于 `m`；这一包含引自计数事实，也正是有限成员的后继得以留在 `m` 内的原因。

```agda
    ω⊆m : (z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ m ⟩
    ω⊆m = ω⊆ m om m∉ω
```

先陈述移位定义域中的隶属，并定义第一个判定：元素要么属于 `ω`，要么该隶属被反驳。这一析取是真正的情形分裂，由排中律给出。

```agda
    Mem : S → Type (ℓ-suc ℓ)
    Mem x = ⟨ fst x ∈ˢ fst D ⟩
    Fin? : S → Type (ℓ-suc ℓ)
    Fin? x = ⟨ fst x ∈ˢ ω ⟩ ⊎ (⟨ fst x ∈ˢ ω ⟩ → Empty.⊥)
```

第二个判定区分后继的成员：`sucʟ mL` 的元素要么属于 `m`，要么等于 `m`，这正是「属于后继」的含义。

```agda
    Top? : S → Type (ℓ-suc ℓ)
    Top? x = ⟨ fst x ∈ˢ m ⟩ ⊎ (fst x ≡ m)
```

第一个判定是排中律的一个实例，施用于 `x` 属于 `ω` 这条隶属命题。

```agda
    fin? : (x : S) → Fin? x
    fin? x = lem (fst x ∈ˢ ω)
```

第二个判定同样是排中律的实例，并经后继的消去细化：`sucʟ mL` 的成员要么属于 `m`、要么等于 `m`，于是隶属被反驳后就只剩相等。

```agda
    top? : (x : S) → Mem x → Top? x
    top? x h = go (lem (fst x ∈ˢ m))
      where
      go : ⟨ fst x ∈ˢ m ⟩ ⊎ (⟨ fst x ∈ˢ m ⟩ → Empty.⊥) → Top? x
      go (inl k)  = inl k
```

在被反驳的情形中，消去消耗后继中的截断隶属；而两种结果互斥：一个元素不能既属于 `m` 又等于 `m`，否则 `m` 将属于自身，这被隶属的非自反性所反驳。

```agda
      go (inr nk) = inr (∈sucV-elim {A = m} {x = fst x} (setIsSet (fst x) m)
        (subst (λ w → ⟨ fst x ∈ˢ w ⟩) (sucʟ-fst mL) h) (λ k → Empty.rec (nk k)) (λ q → q))
    not-both : (x : S) → ⟨ fst x ∈ˢ m ⟩ → fst x ≡ m → Empty.⊥
    not-both x k q = ∈-irrefl m (subst (λ w → ⟨ w ∈ˢ m ⟩) q k)
```

有限情形与顶端情形不能重合。若 `x` 属于 `ω` 且等于 `m`，沿该等式搬运其隶属关系便会得到 `m ∈ ω`，与 `m` 无穷的假设矛盾。

```agda
    ω-fin : (x : S) → ⟨ fst x ∈ˢ ω ⟩ → fst x ≡ m → Empty.⊥
    ω-fin x k q = m∉ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) q k)
```

后继绝不可能是空集。事实上，`a` 属于 `sucV a`；若 `sucV a = ∅`，沿该等式搬运这一隶属关系便会得到空集的一个元素。

```agda
    suc≢∅ : (a : V ℓ) → sucV a ≡ ∅ → Empty.⊥
    suc≢∅ a e = ∅-empty a
      (∈∈ₛ {a = a} {b = ∅} .fst (subst (λ w → ⟨ a ∈ˢ w ⟩) e (self∈sucV a)))
```

三种情形现在定义移位的取值。有限成员被送到其内部后继；`m` 的非有限成员被送到自身；而顶端元素 `m` 被送到 `L` 的空集。这正是两个判定所区分的三种选择。

```agda
    value : (x : S) → Fin? x → Top? x → S
    value x (inl _) _       = sucʟ x
    value x (inr _) (inl _) = x
    value x (inr _) (inr _) = ∅ʟ
```

取值保证落在 `m` 中。对有限成员，其后继由 `ω` 的极限性质成为 `ω` 的成员，而 `ω` 包含于 `m`；对 `m` 的成员，隶属就是那个判定本身；空集则是 `ω` 的成员，因而也是 `m` 的成员。

```agda
    value-in : (x : S) (f : Fin? x) (t : Top? x) → ⟨ fst (value x f t) ∈ˢ m ⟩
    value-in x (inl k) _ =
      subst (λ w → ⟨ w ∈ˢ m ⟩) (sym (sucʟ-fst x)) (ω⊆m (sucV (fst x)) (ω-limit (fst x) k))
    value-in x (inr _) (inl k) = k
    value-in x (inr _) (inr _) = ω⊆m ∅ (#∈ω zero)
```

图公式的见证类型在此声明：要么 `x` 有限且 `y` 是其后继；要么 `x` 非有限、属于 `m` 且 `y` 等于 `x`；要么 `x` 等于顶端 `m` 且 `y` 为空。三种选择被截断，各自携带自己的隶属与等式。

```agda
    Wit : (y x : S) → Type (ℓ-suc ℓ)
    Wit y x = ∥ (⟨ fst x ∈ˢ ω ⟩ × (fst y ≡ sucV (fst x)))
              ⊎ ( ((⟨ fst x ∈ˢ ω ⟩ → Empty.⊥) × ⟨ fst x ∈ˢ m ⟩ × (fst y ≡ fst x))
                ⊎ ((fst x ≡ m) × (fst y ≡ ∅)) ) ∥₁
```

图公式在对象语言中陈述，其第一个析取支说：`x` 属于内部 `ω` 且 `y` 是其后继，由后继子句读出。第二个析取支首先否认 `x` 有限。

```agda
  opaque
    graph : Formula S 2
    graph = ((var (suc zero) ∈̇ con ωʟ) ∧̇ sucAtL (suc zero) zero)
          ∨̇ ( ( (¬̇ (var (suc zero) ∈̇ con ωʟ))
              ∧̇ ((var (suc zero) ∈̇ con mL) ∧̇ (var zero ≐ var (suc zero))) )
```

其内两条受守卫的选项补全第二、第三析取支：`m` 的非有限成员与自身配对，顶端元素与 `L` 的空集配对。

```agda
            ∨̇ ((var (suc zero) ≐ con mL) ∧̇ (var zero ≐ con ∅ʟ)) )
```

后继子句的充分性记录一次：后继原子在二元组语境中的满足，就是 `y` 与外围后继 `sucV x` 之间的等式。

```agda
    private
      sa : (y x : S) → ⟨ (y ∷ x ∷ []) ⊨ sucAtL (suc zero) zero ⟩ ≡ (fst y ≡ sucV (fst x))
      sa y x = cong ⟨_⟩ (sucAtL-adequate (suc zero) zero (y ∷ x ∷ []))
```

向外读取公式时，将命题截断下的析取消去到同为命题的见证类型中。后继子句由充分性转换；中间子句中的反驳则通过命题换级从提升后的宇宙降回所需层级；顶端子句已经具有所需形式。

```agda
    graph-out : (y x : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → Wit y x
    graph-out y x = PT.rec squash₁
      (λ { (inl (k , e)) → ∣ inl (k , transport (sa y x) e) ∣₁
         ; (inr h) → PT.map (λ { (inl (n , (k , e))) →
                                  inr (inl ((λ hx → lower (n hx)) , k , e))
```

第三个析取支只携带顶端情形的两条等式，故其翻译是直接的。

```agda
                              ; (inr (q , e)) → inr (inr (q , e)) }) h })
```

三条向内引理从每种见证重建公式。对有限成员，后继等式沿充分性反方向传输，进入第一个析取支。

```agda
    in-fin : (y x : S) → ⟨ fst x ∈ˢ ω ⟩ → fst y ≡ sucV (fst x) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩
    in-fin y x k e = ∣ inl (k , transport (sym (sa y x)) e) ∣₁
```

对 `m` 的非有限成员，`x ∈ ω` 的反驳被提升为对象层的否定；它与 `x ∈ m` 和 `y = x` 一起构成中间析取支。

```agda
    in-mid : (y x : S) → (⟨ fst x ∈ˢ ω ⟩ → Empty.⊥) → ⟨ fst x ∈ˢ m ⟩ → fst y ≡ fst x
           → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩
    in-mid y x n k e = ∣ inr ∣ inl ((λ hx → lift (n hx)) , (k , e)) ∣₁ ∣₁
```

对顶端元素，顶端情形的两条等式被直接组装进第三个析取支。

```agda
    in-top : (y x : S) → fst x ≡ m → fst y ≡ ∅ → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩
    in-top y x q e = ∣ inr ∣ inr (q , e) ∣₁ ∣₁
```

移位函数现在经由两个判定定义：按判定对输入的分类，取值分别是后继、元素自身或空集。

```agda
  private
    fn : (x : S) → Mem x → S
    fn x h = value x (fin? x) (top? x h)
```

定义子句在三种情形下都得到验证：有限情形引用后继等式，中间情形是定义性的，顶端情形把空集与顶端元素配对。

```agda
    defines' : (x : S) (f : Fin? x) (t : Top? x) → ⟨ (value x f t ∷ x ∷ []) ⊨ graph ⟩
    defines' x (inl k) _       = in-fin (sucʟ x) x k (sucʟ-fst x)
    defines' x (inr n) (inl k) = in-mid x x n k refl
    defines' x (inr n) (inr q) = in-top ∅ʟ x q refl
```

唯一性把图反向读出：图中与 `x` 配对的任何 `y` 都等于所选的取值。证明把截断的析取消耗进等式目标，而后者是 h-集合中的等式。

```agda
    only' : (x : S) (f : Fin? x) (t : Top? x) (y : S)
          → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ value x f t
    only' x f t y hy = PT.rec (isSetS y (value x f t)) (go f t) (graph-out y x hy)
      where
      go : (f : Fin? x) (t : Top? x)
```

情形函数接收展开后的选项与已选定的判定。有限情形配有限肯定时，后继等式与内部配对等式沿后继的第一投影等同传输后彼此一致。

```agda
         → (⟨ fst x ∈ˢ ω ⟩ × (fst y ≡ sucV (fst x)))
           ⊎ ( ((⟨ fst x ∈ˢ ω ⟩ → Empty.⊥) × ⟨ fst x ∈ˢ m ⟩ × (fst y ≡ fst x))
             ⊎ ((fst x ≡ m) × (fst y ≡ ∅)) )
         → y ≡ value x f t
      go (inl k) _       (inl (_ , e))             = S≡ (e ∙ sym (sucʟ-fst x))
```

接下来的五个子句把已选定的有限情形或非有限成员情形与图见证比较。有限选择分别与中间见证中的反驳或顶端等式矛盾；非有限成员选择与有限见证矛盾，凭中间见证的等式与其中间值一致，并由 `m` 的成员不可能等于 `m` 排除顶端见证。

```agda
      go (inl k) _       (inr (inl (n , _ , _)))   = Empty.rec (n k)
      go (inl k) _       (inr (inr (q , _)))       = Empty.rec (ω-fin x k q)
      go (inr n) (inl k) (inl (k' , _))            = Empty.rec (n k')
      go (inr n) (inl k) (inr (inl (_ , _ , e)))   = S≡ e
      go (inr n) (inl k) (inr (inr (q , _)))       = Empty.rec (not-both x k q)
```

若选定的输入是顶端元素，则有限见证与其非有限性矛盾，中间见证则与 `m` 的成员不可能等于 `m` 相矛盾。顶端见证由其空值等式直接给出所需相等。

```agda
      go (inr n) (inr q) (inl (k' , _))            = Empty.rec (n k')
      go (inr n) (inr q) (inr (inl (_ , k , _)))   = Empty.rec (not-both x k q)
      go (inr n) (inr q) (inr (inr (_ , e)))       = S≡ e
```

这些数据确定了从 `sucʟ mL` 到 `mL` 的可定义函数：每个输入都取得位于 `m` 中的选定移位值，而上面的公式正是其图。

```agda
    M : DefinableMap
    M = record
      { dom = D ; cod = mL ; fn = fn
      ; into = λ x h → value-in x (fin? x) (top? x h)
      ; graph = graph
```

排中律为每个输入给出这两个判定。前面的存在性与唯一性论证随即表明，该图恰在选定的值处成立。

```agda
      ; defines = λ x h → defines' x (fin? x) (top? x h)
      ; only = λ x h → only' x (fin? x) (top? x h) }
```

单射性通过比较两个输入各自所属的情形来证明。若二者都有限，则移位值相等就是其后继相等，因而序数后继的单射性认同原来的两个序数。

```agda
    inj' : (x : S) (f : Fin? x) (t : Top? x) (x' : S) (f' : Fin? x') (t' : Top? x')
         → fst (value x f t) ≡ fst (value x' f' t') → fst x ≡ fst x'
    inj' x (inl k) _ x' (inl k') _ e =
      ord-suc-inj (fst x) (fst x') (mem-ord {A = ω} ω-ord (fst x) k)
        (sym (sucʟ-fst x) ∙ e ∙ sucʟ-fst x')
```

有限输入不可能与非有限成员取得相同的移位值：该等式会使后者的值、也就是后者本身属于 `ω`。它也不可能与顶端输入取得相同的值，因为这会令一个后继等于空集。

```agda
    inj' x (inl k) _ x' (inr n') (inl _) e =
      Empty.rec (n' (subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym (sucʟ-fst x) ∙ e) (ω-limit (fst x) k)))
    inj' x (inl k) _ x' (inr n') (inr _) e =
      Empty.rec (suc≢∅ (fst x) (sym (sucʟ-fst x) ∙ e))
    inj' x (inr n) (inl _) x' (inl k') _ e =
```

有限与非有限次序相反的情形给出同样的矛盾。两个非有限成员若取值相等，便立即相等；非有限成员则不可能与顶端取得同一个值，因为等于空集会使它属于 `ω`。

```agda
      Empty.rec (n (subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym (sucʟ-fst x') ∙ sym e) (ω-limit (fst x') k')))
    inj' x (inr n) (inl _) x' (inr n') (inl _) e = e
    inj' x (inr n) (inl _) x' (inr n') (inr _) e =
      Empty.rec (n (subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym e) (#∈ω zero)))
    inj' x (inr n) (inr _) x' (inl k') _ e =
```

对顶端输入而言，与有限输入的值相等会再次令后继成为空集；与非有限成员的值相等则会令该成员等于空集，因而成为有限序数。若两个输入都是顶端，它们各自与 `m` 的等式便认同二者。因此该移位在 `L` 内部是单射。

```agda
      Empty.rec (suc≢∅ (fst x') (sym (sucʟ-fst x') ∙ sym e))
    inj' x (inr n) (inr _) x' (inr n') (inl _) e =
      Empty.rec (n' (subst (λ w → ⟨ w ∈ˢ ω ⟩) e (#∈ω zero)))
    inj' x (inr n) (inr q) x' (inr n') (inr q') e = q ∙ sym q'
  injL : InjL (sucʟ mL) mL
```

可定义移位与前面的分类讨论共同给出编码单射 `sucʟ mL ↪ mL`。还要用到一个基本事实：若一个集合的两个成员由同一个纤维索引表示，则它们相等；将呈现映射作用于索引等式，便恢复出所表示成员的相等。

```agda
  injL = Inj.injL M (λ x h x' h' → inj' x (fin? x) (top? x h) x' (fin? x') (top? x' h'))
opaque
  fiber-inj : (g : V ℓ) {x y : V ℓ} (mx : ⟨ x ∈ˢ g ⟩) (my : ⟨ y ∈ˢ g ⟩)
            → fiber g mx .fst ≡ fiber g my .fst → x ≡ y
  fiber-inj g mx my e = sym (fiber g mx .snd) ∙ cong ⟪ g ⟫↪ e ∙ fiber g my .snd
```

对每个可构造的无穷序数 `a`，若它还是内部基数，归纳目标便是从其笛卡尔平方 `a × a` 回到 `a` 的编码单射。将该命题包装为 `Goal a`，即可在隶属归纳中对 `a` 以下的对象统一使用它。

```agda
Goal : V ℓ → Type (ℓ-suc ℓ)
Goal a = (la : ⟨ isL a ⟩) → IsOrd a → IsCardinalL (a , la)
       → (⟨ a ∈ˢ ω ⟩ → Empty.⊥) → InjL (prodL (a , la)) (a , la)
```

归纳步接收集合 `a`、对 `a` 每个成员的归纳假设，以及四条假设：可构造性、序数性、内部基数性与无穷性。基数性假设排除「`κ` 内部单射入其自身成员」，这正是塌缩计数所要使用的形式。

```agda
module Step (a : V ℓ) (ih : (a' : V ℓ) → ⟨ a' ∈ˢ a ⟩ → Goal a')
            (la : ⟨ isL a ⟩) (oa : IsOrd a) (carda : IsCardinalL (a , la))
            (a∉ω : ⟨ a ∈ˢ ω ⟩ → Empty.⊥) where
```

以 `κ` 表示底层序数为 `a` 的可构造集合。这样，在形成内部构造时，外围序数数据与其属于 `L` 的证明始终成对出现。

```agda
  κ : S
  κ = a , la
```

现在考察带有 Gödel 序的 `κ × κ`，以及将该良序塌缩所得的序数。目标是证明这一塌缩的每个初始段仍在 `κ` 以下有界。

```agda
  open Order κ oa
  open Coll κ oa
```

由于序数 `a` 不是有限序数，它包含每个有限序数。还需证明它对后继封闭：给定 `m ∈ a`，三歧性将 `sucV m` 置于 `a` 以下、等于 `a` 或高于 `a`；接下来的分类将排除后两种可能。

```agda
  ω⊆a : (z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ a ⟩
  ω⊆a = ω⊆ a oa a∉ω
  suc∈ : (m : V ℓ) → ⟨ m ∈ˢ a ⟩ → ⟨ sucV m ∈ˢ a ⟩
  suc∈ m m∈a = go (ord-tri (sucV m) (suc-ord om) a oa)
    where
```

由于 `m` 是序数 `a` 的成员，`m` 本身也是序数。又因 `m` 属于可构造集合 `a`，它也是可构造的，因而确定内部论域中的元素 `mL`。

```agda
    om : IsOrd m
    om = mem-ord {A = a} oa m m∈a
    mL : S
    mL = ordL m om
```

对 `sucV m` 与 `a` 应用三歧性。第一种情形正是所需的隶属关系。若 `sucV m = a`，再比较 `m` 与 `ω`，便把矛盾分成有限情形和接下来处理的两种无穷情形。

```agda
    go : ⟨ sucV m ∈ˢ a ⟩ ⊎ ((sucV m ≡ a) ⊎ ⟨ a ∈ˢ sucV m ⟩) → ⟨ sucV m ∈ˢ a ⟩
    go (inl h) = h
    go (inr (inl e)) = Empty.rec (fin (ord-tri m om ω ω-ord))
      where
      fin : ⟨ m ∈ˢ ω ⟩ ⊎ ((m ≡ ω) ⊎ ⟨ ω ∈ˢ m ⟩) → Empty.⊥
```

若 `m` 属于 `ω`，则其后继也属于 `ω`，从而把基数 `a` 放进 `ω`，与无穷性假设矛盾。若 `m` 等于 `ω` 或包含 `ω`，则在成员 `m` 处施用 `a` 的内部基数性，便会反驳移位单射 `sucʟ mL ↪ mL`，后者是到该基数某个成员的内部单射。

```agda
      fin (inl m∈ω) = a∉ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) e (ω-limit m m∈ω))
      fin (inr r) =
        carda mL m∈a (subst (λ w → InjL w mL) sucL≡κ (Shift.injL mL om m∉ω))
        where
        m∉ω : ⟨ m ∈ˢ ω ⟩ → Empty.⊥
```

局部非有限性由同一三歧性读出：若 `m` 等于 `ω`，所假设的隶属会把 `ω` 放进其自身；若 `ω` 属于 `m`，传递性同样会把 `ω` 放进其自身。两者都与隶属的非自反性矛盾。

```agda
        m∉ω h = rr r
          where
          rr : (m ≡ ω) ⊎ ⟨ ω ∈ˢ m ⟩ → Empty.⊥
          rr (inl e') = ∈-irrefl ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) e' h)
          rr (inr ω∈m) = ∈-irrefl ω (ω-ord .fst ω∈m h)
```

等式 `sucV m = a` 将内部后继 `sucʟ mL` 与 `κ` 认同，于是移位会给出基数性所禁止的、从 `κ` 到 `m` 的单射。在三歧性的余下情形中，`a ∈ sucV m` 意味着 `a ∈ m` 或 `a = m`；两种选择都会导出某个序数属于自身，因而都不可能。

```agda
        sucL≡κ : sucʟ mL ≡ κ
        sucL≡κ = Σ≡Prop (λ v → snd (isL v)) (sucʟ-fst mL ∙ e)
    go (inr (inr h)) = Empty.rec*
      (∈sucV-elim {A = m} {x = a} {P = Empty.⊥* {ℓ-suc ℓ}} Empty.isProp⊥* h
        (λ a∈m → lift (∈-irrefl a (oa .fst a∈m m∈a)))
```

有了后继封闭性，便可在下文所需的较小序数处使用归纳假设。更一般地，若无穷序数 `γ` 位于 `a` 以下，就为 `γ` 选取一个内部基数代表；在该代表处使用归纳假设，将得到单射 `prodL γ ↪ γ`。

```agda
        (λ a≡m → lift (∈-irrefl m (subst (λ w → ⟨ m ∈ˢ w ⟩) a≡m m∈a))))
  prod-into : (γ : S) → IsOrd (fst γ) → ⟨ fst γ ∈ˢ a ⟩
            → (⟨ fst γ ∈ˢ ω ⟩ → Empty.⊥) → InjL (prodL γ) γ
  prod-into γ oγ γ∈a γ∉ω = PT.rec squash₁ build (cardOf γ oγ)
    where
```

基数代表以截断形式交付其数据：序数 `μ` 是内部基数、包含于 `γ`，且 `γ` 单射入它、它单射入 `γ`。函数 `build` 把这些数据变成乘积单射。

```agda
    build : Σ[ μ ∈ S ]
              ( IsOrd (fst μ) × IsCardinalL μ
              × ((z : V ℓ) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst γ ⟩)
              × InjL γ μ × InjL μ γ )
          → InjL (prodL γ) γ
```

该单射复合三条单射。乘积单射把 `γ ↪ μ` 逐坐标提升；归纳假设施用于内部基数 `μ`，给出 `prodL μ ↪ μ`；再经 `μ ↪ γ` 把结果复合回 `γ`。

```agda
    build (μ , oμ , cardμ , μ⊆γ , γ↪μ , μ↪γ) =
      injl-trans (prodL γ) (prodL μ) γ (prod-inj γ μ γ↪μ)
        (injl-trans (prodL μ) μ γ (ih (fst μ) μ∈a (snd μ) oμ cardμ μ∉ω) μ↪γ)
      where
      μ∈a : ⟨ fst μ ∈ˢ a ⟩
```

代表 `μ` 同样位于 `a` 以下。若 `μ ∈ γ`，传递性结合 `γ ∈ a` 即得 `μ ∈ a`；若 `μ = γ`，直接搬运隶属关系即可。余下的比较 `γ ∈ μ` 不可能成立，因为包含关系 `μ ⊆ γ` 会由此给出 `γ ∈ γ`。

```agda
      μ∈a = go (ord-tri (fst μ) oμ (fst γ) oγ)
        where
        go : ⟨ fst μ ∈ˢ fst γ ⟩ ⊎ ((fst μ ≡ fst γ) ⊎ ⟨ fst γ ∈ˢ fst μ ⟩) → ⟨ fst μ ∈ˢ a ⟩
        go (inl h)       = oa .fst h γ∈a
        go (inr (inl e)) = subst (λ w → ⟨ w ∈ˢ a ⟩) (sym e) γ∈a
```

代表 `μ` 也必须是无穷的。若 `μ ∈ ω`，先用无穷序数 `γ` 所给出的 `ω ↪ γ`，再复合 `γ ↪ μ`，便会将 `ω` 单射入有限序数 `μ`，这是不可能的。为后文使用，`Seg p b` 记录一个满足 `r ≺ p` 且塌缩值为 `b` 的前驱 `r`。

```agda
        go (inr (inr h)) = Empty.rec (∈-irrefl (fst γ) (μ⊆γ (fst γ) h))
      μ∉ω : ⟨ fst μ ∈ˢ ω ⟩ → Empty.⊥
      μ∉ω h = no-fin γ μ oγ γ∉ω oμ h γ↪μ
  Seg : OT.Dom → V ℓ → Type (ℓ-suc ℓ)
  Seg p b = Σ[ r ∈ OT.Dom ] ((r OT.≺ p) × (C.col r ≡ b))
```

节段唯一：塌缩值相等的 `p` 的两个前驱相等，因为塌缩映射在索引上是单射的；这一命题被一次性记录，供后续消去使用。

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

塌缩值的每个成员都由塌缩的外向读法与刚证明的唯一性确定其节段。随后给出对的 maximum：其两个坐标在宿主序中的较大者。

```agda
  seg : (p : OT.Dom) (b : V ℓ) → ⟨ b ∈ˢ C.col p ⟩ → Seg p b
  seg p b h = PT.rec (isPropSeg p b) (λ z → z) (C.col-out p b h)
  mx : OT.Dom → ⟪ K ⟫
  mx p = maxOrd (φ p .fst) (φ p .snd)
```

令 `mV p` 为 `p` 的两个坐标之最大值所表示的外围序数。若在塌缩后的 Gödel 序中 `r ≺ p`，则 `r` 的第一坐标位于该最大值的后继之下；这正是 Gödel 序对第一坐标给出的界。

```agda
  mV : OT.Dom → V ℓ
  mV p = ↑ (mx p)
  opaque
    seg-fst : (p r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .fst) ∈ˢ sucV (mV p) ⟩
    seg-fst p r k = fst∈suc (φ r) (φ p) (≺-fwd r p k)
```

每个 `r ≺ p` 的第二坐标也满足同一上界。因此取 `gfin p = sucV (mV p)` 作为两个坐标的共同载体；在有限情形的假设 `mV p ∈ ω` 下，该载体本身也是有限序数。

```agda
    seg-snd : (p r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .snd) ∈ˢ sucV (mV p) ⟩
    seg-snd p r k = snd∈suc (φ r) (φ p) (≺-fwd r p k)
  gfin : OT.Dom → V ℓ
  gfin p = sucV (mV p)
  opaque
```

对每个前驱 `r ≺ p`，两个坐标界分别在 `gfin p` 的呈现中选出一个索引；`h p r` 就是这两个索引组成的有序对。当 `mV p` 有限时，该有序对把 `r` 编码到一个有限序数的平方中。

```agda
    h : (p r : OT.Dom) (k : r OT.≺ p) → ⟪ gfin p ⟫ × ⟪ gfin p ⟫
    h p r k = fiber (gfin p) (seg-fst p r k) .fst , fiber (gfin p) (seg-snd p r k) .fst
```

若两个编码 `h p r` 与 `h p r'` 相等，对该等式应用第一投影便得到第一索引相等。这是从编码恢复 `r` 的两个坐标的第一步。

```agda
    h-fst : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
          → h p r k ≡ h p r' k'
          → fiber (gfin p) (seg-fst p r k) .fst
          ≡ fiber (gfin p) (seg-fst p r' k') .fst
    h-fst p r r' k k' e = cong fst e
```

对同一个编码等式应用第二投影，同样得到第二索引相等。因此，纤维对的相等分别控制了两个分量。

```agda
    h-snd : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
          → h p r k ≡ h p r' k'
          → fiber (gfin p) (seg-snd p r k) .fst
          ≡ fiber (gfin p) (seg-snd p r' k') .fst
    h-snd p r r' k k' e = cong snd e
```

第一纤维索引相等蕴含这些纤维所表示的外围序数相等。由于 `K` 的呈现映射是单射，第一坐标 `φ r .fst` 与 `φ r' .fst` 因而相等。

```agda
  step-e1 : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
          → h p r k ≡ h p r' k' → φ r .fst ≡ φ r' .fst
  step-e1 p r r' k k' e =
    ↪-inj {a = K} (fiber-inj (gfin p) (seg-fst p r k) (seg-fst p r' k') (h-fst p r r' k k' e))
```

第二条传递引理对第二坐标做同样的事，于是纤维对的相等同时确定底层对的两个坐标，这正是塌缩的有限情形所需要的。

```agda
  step-e2 : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
          → h p r k ≡ h p r' k' → φ r .snd ≡ φ r' .snd
  step-e2 p r r' k k' e =
    ↪-inj {a = K} (fiber-inj (gfin p) (seg-snd p r k) (seg-snd p r' k') (h-snd p r r' k k' e))
```

两个纤维对编码相等，就会使 `φ r` 与 `φ r'` 的两个坐标分别相等。对的外延性把两条坐标等式合成起来，再由 `φ` 的单射性得到 `r = r'`。因此，对 `p` 的前驱所作的编码是单射。待证的有限情形是：若 `p` 的最大坐标属于 `ω`，则 `C.col p` 也属于 `ω`。

```agda
  step-inj : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
           → h p r k ≡ h p r' k' → r ≡ r'
  step-inj p r r' k k' e =
    φ-inj r r' (pair≡ (step-e1 p r r' k k' e) (step-e2 p r r' k k' e))
  col-fin : (p : OT.Dom) → ⟨ mV p ∈ˢ ω ⟩ → ⟨ C.col p ∈ˢ ω ⟩
```

证明用三歧性比较塌缩值与 `ω`，并先点名其有限载体：`g` 是 `p` 的外围最大值的后继，即已证明容纳每个前驱两个坐标的那个集合。

```agda
  col-fin p m∈ω = go (ord-tri (C.col p) (C.col-ord p) ω ω-ord)
    where
    g : V ℓ
    g = sucV (mV p)
    og : IsOrd g
```

由 `mV p ∈ ω` 可知这个最大值是序数，其后继 `g` 也仍是序数。`ω` 的极限性质给出 `g ∈ ω`，所以 `g` 是有限序数。这些条件恰好可以用来排除从 `ω` 到 `g × g` 的单射。

```agda
    og = suc-ord (ω-mem-ord (mV p) m∈ω)
    g∈ω : ⟨ g ∈ˢ ω ⟩
    g∈ω = ω-limit (mV p) m∈ω
```

反驳假设 `ω` 包含于塌缩值。于是 `ω` 的每个索引都指名 `col p` 的一个节段：包含关系把被指名的成员放进塌缩之内，而节段引理恢复出相应的前驱。

```agda
    refute : ((z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ C.col p ⟩) → Empty.⊥
    refute sub = finite-excl-ω g og g∈ω f f-inj
      where
      s : (x : ⟪ ω ⟫) → Seg p (⟪ ω ⟫↪ x)
      s x = seg p (⟪ ω ⟫↪ x) (sub (⟪ ω ⟫↪ x) (member ω x))
```

对每个 `x ∈ ω`，令 `s x` 为 `p` 的唯一前驱，并使其塌缩值等于 `x`。映射 `f` 把 `x` 送到编码该前驱两个坐标的纤维索引对，因而送到有限平方 `g × g` 的一个元素。还需证明这样的编码若相等，原来的两个 `ω` 中元素也相等。

```agda
      f : ⟪ ω ⟫ → ⟪ g ⟫ × ⟪ g ⟫
      f x = h p (s x .fst) (s x .snd .fst)
      f-inj : (x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y
      f-inj x y e = ↪-inj {a = ω}
        (sym (s x .snd .snd)
```

单射性由三条等式复合而成：`x` 的节段的塌缩值等于 `x`，两个节段作为前驱由刚证明的有限情形单射相等，`y` 的节段的塌缩值等于 `y`。复合起来便迫使 `x` 与 `y` 一致。

```agda
         ∙ cong C.col (step-inj p (s x .fst) (s y .fst) (s x .snd .fst) (s y .snd .fst) e)
         ∙ s y .snd .snd)
```

三歧性现在给出 `C.col p ∈ ω`。若 `C.col p = ω`，便会得到已被排除的包含 `ω ⊆ C.col p`；若 `ω ∈ C.col p`，序数 `C.col p` 的传递性也会给出同一包含。为构造一般的逆塌缩，固定一个前驱上界 `p` 和一个可构造载体 `g`。

```agda
    go : ⟨ C.col p ∈ˢ ω ⟩ ⊎ ((C.col p ≡ ω) ⊎ ⟨ ω ∈ˢ C.col p ⟩) → ⟨ C.col p ∈ˢ ω ⟩
    go (inl k)         = k
    go (inr (inl e))   = Empty.rec (refute (λ z z∈ω → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈ω))
    go (inr (inr ω∈c)) = Empty.rec (refute (λ z z∈ω → C.col-ord p .fst z∈ω ω∈c))
  module Inv (p : OT.Dom) (g : S)
```

假设对每个 `r ≺ p`，`φ r` 所表示的两个坐标都属于 `g` 的载体。这两条界保证 `r` 所表示的对属于内部乘积 `prodL g`，而该乘积正是逆塌缩的陪域。

```agda
             (bfst : (r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .fst) ∈ˢ fst g ⟩)
             (bsnd : (r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .snd) ∈ˢ fst g ⟩) where
```

塌缩值的每个成员 `x` 都确定其节段：由于节段唯一，截断的隶属被消去，给出一个前驱 `r`，其塌缩值正是 `x` 的底层集合。

```agda
    private
      pre : (x : S) → ⟨ fst x ∈ˢ C.col p ⟩ → Σ[ r ∈ OT.Dom ] (C.col r ≡ fst x)
      pre x mx = seg p (fst x) mx .fst , seg p (fst x) mx .snd .snd
```

对由 `x ∈ C.col p` 选出的前驱 `r`，呈现等式把 `OT.↪ r` 认同为 `φ r` 所表示的两个坐标组成的有序对。因此，证明它属于 `prodL g` 归结为两条坐标界；`bfst` 给出第一条。

```agda
      bound : (x : S) (mx : ⟨ fst x ∈ˢ C.col p ⟩) → ⟨ OT.↪ (pre x mx .fst) ∈ˢ fst (prodL g) ⟩
      bound x mx = subst (λ w → ⟨ w ∈ˢ fst (prodL g) ⟩) (sym (φ-eq (seg p (fst x) mx .fst)))
        (prodL-in g (upK (φ (seg p (fst x) mx .fst) .fst))
                    (upK (φ (seg p (fst x) mx .fst) .snd))
                    (bfst _ (seg p (fst x) mx .snd .fst))
```

`bsnd` 给出第二坐标的隶属关系。两条界合在一起，把所表示的有序对放入 `g × g`，从而完成所需的陪域证明。

```agda
                    (bsnd _ (seg p (fst x) mx .snd .fst)))
```

因此，`p` 以下初始段上的塌缩具有一个到 `prodL g` 的可定义逆映射：`C.col p` 的每个成员都回到其唯一前驱，不同的塌缩值则回到不同的对。由此得到内部单射 `C.colʟ p ↪ prodL g`。主归纳现在要对每个 `p` 证明 `C.col p ∈ a`，首先对它的最大坐标应用三歧性。

```agda
    open I.Inverse (C.colʟ p) (prodL g) pre bound public
      using ( fn; graph; at; only; M; inj; injL ) renaming ( SourceMem to Mem )
  colIn : (p : OT.Dom) → ⟨ C.col p ∈ˢ a ⟩
  colIn p = go (ord-tri (mV p) (ord↑ (mx p)) ω ω-ord)
    where
```

若该对的最大值有限，则由有限情形塌缩值有限，而 `ω` 含于 `a` 使其落入 `a`。否则最大值无穷，转而检查塌缩值与 `a` 之间的三歧性。

```agda
    go : ⟨ mV p ∈ˢ ω ⟩ ⊎ ((mV p ≡ ω) ⊎ ⟨ ω ∈ˢ mV p ⟩) → ⟨ C.col p ∈ˢ a ⟩
    go (inl m∈ω) = ω⊆a (C.col p) (col-fin p m∈ω)
    go (inr inf) = go' (ord-tri (C.col p) (C.col-ord p) a oa)
      where
      m∉ω : ⟨ mV p ∈ˢ ω ⟩ → Empty.⊥
```

在无穷分支中，反设 `mV p ∈ ω`。若 `mV p = ω`，沿该等式搬运此隶属关系便得到 `ω ∈ ω`；若 `ω ∈ mV p`，则 `ω` 的传递性把这两条隶属关系合成，再次得到 `ω ∈ ω`。非自反性排除两种选择，故 `mV p` 不是有限序数。

```agda
      m∉ω h = rr inf
        where
        rr : (mV p ≡ ω) ⊎ ⟨ ω ∈ˢ mV p ⟩ → Empty.⊥
        rr (inl e)   = ∈-irrefl ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) e h)
        rr (inr ω∈m) = ∈-irrefl ω (ω-ord .fst ω∈m h)
```

载体 `g` 是最大值的后继，由于最大值是序数 `κ` 的成员，故 `g` 是序数；随后该序数被打包为 `L` 的元素 `gL`。

```agda
      g : V ℓ
      g = sucV (mV p)
      og : IsOrd g
      og = suc-ord (ord↑ (mx p))
      gL : S
```

载体由前证的后继封闭性属于 `a`，且它是无穷的：若 `g` 属于 `ω`，则作为 `g` 成员的最大值经传递性也属于 `ω`，与刚才确立的无穷性矛盾。

```agda
      gL = ordL g og
      g∈a : ⟨ g ∈ˢ a ⟩
      g∈a = suc∈ (mV p) (member K (mx p))
      g∉ω : ⟨ g ∈ˢ ω ⟩ → Empty.⊥
      g∉ω h = m∉ω (ω-ord .fst (self∈sucV (mV p)) h)
```

对每个 `r ≺ p`，界 `seg-fst` 与 `seg-snd` 都把 `r` 的两个坐标放入 `g = sucV (mV p)`。因此，逆塌缩构造给出从 `C.colʟ p` 到 `prodL gL` 的内部单射。

```agda
      module IV = Inv p gL (seg-fst p) (seg-snd p) using (injL)
```

把逆塌缩单射与 `prod-into gL` 复合，便得到 `C.colʟ p ↪ gL`。后一个单射并非直接在 `gL` 处使用归纳假设：`prod-into` 先为 `gL` 选取内部基数代表 `μ`，在 `μ` 处应用归纳假设，再沿 `μ` 与 `gL` 之间的单射搬运所得的平方单射。

```agda
      col↪g : InjL (C.colʟ p) gL
      col↪g = injl-trans (C.colʟ p) (prodL gL) gL IV.injL (prod-into gL og g∈a g∉ω)
      absurd : ((z : V ℓ) → ⟨ z ∈ˢ a ⟩ → ⟨ z ∈ˢ C.col p ⟩) → Empty.⊥
      absurd sub = carda gL g∈a
        (injl-trans κ (C.colʟ p) gL (inclusion-coded κ (C.colʟ p) sub) col↪g)
```

若基数包含于塌缩值，则把该包含与到 `gL` 的单射复合，将使 `κ` 单射入其自身成员 `gL`，与 `κ` 的内部基数性矛盾。于是塌缩值与 `a` 的三歧性只剩直接隶属一种情形。

```agda
      go' : ⟨ C.col p ∈ˢ a ⟩ ⊎ ((C.col p ≡ a) ⊎ ⟨ a ∈ˢ C.col p ⟩) → ⟨ C.col p ∈ˢ a ⟩
      go' (inl h)       = h
      go' (inr (inl e)) = Empty.rec (absurd (λ z z∈a → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈a))
      go' (inr (inr h)) = Empty.rec (absurd (λ z z∈a → C.col-ord p .fst z∈a h))
  result : InjL (prodL κ) κ
```

乘积先单射入塌缩序型 `C.otL`。该序型的每个成员 `z` 都等于某个 `b : OT.Dom` 的 `C.col b`，而 `colIn b` 把这个塌缩值放入 `a`；因此 `C.otL ⊆ κ`。把第一个单射与这一编码包含复合，便得到所需的内部单射 `prodL κ ↪ κ`。

```agda
  result = injl-trans P C.otL κ injL-ot (inclusion-coded C.otL κ ot⊆a)
    where
    ot⊆a : (z : V ℓ) → ⟨ z ∈ˢ fst C.otL ⟩ → ⟨ z ∈ˢ a ⟩
    ot⊆a z hz = PT.rec (snd (z ∈ˢ a))
      (λ { (b , e) → subst (λ w → ⟨ w ∈ˢ a ⟩) e (colIn b) }) (C.otL-out z hz)
```

现在由隶属关系上的良基归纳证明平方律。给定一个作为内部基数并满足 `ω ∈ κ` 的序数 `κ`，只要补上 `κ` 不是有限序数的证明，上面构造的归纳步骤就给出内部单射 `prodL κ ↪ κ`。

```agda
square-law-L :
    (κ : S) → IsOrd (fst κ) → IsCardinalL κ → ⟨ ω ∈ˢ fst κ ⟩
  → InjL (prodL κ) κ
square-law-L κ oκ cκ ω∈κ =
  WF.WFI.induction regularityV {P = Goal} Step.result (fst κ) (snd κ) oκ cκ
```

最后，`κ` 不可能属于 `ω`。否则，序数 `ω` 的传递性会把 `ω ∈ κ` 与 `κ ∈ ω` 合成，得到 `ω ∈ ω`，与非自反性矛盾。这就满足了归纳步骤所需的无穷性假设。

```agda
    (λ κ∈ω → ∈-irrefl ω (ω-ord .fst ω∈κ κ∈ω))
```