最小の構成可能段階の添字

宇宙レベル ℓ を固定し、レベル ℓ-suc ℓ における排中律を仮定する。この仮定には二つの異なる数学的用途がある。ord-tri は候補の順序数を比較し、降下は「より小さい候補が存在する」という hProp を判定する。

module L.Stage {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

各構成可能集合 x は、少なくとも一つの順序数 α に対する Lset α に属する。本章は、この単なる存在から標準的な上界、すなわち x を含む最小段階の順序数添字を得る。まず、より一般的な問題を解く。順序数上の任意の hProp 値の性質 P について、整礎的な降下が最小の証人を見つけ、順序数の三分法がその一意性を示す。

降下は P を満たす任意の順序数から始まる。α において、より小さい β ∈ α も P を満たすかを問う。肯定なら β における帰納法の結果を使い、否定なら α の最小性が得られる。所属に関する帰納法により、この定義は整礎的である。「より小さい証人が存在する」という主張と最初の証人はいずれも命題的に切り捨てられているが、LeastOrd P 自身が命題なので、それぞれの切り捨てをこの完全なパッケージへ消去できる。

P σ を x ∈ Lset σ に特殊化すると stage x hx が得られる。付随する定理は、この添字が順序数で、その段階が x を含み、より小さい順序数の段階は x を含まないことを述べる。排中律を使うのは、より小さい証人の存在を判定するときと、二つの候補順序数を比較するときだけである。

所属関係は、順序数上の狭義順序と、その整礎帰納の原理の両方を与える。構成可能性からは、述語 IsOrd、段階族 Lset、そして x がある順序数添字の段階に現れるという主張 isL x を得る。したがって同じ所属関係が候補添字の間の降下を制御し、特殊化後には x の段階への所属を表す。

「より小さい証人が存在する」という主張は、命題的に切り捨てられた存在で表す。これは存在だけを記録し、選ばれた β を取り出さない。消去子 rec₁ がこの証拠を使えるのは対象が命題の場合だけであり、下の一意性の証明が LeastOrd P についてまさにそれを示す。積と依存関数型は命題性を保つので、固定した順序数添字に付随する証拠も一意になる。

性質 P は Ω、すなわち hProp の型への写像である。したがって ⟨ P α ⟩ は α における基礎の命題であり、(P α) .snd はその任意の二つの証人が一致することを示す。順序数添字の等号を最小証人のパッケージ全体の等号へ持ち上げるとき、この命題性を使う。

open hPropView 𝒮ᵥ

性質を満たす最小の順序数

順序数の性質 P に対して、LeastOrd P は P を満たす順序数 α と、それより小さい順序数は P を満たさないという証明とを組にする。この定義が扱うのは順序数の添字そのものであり、後で P σ = (x ∈ Lset σ) と特殊化して初めて、その添字は構成可能段階の添字になる。

一意性は、性質が hProp の値を取るという事実を用いる。二人の候補は三分性で比較され、どちらの厳密な向きも相手の最小性によって反駁され、残りの成分はすべて命題である。したがって順序数として等しければ、パッケージ全体としても等しいのである。

最小性は反駁として述べられる。isLeastOrd α とは、任意の集合 γ について、γ が P を満たす順序数でかつ γ ∈ α であるような状況は起こりえない、という主張である。ここで背理的な形の最小性が適切なのは、順序数の厳密な順序が所属を通して読み取られるからである。返すべき「より小さい順序数」の値はなく、導出すべきは不可能な状況だけである。パッケージ全体 LeastOrd は、順序数、その順序数性、そこでの P の証明、そしてこの最小性の条項をひとまとめにする。

module _ (P : S → hProp (ℓ-suc ℓ)) where

isLeastOrd : S → Type (ℓ-suc ℓ)
isLeastOrd α = (γ : S) → IsOrd γ → ⟨ P γ ⟩ → ⟨ γ ∈ˢ α ⟩ → ⊥₀

LeastOrd : Type (ℓ-suc ℓ)
LeastOrd = Σ[ α ∶ S ] (IsOrd α × ⟨ P α ⟩ × isLeastOrd α)

isPropLeastOrd : isProp LeastOrd
isPropLeastOrd (α , ordα , pα , leastα) (α' , ordα' , pα' , leastα') =
  Σ≡Prop propRest α≡α'
  where
  decide : (⟨ α ∈ˢ α' ⟩ ⊎ ((α ≡ α') ⊎ ⟨ α' ∈ˢ α ⟩)) → α ≡ α'

  decide (inl α∈α')       = ⊥₀-rec (leastα' α ordα pα α∈α')
  decide (inr (inl e))    = e
  decide (inr (inr α'∈α)) = ⊥₀-rec (leastα α' ordα' pα' α'∈α)
  α≡α' : α ≡ α'
  α≡α' = decide (ord-tri α ordα α' ordα')

  propRest : (β : S) → isProp (IsOrd β × ⟨ P β ⟩ × isLeastOrd β)
  propRest β = isProp× (isPropIsOrd β)
    (isProp× ((P β) .snd)
      (isPropΠ λ _ → isPropΠ λ _ → isPropΠ λ _ → isPropΠ λ _ → isProp⊥))

leastOrdBelow : (α : S) → IsOrd α → ⟨ P α ⟩ → LeastOrd
leastOrdBelow = ∈-induction step
  where
  step : (α : S) → (∀ β → ⟨ β ∈ˢ α ⟩ → IsOrd β → ⟨ P β ⟩ → LeastOrd)
       → IsOrd α → ⟨ P α ⟩ → LeastOrd

  step α IH ordα pα = decide (lem Smaller)
    where
    Smaller : hProp (ℓ-suc ℓ)
    Smaller = ∃[ β ∶ S ] ((β ∈ˢ α) ⊓ ((IsOrd β , isPropIsOrd β) ⊓ P β))
    decide : Dec ⟨ Smaller ⟩ → LeastOrd

    decide (yes ∃β) = rec₁ isPropLeastOrd
      (λ { (β , (β∈α , (ordβ , pβ))) → IH β β∈α ordβ pβ }) ∃β
    decide (no ¬∃β) = α , ordα , pα , leastProof
      where
      leastProof : isLeastOrd α

      leastProof γ ordγ pγ γ∈α = ¬∃β ∣ γ , (γ∈α , (ordγ , pγ)) ∣₁

leastOrd : ∥ (Σ[ α ∶ S ] (IsOrd α × ⟨ P α ⟩)) ∥₁ → LeastOrd
leastOrd = rec₁ isPropLeastOrd
  (λ { (α , (ordα , pα)) → leastOrdBelow α ordα pα })

段階の添字を返す関数

P σ = (x ∈ Lset σ) とすると、降下は x を含む段階 Lset α の最小の順序数添字 α を返す。関数 stage が α を選び、stage-ord はそれが順序数であることを、stage-mem と stage-earliest はその添字と対応する段階との関係を示す。

この添字は再帰的な構成そのものではなく、三つの安定した事実を通して与えられる。すなわち、順序数であり、その段階が x を含み、その性質をもつ順序数添字の中で最小である。stage を opaque とすることで、この抽象化の境界を保つ。

構成可能性の証明書 ⟨ isL x ⟩ は、leastOrd が期待する入力の形そのものである。構成可能の章でのクラスの定義により、isL x の要素とは、順序数 σ とその順序数性と所属 x ∈ˢ Lset σ の対を単に切り詰めたものである。したがって性質 λ σ → x ∈ˢ Lset σ は降下の仮定を満たし、theEarliest はこの性質に leastOrd を適用する。したがって構成可能性は、最小段階の添字を得るために必要な切り捨てられた存在の前提をちょうど与える。

theEarliest : (x : S) → ⟨ isL x ⟩ → LeastOrd (λ σ → x ∈ˢ Lset σ)
theEarliest x = leastOrd (λ σ → x ∈ˢ Lset σ)

opaque
  stage : (x : S) → ⟨ isL x ⟩ → S
  stage x p = theEarliest x p .fst

パッケージ theEarliest x p は、最小の添字と三つの証明を含む。関数 stage は添字を射影し、その再帰的構成を不透明に保つので、後の議論は順序数性、段階への所属、最小性を使う。これは構成可能集合とその証人から順序数を返す関数であり、宇宙レベルでも階数関数でもない。

opaque
  unfolding stage
  stage-ord : (x : S) (p : ⟨ isL x ⟩) → IsOrd (stage x p)
  stage-ord x p = theEarliest x p .snd .fst

  stage-mem : (x : S) (p : ⟨ isL x ⟩) → ⟨ x ∈ˢ Lset (stage x p) ⟩

三つの定理がインターフェースであり、どれもパッケージの射影である。stage-ord は選ばれた添字が順序数であることを述べ、したがって後に他の添字と比較できる。stage-mem は x を段階 Lset (stage x p) に属させる。これが降下によって示される所属の事実である。stage-earliest は最小性の条項そのものを取り戻す。より小さい順序数 σ で x ∈ˢ Lset σ となるものはない。合わせて、これらは stage x p が章の冒頭で約束された最小の添字にちょうど等しいことを、再帰を開き直すのではなく射影を通して述べている。

  stage-mem x p = theEarliest x p .snd .snd .fst

  stage-earliest : (x : S) (p : ⟨ isL x ⟩)
                 → isLeastOrd (λ σ → x ∈ˢ Lset σ) (stage x p)
  stage-earliest x p = theEarliest x p .snd .snd .snd

まとめ

leastOrd は、ある性質を満たす順序数が存在するという切り詰められた証人から、その最小の順序数を取り出す。その特殊化 stage x hx は x を含む最小の Lset α の順序数添字 α を返し、stage-ord、stage-mem、stage-earliest がその事実を正確に述べる。後の議論では、これらの順序数添字を比較または上から抑えてから、対応する構成可能段階を使える。