累積階層

宇宙レベル ℓ を固定する。このレベルをパラメータとして保つことで、異なる宇宙を同一視せずに、必要な大きさで構成を具体化できる。

module V.Hierarchy {ℓ : Level} where

集合論の言語のモデルにはどれも、「集合」からなる台と、命題に値を持つ等号と所属関係が要る。本章はその台を構成する。累積階層 V は高階帰納型であり、土台にあるのは集合論最古の考え、すなわち集合とはその要素の集まりにほかならないというものである。この型はこの考えをそのまま形にする。すべての集合は、小さな型をインデックスとする集合の族によって表示され、各インデックスが一つの要素に対応する。ある集合の要素であるとは、その族のどれかのインデックスがその要素に命中することにほかならない。同じ要素を持つ二つの表示は同じ集合を表示する。したがって外延性は、このモデルが要求すべき公理ではなく、型の構成のされ方そのものなのである。

本章はこの台の上に構造 𝒮ᵥ を組み立て、外延性から所属関係に沿う再帰原理まで、集合論の最初の性質を証明する。構造の求めるものは、階層が本来の形で供給する。集合の間の等号はパス型であり、階層が h-集合であるため命題値になる。所属関係は階層本来の ∈ で、はじめから hProp に値を取る。本章は宇宙レベル ℓ を一度だけ固定し、全章の構成をこのレベルで述べる。

本章で最も難しい証明を支えるのは、二つの考えである。第一は命題的切り詰めである。「あるインデックスが条件を満たす」という主張は、証人を選ばない純粋な存在として保たれ、切り詰められた主張は命題へしか消去できない。第二は到達可能性である。これは整礎な関係に伴う帰納的データ Acc であり、ある要素からその要素の下降の各一歩が、それ自体到達可能な要素に着地するとき、その要素は到達可能である。この二つが噛み合うのは、階層への所属そのものが切り詰められているからである。整礎性の証明は、切り詰められた形でしか存在しないインデックスを、到達可能性の証明へ変えなければならない。到達可能性はまさに命題である。

import Cubical.Induction.WellFounded as WellFoundedInduction
open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded; isPropAcc; wf→x≮x )
open import Cubical.HITs.CumulativeHierarchy.Base

まずは階層そのものをじっくり読もう。この後の議論はすべてそれの上に立つ。構成子 sett は、小さなインデックス型と階層への族から、その族の像である集合を形作る。所属 y ∈ sett X ix は切り詰められた原像であり、ix i ≡ y となる i : X があるとき、そしてそのときにしか成り立たない。パス構成子は、要素の一致する任意の二つの sett 表示を同一視する。これは型そのものに組み込まれた外延性である。この型がここで定義されるのではなく、本章はその上に構造 𝒮ᵥ を組み立て、その構造の集合論的性質を証明する。

  using ( V; setIsSet; _∈_; elimProp )
open import Cubical.HITs.CumulativeHierarchy.Base
  using ( sett )  -- lint-agda: keep (prose references link through this import)
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; extensionality )

高階帰納型

基本となる考えは集合論で最も古いものである。集合とはその要素の集まりにほからない。この型はこの考えをデータとして実現し、注意すべき制約を二つ伴う。インデックス型は小さくなければならず、X : Type ℓ の形をする。したがって各集合は大きさ ℓ のデータから組み立てられる。また、型全体は setIsSet によって h-集合なので、表示がどう同一視されようと、結果のあいだにはそれ以上の区別できる構造は残らない。

構造

構成で問うのは、構造の record が何を要求するかである。ここでの答えは、階層がすでにそのすべてを備えている、というものである。集合からなる台としては V ℓ があり、h-集合性は追加の要件ではなく、階層がみずから証明する事実である。命題に値を持つ等号としては、h-集合の要素の間のパスが命題をなすので、パス型がそれになる。命題に値を持つ所属関係としては、階層本来の ∈ がはじめから hProp にある。新たに作るべきものは何もなく、これらのフィールドが構造 𝒮ᵥ に組み上がり、一階の言語はこの構造の上で解釈される。添字は階層を指す普通の v である。

等号のフィールドはこの選択を明示する。_≈ˢ_ は x と y を、パス型 x ≡ y と「この型が命題である」ことの証明 setIsSet x y の対へ送る。これは hProp (ℓ-suc ℓ) の要素の形そのものである。同じ h-集合性の定理は、構造の中で二つの役割を持つ。setIsSet はフィールド isSetS を与え、setIsSet x y は等号として用いるパス型が命題であることを証明する。パスそのものを変換する必要はない。h-集合に対しては、二つの要素の間のパス型はもともと命題であり、フィールドはその型を、それに伴う証明とともに記録しているだけである。

𝒮ᵥ : ZFStructureₕ (ℓ-suc ℓ)
𝒮ᵥ = record
  { S      = V ℓ
  ; isSetS = setIsSet
  ; _≈ˢ_   = λ x y → (x ≡ y) , setIsSet x y

所属関係のフィールド _∈ˢ_ は階層本来の ∈ そのものであり、各対での値ははじめから hProp (ℓ-suc ℓ) の中にある。構造の関係は命題値なので、以後の多くの議論では、命題そのものではなくその基礎型が必要になる。hPropView 𝒮ᵥ を開くと、この読み方が x ∈ᵗ y として得られる。これは所属命題の要素のなす型 ⟨ x ∈ˢ y ⟩ を表す。両者は同じ関係の二つの読み方で、∈ˢ が命題を、∈ᵗ がその基礎型を与える。後の整礎性と帰納は、この読みの上に築かれる。

  ; _∈ˢ_   = _∈_ }

open hPropView 𝒮ᵥ

証明を始める前に、階層の位置を一度見ておこう。台 V ℓ は Type (ℓ-suc ℓ) に住み、そのインデックス型より一つ上の宇宙にあり、関係の値もそれに並んで hProp (ℓ-suc ℓ) に住む。階層は小さなインデックスデータから作られた大きな型である。∈∈ₛ によって大きな所属関係と結ばれる小さな所属関係 ∈ₛ は、この後の証明にも現れる。

外延性と所属関係の整礎性

二つの集合 a と b が各点で一致すると仮定する。つまり各 x に対して、命題 x ∈ a と x ∈ b の間のパスがあるとする。すると a の任意の要素はそのパスに沿って b の要素へ輸送でき、その逆もできるので、a と b は互いを包含する。ライブラリの extensionality はまさにこの相互包含をパス a ≡ b へ変換し、subst が各点のパスに沿って所属を輸送することでそれを作る。階層の外延性はしたがって追加の仮定ではなく、その定義の帰結である。

extensionalV : {a b : V ℓ} → ((x : V ℓ) → (x ∈ a) ≡ (x ∈ b)) → a ≡ b
extensionalV {a} {b} h = extensionality a b
  ( (λ x x∈ₛa → ∈∈ₛ {a = x} {b = b} .fst
      (subst ⟨_⟩ (h x) (∈∈ₛ {a = x} {b = a} .snd x∈ₛa)))
  , (λ x x∈ₛb → ∈∈ₛ {a = x} {b = a} .fst

仮定 h は、各 x に対して命題 x ∈ a と x ∈ b の間のパスを与える。目標はパス a ≡ b である。ライブラリの extensionality は小さな所属関係を期待するので、証明は橋 ∈∈ₛ を一方向に通る。入力 x∈ₛa は x の a への小所属関係である。その変換 ∈∈ₛ .snd x∈ₛa は小から大へ向かい、x ∈ a の要素を生成する。次に subst ⟨_⟩ (h x) がその要素を各点のパスに沿って輸送する。h x は二つの所属命題が x で一致することを言うので、輸送された値は x ∈ b に住む。最後に ∈∈ₛ .fst が大から小へ戻し、x の b への小所属関係が得られる。これが extensionality が入力として受け取る相互包含の前方の成分である。

      (subst ⟨_⟩ (sym (h x)) (∈∈ₛ {a = x} {b = b} .snd x∈ₛb))) )

第二の成分は、同じ橋を逆向きに通るものである。x の b への小所属関係を大へ変換し、sym (h x) に沿って逆方向へ輸送し、x の a への小所属関係へ戻す。二つの成分が合わさって相互包含が得られ、extensionality はそこから a ≡ b を作る。これが extensionalV が返すパスである。

(∈∈ₛ を通して現れる ∈ₛ はライブラリの小さな所属関係であり、「集合の小さな提示」の章で詳しく述べる。ここでは両者を結ぶ役割だけを果たす。)

本書における正則性は、所属関係が整礎であるという主張である。すなわち、台のすべての要素が ∈ᵗ の下で到達可能である、というものである。その意味は、上で導入した到達可能性のデータ Acc にある。証明は、この高階帰納型を族 λ s → Acc _∈ᵗ_ s へ消去することによって進む。任意の族への消去はいつでもできるわけではなく、ここでそれが許されるのは、各 Acc _∈ᵗ_ s が命題であり、isPropAcc s がまさにその証明を与えるからである。sett の場合、分岐は族 ix と、各インデックスについて rec i : Acc _∈ᵗ_ (ix i) を与える帰納仮定を受け取る。組み立てるべきは Acc _∈ᵗ_ (sett X ix) であり、acc の形から、これは集合の任意の要素 y に対する到達可能性を与えることにほかならない。

regularityV : WellFounded _∈ᵗ_
regularityV = elimProp (λ s → isPropAcc s)
  (λ X ix rec → acc (λ y y∈ →
    rec₁ (isPropAcc y)
           (λ { (i , p) → subst (Acc _∈ᵗ_) p (rec i) })

このような要素 y に対し、証拠 y∈ が与えるのは、p : ix i ≡ y を持つ対 (i , p) の命題的切り詰めだけである。rec₁ (isPropAcc y) がこの切り詰められた原像を消去できるのは、実際の目標 Acc _∈ᵗ_ y が命題であり、isPropAcc y がその命題性を証明するからである。分岐の中では subst (Acc _∈ᵗ_) p (rec i) が帰納仮定を ix i から y へ輸送する。証明全体として、インデックスは使われるが、大域的に一つを選ぶことはない。

           y∈))

正則性の最初の帰結は非反射性である。集合は自分自身に属しない。到達可能性の言葉で言えば、これはすぐに分かる。自分自身と整礎な関係に立つ要素は、到達可能性のデータと矛盾する。下降の各一歩が到達可能な要素に着地することを、到達可能性は要求するからである。ここでの導出は、上で証明した Acc の主張を使うものであり、Foundation のすべての古典的定式化を捉えると主張するものではない。

仮定 ⟨ A ∈ˢ A ⟩ は、所属命題の基礎型の要素であり、これは regularityV が証明された関係 ∈ᵗ そのものである。整礎な関係に対しては、どの要素も自分自身とその関係に立つことはできない。これがライブラリの非反射性の定理 wf→x≮x であり、ここでは regularityV を整礎性の入力として適用する。結果は矛盾であり、空の型 ⊥₀ がそれを示す。

∈-irrefl : (A : S) → ⟨ A ∈ˢ A ⟩ → ⊥₀
∈-irrefl A = wf→x≮x regularityV {x = A}

所属関係上の再帰

整礎性には計算上の見返りがある。整礎な関係は再帰を支えるのである。具体的には、x での値は x の各要素 y での値に依存でき、所属関係が整礎であるためこの依存は必ず停止する。対象は命題に限らず任意の依存型族 P でよく、これがこの原理を証明原理にとどまらない再帰原理にしている。これは所属関係に沿う再帰の型論的形態であり、序数で添字付けられた階層を介さずに述べられる。段階の添字に沿って再帰するのではなく、所属関係そのものに沿って再帰するのである。再帰方程式も命題としての等式で成り立つため、後の議論はそれを頼りに計算できる。

∈-induction の型は外から内へ読む。型族 P は各集合に対して任意の宇宙 Type ℓ' の型を割り当てるので、構成される値は集合とともに実際に変わりえる。ステップ関数 e は集合 x と、x の各要素 y での再帰的な値 P y を受け取る。所属関係は所属命題を Type として読む ∈ᵗ を通して現れる。そして P x を返す。この定義を正当化するのは regularityV である。ライブラリの WFI.induction をこの整礎な関係で実例化すれば、ステップ関数が全域の族へ変わる。ここで整礎性を改めて証明する必要はない。

∈-induction : ∀ {ℓ'} {P : V ℓ → Type ℓ'}
            → (∀ x → (∀ y → y ∈ᵗ x → P y) → P x)
            → ∀ x → P x
∈-induction = WellFoundedInduction.WFI.induction regularityV

∈-induction-compute : ∀ {ℓ'} {P : V ℓ → Type ℓ'}

計算法則は、各要素での再帰呼び出しを定義の内側に隠さず、等式として示す。すなわち ∈-induction e x は、ステップ関数を x と各要素 y での ∈-induction e y に適用したものに等しい、ということである。この等式は命題としての等式として述べられており、定義的に成り立つとは限らない。それを明示しておけば、簡約が定義的でない場合でも、後の証明はこの等式によって再帰的に定義された値を書き換えられる。この法則はライブラリの WFI.induction-compute であり、任意の整礎な関係に対して証明され、ここでは所属関係に実例化されている。

  (e : ∀ x → (∀ y → y ∈ᵗ x → P y) → P x) (x : V ℓ)
  → ∈-induction e x ≡ e x (λ y _ → ∈-induction e y)
∈-induction-compute = WellFoundedInduction.WFI.induction-compute regularityV

まとめ

階層 V は高階帰納型であり、集合は小さな族の像で、型全体は h-集合である。構造 𝒮ᵥ に組み上げると、等号にはパス型が、所属関係には本来の ∈ が入る。どちらも命題値である。外延性 (extensionalV) は小所属関係の橋を経て外延的なパス構成子から、所属関係の整礎性 (regularityV) は到達可能性への消去から従う。整礎性はさらに非反射性と、再帰原理 ∈-induction とその計算法則 ∈-induction-compute をもたらする。小さな所属関係 ∈ₛ とその ∈ への橋は、「集合の小さな提示」の章で扱われる。