Bedrock把后继基数单射到幂集
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图L 内部的 Cantor 定理排除了从 𝒫 κ 到 κ 的内部编码单射。本章从 κ 的后继基数 δ 以及另行给出的比较 InjL (𝒫 κ) δ 出发，构造反方向的比较 InjL δ (𝒫 κ)。这里，InjL a b 是「存在一张 L 中的图，编码从 a 到 b 的单射」的命题截断。证明先把 δ 上的序数次序沿给定单射拉回到 𝒫 κ，再把所得次序塌缩为序数 μ，最后用 Cantor 障碍证明 μ 不可能属于 δ。
{-# OPTIONS --cubical --safe --guardedness #-}
经典推理通过显式参数 lem 引入。序数三歧性给出证明中可见的分类讨论，而这里使用的分离定理与编码单射结果也以同一个假设实例化。因此，本章把经典依赖统一记录在一处。
open import Base.Prelude open import Base.Classical using ( LEM )
排中律假设取在 ℓ-suc ℓ，相关的集合命题与编码图命题正位于这一层级。因此，下文每次经典比较都可追溯到这个参数。
module L.GCH.SuccessorIntoPowerSet {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
对角子集与稍后的拉回序都必须是 L 中的集合，因此二者都由在可构造模型中解释的一阶公式描述。这里的语法可表达隶属、合取、否定，以及描述这些关系所需的有界或无界存在见证。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_; ¬̇_; ∃̇_; ∃̇∈ ) import FOL.ZFModel import FOL.Absoluteness
为证明拉回序良基，证明把它的每个下降步骤送到外围累积层级中的一个隶属步骤，再在那里应用正则性。关于可构造序数的事实随后把序数以下的隶属转化为比较所需的序数结构。
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV ) open import V.Coding {ℓ} using ( pr ) open import L.Constructible {ℓ} using ( 𝒮ʟ; IsOrd; isL; isL-trans; isTransV; isPropIsTransV ) open import L.Ordinal {ℓ} using ( mem-ord )
内部大小比较分为两个层次。InjCode F a b 保留一张特定的可构造图及其单射律，而 InjL a b 只保留这种码存在的命题截断。后继基数的最小性、编码包含与单射复合使证明能够组合这些比较，而不暴露一张全局选定的图。
open import L.Ordinal.Linear {ℓ} lem using ( Tri; ord-tri ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL ) open import L.Cardinal {ℓ} lem using ( InjCode; InjL; SuccCardL ) open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate; inclusion-coded; injl-trans; module Relation ) open import L.Coding.Model {ℓ} using ( svAt-out; domAt-in )
前面的两项结果控制最终比较。每个严格低于后继基数 δ 的序数都可单射到其基数 κ；另一方面，编码良序可以塌缩为可构造序数，并得到通往塌缩像及从塌缩像返回的编码映射。第三项材料 InjL (𝒫 κ) δ 是本章条件定理的假设，不能仅由后继基数记录推出。
open import L.Coding.Injection {ℓ} lem using ( injAt-out ) open import L.GCH.BelowSuccessorCardinal {ℓ} lem using ( below-succ-injects ) open import L.GCH.Assembly {ℓ} lem using ( SuccIntoPower ) open import L.DefinableInjection {ℓ} lem using ( module Inj ) open import L.GCH.OrderType {ℓ} lem using ( Holds; module Code )
下文若干等式要认同第二分量为证明的依值对。由于这些证明分量都是命题，只需证明底层集合相等；随后便可沿所得同一视搬运隶属与图成立的事实。
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× ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
可达性记录表达拉回序所需的良基递归。命题截断在全章中表达仅仅存在；每次从中消去时，目标始终是命题，例如空类型或另一个 InjL 陈述。
import Cubical.Induction.WellFounded as WF open WF using ( Acc; acc; WellFounded ) import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
应用正则性与传递性时，底层集合的隶属在外围层级中读取。这个外围关系必须与「连同可构造性证明打包的元素」之间的隶属相区分。
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
以 SV.S 表示外围集合。当逐点包含等陈述直接量化累积层级中的底层对象时，就使用这个论域。
module SV = hPropStructure 𝒮ᵥ using ( S )
以 SL.S 表示集合连同其可构造性证书。内部幂集、后继基数谓词与编码单射关系都以这个论域中的元素为参数。
module SL = hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )
L 上的 ZF 结构确定其内部幂集。相应规格把 𝒫 κ 中的隶属与内部子集关系等同起来，其中量化范围是可构造模型的元素。
module ModelL = FOL.ZFModel 𝒮ʟ using ( isZFModel; module isZFModel; ℩-spec )
对象语言公式将在可构造集合组成的环境中求值。绝对性给出语义读法，把这些满足陈述与证明所用的宿主层谓词连接起来。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ ) open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
SL.S 的元素由底层集合与可构造性证明组成。由于可构造性是命题，底层集合的相等可提升为 SL.S 中的相等，无须另行选择证书之间的相等。
S≡ : {x y : SL.S} → fst x ≡ fst y → x ≡ y S≡ = Σ≡Prop (λ v → snd (isL v))
内部子集属于模型的幂集
第一个构造把逐点的内部包含转化为模型幂集中的隶属。它适用于任意可构造集合 κ 与 y：若 y 的每个可构造元素都属于 κ，则 y 是 κ 的内部子集，因而属于 𝒫 κ。
into-power : (zf : ModelL.isZFModel) (κ y : SL.S) → ((z : SL.S) → ⟨ fst z ∈ˢ fst y ⟩ → ⟨ fst z ∈ˢ fst κ ⟩) → ⟨ fst y ∈ˢ fst (ModelL.isZFModel.𝒫 zf κ) ⟩ into-power zf κ y sub =
幂集规格断言：y 属于 𝒫 κ，当且仅当逐点的内部子集条件成立。沿这一等价改写后，目标恰好就是已经给出的包含证明。
subst ⟨_⟩ (sym (ModelL.℩-spec (hasPower κ) y)) sub where open ModelL.isZFModel zf using ( hasPower )
L 内部的 Cantor 对角论证
现在固定任意可构造集合 κ，并对它的模型幂集证明内部 Cantor 障碍。这一部分不需要假设 κ 是基数或无穷集。
module Cantor (zf : ModelL.isZFModel) (κ : SL.S) where
在整个对角论证中，𝒫 κ 指固定的 L 上 ZF 模型所给出的幂集。因此，它的成员恰是该模型内部所识别的子集。
open ModelL.isZFModel zf using ( 𝒫 )
对角论证针对一条显式给定的图 F 及其编码展开。后文一切陈述都只关于这条固定的图。
module Diag (F : SL.S) (code : InjCode F (𝒫 κ) κ) where
图的环境把图与其全域所及的幂集配对。
γF : SL.S ^ 2 γF = F ∷ 𝒫 κ ∷ []
编码的值域条款说：图记录的每个值都属于 κ。
ranF : (x y : SL.S) → Holds F x y → ⟨ fst y ∈ fst κ ⟩ ranF = code .snd .snd .snd
全域性条款断言：𝒫 κ 的每个成员在 F 下都有某个值。值的见证仍处于命题截断之下，因此这里只给出存在性，而不全局选定一个值。
valF : (x : SL.S) → ⟨ fst x ∈ fst (𝒫 κ) ⟩ → ∥ Σ[ y ∈ SL.S ] Holds F x y ∥₁ valF = domAt-in zero (suc zero) γF (code .snd .fst)
单射性条款由值恢复输入：记录值相同的两个成员，其底层集合相等。
injF : (y x x' : SL.S) → Holds F x y → Holds F x' y → fst x ≡ fst x' injF = injAt-out zero γF (code .snd .snd .fst)
对角谓词说：仅仅地存在幂集的某个成员 A，其被记录的值等于 ξ，而 ξ 不属于 A。存在是截断的；并不选定这样的集合。
Diagonal : SL.S → Type (ℓ-suc ℓ) Diagonal ξ = ∥ Σ[ A ∈ SL.S ] ( ⟨ fst A ∈ fst (𝒫 κ) ⟩ × Holds F A ξ × (⟨ fst ξ ∈ fst A ⟩ → Empty.⊥) ) ∥₁
应用原子的满足，依应用编码的充分性，字面上就是宿主层图成立。
private a1 : (ξ A : SL.S) → ⟨ (A ∷ ξ ∷ []) ⊨ appC F zero (suc zero) ⟩ ≡ Holds F A ξ a1 ξ A = cong ⟨_⟩ (appC-adequate F zero (suc zero) (A ∷ ξ ∷ []))
定义对角条件的公式在 𝒫 κ 内寻找集合 A，使 F 记录配对 (A, ξ)，且 ξ 不属于 A。有界量词准确记录见证是 κ 的内部子集；随后在 κ 上应用分离，得到所有满足这一条件的 ξ∈κ 所组成的集合。
opaque φD : Formula SL.S 1 φD = ∃̇∈ (con (𝒫 κ)) (appC F zero (suc zero) ∧̇ ¬̇ (var (suc zero) ∈̇ var zero))
应用编码的充分性把「将 F 应用于 A」这一公式原子与语义陈述 Holds F A ξ 认同起来。正是这条等式使下文能够在两个方向上互换使用对角公式与编码图。
φD-out : (ξ : SL.S) → ⟨ (ξ ∷ []) ⊨ φD ⟩ → Diagonal ξ φD-out ξ = PT.map (λ { (A , (mA , (h , n))) → A , mA , transport (a1 ξ A) h , (λ k → lower (n k)) })
反过来，给定 A ∈ 𝒫 κ、图事实 Holds F A ξ 与 ξ ∉ A 的证明，就可满足对角公式。这些数据被封装在公式的有界存在量化所带的命题截断中。
φD-in : (ξ A : SL.S) → ⟨ fst A ∈ fst (𝒫 κ) ⟩ → Holds F A ξ → (⟨ fst ξ ∈ fst A ⟩ → Empty.⊥) → ⟨ (ξ ∷ []) ⊨ φD ⟩ φD-in ξ A mA h n = ∣ A , (mA , (transport (sym (a1 ξ A)) h , (λ k → lift (n k)))) ∣₁
对角集合由该有界公式从 κ 中分离而出。
D₀ : SL.S D₀ = fst (fst (hasSeparationL κ φD))
其隶属规格即分离自身的读法：属于对角集合，当且仅当属于 κ 且满足对角公式。
D₀-spec : (ξ : SL.S) → (ξ SL.∈ˢ D₀) ≡ ((ξ SL.∈ˢ κ) ⊓ ((ξ ∷ []) ⊨ φD)) D₀-spec = snd (fst (hasSeparationL κ φD))
对角集合是内部幂集的成员：逐点读取证明其每个模型元素都属于 κ。
D₀∈𝒫κ : ⟨ fst D₀ ∈ fst (𝒫 κ) ⟩ D₀∈𝒫κ = into-power zf κ D₀ (λ z h → fst (subst ⟨_⟩ (D₀-spec z) h))
为导出矛盾，假设图把对角集合 D₀ 映到某个值 ξ。值域条款将给出 ξ ∈ κ，而 D₀ 的定义将同时迫使 ξ ∈ D₀ 与 ξ ∉ D₀。
absurd : Σ[ ξ ∈ SL.S ] Holds F D₀ ξ → Empty.⊥ absurd (ξ , h₀) = out inside where
假设 ξ ∈ D₀。对角公式便在命题截断下给出集合 A ∈ 𝒫 κ，使 F 把 A 映到 ξ，且 ξ ∉ A。由于 F 也把 D₀ 映到 ξ，单射性认同 A 与 D₀ 的底层集合；把所假设的隶属搬运到 A 中，便与 ξ ∉ A 矛盾。
out : ⟨ fst ξ ∈ fst D₀ ⟩ → Empty.⊥ out hm = PT.rec Empty.isProp⊥ (λ { (A , _ , hA , n) → n (subst (λ w → ⟨ fst ξ ∈ w ⟩) (injF ξ D₀ A h₀ hA) hm) }) (φD-out ξ (snd (subst ⟨_⟩ (D₀-spec ξ) hm)))
反方向把刚才的反驳作为数据使用。值域条款给出 ξ ∈ κ；取 A = D₀，再用 F 把 D₀ 映到 ξ 以及前一步证明的 ξ ∉ D₀，即可见证对角公式。分离规格于是给出 ξ ∈ D₀，再把反驳应用于它便得到矛盾。
inside : ⟨ fst ξ ∈ fst D₀ ⟩ inside = subst ⟨_⟩ (sym (D₀-spec ξ)) (ranF D₀ ξ h₀ , φD-in ξ D₀ D₀∈𝒫κ h₀ out)
两半反驳任何从幂集到 κ 的内部编码单射：该单射被消去为图，而图在对角集处的值被消去为矛盾。目标是空类型，故两次消去都合法。
no-inj : InjL (𝒫 κ) κ → Empty.⊥ no-inj = PT.rec Empty.isProp⊥ step where step : Σ[ F ∈ SL.S ] InjCode F (𝒫 κ) κ → Empty.⊥ step (F , code) = PT.rec Empty.isProp⊥ D.absurd (D.valF D.D₀ D.D₀∈𝒫κ)
对所选图 F，对角构造同时给出内部子集 D₀，并证明图不可能为它指派任何值。然而全域性仍为它指派一个值，于是这张图导致矛盾。
where module D = Diag F code
良序化幂集并比较其序型
为构造反方向比较，固定 κ 的后继基数 δ，并固定一张编码所假设单射 𝒫 κ ↪ δ 的具体图 G。这张图只在从命题截断取得的局部分支内可用；最终结果仍将是一个 InjL 陈述。
module Build (zf : ModelL.isZFModel) (κ δ : SL.S) (sc : SuccCardL δ κ) (G : SL.S) (code : InjCode G (ModelL.isZFModel.𝒫 zf κ) δ) where
这里的源 𝒫 κ 仍是固定 ZF 模型所确定的内部幂集。构造始终不会把它换成底层集合的外围幂集。
open ModelL.isZFModel zf using ( 𝒫 )
后继的序数性是其记录的第一分量。
ordδ : IsOrd (fst δ) ordδ = sc .fst
幂集被命名为比较的源。
P : SL.S P = 𝒫 κ
图的环境把图与幂集配对。
γG : SL.S ^ 2 γG = G ∷ P ∷ []
编码的值域条款说：每个值都落在后继中。
ranG : (x y : SL.S) → Holds G x y → ⟨ fst y ∈ fst δ ⟩ ranG = code .snd .snd .snd
单值性针对同一个固定输入：若 G 同时记录 G(x)=y 与 G(x)=y'，则 y 与 y' 的底层集合相等。这一唯一性将使 x 的可能值所组成的类型成为命题。
svG : (x y y' : SL.S) → Holds G x y → Holds G x y' → fst y ≡ fst y' svG = svAt-out zero γG (code .fst)
全域性为每个 x ∈ P 给出经过命题截断的值见证，此时尚未选定一个值。稍后，单值性将证明可能值组成的纤维是命题，从而可以从这层命题截断消去并在局部读出值。
valG : (x : SL.S) → ⟨ fst x ∈ fst P ⟩ → ∥ Σ[ y ∈ SL.S ] Holds G x y ∥₁ valG = domAt-in zero (suc zero) γG (code .snd .fst)
编码单射 G 的单射性子句由值恢复源端成员：若两个源端成员具有相同的记录值，则它们的底层集合相等。
injG : (y x x' : SL.S) → Holds G x y → Holds G x' y → fst x ≡ fst x' injG = injAt-out zero γG (code .snd .snd .fst)
固定输入 x 后，G 的任意两个图取值都因单值性而相等。由于可构造性证明是命题，底层取值的相等可提升为完整见证的相等。因此，所有可能取值组成的纤维本身也是命题。
isPropVal : (x : SL.S) → isProp (Σ[ y ∈ SL.S ] Holds G x y) isPropVal x (y , h) (y' , h') = Σ≡Prop (λ w → snd (pr (fst x) (fst w) ∈ fst G)) (S≡ (svG x y y' h h'))
定义域子句起初只在命题截断下给出 G 的取值。上一步的唯一性使目标纤维取值于命题，因此可以消去截断，并在后续构造中使用这个唯一取值。这一步依赖唯一性，而不是一般的选择原理。
val : (x : SL.S) → ⟨ fst x ∈ fst P ⟩ → Σ[ y ∈ SL.S ] Holds G x y val x m = PT.rec (isPropVal x) (λ z → z) (valG x m)
定义 a 先于 b，意思是二者都属于 P，并且在命题截断下存在图取值 x 与 y，满足 G(a)=x、G(b)=y 及 x∈y。命题截断只记录合适的像存在，而不保留对见证的选取。
Read : SL.S → SL.S → Type (ℓ-suc ℓ) Read a b = ∥ Σ[ x ∈ SL.S ] Σ[ y ∈ SL.S ] ( ⟨ fst a ∈ fst P ⟩ × ⟨ fst b ∈ fst P ⟩ × Holds G a x × Holds G b y × ⟨ fst x ∈ fst y ⟩ ) ∥₁
为了在对象语言中表达这条关系，环境把 A、B 及其候选像 x、y 放在两次应用 G 都能读取的位置。这样，同一条公式便能同时陈述 G(A)=x、G(B)=y 与 x∈y。
private env5 : SL.S → SL.S → SL.S → SL.S → SL.S → SL.S ^ 5 env5 p A B x y = y ∷ x ∷ B ∷ A ∷ p ∷ []
第一条充分性等式把编码后的应用认同为图陈述 Holds G A x。它在对象语言公式与「编码图把 A 送到 x」这一断言之间建立桥梁。
b1 : (p A B x y : SL.S) → ⟨ env5 p A B x y ⊨ appC G (suc (suc (suc zero))) (suc zero) ⟩ ≡ Holds G A x b1 p A B x y = cong ⟨_⟩ (appC-adequate G (suc (suc (suc zero))) (suc zero) (env5 p A B x y))
第二条充分性等式对 B 与 y 作同样的转换。两条等式合在一起，使拉回关系既可通过公式满足来证明，也可通过关于 G 的图的通常陈述来证明。
b2 : (p A B x y : SL.S)
→ ⟨ env5 p A B x y ⊨ appC G (suc (suc zero)) zero ⟩ ≡ Holds G B y
b2 p A B x y = cong ⟨_⟩
(appC-adequate G (suc (suc zero)) zero (env5 p A B x y))
定义公式先把两个端点限制在内部幂集内，再量化两个模型元素作为它们的像。两条应用原子与两个像之间的隶属比较合在一起，给出 P 上一条关系的一阶描述；关系构造随后把这一描述表示为 L 中的集合。
private opaque φR : Formula SL.S 3 φR = (var (suc zero) ∈̇ con P) ∧̇ ((var zero ∈̇ con P) ∧̇ ∃̇ (∃̇ (appC G (suc (suc (suc zero))) (suc zero)
在两层存在绑定之内，其余子句分别断言两个见证是两端点的 G 像，并且第一像属于第二像。这正是沿 G 拉回的 δ 上的隶属次序。
∧̇ (appC G (suc (suc zero)) zero ∧̇ (var (suc zero) ∈̇ var zero)))))
向外读取公式时，首先把两个像的见证保留在命题截断之下。随后，两条充分性等式把编码应用转换成图事实，恰好得到 Read 中的语义数据：端点隶属、两个取值及二者的隶属比较。
read : (a b p : SL.S) → ⟨ (b ∷ a ∷ p ∷ []) ⊨ φR ⟩ → Read a b read a b p (ma , mb , h) = PT.rec squash₁ (λ { (x , hx) → PT.map (λ { (y , ha , hb , hxy) → x , y , ma , mb , transport (b1 p a b x y) ha , transport (b2 p a b x y) hb , hxy }) hx }) h
向内读法沿反向的充分性等式把每条宿主侧事实运回，填充存在与应用槽位以重建公式满足。
fill : (a b p : SL.S) → Read a b → ⟨ (b ∷ a ∷ p ∷ []) ⊨ φR ⟩ fill a b p = PT.rec (snd ((b ∷ a ∷ p ∷ []) ⊨ φR)) (λ { (x , y , ma , mb , ha , hb , hxy) → ma , mb , ∣ x , ∣ y , transport (sym (b1 p a b x y)) ha , transport (sym (b2 p a b x y)) hb , hxy ∣₁ ∣₁ })
有界关系构造现在把这个可定义谓词化为 L 中实际的关系集合。上面证明的两个方向保证，编码关系中的隶属恰好具有 Read 所表达的命题截断内容。
module Pullback = Relation P P φR (λ a b → Read a b , squash₁) read fill
在反方向读取中，两条充分性等式把图事实 Holds G A x 与 Holds G B y 转回应用原子。再把 x 与 y 封装为两层存在量词的见证，便重建定义公式的满足。
R : SL.S R = Pullback.rel
从 R 的一条关系项可以读回定义拉回关系的命题截断数据：两个端点属于幂集，它们具有 G 像，并且第一像属于第二像。
R-out : (a b : SL.S) → Holds R a b → Read a b R-out = Pullback.pair-out
向内读式由两个端点隶属、两条 G 像事实及二像间的隶属构造关系条目。
R-in : (a b x y : SL.S) → ⟨ fst a ∈ fst P ⟩ → ⟨ fst b ∈ fst P ⟩ → Holds G a x → Holds G b y → ⟨ fst x ∈ fst y ⟩ → Holds R a b R-in a b x y ma mb ha hb hxy = Pullback.into a b ma mb ∣ x , y , ma , mb , ha , hb , hxy ∣₁
编码关系的每条关系项，其两个端点都属于 P。证明读取命题截断下的见证，舍去像的数据，只保留两条端点隶属事实；由于二者的积是命题，这样消去命题截断是允许的。
Rsub : (a b : SL.S) → Holds R a b → ⟨ fst a ∈ fst P ⟩ × ⟨ fst b ∈ fst P ⟩ Rsub a b h = PT.rec (isProp× (snd (fst a ∈ fst P)) (snd (fst b ∈ fst P))) (λ { (_ , _ , ma , mb , _) → ma , mb })
应用向外读法即可取得提取所需的见证。由于结论是两个端点隶属命题组成的命题，对这些见证的命题截断作消去是合法的。
(R-out a b h)
序型构造用一个小的呈现域 Dom 表示 P 的成员。关系 a ≺ b 恰好记录相应成员被 R 关联这一编码事实；因此，后续证明可以在索引上研究拉回序，并最终将其塌缩。
module OT = Code P R Rsub using ( Dom; Dom≡; toDom; up; up-mem; up-toDom; ↪; _≺_; ≺-in; ≺-out ; module Conjuncts )
对这个域中的索引 b，令 v b 为 G 赋给其所表示的 P 成员的唯一取值。接下来将证明这些代表都是 δ 以下的序数。
v : OT.Dom → SL.S v b = fst (val (OT.up b) (OT.up-mem b))
所取值的第二分量记录相应的图事实 Holds G (up b) (v b)。它将把代表之间的比较与拉回关系中的关系项连接起来。
v-holds : (b : OT.Dom) → Holds G (OT.up b) (v b) v-holds b = snd (val (OT.up b) (OT.up-mem b))
由单射码的值域子句，G 的每个取值都属于后继基数 δ。因此，所有代表都位于同一个序数内，可以在其中使用隶属比较与序数三歧性。
v∈δ : (b : OT.Dom) → ⟨ fst (v b) ∈ fst δ ⟩ v∈δ b = ranG (OT.up b) (v b) (v-holds b)
每个 G 取值是序数，承继自 δ 的序数性。
ord-v : (b : OT.Dom) → IsOrd (fst (v b)) ord-v b = mem-ord {A = fst δ} ordδ (fst (v b)) (v∈δ b)
向前比较把拉回关系中的一步前驱关系转化为两个代表序数之间的隶属。读取关系条目会得到两个像见证；G 的单值性把它们分别认同为固定取值 v a 与 v b。
≺-fwd : (a b : OT.Dom) → a OT.≺ b → ⟨ fst (v a) ∈ fst (v b) ⟩ ≺-fwd a b k = PT.rec (snd (fst (v a) ∈ fst (v b))) (λ { (x , y , _ , _ , ha , hb , hxy) → subst2 (λ s t → ⟨ s ∈ t ⟩) (svG (OT.up a) x (v a) ha (v-holds a))
两条单值性等式把从 R 读出的像见证分别换成固定代表 v a 与 v b。沿这两条等式搬运 x∈y，便得到所需比较 v a ∈ v b。
(svG (OT.up b) y (v b) hb (v-holds b)) hxy }) (R-out (OT.up a) (OT.up b) (OT.≺-out a b k))
向后比较由两个代表序数的隶属重新引入两条图事实及二像间的隶属，构造拉回关系。
≺-bwd : (a b : OT.Dom) → ⟨ fst (v a) ∈ fst (v b) ⟩ → a OT.≺ b ≺-bwd a b h = OT.≺-in a b (R-in (OT.up a) (OT.up b) (v a) (v b) (OT.up-mem a) (OT.up-mem b) (v-holds a) (v-holds b) h)
为证明良基性，固定一个层级元素 u，并考察代表值为 u 的所有域索引。谓词 Pacc u 要求每个这样的索引在拉回序中可达，从而为对外围隶属关系作归纳做好准备。
private Pacc : V ℓ → Type (ℓ-suc ℓ) Pacc u = (b : OT.Dom) → fst (v b) ≡ u → Acc OT._≺_ b
归纳步为代表序数严格低于 u 的前驱构造可达性：向前比较把隶属运到代表，归纳假设在该处供给可达性。
accStep : (u : V ℓ) → (∀ u' → ⟨ u' ∈ˢ u ⟩ → Pacc u') → Pacc u accStep u IH b e = acc (λ a k → IH (fst (v a)) (subst (λ w → ⟨ fst (v a) ∈ˢ w ⟩) e (≺-fwd a b k)) a refl)
每个层级元素处的可达性由环境层级的正则性归纳证明，后者即其隶属的良基性。
accAt : (u : V ℓ) → Pacc u accAt = WF.WFI.induction regularityV {P = Pacc} accStep
拉回序的良基性由每个代表序数处的可达性装配而成。
wf : WellFounded OT._≺_ wf b = accAt (fst (v b)) b refl
拉回序的传递性复合两条向前比较，经由序数 δ 的传递性施于两条代表隶属。
≺-trans : {a b c : OT.Dom} → a OT.≺ b → b OT.≺ c → a OT.≺ c ≺-trans {a} {b} {c} k k' = ≺-bwd a c (ordδ .snd (fst (v c)) (v∈δ c) (≺-fwd a b k) (≺-fwd b c k'))
拉回序的三歧性来自 δ 中代表取值的序数三歧性：对任意 a 与 b，或者 v a ∈ v b，或者两个取值相等，或者 v b ∈ v a。
tri : (a b : OT.Dom) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a)) tri a b = go (ord-tri (fst (v a)) (ord-v a) (fst (v b)) (ord-v b)) where go : Tri (fst (v a)) (fst (v b)) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
严格低于情形直接产出拉回比较。相等情形通过 G 的单射性施于相等的代表取值认同两个域成员。严格高于情形反转比较。
go (inl h) = inl (≺-bwd a b h) go (inr (inl e)) = inr (inl (OT.Dom≡ (injG (v a) (OT.up a) (OT.up b) (v-holds a) (subst (λ w → ⟨ pr (OT.↪ b) w ∈ fst G ⟩) (sym e) (v-holds b))))) go (inr (inr h)) = inr (inr (≺-bwd b a h))
良基性与传递性现在支持构造塌缩映射 col 及其像 otL。三歧性进一步给出塌缩的单射性：不同的域索引不可能具有相同的塌缩值。这些事实既给出塌缩表，也提供稍后反转它所需的数据。
module C = OT.Conjuncts wf ≺-trans using ( module Inj; col; col-ord; col-out; colTable; colTable-in ; colTable-pair; otL; otL-in; otL-out ) module I = C.Inj tri using ( code; col-inj; module Inverse )
塌缩表是从内部幂集 P 到其塌缩像 otL 的编码单射。把这张特定的表及其单射性证明放入命题截断，便得到内部陈述 InjL P otL。
power-into-ot : InjL P C.otL power-into-ot = ∣ C.colTable , I.code ∣₁
要证明塌缩像是序数，需要同时证明该像传递，并且它的每个成员都是传递集。对于第二项条件，属于 otL 的事实会在命题截断下给出一个索引 b，其塌缩值呈现给定成员。
ot-ord : IsOrd (fst C.otL) ot-ord = tr , mem where mem : (x : V ℓ) → ⟨ x ∈ˢ fst C.otL ⟩ → isTransV x mem x h = PT.rec (isPropIsTransV x)
每个塌缩值 col b 已知都是序数，因而是传递集。沿等式 col b = x 搬运这一传递性，便证明像的任意成员 x 都传递。
(λ { (b , e) → subst isTransV e (C.col-ord b .fst) }) (C.otL-out x h)
还需证明像本身是传递集。给定 y∈x 与 x∈otL，otL 的向外描述会在命题截断下把 x 呈现为某个塌缩值 col b；目标隶属 y∈otL 是命题，因此可以局部使用这个见证。
tr : isTransV (fst C.otL) tr {x} {y} y∈x x∈ot = PT.rec (snd (y ∈ˢ fst C.otL)) outer (C.otL-out x x∈ot) where outer : Σ[ b ∈ OT.Dom ] (C.col b ≡ x) → ⟨ y ∈ˢ fst C.otL ⟩
把 x 换成 col b 后，关于 col b 中隶属关系的塌缩等式再次在命题截断下给出一个前驱 r≺b，其塌缩值为 y。这个更小的塌缩值正是把 y 放回像中所需的见证。
outer (b , e) = PT.rec (snd (y ∈ˢ fst C.otL)) inner (C.col-out b y (subst (λ w → ⟨ y ∈ˢ w ⟩) (sym e) y∈x)) where inner : Σ[ r ∈ OT.Dom ] ((r OT.≺ b) × (C.col r ≡ y)) → ⟨ y ∈ˢ fst C.otL ⟩
前驱的塌缩沿其等式运到 y，把 y 放进像内，完成传递性证明。
inner (r , _ , e2) = subst (λ w → ⟨ w ∈ˢ fst C.otL ⟩) e2 (C.otL-in r)
对层级元素 w，纤维 Fib w 由一个索引 b 与等式 col b = w 组成。因此，这个纤维的元素恰是 w 在塌缩映射下的原像。
Fib : V ℓ → Type (ℓ-suc ℓ) Fib w = Σ[ b ∈ OT.Dom ] (C.col b ≡ w)
col 的单射性使每个纤维成为命题。若 b 与 b' 都塌缩到 w，两条等式就把 col b 与 col b' 认同，单射性继而认同两个索引。外围层级 V ℓ 是集合，因此每个等式类型 col b = w 都是命题，其中的证明不会造成进一步区别。
isPropFib : (w : V ℓ) → isProp (Fib w) isPropFib w (b , e) (b' , e') = Σ≡Prop (λ _ → setIsSet _ _) (I.col-inj b b' (e ∙ sym e'))
隶属 w∈otL 起初只在命题截断下给出一个原像索引。由于刚刚证明了 Fib w 是命题，可以消去这一截断，恢复塌缩值为 w 的唯一索引。
fib : (w : V ℓ) → ⟨ w ∈ˢ fst C.otL ⟩ → Fib w fib w h = PT.rec (isPropFib w) (λ z → z) (C.otL-out w h)
刚得到的唯一原像使塌缩表可以在整个 otL 上反向读取。该索引所表示的原成员属于 P，因此逆向构造会产生 L 中的一张图，尤其给出下文所用的内部编码单射 Back.injL : InjL otL P。
module Back where open I.Inverse C.otL P (λ w mw → fib (fst w) mw) (λ w mw → OT.up-mem (fib (fst w) mw .fst)) public using ( fn; graph; at; only; M; inj; injL ) renaming ( SourceMem to Mem )
把塌缩序数 otL 记作 μ。序数三歧性比较 μ 与后继基数 δ。辅助函数 from-sub 提取出相等分支与 δ∈μ 分支共有的构造：只要 δ 的每个成员也属于 μ，它就会产生所需的 InjL δ P。
result : InjL δ P result = go (ord-tri (fst C.otL) ot-ord (fst δ) ordδ) where from-sub : ((z : SV.S) → ⟨ z ∈ˢ fst δ ⟩ → ⟨ z ∈ˢ fst C.otL ⟩) → InjL δ P
包含编码把子集事实打包为从 δ 到塌缩像的编码单射，逆塌缩单射再把它复合入幂集。
from-sub sub = injl-trans δ C.otL P (inclusion-coded δ C.otL sub) Back.injL
三歧性首先考察 μ∈δ。在这一分支中，below-succ-injects 利用后继基数事实得到 InjL μ κ。将它与 InjL P μ 复合便得到 InjL P κ，这与内部 Cantor 定理矛盾。因此，被排除的恰好是塌缩序数严格低于 δ 的情形。
go : Tri (fst C.otL) (fst δ) → InjL δ P go (inl ot∈δ) = Empty.rec (Cantor.no-inj zf κ (injl-trans P C.otL κ power-into-ot (below-succ-injects κ δ sc C.otL ot-ord ot∈δ))) go (inr (inl e)) =
余下两种情形都给出 from-sub 所需的包含。若 μ=δ，沿等式搬运便把 δ 中的每个隶属变为 μ 中的隶属。若 δ∈μ，序数 μ 的传递性同样给出 δ⊆μ。在任一情形中，把这个包含编码为单射并与逆塌缩单射复合，便得到 InjL δ P。
from-sub (λ z h → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) h) go (inr (inr δ∈ot)) = from-sub (λ z h → ot-ord .fst h δ∈ot)
后继基数到达幂集
该定理接收后继基数见证 sc 与命题截断下的单射 InjL (𝒫 κ) δ。由于目标 InjL δ (𝒫 κ) 本身是命题，证明只能在局部分支中考察一张具体图 G。附加假设 κ∉ω 出现在 SuccIntoPower 的陈述中，但本证明没有使用它。在 GCH 的装配中，succCardExists 只在命题截断下给出 δ 及其见证 sc；power-into-succ 另行构造 pis : InjL (𝒫 κ) δ，再把它交给 succ-into-power。所得结论只记录两个方向的编码单射在命题截断下存在，并未选定任何一张图，也未产生双射、集合相等或基数等式。
succ-into-power : (zf : ModelL.isZFModel) → SuccIntoPower zf succ-into-power zf κ δ κ∉ω sc = PT.rec squash₁ (λ { (G , code) → Build.result zf κ δ sc G code })