---
title: "Mostowski 崩壊"
module: V.Collapse
lang: ja
site: "Bedrock"
description: "Mostowski 崩壊"
stage: "GCH の証明"
reading_order: 104
canonical: https://bedrock.institute/ja/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/zh/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 ℓ` に属し、得られる集合は正当に小さくなります。再帰のステップは新しい集合を提示します。インデックスがファイバーであり、各インデックスは、`x` の対応する要素 `⟪ x ⟫↪ m` への `rec` の適用を名指します。再帰呼び出しを正当化するため、所属証明 `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` が、再帰呼び出しを `π y` とした `step x` の提示する集合とパスで等しい、というものです。この規則は同じ再帰原理の伴う定理 `∈-induction-compute` がそのまま供給するので、新たな証明は要りません。以後の節では定義を展開する代わりに、このパスに沿って所属の証明を輸送します。

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

`π` の最初の性質はその要素を特徴づけます。`z` が `π x` に属するなら、台のある要素の崩壊が `z` に等しいことが単に存在します。この主張は切り詰められています。そのような要素を選ぶのではなく、そのような組の型が住まれていることだけを示すのです。

証明は所属の証拠 `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)` です。この節では、任意の崩壊値の要素が再び台の要素の崩壊である、すなわち `π-member` の内容だけを使って、`πX` が推移的であることを示します。

集合 `πX` は `π` を `X` に制限した像であり、台そのものの提示のインデックス型 `⟪ X ⟫` の上に `sett` で構成されます。その要素に関する補題はこの提示をそのまま読んだものです。`πX` の要素は、`X` のある `y` に対する `π 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` も像に属します。証明は切り詰められた仮定 `x∈πX` を `PT.rec` で消去します。目標の `⟨ y ∈ˢ πX ⟩` が命題であるため、これは正当です。`π z ≡ x` かつ `z ∈ X` を満たす各証拠 `z` は、問題を `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)` が `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))
```

`x` の要素として `b = ⟪ x ⟫↪ (p .fst)` を名指すファイバー `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` に対し、同じ崩壊値を持つ `X` の任意の `y` がパスによって `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` に崩壊する `y ∩ X` の任意の `b` が `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` は、`π` とどこでも一致します。この一意性により、崩壊は構成の多数の出力のひとつではなく、well-defined な対象になります。

主張は、計算規則 `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)))
```

途中のパスそのものは、提示する関数への同一性 (congruence) の適用です。`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π` を計算規則に沿って輸送してから消去し、`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 ∈ᵗ 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` そのものである場合に特に当てはまります。推移的な台は崩壊によって各点で固定され、そのような台の上では崩壊写像は恒等写像になります。