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

宇宙レベル ℓ を固定し、lem : LEM (ℓ-suc ℓ) を仮定する。この仮定は該当するレベルの各命題に判定を与え、以下の構成の明示的なパラメータとして保たれる。

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

L の内部での計数は基数によって述べるが、具体的な構成が与えるのは任意の順序数であることが少なくない。L の順序数 α に対し、本章では α に含まれる内部基数 μ と、両方向の内部単射を構成する。したがって μ はモデルの内部で α の濃度を代表する。この代表は、α の後続の中から、α が内部単射する最小の順序数を探して得られる。

レベル ℓ-suc ℓ における排中律を仮定する。この仮定は整列順序上の探索と順序数の三分法で使われる。結論の単射はすべて L の内部にあり、そのグラフは外部関数ではなく構成可能集合である。

ここでは二つの構造を使う。周囲の階層は所属関係と探索に用いる小さな表示を与え、構成可能構造は順序数、基数、内部単射の述語を与える。構成可能性は所属に沿って下方へ伝わるので、周囲の階層で見つけた要素を L の論域へ戻せる。

探索は、順序数を表示するインデックスの整列順序に基づく。この順序は、表示される要素の間の所属と一致する。包含の符号化が包含を内部単射に変え、単射の推移性が内部単射を合成する。

open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( sucV )

候補集合は後続 sucV α である。命題的切り詰めは、外部で代表を選ぶことなく適切な代表の存在を表す。和型と空型は後の三分法の議論で使われる。

周囲の集合を SV.S、構成可能集合を SL.S と書く。SL.S の要素は周囲の集合と構成可能性の証明の対である。所属の比較は第一成分について行い、InjL と IsCardinalL は完全な構成可能要素について述べる。

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

順序数 α に対し、定理は五つの性質を持つ μ が単に存在することを述べる。μ は順序数かつ内部基数で、μ ⊆ α であり、内部単射 α ↪ μ と μ ↪ α がある。切り詰めにより結論全体は命題になる。

cardOf :
    (α : SL.S) → IsOrd (α .fst)
  → ∥ Σ[ μ ∶ SL.S ]
       ( IsOrd (μ .fst) × IsCardinalL μ

最終的な証人は、代表 μ と以下で構成する五つの証明からなる。目標は切り詰められているので、成分がそろえばこの一つの依存対を入れることで定理が閉じる。

       × ((z : SV.S) → ⟨ z ∈ˢ μ .fst ⟩ → ⟨ z ∈ˢ α .fst ⟩)
       × InjL α μ × InjL μ α ) ∥₁

α に対する補助的な探索の準備は、後続の構成可能性、α 自身を名指すインデックスとその等式、表示インデックス上の整列順序 w を与える。w の順序関係は、名指された順序数の間の所属である。

cardOf α oα = ∣ μ , oμ , cardμ , μ⊆α , α↪μ , μ↪α ∣₁
  where
  module LC = LeastCardInjL α oα using ( hSucα; self; self-eq; w; w-lt )

T を、順序数 α の基礎集合の後続とする。後続も順序数なので、T の各要素は順序数であり、探索の全体で所属から得られる順序を使える。

  T : SV.S
  T = sucV (α .fst)

  oT : IsOrd T
  oT = suc-ord oα

集合 T は構成可能である。この証明が必要なのは、探索インデックスが最初に名指すのは T の周囲の要素にすぎず、構成可能性の下方閉性によって初めてその要素を SL.S の要素にできるからである。

  opaque
    hT : ⟨ isL T ⟩
    hT = LC.hSucα

T の表示インデックス b に対し、upL b は名指された要素とその構成可能性の証明を対にする。後者は、その要素が T に属することと T の構成可能性から従う。

  upL : ⟪ T ⟫ → SL.S
  upL b = ⟪ T ⟫↪ b , isL-trans (member T b) hT
  Good : ⟪ T ⟫ → hProp (ℓ-suc ℓ)
  Good b = InjL α (upL b) , squash₁

  definedGood : FOL.Semantics.FormulaPredicate 𝒮ʟ ⟪ T ⟫ SL.S id Good
  definedGood = FOL.Semantics.presented 2 (injLAt zero (suc zero))
    (λ b → α ∷ upL b ∷ [])
    (λ b → ⇔toPath
      (InjLAt.fill zero (suc zero) (α ∷ upL b ∷ []))
      (InjLAt.read zero (suc zero) (α ∷ upL b ∷ [])))

α からインデックス b が名指す構成可能要素 upL b への内部符号化単射があるとき、b を良いインデックスと呼ぶ。パッケージ definedGood はこの性質を injLAt によって公開する。二つの環境位置には α と upL b が入り、InjLAt.fill と InjLAt.read が意味論の両方向を証明する。したがって後の最小要素探索が見るのは、任意のホスト述語ではなく固定された対象論理式である。

  selfGood : ⟨ Good LC.self ⟩
  selfGood = inclusion-coded α α (λ z z∈α → z∈α)

  nonempty : ∥ Σ[ b ∶ ⟪ T ⟫ ] ⟨ Good b ⟩ ∥₁
  nonempty = ∣ LC.self , selfGood ∣₁

α を名指すインデックスは良いものである。名指された要素は α に等しく、恒等的な包含が α から自身への内部単射を符号化する。したがって良いインデックスの型には単に要素が存在する。

  least : Σ[ b ∶ ⟪ T ⟫ ] IsLeast LC.w Good b
  least = leastOfFormula LC.w definedGood lem nonempty

  m : ⟪ T ⟫
  m = least .fst

整列順序 w と definedGood に、論理式に面する最小要素探索を適用する。排中律が表示された単射論理式の充足を判定し、非空性が最小の良いインデックスを保証する。そのインデックスを m と書く。

  μ : SL.S
  μ = upL m

  μ∈T : ⟨ μ .fst ∈ˢ T ⟩
  μ∈T = member T m

選んだインデックス m を構成可能な論域へ持ち上げ、その結果を μ と呼ぶ。定義により、μ の基礎集合は m が T の中で名指す要素である。

  oμ : IsOrd (μ .fst)
  oμ = mem-ord {A = T} oT (μ .fst) μ∈T

表示の定理から μ ∈ T が得られる。T は順序数なので、その各要素も順序数である。したがって μ は必要な順序数性を持つ。

  α↪μ : InjL α μ
  α↪μ = (least .snd) .fst

最小インデックスの良さは、今では論理式で定義された命題 InjL α μ として直接述べられる。μ は m が名指す構成可能な要素だからである。したがって、選ばれた候補から前向きの単射が直ちに得られる。

  cardμ : IsCardinalL μ
  cardμ δ δ∈μ μ↪δ = (least .snd) .snd b bGood b<m
    where
    δ∈T : ⟨ δ .fst ∈ˢ T ⟩
    δ∈T = oT .fst {x = μ .fst} {y = δ .fst} δ∈μ μ∈T

μ が基数であることを示すため、ある要素 δ ∈ μ に内部単射 μ ↪ δ があると仮定する。順序数 T の推移性から δ ∈ T となり、T の表示が δ を名指すインデックス b を与える。

    b : ⟪ T ⟫
    b = fiber T δ∈T .fst
    bδ : ⟪ T ⟫↪ b ≡ δ .fst

ファイバーの定理は、インデックス b と、その表示要素を δ と同一視する等式を与える。このデータにより、所属と単射の主張を、インデックスで表された要素と構成可能要素 δ の間で移送できる。

    bδ = fiber T δ∈T .snd
    bS : upL b ≡ δ
    bS = Σ≡Prop (λ x → (isL x) .snd) bδ
    bGood : ⟨ Good b ⟩
    bGood = subst (InjL α) (sym bS) (injl-trans α μ δ α↪μ μ↪δ)

インデックス b は良いものである。α ↪ μ と仮定した μ ↪ δ を合成し、ファイバーの等式でインデックスの表示要素に合わせる。したがって b は同じ探索の別の候補である。

    b<m : let module W = SWO LC.w in b W.<∙ m
    b<m = transport (λ i → sym (LC.w-lt b m) i)
            (subst (λ z → ⟨ z ∈ˢ μ .fst ⟩) (sym bδ) δ∈μ)

さらに b < m である。w の関係は表示された順序数の間の所属であり、仮定 δ ∈ μ を移送すると、まさにこの比較が得られる。最小の良いインデックスより下に良いインデックスがあることは不可能なので、そのような単射 μ ↪ δ は存在しない。したがって μ は内部基数である。

  μ⊆α : (z : SV.S) → ⟨ z ∈ˢ μ .fst ⟩ → ⟨ z ∈ˢ α .fst ⟩
  μ⊆α = go (ord-tri (μ .fst) oμ (α .fst) oα)
    where
    go : Tri (μ .fst) (α .fst) → (z : SV.S) → ⟨ z ∈ˢ μ .fst ⟩ → ⟨ z ∈ˢ α .fst ⟩

残るのは μ ⊆ α である。順序数の三分法で二つの基礎順序数を比較する。μ ∈ α なら α の推移性から包含が従い、μ = α なら等式に沿う移送で得られる。

    go (inl μ∈α)       z z∈μ = oα .fst z∈μ μ∈α
    go (inr (inl e))   z z∈μ = subst (λ v → ⟨ z ∈ˢ v ⟩) e z∈μ

第三の場合 α ∈ μ は最小性に反する。α を名指すインデックスは良く、α ∈ μ はそのインデックスが w で m より真に小さいことを意味する。したがって三分法の最初の二つの場合だけが残る。

    go (inr (inr α∈μ)) z z∈μ =
      ⊥₀-rec ((least .snd) .snd LC.self selfGood
        (transport (λ i → sym (LC.w-lt LC.self m) i)
          (subst (λ v → ⟨ v ∈ˢ μ .fst ⟩) (sym LC.self-eq) α∈μ)))

包含 μ ⊆ α は内部単射 μ ↪ α を符号化する。α ↪ μ、μ の順序数性と基数性を合わせると、約束した代表が完成する。順序数の大きさに関する議論は、L を離れずにこの内部基数へ移せる。

  μ↪α : InjL μ α
  μ↪α = inclusion-coded μ α μ⊆α

代表 μ は順序数基数であり、α へ内部単射でき、α からも内部単射でき、α の中に含まれる。これにより、任意の構成可能順序数に関する基数算術を、内部基数に関する基数算術へ帰着できる。

順序数の基数代表を選ぶ