---
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: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 基本公理

集合を作る演算を構成可能宇宙へ移すには、どうすればよいでしょうか。集合が `L` に属するとは、ある順序数段階 `Lset σ` の定義可能部分集合として表示できることです。本章では、必要な入力を含む一つの順序数段階を見つけ、その段階上で目的の集合を外延にもつ論理式を書き、周囲の階層で外延的な等式を証明する、という方法を繰り返します。

閉包補題 `defSet→isL` がこの方法を完成させます。順序数 `σ` と、外延が `x` である一変数論理式の単なる存在が与えられると、`𝒟ₒ-intro` は `x` を `Lset σ` の定義可能部分集合として認識し、`𝒟ₒ→isL` はそれを `L` に入れます。恒等式 `Lset (sucV σ) ≡ 𝒟ₒ (Lset σ)` は段階の計算を説明します。次の段階は、現在の段階の定義可能部分集合全体にちょうど一致します。`LsetS` と `𝒟ₒS` はこの二つの集合を台 `S` の要素としてまとめます。

この方法で空集合、非順序対、和集合を `L` の中に構成します。外延性では推移性により構成可能な要素についての一致を周囲のすべての要素へ広げますが、正則性では階層の可到達性の証明を再帰的に制限します。二つの入力に共通段階が必要なとき、`bound2` は元の段階を比較せずに共通の厳密上界を与えます。

設定は宇宙レベル `ℓ` を一つ固定し、そのレベルの累積階層 `V` の中で作業します。本章はすべて構成的であり、排中律もサイズ変更も選択公理も仮定しません。公理が証明される台は、`V` の集合と構成可能性の証明書 `isL` の対からなる型であり、以下の主張はすべて周囲の階層だけから立証されます。

```agda
{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude

module L.Axioms.Basic {ℓ : Level} where

open import FOL.Syntax using ( Formula; var; con; _≐_; _∈̇_; _∨̇_; ⊤̇; ⊥̇; ∃̇∈ )
```

閉包パターンの切り出しのステップは一階の言語の中で行われます。その論理式は構造の小さな添字型の上にあり、等式と所属が原子的な述語で、選言と有界存在量化が使えます。これがまさに定義可能性の演算子が消費するものです。構造から部分構造への移行について、後で効いてくる周囲の事実が二つあります。制限の中の二つの要素の間のパスは、すでに基底の集合の間のパスであり、継承される公理が利用するのはこの向きです。

```agda
open import FOL.ZFStructure using ( ↾-reflects; module hPropStructure )
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
```

持ち上げる対象となる各構成は、周囲の階層ですでに所属の法則を満たしています。空集合は元をひとつももたず、非順序対のすべての元は二つの項のいずれかであり、和集合は正確な双方向の特徴づけをもちます。これらの周囲の法則は階層で一度証明され、後で切り出される論理式を外延性で検査するときの基準となります。再証明されるのではなく、継承されるのです。計算にはさらに二つの周囲の事実が入ります。後者 `sucV σ` への所属は「`σ` の要素である」場合と「`σ` そのものである」場合に分かれること、そして一元集合が対 `⁅ x , x ⁆` と同一視されることです。順序対のクラトフスキー符号 `pr` がどの段階に置かれるかは、非順序対から計算されます。

```agda
        ; 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
```

構成可能な側は、塔とその簿記を供給します。`Lset` は集合を添字として段階を与え、`IsOrd` は順序数性の証明書、`isL` は構成可能集合のクラスで、`isL-trans` により推移的です。段階の定義可能冪集合は `𝒟ₒ` です。`𝒟ₒ-intro` が論理式と外延的な等式から定義可能部分集合を認識し、`Lset-in`、`Lset-out`、`Lset⊆𝒟ₒ`、`Lset-mono`、`Lset→isL` は段階への所属の変換、より大きな段階に沿った持ち上げ、構成可能性の証明書としての読み替えを可能にします。段階の推移性は `layer-trans` です。

```agda
        ; layer-trans; 𝒟ₒ; 𝒟ₒ-intro; Lset-in; Lset-out; Lset⊆𝒟ₒ
        ; Lset-mono; Lset→isL )
open import L.Ordinal {ℓ} using ( ∅-ord; suc-ord; bound2 )

open import Cubical.Data.FinData using ( zero; suc )
open import Cubical.Data.Sum using ( inl; inr )
```

段階を制御する順序数の事実は三つです。空集合は順序数であり、順序数の後者も順序数であり、`bound2` は二つの順序数をそれぞれ真に含む順序数を返します。対の構成では最後の結果により、もとの段階を比較したり最大のものを選んだりせず、二つの構成可能な実引数を一つの共通段階へ置きます。有限添字型はその段階内の有限像を記述し、二つの型の和はそれらを定義する論理和を表します。

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Foundations.Prelude using ( isPropIsContr )
open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
```

周囲の階層の所属は命題値であり、提示の埋め込みのファイバーも命題です。そのため `∈-asFiber` は、与えられた所属の証明を小さな提示の実際の添字と、その要素へ戻るパスに変換します。すなわち `⟨ x ∈ Lset σ ⟩` から `m : ⟪ Lset σ ⟫` と `⟪ Lset σ ⟫↪ m ≡ x` が得られ、論理式はこの要素を定数で名指せます。対応するファイバー自体が命題なのでデータを直接得られるのであり、この段階で消去すべき別の外側の切り詰めはありません。

```agda
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
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 hPropStructure 𝒮ʟ
```

意味論の側は一度だけ確定します。真理値はレベル `ℓ-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 = δ} (snd (x ∈ 𝒟ₒ (Lset σ))) δ∈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
    (PT.rec (snd (x ∈ 𝒟ₒ (Lset σ))) (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 = PT.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 = PT.map (λ { (i , q) → lower i , q })

module FinOf (σ : V ℓ) (oσ : IsOrd σ) where
  module DefC = DefOf (Lset σ)
```

論理式は等式の有限論理和です。長さ零では等しい相手がいないので論理式は偽となり、長さが後者のときは自由変数を族の最初の要素を名指す定数と比較し、残りの要素は族をずらした再帰呼び出しに委ねます。アリティは全体を通して一です。一つの自由変数のスロットが論理和全体に使われ、関数 `g` は単射である必要はなく、異なる位置が同じ要素を名指してもかまいません。

```agda
  finDisj : (n : ℕ) → (Fin n → ⟪ Lset σ ⟫) → Formula ⟪ Lset σ ⟫ 1
  finDisj zero    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 zero    g m bot = Empty.rec* bot
    sat→hits (suc n) g m = PT.rec squash₁
      (λ { (inl e)  → ∣ zero , sym e ∣₁
         ; (inr sat) → PT.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 zero g m =
      PT.rec (snd ((DefC.ι m ∷ []) DefC.⊨ᵐ finDisj zero g)) (λ { (() , _) })
```

長さが後者のとき、命中は添字が `zero` であるか後者 `suc i` であるかのいずれかである切り詰められた対です。最初の場合、パスが要素を最初の定数と同一視し、論理式の左の選言肢が充足されます。第二の場合、ずらした族に対する再帰呼び出しが尾部の論理和の充足を生み、それが右の選言肢になります。どちらの場合も答えは切り詰めの内部で返されるので、証明が命中のもつ添字に依存することはありません。

```agda
    hits→sat (suc n) g m =
      PT.rec (snd ((DefC.ι m ∷ []) DefC.⊨ᵐ finDisj (suc n) g))
        (λ { (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 (PT.rec (snd (y ∈ F))
      (λ { ((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∈ₛ = PT.rec (snd (y ∈ₛ DefC.defSet (finDisj n g)))
      (λ { (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 = PT.rec2 squash₁ go px py
  where
  Bound : Type (ℓ-suc ℓ)
```

二つの切り詰めは `PT.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` はそのような対が第一射影で決まるという原理です。基底の集合 `fst a` と `fst b` の間のパスがあれば、すでにパス `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 = fst a} {b = fst b} vwise)
  where
  vwise : (v : V ℓ) → (v ∈ fst a) ≡ (v ∈ fst b)
```

仮定 `h` が語るのは台の元、つまり構成可能な対についてだけです。これを階層の任意の `v` に拡張するために働くのが推移性です。`v ∈ fst a` と `a` の携える証明書から、`isL-trans` が `v` 自身の構成可能性を導きます。その証明書を `v` と対にすれば `v` が台の元として提示され、その元での `h` が制限された所属のパスを与えます。このパスに沿って `v∈a` を輸送すれば `⟨ v ∈ fst b ⟩` に着くので、`fwd` は普通の含意です。二つの含意を `⇔toPath` でパスにまとめれば、`extensionalV` が要求する周囲の所属の各点パスが得られます。

```agda
  vwise v = ⇔toPath fwd bwd
    where
    fwd : ⟨ v ∈ fst a ⟩ → ⟨ v ∈ fst b ⟩
    fwd v∈a = subst ⟨_⟩ (h (v , isL-trans v∈a (a .snd))) v∈a
    bwd : ⟨ v ∈ fst b ⟩ → ⟨ v ∈ fst a ⟩
```

逆向きは同じ議論を `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 = hPropStructure 𝒮ᵥ
```

この持ち上げは、周囲の可到達性データに対する再帰です。`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` の適用です。第二の定理は単なる存在から出発します。仮定の切り詰めを `PT.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 = PT.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` からなる切り詰められた対として現れます。偽の充足は空のホスト型なので、`Empty.rec* h` がそのような元を一切否定します。包含が命題値の主張として述べられているため、そこへの切り詰めの除去は正当です。

```agda
  defSet⊥≡∅ = extensionality (DefC.defSet ⊥̇) ∅ (sub₁ , sub₂)
    where
    sub₁ : ⟨ DefC.defSet ⊥̇ ⊆ ∅ ⟩
    sub₁ y y∈ₛ = PT.rec (snd (y ∈ₛ ∅))
      (λ { ((m , h) , q) → Empty.rec* h })
```

第二の包含は空虚です。`∅-empty` は周囲の空集合の候補となる元を直接的に反証へ変えます。両方向が揃えば、`defSet ⊥̇` と `∅` は集合として等しく、`∅∈𝒟ₒ` は空集合が任意の段階の定義可能部分集合であることを記録します。そこから閉包の補題が最後にもう一度だけ働き、今度は段階 `∅` そのもので、その順序数性は補題 `∅-ord` が供給します。空集合は、それ自身の一段上で構成可能なのです。

```agda
      (∈∈ₛ {a = y} {b = DefC.defSet ⊥̇} .snd y∈ₛ)
    sub₂ : ⟨ ∅ ⊆ DefC.defSet ⊥̇ ⟩
    sub₂ y y∈ₛ = Empty.rec (∅-empty y y∈ₛ)

∅∈L : ⟨ isL ∅ ⟩
∅∈L = 𝒟ₒ→isL ∅ ∅-ord ∅ (∅∈𝒟ₒ ∅)
```

パッケージ化は基底の集合に対応しています。`∅ʟ` は `∅` とその構成可能性の証明書の対であり、台 `S` の元です。モデルの存在主張は、元をひとつももたない集合が一意に存在することを要求します。提示される証人は `∅ʟ` であり、仕様は階層から取られたもので、候補となる集合の基底の集合で `empty-spec` を読んだものです。一意性は `uniqueL` によって従います。これが最初のフィールドであり、次の二つの構成の型がすでにここに見えています。すなわち、上界を定め、切り出し、締めくくる、という型です。

```agda
∅ʟ : S
∅ʟ = ∅ , ∅∈L

hasEmptyL : isContr (SetOf (λ _ → ⊥))
hasEmptyL = uniqueL _ (∅ʟ , (λ x → empty-spec (fst x)))
```

## 一つの段階内で対を作る

一つの段階の二要素について、二定数の論理和がその非順序対を定義可能部分集合として切り出します。派生する結果は、一元集合を一段階上へ、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∈ₛ = PT.rec (snd (w ∈ₛ ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆))
      (λ { ((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∈ₛ = PT.rec (snd (w ∈ₛ DefC.defSet φ))
      (λ { (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
  Q : S → hProp (ℓ-suc ℓ)
  Q x = (x ≈ˢ a) ⊔ (x ≈ˢ b)

  mkPair : (σ : V ℓ) → IsOrd σ → ⟨ fst a ∈ Lset σ ⟩ → ⟨ fst b ∈ Lset σ ⟩
         → SetOf Q
```

証人は基底の集合の周囲の非順序対であり、その構成可能性の証明書とともにまとめられます。証明書は有界な構成から来ます。`Lset σ` の二つの要素の対はそこの定義可能部分集合であり、補題 `𝒟ₒ→isL` が順序数段階の定義可能部分集合を `L` へ引き上げます。仕様は、非順序対に対する階層そのものの分類 `pair-spec` を基底の集合で読んだものです。制限された台での所属は周囲の所属ですから、モデルによるこのフィールドの読みは階層の分類と一致します。

```agda
  mkPair σ oσ fa∈ fb∈ = pairElt , (λ z → pair-spec (fst a) (fst b) (fst z))
    where
    pairElt : S
    pairElt = ⁅ fst a , fst b ⁆
            , 𝒟ₒ→isL σ oσ ⁅ fst a , fst b ⁆ (pair∈𝒟ₒ σ (fst a) (fst b) fa∈ fb∈)
```

この構成はまだフィールドではありません。段階が必要ですが、手もとにあるのはその単なる存在だけです。`build` は `PT.rec` で `isL-directed` の切り詰めを除去します。その目標 `∥ SetOf Q ∥₁` 自身が切り詰められているので、`a` と `b` の二つの構成可能性の証明書を、共通段階と二つの所属が読み取れるところまで開けばよく、そこで `mkPair` が対を構成します。外部に向かって段階が選ばれることはありません。

```agda
  build : ∥ SetOf Q ∥₁
  build = PT.rec squash₁
    (λ { (σ , (oσ , (fa∈ , fb∈))) → ∣ mkPair σ oσ fa∈ fb∈ ∣₁ })
    (isL-directed (fst a) (fst b) (a .snd) (b .snd))

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 σ` は推移的なので、`fst a` の要素の各要素もやはり段階にあるからです。そこで有界存在の論理式、「実引数のある要素が自分を要素にもつ」が、周囲の和集合 `⋃ (fst a)` をちょうど切り出します。

外延的な等式は二つの包含で証明されます。一つの向きは論理式の充足を読みます。`y` を要素にもつ証人 `v` は、階層の和集合の分類が求める入力にちょうど一致します。もう一つの向きは和集合の分類から始まり、途中の要素 `v` をまず段階へ引き込まねばなりません。これこそ段階の推移性が二度適用されて果たす役目です。最後の仕様は二つの量化子を比べます。構成可能な条件は台の証人の上だけで量化し、階層の和集合の法則はすべての `V` の上で量化しますが、`isL-trans` が両方向でこの二つの範囲を同一視します。和集合が整ったとき、本章は五つの公理、すなわち外延性、正則性、空集合、対、和集合を証明し終えています。

所属の条件 `Q` は、モデルの真理値の内部での添字つき論理和です。`a` の要素であるある `y` について `x` が `y` の要素であるとき、`x` はこの和集合を実現します。構成 `mkUnion` が仮定するのは一つだけ、ある順序数段階 `σ` が `a` の基底の集合を含むことです。収容すべき第二の引数はないので、対の場合と違って上界順序数は不要であり、`a` がすでにもつ段階そのもので足ります。

```agda
module UnionOf (a : S) where
  Q : S → hProp (ℓ-suc ℓ)
  Q x = ∃[ y ∶ S ] (y ∈ˢ a) ⊓ (x ∈ˢ y)

  mkUnion : (σ : V ℓ) → IsOrd σ → ⟨ fst a ∈ Lset σ ⟩ → SetOf Q
  mkUnion σ oσ fa∈ = unionElt , spec
```

段階 `Lset σ` では、論理式はその小さな提示の上を動きます。`Lset-layer σ` と `layer-trans` から得られる推移性は、段階の要素の要素が再びその段階に属することを述べます。与えられた `fst a` の段階への所属に `∈-asFiber` を適用すると、代表元 `mₐ` とパス `qₐ : ⟪ Lset σ ⟫↪ mₐ ≡ fst a` が得られます。上と同様、これは外側の切り詰めを消去した結果ではなく、直接得られるファイバーのデータです。

```agda
    where
    module DefA = DefOf (Lset σ)
    Atrans = layer-trans (Lset-layer σ)
    mₐ = ∈-asFiber {a = fst a} {b = Lset σ} fa∈ .fst
    qₐ : ⟪ Lset σ ⟫↪ mₐ ≡ fst a
```

論理式は自由変数のスロットを一つもつ有界存在です。変数は定数 `mₐ` の要素、すなわち段階の内部で提示された `a` の要素の上を渡り、母式は束縛変数が外側の変数を要素にもつと述べます。束縛変数が量化子の本体の中で第一のスロットを占めるため、外側の変数は後者のスロットに置かれます。外延として主張されるのは周囲の和集合 `⋃ (fst a)` であり、等式 `defSet≡` は一回の外延性で、二つの包含に分かれます。

```agda
    qₐ = ∈-asFiber {a = fst a} {b = Lset σ} fa∈ .snd

    φ : Formula ⟪ Lset σ ⟫ 1
    φ = ∃̇∈ (con mₐ) (var (suc zero) ∈̇ var zero)

    defSet≡ : DefA.defSet φ ≡ ⋃ (fst a)
    defSet≡ = extensionality (DefA.defSet φ) (⋃ (fst a)) (sub₁ , sub₂)
```

最初の包含は、論理式を充足するものはすべて周囲の和集合にある、と言います。定義可能部分集合の元 `y` は、`defSet` の読み取り補題によって、添字 `m` と充足の証明からなる切り詰められた対として、`y` を埋め込まれた要素 `⟪ Lset σ ⟫↪ m` と同一視するパス `q` とともに届きます。充足の仮定は要素を添字で名指すので、それを消費できるのは埋め込まれた要素に対してだけです。`q` に沿った輸送が目標を `y` からその要素へ移し、命題 `y ∈ₛ ⋃ (fst a)` への消去がこの一歩全体を正当に保ちます。

```agda
      where
      sub₁ : ⟨ DefA.defSet φ ⊆ ⋃ (fst a) ⟩
      sub₁ y y∈ₛ = PT.rec (snd (y ∈ₛ ⋃ (fst a)))
        (λ { ((m , h) , q) →
          subst (λ w → ⟨ w ∈ₛ ⋃ (fst a) ⟩) q
```

有界存在の充足の証明は、範囲からの証人 `v` を、母式の二つの所属とともに単に与えます。すなわち `fst v` が埋め込まれた `mₐ` の要素であり、埋め込まれた `m` が `fst v` の要素であることです。この二つこそ、階層の和集合の分類が導入の向きで消費する入力です。`⟪ Lset σ ⟫↪ m` を `⋃ (fst a)` の中に置くには、それを要素にもつ `fst a` の要素を一つ示せば足ります。

```agda
            (PT.rec (snd (⟪ Lset σ ⟫↪ m ∈ₛ ⋃ (fst a)))
              (λ { (v , (fstv∈mₐ , m∈fstv)) →
                union-ax (fst a) (⟪ Lset σ ⟫↪ m) .snd
                  ∣ fst v
                  , ( ∈∈ₛ {a = fst v} {b = fst a} .fst
```

しかし母式の二つの所属は制限された提示の言葉で語っており、周囲の所属へ変えねばなりません。変換は `∈∈ₛ` が行い、すでに手もとのパス `qₐ` が範囲を埋め込まれた `mₐ` から `fst a` へ書き換えるので、証人 `fst v` は `fst a` の要素として提示されます。第二の項はそのまま使えます。それは埋め込まれた `m` の `fst v` への所属としてすでに成っているからです。両方の所属が周囲の形になれば和集合の分類が適用され、最初の包含が閉じます。

```agda
                        (subst (λ w → ⟨ fst v ∈ w ⟩) qₐ fstv∈mₐ)
                    , ∈∈ₛ {a = ⟪ Lset σ ⟫↪ m} {b = fst v} .fst m∈fstv ) ∣₁ })
              (subst ⟨_⟩ (DefA.defSet-mem φ m) ∣ (m , h) , refl ∣₁)) })
        (∈∈ₛ {a = y} {b = DefA.defSet φ} .snd y∈ₛ)
      sub₂ : ⟨ ⋃ (fst a) ⊆ DefA.defSet φ ⟩
```

逆の包含は、同じ分類のもう一方の向きを読みます。周囲の和集合への `y` の所属とは、単に、`fst a` のある要素 `v` が `y` を要素にもつことです。補助補題 `member` は、この特定の `v` に対して `y` を定義可能部分集合の中に示さねばなりません。ここで段階の仮定が働きます。これまでのところ、途中の `v` が段階で見えることを保証するものは何もないからです。

```agda
      sub₂ y y∈ₛ = PT.rec (snd (y ∈ₛ DefA.defSet φ))
        (λ { (v , (v∈ₛfa , y∈ₛv)) → member v v∈ₛfa y∈ₛv })
        (union-ax (fst a) y .fst y∈ₛ)
        where
        member : (v : V ℓ) → ⟨ v ∈ₛ fst a ⟩ → ⟨ y ∈ₛ v ⟩
```

補助補題はまず `y` を段階の代表元 `m'` と、その同一視のパス `q'` に変換し、`defSet` の所属の読みを逆向きに用います。`m'` を名指す定数のところでの φ の充足は埋め込まれた `m'` の所属となり、`q'` に沿った輸送がその所属を `y` へ移します。残るは充足の証明 `sat` で、これは二つの所属 `v ∈ₛ 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` の要素です。次に段階の推移性を二度適用します。`fst a` が `Lset σ` にあり段階が推移的である以上、その要素 `v` も `Lset σ` にあり、`v` への `y` の所属に同じ推論を適用すれば、`y` 自身も段階の要素であると証明されます。こうして `a` の要素の要素が段階へ引き込まれ、論理式の量化子がそれを見えるようにするのはまさにこのためです。

```agda
          where
          v∈fa = ∈∈ₛ {a = v} {b = fst a} .snd v∈ₛfa
          y∈v = ∈∈ₛ {a = y} {b = v} .snd y∈ₛv
          v∈A = Atrans {x = fst a} {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` が論理式と等式を `⋃ (fst a)` の `𝒟ₒ (Lset σ)` への所属に変えます。閉包の補題 `𝒟ₒ→isL` を一度適用すれば構成は完成です。`σ` が順序数である以上、`Lset σ` の定義可能部分集合は構成可能であり、`⋃ (fst a)` は証明書とともに台の要素として `L` に入ります。次のブロックはこの包みを分類します。

```agda
                , ( subst (λ w → ⟨ v ∈ w ⟩) (sym qₐ) v∈fa
                  , subst (λ w → ⟨ w ∈ v ⟩) (sym q') y∈v ) ∣₁

    union∈𝒟ₒ : ⟨ ⋃ (fst a) ∈ 𝒟ₒ (Lset σ) ⟩
    union∈𝒟ₒ = 𝒟ₒ-intro (Lset σ) (⋃ (fst a)) ∣ φ , defSet≡ ∣₁

    unionElt : S
```

仕様は真理値のパスであり、二つの部品の合成です。階層そのものの和集合の法則 `union-spec` は、周囲の和集合への `fst z` の所属を、階層全体を渡る添字つき論理和として分類します。すなわち `fst a` のある `y` が `fst z` を要素にもつ、というものです。残る仕事は、この周囲の添字つき論理和を `Q z` に変えることです。`Q z` は台 `S` の上、つまり構成可能な証人だけの上で量化します。二つの量化の範囲は異なっており、次のブロックの橋渡しがこの二つの切り詰められた論理和を同一視します。

```agda
    unionElt = ⋃ (fst a) , 𝒟ₒ→isL σ oσ (⋃ (fst a)) union∈𝒟ₒ

    spec : (z : S) → (z ∈ˢ unionElt) ≡ Q z
    spec z = union-spec (fst a) (fst z) ∙ bridge
      where
      bridge : (∃[ y ∶ (V ℓ) ] (y ∈ fst a) ⊓ (fst z ∈ y)) ≡ Q z
```

橋渡しは、二つの切り詰められた論理和の間の一対の写像であり、`⇔toPath` によってパスに結ばれます。前向きには、二つの所属を伴う周囲の証人 `y` が構成可能性の証明書を得ます。根拠はまさに `y` が `fst a` の要素であることで、`a` 自身の証明書 `a .snd` が手もとにあります。クラスの推移性、ここでは「`y` の所属」と「`a` の証明書」に適用される `isL-trans` が `y` 自身を証明するので、証人は所属を保ったまま台の要素として提示できます。後向きには、台の証人はその基底の集合へ射影され、証明書は捨てられますが所属は保たれます。どちらの向きも真理値の作られ方を覗かず、抽象的な Ω の値に作用します。橋が整えば `spec` は合成パスとなり、モデルの和集合のフィールドがここに供給されます。

```agda
      bridge = ⇔toPath
        (PT.map (λ { (y , py) →
          (y , isL-trans {x = fst a} {y = y} (py .fst) (a .snd)) , py }))
        (PT.map (λ { (y , py) → fst y , py }))

  build : ∥ SetOf Q ∥₁
```

組み立ては対のフィールドを写したものです。実引数自身の証明書 `a .snd` は切り詰められており、`build` はそれを `PT.rec` で除去して、実現する集合の単なる存在へします。証明書の名指す段階で `mkUnion` が走り、証人が生まれます。フィールドそのものは、その後の一意性原理の一度の適用、`mere→uniqueL` です。単に存在する証人が収縮性のデータへ変わり、これはモデルの record のすべての存在フィールドが取る形です。

```agda
  build = PT.rec squash₁ (λ { (σ , (oσ , fa∈)) → ∣ mkUnion σ oσ fa∈ ∣₁ }) (a .snd)

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` は順序対を二段階上へ置きます。順序対で書かれたものが段階に配置できるのは、まさにこのためです。