この章を読むか、対話型目次と依存グラフで別のルートを選べます。

崩壊は累積階層の集合レベルの台に着地する。したがって出力は A の点ではなく集合である。この台を以下では SV.S と書く。これは h-集合、すなわち任意の二要素の間の等式型が命題となる型である。所属関係 _∈ˢ_ は各所属の主張を hProp、つまり根底の型 ⟨ b ∈ˢ a ⟩ とその型が命題である証明の対として与える。したがって所属と推移性は階層本来の関係で直接述べられる。

module L.Mostowski {ℓ : Level} where

関係だけでどれほどの集合論的構造が得られるのか。Type ℓ 値の推移的な整礎関係 _≺_ を持つ小さな型 A を固定する。Mostowski の答えは、関係だけから再帰によって関数 col : A → SV.S が定まり、

col p = { col r | r ≺ p }

つまり各点がその前者の崩壊値からなる集合へ写される、というものである。計算法則が各値への所属を特徴付け、関係の推移性によって各崩壊値はここでいう順序数、すなわち自身が推移的で各要素も推移的な集合になる。

有限の例で仕組みを見る。三点 s、r、p が s ≺ r、r ≺ p、および推移性から従う s ≺ p だけを関係として持つとすると、再帰は col s の要素を何も強制せず、col r = { col s }、col p = { col s, col r } となる。これはまさに von Neumann の 0、1、2 の図である。再帰は点そのものを見ず、前者の錐だけを見る。

設定の三つの特徴がその後のすべてを形作る。第一に、A と各繊維 x ≺ y は Type ℓ にあるので、各 p の前者の錐は小さな型 Σ[ r ∶ A ] (r ≺ p) である。階層 V の sett 構成子はまさにこのような小さな族を SV.S の集合に変える。第二に、sett 集合への所属は構成上命題的切り詰めである。⟨ b ∈ˢ a ⟩ はあるインデックスで族の値が b に等しいことが単に存在すると述べるのであって、選ばれたインデックスが得られるとは言わない。したがって本章では、一方向には与えられたデータから所属を証明し (r ≺ p が col r ∈ˢ col p を与える)、他方向には崩壊値の等式を伴う、単に存在する前者しか得られない。第三に、後の消去の目標は集合の等式や isTransV x といった命題なので、そこへの切り詰めの消去は正当である。_≺_ に対する外延性の仮定は現れず、同じ前者の錐を持つ二点は区別されない。崩壊は正準であるが、単射であるとは主張しない。構成は整礎再帰と輸送だけを用い、ここでは古典的な原理を何も仮定しない。

構成を駆動する要素は二つである。第一は階層の像演算 sett で、小さなインデックス型 X と族 X → V ℓ からその族の値の集合を形作り、所属はあるインデックスが目標に命中するときに単に成り立つ。第二は整礎性の証明 WellFounded _≺_、すなわち A のすべての要素が ≺ に沿って到達可能であるという主張で、その帰納原理が再帰的に定義された関数を構成し、付随する計算法則が各点での振る舞いを記録する。命題的切り詰めは ∥ _ ∥₁ とその導入 ∣ _ ∣₁ を通して現れる。像への所属は設計上切り詰められているからである。順序数の目標 IsOrd、推移性 isTransV、そしてその命題性の証明 isPropIsTransV は L の構成から来ており、最後の定理がそれらを必要とするときにだけ現れる。

open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
open import Cubical.Induction.WellFounded using ( WellFounded; module WFI )

階層構造は等号と所属がレベル ℓ-suc ℓ の hProp に値を取る。一方、A と各繊維 x ≺ y は Type ℓ にあるので、各前者の錐は sett を適用できる小さな添字型である。構成に必要な大きさの事実はこれだけで、排中律は仮定しない。

module SV = hPropView 𝒮ᵥ
open SV using ( _∈ˢ_ )

以下では二つの課題を果たす。まず崩壊の二つの所属法則を示す。与えられた前者から要素を構成できる一方、要素から逆に得られるのは、崩壊値の等式を伴って単に存在する前者だけである。次にこの二法則を整礎帰納法で用い、各 p について IsOrd (col p) を証明する。明示的な入力と切り詰められた出力の非対称性は両方の課題で本質的である。

再帰を可能にするのは整礎性である。wf から得られる帰納原理によれば、A 上の族 P を定義するには、各 p で全ての前者 r ≺ p における P の値から P p を構成すれば十分である。推移性の証拠 ≺-trans は col の定義には使われず、得られた集合の推移性を後で証明するときに使われる。

module Mostowski (A : Type ℓ) (_≺_ : A → A → Type ℓ)
                 (wf : WellFounded _≺_)
                 (≺-trans : {x y z : A} → x ≺ y → y ≺ z → x ≺ z) where

module W = WFI wf using ( induction; induction-compute )

colStep : (p : A) → (∀ r → r ≺ p → SV.S) → SV.S

再帰の一段は前者の錐の像である。p と、各 r ≺ p に対してすでに col r を知る再帰呼び出し rec が与えられれば、この段は sett (Σ[ r ∶ A ] (r ≺ p)) (λ z → rec (z .fst) (z .snd)) を形作る。インデックス型は対 (r , r ≺ p) の全空間であり、族はその対を rec r へ送る。抽象的には、これがまさに章の冒頭で宣言した崩壊方程式 { col r | r ≺ p } である。段の型が任意の段関数 rec を量化している点に注目してほしい。おかげで同じデータが定義と、後述の計算法則を通した推論の両方に使える。

colStep p rec = sett (Σ[ r ∶ A ] (r ≺ p)) (λ z → rec (z .fst) (z .snd))

opaque
  col : A → SV.S
  col = W.induction {P = λ _ → SV.S} colStep

  col-eq : (p : A) → col p ≡ sett (Σ[ r ∶ A ] (r ≺ p)) (λ z → col (z .fst))

関数 col は整礎帰納法で定義される。その計算規則 col-eq は col p を前者の錐の col による像と同一視する。後の所属証明ではこの等式を使い、再帰的に定義された値と明示的な像の間を移る。明示的な像への所属には sett が与える切り詰められた逆像の分類がある。

  col-eq = W.induction-compute colStep

col-in : (p r : A) → r ≺ p → ⟨ col r ∈ˢ col p ⟩
col-in p r rp =
  subst (λ v → ⟨ col r ∈ˢ v ⟩) (sym (col-eq p)) ∣ (r , rp) , refl ∣₁

col-out : (p : A) (b : SV.S) → ⟨ b ∈ˢ col p ⟩

所属には両方向の計算法則があり、両者は有益な非対称を示す。順方向：r ≺ p が与えられれば col r は col p の要素である。証拠は対 (r , rp) と、col r がインデックス r で命中することを記録するパス refl であり、col-eq p に沿って (等式は逆向きに証明されているので sym の形で) 輸送することで、この明示的な像の要素が型 ⟨ col r ∈ˢ col p ⟩ へ移る。逆方向：任意の所属 ⟨ b ∈ˢ col p ⟩ から得られるのは、切り詰められた主張、すなわち col r ≡ b となる r ≺ p が単に存在することだけである。証明は所属を col-eq p に沿って明示的な像への所属へ輸送し、それは構成により切り詰められた原像なので、インデックスのデータを等式を伴う前者として読み替える。ここで特定の r を選ぶことは一切ない。切り詰め ∥ _ ∥₁ が、所属から分かることの正直な記録である。

        → ∥ Σ[ r ∶ A ] ((r ≺ p) × (col r ≡ b)) ∥₁
col-out p b b∈ =
  map₁ (λ z → (z .fst) .fst , (z .fst) .snd , z .snd)
    (subst (λ v → ⟨ b ∈ˢ v ⟩) (col-eq p) b∈)

col-ord : (p : A) → IsOrd (col p)

最後の定理は、すべての崩壊値が順序数であると言う。IsOrd (col p) は対に展開され、col p が推移的であることと、その各要素が推移的であることからなる。証明は p 上の整礎帰納で進み、帰納の仮定 rec が各前者 r ≺ p に対して IsOrd (col r) を供給し、目標はその二つの成分から組み上がる。仮定 ≺-trans が力を発揮するのはまさにここである。二つの節を読む前に、三点の列 s ≺ r ≺ p を思い浮かべてほしい。関係の推移性こそが、col r についての所属の事実を col p の中で再演することを可能にする。

col-ord = W.induction {P = λ p → IsOrd (col p)} ih
  where
  ih : (p : A) → (∀ r → r ≺ p → IsOrd (col r)) → IsOrd (col p)
  ih p rec = tr , mem
    where

最初の節は、col p のすべての要素が推移的であるというものである。証明は col-out p x x∈ から始まる。要素 x は、単に存在する前者 r ≺ p に対する col r であり、等式 e : col r ≡ x を伴う。帰納の仮定が isTransV (col r) を供給し、subst isTransV e がその証明を等式に沿って型 isTransV x へ輸送する。切り詰めの消去が正当なのは、目標の isTransV x が命題であり isPropIsTransV x がそれを証明するからである。証拠を取り出すのではなく、単に存在する場合分けから命題を確立しているだけである。

    mem : (x : SV.S) → ⟨ x ∈ˢ col p ⟩ → isTransV x
    mem x x∈ = rec₁ (isPropIsTransV x)
      (λ z → subst isTransV ((z .snd) .snd) (rec (z .fst) ((z .snd) .fst) .fst))
      (col-out p x x∈)
    tr : isTransV (col p)

第二の節は col p 自身の推移性を示す。y ∈ x と x ∈ col p が与えられたとき y ∈ col p を示す。まず x ∈ col p を col-out で剥がし、col r ≡ x となる r ≺ p が単に得られる。この等式が与えられた y ∈ x を ⟨ y ∈ˢ col r ⟩ へ輸送し、実行例の中間の環 r がまさにここで列の両端をつなぐ。

    tr {x} {y} y∈x x∈col = rec₁ ((y ∈ˢ col p) .snd) outer (col-out p x x∈col)
      where
      outer : Σ[ r ∶ A ] ((r ≺ p) × (col r ≡ x)) → ⟨ y ∈ˢ col p ⟩
      outer (r , rp , e) =
        rec₁ ((y ∈ˢ col p) .snd) inner

これで列が閉じる。y ∈ col r から、r で col-out を適用すると、col s ≡ y となる s ≺ r が単に得られ、その等式を e2 とする。関係の推移性が s ≺ r と r ≺ p を合成して s ≺ p を与え、col-in p s が col s を col p の要素へ引き上げる。最後に e2 に沿った subst が所属の目標の中で col s を y に置き換え、⟨ y ∈ˢ col p ⟩ が得られる。切り詰めの消去はどちらも命題 ⟨ y ∈ˢ col p ⟩ の中に着地し、議論全体が使うのは整礎再帰、輸送、そして推移性の仮定だけである。古典的な原理は本章のどこにも入らない。

          (col-out r y (subst (λ v → ⟨ y ∈ˢ v ⟩) (sym e) y∈x))
        where
        inner : Σ[ s ∶ A ] ((s ≺ r) × (col s ≡ y)) → ⟨ y ∈ˢ col p ⟩
        inner (s , sr , e2) =
          subst (λ v → ⟨ v ∈ˢ col p ⟩) e2 (col-in p s (≺-trans sr rp))

推移的な整礎関係の崩壊