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

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λ ∅∈λ)
  (sup : Superadequate lam)
  (X-isL : ⟨ isL X ⟩) where

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

凝縮により、崩壊像はある順序数 β による 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≡ : hullL .fst ≡ 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 ≡ v .fst))

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

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

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

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

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

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

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

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

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

ρ : Fin  → Fin 
ρ 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 
invFo = (var zero ∈̇ con hullL) ∧̇ renameFo ρ P.piFo

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

π-graph : (x : S) (mx : ⟨ x .fst ∈ˢ HS.M ⟩) (v : S) → HSC.π (x .fst) ≡ v .fst
        → ⟨ (v ∷ x ∷ []) ⊨ P.piFo ⟩
π-graph x mx v e = rec₁ (((v ∷ x ∷ []) ⊨ P.piFo) .snd) 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.π (x .fst) , G .fst} {y = v} e) (S≡ {x = P.up (x .fst) mx} {y = x} refl)
      (G .snd mx)
    where

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

    G = P.good-at α oα (x .fst) mx (layer-trans (Lset-layer α) {x = HS.M} {y = x .fst} 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 (x' .fst) (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' : ⟨ x' .fst ∈ˢ HS.M ⟩

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

  mx' = subst (λ w → ⟨ x' .fst ∈ˢ 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') → (fn v m) .fst ≡ (fn v' m') .fst → v .fst ≡ v' .fst
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

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

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

δ : V ℓ
δ = δL .fst

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

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

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

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

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

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

段階の添字より上に、超適切な層が得られる。そこは、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) ((sucʟ δL) .snd)

構成可能性の証明により、周囲の集合 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↪μ μ↪δ))