---
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: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---
```agda
{-# OPTIONS --cubical --safe --guardedness #-}
```
# 累積階層は ZF と ZFC のモデル
```agda
open import Base.Prelude
```
宇宙レベルの計算は正確で、一度読んでおくべきものである。モデルの台はレベル `ℓ` の階層 `S` であり、それ自身 `Type (ℓ-suc ℓ)` の要素である。モデルの等号と所属を担う真理値は `hProp (ℓ-suc ℓ)` に住む。仮定 `ΩResizing (ℓ-suc ℓ) ℓ` は、以下で使う二つの大きさの制御、すなわちこの真理値レベルでの命題リサイズと、`hProp ℓ` の各命題を符号化して復元できる小さな台を与える。選択の補題はレベル `ℓ` の集合値族に対する選択を消費する。ZF の主定理は `ΩResizing (ℓ-suc ℓ) ℓ` を仮定し、その古典的帰結は `LEM (ℓ-suc ℓ)` を、ZFC の定理は `SetChoice (ℓ-suc ℓ)` を仮定する。したがってすべての仮定を支配する単一の一律のレベルはなく、各原理はその主張が意味を持つちょうどその場所で取られる。
```agda
module V.Model {ℓ : Level} where
```
```agda
open import Base.Impredicativity
using ( Resizing; ΩResizing; ΩResizing→Resizing )
open import Base.Classical using ( LEM; LEM→ΩResizing )
open import Base.Choice using ( SetChoice; SetChoice→LEM; lowerSetChoice )
open import FOL.ZFStructure using ( ZFStructure )
open import FOL.Syntax using ( Formula )
import FOL.Semantics
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV )
open import V.Smallness {ℓ} using ( separateFromSmall )
```
本章は、固定した一つの宇宙レベル `ℓ` の上で、累積階層の内側に ZF の各公理を実現する。集合の存在を要求する各公理については、その集合を構成し、所属関係が真理値のパスとして要求された記述にちょうど等しいことを証明する。関係する仮定は初めに区別しておく価値がある。基本的な構成、すなわち空集合、対、和集合は、階層自身の集合構成子の代償しか要らず、置換も同様で、その構成子の所属規則から直接読み取れる。完全な分出には命題リサイズが必要で、各充足命題に一段低い宇宙の代表を与える。冪集合には命題の命題宇宙リサイズ `ΩResizing` が必要である。`ΩResizing` は上位の命題宇宙を低いレベルの型で提示し、命題リサイズを含意する。組み立てられた ZF の定理 `V⊨ZF` はちょうど `ΩResizing (ℓ-suc ℓ) ℓ` を仮定する。古典的な便利のための帰結 `V⊨ZF-fromLEM` は `LEM (ℓ-suc ℓ)` からそのリサイズの束を導く。ZFC の部分では、定理 `V⊨ZFC` がレベル `ℓ-suc ℓ` の集合値族に対する選択を別に仮定する。ディアコネスクの定理により、これは ZF のリサイズ入力を得るための排中律を含意し、一段下げれば選択集合の公理を供給する。本章は、階層がすでに持つ構成を公理の要求する正確な形へ一公理ずつ変換し、これらの定理へ至る。
「階層が公理を満たす」とは形式的にはどういう意味であろうか。一階論理の諸章が語彙を供給する。構造とは h-集合である台のことであり、その等号と所属は、固定された二元型のブール値ではなく真理値を取る。論理式は対象言語の構文の要素であり、公理のスキーマはその自由変数の枠を量化する。充足は、台の要素からなる環境のもとで論理式を読み、真理値を返す関係である。以下では ZF の公理を、まさにこの言葉で一つずつ導き直す。
階層が提供するのは構造 `𝒮ᵥ` である。その等号は高次帰納型 `V ℓ` のパス型であり、所属は階層本来の `∈` である。この構造の外延性と正則性は階層そのものの章で証明済みで、ここでは再証明せずに引用する。さらに小ささの章から一つの道具を持ち越する。各値が小さい述語から集合を作る適合装置で、リサイズが小ささを供給しだい完全な分出になる。全体を通じて、命題の間の双条件は標準の書き換え `⇔toPath` で真理値の間のパスに変えられる。以下の仕様のほとんどすべてがこの一手で終わる。
cubical の三つの一般的な事実が後の証明を形作る。等号の型が命題である型への埋め込みは単射であり、復元した添字が唯一の可能性であることを示す場面で効く。第二成分が命題である依存対の間のパスは、第一射影の間のパスで決まる。さらに、像の集合への所属の主張はたいてい切り詰められた存在の形をしており、`∣_∣₁` で導入し、`rec₁` で命題値の目標へ消去する。矛盾は空の型で扱う。
```agda
open import Cubical.Functions.Embedding
using ( Embedding-into-isSet→isSet; isEmbedding→Inj )
```
中心となる構成は集合の構成子 `sett` である。小さな添字の型 `X` と族 `X → S` から像の集合を作り、所属 `y ∈ sett X ix` は、ある添字が `y` を呈示することが純粋に存在するとき、そのときに限り成る。置換はこの所属の規則から直接読み取る。階層が h-集合であること (`setIsSet` が記録する) により、パス型 `x ≡ y` は命題となり、構造の等号の正当な真理値になる。
```agda
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∈ → ⊥₀-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)` を与えるが、二つの所属がともに小形式である。書き換えは命題の截断の内部で行われ、目標も命題なので、`map₁` が証人をその場で変える。`∈∈ₛ` が `v ∈ₛ a` を `a` の通常の要素へ、`x ∈ₛ v` を `v` の通常の要素へ変える。結果は添字付き選言 `∃[ x ] P x の証人、すなわち`hProp` 上で台を量化する単なる存在の主張であり、どの元も選ばれない。
```agda
(λ x∈ → 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 (map₁
```
逆方向は同じ交換を逆向きに行う。添字付き選言の切り詰められた証人から出発し、`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 は各公理について、その所属がパスとして定められた記述に等しい集合を要求する。仮定は部分によって異なるので、分けて述べる価値がある。基本的な構成、すなわち空集合、対、和、無限と、置換の議論全体には、追加の仮定はまったく要らない。完全な分出には命題リサイズが必要で、各論理式の充足が点ごとに小さな命題になる。冪集合には `ΩResizing` から導かれる命題宇宙リサイズが必要で、その小さな台は `hProp ℓ` の各命題を符号化して復元できる。まとめられた定理は合算のコストを記録する。`V⊨ZF` はちょうど `ΩResizing (ℓ-suc ℓ) ℓ` を仮定し、その帰結 `V⊨ZF-fromLEM` は `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` が添字で呈示されると言うので、截断の内部でさらに `map₁` を行い、`f i ≡ v` なる対 `(i , q)` を取り出す。そして `v` における `x` の所属を `q` の逆向きに沿って運び、`f i` に着地させる。目標は截断を保つので、消去には `squash₁` を命題性の証拠として `rec₁` で `∥ Σ[ i ] ⟨ x ∈ˢ f i ⟩ ∥₁` に入る。結論は純粋な存在のままである。ある族の元が `x` を含むのであり、どの元も選ばれない。
```agda
→ ⟨ x ∈ˢ (⋃ (sett X f)) ⟩ → ∥ Σ[ i ∶ X ] ⟨ x ∈ˢ f i ⟩ ∥₁
union-family-out X f x h = rec₁ squash₁
(λ { (v , hv , hx) → 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)
```
```agda
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 = 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 = 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 (λ p → p .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
(rec₁ (setIsSet x a)
(λ { (inl e) → e ; (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 ∣ inl (singl-cls x .fst x∈ₛ) ∣₁
numeralV : ℕ → S
numeralV 0 = ∅
numeralV (suc n) = numeralV n ∪ ⁅ numeralV n , numeralV n ⁆
numeralV≡# : (n : ℕ) → numeralV n ≡ # n
```
二つの列の一致は `ℕ` 上の帰納法で示す。零では両辺とも空集合に簡約されるので、パスは `refl` である。後続の段階では、同じ「対の併合」の形の下で共點性によって両辺を書き換え、対の内部で同定 `pair-singleton` を適用する。外延性の結果が使われるのはこの一歩である。列が整列すると、残りの仕事は `ω` の所属をモデルの語彙で読むことである。`ω-specV` は、`ω` への所属が添字付き選言「`x` はある `numeralV` と等しい」と等しいことを述べる。添字は `Lift ℕ`、つまり持ち上げられた自然数の型を渡る。右辺の等しさは `≈ˢ`、すなわち構造の集合の外延的等しさなので、この主張は選ばれた提示ではなく集合 `x` そのものについてのものである。
```agda
numeralV≡# 0 = 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
(map₁ (λ { (i , p) → lift (lower i)
, sym p ∙ sym (numeralV≡# (lower i)) }))
(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≡ =
rec₁ pP
(λ { (v , (v∈₂ , x∈v)) → rec₁ pP
(λ { (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
; (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 ∣ 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 ∣ 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
```
```agda
pinZero : (z : S) → ⟨ z ∈ˢ a zero ⟩ → ⊥₀
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}
(((z ∈ˢ a n) ⊔ (z ≈ˢ a n)) .snd)
(subst (λ w → ⟨ z ∈ˢ w ⟩) (q (suc n)) z∈)
(λ z∈#n → ∣ inl (subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (q n)) z∈#n) ∣₁)
(λ z≡#n → ∣ 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 = rec₁ ((z ∈ˢ a (suc n)) .snd)
(λ { (inl z∈n) → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (q (suc n)))
(∈sucV-inl {A = # n} (subst (λ w → ⟨ z ∈ˢ w ⟩) (q n) z∈n))
; (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 ∷ []) ⊨ φ` を小さくしなければならないが、手作業でこれを行う Δ₀ の証人はない。必要な命題リサイズは、そのような各命題に点ごとに小さな代表を与え、小ささの適合装置 `separateFromSmall` を適用できるようにする。冪集合が提示するのは別の問題である。`a` の候補となる部分集合は `⟪ a ⟫` で添字付けられた所属の命題の族であり、そこから集合を作るには、各命題を一つの固定された小さな型へ符号化しなければならない。`ΩResizing` は、これらの符号化、復号、および必要な往復法則を取り出せる低いレベルの型を与える。後の組み立ては命題宇宙リサイズだけをパラメータとして受け取り、古典的な場合は `LEM→ΩResizing` から導かれる。
## 冪集合
冪集合は、ライブラリのヘッダ自身が提供しないと明言する唯一の構成であり、命題宇宙リサイズこそがそれを作る材料である。`a` の候補となる部分集合は、低いレベルの型 `Ω` への特性関数 `⟪ a ⟫ → Ω` で記述する。各値 `χ m` を復号すれば添字 `m` 上の命題が得られ、その命題が成り立つ添字が呈示する要素は `sett` で一つの集合に集められる。証明は二つの包含を確立する。関数が選んだものはすべて与えられた部分集合に含まれ、部分集合のすべての元が選ばれる、というものである。第二の方向は、命題に対する復号してから符号化する往復と、外延性を用いる。
冪集合の構成は、必要なデータを `ωr` から直接取り出す。それが与える低いレベルの型を `Ω`、上位の命題宇宙から `Ω` への型同値を `e` と書く。`e` の順写像は上位の命題を `Ω` の要素へ符号化する。
```agda
module Power (ωr : ΩResizing (ℓ-suc ℓ) ℓ) where
```
```agda
private
Ω : Type ℓ
Ω = ωr .fst
```
`ωr` の第二成分が同値 `e` である。その順写像 `code` は上位の各命題を `Ω` の代表へ送り、逆写像によってその代表から命題の情報を復元できる。
```agda
e : hProp (ℓ-suc ℓ) ≃ Ω
e = ωr .snd
code : hProp (ℓ-suc ℓ) → Ω
code = equivFun e
```
レベル `ℓ` の命題をまず上位の命題宇宙へ持ち上げ、それから符号化する。真の命題も同じように符号化し、基準値とする。
```agda
up : hProp ℓ → hProp (ℓ-suc ℓ)
up P = Lift {j = ℓ-suc ℓ} ⟨ P ⟩ ,
isOfHLevelLift 1 ⟨ P ⟩isProp
top : Ω
top = code ⊤
```
`x : Ω` を復号するには、真の命題の符号が `x` に等しいという命題を取る。`e` は `Ω` を命題宇宙と結ぶので、この等式を命題にするための h-集合構造も運ぶ。
```agda
setΩ : isSet Ω
setΩ = isOfHLevelRespectEquiv 2 e isSetHProp
decode : Ω → hProp ℓ
decode x = (top ≡ x) , setΩ top x
```
```agda
encode : hProp ℓ → Ω
encode P = code (up P)
```
冪集合の証明に必要な法則は一つだけである。命題を符号化して復号すると元の命題に戻る。一方では符号の等式を型同値によって反映し、`P` の証明を得る。他方では `P` の証明によってその持ち上げを真の命題と同一視し、両者の符号を同一視する。命題外延性がこの二つの写像を必要な命題の等式にまとめる。
```agda
decode∘encode : (P : hProp ℓ) → decode (encode P) ≡ P
decode∘encode P = ⇔toPath
(λ q → lower (subst ⟨_⟩
(invEq (congEquiv e) q) tt*))
(λ p → cong code (⇔toPath (λ _ → lift p) (λ _ → tt*)))
```
これで特性関数 `χ : ⟪ a ⟫ → Ω` は `decode (χ m)` が成り立つ添字を選び、族 `F` はそれらの添字が呈示する要素を集める。
```agda
F : (a : S) → (⟪ a ⟫ → Ω) → 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 ⟫ → Ω) (F a)
private
fwd : (a x : S) → ⟨ x ∈ˢ 𝒫V a ⟩ → ⟨ x ⊆ a ⟩
fwd a x = rec₁ (⟨ x ⊆ a ⟩isProp) λ { (χ , p) y y∈ₛx →
```
`x ⊆ a` の証明は元ごとに進み、まず冪集合への切り詰められた所属を消去する。`y` の `x` への所属を呈示するパスに沿って運び戻すと、それは選ばれた集合 `F a χ` への小さな所属になり、`∈∈ₛ` で変換すると呈示するファイバーが得られる。すなわち添字 `m` と、`decode (χ m)` が成り立つことの証明、さらに `y` を呈示された要素 `⟪ a ⟫↪ m` と同一視するパスである。
```agda
rec₁ (⟨ y ∈ₛ a ⟩isProp)
(λ { ((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 ⟫ → Ω
χₓ 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 = rec₁ (⟨ y ∈ₛ x ⟩isProp)
(λ { ((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` を消費し、冪集合は `ΩResizing` から取り出した低いレベルの型だけで組み立てられた。
```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 の各フィールドにはすでに証拠が揃っており、この節はそれらを一つの数学的定理へ組み立てる。累積階層 `V ℓ` は ZF を満たす、という定理である。公理はその導出の仕方ごとに分類できる。空集合、対、和集合は章の冒頭で変換した基本的な集合である。完全な分出と冪集合は二つの小ささの結果で、どちらも同じ命題宇宙リサイズの仮定から得られる。分出は導かれた `resizing` で各充足命題を小さくして `separateFromSmall` を適用できようにし、冪集合は命題宇宙リサイズだけを使う。置換は切り詰められていないファイバーから作った像であり、無限はライブラリの `ω` と数項の整列である。残るのは梱包の一段階であるが、そこには本物の数学的入力が一つある。`isZFModel` の各フィールドは `isContr (SetOf Q)`、すなわち実現する集合と、すべての実現者をそこへ収縮させるデータを要求する。外延性がまさにその収縮を `setOf-unique` を通して与える。主定理 `V⊨ZF` はちょうど `ΩResizing (ℓ-suc ℓ) ℓ` を仮定し、便利のための帰結 `V⊨ZF-fromLEM` は `LEM (ℓ-suc ℓ)` を仮定して、`LEM→ΩResizing` により命題宇宙リサイズの仮定を導く。
組み立ては `ΩResizing (ℓ-suc ℓ) ℓ` を単一のパラメータとして受け取る。冪集合の構成はその低いレベルの型と型同値を直接使い、分出は `ΩResizing→Resizing` から導かれる命題リサイズを使う。完全な分出は直接に述べられる。集合 `a` と自由変数の枠を一つ持つ論理式 `φ` が与えられたとき、各 `y` について真理値 `y ∈ˢ s` が「`y ∈ˢ a`」と「一点環境 `y ∷ []` での `φ` の充足」の連言にパスとして等しい集合 `s` を作る。これはモデルの record が要求する分出の仕様の形そのものである。
```agda
module VModel (ωr : ΩResizing (ℓ-suc ℓ) ℓ) where
```
```agda
open Power ωr public
private
resizing : Resizing (ℓ-suc ℓ) ℓ
resizing = ΩResizing→Resizing ωr
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` が揃うと、`VModel.V⊨ZF` はすでに示した証拠を `isZFModel` に組み立てる。以下の公開定理はこの組み立てに命題宇宙リサイズの仮定を渡す。
```agda
separateFull a φ =
separateFromSmall a (λ y → (y ∷ []) ⊨ φ) (λ y → resizing ((y ∷ []) ⊨ φ))
V⊨ZF : isZFModel
V⊨ZF = 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` は、単一の仮定 `ΩResizing (ℓ-suc ℓ) ℓ` の下で累積階層 `V ℓ` が ZF を満たすことを述べる。二つの図式のフィールドはどちらもすべての論理式を受け取る関数なので、分出と置換はすべての論理式に対して一度に成り立つ。そこでは一階論理の諸章による対象言語の深い埋め込みが働く。別の便利のための定理 `V⊨ZF-fromLEM` は `LEM (ℓ-suc ℓ)` を受け取り、そこから命題宇宙リサイズの仮定を導く。証明されるのは、明示された仮定の下でのモデルの構成であり、無条件の無矛盾性の主張ではない。
公開される `V⊨ZF` は、正確な命題宇宙リサイズの境界での組み立てそのものである。`V⊨ZF-fromLEM` の定義は一度の合成である。`LEM→ΩResizing` は排中律を用い、上位の命題宇宙を低いレベルの型 `Lift Bool` で提示し、得られた束を `V⊨ZF` に渡す。冪集合の構成はこの提示を直接使い、`ΩResizing→Resizing` は分出に必要な各命題の代表を導く。したがって後続レベルでの一つの古典的仮定が二つの大きさの制御をともに供給するが、それは主要な境界ではなく帰結として明示される。
```agda
V⊨ZF : ΩResizing (ℓ-suc ℓ) ℓ → isZFModel
V⊨ZF = VModel.V⊨ZF
V⊨ZF-fromLEM : LEM (ℓ-suc ℓ) → isZFModel
V⊨ZF-fromLEM lem = V⊨ZF (LEM→ΩResizing lem)
```
## 選択公理を別に仮定する
排中律から選択は導けないため、ZFC の最後の公理は独立な仮定として受け、選択集合の公理はそこから証明する。インターフェースは `SetChoice` である。h-集合 `X : Type ℓ` と h-集合値の族 `B : X → Type ℓ` に対し、各値が単に居住するなら、`X` 全体の上の選択関数が、切り詰められた形で存在する。以下の補題は、このインターフェースのレベル `ℓ` の実例と、固定された階層構造 `𝒮ᵥ` 上の `isZFModel` を仮定し、そこから交 `∩` とその仕様を使う。選択を施す族は小さな提示である。添字の型は h-集合 `⟪ a ⟫` であり、添字 `m` 上のファイバーは `m` が提示する集合 `⟪ ⟪ a ⟫↪ m ⟫` である。したがって選択が選ぶのは集合の要素ではなく提示の添字である。選ばれた添字から、`sett` を一度適用して集合 `c` を作る。そして互いに素であることの仮定 `disj` により、モデルの交を通して、`c` が `a` の各元と交わる点の集合が可縮、したがって一意であることが示される。切り詰めは設計上非対称である。選択集合そのものは単なる存在であるが、各交わりは明示的な `isContr` のデータを持つ。最終定理は一つの `SetChoice (ℓ-suc ℓ)` の実例を二度使う。`SetChoice→LEM` がそれを ZF の部分のための `LEM (ℓ-suc ℓ)` へ変換し、`lowerSetChoice` がそれを選択の補題のための `SetChoice ℓ` へ下げる。つまり `V⊨ZFC` は選択だけから証明される。排中律はディアコネスクの定理により選択から回収されるのであって、逆ではない。
選択集合の構成には二つの準備的事実が使われる。第一は、選択を適用する添字の型に関するものである。各提示の型 `⟪ a ⟫` は h-集合である。`⟪ a ⟫↪` を通して階層へ埋め込まれ、その埋め込みの性質 `isEmb⟪ a ⟫↪` は提示の導入時に記録済みであり、階層自身は `setIsSet` により h-集合だからである。cubical の一般結果 `Embedding-into-isSet→isSet` が埋め込みに沿って h-集合性を引き戻すので、任意の集合 `a` に対して `isSet⟪ a ⟫` が成る。したがって添字の間の等号の型はすべて命題である。同じ結果を各要素 `⟪ a ⟫↪ m` に適用すると、族の各値 `⟪ ⟪ a ⟫↪ m ⟫` も h-集合となり、`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 → (P v) .snd) (u (w .fst) (w .snd))
```
```agda
module ChoiceLemma (zf : isZFModel) (ac : SetChoice ℓ) where
```
```agda
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 ⟫`、つまり各添字が提示する集合である。各値は `isSet⟪_⟫` により h-集合である。残るのはそれぞれを単に居住させることで、それが `pick` の役目である。各添字 `m` に対し、`memb a m` が確かめる要素のところで `inh` が、提示された集合 `⟪ a ⟫↪ m` の要素の単なる存在を与え、`∈-asFiber` がその所属から `⟪ a ⟫↪ m` の提示への実際の添字を取り出す。入力の切り詰めは終始保存されるので、`pick` が `a` の要素の内部で点を選ぶと主張することはなく、単なる存在に添字を付け直すだけである。
```agda
→ isContr (Σ[ z ∶ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)) ∥₁
choice a inh disj = map₁ mk (ac ⟪ a ⟫ isSet⟪ a ⟫
(λ m → ⟪ ⟪ a ⟫↪ m ⟫)
(λ m → isSet⟪ ⟪ a ⟫↪ m ⟫) pick)
where
pick : (m : ⟪ a ⟫) → ∥ ⟪ ⟪ a ⟫↪ m ⟫ ∥₁
pick m = map₁
```
選択関数はその後、各添字 `m` に対して提示された集合の実際の要素 `g m` を返す。添字の h-集合上の選択は切り詰められていないデータ、すなわち `⟪ a ⟫↪ m` の提示の要素を与える。残りの `mk` はこれを結論へ包装する。集合 `c` と、`a` の各元 `x` に対する、交 `c ∩ x` の点の型の緊縮データである。選択関数が添字の水準で既に切り詰められていないデータを生んでいるため、`mk` は普通の関数であり、切り詰めが再び現れるのは全体が `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 = 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 ℓ)` の一つの実例が二度使われる。`SetChoice→LEM` がそれを `LEM (ℓ-suc ℓ)` へ変換し、`LEM→ΩResizing` がさらに `V⊨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-集合で、各値も同じく提示の h-集合である。したがって選択が選ぶのは族の提示の添字である。その後、非交性が各交の可縮性を示す。したがって選択集合は単に存在するだけであり、各交点は明示的な `isContr` のデータとして一意である。定理 `V⊨ZFC` が述べるのは結合後の正確なコストである。`SetChoice (ℓ-suc ℓ)` は `SetChoice→LEM` を通して `LEM (ℓ-suc ℓ)` を与え、さらに `LEM→ΩResizing` が ZF の正確な入力を供給する。同じ選択の実例を `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
```
一つの実例が二つの結論に使われる。`SetChoice→LEM` はそれをレベル `ℓ-suc ℓ` の排中律へ変換し、`LEM→ΩResizing` がさらに `V⊨ZF` の要求する命題宇宙リサイズの仮定へ変換するので、`base` が得られる。選択集合の部分では、`lowerSetChoice` が同じ実例を `SetChoice ℓ` に下げる。これが `ChoiceLemma.choice` の要求するものであり、補題は `base` に適用される。こうして、後続レベルでの一つの選択の実例が明示的な古典的リサイズの橋渡しを通して ZF モデルを与え、一段下げたそれが選択集合の公理を与える。
```agda
base = V⊨ZF (LEM→ΩResizing (SetChoice→LEM ac))
```
## まとめ
本章の勘定はこれで完結する。空集合、対、和集合は既存の構成を `∈∈ₛ` と `⇔toPath` で変換したものである。置換は切り詰められていないファイバーの上の `sett` を通して直接従い、強い無限は `ω` の定義に一つの列の整列 (`numeralV≡#`) を加えたものである。残る二つの欄、完全な分出と冪集合に必要なのは、`Base.Impredicativity` がまとめた `Impredicativity` の命題宇宙リサイズの仮定そのものである。主定理 `V⊨ZF` はその正確なコストを露わにし、`V⊨ZF-fromLEM` はその古典的な便利のための帰結である。最後の定理には、さらに独立な集合値族に対する選択の実例が一つ要る。`SetChoice (ℓ-suc ℓ)` は ZF の部分に `LEM (ℓ-suc ℓ)` を与え、そこから命題宇宙リサイズが得られる。同じ実例を一段下げた `SetChoice ℓ` が選択集合の補題を駆動し、`V⊨ZFC` が得られる。構成可能宇宙の諸章が内側から調べることになる宇宙が、ここに存在するようになった。