--- title: "累積階層" module: V.Hierarchy lang: ja site: "Bedrock" description: "累積階層" stage: "周囲の累積階層" reading_order: 20 canonical: https://bedrock.institute/ja/V.Hierarchy.html html: V.Hierarchy.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/Hierarchy.lagda.md prerequisites: [Base.Prelude, FOL.ZFStructure] routes: [ambient-model] translations: [https://bedrock.institute/en/V.Hierarchy.md, https://bedrock.institute/zh/V.Hierarchy.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # 累積階層 集合論の言語のモデルにはどれも、「集合」からなる台と、命題に値を持つ等号と所属関係が要ります。本章はその台を構成します。累積階層 `V` は高階帰納型であり、土台にあるのは集合論最古の考え、すなわち集合とはその要素の集まりにほかならないというものです。この型はこの考えをそのまま形にします。すべての集合は、小さな型をインデックスとする集合の族によって表示され、各インデックスが一つの要素に対応します。ある集合の要素であるとは、その族のどれかのインデックスがその要素に命中することにほかなりません。同じ要素を持つ二つの表示は同じ集合を表示します。したがって外延性は、このモデルが要求すべき公理ではなく、型の構成のされ方そのものなのです。 本章はこの台の上に構造 `𝒮ᵥ` を組み立て、外延性から所属関係に沿う再帰原理まで、集合論の最初の性質を証明します。構造の求めるものは、階層が本来の形で供給します。集合の間の等号はパス型であり、階層が h-集合であるため命題値になります。所属関係は階層本来の `∈` で、はじめから `hProp` に値を取ります。本章は宇宙レベル `ℓ` を一度だけ固定し、全章の構成をこのレベルで述べます。 ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module V.Hierarchy {ℓ : Level} where open import FOL.ZFStructure using ( ZFStructure; module hPropStructure ) ``` 本章で最も難しい証明を支えるのは、二つの考えです。第一は命題的切り詰めです。「あるインデックスが条件を満たす」という主張は、証人を選ばない純粋な存在として保たれ、切り詰められた主張は命題へしか消去できません。第二は到達可能性です。これは整礎な関係に伴う帰納的データ `Acc` であり、ある要素からその要素の下降の各一歩が、それ自体到達可能な要素に着地するとき、その要素は到達可能です。この二つが噛み合うのは、階層への所属そのものが切り詰められているからです。整礎性の証明は、切り詰められた形でしか存在しないインデックスを、到達可能性の証明へ変えなければなりません。到達可能性はまさに命題です。 ```agda import Cubical.HITs.PropositionalTruncation as PT import Cubical.Data.Empty as Empty import Cubical.Induction.WellFounded as WellFoundedInduction open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded; isPropAcc; wf→x≮x ) open import Cubical.HITs.CumulativeHierarchy.Base ``` まずは階層そのものをじっくり読みましょう。この後の議論はすべてそれの上に立ちます。構成子 `sett` は、小さなインデックス型と階層への族から、その族の像である集合を形作ります。所属 `y ∈ sett X ix` は切り詰められた原像であり、`ix i ≡ y` となる `i : X` があるとき、そしてそのときにしか成り立ちません。パス構成子は、要素の一致する任意の二つの `sett` 表示を同一視します。これは型そのものに組み込まれた外延性です。この型がここで定義されるのではなく、本章はその上に構造 `𝒮ᵥ` を組み立て、その構造の集合論的性質を証明します。 ```agda using ( V; setIsSet; _∈_; elimProp ) open import Cubical.HITs.CumulativeHierarchy.Base using ( sett ) -- lint-agda: keep (prose references link through this import) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ; extensionality ) ``` ## 高階帰納型 基本となる考えは集合論で最も古いものです。集合とはその要素の集まりにほかりません。この型はこの考えをデータとして実現し、注意すべき制約を二つ伴います。インデックス型は小さくなければならず、`X : Type ℓ` の形をします。したがって各集合は大きさ `ℓ` のデータから組み立てられます。また、型全体は `setIsSet` によって h-集合なので、表示がどう同一視されようと、結果のあいだにはそれ以上の区別できる構造は残りません。 ## 構造 構成で問うのは、構造の record が何を要求するかです。ここでの答えは、階層がすでにそのすべてを備えている、というものです。集合からなる台としては `V ℓ` があり、h-集合性は追加の要件ではなく、階層がみずから証明する事実です。命題に値を持つ等号としては、h-集合の要素の間のパスが命題をなすので、パス型がそれになります。命題に値を持つ所属関係としては、階層本来の `∈` がはじめから `hProp` にあります。新たに作るべきものは何もなく、これらのフィールドが構造 `𝒮ᵥ` に組み上がり、一階の言語はこの構造の上で解釈されます。添字は階層を指す普通の `v` です。 等号のフィールドはこの選択を明示します。`_≈ˢ_` は `x` と `y` を、パス型 `x ≡ y` と「この型が命題である」ことの証明 `setIsSet x y` の対へ送ります。これは `hProp (ℓ-suc ℓ)` の要素の形そのものです。同じ h-集合性の定理は、構造の中で二つの役割を持ちます。`setIsSet` はフィールド `isSetS` を与え、`setIsSet x y` は等号として用いるパス型が命題であることを証明します。パスそのものを変換する必要はありません。h-集合に対しては、二つの要素の間のパス型はもともと命題であり、フィールドはその型を、それに伴う証明とともに記録しているだけです。 ```agda 𝒮ᵥ : ZFStructure (ℓ-suc ℓ) 𝒮ᵥ = record { S = V ℓ ; isSetS = setIsSet ; _≈ˢ_ = λ x y → (x ≡ y) , setIsSet x y ``` 所属関係のフィールド `_∈ˢ_` は階層本来の `∈` そのものであり、各対での値ははじめから `hProp (ℓ-suc ℓ)` の中にあります。構造の関係は命題値なので、以後の多くの議論では、命題そのものではなくその基礎型が必要になります。`hPropStructure 𝒮ᵥ` を開くと、この読み方が `x ∈ᵗ y` として得られます。これは所属命題の要素のなす型 `⟨ x ∈ˢ y ⟩` を表します。両者は同じ関係の二つの読み方で、`∈ˢ` が命題を、`∈ᵗ` がその基礎型を与えます。後の整礎性と帰納は、この読みの上に築かれます。 ```agda ; _∈ˢ_ = _∈_ } open hPropStructure 𝒮ᵥ ``` 証明を始める前に、階層の位置を一度見ておきましょう。台 `V ℓ` は `Type (ℓ-suc ℓ)` に住み、そのインデックス型より一つ上の宇宙にあり、関係の値もそれに並んで `hProp (ℓ-suc ℓ)` に住みます。階層は小さなインデックスデータから作られた大きな型です。`∈∈ₛ` によって大きな所属関係と結ばれる小さな所属関係 `∈ₛ` は、この後の証明にも現れます。 ## 外延性と所属関係の整礎性 二つの集合 `a` と `b` が各点で一致すると仮定します。つまり各 `x` に対して、命題 `x ∈ a` と `x ∈ b` の間のパスがあるとします。すると `a` の任意の要素はそのパスに沿って `b` の要素へ輸送でき、その逆もできるので、`a` と `b` は互いを包含します。ライブラリの `extensionality` はまさにこの相互包含をパス `a ≡ b` へ変換し、`subst` が各点のパスに沿って所属を輸送することでそれを作ります。階層の外延性はしたがって追加の仮定ではなく、その定義の帰結です。 ```agda extensionalV : {a b : V ℓ} → ((x : V ℓ) → (x ∈ a) ≡ (x ∈ b)) → a ≡ b extensionalV {a} {b} h = extensionality a b ( (λ x x∈ₛa → ∈∈ₛ {a = x} {b = b} .fst (subst ⟨_⟩ (h x) (∈∈ₛ {a = x} {b = a} .snd x∈ₛa))) , (λ x x∈ₛb → ∈∈ₛ {a = x} {b = a} .fst ``` 仮定 `h` は、各 `x` に対して命題 `x ∈ a` と `x ∈ b` の間のパスを与えます。目標はパス `a ≡ b` です。ライブラリの `extensionality` は小さな所属関係を期待するので、証明は橋 `∈∈ₛ` を一方向に通ります。入力 `x∈ₛa` は `x` の `a` への小所属関係です。その変換 `∈∈ₛ .snd x∈ₛa` は小から大へ向かい、`x ∈ a` の要素を生成します。次に `subst ⟨_⟩ (h x)` がその要素を各点のパスに沿って輸送します。`h x` は二つの所属命題が `x` で一致することを言うので、輸送された値は `x ∈ b` に住みます。最後に `∈∈ₛ .fst` が大から小へ戻し、`x` の `b` への小所属関係が得られます。これが `extensionality` が入力として受け取る相互包含の前方の成分です。 ```agda (subst ⟨_⟩ (sym (h x)) (∈∈ₛ {a = x} {b = b} .snd x∈ₛb))) ) ``` 第二の成分は、同じ橋を逆向きに通るものです。`x` の `b` への小所属関係を大へ変換し、`sym (h x)` に沿って逆方向へ輸送し、`x` の `a` への小所属関係へ戻します。二つの成分が合わさって相互包含が得られ、`extensionality` はそこから `a ≡ b` を作ります。これが `extensionalV` が返すパスです。 (`∈∈ₛ` を通して現れる `∈ₛ` はライブラリの**小さな**所属関係であり、「集合の小さな提示」の章で詳しく述べます。ここでは両者を結ぶ役割だけを果たします。) 本書における正則性は、所属関係が整礎であるという主張です。すなわち、台のすべての要素が `∈ᵗ` の下で到達可能である、というものです。その意味は、上で導入した到達可能性のデータ `Acc` にあります。証明は、この高階帰納型を族 `λ s → Acc _∈ᵗ_ s` へ消去することによって進みます。任意の族への消去はいつでもできるわけではなく、ここでそれが許されるのは、各 `Acc _∈ᵗ_ s` が命題であり、`isPropAcc s` がまさにその証明を与えるからです。`sett` の場合、分岐は族 `ix` と、各インデックスについて `rec i : Acc _∈ᵗ_ (ix i)` を与える帰納仮定を受け取ります。組み立てるべきは `Acc _∈ᵗ_ (sett X ix)` であり、`acc` の形から、これは集合の任意の要素 `y` に対する到達可能性を与えることにほかなりません。 ```agda regularityV : WellFounded _∈ᵗ_ regularityV = elimProp (λ s → isPropAcc s) (λ X ix rec → acc (λ y y∈ → PT.rec (isPropAcc y) (λ { (i , p) → subst (Acc _∈ᵗ_) p (rec i) }) ``` このような要素 `y` に対し、証拠 `y∈` が与えるのは、`p : ix i ≡ y` を持つ対 `(i , p)` の命題的切り詰めだけです。`PT.rec (isPropAcc y)` がこの切り詰められた原像を消去できるのは、実際の目標 `Acc _∈ᵗ_ y` が命題であり、`isPropAcc y` がその命題性を証明するからです。分岐の中では `subst (Acc _∈ᵗ_) p (rec i)` が帰納仮定を `ix i` から `y` へ輸送します。証明全体として、インデックスは使われますが、大域的に一つを選ぶことはありません。 ```agda y∈)) ``` 正則性の最初の帰結は非反射性です。集合は自分自身に属しません。到達可能性の言葉で言えば、これはすぐに分かります。自分自身と整礎な関係に立つ要素は、到達可能性のデータと矛盾します。下降の各一歩が到達可能な要素に着地することを、到達可能性は要求するからです。ここでの導出は、上で証明した `Acc` の主張を使うものであり、Foundation のすべての古典的定式化を捉えると主張するものではありません。 仮定 `⟨ A ∈ˢ A ⟩` は、所属命題の基礎型の要素であり、これは `regularityV` が証明された関係 `∈ᵗ` そのものです。整礎な関係に対しては、どの要素も自分自身とその関係に立つことはできません。これがライブラリの非反射性の定理 `wf→x≮x` であり、ここでは `regularityV` を整礎性の入力として適用します。結果は矛盾であり、空の型 `Empty.⊥` がそれを示します。 ```agda ∈-irrefl : (A : S) → ⟨ A ∈ˢ A ⟩ → Empty.⊥ ∈-irrefl A = wf→x≮x regularityV {x = A} ``` ## 所属関係上の再帰 整礎性には計算上の見返りがあります。整礎な関係は再帰を支えるのです。具体的には、`x` での値は `x` の各要素 `y` での値に依存でき、所属関係が整礎であるためこの依存は必ず停止します。対象は命題に限らず任意の依存型族 `P` でよく、これがこの原理を証明原理にとどまらない再帰原理にしています。これは所属関係に沿う再帰の型論的形態であり、序数で添字付けられた階層を介さずに述べられます。段階の添字に沿って再帰するのではなく、所属関係そのものに沿って再帰するのです。再帰方程式も命題としての等式で成り立つため、後の議論はそれを頼りに計算できます。 `∈-induction` の型は外から内へ読みます。型族 `P` は各集合に対して任意の宇宙 `Type ℓ'` の型を割り当てるので、構成される値は集合とともに実際に変わりえます。ステップ関数 `e` は集合 `x` と、`x` の各要素 `y` での再帰的な値 `P y` を受け取ります。所属関係は所属命題を Type として読む `∈ᵗ` を通して現れます。そして `P x` を返します。この定義を正当化するのは `regularityV` です。ライブラリの `WFI.induction` をこの整礎な関係で実例化すれば、ステップ関数が全域の族へ変わります。ここで整礎性を改めて証明する必要はありません。 ```agda ∈-induction : ∀ {ℓ'} {P : V ℓ → Type ℓ'} → (∀ x → (∀ y → y ∈ᵗ x → P y) → P x) → ∀ x → P x ∈-induction = WellFoundedInduction.WFI.induction regularityV ∈-induction-compute : ∀ {ℓ'} {P : V ℓ → Type ℓ'} ``` 計算法則は、各要素での再帰呼び出しを定義の内側に隠さず、等式として示します。すなわち `∈-induction e x` は、ステップ関数を `x` と各要素 `y` での `∈-induction e y` に適用したものに等しい、ということです。この等式は命題としての等式として述べられており、定義的に成り立つとは限りません。それを明示しておけば、簡約が定義的でない場合でも、後の証明はこの等式によって再帰的に定義された値を書き換えられます。この法則はライブラリの `WFI.induction-compute` であり、任意の整礎な関係に対して証明され、ここでは所属関係に実例化されています。 ```agda (e : ∀ x → (∀ y → y ∈ᵗ x → P y) → P x) (x : V ℓ) → ∈-induction e x ≡ e x (λ y _ → ∈-induction e y) ∈-induction-compute = WellFoundedInduction.WFI.induction-compute regularityV ``` ## まとめ 階層 `V` は高階帰納型であり、集合は小さな族の像で、型全体は h-集合です。構造 `𝒮ᵥ` に組み上げると、等号にはパス型が、所属関係には本来の `∈` が入ります。どちらも命題値です。外延性 (`extensionalV`) は小所属関係の橋を経て外延的なパス構成子から、所属関係の整礎性 (`regularityV`) は到達可能性への消去から従います。整礎性はさらに非反射性と、再帰原理 `∈-induction` とその計算法則 `∈-induction-compute` をもたらします。小さな所属関係 `∈ₛ` とその `∈` への橋は、「集合の小さな提示」の章で扱われます。