---
title: "Mostowski 塌缩"
module: V.Collapse
lang: zh
site: "Bedrock"
description: "Mostowski 塌缩"
stage: "证明 GCH"
reading_order: 104
canonical: https://bedrock.institute/zh/V.Collapse.html
html: V.Collapse.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/Collapse.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, V.Hierarchy, V.Presentation]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/V.Collapse.md, https://bedrock.institute/ja/V.Collapse.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Mostowski 塌缩

环境累积层级中的每个集合都带有典范呈现：一个索引类型连同指称其元素的索引映射。本章讨论相反的问题。设我们取定一个集合 `X`，只考察层级中属于 `X` 的元素，并沿用层级自身的隶属关系。这个受限结构在什么意义上本身就是一个集合？Mostowski 塌缩给出了回答：沿隶属关系的递归定义塌缩映射 `π`，`π` 在 `X` 上的像是一个传递集；若 `X` 满足结构外延性，则 `π` 在 `X` 上单射，从而给出载体与其塌缩像之间的同构。

三种数学表示贯穿整个证明。第一，隶属关系取命题为值：本章在 ZF 结构 `𝒮ᵥ` 中工作，其隶属谓词以命题为值，因此隶属陈述 `⟨ z ∈ˢ x ⟩` 指称一个底层命题，而不是裸的真值。第二，层级中的集合通过其小呈现来使用：一个索引类型连同指名 `x` 之成员的索引函数 `⟪ x ⟫↪`，于是构造新集合就意味着用索引去呈现它。第三，关于成员的陈述常常只是「仅仅为真」：命题截断 `∥_∥₁` 把「某个索引见证此事实」这类陈述变成「这样的见证仅仅存在」，而不选取任何见证。宇宙层级值得精确陈述：层级的载体类型 `S` 落在 `Type (ℓ-suc ℓ)` 中，而每个呈现索引类型 (如 `⟪ x ⟫`) 都是小的，落在 `Type ℓ` 中；因此索引类型与载体并不同处同一个宇宙层级。

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

open import Base.Prelude

module V.Collapse {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure; Transitive )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; ∈-induction; ∈-induction-compute )
```

三种表示相互咬合。呈现 `sett I f` 产生的集合，其隶属是截断的：成员由索引给出，但隶属陈述只记录这样的索引仅仅存在。这正是后面关于 `π` 成员的引理以截断对作结的原因，也是在那里消去截断合法的原因：消去的目标是隶属陈述 `⟨ _ ⟩` 的底层命题，本身仍是命题，因此不会有被选取的见证逃逸成数据。等价 `∈∈ₛ` 连接了这里使用的两种隶属：嵌入的原生隶属与小关系中的隶属；两个方向都用于在两种形态之间转换隶属证书。

```agda
open import V.Presentation {ℓ} using ( member; fiber )

open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
```

还差一种表示就齐备了：环境层级自带良基的隶属关系，连同原理 `∈-induction` 与 `∈-induction-compute`，前者沿隶属关系递归地定义函数，后者记录由此得到的计算律；层级还带有自身的外延性原理。正是它们驱动塌缩：映射 `π` 将由隶属递归定义，把每个集合的成员经载体 `X` 过滤。表示就位之后，第一个问题是我们应当对载体 `X` 本身提出什么要求。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; _⊆_ )

open hPropStructure 𝒮ᵥ
```

## 载体假设

塌缩以一个集合 `X : S` 为载体。本章出现两个关于 `X` 的假设，作用不同。传递性说 `X` 的元素的元素仍在 `X` 中；它使塌缩的像表现良好。结构外延性说具有相同的 `X` 中成员的两个 `X` 元素相等；它使塌缩映射单射，并且仅它就足以支撑本章的同构部分。

传递性谓词的表述与绝对性章完全一致：`Transitive 𝒮ᵥ (λ x → x ∈ˢ u)` 说的是，若在结构中 `y` 是 `x` 的成员，且在小关系中 `x` 属于 `u`，则 `y` 属于 `u`。由于这里的类由对固定集合 `u` 的小隶属给出，`u` 的传递性见证就是通常的对元素之元素的封闭性；它属于 `Type (ℓ-suc ℓ)`，因为它量化结构元素并返回层级 `ℓ` 的命题。

```agda
isTrans : S → Type (ℓ-suc ℓ)
isTrans u = Transitive 𝒮ᵥ (λ x → x ∈ˢ u)
```

外延性是驱动单射性的假设。对固定载体集合 `X` 陈述，它比较同属 `X` 的两个元素 `x` 与 `y`：若 `X` 中属于 `x` 的每个成员也属于 `y`，且反之亦然，则 `x ≡ y`。结论是一条路径，而不是隶属陈述之间的双向蕴含。

每个被量化的成员 `z` 只在 `X` 上取值：假设 `z ∈ᵗ X` 把注意力限制在载体成员上，因此比较忽略 `X` 之外的元素。两个包含方向分别陈述为截断隶属类型 `⟨ z ∈ˢ _ ⟩` 之间的蕴含，最后才以路径 `x ≡ y` 作结。该陈述不涉及 `X` 的传递性；后面的单射性证明只使用 `isExt X`。

```agda
isExt : S → Type (ℓ-suc ℓ)
isExt X = (x y : S) → x ∈ᵗ X → y ∈ᵗ X
        → ((z : S) → z ∈ᵗ X → ⟨ z ∈ˢ x ⟩ → ⟨ z ∈ˢ y ⟩)
        → ((z : S) → z ∈ᵗ X → ⟨ z ∈ˢ y ⟩ → ⟨ z ∈ˢ x ⟩)
        → x ≡ y
```

塌缩映射对任意载体 `X` 一次性构造完成。把它包装成以 `X` 为参数的模块，使载体在其后每个引理中都保持显式。

从这里直到像的传递性，一切结论都对任意 `X : S` 成立；在外延性一节之前不需要对载体的任何假设。值得指出：Mostowski 塌缩的经典陈述常常预先假定良基性与外延性，而这里良基性由环境层级免费提供，外延性只在证明单射性时才登场。

```agda
module Collapse (X : S) where
```

## 递归塌缩

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

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

```agda
  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` 块把 `π` 标记为密封，即类型检查器不会在使用处自动展开它；这使提到 `π` 的证明项保持精简。

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

  opaque
    unfolding π
```

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

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

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

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

```agda
  π-member : (x z : S) → ⟨ z ∈ˢ π x ⟩
           → ∥ Σ[ y ∈ S ] (⟨ y ∈ˢ X ⟩ × (π y ≡ z)) ∥₁
  π-member x z z∈ = PT.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` 则直接复用。结果是用 `PT.map` 构造的截断对，因此尽管每个成分都是显式的，结论仍只是存在性陈述。

```agda
       → Σ[ 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` 重新打包。

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

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

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

```agda
    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` 属于像。证明用 `PT.rec` 消去截断的假设 `x∈πX`，这是合法的，因为目标 `⟨ y ∈ˢ πX ⟩` 是命题。每个满足 `π z ≡ x` 且 `z ∈ X` 的见证都把问题化为 `y ∈ π z`。

```agda
  π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 = PT.rec (snd (y ∈ˢ πX)) 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` 中的隶属已直接暴露了塌缩数据。

```agda
    go (z , z∈X , pzx) = PT.rec (snd (y ∈ˢ πX)) 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` 完成，塌缩的像是一个真正的传递集。

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

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

第一个成分是隶属证明的原像。把 `fiber x` 作用于 `yx : y ∈ᵗ x`，得到 `x` 的呈现中的一个实际索引 `m`，连同路径 `⟪ x ⟫↪ m ≡ y`。这正是为 `πX-intro` 提供见证的那条显式构造引理：由于嵌入的原像都是命题，截断的隶属可以消去到这个对类型中。

```agda
  π∈-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`，再用 `∈∈ₛ` 的前向一半把这条原生小隶属证书转换为小关系中的隶属。这是两种隶属直接相遇的唯一场合，`∈∈ₛ` 恰是桥。

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

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

```agda
    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` 是命题，因此用 `PT.rec` 消去截断是合法的。沿 `π x` 的计算律搬运假设，便把它化为 `step x` 所呈现集合的成员，其成员由 `Fiber x` 索引。

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

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

```agda
      (λ { (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` 的每个元素建立的性质。

```agda
  module InjExt (Xext : isExt X) where

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

外延性比较中的两个包含分别用恢复引理证明。第一方向把 `x` 的成员 `z` 移入 `y`：假设 `π x ≡ π y` 以及对 `x` 成员的归纳假设，结论为 `⟨ z ∈ˢ y ⟩`。

为证 `z` 属于 `y`，对目标集合 `y` 应用恢复引理：只需知道 `π z` 是 `π y` 的成员，且任何塌缩到 `π z` 的 `b ∈ y ∩ X` 都等于 `z`。隶属部分由前向引理得到：由于 `z` 是 `x` 的成员且二者都在 `X` 中，有 `⟨ π z ∈ˢ π x ⟩`，路径 `e : π x ≡ π y` 把它搬运为 `⟨ π z ∈ˢ π y ⟩`。

```agda
    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
```

比较原理正是归纳假设发挥作用之处。若 `b ∈ y ∩ X` 且 `π b ≡ π z`，则对称路径给出 `π z ≡ π b`，对 `x` 的成员 `z` 应用假设 `IH z` 得到 `z ≡ b`；再对称化即得原理所需的 `b ≡ z`。注意这一方向从不需要知道见证 `b` 实际存在，只需知道它若有会如何表现。

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

第二个包含沿相反方向运行同一论证，把 `y` 的成员 `z` 移入 `x`。两个包含合起来得到单射性的归纳步：在路径 `π x ≡ π y` 之下，两个集合恰有相同的 `X` 成员，结构外延性于是断言 `x ≡ y`。

证明是 `in⊆` 的镜像：对目标集合 `x` 应用恢复引理，而 `⟨ π z ∈ˢ π x ⟩` 来自在对 `(y, z)` 上的前向引理，再沿反向路径 `e` 搬运。唯一的不对称是给定路径的方向，它对应 `x` 与 `y` 角色的互换。

```agda
    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
```

这里的比较子句比 `in⊆` 中的简单：给定 `b ∈ x ∩ X` 与 `π b ≡ π z`，归纳假设 `IH b` 直接在 `b` 处适用，无需对称化便得 `b ≡ z`。恢复引理随后沿该路径把 `b ∈ᵗ x` 搬运为 `z ∈ᵗ x`，正如所需。

```agda
      (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
```

归纳步 `step-inj` 现在把两个包含组装成对载体外延性假设 `Xext` 的一次应用。给定 `x, y ∈ X` 与路径 `e : π x ≡ π y`，子句 `to` 与 `from` 正是 `isExt X` 所要求的比较，各自委托给 `in⊆` 或 `out⊆`，并以 `e` 的恰当定向。结论是路径 `x ≡ y`，故 `P x` 成立。

```agda
      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
```

单射性定理由 ∈ 归纳立即得到，因为每次调用 `step-inj` 恰是谓词 `P` 的归纳步。

无需新论证：对环境层级的隶属归纳从上面验证的步进为每个 `x` 产生 `P x`。展开 `P`，这恰是 `π` 在载体上的单射性：塌缩值相等的两个 `X` 元素相等。

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

有了单射性，同构的反向立即得到：塌缩的隶属可以追溯到载体中真正的隶属。

给定 `⟨ π y ∈ˢ π x ⟩`，恢复引理对仅仅存在的呈现见证进行消去：从指名某个 `b ∈ᵗ x` 且满足 `π b ≡ π y` 的纤维出发，它给出 `b ≡ y`，因为这里供给的比较子句直接应用 `π-inj` 得出该等式。正是单射性把恢复出的载体元素与 `y` 等同起来。再沿这条路径搬运 `b` 的隶属证书，便得到 `y ∈ᵗ x`。这一消去是合法的，因为其目标 `y ∈ᵗ x` 本身是命题，即命题值隶属的底层类型；见证 `b` 从未被选为数据，结论也只是这条命题值的隶属陈述。

```agda
    π∈-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)
```

把两个方向合起来便得到塌缩的同构解读：在载体上，隶属与塌缩后的隶属相互决定。

打包的结果是一对蕴含，而非等价类型：由 `⟨ y ∈ˢ x ⟩` 经前向引理到 `⟨ π y ∈ˢ π x ⟩`，再经 `π∈-bwd` 返回。这就是塌缩在载体上构成同构的精确含义：它保持且反映 `X` 的元素之间的隶属，并由 `π-inj` 在其上单射。

```agda
    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` 处的等式。

```agda
  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`。

```agda
    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)` 保证递归调用合法。这是良基递归定义的标准唯一性论证，适配到呈现集合的构造子上。

```agda
      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`，恰好对应证明中会遇到的情况。

```agda
  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π` 沿计算律搬运，再用 `PT.rec` 消去，露出 `Fiber y` 的一个纤维以及指名成员的 `π` 值等于 `x` 的路径。

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

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

```agda
        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 ⟩`。

```agda
          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`，再由 `∈∈ₛ` 的前向一半返回通常的隶属证明。

```agda
        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`，归纳完成。

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

不动点命题尤其适用于 `Y` 就是载体 `X` 本身的情形：传递的载体被塌缩逐点固定，因此在这样的载体上塌缩映射就是恒等映射。