Mostowski 塌缩

递归塌缩

对每个集合 x，映射 π 应把 x 映为 x 中同时属于载体 X 的那些元素的塌缩值组成的集合。这是一个沿成员关系的递归定义：要知道 π x，只需要 x 的元素 y 的 π y。环境层级中成员关系的良基性恰好允许这种形式的定义，并同时给出其计算律。

索引类型 Fiber x 选取被过滤的元素：x 的呈现中的一个索引 m，使得所指名的元素 ⟪ x ⟫↪ m 是 X 的小元素。由于过滤使用小成员关系 (它本身是层级 ℓ 的命题)，索引类型落在 Type ℓ 中，所得的集合合法地是小的。递归步随后呈现一个新集合：索引就是这些索引对，每个索引指名 rec 作用于 x 的相应元素 ⟪ x ⟫↪ m 的值，并附带递归原理所需的成员关系证明 member x m 以保证递归调用合法。注意信息的流向：这里没有用 fiber；载体成员关系的见证作为数据随索引对一起携带。

Fiber : S → Type ℓ
Fiber x = Σ[ m ∶ ⟪ x ⟫ ] ⟨ ⟪ x ⟫↪ m ∈ₛ X ⟩

step : (x : S) → (∀ y → y ∈ᵗ x → S) → S
step x rec = sett (Fiber x) (λ p → rec (⟪ x ⟫↪ (p .fst)) (member x (p .fst)))

把 ∈ 递归原理在 step 处实例化便得到塌缩映射 π。递归定理还给出把 π x 展开为 step x 所呈现集合的等式，后面的每个论证实际使用的正是这条等式。

定义 π = ∈-induction step 是对层级章递归原理的一次调用：由于成员关系良基，由该递归步定义的函数在整个 S 上存在。opaque 块把 π 标记为密封，即类型检查器不会在使用处自动展开它；这使提到 π 的证明项保持精简。

opaque
  π : S → S
  π = ∈-induction step

opaque
  unfolding π

仅靠密封会隐藏定义，所以第二个块显式允许展开 π 并记录计算律：π x 以一条路径等于 step x 在递归调用取为 π y 时呈现的集合。这条律由同一递归原理的伴随定理 ∈-induction-compute 直接提供，无需新的证明。后面的章节沿这条路径搬运成员关系证明，而不是展开定义。

  π-compute : (x : S) → π x ≡ step x (λ y _ → π y)
  π-compute = ∈-induction-compute step

π 的第一条性质刻画它的元素。若 z 属于 π x，则「仅仅存在」载体中某个元素的塌缩等于 z。该陈述是截断的：我们不选取这样的元素，只证明这种对的类型被 inhabit。

证明从成员关系证书 z∈ 出发，沿 π 的计算律进行搬运。把 π x 改写为 sett (Fiber x) ⋯ 之后，呈现集合的成员关系类型让我们直接读出索引：一个索引对 p，连同指名元素的 π 值等于 z 的路径。于是计算律把抽象的成员关系转化为具体的递归数据。

π-member : (x z : S) → ⟨ z ∈ˢ π x ⟩
         → ∥ Σ[ y ∶ S ] (⟨ y ∈ˢ X ⟩ × (π y ≡ z)) ∥₁
π-member x z z∈ = map₁ mk (subst (λ w → ⟨ z ∈ˢ w ⟩) (π-compute x) z∈)
  where
  mk : Σ[ p ∶ Fiber x ] (π (⟪ x ⟫↪ (p .fst)) ≡ z)

辅助函数 mk 把这份递归数据重塑为承诺的形式。见证 ⟪ x ⟫↪ (p .fst) 正是索引对所指名的 x 的元素；第二分量 ∈∈ₛ ⋯ .snd 把索引对的载体成员关系证书从原生成员关系转换为小成员关系；路径 q 则直接复用。结果是用 map₁ 构造的截断对，因此尽管每个成分都是显式的，结论仍只是存在性陈述。

     → Σ[ y ∶ S ] (⟨ y ∈ˢ X ⟩ × (π y ≡ z))
  mk (p , q) = ⟪ x ⟫↪ (p .fst)
             , ( ∈∈ₛ {a = ⟪ x ⟫↪ (p .fst)} {b = X} .snd (p .snd)
               , q )

传递的像

塌缩在载体上的像本身应当是一个集合。定义 πX 时以 X 的索引类型来呈现它：其元素就是载体元素的塌缩值 π (⟪ X ⟫↪ m)。本节证明 πX 是传递的，只用到 π-member 的内容：任何塌缩值的元素本身又是某个载体元素的塌缩。

集合 πX 是 π 限制在 X 上的像，用 sett 建立在载体自身呈现的索引类型 ⟪ X ⟫ 之上。其成员关系引理是对该呈现的直接解读：πX 的元素「仅仅」是某个 y ∈ X 的 π y；证明只需拆开索引 m，把路径 π (⟪ X ⟫↪ m) ≡ z 与由呈现的忠实性给出的成员关系证书 member X m 重新打包。

πX : S
πX = sett ⟪ X ⟫ (λ m → π (⟪ X ⟫↪ m))

πX-member : (z : S) → ⟨ z ∈ˢ πX ⟩
          → ∥ Σ[ y ∶ S ] (⟨ y ∈ˢ X ⟩ × (π y ≡ z)) ∥₁
πX-member z z∈ = map₁ mk z∈

反向的引入说 πX 包含它应有的所有塌缩值：若 y 是 X 的元素，则 π y 是 πX 的元素。这里呈现章的引理 fiber 至关重要：成员关系证明 y∈X 给出实际的索引 m 和路径 ⟪ X ⟫↪ m ≡ y，对该路径施加 cong π 便把 π y 展示为索引 m 处的塌缩值。与 π-member 不同，这一方向的输入不是截断的；只有输出因呈现集合的成员关系是截断的才包在 ∥_∥₁ 中。

  where
  mk : Σ[ m ∶ ⟪ X ⟫ ] (π (⟪ X ⟫↪ m) ≡ z)
     → Σ[ y ∶ S ] (⟨ y ∈ˢ X ⟩ × (π y ≡ z))
  mk (m , q) = ⟪ X ⟫↪ m , ( member X m , q )

πX-intro : (y : S) → ⟨ y ∈ˢ X ⟩ → ⟨ π y ∈ˢ πX ⟩

πX 的传递性取 isTrans 要求的形式：若 y 是 x 的元素且 x 属于像，则 y 属于像。证明用 rec₁ 消去截断的假设 x∈πX，这是合法的，因为目标 ⟨ y ∈ˢ πX ⟩ 是命题。每个满足 π z ≡ x 且 z ∈ X 的见证都把问题化为 y ∈ π z。

πX-intro y y∈X = ∣ fiber X y∈X .fst , cong π (fiber X y∈X .snd) ∣₁

πX-trans : isTrans πX
πX-trans {x} {y} y∈x x∈πX = rec₁ ((y ∈ˢ πX) .snd) go (πX-member x x∈πX)
  where
  go : Σ[ z ∶ S ] (⟨ z ∈ˢ X ⟩ × (π z ≡ x)) → ⟨ y ∈ˢ πX ⟩

内层步骤先把 y∈x 沿路径 π z ≡ x 搬运得到 y ∈ᵗ π z，再用 π-member 得知 y「仅仅」是 X 中某个 w 的塌缩。注意与经典图景的不同之处：传递性证明不需要对 y 做归纳，因为呈现集合 π z 中的成员关系已直接暴露了塌缩数据。

  go (z , z∈X , pzx) = rec₁ ((y ∈ˢ πX) .snd) go₂ (π-member z y y∈πz)
    where
    y∈πz : y ∈ᵗ π z
    y∈πz = subst (λ w → y ∈ᵗ w) (sym pzx) y∈x
    go₂ : Σ[ w ∶ S ] (⟨ w ∈ˢ X ⟩ × (π w ≡ y)) → ⟨ y ∈ˢ πX ⟩

最后 go₂ 沿路径 π w ≡ y 搬运所需的成员关系：由于 w 属于 X，πX-intro 给出 ⟨ π w ∈ˢ πX ⟩，该路径把 π w 与 y 等同起来。至此 πX-trans 完成，塌缩的像是一个真正的传递集。

    go₂ (w , w∈X , pwy) = subst (λ v → ⟨ v ∈ˢ πX ⟩) pwy (πX-intro w w∈X)

前向引理记录塌缩如何保持载体元素之间的成员关系。若 y 是 x 的元素且二者都在载体 X 中，则 π y 在小关系下是 π x 的元素。这条引理是同构证明的主力：单射性证明中的两个包含都化归到它。与截断的 π-member 不同，这里所有数据都是显式的，因为 y ∈ᵗ x 本身就指名了一个见证。

第一个成分是从成员关系证明恢复的、呈现映射在 y 上的纤维中的一个元素。把 fiber x 作用于 yx : y ∈ᵗ x，得到 x 的呈现中的一个实际索引 m，连同路径 ⟪ x ⟫↪ m ≡ y。这正是为 πX-intro 提供见证的那条显式构造引理：由于嵌入的纤维都是命题，截断的成员关系可以消去到这个对类型中。

π∈-fwd : (x y : S) → y ∈ᵗ x → y ∈ᵗ X → ⟨ π y ∈ˢ π x ⟩
π∈-fwd x y yx yu = subst (λ w → ⟨ π y ∈ˢ w ⟩) (sym (π-compute x)) wit
  where
  fib : Σ[ m ∶ ⟪ x ⟫ ] (⟪ x ⟫↪ m ≡ y)
  fib = fiber x yx

载体成员关系 yu 谈论的是 y，而对是从 ⟪ x ⟫↪ m 构造的，所以证明沿路径 p 把 yu 反向搬运得到 ⟪ x ⟫↪ m ∈ˢ X，再用 ∈∈ₛ 的前向一半把这条原生小成员关系证书转换为小关系中的成员关系。这是两种成员关系直接相遇的唯一场合，∈∈ₛ 恰是桥。

  m : ⟪ x ⟫
  m = fib .fst
  p : ⟪ x ⟫↪ m ≡ y
  p = fib .snd
  sm : ⟨ ⟪ x ⟫↪ m ∈ₛ X ⟩

此时对 (m , sm) 已属于 Fiber x，见证 wit 把 π y 展示为 step x 所呈现集合的元素：索引就是这个对，路径分量是 cong π p，把 π (⟪ x ⟫↪ m) 与 π y 等同。再沿 π x 的计算律搬运，这个成员关系便落在 π x 本身之下，前向引理完成。

  sm = ∈∈ₛ {a = ⟪ x ⟫↪ m} {b = X} .fst (subst (λ w → ⟨ w ∈ˢ X ⟩) (sym p) yu)
  wit : ⟨ π y ∈ˢ sett (Fiber x) (λ q → π (⟪ x ⟫↪ (q .fst))) ⟩
  wit = ∣ (m , sm) , cong π p ∣₁

外延性与塌缩同构

传递的像就位之后，剩下的问题是载体在塌缩下是否不会合并。本节假设载体的结构外延性 isExt X，证明 π 在 X 上单射，从而载体元素之间的成员关系与其塌缩值之间的成员关系双向一致。关键一步是恢复引理：从 ⟨ π z ∈ˢ π x ⟩ 与一个比较原理出发，它重构 z ∈ᵗ x。这里只有外延性登场；不需要载体的传递性，因为传递性论证本可提供的成员关系已由索引对或 isExt X 内部的量化携带。

恢复引理接受两个输入。其一是截断陈述 ⟨ π z ∈ˢ π x ⟩；其二是比较原理 same，断言任何属于 x ∩ X 且满足 π b ≡ π z 的 b 必等于 z。目标 z ∈ᵗ x 是命题，因此用 rec₁ 消去截断是合法的。沿 π x 的计算律搬运假设，便把它化为 step x 所呈现集合的元素，其元素由 Fiber x 索引。

private
  π∈-recover : (x z : S) → ⟨ π z ∈ˢ π x ⟩
             → ((b : S) → b ∈ᵗ x → b ∈ᵗ X → π b ≡ π z → b ≡ z)
             → z ∈ᵗ x
  π∈-recover x z h same = rec₁ ((z ∈ˢ x) .snd)

给定指名 b = ⟪ x ⟫↪ (p .fst) 为 x 元素的索引对 p 以及塌缩路径 π b ≡ π z，比较原理即可触发。其假设直接得到满足：member x (p .fst) 证明 b ∈ᵗ x，而 ∈∈ₛ 的第二分量把索引对的载体成员关系证书转换为 b ∈ᵗ X。结论 b ≡ z 把成员关系证书 b ∈ᵗ x 搬运为 z ∈ᵗ x，这正是目标。

    (λ { (p , q) → subst (λ w → ⟨ w ∈ˢ x ⟩)
      (same (⟪ x ⟫↪ (p .fst)) (member x (p .fst))
        (∈∈ₛ {a = ⟪ x ⟫↪ (p .fst)} {b = X} .snd (p .snd)) q)
      (member x (p .fst)) })
    (subst (λ w → ⟨ π z ∈ˢ w ⟩) (π-compute x) h)

依赖外延性的材料现在放入一个以 Xext : isExt X 为参数的模块，使该假设显式出现，且不会在别处悄悄可用。在模块内部，归纳谓词 P 就是相对于载体的单射性陈述本身：对 X 中的 x，所有塌缩值与之相同的 y ∈ X 都经路径等于 x。这正是成员关系归纳要同时对 x 的每个元素建立的性质。

module InjExt (Xext : isExt X) where

P : S → Type (ℓ-suc ℓ)
P x = (y : S) → x ∈ᵗ X → y ∈ᵗ X → π x ≡ π y → x ≡ y

in⊆ : (x y z : S) → x ∈ᵗ X → y ∈ᵗ X → z ∈ᵗ x → z ∈ᵗ X
    → π x ≡ π y
    → ((a : S) → a ∈ᵗ x → P a)
    → ⟨ z ∈ˢ y ⟩
in⊆ x y z xu yu zx zu e IH = π∈-recover y z

  (subst (λ w → ⟨ π z ∈ˢ w ⟩) e (π∈-fwd x z zx zu))
  (λ b by bu q → sym (IH z zx b zu bu (sym q)))

out⊆ : (x y z : S) → x ∈ᵗ X → y ∈ᵗ X → z ∈ᵗ y → z ∈ᵗ X
     → π y ≡ π x
     → ((a : S) → a ∈ᵗ x → P a)
     → ⟨ z ∈ˢ x ⟩
out⊆ x y z xu yu zy zu e IH = π∈-recover x z

  (subst (λ w → ⟨ π z ∈ˢ w ⟩) e (π∈-fwd y z zy zu))
  (λ b bx bu q → IH b bx z bu zu q)

step-inj : (x : S) → ((a : S) → a ∈ᵗ x → P a) → P x
step-inj x IH y xu yu e = Xext x y xu yu to from
  where

  to : (z : S) → z ∈ᵗ X → ⟨ z ∈ˢ x ⟩ → ⟨ z ∈ˢ y ⟩
  to z zu zx = in⊆ x y z xu yu zx zu e IH
  from : (z : S) → z ∈ᵗ X → ⟨ z ∈ˢ y ⟩ → ⟨ z ∈ˢ x ⟩
  from z zu zy = out⊆ x y z xu yu zy zu (sym e) IH

π-inj : (x y : S) → x ∈ᵗ X → y ∈ᵗ X → π x ≡ π y → x ≡ y
π-inj = ∈-induction step-inj

π∈-bwd : (x y : S) → x ∈ᵗ X → y ∈ᵗ X → ⟨ π y ∈ˢ π x ⟩ → y ∈ᵗ x
π∈-bwd x y xu yu h = π∈-recover x y h
  (λ b bx bu q → π-inj b y bu yu q)

iso : (x y : S) → x ∈ᵗ X → y ∈ᵗ X
    → (⟨ y ∈ˢ x ⟩ → ⟨ π y ∈ˢ π x ⟩) × (⟨ π y ∈ˢ π x ⟩ → ⟨ y ∈ˢ x ⟩)
iso x y xu yu = (λ yx → π∈-fwd x y yx yu) , π∈-bwd x y xu yu

递归等式 π x ≡ step x (λ y _ → π y) 不仅是 ∈-induction 所构造的这个特定函数的性质：它在路径意义下刻画了塌缩。任何满足同一递归等式 (递归调用中也是 f 自身) 的函数 f 都处处与 π 一致。这一唯一性使塌缩成为良定义的对象，而不是某个构造的众多可能输出之一。

陈述量化所有配备计算规则 h : f x ≡ sett (Fiber x) (λ p → f (⟪ x ⟫↪ (p .fst))) 的 f : S → S。注意其形状：与 π 自身的律一样，右边呈现的集合，其元素是 x 中被过滤元素的 f 像。结论是路径族 π x ≡ f x，由 ∈ 归纳证明，因为在 x 的元素处已知等式便决定了在 x 处的等式。

unique : (f : S → S)
       → ((x : S) → f x ≡ sett (Fiber x) (λ p → f (⟪ x ⟫↪ (p .fst))))
       → (x : S) → π x ≡ f x
unique f h = ∈-induction stepU
  where

归纳步串联三条路径。从 π-compute x 出发，左边变为递归调用取 π 时 step x 呈现的集合；中间路径 step-eq 把递归调用从 π 换成 f；sym (h x) 展开 f x。复合路径仅凭归纳假设便展示出 π x ≡ f x。

  stepU : (x : S) → ((y : S) → y ∈ᵗ x → π y ≡ f y) → π x ≡ f x
  stepU x IH = π-compute x ∙ step-eq ∙ sym (h x)
    where
    step-eq : sett (Fiber x) (λ p → π (⟪ x ⟫↪ (p .fst)))
            ≡ sett (Fiber x) (λ p → f (⟪ x ⟫↪ (p .fst)))

中间路径本身是对呈现函数应用同余性：保持 sett 固定，索引函数从 λ p → π (⋯) 变为 λ p → f (⋯)，funExt 提供这两个函数的逐点相等。每一点都是归纳假设的实例，作用于索引对 p 所指名的元素，并由成员关系证书 member x (p .fst) 保证递归调用合法。这是良基递归定义的标准唯一性论证，适配到呈现集合的构造子上。

    step-eq = cong (sett (Fiber x)) (funExt ih')
      where
      ih' : (p : Fiber x) → π (⟪ x ⟫↪ (p .fst)) ≡ f (⟪ x ⟫↪ (p .fst))
      ih' p = IH (⟪ x ⟫↪ (p .fst)) (member x (p .fst))

塌缩何时什么都不改变？若 Y 是载体的传递子集，即 Y 的元素的元素仍在 Y 中，则定义塌缩时的过滤对 Y 的元素是完全的：没有任何东西被丢弃，故对每个 y ∈ᵗ Y 有 π y ≡ y。这个不动点命题通过对 y 的 ∈ 归纳证明，比较 π y 与 y 时用的是层级自身的外延性原理。

陈述组合了两个载体侧的数据：小关系下的包含 ⟨ Y ⊆ X ⟩ 与传递性 isTrans Y，即 Y 对元素的元素的封闭性。归纳假设把两种成员关系都写在面上：它只对同时属于 Y 的 y 的元素 m 断言 π m ≡ m，恰好对应证明中会遇到的情况。

fixes : (Y : S) → ⟨ Y ⊆ X ⟩ → isTrans Y → (y : S) → y ∈ᵗ Y → π y ≡ y
fixes Y YX Ytr = ∈-induction stepF
  where
  stepF : (y : S) → ((m : S) → m ∈ᵗ y → m ∈ᵗ Y → π m ≡ m)
        → y ∈ᵗ Y → π y ≡ y

归纳步通过 extensionalV 比较两个集合，这是层级自身的外延性原理：只要元素相同两个集合便相等，这里表述为由双向蕴含生成的路径族。方向 to 说明塌缩集合的元素已是 y 的元素；证明先把截断成员关系 xπ 沿计算律搬运，再用 rec₁ 消去，露出 Fiber y 的一个索引对以及指名元素的 π 值等于 x 的路径。

  stepF y IH yY = extensionalV (λ x → ⇔toPath (to x) (from x))
    where
    to : (x : S) → ⟨ x ∈ˢ π y ⟩ → x ∈ᵗ y
    to x xπ = rec₁ ((x ∈ˢ y) .snd) go
      (subst (λ w → ⟨ x ∈ˢ w ⟩) (π-compute y) xπ)

给定这样的索引对，所指名的元素 ⟪ y ⟫↪ (p .fst) 是 y 的元素且由传递性属于 Y，归纳假设适用于它并将其固定：它的 π 值等于它自身。把这个不动点路径的对称与塌缩路径 q 复合，得到从指名元素到 x 的路径，沿它搬运成员关系证书便落在 x ∈ᵗ y。

      where
      go : Σ[ p ∶ Fiber y ] (π (⟪ y ⟫↪ (p .fst)) ≡ x) → x ∈ᵗ y
      go (p , q) = subst (λ w → ⟨ w ∈ˢ y ⟩) (sym ih' ∙ q) (member y (p .fst))
        where
        ih' : π (⟪ y ⟫↪ (p .fst)) ≡ ⟪ y ⟫↪ (p .fst)

方向 from 说明 y 的每个元素都在塌缩中幸存。这里先用 Y 的传递性看出 x 本身属于 Y；归纳假设随后给出路径 π x ≡ x，把前向引理的结论 ⟨ π x ∈ˢ π y ⟩ 沿该路径搬运，成员关系便落在 x 本身处，得到 ⟨ x ∈ˢ π y ⟩。

        ih' = IH (⟪ y ⟫↪ (p .fst)) (member y (p .fst))
          (Ytr {x = y} {y = ⟪ y ⟫↪ (p .fst)} (member y (p .fst)) yY)

    from : (x : S) → x ∈ᵗ y → ⟨ x ∈ˢ π y ⟩
    from x xy = subst (λ w → ⟨ w ∈ˢ π y ⟩) (IH x xy x∈Y)
      (π∈-fwd y x xy x∈X)

两个辅助事实互为镜像。x 属于 Y 由传递性作用于 x ∈ᵗ y 与 y ∈ᵗ Y 得到。由此，x 属于载体 X 分两小步得出：∈∈ₛ 的反向一半把 x ∈ᵗ Y 化为小成员关系陈述，假设 YX 把该陈述沿包含搬运到 X，再由 ∈∈ₛ 的前向一半返回通常的成员关系证明。

      where
      x∈Y : x ∈ᵗ Y
      x∈Y = Ytr {x = y} {y = x} xy yY
      x∈X : x ∈ᵗ X
      x∈X = ∈∈ₛ {a = x} {b = X} .snd

两个方向都建立后，⇔toPath 把每个 x 处的双向蕴含转换为路径，extensionalV 再把所得的路径族组装成 π y ≡ y。由于 y 是 Y 的任意元素，塌缩逐点固定 Y，归纳完成。

        (YX x (∈∈ₛ {a = x} {b = Y} .fst x∈Y))