基本公理

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

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

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

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

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

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 は二つの順序数をそれぞれ真に含む順序数を返す。対の構成では最後の結果により、もとの段階を比較したり最大のものを選んだりせず、二つの構成可能な実引数を一つの共通段階へ置く。有限添字型はその段階内の有限像を記述し、二つの型の和はそれらを定義する論理和を表す。

open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )

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

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 が次の段階の添字を供給する。

  using ( ∅; ∅-empty; ⁅_,_⁆; ⁅_⁆s; pairing-ax; ⋃_; union-ax
        ; module InfinitySet )
open InfinitySet using ( sucV )

open hPropView 𝒮ʟ

意味論の側は一度だけ確定する。真理値はレベル ℓ-suc ℓ の命題なので、論理式の解釈は通常の型構成に落ちる。制限された構造を命題値の意味論を通して読むと、構造的な所属 ∈ˢ と、命題の基礎型を取る括弧の記法 ⟨_⟩ が得られる。実現する集合とは、台 S の要素、すなわち構成可能性の証明書を添えた集合に、その所属がどの仕様を実現するかを言う等式を添えたものである。これが型 SetOf Q である。一つの実現集合を可縮性のデータへ変える原理 setOf-unique が、本章の残りの各公理フィールドを純粋な存在の問題へ帰着させる。

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 に直接渡され、その結論も同じ形で切り詰められているため、構成可能性の証人が取り出されたり選ばれたりすることはない。

𝒟ₒ→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 を与える。順序数の段階、定義する論理式、外延的な等式、というこの証明書の形こそ、本章の残りが実例化するパターンである。

defSet→isL : (σ : V ℓ) → IsOrd σ → (x : V ℓ)
           → ∥ Σ[ φ ∶ Formula ⟪ Lset σ ⟫  ] (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 を通しての β の順序数性だけである。

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 β と、今作った証明書である。この要素を通して、段階は普通の台の点として構成可能な構造に入る。

LsetS β oβ = Lset β , isL-Lset β oβ

後者段階

塔のステップは定義可能冪集合であり、後者の添字ではステップがすべてである。Lset (sucV σ) は 𝒟ₒ (Lset σ) にちょうど一致する。この恒等式は二つの包含として証明される。一つの向きには、σ は自身の後者の要素なので、𝒟ₒ (Lset σ) は和を取られる集合の一つなので、その各要素が次の段階に入る。もう一つの向きでは、Lset (sucV σ) の要素は sucV σ のある δ に対する 𝒟ₒ (Lset δ) に属する。δ が σ の要素ならその集合はすでに Lset σ にあり、したがってその定義可能部分集合の一つである。δ が σ そのものなら包含は直ちに成る。どちらの向きも相対化を使わず、演算子の単調性も要らない。ここには σ の順序数性の仮定もない。

この恒等式があれば、定義可能冪集合の構成可能性はただちに従う。段階は一段上で構成可能であり、段階の定義可能冪集合はまさにその次の段階だからである。

二つの集合は周囲の外延性によって比較され、パスは一対の包含へ帰着する。より難しい包含には橋渡しの補題が要る。次の段階の要素 x から、ある前の段階の定義可能冪集合が x を含むことが単に成り立ち、その証人 δ は sucV σ の要素である。sucV σ の構成により、その要素は σ の要素か σ 自身のどちらかなので、この証人はまさに議論が場合分けできる情報である。

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 σ) が命題であることこそ、切り詰められた証人をここで除去できる前提である。

              → ⟨ 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 σ での段階に直接入る。二つの包含を合わせれば、パスとしての恒等式が得られる。

  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 σ) が得られる。この恒等式には σ の順序数性の仮定はない。

  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 σ)) ⟩ になる。この恒等式のほかに演算子の性質は何も使っていない。

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 σ) を指す台の要素を与える。前の節が段階そのものをまとめたのに対し、こちらは段階の定義可能部分集合の全体をまとめる。

𝒟ₒ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 の各方向は切り詰めの内部での一つの写像である。表現された集合への所属は、構成上、添字の切り詰められた存在だからである。

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 σ から切り出されるものである。

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 })

module FinOf (σ : V ℓ) (oσ : IsOrd σ) where

module DefC = DefOf (Lset σ)

finDisj : (n : ℕ) → (Fin n → ⟪ Lset σ ⟫) → Formula ⟪ Lset σ ⟫ 
finDisj     g = ⊥̇
finDisj (suc n) g =
  (var zero ≐ con (g zero)) ∨̇ finDisj n (λ i → g (suc i))

private

  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)

  sat→hits     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) })

  hits→sat : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫) (m : ⟪ Lset σ ⟫)
           → Hits n g (⟪ Lset σ ⟫↪ m)
           → ⟨ (DefC.ι m ∷ []) DefC.⊨ᵐ finDisj n g ⟩
  hits→sat  g m =
    rec₁ (((DefC.ι m ∷ []) DefC.⊨ᵐ finDisj zero g) .snd) (λ { (() , _) })

  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≡ : (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))

  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)

          (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) ⟩

  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)))

            (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∈𝒟ₒ 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)) ∣₁

  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 σ への二つの所属である。

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β は α と β の両方を含む単一の順序数上界を、その順序数性と二つの所属とともに返す。

  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 が完成し、それとともに定理全体、すなわち任意の二つの構成可能集合が共通の順序数段階を「単に存在する」という形でもつことが示される。対のフィールドは、二つの実引数が同じ段階で見えることを必要とするので、消費するのはまさにこれである。

                                  , 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 がそれを供給する。

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 が要求する周囲の所属の各点パスが得られる。

  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 を提供している。課題はそのデータを証明書を通して持ち上げることである。

    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) に属し、所属証明の一部ではない。したがって、可到達性は基底の集合に沿って元ごとに移る。

  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) が命題だからで、返るのは同じ収縮性のデータである。以後、残りの各公理フィールドは、証人を一つ、切り詰められた形で提示するだけで証明される。

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 が要求する切り詰められた形で与えられる。

∅∈𝒟ₒ : (σ : V ℓ) → ⟨ ∅ ∈ 𝒟ₒ (Lset σ) ⟩
∅∈𝒟ₒ σ = 𝒟ₒ-intro (Lset σ) ∅ ∣ ⊥̇ , defSet⊥≡∅ ∣₁
  where
  module DefC = DefOf (Lset σ)
  defSet⊥≡∅ : DefC.defSet ⊥̇ ≡ ∅

この等式は、周囲の空集合に対する一回の外延性で、二つの包含からなる。最初の向きが実質のある方向である。定義可能部分集合の元 y は、defSet の読み取り補題により、添字 m と ⊥̇ の充足の証明 h からなる切り詰められた対として現れる。偽の充足は空のホスト型なので、⊥*-rec h がそのような元を一切否定する。包含が命題値の主張として述べられているため、そこへの切り詰めの除去は正当である。

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

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

      (∈∈ₛ {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 によって従う。これが最初のフィールドであり、次の二つの構成の型がすでにここに見えている。すなわち、上界を定め、切り出し、締めくくる、という型である。

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

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

一つの段階内で対を作る

一つの段階の二要素について、二定数の論理和がその非順序対を定義可能部分集合として切り出す。派生する結果は、一元集合を一段階上へ、Kuratowski の順序対の符号を二段階上へ置く。

一つの段階の二つの要素の非順序対は、その段階の定義可能部分集合である。それぞれの要素はある添字の ⟪ Lset σ ⟫↪ であり、その二つの添字を名指す論理式がちょうどこの対を切り出す。確認には、階層そのものの対の公理と突き合わせて一方向ずつの外延性が要る。定義可能部分集合の元は論理和を充足するので二者のいずれかであり、逆に二者のそれぞれは論理和を充足するので元である。

この議論のどこにもモデルは現れない。述べられているのは塔そのものについての事実であり、そのように述べられる。Kuratowski 符号の順序対は非順序対を二段重ねたものなので、その項目より二段階上の段階にある。

順序数性は要求されない。後者の恒等式が要求しないのと同じ理由で、切り出しは比較ではないからである。一元集合は退化した対であり、順序対は一元集合と対の対である。

この主張は、x と y が段階 Lset σ に属することだけを仮定する。σ の順序数性は要求されない。部分集合を切り出すのに段階の比較は要らないからである。証明書は 𝒟ₒ-intro で組み立てる。すなわち論理式 φ と、φ のこの段階での外延がちょうど ⁅ x , y ⁆ であることを言う等式 defSet≡ を、定義可能性の演算子のインターフェースが期待する切り詰められた形で対にするのである。

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 が得られる。提示の埋め込みのファイバーが命題なので、このデータを直接復元できる。ここでは所属の仮定を別の外側の切り詰めとして扱わない。

  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ᵧ に沿って輸送する。

  qᵧ = ∈-asFiber {a = y} {b = Lset σ} y∈ .snd

  φ : Formula ⟪ Lset σ ⟫ 
  φ = (var zero ≐ con mₓ) ∨̇ (var zero ≐ con mᵧ)

  defSet≡ : DefC.defSet φ ≡ ⁅ x , y ⁆
  defSet≡ =

同一視の前半は一回の外延性で、定義可能部分集合から埋め込まれた代表元の対への向きであり、二つの包含に分かれる。ここで示す向きが言うのは、φ を充足するものはすべて名指された二つの要素のいずれかである、ということである。

      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 に沿った輸送が包含を仕上げる。

    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 がその代表元の定数のところで φ を充足し、したがって定義可能部分集合の元であることを示せる。

      (∈∈ₛ {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 ⁆ へ書き換える。

      (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 σ) ⟩ が得られる。すなわち、一つの段階の二つの要素の非順序対は、ここで示された次段階を上界としてもつ。

        (∈∈ₛ {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 へ輸送する。

  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 符号は一つの非順序対を別の非順序対の内側に入れ子にするので、対の閉包を二回使うことで順序対符号の二後者段階という上界が得られるが、そこで初めて現れるとは主張していない。

            → ⟨ 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 は、両方の実引数の基底集合を含む共通の順序数段階を仮定し、上界の段階がまさにそれを供給する。

module PairOf (a b : S) where

Q : S → hProp (ℓ-suc ℓ)
Q x = (x ≈ˢ a) ⊔ (x ≈ˢ b)

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

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 : ∥ SetOf Q ∥₁
build = rec₁ squash₁
  (λ { (σ , (oσ , (fa∈ , fb∈))) → ∣ mkPair σ oσ fa∈ fb∈ ∣₁ })
  (isL-directed (a .fst) (b .fst) (a .snd) (b .snd))

hasPairL : (a b : S) → isContr (SetOf (λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b)))

フィールド hasPairL が要求するのは、実現者の型の可縮性、すなわち標準的な実現者と、中心から任意の実現者へのパスである。切り詰められた共通段階の上界は、切り詰められた存在 ∥ SetOf Q ∥₁ の中へだけ除去され、その内部で mkPair が段階と二つの所属証明から実現者を構成する。つぎに mere→uniqueL は uniqueL と外延性を用い、単なる存在と一意性から明示的な可縮中心を得る。したがって共通段階を恣意的に選ぶ必要はないが、最終結果には isContr が要求する明確な標準的実現者が含まれる。

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 がすでにもつ段階そのもので足りる。

module UnionOf (a : S) where

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

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

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

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

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

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

          (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

                      (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 φ ⟩

    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 ∈ₛ 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))

        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

        fib = ∈-asFiber {a = y} {b = Lset σ} y∈A
        m' = fib .fst
        q' = fib .snd
        sat : ⟨ (DefA.ι m' ∷ []) DefA.⊨ᵐ φ ⟩
        sat = ∣ (v , v∈A)

              , ( 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

  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

    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 ∥₁

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