無限構成可能段階をその添字へ単射する

この章を読むか、読書案内と依存マップで別のルートを選べます。

読書案内 · 依存マップ

この章では GCH に用いる段階評価を証明します。δ が有限でない構成可能順序数なら、Lset δ から δ への内部的に符号化された単射が存在します。結論 InjL は、単射の条件を満たす構成可能なグラフの型を命題的切り詰めにかけたものです。したがって、そのようなグラフの存在だけを主張し、特定のグラフは保持しません。ホスト側の関数も全単射も主張せず、δ 自身が内部基数であることも仮定しません。

{-# OPTIONS --cubical --safe --guardedness #-}

この証明では、存在と選択を一貫して区別します。古典的推論は適切な段階と基数代表を与えますが、外部に示される単射はすべて命題的切り詰めの内側にとどまります。したがって、局所的な証人を命題の証明の中で使っても、それが標準的な大域データになることはありません。

open import Base.Prelude
open import Base.Classical using ( LEM )

議論は宇宙レベルについて一様であり、明示された排中律の実例 lem : LEM (ℓ-suc ℓ) だけを使います。とくに、後で内部の基数代表へ移ることによって、もとの順序数 δ が基数であるという仮定が暗黙に加わることはありません。

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

逆崩壊を L の内部の単射にするには、そのグラフを構成可能構造の一階言語で表さなければなりません。必要なのは変数、定数、所属、連言だけです。論理式の名前替えによって二つの引数位置を交換しても充足関係が保たれ、周囲の累積階層が崩壊を計算する集合を与えます。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_ )
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

包が必要な外延性を備えるため、崩壊は包の上で単射になります。後で self∈sucV は δ を集合論的な後続 δ+1 に入れ、構成可能段階の補題は推移性、単調性、段階とその層の間の移行を与えます。この議論では、順序数の後続と構成可能な後続段階を区別します。

open import V.Collapse {ℓ} using ( isExt )
open import V.Model {ℓ} using ( self∈sucV )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-layer; layer-trans )
open import L.Ordinal {ℓ} using ( #∈ω; suc-ord )

後では、段階に関する二つの相補的な事実を用います。構成可能段階は L の要素としてまとめられ、順序数 x が段階 Lset α に属するなら、階数の比較から x ∈ α が従います。目標 InjL は内部的に符号化された単射の単なる存在を記録し、IsCardinalL は後で導入する基数代表にだけ適用されます。

open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset→∈ )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Numerals {ℓ} using ( sucʟ; sucʟ-fst )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Cardinal {ℓ} lem using ( InjL; IsCardinalL )

求める評価は StageCountedCoded という型で表されます。証明では、まず任意の無限順序数 δ を内部の基数代表 μ で表し、適切な Skolem 包を μ へ数え上げ、最後に符号化された単射を合成します。逆崩壊もこの鎖に組み込めるよう、そのグラフが L の要素である定義可能写像として表します。

open import L.GCH.Assembly {ℓ} lem using ( StageCountedCoded )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.GCH.CardinalRepresentative {ℓ} lem using ( cardOf )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
open import L.GCH.SkolemHull {ℓ} lem

全体の比較は三つの材料を組み合わせます。凝縮は包を段階 Lset β に変え、有限でない順序数に対するシフトと基数代表 μ は始点を μ へ単射できるようにし、最後に合成がこれらの局所的な比較を求める端点へつなぎ戻します。どの段階でも、内部的に符号化された単射がホスト側の関数に変わることはありません。

  using ( module Frame; module HullStage; module HullElemDown )
open import L.GCH.ConstructibleHull {ℓ} lem using ( module PiIn; module Condense′ )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( ordL; ω⊆; no-fin; module Shift )
open import L.GCH.AdequateStages {ℓ} lem using ( superadequate-above; Superadequate )
open import L.GCH.StageCountingTools {ℓ} lem using ( move )

包の計数定理が、ここでの量的な入力です。出発集合が有限でない内部基数へ単射するなら、そこから生成される包も同じ基数へ単射します。また、各順序数が自分自身の構成可能段階に含まれることと、構成可能性の証明が命題なので基礎集合の等しさから構成可能な台の要素の等しさが決まることも用います。

open import L.GCH.HullCounting {ℓ} lem using ( ord⊆Lset; module Count; S≡ )

逆崩壊は、構成可能な台 S の要素の間の写像として比較されます。その要素は基礎集合と構成可能性の証明を含みますが、証明の成分は命題です。したがって、基礎集合の等しさから S での等しさが決まり、符号化されたグラフは値を表示する構成可能性の証拠に依存しません。

open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )

有限でないことは、後の計数の議論で二つの具体的な役割を果たします。シフト単射 δ+1 ↪ δ を与え、また空集合を含むすべての有限順序数が δ より下にあることを保証します。逆崩壊の論理式に用いる長さ二の環境は、この無限性の議論とは独立です。

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet; ∅ )
open InfinitySet {ℓ} using ( ω; sucV )
open import Cubical.Data.Vec using ( _∷_; [] )
import Cubical.Data.Empty as Empty

命題的切り詰めは、二つの決定的な箇所に現れます。包がある論理式を満たすことを示す際には、包が単に構成可能であるという事実を命題である充足の主張へ消去できます。また、すべての InjL の結論も、その最外層が命題的切り詰めです。したがって、ここでの切り詰めの消去先は常に命題です。

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( squash₁ )

_∈ˢ_ と書く所属は、周囲の階層構造 𝒮ᵥ における所属です。包、その崩壊像、順序数の添字が構成可能構造の要素としてまとめられる前には、それらについての主張をこの所属で表します。

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

型 S は構成可能構造の台です。その要素は、周囲の集合と、その集合が L に属することの証明からなります。以下の内部的に符号化された写像では、定義域、終域、グラフのパラメータがすべてこの台に属します。

open hPropStructure 𝒮ʟ using ( S )

対象言語の論理式が 𝒮ʟ で満たされることは、絶対性を通して、周囲の集合についての対応する命題として読まれます。この橋渡しにより、逆崩壊のグラフを外側で証明し、同じ関係を L の内部の定義可能なグラフとしてまとめられます。

open FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using () renaming ( _⊨ᵐ_ to _⊨_ )

ここでは、約束の小さな違いを調整する必要があります。崩壊の論理式 piFo は値と逆像を (v,x) の順で読みますが、定義可能写像のグラフは (x,v) の順で評価されます。二つの自由変数を入れ替え、名前替えのもとでの充足の不変性を使えば、同じ関係を必要な順序で表せます。モデルも論理式の意味も変わりません。

module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename )

強化された十分な段階で Skolem 包を数える

まず、議論の幾何的な部分を、後で行う基数評価から切り離します。後続について閉じた順序数 lam と、Lset lam に含まれる出発集合 X を固定します。さらに、この添字が空集合を含み、X から生成される Skolem 包が必要な意味で初等的であると仮定します。この時点では、目標となる基数はまだ現れません。

module Site (lam : V ℓ) (ordλ : IsOrd lam)
  (succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : V ℓ) (X⊆Lλ : (z : V ℓ) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
  (elem : Frame.A.Elementary lam ordλ succλ X X⊆Lλ ∅∈λ)

lam の強化された十分性は、凝縮に必要な閉性と正しさの条件を与えます。X の構成可能性により、包を生成する有限な閉包段階の列とその合併は L の中にとどまります。したがって、包とその崩壊像の双方を構成可能構造の内部で表せます。

  (sup : Superadequate lam)
  (X-isL : ⟨ isL X ⟩) where

凝縮により、崩壊像はある順序数 β による Lset β と同一視されます。一方、包の構成から包 M が構成可能であることも分かります。この二つの事実によって、逆崩壊を構成可能段階から構成可能な包への写像として扱えます。

  condenses′ = Condense′.condenses′ lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL
  M-isL = Condense′.M-isL lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL

崩壊を π : M → πX と書き、その像を πX と書きます。崩壊の仕組みから、πX の点の逆像、外延的な包の上での単射性、包の推移的な部分を固定することが得られます。論理式 piFo は π のグラフを表し、その妥当性補題が、この論理式の充足と実際の崩壊値を結びます。

  module HS = HullStage lam ordλ succλ X X⊆Lλ ∅∈λ using ( M )
  module HSH = HullStage.H lam ordλ succλ X X⊆Lλ ∅∈λ using ( X⊆M )
  module HSC = HullStage.C lam ordλ succλ X X⊆Lλ ∅∈λ
    using ( πX; π; fixes; πX-intro; πX-member )
  module P = PiIn (HS.M , M-isL) using ( piFo; up; good-at; piFo-val )

順序数 β は、崩壊像が位置する高さを表します。この一般的な場では、まだ数えるべき順序数 δ も目標の基数もないため、β をそれらと比較することはできません。

  β : V ℓ
  β = condenses′ .fst

付随する順序数性の証明により、Lset β は順序数で添字づけられた段階になります。後で、ある順序数が Lset β に属することを β との順序数比較へ変換する際にも、この証明が必要です。

  oβ : IsOrd β
  oβ = condenses′ .snd .fst

等式 ext : πX = Lset β は、崩壊の理論と構成可能階層を結ぶ要です。これは崩壊像への所属を β の段階への所属に変換します。後で崩壊が δ を固定すると示した後、まさにこの等式によって δ ∈ Lset β が得られます。

  ext : HSC.πX ≡ Lset β
  ext = condenses′ .snd .snd

β は順序数なので Lset β は構成可能であり、台 S の要素 Lβ としてまとめられます。このまとめられた段階が逆崩壊写像の定義域になります。

  Lβ : S
  Lβ = LsetS β oβ

順序数 β 自身も構成可能であり、βL としてまとめられます。逆崩壊写像が使うのは Lβ ですが、まとめられた添字は、後の有界部分集合の議論で β と目標の基数を内部的に符号化された単射によって比較するために使われます。

  βL : S
  βL = ordL β oβ

内部的に符号化された写像の終域は、外側で記述された包の要素の集まりではなく、台 S の要素でなければなりません。hullL は、構成可能性の証拠とともに包の内部的な表示を与えます。

  hullL : S
  hullL = Condense′.hullL lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL

等式 M≡ は、包の二つの表示を結びます。崩壊の定理は周囲の集合 M を扱い、内部のグラフは台の要素 hullL を扱います。この等式に沿って輸送することで、同じ所属の証拠を両方で使えます。

  M≡ : fst hullL ≡ HS.M
  M≡ = Condense′.hullL-spec lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL

包の枠組みから、M 上の所属関係が外延的であることが分かります。これは、包の二つの要素が同じ崩壊値をもつなら等しいと結論するために必要な仮定です。

  Mext : isExt HS.M
  Mext = Frame.Mext lam ordλ succλ X X⊆Lλ ∅∈λ

この外延的な包に崩壊の単射性定理を適用すると π-inj が得られます。これは、各逆像の一意性と、それらの逆像から作る逆崩壊写像の単射性の両方を証明するために使われます。

  module CI = HullStage.C.InjExt lam ordλ succλ X X⊆Lλ ∅∈λ Mext using ( π-inj )

崩壊の値 v の逆像とは、崩壊させたものが v の底の集合と等しくなるような、包の要素 x のことです。この記録は切り詰められていない依存対であり、逆像とその所属とその同一視を明示的に運びます。

  Pre : S → Type (ℓ-suc ℓ)
  Pre v = Σ[ x ∈ V ℓ ] (⟨ x ∈ˢ HS.M ⟩ × (HSC.π x ≡ fst v))

逆像は一意です。崩壊が包の上で単射だからです。同じ値をもつ二つの記録は π-inj を通して逆像を同一視し、残りの成分は命題になります。だからこそ、証人を選ばずに逆像を復元できるのです。

  isPropPre : (v : S) → isProp (Pre v)
  isPropPre v (x , mx , e) (x' , mx' , e') =
    Σ≡Prop (λ x → isProp× (snd (x ∈ˢ HS.M)) (setIsSet _ _)) (CI.π-inj x x' mx mx' (e ∙ sym e'))

逆崩壊を定義する必要があるのは、その像の点だけであり、凝縮によってこの像は Lset β と同一視されています。そこで Mem v は、v の基礎集合がこの段階に属するという命題です。この定義域の証拠から、逆像の型に要素があることが分かります。

  Mem : S → Type (ℓ-suc ℓ)
  Mem v = ⟨ fst v ∈ˢ fst Lβ ⟩

Lset β への所属から最初に得られるのは、崩壊の逆像の型を命題的に切り詰めたものだけです。Pre v はすでに命題であると示されているため、切り詰めの消去によってその一意な要素を取り出せます。したがって pre は一意性によって逆像の値を得ており、複数の逆像から恣意的に選んではいません。

  pre : (v : S) → Mem v → Pre v
  pre v m = PT.rec (isPropPre v) (λ w → w)
    (HSC.πX-member (fst v) (subst (λ w → ⟨ fst v ∈ˢ w ⟩) (sym ext) m))

逆像は構成可能な集合としてまとめられます。その構成可能性は、まとめられた包と包を同一視することを通して、包から運ばれます。この関数が定義されるのは β の段階の要素の上だけで、終域は包です。崩壊の像の上での逆であり、大域的な逆ではありません。

  fn : (v : S) → Mem v → S
  fn v m = pre v m .fst
         , isL-trans {x = fst hullL} {y = pre v m .fst}
             (subst (λ w → ⟨ pre v m .fst ∈ˢ w ⟩) (sym M≡) (pre v m .snd .fst)) (snd hullL)

改名は、二つの変数の枠を入れ替えます。枠ゼロが枠一になり、逆もまた同様です。

  ρ : Fin 2 → Fin 2
  ρ zero = suc zero
  ρ (suc zero) = zero

二つの環境には、同じ台の要素が逆の順序で並んでいます。証明 ag は二つの変数添字のそれぞれについて、ρ を適用してから変数を参照することと、入れ替えた環境でその変数を参照することが一致すると確かめます。この各点での一致が、名前替えのもとで充足関係を保つための仮定です。

  private
    ag : (x v : S) → Ren.Agrees ρ (x ∷ v ∷ []) (v ∷ x ∷ [])
    ag x v zero = refl
    ag x v (suc zero) = refl

名前を替えた論理式の、順序どおりの環境での充足は、入れ替えた環境のもとでのもとの論理式の充足と等しくなります。これが、崩壊のグラフの枠を整えるために使う輸送です。

    rn : (x v : S) → ⟨ (x ∷ v ∷ []) ⊨ renameFo ρ P.piFo ⟩ ≡ ⟨ (v ∷ x ∷ []) ⊨ P.piFo ⟩
    rn x v = cong ⟨_⟩ (Ren.⊨-rename ρ P.piFo (x ∷ v ∷ []) (v ∷ x ∷ []) (ag x v))

逆崩壊のグラフはこの連言です。逆像が包に属し、名前を替えた対のグラフが逆像と値について成り立つ、というものです。

  invFo : Formula S 2
  invFo = (var zero ∈̇ con hullL) ∧̇ renameFo ρ P.piFo

包の要素 x の崩壊が v なら、実際の対 (v,x) は piFo を満たします。包の構成可能性そのものが命題的切り詰めを通して与えられるため、その切り詰めを命題である充足の主張へ消去し、包を含む任意の構成可能段階で証明します。

  π-graph : (x : S) (mx : ⟨ fst x ∈ˢ HS.M ⟩) (v : S) → HSC.π (fst x) ≡ fst v
          → ⟨ (v ∷ x ∷ []) ⊨ P.piFo ⟩
  π-graph x mx v e = PT.rec (snd ((v ∷ x ∷ []) ⊨ P.piFo)) read M-isL
    where
    read : Σ[ α ∈ V ℓ ] (IsOrd α × ⟨ HS.M ∈ˢ Lset α ⟩) → ⟨ (v ∷ x ∷ []) ⊨ P.piFo ⟩

読みの主張は、二つの枠を運びます。崩壊の値は v の底の集合と同一視され、包の要素は x の底の集合と同一視されます。

    read (α , oα , M∈Lα) =
      subst2 (λ a b → ⟨ (a ∷ b ∷ []) ⊨ P.piFo ⟩)
        (S≡ {x = HSC.π (fst x) , G .fst} {y = v} e) (S≡ {x = P.up (fst x) mx} {y = x} refl)
        (G .snd mx)
      where

包を含む構成可能段階 Lset α が与えられると、層の推移性によって各包の要素 x も同じ段階に入ります。補題 good-at は、π x の構成可能性の証明と、まとめられた崩壊値と要素が piFo を満たすことの証明を与えます。

      G = P.good-at α oα (fst x) mx (layer-trans (Lset-layer α) {x = HS.M} {y = fst x} mx M∈Lα)

証明 defines は、実際の逆像の値と内部の論理式を結ぶ橋です。第一成分はその値をまとめられた包に入れ、第二成分は崩壊の等式と名前替えを用いて、invFo がその値を対応する像の点に関係づけることを示します。

  defines : (v : S) (m : Mem v) → ⟨ (fn v m ∷ v ∷ []) ⊨ invFo ⟩
  defines v m =
      subst (λ w → ⟨ pre v m .fst ∈ˢ w ⟩) (sym M≡) (pre v m .snd .fst)
    , transport (sym (rn (fn v m) v)) (π-graph (fn v m) (pre v m .snd .fst) v (pre v m .snd .snd))

残るのは逆像の特定だけです。逆のグラフを満たすどんな逆像も、まとめられた逆像と同じ崩壊の値をもち、崩壊の単射性が、二つの逆像の等しさを返します。

  only : (v : S) (m : Mem v) (x' : S) → ⟨ (x' ∷ v ∷ []) ⊨ invFo ⟩ → x' ≡ fn v m
  only v m x' (hx , hp) = S≡ (CI.π-inj (fst x') (pre v m .fst) mx' (pre v m .snd .fst)
    (sym (P.piFo-val x' mx' v (transport (rn x' v) hp)) ∙ sym (pre v m .snd .snd)))
    where
    mx' : ⟨ fst x' ∈ˢ HS.M ⟩

グラフを満たす別の出力 x' について、第一の連言はその基礎集合がまとめられた包に属することを述べます。M≡ に沿って輸送すると周囲の包 M への所属が得られ、崩壊の単射性によって x' と復元した逆像を比較するための前提になります。

    mx' = subst (λ w → ⟨ fst x' ∈ˢ w ⟩) M≡ hx

以上の結果により、制限された逆写像は一価な定義可能写像として内部化されます。各 v ∈ Lβ は包へ送られて invFo を満たし、only は同じグラフを満たすほかの出力がこの値に等しいことを示します。単射性はさらに必要な性質であり、次に別途証明します。

  Dmap : DefinableMap
  Dmap = record
    { dom = Lβ ; cod = hullL ; fn = fn
    ; into = λ v m → subst (λ w → ⟨ pre v m .fst ∈ˢ w ⟩) (sym M≡) (pre v m .snd .fst)
    ; graph = invFo ; defines = defines ; only = only }

一意性によって定まる各逆像は π(pre(v)) = v を満たします。したがって、逆崩壊写像の二つの値が等しければ、その等式に π を作用させ、両端の逆像の等式と合成することで v = v' が得られます。よって崩壊像上の逆写像は単射です。この段階で使うのは右逆の等式であり、崩壊そのものの単射性ではありません。

  inj : (v : S) (m : Mem v) (v' : S) (m' : Mem v') → fst (fn v m) ≡ fst (fn v' m') → fst v ≡ fst v'
  inj v m v' m' q = sym (pre v m .snd .snd) ∙ cong HSC.π q ∙ pre v' m' .snd .snd

制限された逆は、Lβ から包への符号化された単射としてまとめられ、最初の節の構成が完成します。まとめは切り詰められた形を保つので、公開されるのは符号化されたグラフの存在だけです。

  Lβ↪M : InjL Lβ hullL
  Lβ↪M = Inj.injL Dmap inj

Skolem 包を元の段階へ崩壊して戻す

計数のモジュール At は、非有限の構成可能な順序数 δL、その順序数性、ω への所属の排除、同じく非有限な内部の基数代表 μ、そして δL と μ の間の双方向の符号化された単射を固定します。これらが、基数代表で非有限の段階を数えるために必要なデータそのものです。

module At (δL : S) (oδ : IsOrd (fst δL)) (δ∉ω : ⟨ fst δL ∈ˢ ω ⟩ → Empty.⊥)
          (μ : S) (oμ : IsOrd (fst μ)) (cμ : IsCardinalL μ)
          (μ∉ω : ⟨ fst μ ∈ˢ ω ⟩ → Empty.⊥)
          (δ↪μ : InjL δL μ) (μ↪δ : InjL μ δL) where

台の要素 δL と、その基礎となる周囲の順序数 δ = fst δL を区別すると見通しがよくなります。集合論的後続、段階への所属、崩壊は δ に作用し、内部的に符号化された単射の端点にはまとめられた δL を使います。

  δ : V ℓ
  δ = fst δL

順序数 δ の段階は、それを含む最初の構成可能な層であり、ここでは、十分に高い超適切な層を見つけるための出発点の添字を供給します。

  private
    α₀ : V ℓ
    α₀ = stage δ (snd δL)

最小段階の構成は常に順序数の添字を返します。これを構成可能集合 δ に適用すると α₀ の順序数性が得られます。この事実は、δ 自身が順序数であるという別の仮定から導かれるのではありません。

    oα₀ : IsOrd α₀
    oα₀ = stage-ord δ (snd δL)

順序数 δ はそれ自身の段階に属します。これが、δ を構成可能階層の中に位置づける所属の事実です。

    δ∈Lα₀ : ⟨ δ ∈ˢ Lset α₀ ⟩
    δ∈Lα₀ = stage-mem δ (snd δL)

段階の添字より上に、超適切な層が得られます。そこは、Skolem 包の構成と凝縮の移送に必要なすべての閉じの条件を携えています。

    sa = superadequate-above α₀ oα₀

上で得た強化された十分な段階を取り、その順序数添字を λ と書きます。以後の包と凝縮の議論は、すべてこの十分に高い一つの段階で行います。

  opaque
    lam : V ℓ
    lam = sa .fst

選ばれた高い添字 λ は順序数です。その推移性により、まず比較 δ ∈ α₀ ∈ λ から δ ∈ λ を得て、さらに δ+1 の各要素を λ より下に置きます。

    ordλ : IsOrd lam
    ordλ = sa .snd .fst

後続についての閉性は、直後に使う添字の第二の性質です。δ ∈ λ から δ+1 ∈ λ が従います。これは順序数添字 λ についての主張であり、構成可能段階の後続を取ることとは異なります。

    succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩
    succλ = sa .snd .snd .snd .fst .snd .fst

強化された十分性は、λ の各要素 d の上に、なお λ に属する十分な段階 γ が単に存在することを述べます。このような中間の十分な段階が、包の計数と凝縮に必要な局所的な反映と閉性を与えます。

    sup : Superadequate lam
    sup = sa .snd .snd .snd .snd

まず、δ ∈ Lset α₀ と、δ と α₀ がともに順序数であることから δ ∈ α₀ が従います。さらに α₀ ∈ λ なので、順序数 λ の推移性により δ ∈ λ を得ます。

    δ∈λ : ⟨ δ ∈ˢ lam ⟩
    δ∈λ = ordλ .fst (ord∈Lset→∈ α₀ oα₀ δ oδ δ∈Lα₀) (sa .snd .snd .fst)

始点集合をフォン・ノイマン後続 X = δ+1 とします。これは δ と、それより小さいすべての順序数を含み、δ が順序数なので推移的です。これらの性質を用いて、後で崩壊が δ を固定することを示します。

  X : V ℓ
  X = sucV δ

順序数添字の後続についての閉性から、X = δ+1 ∈ λ が得られます。これは順序数の比較です。包の構成に必要な、X の各要素が Lset λ に属するという別の主張は、次の段階で導きます。

  sucδ∈λ : ⟨ X ∈ˢ lam ⟩
  sucδ∈λ = succλ δ δ∈λ

z ∈ X なら、順序数 λ の推移性と X ∈ λ から z ∈ λ が従います。さらに、順序数はそれ自身の構成可能段階に含まれるという一般的な事実により、z ∈ Lset λ を得ます。したがって、必要な前提はちょうど X ⊆ Lset λ です。

  X⊆Lλ : (z : V ℓ) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩
  X⊆Lλ z hz = ord⊆Lset lam ordλ z (ordλ .fst hz sucδ∈λ)

δ は有限でないため、すべての有限順序数は δ より下にあり、とくに ∅ ∈ δ です。これを δ ∈ λ と順序数 λ の推移性に合わせると、包の構成に必要な別の前提 ∅ ∈ λ が得られます。

  ∅∈λ : ⟨ ∅ ∈ˢ lam ⟩
  ∅∈λ = ordλ .fst (ω⊆ δ oδ δ∉ω ∅ (#∈ω zero)) δ∈λ

始点の集合は構成可能です。構成可能な集合の符号化された後続も構成可能であり、符号化された後続と集合論の後続を同一視する等式に沿って運ばれるからです。

  X-isL : ⟨ isL X ⟩
  X-isL = subst (λ w → ⟨ isL w ⟩) (sucʟ-fst δL) (snd (sucʟ δL))

構成可能性の証明により、周囲の集合 X = δ+1 は台の要素 XS になります。変わるのは表示だけであり、計数の問題は依然として δ の後続を基数代表 μ へ単射することです。

  XS : S
  XS = X , X-isL

始点は鎖 δ+1 ↪ δ ↪ μ によって数えられます。最初の符号化された単射は、任意の非有限順序数 δ に対するシフトであり、二番目は δ からその基数代表 μ への仮定された内部単射です。これらを合成して InjL XS μ を得ますが、δ 自身が基数であるとは仮定しません。

  base : InjL XS μ
  base = injl-trans XS δL μ
    (move (sucʟ δL) XS δL δL (sucʟ-fst δL) refl (Shift.injL δL oδ δ∉ω))
    δ↪μ

X から生成される Skolem 包は、周囲の段階 Lset λ の初等部分構造です。この初等性により、計数定理と凝縮の議論は、包と段階の間で必要な論理式と証人を移すことができます。

  elem = HullElemDown.elem lam ordλ X X⊆Lλ ∅∈λ

Skolem 包は、基数の代表 μ によって数えられます。始点がすでに μ へ単射し、包の章が、閉じても計数が保たれることを示しているからです。

  hull↪μ = Count.hull↪κ lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL μ oμ cμ μ∉ω base

一般の凝縮構成をこの包に適用します。すると、その段階 Lβ が崩壊像となる順序数 β、構成可能集合としての包、そして逆崩壊から得られる、命題的に切り詰められた符号化単射 Lβ ↪ M が与えられます。

  module St = Site lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL
    using ( β; oβ; ext; Lβ; hullL; Lβ↪M )

残る比較では、この包について三つの事実を使います。その基礎集合は M であり、始点の各要素は M に属し、崩壊 π は M を Lβ へ写すとともに、M の推移的部分集合の要素を固定します。これらを推移的な始点 δ+1 に適用すると、δ を Lβ に置くことができます。

  module HS = HullStage lam ordλ succλ X X⊆Lλ ∅∈λ using ( M )
  module HSH = HullStage.H lam ordλ succλ X X⊆Lλ ∅∈λ using ( X⊆M )
  module HSC = HullStage.C lam ordλ succλ X X⊆Lλ ∅∈λ
    using ( π; fixes; πX-intro )

順序数 δ はそれ自身の後続に属します。それが、包の構成の始点の集合です。

  δ∈X : ⟨ δ ∈ˢ X ⟩
  δ∈X = self∈sucV δ

したがって、順序数 δ は包に属します。包が、始点の集合のすべての要素を含むからです。

  δ∈M : ⟨ δ ∈ˢ HS.M ⟩
  δ∈M = HSH.X⊆M δ δ∈X

後続 X = δ+1 は推移的で、包 M に含まれます。したがって崩壊は X の各要素を固定し、とくに δ ∈ X から π(δ) = δ が従います。

  πδ : HSC.π δ ≡ δ
  πδ = HSC.fixes X
    (λ a a∈ₛX → ∈∈ₛ {a = a} {b = HS.M} .fst (HSH.X⊆M a (∈∈ₛ {a = a} {b = X} .snd a∈ₛX)))
    (suc-ord oδ .fst) δ δ∈X

順序数 δ は、崩壊の層 Lset β の中にあります。その崩壊 (すなわちそれ自身) が崩壊の像の中にあり、崩壊の像が Lset β に等しいからです。

  δ∈Lβ : ⟨ δ ∈ˢ Lset St.β ⟩
  δ∈Lβ = subst (λ w → ⟨ w ∈ˢ Lset St.β ⟩) πδ
    (subst (λ w → ⟨ HSC.π δ ∈ˢ w ⟩) St.ext (HSC.πX-intro δ δ∈M))

ここで順序数の段階境界を適用します。順序数 δ が Lset β に属するなら、δ は順序数添字 β に属します。したがって δ ∈ β です。これは段階の単調性に必要な狭義比較であり、その向きから Lset δ ⊆ Lset β が得られます。

  δ∈β : ⟨ δ ∈ˢ St.β ⟩
  δ∈β = ord∈Lset→∈ St.β St.oβ δ oδ δ∈Lβ

標準的な台の表示 Lδ の基礎集合は Lset δ です。At.result はこれを始域とし、最後の定理は、基礎集合が同じ段階に等しい任意の台の要素へこの始域を輸送します。

  Lδ : S
  Lδ = LsetS δ oδ

最終の比較は鎖 Lset δ ↪ Lset β ↪ M ↪ μ ↪ δ に沿います。四つの矢印は順に、δ ∈ β を用いた段階の単調性、逆崩壊、包の計数、そして仮定された単射 μ ↪ δ から得られます。これらを合成すると InjL Lδ δL、すなわち δ の段階から δ への内部的に符号化された単射が命題的切り詰めのもとで存在することが示されます。

  result : InjL Lδ δL
  result = injl-trans Lδ St.Lβ δL
    (inclusion-coded Lδ St.Lβ (λ z hz → Lset-mono {α = St.β} {β = δ} δ∈β hz))
    (injl-trans St.Lβ St.hullL δL St.Lβ↪M
      (injl-trans St.hullL μ δL hull↪μ μ↪δ))

一般の有限でない構成可能順序数 δ に対し、cardOf は基数代表を命題的切り詰めのもとでのみ与えます。証明は消去子の内部で局所的な代表 μ を用い、At.result を適用します。目標 InjL Lδ δ 自身が命題的に切り詰められた存在であり、したがって命題なので、この消去は正当です。得られる定理は、後で GCH の組み立てと有界部分集合の議論の双方に段階計数のインターフェースとして使われます。この定理だけが示すのは Lset δ ↪ δ であり、それ自体で GCH を証明するものではありません。

stage-counted : StageCountedCoded
stage-counted δ Lδ oδ δ∉ω q = PT.rec squash₁ build (cardOf δ oδ)
  where
  build : Σ[ μ ∈ S ]
            ( IsOrd (fst μ) × IsCardinalL μ

cardOf の局所的な証人は、μ が順序数かつ内部の基数であること、その基礎集合が δ に含まれること、そして両方向の符号化された単射が存在することを記録します。包含の証明は基数代表の組に含まれますが、At.result では使われません。この構成が使うのは、二つの単射と、順序数性、基数性、有限でないことです。最後に move は、等式 q : fst Lδ = Lset (fst δ) に沿って、始域を標準的な表示 LsetS (fst δ) oδ から StageCountedCoded が要求する表示へ移します。

            × ((z : V ℓ) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst δ ⟩)
            × InjL δ μ × InjL μ δ )
        → InjL Lδ δ
  build (μ , oμ , cμ , μ⊆δ , δ↪μ , μ↪δ) =
    move (LsetS (fst δ) oδ) Lδ δ δ (sym q) refl

最後に、包の計数定理が要求する有限でないことを確認します。もし μ ∈ ω なら、符号化された単射 δ ↪ μ によって有限でない順序数 δ が有限順序数へ単射し、δ ∉ ω に反します。したがって μ ∉ ω です。この最後の前提により、At.result は選ばれた Lset δ の表示から δ への、命題的に切り詰められた符号化単射をちょうど与えます。

      (At.result δ oδ δ∉ω μ oμ cμ μ∉ω δ↪μ μ↪δ)
    where
    μ∉ω : ⟨ fst μ ∈ˢ ω ⟩ → Empty.⊥
    μ∉ω h = no-fin δ μ oδ δ∉ω oμ h δ↪μ