Mostowski 塌缩

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

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

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

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 本身提出什么要求。

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 ℓ)，因为它量化结构元素并返回层级 ℓ 的命题。

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。

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 塌缩的经典陈述常常预先假定良基性与外延性，而这里良基性由环境层级免费提供，外延性只在证明单射性时才登场。

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；载体隶属的见证作为数据随纤维一起携带。

  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∈ = 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 构造的截断对，因此尽管每个成分都是显式的，结论仍只是存在性陈述。

       → Σ[ 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∈ = PT.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 属于像。证明用 PT.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 = 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 中的隶属已直接暴露了塌缩数据。

    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 完成，塌缩的像是一个真正的传递集。

      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 提供见证的那条显式构造引理：由于嵌入的原像都是命题，截断的隶属可以消去到这个对类型中。

  π∈-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) 已 inhabit 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 是命题，因此用 PT.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 = 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，这正是目标。

      (λ { (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

外延性比较中的两个包含分别用恢复引理证明。第一方向把 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 ⟩。

    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 实际存在，只需知道它若有会如何表现。

      (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 角色的互换。

    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，正如所需。

      (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 成立。

      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 元素相等。

    π-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 从未被选为数据，结论也只是这条命题值的隶属陈述。

    π∈-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 在其上单射。

    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π 沿计算律搬运，再用 PT.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π = PT.rec (snd (x ∈ˢ y)) 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))

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