---
title: "基本公理"
module: L.Axioms.Basic
lang: ja
site: "Bedrock"
description: "基本公理"
stage: "構成可能段階と公理"
reading_order: 31
canonical: https://bedrock.institute/ja/L.Axioms.Basic.html
html: L.Axioms.Basic.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Axioms/Basic.lagda.md
prerequisites: [Base.Prelude, FOL.Syntax, FOL.ZFStructure, FOL.ZFModel, V.Hierarchy, V.Model, V.Coding, L.Definability, L.Constructible, L.Ordinal]
routes: [constructible-axioms]
translations: [https://bedrock.institute/en/L.Axioms.Basic.md, https://bedrock.institute/zh/L.Axioms.Basic.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---
```agda
{-# OPTIONS --cubical --safe --guardedness #-}
```
# 基本公理
```agda
open import Base.Prelude
```
設定は宇宙レベル `ℓ` を一つ固定し、そのレベルの累積階層 `V` の中で作業する。本章はすべて構成的であり、排中律もサイズ変更も選択公理も仮定しない。公理が証明される台は、`V` の集合と構成可能性の証明書 `isL` の対からなる型であり、以下の主張はすべて周囲の階層だけから立証される。
```agda
module L.Axioms.Basic {ℓ : Level} where
```
```agda
open import FOL.Syntax using ( Formula; var; con; _≐_; _∈̇_; _∨̇_; ⊤̇; ⊥̇; ∃̇∈ )
open import FOL.ZFStructure using ( ↾-reflects; module hPropView )
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV )
open import V.Model {ℓ}
using ( empty-spec; pair-spec; union-spec; self∈sucV; ∈sucV-elim
; pair-singleton )
open import V.Coding {ℓ} using ( pr )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Constructible {ℓ}
using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-layer
; layer-trans; 𝒟ₒ; 𝒟ₒ-intro; Lset-in; Lset-out; Lset⊆𝒟ₒ
; Lset-mono; Lset→isL )
open import L.Ordinal {ℓ} using ( ∅-ord; suc-ord; bound2 )
```
集合を作る演算を構成可能宇宙へ移すには、どうすればよいであろうか。集合が `L` に属するとは、ある順序数段階 `Lset σ` の定義可能部分集合として表示できることである。本章では、必要な入力を含む一つの順序数段階を見つけ、その段階上で目的の集合を外延にもつ論理式を書き、周囲の階層で外延的な等式を証明する、という方法を繰り返す。
閉包補題 `defSet→isL` がこの方法を完成させる。順序数 `σ` と、外延が `x` である一変数論理式の単なる存在が与えられると、`𝒟ₒ-intro` は `x` を `Lset σ` の定義可能部分集合として認識し、`𝒟ₒ→isL` はそれを `L` に入れる。恒等式 `Lset (sucV σ) ≡ 𝒟ₒ (Lset σ)` は段階の計算を説明する。次の段階は、現在の段階の定義可能部分集合全体にちょうど一致する。`LsetS` と `𝒟ₒS` はこの二つの集合を台 `S` の要素としてまとめる。
この方法で空集合、非順序対、和集合を `L` の中に構成する。外延性では推移性により構成可能な要素についての一致を周囲のすべての要素へ広げるが、正則性では階層の可到達性の証明を再帰的に制限する。二つの入力に共通段階が必要なとき、`bound2` は元の段階を比較せずに共通の厳密上界を与える。
```agda
open import Cubical.HITs.PropositionalTruncation using ( rec2 )
open import Cubical.Foundations.Prelude using ( isPropIsContr )
```
閉包パターンの切り出しのステップは一階の言語の中で行われる。その論理式は構造の小さな添字型の上にあり、等式と所属が原子的な述語で、選言と有界存在量化が使える。これがまさに定義可能性の演算子が消費するものである。構造から部分構造への移行について、後で効いてくる周囲の事実が二つある。制限の中の二つの要素の間のパスは、すでに基底の集合の間のパスであり、継承される公理が利用するのはこの向きである。
持ち上げる対象となる各構成は、周囲の階層ですでに所属の法則を満たしている。空集合は元をひとつももたず、非順序対のすべての元は二つの項のいずれかであり、和集合は正確な双方向の特徴づけをもつ。これらの周囲の法則は階層で一度証明され、後で切り出される論理式を外延性で検査するときの基準となる。再証明されるのではなく、継承されるのである。計算にはさらに二つの周囲の事実が入る。後者 `sucV σ` への所属は「`σ` の要素である」場合と「`σ` そのものである」場合に分かれること、そして一元集合が対 `⁅ x , x ⁆` と同一視されることである。順序対のクラトフスキー符号 `pr` がどの段階に置かれるかは、非順序対から計算される。
構成可能な側は、塔とその簿記を供給する。`Lset` は集合を添字として段階を与え、`IsOrd` は順序数性の証明書、`isL` は構成可能集合のクラスで、`isL-trans` により推移的である。段階の定義可能冪集合は `𝒟ₒ` である。`𝒟ₒ-intro` が論理式と外延的な等式から定義可能部分集合を認識し、`Lset-in`、`Lset-out`、`Lset⊆𝒟ₒ`、`Lset-mono`、`Lset→isL` は段階への所属の変換、より大きな段階に沿った持ち上げ、構成可能性の証明書としての読み替えを可能にする。段階の推移性は `layer-trans` である。
段階を制御する順序数の事実は三つである。空集合は順序数であり、順序数の後者も順序数であり、`bound2` は二つの順序数をそれぞれ真に含む順序数を返す。対の構成では最後の結果により、もとの段階を比較したり最大のものを選んだりせず、二つの構成可能な実引数を一つの共通段階へ置く。有限添字型はその段階内の有限像を記述し、二つの型の和はそれらを定義する論理和を表す。
```agda
open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )
```
周囲の階層の所属は命題値であり、提示の埋め込みのファイバーも命題である。そのため `∈-asFiber` は、与えられた所属の証明を小さな提示の実際の添字と、その要素へ戻るパスに変換する。すなわち `⟨ x ∈ Lset σ ⟩` から `m : ⟪ Lset σ ⟫` と `⟪ Lset σ ⟫↪ m ≡ x` が得られ、論理式はこの要素を定数で名指せる。対応するファイバー自体が命題なのでデータを直接得られるのであり、この段階で消去すべき別の外側の切り詰めはない。
```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; sett )
open import Cubical.HITs.CumulativeHierarchy.Properties
using ( _∈ₛ_; ∈∈ₛ; ∈-asFiber; extensionality; _⊆_; ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
```
本章で必要な周囲の集合は、それぞれ正確な所属の特徴づけを伴う。空集合には `∅-empty`、非順序対 `⁅_,_⁆` とその一元の変種には `pairing-ax`、和集合には `union-ax` と `⋃_` である。これらは階層そのものの分類結果であり、所属の法則の両方向を与えるので、後で切り出される定義可能部分集合は、これらと突き合わせて外延性で検査できる。後者演算 `sucV` が次の段階の添字を供給する。
```agda
using ( ∅; ∅-empty; ⁅_,_⁆; ⁅_⁆s; pairing-ax; ⋃_; union-ax
; module InfinitySet )
open InfinitySet using ( sucV )
open hPropView 𝒮ʟ
```
意味論の側は一度だけ確定する。真理値はレベル `ℓ-suc ℓ` の命題なので、論理式の解釈は通常の型構成に落ちる。制限された構造を命題値の意味論を通して読むと、構造的な所属 `∈ˢ` と、命題の基礎型を取る括弧の記法 `⟨_⟩` が得られる。実現する集合とは、台 `S` の要素、すなわち構成可能性の証明書を添えた集合に、その所属がどの仕様を実現するかを言う等式を添えたものである。これが型 `SetOf Q` である。一つの実現集合を可縮性のデータへ変える原理 `setOf-unique` が、本章の残りの各公理フィールドを純粋な存在の問題へ帰着させる。
```agda
module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf; setOf-unique )
```
## 定義可能部分集合は構成可能である
段階 `Lset (sucV σ)` は `δ ∈ sucV σ` で添字づけられた集合族の和である。`σ ∈ sucV σ` なので、集合 `𝒟ₒ (Lset σ)` は和を取られる集合の一つである。したがって、そのすべての要素は `Lset (sucV σ)` に属する。`σ` が順序数ならその後者も順序数であり、この段階への所属から `isL` の証明書が得られる。
補題 `𝒟ₒ→isL` は、順序数 `σ` とその順序数性の証明書 `oσ`、集合 `x`、そして「`x` が `σ` での段階の定義可能冪集合に属する」証明を受け取り、`x` が構成可能であると結論する。証明は `x` を一段引き上げる。`σ` は自身の後者 `sucV σ` の要素でもあるので、包含 `Lset-in` は「`𝒟ₒ (Lset σ)` への所属」を「段階 `Lset (sucV σ)` への所属」へ変える。この段階の添字は `suc-ord oσ` により順序数である。そのうえで `Lset→isL` を一度適用すれば、この段階への所属が証明書 `isL x` に変わる。切り詰められた仮定はそのまま使われる。仮定は `Lset-in` に直接渡され、その結論も同じ形で切り詰められているため、構成可能性の証人が取り出されたり選ばれたりすることはない。
```agda
𝒟ₒ→isL : (σ : V ℓ) → IsOrd σ → (x : V ℓ) → ⟨ x ∈ 𝒟ₒ (Lset σ) ⟩ → ⟨ isL x ⟩
𝒟ₒ→isL σ oσ x x∈𝒟ₒσ = Lset→isL (sucV σ) (suc-ord oσ) x
(Lset-in (sucV σ) σ x (self∈sucV σ) x∈𝒟ₒσ)
```
閉包の補題を演算子の認識の原理と合成すると、本章のどの構成も使う形が得られる。集合を `L` の中に置くには、順序数の段階、論理式、そしてその論理式がちょうどその集合を定義すると言う外延的な等式を示せばよいのである。この出示は存在の water準にすぎない。すなわち論理式と等式の組の切り詰められた対であり、それで十分である。以下の空集合、対、和集合はその最初の三つの実例である。
`defSet→isL` の仮定は切り詰められた存在式である。すなわち、段階の要素の上のアリティ 1 の論理式 `φ` で `defSet (Lset σ) φ ≡ x` を満たすものが、単に存在するということである。認識の原理 `𝒟ₒ-intro` はまさにこのようなデータを「`x` が `𝒟ₒ (Lset σ)` に属する」という所属へ変える。この所属は命題なので、そこへの切り詰めの除去は正当であり、論理式が選ばれることはない。`𝒟ₒ→isL` との一行の合成がただちに `isL x` を与える。順序数の段階、定義する論理式、外延的な等式、というこの証明書の形こそ、本章の残りが実例化するパターンである。
```agda
defSet→isL : (σ : V ℓ) → IsOrd σ → (x : V ℓ)
→ ∥ Σ[ φ ∶ Formula ⟪ Lset σ ⟫ 1 ] (DefOf.defSet (Lset σ) φ ≡ x) ∥₁
→ ⟨ isL x ⟩
defSet→isL σ oσ x p = 𝒟ₒ→isL σ oσ x (𝒟ₒ-intro (Lset σ) x p)
```
このパターンの第零の実例は段階そのものである。「真」の論理式は集合の全体を定義するので、どの段階もそれ自身の定義可能部分集合であり、したがって一段上で構成可能である。これこそが、段階を一つの論理式で**名指す**ことを可能にする事実であり、段階で量化子を有界にする構成はすべてこれに依拠する。さらに、段階とその構成可能性の証明書を対にする包み `LsetS` と合わせて、段階そのものが `L` の台の要素になる。
`isL-Lset` の証明は `x = Lset β` における `𝒟ₒ→isL` の直接の実例である。証人となる論理式は定数真の論理式 `⊤̇` であり、`defSet⊤≡A` がその外延を台の集合の全体、ここでは段階 `Lset β` 自身と同一視する。論理式と等式の組を一度の切り詰めに包めば `𝒟ₒ (Lset β)` の要素が得られ、閉包の補題がそれを `⟨ isL (Lset β) ⟩` へ引き上げる。証明は段階の内部構造を一切調べず、論に入るのは `suc-ord` を通しての `β` の順序数性だけである。
```agda
opaque
isL-Lset : (β : V ℓ) → IsOrd β → ⟨ isL (Lset β) ⟩
isL-Lset β oβ = 𝒟ₒ→isL β oβ (Lset β)
(𝒟ₒ-intro (Lset β) (Lset β) ∣ ⊤̇ , DefOf.defSet⊤≡A (Lset β) ∣₁)
LsetS : (β : V ℓ) → IsOrd β → S
```
制限された構造の台 `S` は、集合と「それがクラスに属する」ことの証明の対からなる。`LsetS` は順序数の段階に対してまさにこの対を与える。すなわち基礎の集合 `Lset β` と、今作った証明書である。この要素を通して、段階は普通の台の点として構成可能な構造に入る。
```agda
LsetS β oβ = Lset β , isL-Lset β oβ
```
## 後者段階
塔のステップは定義可能冪集合であり、後者の添字ではステップがすべてである。`Lset (sucV σ)` は `𝒟ₒ (Lset σ)` にちょうど一致する。この恒等式は二つの包含として証明される。一つの向きには、`σ` は自身の後者の要素なので、`𝒟ₒ (Lset σ)` は和を取られる集合の一つなので、その各要素が次の段階に入る。もう一つの向きでは、`Lset (sucV σ)` の要素は `sucV σ` のある `δ` に対する `𝒟ₒ (Lset δ)` に属する。`δ` が `σ` の要素ならその集合はすでに `Lset σ` にあり、したがってその定義可能部分集合の一つである。`δ` が `σ` そのものなら包含は直ちに成る。どちらの向きも相対化を使わず、演算子の単調性も要らない。ここには `σ` の順序数性の仮定もない。
この恒等式があれば、定義可能冪集合の構成可能性はただちに従う。段階は一段上で構成可能であり、段階の定義可能冪集合はまさにその次の段階だからである。
二つの集合は周囲の外延性によって比較され、パスは一対の包含へ帰着する。より難しい包含には橋渡しの補題が要る。次の段階の要素 `x` から、ある前の段階の定義可能冪集合が `x` を含むことが単に成り立ち、その証人 `δ` は `sucV σ` の要素である。`sucV σ` の構成により、その要素は `σ` の要素か `σ` 自身のどちらかなので、この証人はまさに議論が場合分けできる情報である。
```agda
Lset-suc : (σ : V ℓ) → Lset (sucV σ) ≡ 𝒟ₒ (Lset σ)
Lset-suc σ = extensionality (Lset (sucV σ)) (𝒟ₒ (Lset σ)) (sub₁ , sub₂)
where
fromEarlier : (x : V ℓ)
→ Σ[ δ ∶ V ℓ ] (⟨ δ ∈ sucV σ ⟩ × ⟨ x ∈ 𝒟ₒ (Lset δ) ⟩)
```
証人の消去は、まさにこの二分法を使う。`∈sucV-elim` は「`δ` が `sucV σ` に属する」証明と二つの分岐を受け取る。第一の分岐では `δ` は `σ` の要素なので、`Lset-in` が `x` を `Lset σ` の内側に置き、補題 `Lset⊆𝒟ₒ` は段階のすべての要素がその定義可能部分集合の一つであると言うので、`x` は `𝒟ₒ (Lset σ)` へ引き上げられる。第二の分岐では `δ` は `σ` 自身であり、`subst` が与えられた所属をパス `δ ≡ σ` に沿って輸送し、段階の添字を付け替える。目標全体 `x ∈ 𝒟ₒ (Lset σ)` が命題であることこそ、切り詰められた証人をここで除去できる前提である。
```agda
→ ⟨ x ∈ 𝒟ₒ (Lset σ) ⟩
fromEarlier x (δ , (δ∈suc , x∈𝒟ₒδ)) =
∈sucV-elim {A = σ} {x = δ} ((x ∈ 𝒟ₒ (Lset σ)) .snd) δ∈suc
(λ δ∈σ → Lset⊆𝒟ₒ σ x (Lset-in σ δ x δ∈σ x∈𝒟ₒδ))
(λ δ≡σ → subst (λ w → ⟨ x ∈ 𝒟ₒ (Lset w) ⟩) δ≡σ x∈𝒟ₒδ)
```
第一の包含はこの橋を順向きに使う。`Lset (sucV σ)` の構造的な要素は `∈∈ₛ` によって周囲の所属へ変換され、段階の特徴づけ `Lset-out` が切り詰められた前段階の証人を返し、`fromEarlier` がそれを `𝒟ₒ (Lset σ)` へ写す。消去の着地点は命題 `x ∈ 𝒟ₒ (Lset σ)` であり、`δ` の選択を捨ててよい根拠はこれである。逆向きの包含には、`σ` が自身の後者に属することだけが要る。`∈∈ₛ` で構造的な所属を周囲の形へ変換したのち、証人 `self∈sucV σ` とともに `Lset-in` を適用すれば、`𝒟ₒ (Lset σ)` の任意の要素が `sucV σ` での段階に直接入る。二つの包含を合わせれば、パスとしての恒等式が得られる。
```agda
sub₁ : ⟨ Lset (sucV σ) ⊆ 𝒟ₒ (Lset σ) ⟩
sub₁ x x∈ₛ = ∈∈ₛ {a = x} {b = 𝒟ₒ (Lset σ)} .fst
(rec₁ ((x ∈ 𝒟ₒ (Lset σ)) .snd) (fromEarlier x)
(Lset-out (sucV σ) x (∈∈ₛ {a = x} {b = Lset (sucV σ)} .snd x∈ₛ)))
sub₂ : ⟨ 𝒟ₒ (Lset σ) ⊆ Lset (sucV σ) ⟩
```
もう一方の包含では、`self∈sucV σ` により、`𝒟ₒ (Lset σ)` が `Lset (sucV σ)` の定義で和を取られる集合の一つだと分かる。したがって `Lset-in` は、その定義可能冪集合の各要素を後者段階へ送る。第一の包含と合わせ、周囲の外延性からパス `Lset (sucV σ) ≡ 𝒟ₒ (Lset σ)` が得られる。この恒等式には `σ` の順序数性の仮定はない。
```agda
sub₂ x x∈ₛ = ∈∈ₛ {a = x} {b = Lset (sucV σ)} .fst
(Lset-in (sucV σ) σ x (self∈sucV σ)
(∈∈ₛ {a = x} {b = 𝒟ₒ (Lset σ)} .snd x∈ₛ))
```
後者の恒等式は、段階が一段上で構成可能という主張を、定義可能冪集合そのものについての主張へ変える。`Lset (sucV σ)` はちょうど `𝒟ₒ (Lset σ)` であり、前者は前の補題によって構成可能なので、任意の順序数の段階の定義可能冪集合は構成可能である。したがってそれを、構成可能性の証明書を添えた `L` の集合として台の要素にまとめ直せる。
証明は後者の恒等式に沿った輸送である。後者における (その順序数性は `suc-ord oσ` である) `isL-Lset` の適用が `⟨ isL (Lset (sucV σ)) ⟩` を与え、パス `Lset-suc σ` に沿って目標を書き換えれば `⟨ isL (𝒟ₒ (Lset σ)) ⟩` になる。この恒等式のほかに演算子の性質は何も使っていない。
```agda
opaque
isL-𝒟ₒ : (σ : V ℓ) → IsOrd σ → ⟨ isL (𝒟ₒ (Lset σ)) ⟩
isL-𝒟ₒ σ oσ = subst (λ w → ⟨ isL w ⟩) (Lset-suc σ)
(isL-Lset (sucV σ) (suc-ord oσ))
𝒟ₒS : (σ : V ℓ) → IsOrd σ → S
```
包み `𝒟ₒS` は段階の定義可能冪集合とその構成可能性の証明書を対にし、ちょうど `𝒟ₒ (Lset σ)` を指す台の要素を与える。前の節が段階そのものをまとめたのに対し、こちらは段階の定義可能部分集合の全体をまとめる。
```agda
𝒟ₒS σ oσ = 𝒟ₒ (Lset σ) , isL-𝒟ₒ σ oσ
```
## 有限族
閉包のパターンは有限族の上でいちばんよく見える。段階 `Lset σ` と、その要素 `n` 個からなる族を固定する。それらの像は集合 `finSet n h` であり、「これと等しい」の有限論理和がちょうどその像を段階から切り出す。長さ零では論理式は偽となり、その後は長さが一つ増えるごとに定数と自由変数の比較が一つ増える。族の要素は繰り返してよく、異なる位置が同じ集合を名指してもかまわない。
内容のすべては一つの帰納である。論理和の充足と族への命中とを同一視するもので、両方向とも名指された要素の埋め込まれた代表に対して述べられる。両方向が揃えば、周囲の外延性によって `defSet≡`、すなわち定義可能部分集合が像にちょうど一致するという等式が証明される。`finSet∈𝒟ₒ` は像を `𝒟ₒ (Lset σ)` の要素として記録し、`finSetL` は「族の各要素が段階に属する」という仮定から、閉包の補題 `defSet→isL` を経て証明書 `isL (finSet n h)` を与える。
像の集合は直接定義される。`finSet n h` は、階層の宇宙へ持ち上げた添字型 `Fin n` と、`lower` をほどこしてから `h` を適用する添字写像によって表現された集合である。所属は階層に適した切り詰めの形で特徴づけられる。`y` が `finSet n h` に属するのは、ある添字 `i` が `h i ≡ y` を満たすことが単に成り立つとき、そのときに限る。`finSet-in` と `finSet-out` の各方向は切り詰めの内部での一つの写像である。表現された集合への所属は、構成上、添字の切り詰められた存在だからである。
```agda
finSet : (n : ℕ) → (Fin n → V ℓ) → V ℓ
finSet n h = sett (Lift {ℓ-zero} {ℓ} (Fin n)) (λ i → h (lower i))
finSet-in : (n : ℕ) (h : Fin n → V ℓ) (y : V ℓ)
→ ∥ Σ[ i ∶ Fin n ] (h i ≡ y) ∥₁ → ⟨ y ∈ finSet n h ⟩
finSet-in n h y = map₁ (λ { (i , q) → lift i , q })
```
逆向きの所属の補題 `finSet-out` は、同じ写像を逆に読んだもので、持ち上げられた添字から `Fin n` へ降りる。つづいて定義可能性の作業は順序数の段階 `σ` で行われる。`DefOf (Lset σ)` の内側で作業すると、定数のアルファベットはその段階の小さな添字型 `⟪ Lset σ ⟫` に確定し、段階の要素は定数で名指せる。問題になる定義可能部分集合は、`Lset σ` から切り出されるものである。
```agda
finSet-out : (n : ℕ) (h : Fin n → V ℓ) (y : V ℓ)
→ ⟨ y ∈ finSet n h ⟩ → ∥ Σ[ i ∶ Fin n ] (h i ≡ y) ∥₁
finSet-out n h y = map₁ (λ { (i , q) → lower i , q })
```
```agda
module FinOf (σ : V ℓ) (oσ : IsOrd σ) where
```
```agda
module DefC = DefOf (Lset σ)
```
論理式は等式の有限論理和である。長さ零では等しい相手がいないので論理式は偽となり、長さが後者のときは自由変数を族の最初の要素を名指す定数と比較し、残りの要素は族をずらした再帰呼び出しに委ねる。アリティは全体を通して一である。一つの自由変数のスロットが論理和全体に使われ、関数 `g` は単射である必要はなく、異なる位置が同じ要素を名指してもかまわない。
```agda
finDisj : (n : ℕ) → (Fin n → ⟪ Lset σ ⟫) → Formula ⟪ Lset σ ⟫ 1
finDisj 0 g = ⊥̇
finDisj (suc n) g =
(var zero ≐ con (g zero)) ∨̇ finDisj n (λ i → g (suc i))
private
```
橋渡しの主張 `Hits` は、環境で名指された要素が族に単に命中することを言う。パスは名指された要素の埋め込まれた代表 `⟪ Lset σ ⟫↪ (g i)` に対して書かれる。二つの方向は、定義可能部分集合が見る「論理和の充足」と、像の集合が見る「族への命中」とを結ぶ。
```agda
Hits : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫) (y : V ℓ) → Type (ℓ-suc ℓ)
Hits n g y = ∥ Σ[ i ∶ Fin n ] (⟪ Lset σ ⟫↪ (g i) ≡ y) ∥₁
sat→hits : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫) (m : ⟪ Lset σ ⟫)
→ ⟨ (DefC.ι m ∷ []) DefC.⊨ᵐ finDisj n g ⟩
→ Hits n g (⟪ Lset σ ⟫↪ m)
```
充足から命中へは、長さについての再帰で進む。零では論理式は偽であり、その証明は荒謬である。後者では充足は切り詰められた論理和である。左の分岐では環境が最初の定数と等しく、添字 `zero` が得られる。右の分岐では再帰呼び出しがずらした族への命中を返し、その添字が一つ上げられる。各分岐は証人を切り詰めの内部で返し、目標の `Hits` が命題値であるため、外側の消去は正当である。
```agda
sat→hits 0 g m bot = ⊥*-rec bot
sat→hits (suc n) g m = rec₁ squash₁
(λ { (inl e) → ∣ zero , sym e ∣₁
; (inr sat) → map₁ (λ { (i , q) → suc i , q })
(sat→hits n (λ i → g (suc i)) m sat) })
```
逆方向は命中を充足に変えるもので、これも長さについての再帰で進む。長さ零では型 `Fin 0` の添字が存在しないので、そこの命中は空の添字型とのマッチングで反証できる。これは論理式が零で偽であることと対応する。`hits→sat` はすべての長さに対して一度に述べられているため、後者の場合の再帰呼び出しは仮定を何も引き回さずに使える。
```agda
hits→sat : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫) (m : ⟪ Lset σ ⟫)
→ Hits n g (⟪ Lset σ ⟫↪ m)
→ ⟨ (DefC.ι m ∷ []) DefC.⊨ᵐ finDisj n g ⟩
hits→sat 0 g m =
rec₁ (((DefC.ι m ∷ []) DefC.⊨ᵐ finDisj zero g) .snd) (λ { (() , _) })
```
長さが後者のとき、命中は添字が `zero` であるか後者 `suc i` であるかのいずれかである切り詰められた対である。最初の場合、パスが要素を最初の定数と同一視し、論理式の左の選言肢が充足される。第二の場合、ずらした族に対する再帰呼び出しが尾部の論理和の充足を生み、それが右の選言肢になる。どちらの場合も答えは切り詰めの内部で返されるので、証明が命中のもつ添字に依存することはない。
```agda
hits→sat (suc n) g m =
rec₁ (((DefC.ι m ∷ []) DefC.⊨ᵐ finDisj (suc n) g) .snd)
(λ { (zero , q) → ∣ inl (sym q) ∣₁
; (suc i , q) →
∣ inr (hits→sat n (λ j → g (suc j)) m ∣ i , q ∣₁) ∣₁ })
```
橋の二つの方向は、恒等式 `defSet≡` が必要とする二つの包含にちょうど一致する。証明は周囲の外延性によるもので、集合のパスは一対の包含へ帰着し、像の集合には略称 `F` が使われる。残りの作業は、構造的な所属の記法と周囲の所属の記法のあいだの簿記である。
```agda
defSet≡ : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫)
→ DefC.defSet (finDisj n g) ≡ finSet n (λ i → ⟪ Lset σ ⟫↪ (g i))
defSet≡ n g = extensionality _ _ (sub₁ , sub₂)
where
F = finSet n (λ i → ⟪ Lset σ ⟫↪ (g i))
```
第一の包含は、定義可能部分集合の構造的な要素 `y` から始まる。変換 `∈∈ₛ` がそれを周囲の所属へ変え、その読み取り補題が切り詰められた定義データを与える。すなわち充足の証明書を伴う環境 `m` と、`y` を `m` の名指す要素と同一視するパス `q` である。この時点で証明すべき目標は命題 `⟨ y ∈ F ⟩` であり、これが切り詰めの除去を正当化する。
```agda
sub₁ : ⟨ DefC.defSet (finDisj n g) ⊆ F ⟩
sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = F} .fst (rec₁ ((y ∈ F) .snd)
(λ { ((m , h) , q) →
subst (λ v → ⟨ v ∈ F ⟩) q
(finSet-in n (λ i → ⟪ Lset σ ⟫↪ (g i)) (⟪ Lset σ ⟫↪ m)
```
充足の証明書は、定義可能部分集合への所属の計算規則 `defSet-mem` によって、環境 `m` での論理和の充足へ変換される。橋渡しの補題 `sat→hits` が命中を生み、`finSet-in` がその命中を、埋め込まれた要素の像への所属として読む。最後に `q` に沿った輸送が、その所属を名指された要素から `y` 自身へ移す。
```agda
(sat→hits n g m
(subst ⟨_⟩ (DefC.defSet-mem (finDisj n g) m)
∣ (m , h) , refl ∣₁))) })
(∈∈ₛ {a = y} {b = DefC.defSet (finDisj n g)} .snd y∈ₛ))
sub₂ : ⟨ F ⊆ DefC.defSet (finDisj n g) ⟩
```
逆の包含は `y ∈ F` から始まる。除去規則 `finSet-out` は、添字 `i : Fin n` とパス `q : ⟪ Lset σ ⟫↪ (g i) ≡ y` を単に与える。代表元 `g i` では、切り詰められた証人 `∣ i , refl ∣₁` が `Hits n g (⟪ Lset σ ⟫↪ (g i))` を示し、`hits→sat` がそれを有限論理和の充足へ変換する。その後 `q` に沿って輸送すれば、`y` の定義可能部分集合への所属が得られる。
```agda
sub₂ y y∈ₛ = rec₁ ((y ∈ₛ DefC.defSet (finDisj n g)) .snd)
(λ { (i , q) →
subst (λ v → ⟨ v ∈ₛ DefC.defSet (finDisj n g) ⟩) q
(∈∈ₛ {a = ⟪ Lset σ ⟫↪ (g i)} {b = DefC.defSet (finDisj n g)} .fst
(subst ⟨_⟩ (sym (DefC.defSet-mem (finDisj n g) (g i)))
```
充足は `defSet` の所属の読みを逆向きに用いて、埋め込まれた `g i` の定義可能部分集合への構造的な所属として読まれ、命中のパスに沿った輸送がそれを `y` へ移す。二つの包含を組み合わせれば、`defSet≡` は集合としてのパスでこの等式を述べる。有限論理和が切り出す部分集合は族の像であり、族に繰り返しがあっても同様である。同じ要素が複数の定数で名指されても像は変わらないからである。
```agda
(hits→sat n g (g i) ∣ i , refl ∣₁))) })
(finSet-out n (λ i → ⟪ Lset σ ⟫↪ (g i)) y
(∈∈ₛ {a = y} {b = F} .snd y∈ₛ))
finSet∈𝒟ₒ : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫)
→ ⟨ finSet n (λ i → ⟪ Lset σ ⟫↪ (g i)) ∈ 𝒟ₒ (Lset σ) ⟩
```
この節は二段階で結ばれる。第一に、`finSet∈𝒟ₒ` は今証明した論理式と等式を `𝒟ₒ-intro` に渡し、像の集合を段階の定義可能冪集合の要素として記録する。この定義可能性の証明書は切り詰められているため、保持されるデータに特定の論理式は含まれない。第二に、`finSetL` は任意の集合の族と、各要素がこの段階に属する証明から出発する。各要素に対して `∈-asFiber` が段階の提示の添字と要素へのパスを与え、`cong (finSet n) (funExt qg)` でそれらのパスに沿って像の集合を書き換えると、`defSet≡` が扱う埋め込まれた族と同一視できる。閉包の補題 `defSet→isL` が `finSet n h` の構成可能性を与える。
```agda
finSet∈𝒟ₒ n g = 𝒟ₒ-intro (Lset σ) _ ∣ finDisj n g , defSet≡ n g ∣₁
finSetL : (n : ℕ) (h : Fin n → V ℓ) → ((i : Fin n) → ⟨ h i ∈ Lset σ ⟩)
→ ⟨ isL (finSet n h) ⟩
finSetL n h hσ = defSet→isL σ oσ (finSet n h)
∣ finDisj n g , (defSet≡ n g ∙ cong (finSet n) (funExt qg)) ∣₁
```
仮定 `hσ i` は、`h i` がこの段階に属することを切り詰められた形で述べるにすぎない。階層の集合への所属は埋め込み `⟪ Lset σ ⟫↪` のファイバーの切り詰めであり、この写像は埋め込みなのでファイバーの型は命題である。したがってファイバーの型への切り詰めの除去は正当であり、`∈-asFiber` がまさにその変換を行う。ゆえに `g i` は選ばれた添字であり、その埋め込まれた元から `h i` へのパスが `qg i` である。`defSet→isL` に渡す証明書は、代表元 `g` に対する有限論理和と `defSet≡ n g` を組にし、さらに書き換え `funExt qg` を続けることで、埋め込まれた族 `finSet n (λ i → ⟪ Lset σ ⟫↪ (g i))` についての同一視を元の族 `finSet n h` へと運ぶ。
```agda
where
g : Fin n → ⟪ Lset σ ⟫
g i = ∈-asFiber {a = h i} {b = Lset σ} (hσ i) .fst
qg : (i : Fin n) → ⟪ Lset σ ⟫↪ (g i) ≡ h i
qg i = ∈-asFiber {a = h i} {b = Lset σ} (hσ i) .snd
```
## 二つの集合を一つの段階へ
`isL-directed` は、任意の二つの構成可能集合を一つの共通の順序数段階へ置く。
構成可能集合はそれぞれ固有の段階をもち、それは構成可能性の切り詰められた証明書によって単に与えられる。結論はこの二つを組み合わせる。すなわち、両方の集合を含む段階をもつ順序数 `σ` が単に存在するということである。`bound2` は与えられた二つの順序数をともに含む順序数を作り、段階の単調性が各集合をその固有の段階から上界の段階へ引き上げる。結論は切り詰められた形で述べられるので、外部に段階が示されることはない。局所的には、二つの証明書がそれぞれの名指す段階を読み取れるところまで開かれるだけである。
この定理は二つの構成可能集合を切り詰められた証明書として受け取る。`⟨ isL x ⟩` と `⟨ isL y ⟩` は、それぞれが `L` に属することを述べるだけで、段階を名指ししない。結論も同様に切り詰められているため、この二つの証明書は切り詰められた存在の主張の中へしか除去されず、外部に向かって段階が選ばれることはない。局所的には、目標の内容は `Bound` にまとめられている。すなわち順序数 `σ`、その順序数性、そして `Lset σ` への二つの所属である。
```agda
isL-directed : (x y : V ℓ) → ⟨ isL x ⟩ → ⟨ isL y ⟩
→ ∥ Σ[ σ ∶ V ℓ ] (IsOrd σ × (⟨ x ∈ Lset σ ⟩ × ⟨ y ∈ Lset σ ⟩)) ∥₁
isL-directed x y px py = rec2 squash₁ go px py
where
Bound : Type (ℓ-suc ℓ)
```
二つの切り詰めは `rec2` によって一度に除去される。その目標は切り詰め `∥ Bound ∥₁` である。実際に働く部分 `go` が受け取るのは、証明書が隠している明示的なデータ、すなわち順序数である段階 `α` と `x ∈ Lset α`、および順序数である段階 `β` と `y ∈ Lset β` である。両者を併合することは大きさの比較ではない。`bound2 α β oα oβ` は `α` と `β` の両方を含む単一の順序数上界を、その順序数性と二つの所属とともに返す。
```agda
Bound = Σ[ σ ∶ V ℓ ] (IsOrd σ × (⟨ x ∈ Lset σ ⟩ × ⟨ y ∈ Lset σ ⟩))
go : Σ[ α ∶ V ℓ ] (IsOrd α × ⟨ x ∈ Lset α ⟩)
→ Σ[ β ∶ V ℓ ] (IsOrd β × ⟨ y ∈ Lset β ⟩) → ∥ Bound ∥₁
go (α , (oα , x∈Lα)) (β , (oβ , y∈Lβ)) =
∣ bnd .fst , (bnd .snd .fst , ( Lset-mono (bnd .snd .snd .fst) x∈Lα
```
上界には `α ∈ σ₀` と `β ∈ σ₀` という所属が付いてくるので、単調性 `Lset-mono` は `x ∈ Lset α` を上界の段階 `Lset σ₀` へ引き上げる。`β` からの `y` についても同様である。組み立てた三つ組を `∣_∣₁` で包めば `go` が完成し、それとともに定理全体、すなわち任意の二つの構成可能集合が共通の順序数段階を「単に存在する」という形でもつことが示される。対のフィールドは、二つの実引数が同じ段階で見えることを必要とするので、消費するのはまさにこれである。
```agda
, Lset-mono (bnd .snd .snd .snd) y∈Lβ )) ∣₁
where bnd = bound2 α β oα oβ
```
## 継承される二つの公理
外延性と正則性はいずれも周囲の階層から制限されるが、議論は異なる。外延性では `isL-trans` により、どちらかの構成可能集合の周囲での要素を台の要素にし、台の要素について仮定した一致を適用する。周囲の外延性が基底の集合を同一視し、制限の反射が台のパスを与える。正則性は `isL-trans` を使わない。周囲の可到達性を、すでに構成可能性の証明書を持つ対へ再帰的に制限する。
`L` の内部での外延性の形はこうである。台の二つの元がすべての台の元について所属が一致するなら、それらはパスとして等しい。証明は基底の階層へ帰着する。台は集合と構成可能性の証明書の対からなり、`↾-reflects` はそのような対が第一射影で決まるという原理である。基底の集合 `a .fst` と `b .fst` の間のパスがあれば、すでにパス `a ≡ b` が得られる。したがって仕事のすべてはその基底のパスを作ることにあり、`vwise` を前提に `extensionalV` がそれを供給する。
```agda
extensionalL : {a b : S} → ((x : S) → (x ∈ˢ a) ≡ (x ∈ˢ b)) → a ≡ b
extensionalL {a} {b} h =
↾-reflects {𝒮 = 𝒮ᵥ} {M = isL} (extensionalV {a = a .fst} {b = b .fst} vwise)
where
vwise : (v : V ℓ) → (v ∈ a .fst) ≡ (v ∈ b .fst)
```
仮定 `h` が語るのは台の元、つまり構成可能な対についてだけである。これを階層の任意の `v` に拡張するために働くのが推移性である。`v ∈ a .fst` と `a` の携える証明書から、`isL-trans` が `v` 自身の構成可能性を導く。その証明書を `v` と対にすれば `v` が台の元として提示され、その元での `h` が制限された所属のパスを与える。このパスに沿って `v∈a` を輸送すれば `⟨ v ∈ b .fst ⟩` に着くので、`fwd` は普通の含意である。二つの含意を `⇔toPath` でパスにまとめれば、`extensionalV` が要求する周囲の所属の各点パスが得られる。
```agda
vwise v = ⇔toPath fwd bwd
where
fwd : ⟨ v ∈ a .fst ⟩ → ⟨ v ∈ b .fst ⟩
fwd v∈a = subst ⟨_⟩ (h (v , isL-trans v∈a (a .snd))) v∈a
bwd : ⟨ v ∈ b .fst ⟩ → ⟨ v ∈ a .fst ⟩
```
逆向きは同じ議論を `b` から読んだもので、`h` の向きが `a` から `b` へ向くことに応じて `sym` が付く。これで `extensionalL` が閉じる。正則性が求めるのは別のもの、すなわち台の所属関係の整礎性を明示的な可到達性データとして得ることである。対 `(v , p)`、つまり集合 `v` とその構成可能性の証明書に対しては、周囲の階層がすでに `v` の `Acc` を提供している。課題はそのデータを証明書を通して持ち上げることである。
```agda
bwd v∈b = subst ⟨_⟩ (sym (h (v , isL-trans v∈b (b .snd)))) v∈b
regularityL : WellFounded _∈ᵗ_
regularityL (v , p) = accL v (regularityV v) p
where
module Vmem = hPropView 𝒮ᵥ
```
この持ち上げは、周囲の可到達性データに対する再帰である。`u` が可到達なら、定義により `u` のすべての周囲の元 `y` も可到達であり、句 `rec` はまさにそれをまとめている。制限された元 `(u , q)` の元 `(y , r)` は `u` の周囲の元 `y` へ射影されるので、`accL` は `rec y y∈` について再帰し、結果に証明書 `r` を付けて返せる。制限された所属 `y ∈ᵗ (u , q)` は基底の関係 `y ∈ u` だけを継承する。証明書 `r` は前駆の台の要素 `(y , r)` に属し、所属証明の一部ではない。したがって、可到達性は基底の集合に沿って元ごとに移る。
```agda
accL : (u : V ℓ) → Acc Vmem._∈ᵗ_ u → (q : u ∈ᶜ isL) → Acc _∈ᵗ_ (u , q)
accL u (acc rec) q = acc (λ { (y , r) y∈ → accL y (rec y y∈) r })
```
## 外延性から得られる一意性
`uniqueL` は外延性から一意性を導く。固定された所属の仕様を実現する集合は一意であり、したがって、このあと残っている公理のフィールドには「単に存在する」証人だけで足りる。
議論は、実現者に台の外延性を適用するものである。同じ述語 `Q` を実現する二つの集合は、すべての台の元で同じ真理値、すなわち `Q x` を取るので、`extensionalL` が両者を同一視する。ここで必要な一意性の形は収縮性であり、収縮性は命題である。まさにこのことにより、単に存在する実現者を収縮性のデータそのものへ変えられるのである。
実現者の一意性は収縮性のデータである。すなわち中心、これは仕様を実現する任意の集合であり、および中心から任意の実現集合へのパスである。パスを生む部分は `extensionalL` である。実現する二つの集合は同じ所属の仕様を携えるので一致する。中心とパスの組み立ては、`extensionalL` に対する `setOf-unique` の適用である。第二の定理は単なる存在から出発する。仮定の切り詰めを `rec₁` で除去できるのは、その目標 `isContr (SetOf Q)` が命題だからで、返るのは同じ収縮性のデータである。以後、残りの各公理フィールドは、証人を一つ、切り詰められた形で提示するだけで証明される。
```agda
uniqueL : (Q : S → hProp (ℓ-suc ℓ)) → SetOf Q → isContr (SetOf Q)
uniqueL = setOf-unique extensionalL
mere→uniqueL : (Q : S → hProp (ℓ-suc ℓ)) → ∥ SetOf Q ∥₁ → isContr (SetOf Q)
mere→uniqueL Q = rec₁ isPropIsContr (uniqueL Q)
```
## 空集合
対象言語の偽な論理式が周囲の空集合を定義可能部分集合として切り出し、`hasEmptyL` がその構成可能性と所属をもたないという仕様をまとめる。
対象言語の偽はどの段階からも何も切り出さない。`defSet ⊥̇` の元はその添字のところで偽の証明を伴うことになるからである。したがって `defSet ⊥̇` は外延性を一つ隔てただけで空集合であり、空集合は構成可能である。その仕様は階層から来る。`L` における所属は階層における所属だからである。そして前節の一意性原理が、この証人をモデルが要求する収縮性のデータへ変える。
空集合は最初に構成される集合であり、しかも上界をまったく必要としない。実引数 `σ` は任意の段階を渡り、順序数性の仮定もない。空集合を定義する論理式はどの段階ででも読めるからである。証明書は、対象言語の偽 `⊥̇` と等式 `defSet⊥≡∅` の対であり、`𝒟ₒ-intro` が要求する切り詰められた形で与えられる。
```agda
∅∈𝒟ₒ : (σ : V ℓ) → ⟨ ∅ ∈ 𝒟ₒ (Lset σ) ⟩
∅∈𝒟ₒ σ = 𝒟ₒ-intro (Lset σ) ∅ ∣ ⊥̇ , defSet⊥≡∅ ∣₁
where
module DefC = DefOf (Lset σ)
defSet⊥≡∅ : DefC.defSet ⊥̇ ≡ ∅
```
この等式は、周囲の空集合に対する一回の外延性で、二つの包含からなる。最初の向きが実質のある方向である。定義可能部分集合の元 `y` は、`defSet` の読み取り補題により、添字 `m` と `⊥̇` の充足の証明 `h` からなる切り詰められた対として現れる。偽の充足は空のホスト型なので、`⊥*-rec h` がそのような元を一切否定する。包含が命題値の主張として述べられているため、そこへの切り詰めの除去は正当である。
```agda
defSet⊥≡∅ = extensionality (DefC.defSet ⊥̇) ∅ (sub₁ , sub₂)
where
sub₁ : ⟨ DefC.defSet ⊥̇ ⊆ ∅ ⟩
sub₁ y y∈ₛ = rec₁ ((y ∈ₛ ∅) .snd)
(λ { ((m , h) , q) → ⊥*-rec h })
```
第二の包含は空虚である。`∅-empty` は周囲の空集合の候補となる元を直接的に反証へ変える。両方向が揃えば、`defSet ⊥̇` と `∅` は集合として等しく、`∅∈𝒟ₒ` は空集合が任意の段階の定義可能部分集合であることを記録する。そこから閉包の補題が最後にもう一度だけ働き、今度は段階 `∅` そのもので、その順序数性は補題 `∅-ord` が供給する。空集合は、それ自身の一段上で構成可能なのである。
```agda
(∈∈ₛ {a = y} {b = DefC.defSet ⊥̇} .snd y∈ₛ)
sub₂ : ⟨ ∅ ⊆ DefC.defSet ⊥̇ ⟩
sub₂ y y∈ₛ = ⊥₀-rec (∅-empty y y∈ₛ)
∅∈L : ⟨ isL ∅ ⟩
∅∈L = 𝒟ₒ→isL ∅ ∅-ord ∅ (∅∈𝒟ₒ ∅)
```
パッケージ化は基底の集合に対応している。`∅ʟ` は `∅` とその構成可能性の証明書の対であり、台 `S` の元である。モデルの存在主張は、元をひとつももたない集合が一意に存在することを要求する。提示される証人は `∅ʟ` であり、仕様は階層から取られたもので、候補となる集合の基底の集合で `empty-spec` を読んだものである。一意性は `uniqueL` によって従う。これが最初のフィールドであり、次の二つの構成の型がすでにここに見えている。すなわち、上界を定め、切り出し、締めくくる、という型である。
```agda
∅ʟ : S
∅ʟ = ∅ , ∅∈L
hasEmptyL : isContr (SetOf (λ _ → ⊥))
hasEmptyL = uniqueL _ (∅ʟ , (λ x → empty-spec (x .fst)))
```
## 一つの段階内で対を作る
一つの段階の二要素について、二定数の論理和がその非順序対を定義可能部分集合として切り出す。派生する結果は、一元集合を一段階上へ、Kuratowski の順序対の符号を二段階上へ置く。
一つの段階の二つの要素の非順序対は、その段階の定義可能部分集合である。それぞれの要素はある添字の `⟪ Lset σ ⟫↪` であり、その二つの添字を名指す論理式がちょうどこの対を切り出す。確認には、階層そのものの対の公理と突き合わせて一方向ずつの外延性が要る。定義可能部分集合の元は論理和を充足するので二者のいずれかであり、逆に二者のそれぞれは論理和を充足するので元である。
この議論のどこにもモデルは現れない。述べられているのは塔そのものについての事実であり、そのように述べられる。Kuratowski 符号の順序対は非順序対を二段重ねたものなので、その項目より二段階上の段階にある。
順序数性は要求されない。後者の恒等式が要求しないのと同じ理由で、切り出しは比較ではないからである。一元集合は退化した対であり、順序対は一元集合と対の対である。
この主張は、`x` と `y` が段階 `Lset σ` に属することだけを仮定する。`σ` の順序数性は要求されない。部分集合を切り出すのに段階の比較は要らないからである。証明書は `𝒟ₒ-intro` で組み立てる。すなわち論理式 `φ` と、φ のこの段階での外延がちょうど `⁅ x , y ⁆` であることを言う等式 `defSet≡` を、定義可能性の演算子のインターフェースが期待する切り詰められた形で対にするのである。
```agda
pair∈𝒟ₒ : (σ x y : V ℓ) → ⟨ x ∈ Lset σ ⟩ → ⟨ y ∈ Lset σ ⟩
→ ⟨ ⁅ x , y ⁆ ∈ 𝒟ₒ (Lset σ) ⟩
pair∈𝒟ₒ σ x y x∈ y∈ = 𝒟ₒ-intro (Lset σ) ⁅ x , y ⁆ ∣ φ , defSet≡ ∣₁
where
module DefC = DefOf (Lset σ)
```
論理式は段階の小さな提示 `⟪ Lset σ ⟫` から定数を取る必要がある。二つの所属の証明に `∈-asFiber` を適用すると、実際の添字 `mₓ`、`mᵧ` と、パス `qₓ : ⟪ Lset σ ⟫↪ mₓ ≡ x`、`qᵧ : ⟪ Lset σ ⟫↪ mᵧ ≡ y` が得られる。提示の埋め込みのファイバーが命題なので、このデータを直接復元できる。ここでは所属の仮定を別の外側の切り詰めとして扱わない。
```agda
mₓ = ∈-asFiber {a = x} {b = Lset σ} x∈ .fst
qₓ : ⟪ Lset σ ⟫↪ mₓ ≡ x
qₓ = ∈-asFiber {a = x} {b = Lset σ} x∈ .snd
mᵧ = ∈-asFiber {a = y} {b = Lset σ} y∈ .fst
qᵧ : ⟪ Lset σ ⟫↪ mᵧ ≡ y
```
論理式は自由変数のスロットをひとつもち、「変数は定数 `mₓ` に等しい、または定数 `mᵧ` に等しい」と読む。その外延として主張されるのは `x` と `y` の非順序対である。証明は外延をこの対に直接同一視するのではない。まず外延を埋め込まれた代表元の対、つまり定数が実際に住んでいる対と同一視し、それから構成子 `⁅_,_⁆` への `cong₂` の適用によって等式全体を `qₓ` と `qᵧ` に沿って輸送する。
```agda
qᵧ = ∈-asFiber {a = y} {b = Lset σ} y∈ .snd
φ : Formula ⟪ Lset σ ⟫ 1
φ = (var zero ≐ con mₓ) ∨̇ (var zero ≐ con mᵧ)
defSet≡ : DefC.defSet φ ≡ ⁅ x , y ⁆
defSet≡ =
```
同一視の前半は一回の外延性で、定義可能部分集合から埋め込まれた代表元の対への向きであり、二つの包含に分かれる。ここで示す向きが言うのは、φ を充足するものはすべて名指された二つの要素のいずれかである、ということである。
```agda
extensionality (DefC.defSet φ) ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆
(sub₁ , sub₂)
∙ cong₂ ⁅_,_⁆ qₓ qᵧ
where
sub₁ : ⟨ DefC.defSet φ ⊆ ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆ ⟩
```
定義可能部分集合の元 `w` は、読み取り補題によって、添字 `m` と「`m` を名指す環境での φ の充足の証明」からなる切り詰められた対として現れる。等式の論理和の充足が記録するのは、`m` の名指す要素が二つの定数のいずれかに等しいこと、単にそれだけである。この切り詰められた論理和は、階層の対の特徴づけが右から左の向きで必要とする仮定にちょうど一致するので、`pairing-ax` は埋め込まれた要素 `⟪ Lset σ ⟫↪ m` を埋め込まれた代表元の対の中に置く。そのうえで、`w` を埋め込まれた添字と同一視するパス `q` に沿った輸送が包含を仕上げる。
```agda
sub₁ w w∈ₛ = rec₁ ((w ∈ₛ ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆) .snd)
(λ { ((m , h) , q) →
subst (λ v → ⟨ v ∈ₛ ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆ ⟩) q
(pairing-ax (⟪ Lset σ ⟫↪ mₓ) (⟪ Lset σ ⟫↪ mᵧ) (⟪ Lset σ ⟫↪ m) .snd
(subst ⟨_⟩ (DefC.defSet-mem φ m) ∣ (m , h) , refl ∣₁)) })
```
逆の包含は、階層の対の特徴づけをもう一方の向きで読む。埋め込まれた代表元の対の元 `w` は、二つの項のいずれかに単に等しいことが分かる。二つの分岐はそれぞれ、対応する代表元を同じ補助補題に渡す。`w` がどちらの代表元に等しいかが分かれば、`w` がその代表元の定数のところで φ を充足し、したがって定義可能部分集合の元であることを示せる。
```agda
(∈∈ₛ {a = w} {b = DefC.defSet φ} .snd w∈ₛ)
sub₂ : ⟨ ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆ ⊆ DefC.defSet φ ⟩
sub₂ w w∈ₛ = rec₁ ((w ∈ₛ DefC.defSet φ) .snd)
(λ { (inl p) → memOf mₓ ∣ inl refl ∣₁ p
; (inr p) → memOf mᵧ ∣ inr refl ∣₁ p })
```
補助補題 `memOf` は、代表元 `mᵢ`、`mᵢ` を名指す定数のところでの φ の充足の証明、そして `w` を `mᵢ` の埋め込まれた要素と同一視するパスを受け取る。`defSet` の所属の読みは、定数のところでの充足を、埋め込まれた要素の定義可能部分集合への所属に変える。パスに沿った輸送 (向きは `sym p`) がその所属を `w` へ移す。両方の包含が証明されれば、外延性が埋め込まれた代表元の対との等式を与え、つづく構成子 `⁅_,_⁆` への `cong₂` の適用の一歩が、パス `qₓ` と `qᵧ` に沿ってその対を `⁅ x , y ⁆` へ書き換える。
```agda
(pairing-ax (⟪ Lset σ ⟫↪ mₓ) (⟪ Lset σ ⟫↪ mᵧ) w .fst w∈ₛ)
where
memOf : (mᵢ : ⟪ Lset σ ⟫) → ⟨ (DefC.ι mᵢ ∷ []) DefC.⊨ᵐ φ ⟩
→ w ≡ ⟪ Lset σ ⟫↪ mᵢ → ⟨ w ∈ₛ DefC.defSet φ ⟩
memOf mᵢ sat p = subst (λ v → ⟨ v ∈ₛ DefC.defSet φ ⟩) (sym p)
```
最初の派生結果は、定義可能性の主張を段階への所属に変えるものである。この章の前の方で証明した後者の恒等式によれば `Lset (sucV σ)` はちょうど `𝒟ₒ (Lset σ)` なので、その恒等式に沿って (向きは `sym`)`pair∈𝒟ₒ` の結論を輸送すれば `⟨ ⁅ x , y ⁆ ∈ Lset (sucV σ) ⟩` が得られる。すなわち、一つの段階の二つの要素の非順序対は、ここで示された次段階を上界としてもつ。
```agda
(∈∈ₛ {a = ⟪ Lset σ ⟫↪ mᵢ} {b = DefC.defSet φ} .fst
(subst ⟨_⟩ (sym (DefC.defSet-mem φ mᵢ)) sat))
pair∈Lset-suc : (σ x y : V ℓ) → ⟨ x ∈ Lset σ ⟩ → ⟨ y ∈ Lset σ ⟩
→ ⟨ ⁅ x , y ⁆ ∈ Lset (sucV σ) ⟩
pair∈Lset-suc σ x y x∈ y∈ =
```
一元集合は退化した場合である。対の配置を `x` に二度適用すれば、次の段階に対 `⁅ x , x ⁆` が得られ、`⁅ x , x ⁆` を `⁅ x ⁆s` と同一視する階層の `pair-singleton` がその所属を一元集合 `⁅ x ⁆s` へ輸送する。
```agda
subst (λ w → ⟨ ⁅ x , y ⁆ ∈ w ⟩) (sym (Lset-suc σ)) (pair∈𝒟ₒ σ x y x∈ y∈)
sgl∈Lset-suc : (σ x : V ℓ) → ⟨ x ∈ Lset σ ⟩ → ⟨ ⁅ x ⁆s ∈ Lset (sucV σ) ⟩
sgl∈Lset-suc σ x x∈ = subst (λ w → ⟨ w ∈ Lset (sucV σ) ⟩) (pair-singleton x)
(pair∈Lset-suc σ x x x∈ x∈)
pr∈Lset-suc : (σ x y : V ℓ) → ⟨ x ∈ Lset σ ⟩ → ⟨ y ∈ Lset σ ⟩
```
順序対の符号 `pr x y` は、一元集合 `⁅ x ⁆s` と非順序対 `⁅ x , y ⁆` を二つの項にもつ対である。二つの項はいずれも `Lset (sucV σ)` にあり、第一は一元集合の結果から、第二は対の結果から従うので、外側の非順序対はさらに一段階上の段階に置ける。すなわち `pr x y` は `Lset (sucV (sucV σ))` にある。Kuratowski 符号は一つの非順序対を別の非順序対の内側に入れ子にするので、対の閉包を二回使うことで順序対符号の二後者段階という上界が得られるが、そこで初めて現れるとは主張していない。
```agda
→ ⟨ pr x y ∈ Lset (sucV (sucV σ)) ⟩
pr∈Lset-suc σ x y x∈ y∈ = pair∈Lset-suc (sucV σ) ⁅ x ⁆s ⁅ x , y ⁆
(sgl∈Lset-suc σ x x∈) (pair∈Lset-suc σ x y x∈ y∈)
```
## 対の公理
`hasPairL` はまず任意の二つの構成可能集合を共通段階へ入れ、次に有界な対の構成と一意性原理を適用する。
この公理の証人は、二つの実引数の共通の順序数段階における非順序対であり、その構成可能性は前節の補題が示す。仕様は、非順序対に対する階層そのものの分類を基底の集合で読んだものである。一意性はその後、外延性から来る。
対のフィールドは二つの実引数について述べられる。述語 `Q x` は、要素 `x` が `a` または `b` に等しいことを、モデルの真理値で解釈した論理和として表す。集合がこのフィールドを実現するとは、その要素がちょうど `Q` を満たすことである。構成 `mkPair` は、両方の実引数の基底集合を含む共通の順序数段階を仮定し、上界の段階がまさにそれを供給する。
```agda
module PairOf (a b : S) where
```
```agda
Q : S → hProp (ℓ-suc ℓ)
Q x = (x ≈ˢ a) ⊔ (x ≈ˢ b)
mkPair : (σ : V ℓ) → IsOrd σ → ⟨ a .fst ∈ Lset σ ⟩ → ⟨ b .fst ∈ Lset σ ⟩
→ SetOf Q
```
証人は基底の集合の周囲の非順序対であり、その構成可能性の証明書とともにまとめられる。証明書は有界な構成から来る。`Lset σ` の二つの要素の対はそこの定義可能部分集合であり、補題 `𝒟ₒ→isL` が順序数段階の定義可能部分集合を `L` へ引き上げる。仕様は、非順序対に対する階層そのものの分類 `pair-spec` を基底の集合で読んだものである。制限された台での所属は周囲の所属であるから、モデルによるこのフィールドの読みは階層の分類と一致する。
```agda
mkPair σ oσ fa∈ fb∈ = pairElt , (λ z → pair-spec (a .fst) (b .fst) (z .fst))
where
pairElt : S
pairElt = ⁅ a .fst , b .fst ⁆
, 𝒟ₒ→isL σ oσ ⁅ a .fst , b .fst ⁆ (pair∈𝒟ₒ σ (a .fst) (b .fst) fa∈ fb∈)
```
この構成はまだフィールドではない。段階が必要であるが、手もとにあるのはその単なる存在だけである。`build` は `rec₁` で `isL-directed` の切り詰めを除去する。その目標 `∥ SetOf Q ∥₁` 自身が切り詰められているので、`a` と `b` の二つの構成可能性の証明書を、共通段階と二つの所属が読み取れるところまで開けばよく、そこで `mkPair` が対を構成する。外部に向かって段階が選ばれることはない。
```agda
build : ∥ SetOf Q ∥₁
build = rec₁ squash₁
(λ { (σ , (oσ , (fa∈ , fb∈))) → ∣ mkPair σ oσ fa∈ fb∈ ∣₁ })
(isL-directed (a .fst) (b .fst) (a .snd) (b .snd))
```
```agda
hasPairL : (a b : S) → isContr (SetOf (λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b)))
```
フィールド `hasPairL` が要求するのは、実現者の型の可縮性、すなわち標準的な実現者と、中心から任意の実現者へのパスである。切り詰められた共通段階の上界は、切り詰められた存在 `∥ SetOf Q ∥₁` の中へだけ除去され、その内部で `mkPair` が段階と二つの所属証明から実現者を構成する。つぎに `mere→uniqueL` は `uniqueL` と外延性を用い、単なる存在と一意性から明示的な可縮中心を得る。したがって共通段階を恣意的に選ぶ必要はないが、最終結果には `isContr` が要求する明確な標準的実現者が含まれる。
```agda
hasPairL a b = mere→uniqueL (PairOf.Q a b) (PairOf.build a b)
```
## 和集合の公理
和集合には上界の探索が要らない。実引数を含む一つの段階で足りる。段階 `Lset σ` は推移的なので、`a .fst` の要素の各要素もやはり段階にあるからである。そこで有界存在の論理式、「実引数のある要素が自分を要素にもつ」が、周囲の和集合 `⋃ (a .fst)` をちょうど切り出す。
外延的な等式は二つの包含で証明される。一つの向きは論理式の充足を読む。`y` を要素にもつ証人 `v` は、階層の和集合の分類が求める入力にちょうど一致する。もう一つの向きは和集合の分類から始まり、途中の要素 `v` をまず段階へ引き込まねばならない。これこそ段階の推移性が二度適用されて果たす役目である。最後の仕様は二つの量化子を比べる。構成可能な条件は台の証人の上だけで量化し、階層の和集合の法則はすべての `V` の上で量化するが、`isL-trans` が両方向でこの二つの範囲を同一視する。和集合が整ったとき、本章は五つの公理、すなわち外延性、正則性、空集合、対、和集合を証明し終えている。
所属の条件 `Q` は、モデルの真理値の内部での添字つき論理和である。`a` の要素であるある `y` について `x` が `y` の要素であるとき、`x` はこの和集合を実現する。構成 `mkUnion` が仮定するのは一つだけ、ある順序数段階 `σ` が `a` の基底の集合を含むことである。収容すべき第二の引数はないので、対の場合と違って上界順序数は不要であり、`a` がすでにもつ段階そのもので足りる。
```agda
module UnionOf (a : S) where
```
```agda
Q : S → hProp (ℓ-suc ℓ)
Q x = ∃[ y ∶ S ] (y ∈ˢ a) ⊓ (x ∈ˢ y)
mkUnion : (σ : V ℓ) → IsOrd σ → ⟨ a .fst ∈ Lset σ ⟩ → SetOf Q
mkUnion σ oσ fa∈ = unionElt , spec
```
段階 `Lset σ` では、論理式はその小さな提示の上を動く。`Lset-layer σ` と `layer-trans` から得られる推移性は、段階の要素の要素が再びその段階に属することを述べる。与えられた `a .fst` の段階への所属に `∈-asFiber` を適用すると、代表元 `mₐ` とパス `qₐ : ⟪ Lset σ ⟫↪ mₐ ≡ a .fst` が得られる。上と同様、これは外側の切り詰めを消去した結果ではなく、直接得られるファイバーのデータである。
```agda
where
module DefA = DefOf (Lset σ)
Atrans = layer-trans (Lset-layer σ)
mₐ = ∈-asFiber {a = a .fst} {b = Lset σ} fa∈ .fst
qₐ : ⟪ Lset σ ⟫↪ mₐ ≡ a .fst
```
論理式は自由変数のスロットを一つもつ有界存在である。変数は定数 `mₐ` の要素、すなわち段階の内部で提示された `a` の要素の上を渡り、母式は束縛変数が外側の変数を要素にもつと述べる。束縛変数が量化子の本体の中で第一のスロットを占めるため、外側の変数は後者のスロットに置かれる。外延として主張されるのは周囲の和集合 `⋃ (a .fst)` であり、等式 `defSet≡` は一回の外延性で、二つの包含に分かれる。
```agda
qₐ = ∈-asFiber {a = a .fst} {b = Lset σ} fa∈ .snd
φ : Formula ⟪ Lset σ ⟫ 1
φ = ∃̇∈ (con mₐ) (var (suc zero) ∈̇ var zero)
defSet≡ : DefA.defSet φ ≡ ⋃ (a .fst)
defSet≡ = extensionality (DefA.defSet φ) (⋃ (a .fst)) (sub₁ , sub₂)
```
最初の包含は、論理式を充足するものはすべて周囲の和集合にある、と言う。定義可能部分集合の元 `y` は、`defSet` の読み取り補題によって、添字 `m` と充足の証明からなる切り詰められた対として、`y` を埋め込まれた要素 `⟪ Lset σ ⟫↪ m` と同一視するパス `q` とともに届く。充足の仮定は要素を添字で名指すので、それを消費できるのは埋め込まれた要素に対してだけである。`q` に沿った輸送が目標を `y` からその要素へ移し、命題 `y ∈ₛ ⋃ (a .fst)` への消去がこの一歩全体を正当に保つ。
```agda
where
sub₁ : ⟨ DefA.defSet φ ⊆ ⋃ (a .fst) ⟩
sub₁ y y∈ₛ = rec₁ ((y ∈ₛ ⋃ (a .fst)) .snd)
(λ { ((m , h) , q) →
subst (λ w → ⟨ w ∈ₛ ⋃ (a .fst) ⟩) q
```
有界存在の充足の証明は、範囲からの証人 `v` を、母式の二つの所属とともに単に与える。すなわち `v .fst` が埋め込まれた `mₐ` の要素であり、埋め込まれた `m` が `v .fst` の要素であることである。この二つこそ、階層の和集合の分類が導入の向きで消費する入力である。`⟪ Lset σ ⟫↪ m` を `⋃ (a .fst)` の中に置くには、それを要素にもつ `a .fst` の要素を一つ示せば足りる。
```agda
(rec₁ ((⟪ Lset σ ⟫↪ m ∈ₛ ⋃ (a .fst)) .snd)
(λ { (v , (fstv∈mₐ , m∈fstv)) →
union-ax (a .fst) (⟪ Lset σ ⟫↪ m) .snd
∣ v .fst
, ( ∈∈ₛ {a = v .fst} {b = a .fst} .fst
```
しかし母式の二つの所属は制限された提示の言葉で語っており、周囲の所属へ変えねばならない。変換は `∈∈ₛ` が行い、すでに手もとのパス `qₐ` が範囲を埋め込まれた `mₐ` から `a .fst` へ書き換えるので、証人 `v .fst` は `a .fst` の要素として提示される。第二の項はそのまま使える。それは埋め込まれた `m` の `v .fst` への所属としてすでに成っているからである。両方の所属が周囲の形になれば和集合の分類が適用され、最初の包含が閉じる。
```agda
(subst (λ w → ⟨ v .fst ∈ w ⟩) qₐ fstv∈mₐ)
, ∈∈ₛ {a = ⟪ Lset σ ⟫↪ m} {b = v .fst} .fst m∈fstv ) ∣₁ })
(subst ⟨_⟩ (DefA.defSet-mem φ m) ∣ (m , h) , refl ∣₁)) })
(∈∈ₛ {a = y} {b = DefA.defSet φ} .snd y∈ₛ)
sub₂ : ⟨ ⋃ (a .fst) ⊆ DefA.defSet φ ⟩
```
逆の包含は、同じ分類のもう一方の向きを読む。周囲の和集合への `y` の所属とは、単に、`a .fst` のある要素 `v` が `y` を要素にもつことである。補助補題 `member` は、この特定の `v` に対して `y` を定義可能部分集合の中に示さねばならない。ここで段階の仮定が働く。これまでのところ、途中の `v` が段階で見えることを保証するものは何もないからである。
```agda
sub₂ y y∈ₛ = rec₁ ((y ∈ₛ DefA.defSet φ) .snd)
(λ { (v , (v∈ₛfa , y∈ₛv)) → member v v∈ₛfa y∈ₛv })
(union-ax (a .fst) y .fst y∈ₛ)
where
member : (v : V ℓ) → ⟨ v ∈ₛ a .fst ⟩ → ⟨ y ∈ₛ v ⟩
```
補助補題はまず `y` を段階の代表元 `m'` と、その同一視のパス `q'` に変換し、`defSet` の所属の読みを逆向きに用いる。`m'` を名指す定数のところでの φ の充足は埋め込まれた `m'` の所属となり、`q'` に沿った輸送がその所属を `y` へ移す。残るは充足の証明 `sat` で、これは二つの所属 `v ∈ₛ (λ p → p .fst) a` と `y ∈ₛ v` から組み立てられる。`Atrans` を通して段階の推移性を適用すれば、まず `v` が `Lset σ` にあり、ついで `y` もそうであることが証明され、二つの項はパス `sym qₐ` と `sym q'` に沿って埋め込まれた提示へ輸送される。
```agda
→ ⟨ y ∈ₛ DefA.defSet φ ⟩
member v v∈ₛfa y∈ₛv =
subst (λ w → ⟨ w ∈ₛ DefA.defSet φ ⟩) q'
(∈∈ₛ {a = ⟪ Lset σ ⟫↪ m'} {b = DefA.defSet φ} .fst
(subst ⟨_⟩ (sym (DefA.defSet-mem φ m')) sat))
```
ここが段階の仮定が働く場所であり、対の構成には要らなかった一手である。まず `∈∈ₛ` によって二つの周囲の所属を構造的な形から読み出す。`v` は `a` の基底の集合の要素、`y` は `v` の要素である。次に段階の推移性を二度適用する。`a .fst` が `Lset σ` にあり段階が推移的である以上、その要素 `v` も `Lset σ` にあり、`v` への `y` の所属に同じ推論を適用すれば、`y` 自身も段階の要素であると証明される。こうして `a` の要素の要素が段階へ引き込まれ、論理式の量化子がそれを見えるようにするのはまさにこのためである。
```agda
where
v∈fa = ∈∈ₛ {a = v} {b = a .fst} .snd v∈ₛfa
y∈v = ∈∈ₛ {a = y} {b = v} .snd y∈ₛv
v∈A = Atrans {x = a .fst} {y = v} v∈fa fa∈
y∈A = Atrans {x = v} {y = y} y∈v v∈A
```
`y` が段階にあるという証明書が手に入れば、ファイバー変換 `∈-asFiber` が代表元 `m'` と、埋め込まれた要素から `y` への同一視のパス `q'` を供給する。次に、この代表元のところでの φ の充足の証明を切り詰めの内部で組み立てる。証人は段階への所属 `v∈A` を伴う `v` の対であり、母式の二つの項は埋め込まれた提示へ輸送される。`v` は `sym qₐ` に沿って埋め込まれた `mₐ` へ、埋め込まれた `m'` は `sym q'` に沿って `v` へ入る。これが有界存在が要求するデータにちょうど一致する。
```agda
fib = ∈-asFiber {a = y} {b = Lset σ} y∈A
m' = fib .fst
q' = fib .snd
sat : ⟨ (DefA.ι m' ∷ []) DefA.⊨ᵐ φ ⟩
sat = ∣ (v , v∈A)
```
二つの包含は等式 `defSet≡` に組み上げられ、認識の原理 `𝒟ₒ-intro` が論理式と等式を `⋃ (a .fst)` の `𝒟ₒ (Lset σ)` への所属に変える。閉包の補題 `𝒟ₒ→isL` を一度適用すれば構成は完成である。`σ` が順序数である以上、`Lset σ` の定義可能部分集合は構成可能であり、`⋃ (a .fst)` は証明書とともに台の要素として `L` に入る。次のブロックはこの包みを分類する。
```agda
, ( subst (λ w → ⟨ v ∈ w ⟩) (sym qₐ) v∈fa
, subst (λ w → ⟨ w ∈ v ⟩) (sym q') y∈v ) ∣₁
union∈𝒟ₒ : ⟨ ⋃ (a .fst) ∈ 𝒟ₒ (Lset σ) ⟩
union∈𝒟ₒ = 𝒟ₒ-intro (Lset σ) (⋃ (a .fst)) ∣ φ , defSet≡ ∣₁
unionElt : S
```
仕様は真理値のパスであり、二つの部品の合成である。階層そのものの和集合の法則 `union-spec` は、周囲の和集合への `z .fst` の所属を、階層全体を渡る添字つき論理和として分類する。すなわち `a .fst` のある `y` が `z .fst` を要素にもつ、というものである。残る仕事は、この周囲の添字つき論理和を `Q z` に変えることである。`Q z` は台 `S` の上、つまり構成可能な証人だけの上で量化する。二つの量化の範囲は異なっており、次のブロックの橋渡しがこの二つの切り詰められた論理和を同一視する。
```agda
unionElt = ⋃ (a .fst) , 𝒟ₒ→isL σ oσ (⋃ (a .fst)) union∈𝒟ₒ
spec : (z : S) → (z ∈ˢ unionElt) ≡ Q z
spec z = union-spec (a .fst) (z .fst) ∙ bridge
where
bridge : (∃[ y ∶ (V ℓ) ] (y ∈ a .fst) ⊓ (z .fst ∈ y)) ≡ Q z
```
橋渡しは、二つの切り詰められた論理和の間の一対の写像であり、`⇔toPath` によってパスに結ばれる。前向きには、二つの所属を伴う周囲の証人 `y` が構成可能性の証明書を得る。根拠はまさに `y` が `a .fst` の要素であることで、`a` 自身の証明書 `a .snd` が手もとにある。クラスの推移性、ここでは「`y` の所属」と「`a` の証明書」に適用される `isL-trans` が `y` 自身を証明するので、証人は所属を保ったまま台の要素として提示できる。後向きには、台の証人はその基底の集合へ射影され、証明書は捨てられるが所属は保たれる。どちらの向きも真理値の作られ方を覗かず、抽象的な Ω の値に作用する。橋が整えば `spec` は合成パスとなり、モデルの和集合のフィールドがここに供給される。
```agda
bridge = ⇔toPath
(map₁ (λ { (y , py) →
(y , isL-trans {x = a .fst} {y = y} (py .fst) (a .snd)) , py }))
(map₁ (λ { (y , py) → y .fst , py }))
build : ∥ SetOf Q ∥₁
```
組み立ては対のフィールドを写したものである。実引数自身の証明書 `a .snd` は切り詰められており、`build` はそれを `rec₁` で除去して、実現する集合の単なる存在へする。証明書の名指す段階で `mkUnion` が走り、証人が生まれる。フィールドそのものは、その後の一意性原理の一度の適用、`mere→uniqueL` である。単に存在する証人が収縮性のデータへ変わり、これはモデルの record のすべての存在フィールドが取る形である。
```agda
build = rec₁ squash₁ (λ { (σ , (oσ , fa∈)) → ∣ mkUnion σ oσ fa∈ ∣₁ }) (a .snd)
```
```agda
hasUnionL : (a : S) → isContr (SetOf (λ x → ∃[ y ∶ S ] (y ∈ˢ a) ⊓ (x ∈ˢ y)))
hasUnionL a = mere→uniqueL (UnionOf.Q a) (UnionOf.build a)
```
## まとめ
本章は構成可能宇宙のために五つの公理を供給する。外延性公理と正則性公理は継承されたものである。外延性は推移性を用いて周囲の要素を扱い、正則性は周囲の可到達性を直接制限する。そして台の内部で外延性が手に入れば、残りの各公理は証人を一つ提示するだけに帰着する。固定された所属条件を実現する集合は一意だからである。空集合、対、和集合は構成されたものである。いずれも一つの論理式で単一の段階から切り出され、二つの実引数が合流しなければならないところでは、必要な段階を上界順序数が供給する。和集合の仕様は、推移性がもう一度働く場面も示している。周囲の和集合への所属の証人が構成可能性の証明書を得るのはまさに `isL-trans` によってであり、これがモデルの制限された証人と周囲の和集合のすべての証人を同一視するのである。公理と並んで、本章は塔そのものについての配置の事実も記録する。`pair∈Lset-suc` は一つの段階の二つの要素の非順序対を次の段階へ入れ、`sgl∈Lset-suc` は一元集合を、`pr∈Lset-suc` は順序対を二段階上へ置く。順序対で書かれたものが段階に配置できるのは、まさにこのためである。