--- title: "累積階層は ZF と ZFC のモデル" module: V.Model lang: ja site: "Bedrock" description: "累積階層は ZF と ZFC のモデル" stage: "周囲の累積階層" reading_order: 22 canonical: https://bedrock.institute/ja/V.Model.html html: V.Model.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/Model.lagda.md prerequisites: [Base.Prelude, Base.Impredicativity, Base.Classical, Base.Choice, FOL.ZFStructure, FOL.Syntax, FOL.Semantics, FOL.ZFModel, V.Hierarchy, V.Smallness] routes: [ambient-model] translations: [https://bedrock.institute/en/V.Model.md, https://bedrock.institute/zh/V.Model.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # 累積階層は ZF と ZFC のモデル 本章は、固定した一つの宇宙レベル `ℓ` の上で、累積階層の内側に ZF の各公理を実現します。集合の存在を要求する各公理については、その集合を構成し、所属関係が真理値のパスとして要求された記述にちょうど等しいことを証明します。関係する仮定は初めに区別しておく価値があります。基本的な構成、すなわち空集合、対、和集合は、階層自身の集合構成子の代償しか要らず、置換も同様で、その構成子の所属規則から直接読み取れます。完全な分出には命題リサイズが必要で、各充足命題に一段低い宇宙の代表を与えます。冪集合には命題の小分類子 `HPropSmallness` が必要です。リサイズと分類子は `Impredicativity` としてひとまとめにされ、組み立てられた ZF の定理 `V⊨ZF` はちょうど `LEM (ℓ-suc ℓ)` を仮定し、パッキングはそこから従います。ZFC の部分では、定理 `V⊨ZFC` がレベル `ℓ-suc ℓ` の集合レベルの選択を別に仮定します。ディアコネスクの定理により、これは ZF の部分に使う排中律を含意し、一段下げれば選択集合の公理を供給します。本章は、階層がすでに持つ構成を公理の要求する正確な形へ一公理ずつ変換し、この二つの定理へ至ります。 宇宙レベルの計算は正確で、一度読んでおくべきものです。モデルの台はレベル `ℓ` の階層 `S` であり、それ自身 `Type (ℓ-suc ℓ)` の要素です。モデルの等号と所属を担う真理値は `hProp (ℓ-suc ℓ)` に住みます。パッキング `Impredicativity ℓ` は、以下で使う二つの小ささの原理、すなわちこの真理値レベルでの `resizing` と、`hProp ℓ` 全体と同値な小さな型である小分類子 `HPropSmallness ℓ` を結び付けます。選択の補題はレベル `ℓ` の集合レベルの選択を消費し、最後の二つの帰結はそれぞれ `LEM (ℓ-suc ℓ)` と `SetChoice (ℓ-suc ℓ)` を仮定します。したがってすべての仮定を支配する単一の一律のレベルはなく、各原理はその主張が意味を持つちょうどその場所で取られます。 ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module V.Model {ℓ : Level} where open import Base.Impredicativity using ( HPropSmallness; Impredicativity ) ``` 「階層が公理を満たす」とは形式的にはどういう意味でしょうか。一階論理の諸章が語彙を供給します。構造とは h-集合である台のことであり、その等号と所属は、固定された二元型のブール値ではなく真理値を取ります。論理式は対象言語の構文の要素であり、公理のスキーマはその自由変数の枠を量化します。充足は、台の要素からなる環境のもとで論理式を読み、真理値を返す関係です。以下では ZF の公理を、まさにこの言葉で一つずつ導き直します。 ```agda open import Base.Classical using ( LEM; lem→impredicativity ) open import Base.Choice using ( SetChoice; choice→lem; lowerSetChoice ) open import FOL.ZFStructure using ( ZFStructure ) open import FOL.Syntax using ( Formula ) import FOL.Semantics ``` 階層が提供するのは構造 `𝒮ᵥ` です。その等号は高次帰納型 `V ℓ` のパス型であり、所属は階層本来の `∈` です。この構造の外延性と正則性は階層そのものの章で証明済みで、ここでは再証明せずに引用します。さらに小ささの章から一つの道具を持ち越します。各値が小さい述語から集合を作る適合装置で、リサイズが小ささを供給しだい完全な分出になります。全体を通じて、命題の間の双条件は標準の書き換え `⇔toPath` で真理値の間のパスに変えられます。以下の仕様のほとんどすべてがこの一手で終わります。 ```agda import FOL.ZFModel open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV ) open import V.Smallness {ℓ} using ( separateFromSmall ) open import Cubical.Foundations.Equiv using ( equivFun; invEq; secEq ) open import Cubical.Functions.Logic using ( ⇔toPath ) ``` cubical の三つの一般的な事実が後の証明を形作ります。等号の型が命題である型への埋め込みは単射であり、復元した添字が唯一の可能性であることを示す場面で効きます。第二成分が命題である依存対の間のパスは、第一射影の間のパスで決まります。さらに、像の集合への所属の主張はたいてい切り詰められた存在の形をしており、`∣_∣₁` で導入し、`PT.rec` で命題値の目標へ消去します。矛盾は空の型で扱います。 ```agda open import Cubical.Functions.Embedding using ( Embedding-into-isSet→isSet; isEmbedding→Inj ) open import Cubical.Data.Sigma using ( Σ≡Prop ) import Cubical.Data.Sum as Sum import Cubical.Data.Empty as Empty ``` 中心となる構成は集合の構成子 `sett` です。小さな添字の型 `X` と族 `X → S` から像の集合を作り、所属 `y ∈ sett X ix` は、ある添字が `y` を呈示することが純粋に存在するとき、そのときに限り成ります。置換はこの所属の規則から直接読み取ります。階層が h-集合であること (`setIsSet` が記録します) により、パス型 `x ≡ y` は命題となり、構造の等号の正当な真理値になります。 ```agda import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( sett; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Properties ``` 所属には二つの形があり、章全体がこの間を行き来します。すべての集合 `a` は小さな添字の型 `⟪ a ⟫` と、像がちょうど `a` である埋め込み `⟪ a ⟫↪` を持ち、小さな所属 `x ∈ₛ a` はある添字が `x` を呈示することを言います。同値 `∈∈ₛ` が小さな所属と通常の所属を双方向に各点で取り替え、`∈-asFiber` はさらに進んで、`x ∈ a` の証明から添字と呈示するパスの対を切り詰めずに実際に返します。この切り詰められていないことが、添字の復元を選択ではなく関数にします。基本的な集合も用意済みです。反駁 `∅-empty` を持つ空集合、対 `⁅ a , b ⁆` と `pairing-ax`、和 `⋃ a` と `union-ax`、分類を持つ一元集合 `⁅ a ⁆s`、そして二項和 `_∪_` です。 ```agda using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber ; identityPrinciple; _⊆_; extensionality ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; ∅-empty; ⁅_,_⁆; pairing-ax; ⋃_; union-ax; ⁅_⁆s; _∪_ ; SingletonPackage; module InfinitySet ) ``` 一つの具体的な変換が、これからのすべての仕様の証明が使う方法を示します。対について、ライブラリの `pairing-ax` は `x ∈ₛ ⁅ a , b ⁆` と選言 `x ≡ₕ a ⊔ x ≡ₕ b` の双条件を述べます。この構造にとって `≡ₕ u v` はパス型 `u ≡ v` であり、構造の `≈ˢ u v` と定義により同じです。したがって次の節で証明される対の仕様は、`pairing-ax` に `⇔toPath` を適用し、両方向で `∈∈ₛ` を一層だけ通すだけです。順方向は通常の所属を分類が消費する小さな所属へ、逆方向は得られた選言を通常の所属へ戻します。同じ三手順が空集合、和、そして (切り詰めをもう一段加えて) 添字付きの族の和への所属を変換します。 ```agda open import Cubical.HITs.CumulativeHierarchy.Constructions using ( SetPackage ) -- lint-agda: keep (used qualified: SetPackage.classification) open InfinitySet using ( sucV; #_; ω ) open ZFStructure 𝒮ᵥ ``` これらの変換の目標は record `isZFModel` で、その欄は ZF の公理そのものです。外延性、正則性、空集合、対、和、分出、置換、冪集合、そして数項の列と二つの固定方程式で表される強い無限です。各存在の欄は `isContr (SetOf Q)`、すなわちクラス `Q` を実現する集合と一意性のデータを要求し、一意性は外延性が供給します。`isZFCModel` は選択集合の欄を加えます。深く埋め込まれた論理式の充足はこの構造上で具体化されます。`(y ∷ x ∷ []) ⊨ φ` は、アリティ 2 の論理式 `φ` を、最初の自由変数の枠に `y` を、次の枠に `x` を割り当てる環境のもとで読むことを意味します。各公理のスキーマはパラメータの関数として与えられるので、すべての論理式に対するすべての実例が一度に成ります。 ```agda module Model = FOL.ZFModel 𝒮ᵥ open Model using ( SetOf; _⊆ˢ_; setOf-unique; isZFModel; isZFCModel ) module SemanticsV = FOL.Semantics 𝒮ᵥ open SemanticsV.At S id using ( _⊨_ ) ``` ## 基本的な集合 空集合、対、和集合は最も簡単に満たせる欄です。構成とその分類が階層のライブラリにすでにあるからです。残るのは主張の形を整えることだけです。モデルのレコードに対する仕様とは真理値の等式、それもパスであり、台の各要素 `x` について真理値 `x ∈ˢ b` がクラスの記述 `Q x` とパスとして等しくなければなりません。ライブラリは公理を小さな所属 `∈ₛ` を通して述べるので、変換は毎回同じ三手順です。`∈∈ₛ` が小さな所属と通常の所属を各点で取り替え、ライブラリの分類が対応する双条件を供給し、`⇔toPath` がその双条件を要求されるパスに書き換えます。最も対応が直接的なのは対で、ライブラリの「`a` と等しいか `b` と等しい」は欄の `(x ≈ˢ a) ⊔ (x ≈ˢ b)` と定義により同じなので、真の仕事は `∈∈ₛ` の一層だけです。 空集合の仕様は、台の各要素 `x` について、真理値 `x ∈ˢ ∅` がパスとして偽 `⊥` とちょうど一致することを求めます。これは本章の基本変換の縮図です。ライブラリが示すのは、`∅` が小さな所属 `∈ₛ` の意味で元を持たないことなので、まず二つの所属を各点で交換します。順方向では、`∈∈ₛ` が `x ∈ˢ ∅` の証明を `∅-empty` が反駁する小さな所属へ変え、この矛盾から空の型の要素が得られ、まさに含意の要求を満たします。逆方向は構成すべきものがありません。`⊥` には要素がないからです。`⇔toPath` が最後に、得られた命題間の双条件を仕様の要求する真理値のパスへ変換します。 ```agda empty-spec : (x : S) → (x ∈ˢ ∅) ≡ ⊥ empty-spec x = ⇔toPath (λ x∈ → Empty.rec (∅-empty x (∈∈ₛ {a = x} {b = ∅} .fst x∈))) (λ ()) pair-spec : (a b x : S) → (x ∈ˢ ⁅ a , b ⁆) ≡ ((x ≈ˢ a) ⊔ (x ≈ˢ b)) ``` 対は、`⁅ a , b ⁆` への所属が「`a` と等しいか `b` と等しいか」の選言に等しいことを求めます。等しさは構造の `≈ˢ` として読みます。ライブラリの `pairing-ax` は、小さな所属 `x ∈ₛ ⁅ a , b ⁆` と「`a` または `b` との小さな等しさ」の選言との双条件を述べ、その命題の部分はすでに目標の形と一致しています。順方向では、`∈∈ₛ` の一度の適用が通常の所属 `x ∈ˢ ⁅ a , b ⁆` を `pairing-ax` の消費する小形式へ変え、その第一方向が選言を返します。逆方向では、`pairing-ax` の第二方向が小さな所属を与え、`∈∈ₛ` のもう半分がそれを通常の所属へ引き上げます。各方向は、ライブラリの結果の一度の適用に所属記法の交換を一層かぶせただけです。 ```agda pair-spec a b x = ⇔toPath (λ x∈ → pairing-ax a b x .fst (∈∈ₛ {a = x} {b = ⁅ a , b ⁆} .fst x∈)) (λ h → ∈∈ₛ {a = x} {b = ⁅ a , b ⁆} .snd (pairing-ax a b x .snd h)) union-spec : (a x : S) → (x ∈ˢ (⋃ a)) ≡ (∃[ y ∶ S ] (y ∈ˢ a) ⊓ (x ∈ˢ y)) union-spec a x = ⇔toPath ``` 和は存在の形をもつ最初の仕様です。`⋃ a` への所属は、「ある `y` が `a` に属し `x` が `y` に属する」という切り詰められた主張に等しいはずです。順方向では、`union-ax` がまさにそのような切り詰められた三つ組 `(v , v ∈ a , x ∈ v)` を与えますが、二つの所属がともに小形式です。書き換えは命題の截断の内部で行われ、目標も命題なので、`PT.map` が証人をその場で変えます。`∈∈ₛ` が `v ∈ₛ a` を `a` の通常の要素へ、`x ∈ₛ v` を `v` の通常の要素へ変えます。結果は添字付き選言 `∃[ x ] P x の証人、すなわち`hProp` 上で台を量化する単なる存在の主張であり、どの元も選ばれません。 ```agda (λ x∈ → PT.map (λ { (v , va , xv) → v , ∈∈ₛ {a = v} {b = a} .snd va , ∈∈ₛ {a = x} {b = v} .snd xv }) (union-ax a x .fst (∈∈ₛ {a = x} {b = ⋃ a} .fst x∈))) (λ h → ∈∈ₛ {a = x} {b = ⋃ a} .snd (union-ax a x .snd (PT.map ``` 逆方向は同じ交換を逆向きに行います。添字付き選言の切り詰められた証人から出発し、`PT.map` が各場合 `(v , v ∈ a , x ∈ v)` に対して `∈∈ₛ` の逆向きで `union-ax` の消費する小形式の三つ組を組み立てます。その第二方向が `⋃ a` への小さな所属を返し、`∈∈ₛ` のもう半分がそれを通常の所属へ引き上げます。二つの方向を合わせると仕様の要求する真理値のパスが得られ、いずれも一つのライブラリの分類と各点の所属記法の交換から来ます。 ```agda (λ { (v , va , xv) → v , ∈∈ₛ {a = v} {b = a} .fst va , ∈∈ₛ {a = x} {b = v} .fst xv }) h))) ``` 本章の目標は、一つの固定した宇宙レベル `ℓ` の上で、累積階層の内側に ZF の各公理を実現することです。構造 `𝒮ᵥ` は真理値を返す等号と所属を備えた台 `S` を持ち、モデルの record は各公理について、その所属がパスとして定められた記述に等しい集合を要求します。仮定は部分によって異なるので、分けて述べる価値があります。基本的な構成、すなわち空集合、対、和、無限と、置換の議論全体には、追加の仮定はまったく要りません。完全な分出には命題リサイズが必要で、各論理式の充足が点ごとに小さな命題になります。冪集合には小分類子 `HPropSmallness`、つまり `hProp ℓ` 全体と同値な小さな型が必要です。まとめられた帰結は合算のコストを記録します。`V⊨ZF` はちょうど `LEM (ℓ-suc ℓ)` を仮定し、`V⊨ZFC` はちょうど `SetChoice (ℓ-suc ℓ)` を仮定します。この節は仮定の不要な側にとどまり、まず一つの集合の和、次に添字付きの族 `f : X → S` の和について、基本的な所属の仕様を展開します。集合 `⋃ (sett X f)` は中間の集合を通して族の値を集めますが、この和への所属をある族の元への所属として直接読めることは有益です。`union-spec` を展開すると和の元 `v` にわたる切り詰められた存在式が得られ、そのような `v` はそれぞれ `sett` の添字で呈示されるため、その上に第二の切り詰めの層が乗ります。以下の二つの補題は、各方向でこの層を一つへまとめます。 内向きの補題は、一つの具体的な所属 `x ∈ f i` を和全体への所属へ変えます。証人は探し出すのではなく書き下されます。中間の要素は `f i` そのものであり、添字 `i` が自反なパスで呈示し、`h` が `x` がそこに属することを証明します。`union-spec` は真理値の等式なので、`subst ⟨_⟩` が逆向きの仕様に沿ってこの証人を運び、切り詰められた三つ組が和の特徴付けの期待するちょうどその形で消費されます。`union-spec` 自身のほかには何も入りません。 ```agda union-family-in : (X : Type ℓ) (f : X → S) (i : X) (x : S) → ⟨ x ∈ˢ f i ⟩ → ⟨ x ∈ˢ (⋃ (sett X f)) ⟩ union-family-in X f i x h = subst ⟨_⟩ (sym (union-spec (sett X f) x)) ∣ f i , ∣ i , refl ∣₁ , h ∣₁ union-family-out : (X : Type ℓ) (f : X → S) (x : S) ``` 外向きの補題は、和への所属から「`x` を含む族の元が純粋に存在する」ことを取り出します。`union-spec` を展開すると、切り詰められた三つ組 `(v , v は和に属する , x は v に属する)` が得られます。第二成分は `v` が添字で呈示されると言うので、截断の内部でさらに `PT.map` を行い、`f i ≡ v` なる対 `(i , q)` を取り出します。そして `v` における `x` の所属を `q` の逆向きに沿って運び、`f i` に着地させます。目標は截断を保つので、消去には `squash₁` を命題性の証拠として `PT.rec` で `∥ Σ[ i ] ⟨ x ∈ˢ f i ⟩ ∥₁` に入ります。結論は純粋な存在のままです。ある族の元が `x` を含むのであり、どの元も選ばれません。 ```agda → ⟨ x ∈ˢ (⋃ (sett X f)) ⟩ → ∥ Σ[ i ∈ X ] ⟨ x ∈ˢ f i ⟩ ∥₁ union-family-out X f x h = PT.rec PT.squash₁ (λ { (v , hv , hx) → PT.map (λ { (i , q) → i , subst (λ w → ⟨ x ∈ˢ w ⟩) (sym q) hx }) hv }) (subst ⟨_⟩ (union-spec (sett X f) x) h) ``` ## 追加の公理を要しない置換 置換は図式形式の公理で、通常の集合論では、各集合 `a` と `a` 上で関数的な論理式 `φ` に対して像の存在を公理として要請します。ここでは階層そのものが構成を与え、選択原理は一切呼びません。関数性の仮定は緊縮性として述べられます。`a` の各元 `x` に対し、`(y ∷ x ∷ []) ⊨ φ` を満たす `y` の型が緊縮的であり、中心の値には、他のすべての値がそれと同一視されることの証明が伴います。緊縮性が実際のデータを与えるため、この中心の値を読み出して像の構成に使えます。ただし `a` の元は小さな提示を通してしか与えられず、各元は型 `⟪ a ⟫` のある添字 `m` に対して `⟪ a ⟫↪ m` として現れます。そこで構成は像に `⟪ a ⟫` 自身で添字を付けます。繊細になりうる段階、すなわち所属の事実から添字を復元する作業は、`∈-asFiber` の提示のファイバーが切り詰められていないため、選択ではなく関数です。確かめるべきは、出来上がった集合への所属が図式の要求する真理値をちょうど持つことです。順方向は像が提供するデータを読み出すだけです。逆方向は外部の所属から添字を復元し、その後、関数性の仮定の緊縮を一度だけ使い、外部から与えられた値を、復元した添字で構成が選んだ値と同一視します。 一つの準備的事実が以下のすべてを貫きます。`m` が `a` の提示における添字なら、それが呈示する要素 `⟪ a ⟫↪ m` は実際に `a` の要素である、というものです。小さな所属 `⟪ a ⟫↪ m ∈ₛ a` は提示の定義により成り立ち、`∈∈ₛ` がそれを構造的な所属へ引き上げます。続いてこの節のデータを取ります。集合 `a`、自由変数の枠を二つ持つ論理式 `φ`、そして関数性の仮定 `fc` です。`fc` は各 `x ∈ a` に対し、`(y ∷ x ∷ []) ⊨ φ` を満たす `y` の型が緊縮的であると主張します。緊縮性はデータ、つまり中心と緊縮の対なので、`a` の各元に対する中心の値は、いかなる選択原理もなしに計算に使えます。 ```agda private memb : (a : S) (m : ⟪ a ⟫) → ⟨ ⟪ a ⟫↪ m ∈ˢ a ⟩ memb a m = ∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m) module _ (a : S) (φ : Formula S 2) (fc : (x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩)) where ``` 像はこうして直接的な組み立てになります。`replaceImage` は添字型 `⟪ a ⟫` 上の `sett` で、各添字 `m` を、`fc` が要素 `⟪ a ⟫↪ m` のために提供する中心の値へ写します。その仕様は、`replaceImage` への所属が、すべての `x` にわたって `(x ∈ a) ⊓ φ(y, x)` を選言した真理値と等しいことを述べます。これは意味論の形での置換図式です。`y` が像に属するのは、`a` のある元で `φ` の値として生じるときちょうどそのときです。本章の他の場所と同様に、`⇔toPath` が二つの含意を仕様の要求する真理値のパスへ変換します。 ```agda replaceImage : S replaceImage = sett ⟪ a ⟫ (λ m → fc (⟪ a ⟫↪ m) (memb a m) .fst .fst) replaceImage-spec : ∀ y → (y ∈ˢ replaceImage) ≡ (∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ)) replaceImage-spec y = ⇔toPath fwd bwd ``` 仕様の順方向は像への所属から始まります。`replaceImage` は `a` の提示型を添字とする `sett` なので、その所属には `⟪ a ⟫` の添字 `m` と、呈示された要素 `⟪ a ⟫↪ m` から `y` へのパス `q` が伴います。右辺の証拠はこの一つの添字から組み立てられます。第一に、準備的事実 `memb` により、呈示された要素は `a` の元です。第二に、`fc` がその元に対して値と、`φ` がその値とその元について成り立つことの証明を与えるので、その証明を `q` に沿って輸送すれば、論理式の第二の自由変数の枠は呈示された要素から `y` へ移ります。この方向は `fc` の一意性の内容をまったく使いません。像が `y` をどのように呈示しようとも、`φ(y, x)` が成り立つ `a` のある元が得られます。 ```agda where fwd : ⟨ y ∈ˢ replaceImage ⟩ → ⟨ ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ) ⟩ fwd = PT.map λ { (m , q) → ⟪ a ⟫↪ m , memb a m , subst (λ v → ⟨ (v ∷ ⟪ a ⟫↪ m ∷ []) ⊨ φ ⟩) q ``` 逆方向は、一見して選択原理が避けられないように思われる箇所です。切り詰められた証拠 `(x , x∈a , hφ)` を受け取り、像への添字を提示しなければなりません。しかもその添字は、`φ(y, x)` が成り立つ `a` の元 `x` そのものを呈示するものでなければなりません。そこで「`x` が元である」という事実を、それを呈示する添字へ変える必要があります。小ささの章がまさにこれを供給します。`∈-asFiber` は、添字と、呈示された要素から `x` へ戻るパスからなる実際の対 `mf` を、切り詰められていない通常のデータとして返します。復元は関数なので、可能な添字の間で選択を行うことはありません。その後、充足の証明 `hφ` をパス `mf .snd` の逆に沿って輸送し、第二の自由変数の枠を `x` から呈示された要素へ移します。これは前提 `fc` が述べられている形と一致します。 ```agda (fc (⟪ a ⟫↪ m) (memb a m) .fst .snd) } bwd : ⟨ ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ) ⟩ → ⟨ y ∈ˢ replaceImage ⟩ bwd = PT.map λ { (x , x∈a , hφ) → let mf = ∈-asFiber {a = x} {b = a} x∈a hφ' = subst (λ v → ⟨ (y ∷ v ∷ []) ⊨ φ ⟩) (sym (mf .snd)) hφ ``` 復元した添字はなお像への所属へ変えねばならず、一意性が入るのはここだけです。添字 `mf .fst` において関数性の仮定は、適切な値の型が緊縮的であることを言うので、外部から与えられた対 `(y , hφ')` を選ばれた中心と比べます。緊縮は中心とそれへのパスを与え、そのパスの第一射影により、`y` は構成がその呈示された元に割り当てた値、すなわち `replaceImage` への添字と同一視されます。したがって一意性はちょうど一度使われ、外部の値 `y` を内部で選ばれた像の値の一つとして認める役割を果たします。これと呈示する添字 `mf .fst` を合わせれば、`y` の像への所属が得られます。 ```agda in mf .fst , cong fst (fc (⟪ a ⟫↪ (mf .fst)) (memb a (mf .fst)) .snd (y , hφ')) } ``` ## 数項の列と ω 強い無限は、ライブラリがほぼそのまま供給する欄です。ライブラリの `ω` は `Lift ℕ` の上、数項 `#` を族とする `sett` なので、`x` が `ω` に属するのは、ある `#` が `x` に命中することが単に成り立つときであり、そのときに限ります。しかし record の要求はモデル自身の数項の列を通して述べられます。第 0 項は空でなければならず、各後続項の元は前者の元に前者自身を加えたものにちょうど等しくなければなりません。したがって仕事は、後続の取り方が異なる二つの列を整列させることです。モデルの列は `a ∪ ⁅ a , a ⁆` を、ライブラリの列は `sucV a = a ∪ ⁅ a ⁆s` を取ります。同じ項を二度入れた対 `⁅ a , a ⁆` と一元集合 `⁅ a ⁆s` は同じ元を持ち、外延性がそれをパスに変えます。この一度の同一視により二つの列は段階ごとに一致し、`ω` の所属の特徴付けが record の強い無限になります。 同定 `⁅ a , a ⁆ ≡ ⁅ a ⁆s` は集合の間のパスなので、外延性により二つの所属の包含へ帰着します。第一の包含は、同じ項を二度入れた対のすべての元が一元集合の元であることを言います。その入力は `⁅ a , a ⁆` への所属であり、対の公理はそのような所属を切り詰められた選言へ展開します。すなわち、その元は対の左の項を通じて、または右の項を通じて `a` と等しい、というものです。 ```agda pair-singleton : (a : S) → ⁅ a , a ⁆ ≡ ⁅ a ⁆s pair-singleton a = extensionality ⁅ a , a ⁆ ⁅ a ⁆s (s1 , s2) where singl-cls = SetPackage.classification (SingletonPackage a) s1 : ⟨ ⁅ a , a ⁆ ⊆ ⁅ a ⁆s ⟩ ``` どちらの選言支も同じこと、`⁅ a ⁆s` への所属を要求します。そこでまず切り詰められた選言を命題 `x ≡ a` (その命題性は階層が h-集合であることから従います) へ消去し、各分岐が自らのパスを与えれば、二つの結果はまさにその命題性によって同一視されます。ここで使うのは一元集合の分類の逆向きで、パス `x ≡ a` から小さな所属 `x ∈ₛ ⁅ a ⁆s` へ進む方向です。これが後の逆包含で使う向きと逆であることに注意してください。 ```agda s1 x x∈ₛ = singl-cls x .snd (PT.rec (setIsSet x a) (λ { (Sum.inl e) → e ; (Sum.inr e) → e }) (pairing-ax a a x .fst x∈ₛ)) s2 : ⟨ ⁅ a ⁆s ⊆ ⁅ a , a ⁆ ⟩ ``` 逆の包含は逆向きに進みます。分類の順方向の成分が所属 `x ∈ₛ ⁅ a ⁆s` をパス `x ≡ a` に変え、このパスを左の選言支として注入すると、対の公理が `⁅ a , a ⁆` への所属へ変換します。二つの集合の同定が済むと、モデルの数項の列は `ℕ` 上の再帰で定義されます。`numeralV zero` は空集合、`numeralV (suc n)` は段階 `n` に、両方の項がともにその段階である対を併合します。同定の後、等しい項を持つ対と一元集合は同じ元を持つため、これはまさにフォン・ノイマンの後続の一段階 `n ∪ ⁅ n ⁆s` です。 ```agda s2 x x∈ₛ = pairing-ax a a x .snd ∣ Sum.inl (singl-cls x .fst x∈ₛ) ∣₁ numeralV : ℕ → S numeralV zero = ∅ numeralV (suc n) = numeralV n ∪ ⁅ numeralV n , numeralV n ⁆ numeralV≡# : (n : ℕ) → numeralV n ≡ # n ``` 二つの列の一致は `ℕ` 上の帰納法で示します。零では両辺とも空集合に簡約されるので、パスは `refl` です。後続の段階では、同じ「対の併合」の形の下で共點性によって両辺を書き換え、対の内部で同定 `pair-singleton` を適用します。外延性の結果が使われるのはこの一歩です。列が整列すると、残りの仕事は `ω` の所属をモデルの語彙で読むことです。`ω-specV` は、`ω` への所属が添字付き選言「`x` はある `numeralV` と等しい」と等しいことを述べます。添字は `Lift ℕ`、つまり持ち上げられた自然数の型を渡ります。右辺の等しさは `≈ˢ`、すなわち構造の集合の外延的等しさなので、この主張は選ばれた提示ではなく集合 `x` そのものについてのものです。 ```agda numeralV≡# zero = refl numeralV≡# (suc n) = cong₂ (λ u v → ⋃ ⁅ u , v ⁆) (numeralV≡# n) (cong (λ u → ⁅ u , u ⁆) (numeralV≡# n) ∙ pair-singleton (# n)) ω-specV : (x : S) → (x ∈ˢ ω) ≡ (∃[ n ∶ Lift {ℓ-zero} {ℓ-suc ℓ} ℕ ] x ≈ˢ numeralV (lower n)) ``` 証明は `⇔toPath` によって所属の二つの記述をパスに変換します。順方向では、証拠 `(i , p)` は持ち上げられた添字と、`x` からライブラリの数項 `# (lower i)` へのパス `p` です。`p` を整列のパスの逆々と合わせて合成すれば、`x` から `numeralV (lower i)` へのパスが得られます。逆方向では同じパスの代数を逆向きに行い、`x` から `numeralV` へのパスを整列を通して対応する `#` へのパスに書き換えます。`lift` と `lower` の変換は自然数を `Lift` の越しに移すだけです。両方向の数学的内容は整列 `numeralV≡#` とその周囲のパスの代数にあります。 ```agda ω-specV x = ⇔toPath (PT.map (λ { (i , p) → lift (lower i) , sym p ∙ sym (numeralV≡# (lower i)) })) (PT.map (λ { (n , q) → lift (lower n) , sym (q ∙ numeralV≡# (lower n)) })) ``` record の二つの固定方程式は後続の段階への所属について語るため、本章では `sucV` 自身の場合分けが必要です。`sucV A` の元は、切り詰められた意味で、`A` の元であるか `A` と等しいかのいずれかであり、両方向の包含が成り立ちます。ライブラリの数項は `sucV` で後続を取るため、この場合分けによってライブラリと整列した任意の数項列が固定方程式を引き継げます。解析は `sucV A` を和と対の公理で一度展開し、第二の選言支、すなわち一元集合 `⁅ A ⁆s` への所属は、その分類で閉じます。 分析は前節の事実一つから始めます。これを取り出しておく価値があります。`x` が一元集合 `⁅ A ⁆s` に属すればパス `x ≡ A` が強制される、というものです。これは一元集合の分類の前半であり、ここでは `singl≡` として記録します。消去原理 `∈sucV-elim` はこの場合分けを使える形にします。命題 `P`、`x` が `A` の元である場合に `P` を与える証明、`x` が `A` と等しい場合に `P` を与える証明、そして `sucV A` の一つの元が与えられれば、`P` の証明を作る、というものです。`P` が命題であるという要求こそ、切り詰められた場合分けをそこへ消去する根拠です。 ```agda private singl≡ : (A x : S) → ⟨ x ∈ₛ ⁅ A ⁆s ⟩ → x ≡ A singl≡ A x = SetPackage.classification (SingletonPackage A) x .fst ∈sucV-elim : {A x : S} {P : Type (ℓ-suc ℓ)} → isProp P → ⟨ x ∈ˢ sucV A ⟩ → (⟨ x ∈ˢ A ⟩ → P) → (x ≡ A → P) → P ``` 数学的には、`sucV A` は対 `⁅ A , ⁅ A ⁆s ⁆` の和なので、その元はいずれかの成分の元です。分析は二段階で進みます。まず和の公理が、対のある成分 `v` と `x` が `v` の元であることを純粋に与えます。次に対の公理が、`v` のこの対への所属を、切り詰められた選言 `v ≡ A` か `v ≡ ⁅ A ⁆s` かへ分裂させます。左の分岐では、`v ≡ A` に沿って `x ∈ v` を輸送すれば `A` への通常の所属が得られ、これは第一の前提の期待するものです。 ```agda ∈sucV-elim {A} {x} pP x∈ kA k≡ = PT.rec pP (λ { (v , (v∈₂ , x∈v)) → PT.rec pP (λ { (Sum.inl v≡A) → kA (∈∈ₛ {a = x} {b = A} .snd (subst (λ w → ⟨ x ∈ₛ w ⟩) v≡A x∈v)) ``` 右の分岐では、`v ≡ ⁅ A ⁆s` に沿った輸送で一元集合への所属が得られ、`singl≡` がそれをパス `x ≡ A` へ変えます。これは第二の前提の期待するものです。二度の切り詰めの消去はいずれも命題 `P` に着地するため正当であり、二つの場合が合わさって分析を完結させます。最初の包含も独立に記録されます。`∈sucV-inl` は、`A` の元が `sucV A` の元であることを述べます。 ```agda ; (Sum.inr v≡s) → k≡ (singl≡ A x (subst (λ w → ⟨ x ∈ₛ w ⟩) v≡s x∈v)) }) (pairing-ax A ⁅ A ⁆s v .fst v∈₂) }) (union-ax ⁅ A , ⁅ A ⁆s ⁆ x .fst (∈∈ₛ {a = x} {b = sucV A} .fst x∈)) ∈sucV-inl : {A x : S} → ⟨ x ∈ˢ A ⟩ → ⟨ x ∈ˢ sucV A ⟩ ``` `∈sucV-inl` の証明は構成であり、解析ではありません。仮定された `x` の `A` への所属から、和への所属の証人を組み立てます。切り詰めの内部では、対の成分 `A` が、対の公理を通して自反パス付きの左の選言支として提示され、`x` の `A` への所属は、和の公理が消費する小形式へ変換されます。外側の交換が、この小形式の証拠全体を `sucV A` への所属へ引き上げます。 ```agda ∈sucV-inl {A} {x} x∈A = ∈∈ₛ {a = x} {b = sucV A} .snd (union-ax ⁅ A , ⁅ A ⁆s ⁆ x .snd ∣ A , (pairing-ax A ⁅ A ⁆s A .snd ∣ Sum.inl refl ∣₁ , ∈∈ₛ {a = x} {b = A} .fst x∈A) ∣₁) self∈sucV : (a : S) → ⟨ a ∈ˢ sucV a ⟩ ``` 対応する `self∈sucV` は第二の包含、すなわち任意の集合 `a` が自分自身の後続に属することを示します。今度の証拠は対のもう一方の成分 `⁅ a ⁆s` を右の選言支として提示するもので、それが `a` を含むという事実は、一元集合の分類の後半を自反パスに適用したものです。二つの補題を合わせると、固定方程式に必要な内容が得られます。`sucV A` の元とは、切り詰められた意味で、`A` の元と `A` 自身にほかなりません。 ```agda self∈sucV a = ∈∈ₛ {a = a} {b = sucV a} .snd (union-ax ⁅ a , ⁅ a ⁆s ⁆ a .snd ∣ ⁅ a ⁆s , (pairing-ax a ⁅ a ⁆s ⁅ a ⁆s .snd ∣ Sum.inr refl ∣₁ , SetPackage.classification (SingletonPackage a) a .snd refl) ∣₁) ``` ライブラリと整列する任意の列に対する、二つの固定方程式です。レコードは、第 0 の数項が元を持たないこと、また各後続数項の元が前者の元に前者自身を加えたものにちょうど等しいことを要求します。どちらの主張も与えられた列への所属についてですが、前節の場合分けは `sucV` への所属について語ります。整列 `q : a n ≡ # n` がその橋渡しであり、列への所属についての主張は `q` に沿ってライブラリの数項についての対応する主張へ運べます。モジュールは列と整列をパラメータとして受け取るので、同じ補題がモデルの列にも他の列にも使えます。 第 0 の方程式のほうが簡単です。もし `z` が列の第 0 段階の元なら、`q zero` に沿って輸送すればライブラリの空集合の元になります。`∈∈ₛ` による交換を経て、`∅-empty` が小さな所属の形でそれを反駁し、結果は空の型の要素です。主張されない点にも注意してください。モデルの数項そのものの空性を証明するのではなく、そこへの所属が矛盾を導くことだけを示します。固定方程式が要求するのはまさにそれです。 ```agda module NumPin (a : ℕ → S) (q : (n : ℕ) → a n ≡ # n) where pinZero : (z : S) → ⟨ z ∈ˢ a zero ⟩ → Empty.⊥ pinZero z z∈ = ∅-empty z (∈∈ₛ {a = z} {b = ∅} .fst (subst (λ w → ⟨ z ∈ˢ w ⟩) (q zero) z∈)) pinSuc : (n : ℕ) (z : S) ``` 後続の方程式は、`a (suc n)` への所属と、「`a n` への所属または `a n` と等しいこと」の切り詰められた選言との間の変換の対であり、これはレコードのフィールドが定める形です。第二の選言支での等しさは `≈ˢ`、つまり構造の等号なので、整列のパスを直接適用できます。選言の命題性は証明の中で明示的に供給されます。切り詰められた主張の消去子がそれを必要とするからです。 ```agda → (⟨ z ∈ˢ a (suc n) ⟩ → ⟨ (z ∈ˢ a n) ⊔ (z ≈ˢ a n) ⟩) × (⟨ (z ∈ˢ a n) ⊔ (z ≈ˢ a n) ⟩ → ⟨ z ∈ˢ a (suc n) ⟩) pinSuc n z = fwd , bwd where fwd : ⟨ z ∈ˢ a (suc n) ⟩ → ⟨ (z ∈ˢ a n) ⊔ (z ≈ˢ a n) ⟩ ``` 順方向では、まず列での所属を `# (suc n)` への所属へ輸送し、そこで `sucV` の分析が適用され、結論の選言へ消去されます。第一の枝では、`# n` での所属が段階 `n` での整列に沿って `a n` での所属へ運び戻され、左の注入で切り詰められた選言が導入されます。第二の枝では、`z` から `# n` へのパスが逆向きの整列と合成され、`z` から `a n` へのパスが得られ、右の注入を取ります。両枝とも切り詰められた証人を生むので、結果はあくまで純粋な選言であり、判定された場合ではありません。 ```agda fwd z∈ = ∈sucV-elim {A = # n} {x = z} (snd ((z ∈ˢ a n) ⊔ (z ≈ˢ a n))) (subst (λ w → ⟨ z ∈ˢ w ⟩) (q (suc n)) z∈) (λ z∈#n → ∣ Sum.inl (subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (q n)) z∈#n) ∣₁) (λ z≡#n → ∣ Sum.inr (z≡#n ∙ sym (q n)) ∣₁) ``` 逆方向では二つの切り詰められた場合を扱うので、消去子は `a (suc n)` の所属の命題へ入ります。第一の場合、`a n` の元は `# n` へ運ばれ、補題 `∈sucV-inl` がそれをライブラリの後続に入れ、結果は後続の段階での整列に沿って運び戻されます。整列は各段階で両方向に使われます。これが、すべての `n` に対して一度に仮定として取られた理由です。 ```agda bwd : ⟨ (z ∈ˢ a n) ⊔ (z ≈ˢ a n) ⟩ → ⟨ z ∈ˢ a (suc n) ⟩ bwd = PT.rec (snd (z ∈ˢ a (suc n))) (λ { (Sum.inl z∈n) → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (q (suc n))) (∈sucV-inl {A = # n} (subst (λ w → ⟨ z ∈ˢ w ⟩) (q n) z∈n)) ; (Sum.inr z≡n) → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (q (suc n))) ``` 第二の場合は右の選言支を扱い、ここで「後続は自分自身を含む」という事実が働きます。仮定は `z` からモデルの前者へのパス `z ≡ a n` であり、整列 `q n` との合成によりパス `z ≡ # n` になります。このパスが、保持しておいた事実 `self∈sucV (# n)`、すなわち `# n` が自分自身のライブラリの後続に属することを、「`z` は `sucV (# n)` に属する」という主張へ輸送し、最後は後続の段階での整列に沿う輸送で列に戻ります。二つの枝を合わせて逆方向の変換が完成し、整列した任意の列に対して後続の固定方程式が果たされます。 ```agda (subst (λ w → ⟨ w ∈ˢ sucV (# n) ⟩) (sym (z≡n ∙ q n)) (self∈sucV (# n))) }) ``` ## 残る公理に必要な仮定 残る欄は完全な分出と冪集合の二つですが、両者は異なる小ささの問題を提示します。完全な分出は、`Type (ℓ-suc ℓ)` に住む任意の充足命題 `(y ∷ []) ⊨ φ` を小さくしなければなりませんが、手作業でこれを行う Δ₀ の証人はありません。必要なのは非可述性の `resizing` の成分で、そのような各命題に点ごとに小さな代表を与え、小ささの適合装置 `separateFromSmall` を適用できるようにします。冪集合が提示するのは別の問題です。`a` の候補となる部分集合は `⟪ a ⟫` で添字付けられた所属の命題の族であり、そこから集合を作るには、各命題を一つの固定された小さな型へ符号化しなければなりません。`hPropSmallness` の成分はまさにこれを供給します。すなわち `hProp ℓ` 全体と同値な小さな型 `Ω'` で、命題の分類子として働きます。どちらの構成も `Impredicativity` のパッキング全体を使うのではなく、その二つの成分の一方だけを消費します。後の組み立てはパッキングをパラメータとして受け取り、古典的な場合は `lem→impredicativity` から導かれます。 ## 冪集合 冪集合は、ライブラリのヘッダ自身が提供しないと明言する唯一の構成であり、小分類子こそがそれを作る材料です。`a` の候補となる部分集合は、分類子の小さな台への特性関数 `⟪ a ⟫ → Ω'` で記述します。各値 `χ m` を復号すれば添字 `m` 上の命題が得られ、その命題が成り立つ添字が呈示する要素は `sett` で一つの集合に集められます。証明は二つの包含を確立します。関数が選んだものはすべて与えられた部分集合に含まれ、部分集合のすべての元が選ばれる、というものです。第二の方向は、命題に対する復号してから符号化する往復と、外延性を用います。 冪集合の構成は、パッキングの成分のうちちょうど一つを前提とします。すなわち `HPropSmallness ℓ` の証人 `sΩ`、つまり `Type ℓ` の小さな型 `Ω'` と `hProp ℓ` 全体への同値です。それ以外は何も仮定しません。この同値から二つの読み方を取り出します。順方向の写像 `decode` は小さな真理値を、`hProp ℓ` に包装された通常の命題へ変えます。特性関数を添字上の述語として読めるのはこの方向です。 ```agda module Power (sΩ : HPropSmallness ℓ) where private decode : sΩ .fst → hProp ℓ decode = equivFun (sΩ .snd) encode : hProp ℓ → sΩ .fst ``` 逆方向の写像 `encode` は `hProp ℓ` の命題を小さな台へ送り、往復 `decode∘encode` は同値の `secEq` の側です。命題の符号を復号すれば、もとの命題そのものへのパスが返ります。分類子が揃うと、実現する族 `F` は直接的です。特性関数 `χ` に対し、添字 `m` と「`decode (χ m)` が成り立つ」ことの証明の対を集め、それが呈示する要素の `sett` を作ります。選ばれる元は、符号化された真理値を復号すると証明付きの命題になるものにちょうど一致します。 ```agda encode = invEq (sΩ .snd) decode∘encode : (P : hProp ℓ) → decode (encode P) ≡ P decode∘encode = secEq (sΩ .snd) F : (a : S) → (⟪ a ⟫ → sΩ .fst) → S F a χ = sett (Σ[ m ∈ ⟪ a ⟫ ] ⟨ decode (χ m) ⟩) (λ p → ⟪ a ⟫↪ (p .fst)) ``` 冪集合の操作そのものも `sett` です。添字型は `⟪ a ⟫` から小さな台 `Ω'` への関数型であり、族が各特性関数を上で選ばれた集合として実現します。したがって `𝒫V a` への所属とは、切り詰められた意味で、実現された集合のどれかへの所属です。すなわち、特性関数と、それが選ぶ集合から `x` へのパスの切り詰められた対として元が現れます。仕様の順方向は、そのような `x` が周辺の意味で `a` の部分集合であること、つまり階層のライブラリの包含 `⊆` であって構造の関係 `⊆ˢ` ではないことを示します。両者の仲立ちには別の段階を設け、最後に扱います。 ```agda 𝒫V : S → S 𝒫V a = sett (⟪ a ⟫ → sΩ .fst) (F a) private fwd : (a x : S) → ⟨ x ∈ˢ 𝒫V a ⟩ → ⟨ x ⊆ a ⟩ fwd a x = PT.rec ((x ⊆ a) .snd) λ { (χ , p) y y∈ₛx → ``` `x ⊆ a` の証明は元ごとに進み、まず冪集合への切り詰められた所属を消去します。`y` の `x` への所属を呈示するパスに沿って運び戻すと、それは選ばれた集合 `F a χ` への小さな所属になり、`∈∈ₛ` で変換すると呈示するファイバーが得られます。すなわち添字 `m` と、`decode (χ m)` が成り立つことの証明、さらに `y` を呈示された要素 `⟪ a ⟫↪ m` と同一視するパスです。 ```agda PT.rec ((y ∈ₛ a) .snd) (λ { ((m , _) , q) → subst (λ v → ⟨ v ∈ₛ a ⟩) q (∈ₛ⟪ a ⟫↪ m) }) (∈∈ₛ {a = y} {b = F a χ} .snd (subst (λ v → ⟨ y ∈ₛ v ⟩) (sym p) y∈ₛx)) } bwd : (a x : S) → ⟨ x ⊆ a ⟩ → ⟨ x ∈ˢ 𝒫V a ⟩ ``` 残りの作業は、そのファイバーを `y` の `a` への所属に変えることで、パスに沿う輸送がこれを果たします。`a` の呈示された要素は構成によって `a` の元だからです。目標は終始命題値のままなので、二つの切り詰めの消去はいずれも正当です。こうして冪集合の元は、どのように呈示されようと、`a` の元だけを集めます。 逆方向は冪集合への所属の証人を組み立てますが、選択は要りません。特性関数 `χₓ` は明示的に取り戻されます。添字 `m` は、呈示された要素 `⟪ a ⟫↪ m` の `x` における小さな所属の符号 `encode` へ送られます。これは関数であって選択ではありません。埋め込みの小さな所属のファイバーが切り詰められていないからです。切り詰められた対は、`χₓ` と「`χₓ` が選ぶ集合が `x` に等しい」という主張をまとめます。その主張は二つの包含 `s1`、`s2` から外延性によって確立されます。 ```agda bwd a x sub = ∣ χₓ , extensionality (F a χₓ) x (s1 , s2) ∣₁ where χₓ : ⟪ a ⟫ → sΩ .fst χₓ m = encode (⟪ a ⟫↪ m ∈ₛ x) s1 : ⟨ F a χₓ ⊆ x ⟩ ``` 第一の包含は、`χₓ` が選ぶ集合が `x` を超えるものを何も加えないことを示します。`F a χₓ` の小さな元は、添字 `m`、`decode (χₓ m)` が成り立つことの証明、そして呈示するパスを伴います。`χₓ m` はもともと所属 `⟪ a ⟫↪ m ∈ₛ x` の符号として定義されているので、往復 `decode∘encode` が復号された証明をまさにその所属へ書き戻し、呈示するパスがそれを `y` の上へ運びます。したがって選ばれた集合のすべての元は `x` の元です。 ```agda s1 y y∈ₛF = PT.rec ((y ∈ₛ x) .snd) (λ { ((m , h) , q) → subst (λ v → ⟨ v ∈ₛ x ⟩) q (subst ⟨_⟩ (decode∘encode (⟪ a ⟫↪ m ∈ₛ x)) h) }) (∈∈ₛ {a = y} {b = F a χₓ} .snd y∈ₛF) ``` 第二の包含は逆向きに進めます。`x` の任意の元 `y` から、`F a χₓ` の小さな元を作るのです。包含の仮定 `sub` はまず `a` における `y` の呈示するファイバーを与え、その第二成分は、呈示された要素と `y` が同じ元を持つことを証明します。ここでは埋め込みの提示を両方向で使うので、何も選ぶ必要はありません。ファイバーは切り詰められていないデータであり、`⟪ a ⟫↪ m₀ ≡ y` を取り出すパス `q` は普通の項として利用できます。 ```agda s2 : ⟨ x ⊆ F a χₓ ⟩ s2 y y∈ₛx = ∈∈ₛ {a = y} {b = F a χₓ} .fst ∣ (m₀ , h) , q ∣₁ where m₀ = sub y y∈ₛx .fst q : ⟪ a ⟫↪ m₀ ≡ y ``` パス `q` は、包含の仮定の「元が同じ」というデータに `identityPrinciple` を適用して得られ、呈示された要素 `⟪ a ⟫↪ m₀` が `y` に等しいことが分かります。`x` での `y` の所属を `q` の逆向きに沿って運ぶと呈示された要素に着地し、これが往復によって、まさに `decode (χₓ m₀)` が復号する命題です。`χₓ m₀` はもともとこの所属の符号として定義されていたからです。よって添字と運ばれた証明の対 `(m₀ , h)` は `F a χₓ` を定める型の要素となり、選ばれた集合への `y` の所属の証人になります。両包含が揃うと、`power-spec` はこの同値を、周辺の包含 `⊆` と構造の部分集合の関係 `⊆ˢ` との各点の交換と合成し、欄 `hasPower` に、その所属が真理値としてレコードの述べる部分集合の関係に等しい集合を与えます。 ```agda q = equivFun identityPrinciple (sub y y∈ₛx .snd) h : ⟨ decode (χₓ m₀) ⟩ h = subst ⟨_⟩ (sym (decode∘encode (⟪ a ⟫↪ m₀ ∈ₛ x))) (subst (λ v → ⟨ v ∈ₛ x ⟩) (sym q) y∈ₛx) power-spec : (a x : S) → (x ∈ˢ 𝒫V a) ≡ (x ⊆ˢ a) ``` 仕様 `power-spec` は二つの真理値の等式を合成します。一つ目は今示した本質的な同値、すなわち `𝒫V a` への所属と、実際の元の上で量化され切り詰められていない包含 `x ⊆ a` との一致です。二つ目は、その包含を構造自身の部分集合の関係 `x ⊆ˢ a`、つまり構造の所属 `∈ˢ` を通して述べた形へ変換します。`x` の各通常の元を `a` の通常の元へ送る関数が与えられれば、`∈∈ₛ` の両方向が二つの所属の記法を各点で取り替えます。その合成こそ、冪集合のフィールドが受け取るデータです。集合 `𝒫V a` の所属が、真理値として、record の述べる部分集合の関係にちょうど等しいということです。それぞれの小ささの入力が入った場所にも注意してください。分出は点ごとに `resizing` を消費し、冪集合は `hPropSmallness` だけで組み立てられました。 ```agda power-spec a x = ⇔toPath {P = x ∈ˢ 𝒫V a} {Q = x ⊆ a} (fwd a x) (bwd a x) ∙ ⇔toPath {P = x ⊆ a} {Q = x ⊆ˢ a} (λ s y y∈x → ∈∈ₛ {a = y} {b = a} .snd (s y (∈∈ₛ {a = y} {b = x} .fst y∈x))) (λ f y y∈ₛx → ∈∈ₛ {a = y} {b = a} .fst (f y (∈∈ₛ {a = y} {b = x} .snd y∈ₛx))) ``` ## V ⊨ ZF の証明 モデルの record の各フィールドにはすでに証拠が揃っており、この節はそれらを一つの数学的定理へ組み立てます。累積階層は ZF を満たす、という定理です。公理はその導出の仕方ごとに分類できます。空集合、対、和集合は章の冒頭で変換した基本的な集合です。完全な分出と冪集合は二つの小ささの結果で、それぞれ非可述性のパッキングの成分を一つずつ消費します。分出は `resizing` で各充足命題を小さくして `separateFromSmall` を適用できようにし、冪集合は小分類子だけを使います。置換は切り詰められていないファイバーから作った像であり、無限はライブラリの `ω` と数項の整列です。残るのは梱包の一段階ですが、そこには本物の数学的入力が一つあります。`isZFModel` の各フィールドは `isContr (SetOf Q)`、すなわち実現する集合と、すべての実現者をそこへ収縮させるデータを要求します。外延性がまさにその収縮を `setOf-unique` を通して与えます。定理 `V⊨ZF-impredicative` はパッキング `Impredicativity ℓ` を仮定し、定理 `V⊨ZF` は代わりに `LEM (ℓ-suc ℓ)` を仮定して、`lem→impredicativity` によりパッキングを導きます。 組み立てはパッキング `Impredicativity ℓ` をパラメータとして受け、その二つのフィールドは二つの小ささの構成に別々に供給されます。`hPropSmallness` は前節の冪集合の構成に渡され、そこでは分類子だけが使われます。`resizing` は分出で使うものです。完全な分出は直接に述べられます。集合 `a` と自由変数の枠を一つ持つ論理式 `φ` が与えられたとき、各 `y` について真理値 `y ∈ˢ s` が「`y ∈ˢ a`」と「一点環境 `y ∷ []` での `φ` の充足」の連言にパスとして等しい集合 `s` を作ります。これはモデルの record が要求する分出の仕様の形そのものです。 ```agda module VModel (imp : Impredicativity ℓ) where open Impredicativity imp open Power hPropSmallness public separateFull : (a : S) (φ : Formula S 1) → Σ[ s ∈ S ] (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ ((y ∷ []) ⊨ φ))) ``` 分出は、小ささの章の適合装置の一度の適用です。`separateFromSmall` は、`a` の上の述語 `P : S → hProp (ℓ-suc ℓ)` と各値への小ささの証明を受け取り、パスの仕様 `y ∈ˢ s ≡ (y ∈ˢ a) ⊓ P y` をもつ集合 `s` を返します。ここでの述語は `λ y → (y ∷ []) ⊨ φ`、つまり各一点環境での `φ` の充足であり、各点での小ささはそこで適用される `resizing` です。`φ` の形状についての前提は一切要りません。どのような論理式から生じたものであれ、リサイズは各充足命題に小さな代表を割り当てます。`separateFull` が揃えば、すでに示した証拠から型 `isZFModel` の定理 `V⊨ZF-impredicative` を組み立てられます。 ```agda separateFull a φ = separateFromSmall a (λ y → (y ∷ []) ⊨ φ) (λ y → resizing ((y ∷ []) ⊨ φ)) V⊨ZF-impredicative : isZFModel V⊨ZF-impredicative = record { extensional = extensionalV ``` 最初のグループの項目は章の冒頭の変換を再利用します。空集合、対、和集合の明示的な実現者は、それぞれライブラリの集合 `∅`、`⁅ a , b ⁆`、`⋃ a` と、そこで示した仕様です。`extensional` と `regularity` の項目は、階層の章で証明された証拠を引用します。分出の実現者は `separateFull a φ`、すなわち分出された集合とその仕様の対で、すでにフィールドの要求する形をしています。各フィールドはパラメータの関数なので、図式のすべての実例が、すべての論理式に対して一度に供給されます。 ```agda ; regularity = regularityV ; hasEmpty = one _ (∅ , empty-spec) ; hasPair = λ a b → one _ (⁅ a , b ⁆ , pair-spec a b) ; hasUnion = λ a → one _ (⋃ a , union-spec a) ; hasSeparation = λ a φ → one _ (separateFull a φ) ``` 続く二つの項目は、中盤の構成を使います。置換のフィールドは関数性の仮定 `fc` を受け取り、像 `replaceImage` とその仕様を実現者とします。冪集合のフィールドは `𝒫V a` と `power-spec`、つまり小分類子だけから作った構成を取ります。数項の列は三つの項目を占めます。演算 `numeralV` 自身と、二つの固定方程式です。`numeral-zero` は `numeralV zero` には元が住まないことを、`numeral-suc` は `numeralV (suc n)` の元が前者の元か前者と等しいかの二分であることを述べます。どちらの方程式も、整列 `numeralV≡#` に対する `NumPin` の補題の適用から来るため、その内容はちょうどこの整列と `sucV` の場合分けです。 ```agda ; hasReplacement = λ a φ fc → one _ (replaceImage a φ fc , replaceImage-spec a φ fc) ; hasPower = λ a → one _ (𝒫V a , power-spec a) ; numeral = numeralV ; numeral-zero = NumPin.pinZero numeralV numeralV≡# ; numeral-suc = NumPin.pinSuc numeralV numeralV≡# ``` 最後のフィールドは強い無限で、`ω` とその仕様が実現します。`ω` の各元は単にどこかのモデル数項と等しい、というのが record の要求です。補助の `one` は、すべての存在のフィールドを締めくくる一般原則を一行で記録します。任意のクラス `Q : S → hProp (ℓ-suc ℓ)` に対し、`SetOf Q` の元、すなわち実現する集合とその仕様は、`setOf-unique` を外延性に適用すればすべての実現者が与えられたものへ収縮するため、`isContr (SetOf Q)` の元をすでに定めます。したがって上の各明示的な実現者は、そのフィールドの要求する可縮データになり、外延性は各項目で繰り返されず `one` で一度引用されます。 ```agda ; hasInfinity = one _ (ω , ω-specV) } where one : (Q : S → hProp (ℓ-suc ℓ)) → SetOf Q → isContr (SetOf Q) one = setOf-unique extensionalV ``` 定理 `V⊨ZF-impredicative` は、単一の仮定 `Impredicativity ℓ` の下で累積階層が ZF を満たすことを述べます。二つの図式のフィールドはどちらもすべての論理式を受け取る関数なので、分出と置換はすべての論理式に対して一度に成り立ちます。そこでは一階論理の諸章による対象言語の深い埋め込みが働きます。第二の定理は、このパッキングを標準的な古典的仮定に置き換えます。`V⊨ZF` は `LEM (ℓ-suc ℓ)` を受け取り、そこからパッキングを導きます。証明されるのは、明示された仮定の下でのモデルの構成であり、無条件の無矛盾性の主張ではありません。 `V⊨ZF` の定義は一度の合成です。排中律の実例を `lem→impredicativity` がパッキングへ変換し、その結果が `VModel.V⊨ZF-impredicative` に渡されます。この変換、古典の章で示されたものでは、リサイズのフィールドは `lem` をそのレベルでそのまま使い、分類子のフィールドはまず `lowerLEM` で実例を後続一段下げてから、`hProp ℓ` を `Lift Bool` で提示する同値を構成します。したがって後続レベルでの一つの仮定が、モデルが消費する両方のフィールドに届きます。分出はリサイズを通して、冪集合は分類子を通してです。 ```agda V⊨ZF : LEM (ℓ-suc ℓ) → isZFModel V⊨ZF lem = VModel.V⊨ZF-impredicative (lem→impredicativity lem) ``` ## 選択公理を別に仮定する 排中律から選択は導けないため、ZFC の最後の公理は独立な仮定として受け、選択集合の公理はそこから証明します。インターフェースは `SetChoice` です。h-集合 `X : Type ℓ` と族 `B : X → Type ℓ` に対し、各ファイバーが単に居住するなら、`X` 全体の上の選択関数が、切り詰められた形で存在します。以下の補題は、このインターフェースのレベル `ℓ` の実例と、固定された階層構造 `𝒮ᵥ` 上の `isZFModel` を仮定し、そこから交 `∩` とその仕様を使います。選択を施す族は小さな提示です。添字の型は h-集合 `⟪ a ⟫` であり、添字 `m` 上のファイバーは `m` が提示する集合 `⟪ ⟪ a ⟫↪ m ⟫` です。したがって選択が選ぶのは集合の要素ではなく提示の添字です。選ばれた添字から、`sett` を一度適用して集合 `c` を作ります。そして互いに素であることの仮定 `disj` により、モデルの交を通して、`c` が `a` の各元と交わる点の集合が可縮、したがって一意であることが示されます。切り詰めは設計上非対称です。選択集合そのものは単なる存在ですが、各交わりは明示的な `isContr` のデータを持ちます。最終定理は一つの `SetChoice (ℓ-suc ℓ)` の実例を二度使います。`choice→lem` がそれを ZF の部分のための `LEM (ℓ-suc ℓ)` へ変換し、`lowerSetChoice` がそれを選択の補題のための `SetChoice ℓ` へ下げます。つまり `V⊨ZFC` は選択だけから証明されます。排中律はディアコネスクの定理により選択から回収されるのであって、逆ではありません。 選択集合の構成には二つの準備的事実が使われます。第一は、選択を適用する添字の型に関するものです。各提示の型 `⟪ a ⟫` は h-集合です。`⟪ a ⟫↪` を通して階層へ埋め込まれ、その埋め込みの性質 `isEmb⟪ a ⟫↪` は提示の導入時に記録済みであり、階層自身は `setIsSet` により h-集合だからです。cubical の一般結果 `Embedding-into-isSet→isSet` が埋め込みに沿って h-集合性を引き戻すので、任意の集合 `a` に対して `isSet⟪ a ⟫` が成ります。したがって添字の間の等号の型はすべて命題であり、これがまさに `SetChoice` が選択の対象とする型に課す条件です。 ```agda private isSet⟪_⟫ : (a : S) → isSet ⟪ a ⟫ isSet⟪ a ⟫ = Embedding-into-isSet→isSet (⟪ a ⟫↪ , isEmb⟪ a ⟫↪) setIsSet isContrΣ-fromCenter : {P : S → hProp (ℓ-suc ℓ)} (z₀ : S) (p₀ : z₀ ∈ᶜ P) → ((z : S) → z ∈ᶜ P → z₀ ≡ z) ``` 第二の事実は、一意性の議論を緊縮性のデータへ包装します。台の上のクラス `P` に対し、中心 `z₀` とその実現 `p₀`、そして `P` を実現する各 `z` をパス `z₀ ≡ z` に送る緊縮があれば、「集合と `P` の実現」の組の型は緊縮的で、その中心は `(z₀ , p₀)` です。組の間の緊縮は `Σ≡Prop` で組み立てます。第一成分の間のパスを与えれば十分で、各 `P v` が命題であるため第二成分はそれで決まるからです。選択集合の結論はちょうどこの形、`isContr` の意味で一意な一点です。補題の仮定は続いて取られます。固定された構造 `𝒮ᵥ` 上の任意の `isZFModel` を仮定し、そこからはモデルの交 `∩` とその仕様 `∩-spec` だけを使い、これに `SetChoice ℓ` の一実例を添えます。 ```agda → isContr (Σ[ z ∈ S ] (z ∈ᶜ P)) isContrΣ-fromCenter {P} z₀ p₀ u = (z₀ , p₀) , λ w → Σ≡Prop (λ v → snd (P v)) (u (w .fst) (w .snd)) module ChoiceLemma (zf : isZFModel) (ac : SetChoice ℓ) where open Model.isZFModel zf using ( _∩_; ∩-spec ) ``` 補題 `choice` は古典的な選択集合の状況を述べます。仮定は次のとおりです。`inh` は `a` の各元 `x` が単に居住することを言い、族は空でない集合からなります。`disj` は、`a` の二つの元が単に共通の元を共有するだけですでに等しいことを言い、族は互いに素です。結論は、**単に存在する**集合 `c` で、`a` の各元 `x` に対して交 `c ∩ x` の点の型が緊縮的であるというものです。切り詰めは非対称です。選択集合そのものはデータとして与えられず、その切り詰めが居住するだけです。一方、各交点の一意性は明示的な `isContr` のデータです。 ```agda choice : (a : S) → ((x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ ∥₁) → ((x y : S) → ⟨ x ∈ˢ a ⟩ → ⟨ y ∈ˢ a ⟩ → ∥ Σ[ z ∈ S ] (⟨ z ∈ˢ x ⟩ × ⟨ z ∈ˢ y ⟩) ∥₁ → x ≡ y) → ∥ Σ[ c ∈ S ] ((x : S) → ⟨ x ∈ˢ a ⟩ ``` 証明は、族そのものではなく族の小さな提示の上で選択の実例を適用します。添字の型は `⟪ a ⟫` で、第一の準備事実により h-集合です。族は `λ m → ⟪ ⟪ a ⟫↪ m ⟫`、つまり各添字が提示する集合です。残るのは各ファイバーを単に居住させることで、それが `pick` の役目です。各添字 `m` に対し、`memb a m` が確かめる要素のところで `inh` が、提示された集合 `⟪ a ⟫↪ m` の要素の単なる存在を与え、`∈-asFiber` がその所属から `⟪ a ⟫↪ m` の提示への実際の添字を取り出します。入力の切り詰めは終始保存されるので、`pick` が `a` の要素の内部で点を選ぶと主張することはなく、単なる存在に添字を付け直すだけです。 ```agda → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)) ∥₁ choice a inh disj = PT.map mk (ac ⟪ a ⟫ isSet⟪ a ⟫ (λ m → ⟪ ⟪ a ⟫↪ m ⟫) pick) where pick : (m : ⟪ a ⟫) → ∥ ⟪ ⟪ a ⟫↪ m ⟫ ∥₁ pick m = PT.map ``` 選択関数はその後、各添字 `m` に対して提示された集合の実際の要素 `g m` を返します。添字の h-集合上の選択は切り詰められていないデータ、すなわち `⟪ a ⟫↪ m` の提示の要素を与えます。残りの `mk` はこれを結論へ包装します。集合 `c` と、`a` の各元 `x` に対する、交 `c ∩ x` の点の型の緊縮データです。選択関数が添字の水準で既に切り詰められていないデータを生んでいるため、`mk` は普通の関数であり、切り詰めが再び現れるのは全体が `PT.map` で包まれるときだけです。選択集合そのものが単なる存在でありながら、各交わりが明示的な `isContr` のデータを持つのはまさにこのためです。 ```agda (λ { (y , y∈) → ∈-asFiber {a = y} {b = ⟪ a ⟫↪ m} y∈ .fst }) (inh (⟪ a ⟫↪ m) (memb a m)) mk : ((m : ⟪ a ⟫) → ⟪ ⟪ a ⟫↪ m ⟫) → Σ[ c ∈ S ] ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)) ``` `mk` の内部で、選ばれたデータを解釈します。`g m` が返すのは `⟪ a ⟫↪ m` の提示への添字なので、その提示と合成すると実際の集合 `chosen m`、すなわち添字 `m` の指す要素の要素の一つが得られます。選択集合は `c = sett ⟪ a ⟫ chosen`、つまり各添字のために選ばれた集合を階層の集合構成子の一度の適用で集めたものです。 ```agda mk g = c , uniq where chosen : ⟪ a ⟫ → S chosen m = ⟪ ⟪ a ⟫↪ m ⟫↪ (g m) c : S ``` 一意性の前に、`c` についての一つの事実を記録します。選ばれた各集合は、その出身の要素の要素に確かになっています。これは提示から従います。集合の提示への添字 `g m` は `∈ₛ⟪ ⟫↪` により小さな所属であり、`∈∈ₛ` がそれを構造的な所属 `⟨ chosen m ∈ˢ ⟪ a ⟫↪ m ⟩` へ引き上げます。第二の準備事実の一意性の補助が揃うと、`uniq` は三段の議論になります。中心、中心が交に属することの証明、そして他の交点を中心へ緊縮する緊縮です。 ```agda c = sett ⟪ a ⟫ chosen chosen∈ : (m : ⟪ a ⟫) → ⟨ chosen m ∈ˢ ⟪ a ⟫↪ m ⟩ chosen∈ m = ∈∈ₛ {a = chosen m} {b = ⟪ a ⟫↪ m} .snd (∈ₛ⟪ ⟪ a ⟫↪ m ⟫↪ (g m)) uniq : (x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩) uniq x x∈a = isContrΣ-fromCenter {P = λ z → z ∈ˢ (c ∩ x)} z₀ pf₀ uniqz ``` 中心は次のように計算されます。`a` の要素 `x` は切り詰められていない提示のファイバーを持ち、`∈-asFiber` が添字 `m₀` と `x` を提示するパス `mf .snd` を与えます。交点はその添字で選ばれた集合 `z₀ = chosen m₀` です。ここで再び切り詰められていないファイバーが利きます。所属から添字を復元するのは関数であって選択ではないため、中心の定義に選択の実例を呼ぶ必要はありません。 ```agda where mf = ∈-asFiber {a = x} {b = a} x∈a m₀ = mf .fst z₀ = chosen m₀ pf₀ : ⟨ z₀ ∈ˢ (c ∩ x) ⟩ ``` 中心は交 `c ∩ x` に属さねばなりません。モデルの `∩-spec` により、交への所属は真理値として「`c` への所属」と「`x` への所属」の連言に等しく、証明は対称化した仕様に沿って輸送します。`c` への所属は、自反パスとともに、`z₀` が添字 `m₀` で選ばれたことの単なる証明であり、`m₀` は `x` を提示します。`x` への所属は、`chosen∈ m₀` をその提示のパスに沿って輸送することで従います。二つの半分は切り詰められた組として連言されます。残る仕事は緊縮 `uniqz` です。交 `c ∩ x` に属する各 `z` をパス `z₀ ≡ z` に送らねばなりません。 ```agda pf₀ = subst ⟨_⟩ (sym (∩-spec c x z₀)) ( ∣ m₀ , refl ∣₁ , subst (λ w → ⟨ z₀ ∈ˢ w ⟩) (mf .snd) (chosen∈ m₀) ) uniqz : (z : S) → ⟨ z ∈ˢ (c ∩ x) ⟩ → z₀ ≡ z uniqz z pf = PT.rec (setIsSet z₀ z) ``` 緊縮が繊細な半分です。交 `c ∩ x` に属する任意の `z` を取ると、交への所属が `∩-spec` を通して切り詰められた連言 `zcx` へ輸送されます。第一成分は、`z` がある選ばれた集合に属することの単なる証明です。すなわち添字 `m` と、`c` の要素としての `z` から `chosen m` へのパス `q` です。`chosen∈` により `chosen m` は `⟪ a ⟫↪ m` の要素なので、`q` に沿って輸送すれば `z` がその要素の要素でもあることが分かります。したがって `z` は `a` の要素 `x` と `⟪ a ⟫↪ m` の共通の要素であり、非交性が適用されます。`disj` はパス `x ≡ ⟪ a ⟫↪ m` を与えます。二つの要素は同じ集合を提示するので、提示する添字は一致します。提示は埋め込みで添字の上で単射だから、合成したパスに `isEmbedding→Inj` を適用すれば `m ≡ m₀` が従います。よって `chosen m ≡ chosen m₀ = z₀` であり、`q` と合成すれば緊縮のパス `z₀ ≡ z` が得られます。目標は h-集合の要素の間のパス、つまり命題であり、これがここで切り詰めを消去することを正当化します。 本章の最終定理の計算は正確です。`SetChoice (ℓ-suc ℓ)` の一つの実例が二度使われます。`choice→lem` がそれを `LEM (ℓ-suc ℓ)` へ変換し、`V⊨ZF` を通して ZF の部分を駆動します。また `lowerSetChoice` が同じ実例を `SetChoice ℓ` に下げ、選択集合の部分のために `ChoiceLemma` に渡します。選択集合は単に存在するだけですが、各交わりは明示的な緊縮のデータによって一意に定まります。 ```agda (λ { (m , q) → let z∈m : ⟨ z ∈ˢ ⟪ a ⟫↪ m ⟩ z∈m = subst (λ w → ⟨ w ∈ˢ ⟪ a ⟫↪ m ⟩) q (chosen∈ m) x≡m : x ≡ ⟪ a ⟫↪ m x≡m = disj x (⟪ a ⟫↪ m) x∈a (memb a m) ``` 非交性を `a` の二つの要素 `x` と `⟪ a ⟫↪ m` に適用し、重なりの証人として共通の要素 `z` を渡すと、仮定 `disj` はパス `x ≡ ⟪ a ⟫↪ m` を返します。したがって二つの添字は同じ要素を提示します。提示 `⟪ a ⟫↪` は埋め込みであり、添字の上で単射なので、合成 `sym x≡m ∙ sym (mf .snd)` に `isEmbedding→Inj` を適用すれば `m ≡ m₀` が得られます。このパスに `chosen` を施し `q` と合成すれば、緊縮の要求するパス `z₀ ≡ z` が生まれます。目標 `z₀ ≡ z` は h-集合 V の要素の間のパス、つまり命題であり、これがここで場合分けの切り詰めを消去することを正当化します。 ```agda ∣ z , zcx .snd , z∈m ∣₁ m≡m₀ : m ≡ m₀ m≡m₀ = isEmbedding→Inj isEmb⟪ a ⟫↪ m m₀ (sym x≡m ∙ sym (mf .snd)) in sym (cong chosen m≡m₀) ∙ q }) ``` 連言 `zcx` は、`pf` をパス `∩-spec c x z` に沿って輸送して得られ、`c ∩ x` への所属が二つの所属命題の普通の組として書き直されます。二つの成分はその後別々に使われます。第一成分は前段の非交性の証人に入り、第二成分は `z` の所属の輸送 `z∈m` に入ります。中心と緊縮が揃うと、`uniq` が `a` の各要素に対する `isContr` のデータを供給し、`mk` は集合 `c` とそれらのデータを返します。選択集合そのものは、命題の切り詰めの要素として単に存在するだけです。それに対して、各交の一意性は切り詰められていない明示的な `isContr` のデータです。 ```agda (zcx .fst) where zcx : ⟨ z ∈ˢ c ⟩ × ⟨ z ∈ˢ x ⟩ zcx = subst ⟨_⟩ (∩-spec c x z) pf ``` ## 選択だけから V ⊨ ZFC 前節の補題と ZF の定理がここで合流します。構成 `ChoiceLemma.choice` は、固定された階層構造に対して、二つの明示された仮定の下で証明されています。その構造上の任意の `isZFModel` と、`SetChoice ℓ` の一実例です。その添字の型は小さな提示 `⟪ a ⟫` であり h-集合なので、選択が選ぶのは族の提示の添字です。その後、非交性が各交の可縮性を示します。したがって選択集合は単に存在するだけであり、各交点は明示的な `isContr` のデータとして一意です。定理 `V⊨ZFC` が述べるのは結合後の正確なコストです。`SetChoice (ℓ-suc ℓ)` は `choice→lem` を通して ZF の部分に `LEM (ℓ-suc ℓ)` を与え、同じ実例を `lowerSetChoice` で `SetChoice ℓ` に下げたものが選択集合の補題を駆動します。証明されるのは明示された仮定の下でのモデルの構成であり、無条件の証明ではありません。 定理の仮定は一つの実例です。すなわち `SetChoice (ℓ-suc ℓ)`、モデルの真理値の水準の後続における集合レベルの選択です。結論 `isZFCModel` は ZF モデルと内部の選択集合の証明をひとまとめにするので、証明は両方の成分を与えます。ZF の部分には `base` と名前が付きます。選択集合の補題が入力として ZF モデルを受け取るからです。 ```agda V⊨ZFC : SetChoice (ℓ-suc ℓ) → isZFCModel V⊨ZFC ac = record { zf = base ; hasChoice = ChoiceLemma.choice base (lowerSetChoice ac) } where base : isZFModel ``` 一つの実例が二つの結論に使われます。`choice→lem` はそれをレベル `ℓ-suc ℓ` の排中律へ変換し、これは `V⊨ZF` が期待する仮定にちょうど一致するので、`base` が得られます。選択集合の部分では、`lowerSetChoice` が同じ実例を `SetChoice ℓ` に下げます。これが `ChoiceLemma.choice` の要求するものであり、補題は `base` に適用されます。こうして、後続レベルでの一つの選択の実例が排中律を通して ZF モデルを与え、一段下げたそれが選択集合の公理を与えます。 ```agda base = V⊨ZF (choice→lem ac) ``` ## まとめ 本章の勘定はこれで完結します。空集合、対、和集合は既存の構成を `∈∈ₛ` と `⇔toPath` で変換したものです。置換は切り詰められていないファイバーの上の `sett` を通して直接従い、強い無限は `ω` の定義に一つの列の整列 (`numeralV≡#`) を加えたものです。残る二つの欄、完全な分出と冪集合に必要なのは、`Base.Impredicativity` がまとめた `Impredicativity` のパッキングそのものです。組み立てはその正確なコストで `V⊨ZF-impredicative` を与え、排中律がそれを主たる `V⊨ZF` へ引き上げます。最後の定理には、さらに独立な集合レベルの選択の実例が一つ要ります。`SetChoice (ℓ-suc ℓ)` は ZF の部分に `LEM (ℓ-suc ℓ)` を与え、同じ実例を一段下げた `SetChoice ℓ` が選択集合の補題を駆動し、`V⊨ZFC` が得られます。構成可能宇宙の諸章が内側から調べることになる宇宙が、ここに存在するようになりました。