沿编码对作秩下降

后续将对编码作良基递归，并在每一步处理所给码的一个直接部件。递归要良基，就需要一个从码到该部件严格下降的度量。成员关系给不出这个度量。Kuratowski 对定义为 pr a b = ⁅ ⁅ a ⁆s , ⁅ a , b ⁆ ⁆：像 b 这样的部件必须经过中间的无序对 ⁅ a , b ⁆ 才能到达，而这个中间集合本身并不是码。故沿成员关系进行的归纳无法把关于码的假设搬过它们。

秩可以。秩沿成员关系严格增长，且取值于序数，而序数的成员关系是传递的；于是有限的成员链收缩为一次序数比较，递归便可改为按秩作良基归纳。本章组装的正是这些比较：有序对每一侧各一步，再把它们复合成从成对载荷的每一侧到外层带标签码的四步下降。

数学背景是累积层级：其载体 S、命题值的隶属关系 ∈ˢ，以及打包诸集合论运算的结构 𝒮ᵥ。在证明任何下降之前，值得先明确一件预备事项。良基递归需要一个严格度量，而此后所用的度量是 von Neumann 秩，它在与秩有关的章节中定义并研究；在那里，rank-mono 记录秩沿隶属关系严格增长，rank-ord 记录每个秩都是序数。

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

open import Base.Prelude

module L.Coding.Descent {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

从码的形状就能看出具体困难。pr a b 的部件并不是 pr a b 的直接成员：它被包在无序对 ⁅ a , b ⁆ 内，而后者又是外层无序对的两个成员之一。成员关系给出的是一条多步的链，而非一条边，且链上的环节是完全不携带码结构的集合。取代这条链的是序数之间的一个严格不等式：先把每条成员边经秩翻译，再复合起来。

open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Rank {ℓ} using ( rank; rank-mono; rank-ord )

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )

这个比较用到层级的三个材料：无序对 ⁅ u , v ⁆、以命题方式刻画无序对成员关系的配对公理 pairing-ax，以及在底层数据的成员与结构化成员 ∈ˢ 之间转换的 ∈∈ₛ。和类型 _⊎_ 将承载两个分量之间的显式选择：inl 取左，inr 取右。这里保持选择的显式性、而非「仅仅存在」，是重要的，因为下降证明必须指明下降进入的是对的哪一个分量。

open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_,_⁆; pairing-ax; ⁅_⁆s )

关键区别在于传递性可用的位置。这里不把任意集合的隶属关系视为传递的；只有每条成员边先经 rank-mono 化为秩之间的关系后，中间对象才是序数，rank-ord 才提供复合这些严格不等式所需的传递性。

open hPropStructure 𝒮ᵥ

诸步

下降论证立于两条可复用的事实。其一是进入无序对的成员边：若 w 显式地等于 u 或 v，则 w 属于 ⁅ u , v ⁆。其二是秩的步骤：一条成员边 x ∈ˢ y 加上一段从 y 到 z 的秩下降，就给出从 x 到 z 的秩下降。两者合起来把成员关系的链化为单次序数比较，并且在任意集合上成立，不局限于任何具体的对表达式。

配对公理把 ⁅ u , v ⁆ 的成员关系刻画为截断的析取：「成员等于 u 或等于 v」整体仅仅成立。辅助引理 pair∈ 给出去掉截断的逆向：它取显式的和 w ≡ u ⊎ w ≡ v，通过把 ∣ h ∣₁ 放入 pairing-ax 的截断一侧、再经 ∈∈ₛ 转换，返回 ⟨ w ∈ˢ ⁅ u , v ⁆ ⟩ 的证明。这正是下降证明所需的方向：已指明下降进入哪个分量，成员关系便无须再分情形地随之而来。复合步骤 trans≺ 随后做秩的翻译。由 rank-ord z，rank z 是序数，故 rank z 以下的成员关系是传递的，故 rank x ∈ˢ rank y 与 rank y ∈ˢ rank z 复合成 rank x ∈ˢ rank z；第一个假设就是把 rank-mono x y 施于 x ∈ˢ y。注意传递性只用在序数秩上，从不假设任意集合的成员关系传递。

pair∈ : (u v w : S) → (w ≡ u) ⊎ (w ≡ v) → ⟨ w ∈ˢ ⁅ u , v ⁆ ⟩
pair∈ u v w h = ∈∈ₛ {a = w} {b = ⁅ u , v ⁆} .snd (pairing-ax u v w .snd ∣ h ∣₁)

trans≺ : (x y z : S) → ⟨ x ∈ˢ y ⟩ → ⟨ rank y ∈ˢ rank z ⟩ → ⟨ rank x ∈ˢ rank z ⟩
trans≺ x y z x∈y ry∈rz = rank-ord z .fst (rank-mono x y x∈y) ry∈rz

进入带标签的载荷

有了两条基本步骤，编码对的下降只需读出 Kuratowski 对的形状。pr a b 的部件 x 经过两条成员边到达整条码：x 属于 ⁅ a , b ⁆，而 ⁅ a , b ⁆ 属于 pr a b。故 pair-component≺ 对任一分量证明这条两步下降，对标签不加任何条件。取第二分量即得 payload≺：从载荷到其带标签码的下降。标签 c 之下的成对载荷 pr a b 还需再复合一次，而这里两侧确实不同：leftPart 先降入载荷内部的第一分量，再与载荷下降复合；rightPart 只是把载荷下降施用两次。通篇标签 c 是任意集合，无须是数码，也不被降入。

两条边都被显式给出。第一条用给定的选择 h : x ≡ a ⊎ x ≡ b 经 pair∈ a b x h。第二条的选择是 inr refl：无序对 ⁅ a , b ⁆ 定义性地就是外层对的右成员，故 pair∈ ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a , b ⁆ (inr refl) 证明它在 pr a b 中的成员关系，rank-mono 再把它变成秩不等式 rank ⁅ a , b ⁆ ∈ˢ rank (pr a b)。然后 trans≺ 复合两者。注意中间集合 ⁅ a , b ⁆ 只出现在证明内部：pair-component≺ 的命题除码与所选分量外不提任何东西。特化 payload≺ 再次用 inr refl 把 z 读作 pr c z 的右分量，给出对任意标签 c 从载荷到其带标签码的下降。

pair-component≺ : (a b x : S) → (x ≡ a) ⊎ (x ≡ b) → ⟨ rank x ∈ˢ rank (pr a b) ⟩
pair-component≺ a b x h = trans≺ x ⁅ a , b ⁆ (pr a b) (pair∈ a b x h)
  (rank-mono ⁅ a , b ⁆ (pr a b) (pair∈ ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a , b ⁆ (inr refl)))

payload≺ : (c z : S) → ⟨ rank z ∈ˢ rank (pr c z) ⟩
payload≺ c z = pair-component≺ c z z (inr refl)

两条带标签的引理都在序数 rank (pr c (pr a b)) 处复合，用的是 rank-ord 的传递性分量。两者之间的不对称反映嵌套结构。对 leftPart，目标 a 是载荷内部的第一分量，故第一条边是 pair-component≺ a b a (inl refl)，给出 rank a ∈ˢ rank (pr a b)，第二条边是载荷下降 payload≺ c (pr a b)。对 rightPart，目标 b 是载荷自身的第二分量，故两条边都是载荷下降：payload≺ a b 从 b 到 pr a b，再 payload≺ c (pr a b) 从载荷到外层带标签码。两种情形的结论形状相同：rank a 或 rank b 属于 rank (pr c (pr a b))，这正是后续对带标签码所作的良基递归对每个直接部件所要求的度量下降。

leftPart : (c a b : S) → ⟨ rank a ∈ˢ rank (pr c (pr a b)) ⟩
leftPart c a b = rank-ord (pr c (pr a b)) .fst
  (pair-component≺ a b a (inl refl)) (payload≺ c (pr a b))

rightPart : (c a b : S) → ⟨ rank b ∈ˢ rank (pr c (pr a b)) ⟩
rightPart c a b = rank-ord (pr c (pr a b)) .fst (payload≺ a b) (payload≺ c (pr a b))