BedrockL の無限基数における平方律
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップL の無限基数 κ に対し、その要素の順序対からなる集合は、L の内部での符号化された単射によって κ 自身へ注入されます。本章はこの単射を構成します。道筋は対の上の Gödel 順序を経由します。順序を一階の対象言語の論理式として書き下し、順序数 κ のところで外部の Gödel 順序として読み、崩壊によって順序型へ落とし、計数の補題によって κ と比較します。本章は固定された宇宙レベル ℓ の上で、一つ上のレベルの排中律、すなわち以下の順序数の比較が依存する唯一の古典的仮定のもとで進みます。
{-# OPTIONS --cubical --safe --guardedness #-}
この構成がすべて構成的なわけではなく、その理由は形式化ではなく数学にあります。順序数の対を順序づけるには、二つの順序数 a と b について a が b に属するかを判定しなければなりません。本章の古典的な判定はどれもこの一つの問いの実例です。そこでモジュールは、レベル ℓ-suc ℓ の排中律を明示的なデータとして受け取ります。判定される所属の命題の住むレベルです。
open import Base.Prelude open import Base.Classical using ( LEM )
モジュールパラメータはその実例を一度だけ固定し、本章の古典的な段階はどれも正確にこれを消費します。
module L.GCH.CardinalSquareLaw {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
内在化される順序は、一階の対象言語で書かれます。所属と等しさ (等号) の原子式から、結合子、否定、非有界の存在量化子によって作られる論理式であり、周囲の階層の上で解釈されます。階層の二つの事実がその傍らにあり、どちらも議論を閉じるために使われます。所属は整礎であり、順序数は ∈ に沿った帰納を許し、またどの集合も自分自身に属さないため、あり得ない比較はそのまま反証できます。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ¬̇_; ∃̇_ ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV; ∈-irrefl )
符号化された対の座標を読み、それで計数するには、三つの事実が要ります。順序数の後続演算は単射であり、等しい後続は等しい先行者をもちます。順序数の各要素は小さな提示の添字によって名指され、その名指しは単射で、構成可能な集合の要素はそれ自身構成可能です。そして順序対 pr は両座標で単射であり、符号化された対はその二つの成分を確定します。
open import L.Choice.FirstIntersectionStage {ℓ} lem using ( ord-suc-inj ) open import V.Model {ℓ} using ( ∈sucV-elim; ∈sucV-inl; self∈sucV ) open import V.Presentation {ℓ} using ( member; fiber; ↪-inj ) open import V.Coding {ℓ} using ( pr; pr-inj ) open import L.Constructible {ℓ}
構成可能な側では、内側の構造 𝒮ʟ が階層を構成可能な集合という推移的クラスに制限します。全体を通して使う順序数の事実は閉性の事実です。順序数の要素は順序数であり、順序数の後続は順序数であり、ω の要素は順序数であり、任意の二つの順序数は三分法によって比較できます。その傍らには、対の上の外部の Gödel 順序、すなわち本章が内在化する順序があります。
using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset→isL ) open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; ω-ord; #∈ω; ω-mem-ord ) open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc ) open import L.Ordinal.Linear {ℓ} lem using ( ord-tri ) import L.Ordinal.SquareLaw {ℓ} lem as SQ
二つの順序数の比較は、真理値ではなく三つの場合のデータとしてまとめられます。下の証明は、どの場合が起こったかを検査しなければならないからです。狭義に下、等しい、狭義に上。空集合と ω は L の要素として使え、内部の後続数詞はその基底集合の同一視を伴い、数項のスロットを周囲の自然数として読めるようにします。
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ} using ( lt; eq; gt ) renaming ( Tri to TriW ) open import L.Axioms.Basic {ℓ} using ( ∅ʟ ) open import L.Axioms.Infinity {ℓ} lem using ( ωʟ ) open import L.Axioms.Numerals {ℓ} using ( sucʟ; sucʟ-fst )
L の内部では、順序対とグラフの条件を、内側と外側の二つの読みをもつ一階論理式で表します。対の妥当性は符号化された対を二つの成分からなる周囲の順序対と同一視し、グラフの読みは単値性、定義域、単射性、値が終域に属することを表します。これらの条件が内部の符号化された単射を記述します。
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-out; domAt ) open import L.Coding.Expressions {ℓ} using ( sucAtL; sucAtL-adequate ) open import L.Coding.Injection {ℓ} lem using ( injAt; module Extract; module Small ) open import L.Cardinal {ℓ} lem using ( InjCode; InjL; IsCardinalL; _↪_ ) 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.OrderType {ℓ} lem using ( Holds; module Code ) open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate; ω-limit; finite-excl-ω )
二つの符号化された対の比較は、四つの座標と二つの最大値という六つの依存する証人を伴います。積は同時に成り立つ等式と順序条件を保ち、非交和は比較の場合分けを保ちます。証明の成分は命題なので、得られる順序データに余分な選択を生じさせません。
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop ) open import Cubical.Data.Sum using ( _⊎_; inl; inr ) open import Cubical.Foundations.Prelude using ( subst2 ) open import Cubical.Foundations.HLevels using ( isProp×; isSetΣSndProp )
符号化された対の座標は、κ の基底集合の要素であり、その集合の小さな提示を通して読まれます。提示の傍らには、周囲の所属、空虚性の証明を伴う空集合、そして ω と後続の演算があり、座標の比較と計数はこれらの概念の中で行われます。
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; ∅-empty; module InfinitySet ) open InfinitySet {ℓ} using ( ω; sucV )
三つの論理形式が繰り返し現れます。整礎性はすべての要素への到達可能性のデータとして現れ、これが崩壊を順序に沿って下降させます。反証は空の型に住み、証人の存在だけを主張する条件は切り詰めの下で述べられます。そのような条件を消費する目標がそれ自身命題や切り詰めであるため、それで十分なのです。
open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded ) import Cubical.Induction.WellFounded as WF import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
二つの台が名指され、区別して保たれます。周囲の台は階層本来の所属を運び、内側の台 S は構成可能な集合からなり、各要素は周囲の集合とその構成可能性の証明の対であり、その所属は基底の集合の上で読んだ周囲の所属です。
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ ) module SV = hPropStructure 𝒮ᵥ using () module SL = hPropStructure 𝒮ʟ using (S; _∈ˢ_) open SL using ( S )
絶対性の実例は、構成可能な集合という推移的クラスの上で固定されます。有界な論理式は L の内側でも外側でも同じ意味を持ち、環境は射影を通して読まれ、内側の充足関係は平易な _⊨_ に改名されます。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using (_^_; _⊨ᵐ_) open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
内側の台は h-集合であり、そのため要素の等しさを扱えます。要素は第二成分が命題である対なので、二つの要素が等しいのは基底集合が等しいときに限ります。対のパスの補題は、各成分の等しさから二つの対の等しさを構成します。
isSetS : isSet S isSetS = isSetΣSndProp setIsSet (λ v → snd (isL v)) opaque pair≡ : {A : Type ℓ} {B : Type ℓ} {a a' : A} {b b' : B} → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
対のパスはまさにこの構成です。a ≡ a' と b ≡ b' から、各点で (a , b) ≡ (a' , b') というパスを作ります。順序数は構成可能です。その理由は直接です。順序数 x はみずからの後続に属し、その段階は L の集合であり、段階への所属が構成可能性だからです。この主張は命題なので、証明は事実の外には何も運びません。
pair≡ e1 e2 = λ i → e1 i , e2 i opaque isL-ord : (x : V ℓ) → IsOrd x → ⟨ isL x ⟩ isL-ord x ox = Lset→isL (sucV x) (suc-ord ox) x (ord∈Lset-suc x ox)
したがって順序数 x は、その構成可能性の証明とともに、構成可能な台の要素 ordL x ox とみなせます。二つの座標がともに K に属するという関係に定義可能分出を適用すると、それらの順序対からなる構成可能集合 prodL K が得られます。
ordL : (x : V ℓ) → IsOrd x → S ordL x ox = x , isL-ord x ox open import L.InjectionComposition {ℓ} lem public using ( module Relation ) private module Product (K : S) = Relation K K
積の記述の条件は、二つの座標がともに K の要素であることを述べます。ホスト側の読みは、二つの射影の K の基底集合への周囲の所属であり、その読みの両方向が与えられます。
((var (suc zero) ∈̇ con K) ∧̇ (var zero ∈̇ con K)) (λ x y → (fst x ∈ˢ fst K) ⊓ (fst y ∈ˢ fst K)) (λ x y e h → h) (λ x y e h → h)
したがって prodL K は、K の二つの要素からなる順序対の集合であり、L の内部でそれらを抑える段階から分出されたものです。
prodL : S → S prodL = Product.rel
積への所属は、切り詰められた存在によって特徴づけられます。K の二つの要素 a と b があって、その要素がそれらの順序対に等しい、と。切り詰めは、条件が証人の存在を主張する以上のことを記録しません。この段階では、ある証人の対を別の対と区別する何ものもなく、切り詰めを取り除くことは、証人の一意性が証明された後にはじめて可能になります。
InProd : S → V ℓ → Type (ℓ-suc ℓ) InProd K e = ∥ Σ[ a ∈ S ] Σ[ b ∈ S ] (⟨ fst a ∈ˢ fst K ⟩ × ⟨ fst b ∈ˢ fst K ⟩ × (e ≡ pr (fst a) (fst b))) ∥₁
内向きには、K の任意の二つの要素の順序対が prodL K に属します。これは分出された関係そのものの導入規則です。
prodL-in : (K a b : S) → ⟨ fst a ∈ˢ fst K ⟩ → ⟨ fst b ∈ˢ fst K ⟩ → ⟨ pr (fst a) (fst b) ∈ˢ fst (prodL K) ⟩ prodL-in K a b ma mb = Product.into K a b ma mb (ma , mb)
外向きには、prodL K の要素は、切り詰められた形で K の二つの要素と対の等式から来ます。K の小さな提示に対しては、切り詰めのないより強い主張も使えます。積のすべての要素は、K の二つの添字が名指す要素の順序対なのです。
prodL-out : (K e : S) → ⟨ fst e ∈ˢ fst (prodL K) ⟩ → InProd K (fst e) prodL-out K e h = PT.map (λ { (a , b , q , ma , mb) → a , b , ma , mb , q }) (Product.out K e h) prodL-fst : (K e : S) → ⟨ fst e ∈ˢ fst (prodL K) ⟩ → Σ[ a ∈ ⟪ fst K ⟫ ] Σ[ b ∈ ⟪ fst K ⟫ ] (fst e ≡ pr (⟪ fst K ⟫↪ a) (⟪ fst K ⟫↪ b))
証明は、切り詰められた証人を K の索引のファイバーへ変換し、対の等式をファイバー自身の同定に沿って修復します。その同定は、K の各要素がまさにその索引の名指す集合であることを述べます。
prodL-fst K e h = PT.rec isPropFib (λ { (a , b , ma , mb , q) → fiber (fst K) ma .fst , fiber (fst K) mb .fst , q ∙ cong₂ pr (sym (fiber (fst K) ma .snd)) (sym (fiber (fst K) mb .snd)) }) (prodL-out K e h)
第二成分は一意です。順序対の単射性が名指された集合の等式を取り出し、K の索引の単射性がそれを添字の等式へ変えます。
where inner : (a : ⟪ fst K ⟫) → isProp (Σ[ b ∈ ⟪ fst K ⟫ ] (fst e ≡ pr (⟪ fst K ⟫↪ a) (⟪ fst K ⟫↪ b))) inner a (b , q) (b' , q') = Σ≡Prop (λ _ → setIsSet _ _) (↪-inj {a = fst K} (pr-inj (sym q ∙ q') .snd))
第一成分も同じ理由で一意であり、したがってファイバーの主張全体が命題になります。
isPropFib : isProp (Σ[ a ∈ ⟪ fst K ⟫ ] Σ[ b ∈ ⟪ fst K ⟫ ] (fst e ≡ pr (⟪ fst K ⟫↪ a) (⟪ fst K ⟫↪ b))) isPropFib (a , b , q) (a' , b' , q') = Σ≡Prop inner (↪-inj {a = fst K} (pr-inj (sym q ∙ q') .fst))
論理式としての Gödel 順序
切り詰めのない読みはどの選択にも依存しません。積を手にしたところで、順序が登場します。MaxIs は、a と b が順序数であるとき、m がそれらの最大値であることを述べます。
MaxIs : S → S → S → Type (ℓ-suc ℓ)
定義は二つの選択肢を提示します。a が b に属し m が b であるか、a の b への所属が反証され m が a であるか。切り詰められるのはこの選言だけです。定義は、どちらかの選択肢が成り立つと主張するだけで、どちらかを判定しないからです。順序数の上では排中律が分枝を選び、選ばれた m が a と b の最大値になります。
MaxIs m a b = ∥ (⟨ fst a ∈ˢ fst b ⟩ × (fst m ≡ fst b)) ⊎ ((⟨ fst a ∈ˢ fst b ⟩ → Empty.⊥) × (fst m ≡ fst a)) ∥₁
二つの対の Gödel 比較も同じく切り詰めの下のデータです。第一の対の最大値 m が第二の対の最大値 n に属するか、二つの最大値が等しいときは辞書式に比較します。第一座標どうし、ついで第二座標どうしです。
OrdIs : S → S → S → S → S → S → Type (ℓ-suc ℓ) OrdIs m n a b c d = ∥ ⟨ fst m ∈ˢ fst n ⟩ ⊎ ((fst m ≡ fst n) × ∥ ⟨ fst a ∈ˢ fst c ⟩ ⊎ ((fst a ≡ fst c) × ⟨ fst b ∈ˢ fst d ⟩) ∥₁) ∥₁
最大値は有界な論理式として書けます。a が b に属するとき m は b に等しく、a の b への所属が反証されるとき a に等しい。否定が第二の選択肢を守られた分枝として立てます。a と b が順序数であるとき、この論理式が述べるのはまさに、m がそれらの最大値であることです。
maxAt : ∀ {k} → Fin k → Fin k → Fin k → Formula S k maxAt m a b = ((var a ∈̇ var b) ∧̇ (var m ≐ var b)) ∨̇ ((¬̇ (var a ∈̇ var b)) ∧̇ (var m ≐ var a))
Gödel の比較も同じやり方で書けます。その優先順位は明示的です。まず最大値を比較し、最大値が等しいときは第一座標を比較し、第一座標も等しいときには第二座標を比較します。
ordAt : ∀ {k} → Fin k → Fin k → Fin k → Fin k → Fin k → Fin k → Formula S k ordAt m n a b c d = (var m ∈̇ var n) ∨̇ ((var m ≐ var n) ∧̇ ((var a ∈̇ var c) ∨̇ ((var a ≐ var c) ∧̇ (var b ∈̇ var d))))
部品を合わせると、Lt p q は次のように述べます。p と q は符号化された対であり、それぞれ要素 a、b と要素 c、d からなり、その最大値 m と n は最大値の条件を満たし、その比較は Gödel の条件を満たす、と。六つの証人は切り詰めの下に記録されます。条件が主張するのは証人の存在だけであり、古典的な場合分けが選択肢の中から選ぶのはその後です。
Lt : V ℓ → V ℓ → Type (ℓ-suc ℓ) Lt p q = ∥ Σ[ a ∈ S ] Σ[ b ∈ S ] Σ[ c ∈ S ] Σ[ d ∈ S ] Σ[ m ∈ S ] Σ[ n ∈ S ] ( (p ≡ pr (fst a) (fst b)) × (q ≡ pr (fst c) (fst d)) × MaxIs m a b × MaxIs n c d × OrdIs m n a b c d ) ∥₁
六つの束縛子には、呼び出し側の環境を超える六つのスロットが要り、↑6 は添字をちょうどその数だけずらします。
private ↑6 : ∀ {k} → Fin k → Fin (suc (suc (suc (suc (suc (suc k)))))) ↑6 i = suc (suc (suc (suc (suc (suc i)))))
六つのスロットには i0 から i5 までの名前が付き、量化された証人ごとに一つです。最初の三つの別名は位置 0、1、2 を束縛し、そこには第二の対の最大値、第一の対の最大値、第二の対の第二座標が入ります。
i0 : ∀ {k} → Fin (suc k) i0 = zero i1 : ∀ {k} → Fin (suc (suc k)) i1 = suc zero i2 : ∀ {k} → Fin (suc (suc (suc k)))
別名は続きます。位置 2 には第二の対の第二座標が、位置 3 にはその第一座標が、位置 4 には第一の対の第二座標が入ります。
i2 = suc (suc zero) i3 : ∀ {k} → Fin (suc (suc (suc (suc k)))) i3 = suc (suc (suc zero)) i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k))))) i4 = suc (suc (suc (suc zero)))
位置 5 は第一の対の第一座標であり、六つがそろいます。ついで順序の論理式が始まります。六つの証人を順に束縛し、p と q について Gödel の比較の要求する内容を述べるのです。
i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k)))))) i5 = suc (suc (suc (suc (suc zero)))) opaque ltAt : ∀ {k} → Fin k → Fin k → Formula S k ltAt p q = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (
本体は六つの証人を順に束縛し、五つの原子を連言します。p は第五と第四のスロットの順序対、q は第三と第二のスロットの順序対であり、第一の最大値の原子は p の座標を、第二の最大値の原子は q の座標を結び、順序の原子が二つの最大値を、ついで座標を比較します。六スロットの文脈で読めば、これはまさに、Gödel 順序において p が q より下であることを述べています。
prAtL (↑6 p) i5 i4 ∧̇ (prAtL (↑6 q) i3 i2 ∧̇ (maxAt i1 i5 i4 ∧̇ (maxAt i0 i3 i2 ∧̇ ordAt i1 i0 i5 i4 i3 i2)))))))))
妥当性は、具体的な六項目の文脈に対して確かめられます。この文脈は、呼び出し側の環境に六つの証人を新しいものから順に加えたもの、すなわち n、m、d、c、b、a であり、スロット 0 が n、スロット 5 が a となって別名と一致します。
private env : ∀ {k} → S ^ k → S → S → S → S → S → S → S ^ (suc (suc (suc (suc (suc (suc k)))))) env γ a b c d m n = n ∷ m ∷ d ∷ c ∷ b ∷ a ∷ γ
最初の妥当性の補題は、その文脈で対の原子を読みます。対の原子の充足は、呼び出し側の p と a、b の順序対との間の等式です。
atP : ∀ {k} (p : Fin k) (γ : S ^ k) (a b c d m n : S) → ⟨ env γ a b c d m n ⊨ prAtL (↑6 p) i5 i4 ⟩ ≡ (fst (lookup p γ) ≡ pr (fst a) (fst b)) atP p γ a b c d m n = cong ⟨_⟩ (prAtL-adequate (↑6 p) i5 i4 (env γ a b c d m n))
第二は q と c、d の順序対について同じことをします。この二つの同定により、論理式の充足と Lt の六証人のデータは互いに取り替えられます。
atQ : ∀ {k} (q : Fin k) (γ : S ^ k) (a b c d m n : S) → ⟨ env γ a b c d m n ⊨ prAtL (↑6 q) i3 i2 ⟩ ≡ (fst (lookup q γ) ≡ pr (fst c) (fst d)) atQ q γ a b c d m n = cong ⟨_⟩ (prAtL-adequate (↑6 q) i3 i2 (env γ a b c d m n))
外向きの方向は、六重に入れ子になった切り詰めを順に消費します。γ での ltAt p q の充足から、証人 a から n までと、対の等式、二つの最大値のデータ、そして順序のデータが得られます。
lt-out : ∀ {k} (p q : Fin k) (γ : S ^ k) → ⟨ γ ⊨ ltAt p q ⟩ → Lt (fst (lookup p γ)) (fst (lookup q γ)) lt-out p q γ = PT.rec squash₁ (λ { (a , ha) → PT.rec squash₁ (λ { (b , hb) → PT.rec squash₁ (λ { (c , hc) → PT.rec squash₁ (λ { (d , hd) → PT.rec squash₁ (λ { (m , hm) → PT.rec squash₁ (λ { (n , (hp , (hq , (hM , (hN , hO))))) →
二つの対の等式は妥当性のパスに沿って輸送され、第一の最大値のデータは周囲のレベルへ運ばれます。六つの存在の証人は持ち上げられた意味の水準に住むので、肯定の場合はそのまま残り、反証の場合は持ち上げの外へ降ろされます。
∣ a , b , c , d , m , n , ( transport (atP p γ a b c d m n) hp , transport (atQ q γ a b c d m n) hq , PT.map (λ { (inl h) → inl h ; (inr (n , e)) → inr ((λ k → lower (n k)) , e) }) hM
第二の最大値のデータも同じやり方で写され、呼び出し側の p と q における Lt の証人がそろいます。
, PT.map (λ { (inl h) → inl h ; (inr (n , e)) → inr ((λ k → lower (n k)) , e) }) hN , hO ) ∣₁ }) hm }) hd }) hc }) hb }) ha })
内向きの方向は、Lt を充足の主張へ変えます。主張は命題です。
lt-in : ∀ {k} (p q : Fin k) (γ : S ^ k) → Lt (fst (lookup p γ)) (fst (lookup q γ)) → ⟨ γ ⊨ ltAt p q ⟩ lt-in p q γ = PT.rec (snd (γ ⊨ ltAt p q)) (λ { (a , b , c , d , m , n , (ep , eq' , hM , hN , hO)) → ∣ a , ∣ b , ∣ c , ∣ d , ∣ m , ∣ n
六つの証人は入れ子の存在証人として再び入れられ、対の等式は妥当性のパスに沿って逆向きに輸送されます。
, ( transport (sym (atP p γ a b c d m n)) ep , ( transport (sym (atQ q γ a b c d m n)) eq' , ( PT.map (λ { (inl h) → inl h ; (inr (n , e)) → inr ((λ k → lift (n k)) , e) }) hM , ( PT.map (λ { (inl h) → inl h
二つの最大値のデータは今度は対象レベルの守られた原子へ持ち上げて写され、順序のデータが論理式を閉じます。Gödel のモジュールはついで、集合 P のためのこの順序をまとめます。その記述の条件は、二つの座標がともに P の要素であることを要求し、順序の論理式で両者を結びます。
; (inr (n , e)) → inr ((λ k → lift (n k)) , e) }) hN , hO )))) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ }) private module Godel (P : S) = Relation P P ((var (suc zero) ∈̇ con P) ∧̇ ((var zero ∈̇ con P) ∧̇ ltAt (suc zero) zero))
ホスト側の読みは、両側に P への所属を加え、順序の関係と連言します。二つの方向は、二つの束縛子の占めるスロットで、外向きと内向きの補題を引用します。第一座標が外側のスロット、第二座標が内側のスロットです。
(λ p q → (fst p ∈ˢ fst P) ⊓ ((fst q ∈ˢ fst P) ⊓ (Lt (fst p) (fst q) , squash₁))) (λ p q e h → h .fst , h .snd .fst , lt-out (suc zero) zero (q ∷ p ∷ e ∷ []) (h .snd .snd)) (λ p q e h → h .fst , h .snd .fst , lt-in (suc zero) zero (q ∷ p ∷ e ∷ []) (h .snd .snd))
godel P がその分出された関係です。L の内部における、P の要素からなる順序対のうち、Gödel 順序で互いに下にあるものの集合です。
godel : S → S godel = Godel.rel
内向きには、P の二つの要素 p と q について、p が q より下なら、その順序対は godel P に属します。
godel-in : (P p q : S) → ⟨ fst p ∈ˢ fst P ⟩ → ⟨ fst q ∈ˢ fst P ⟩ → Lt (fst p) (fst q) → ⟨ pr (fst p) (fst q) ∈ˢ fst (godel P) ⟩ godel-in P p q mp mq l = Godel.into P p q mp mq (mp , mq , l)
外向きには、godel P の要素には二つの要素とその間の順序のデータが伴います。
godel-out : (P p q : S) → ⟨ pr (fst p) (fst q) ∈ˢ fst (godel P) ⟩ → ⟨ fst p ∈ˢ fst P ⟩ × ⟨ fst q ∈ˢ fst P ⟩ × Lt (fst p) (fst q) godel-out = Godel.pair-out
ホスト側の順序への移送
順序のモジュールはついで、平方律が述べられる場合である順序数 κ を固定します。
module Order (κ : S) (oκ : IsOrd (fst κ)) where
K は順序数 κ の基底集合です。平方律が展開される台は、まさに κ 以下の順序数からなるこの集合です。
K : V ℓ K = fst κ
↑ は、小さな提示の埋め込みを通して、K の要素を周囲で名指します。各添字はそれが提示する順序数を指すのです。
↑ : ⟪ K ⟫ → V ℓ ↑ = ⟪ K ⟫↪
添字 m : ⟪ K ⟫ は周囲の集合 ↑ m を名指し、それが κ に属する証明を伴います。構成可能性は要素へ受け継がれるので、upK m はこの名指された順序数を L の要素としてまとめます。
upK : ⟪ K ⟫ → S upK m = ↑ m , isL-trans {x = K} {y = ↑ m} (member K m) (snd κ)
比較される順序の台は Pair、すなわち κ の二つの添字の型です。ホスト側の順序対であり、各座標は κ より下の順序数を名指します。
Pair : Type ℓ Pair = ⟪ K ⟫ × ⟪ K ⟫
座標そのものの上には座標の順序 ≺₁ が立っています。外部の平方律の構成から引用されたもので、κ より下の順序数を、それらが名指す周囲の集合どうしの所属によって狭義に比較します。
_≺₁_ : ⟪ K ⟫ → ⟪ K ⟫ → Type (ℓ-suc ℓ) _≺₁_ = SQ._≺₁_ K oκ
順序対の上には Gödel 順序 ≺ₚ が立ちます。まず最大値を比べ、ついで第一座標、最後に第二座標を比べるものです。内部の論理式が再現すべき外部の順序はこれです。
_≺ₚ_ : Pair → Pair → Type (ℓ-suc ℓ) _≺ₚ_ = SQ._≺_ K oκ
最大値の演算 maxOrd は、κ より下の二つの順序数に対して大きい方を返します。これも外部の構成からの引用であり、やはり要素が順序数であるからこそ最大値として読めるのです。
maxOrd : ⟪ K ⟫ → ⟪ K ⟫ → ⟪ K ⟫ maxOrd = SQ.maxOrd K oκ
二つの小さな事実が、両側の比較の準備をします。第一に、順序数 κ の各要素はそれ自身順序数であり、名指された順序数は順序数性の証明を帯びます。第二に、max-out は、基底の集合が a' と b' を名指す要素の上で読んだ内部の最大値の条件が、内部の最大値をちょうど a' と b' のホストの最大値に強いることを述べます。証明はホストの順序の三分法のデータに沿って進みます。
ord↑ : (m : ⟪ K ⟫) → IsOrd (↑ m) ord↑ m = mem-ord {A = K} oκ (↑ m) (member K m) max-out : (a b m : S) (a' b' : ⟪ K ⟫) → fst a ≡ ↑ a' → fst b ≡ ↑ b' → MaxIs m a b → fst m ≡ ↑ (maxOrd a' b') max-out a b m a' b' ea eb = PT.rec (setIsSet _ _) (go (SQ.tri₁ K oκ a' b'))
場合分けの関数が、この議論の形を固定します。ホストの三分法は下・等しい・上に分かれ、内部のデータは肯定の場合 (m が b) と反証の場合 (m が a) に分かれます。二つの場合分けを項ごとに合わせることが内容のすべてです。
where go : (t : TriW (a' ≺₁ b') (a' ≡ b') (b' ≺₁ a')) → (⟨ fst a ∈ˢ fst b ⟩ × (fst m ≡ fst b)) ⊎ ((⟨ fst a ∈ˢ fst b ⟩ → Empty.⊥) × (fst m ≡ fst a)) → fst m ≡ ↑ (SQ.maxGo K oκ a' b' t)
下の場合、肯定の分枝は m と b の等式に b の名指しを合成してホストの最大値を与えます。その反証の分枝は不可能です。反証されている所属は、まさに三分法の証人であり、二つの名指しを通して輸送されるだけだからです。
go (lt h) (inl (_ , e)) = e ∙ eb go (lt h) (inr (na , _)) = Empty.rec (na (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) (sym ea) (sym eb) h)) go (eq p) (inl (a∈b , _)) = Empty.rec (∈-irrefl (↑ b')
等しい場合、肯定の分枝は a が b の内側にあると置きますが、ホストは両者を等しいと宣言しており、名指された順序数 b における所属の非反射性と矛盾します。反証の分枝は、最大値を a と名指し、a の名指しに沿って輸送します。
(subst2 (λ x y → ⟨ x ∈ˢ y ⟩) (ea ∙ cong ↑ p) eb a∈b)) go (eq p) (inr (_ , e)) = e ∙ ea go (gt h) (inl (a∈b , _)) = Empty.rec (∈-irrefl (↑ a') (ord↑ a' .fst {x = ↑ b'} {y = ↑ a'}
上の場合、ホストの証人は b ∈ a を与えます。内部でも肯定の枝を取ると a ∈ b も得られ、推移性によって a での非反射性に反します。
(subst2 (λ x y → ⟨ x ∈ˢ y ⟩) ea eb a∈b) h)) go (gt h) (inr (_ , e)) = e ∙ ea
逆の max-in は、ホストの最大値を内部の述語の中に書き込みます。添字の各対に対して、maxOrd が名指す持ち上げられた要素が、持ち上げられた二つの座標で MaxIs を満たします。
max-in : (a' b' : ⟪ K ⟫) → MaxIs (upK (maxOrd a' b')) (upK a') (upK b') max-in a' b' = go (SQ.tri₁ K oκ a' b') where go : (t : TriW (a' ≺₁ b') (a' ≡ b') (b' ≺₁ a')) → MaxIs (upK (SQ.maxGo K oκ a' b' t)) (upK a') (upK b')
その三つの場合はホストの比較から直ちに従います。下では肯定の分枝に等式が定義的に付随し、等しい場合は非反射性によって所属が退けられ、上ではその座標自身の順序数性を通して退けられます。同じブロックでは code、すなわちホストの対の二つの名指された順序数の周囲の順序対が定義されます。
go (lt h) = ∣ inl (h , refl) ∣₁ go (eq p) = ∣ inr ((λ h → ∈-irrefl (↑ b') (subst (λ w → ⟨ ↑ w ∈ˢ ↑ b' ⟩) p h)) , refl) ∣₁ go (gt h) = ∣ inr ((λ h' → ∈-irrefl (↑ a') (ord↑ a' .fst {x = ↑ b'} {y = ↑ a'} h' h)) , refl) ∣₁ code : Pair → V ℓ code p = pr (↑ (fst p)) (↑ (snd p))
移送の核心は反証の補題です。ここでは矛盾の形をしたデータの対を仮定します。p と q の符号化された対の上で Lt が成り立ちながら、ホストの順序はその比較を拒むのです。こうして仮定された Lt の六つの証人が、一つの矛盾の主張にまとめられます。
private refute : (p q : Pair) → (p ≺ₚ q → Empty.⊥) → Σ[ a ∈ S ] Σ[ b ∈ S ] Σ[ c ∈ S ] Σ[ d ∈ S ] Σ[ m ∈ S ] Σ[ n ∈ S ] ( (code p ≡ pr (fst a) (fst b)) × (code q ≡ pr (fst c) (fst d)) × MaxIs m a b × MaxIs n c d × OrdIs m n a b c d )
結論は空の型です。仮定された順序のデータと拒まれた比較は共存できません。証明は六つの証人を分解し、それらの名指す基底の集合の上で作業します。
→ Empty.⊥ refute (a' , b') (c' , d') nk (a , b , c , d , m , n , (ep , eq' , hM , hN , hO)) = PT.rec Empty.isProp⊥ outer hO where ea : fst a ≡ ↑ a'
順序対の単射性が、各符号化の等式から、証人の基底集合と対応する名指された順序数の同定を取り出します。この四つの等式が、後のすべての比較の錨となります。
ea = sym (pr-inj ep .fst) eb : fst b ≡ ↑ b' eb = sym (pr-inj ep .snd) ec : fst c ≡ ↑ c' ec = sym (pr-inj eq' .fst)
二つの最大値は、二つの最大値のデータに max-out を適用して、ホストの最大値と同一視されます。ここで構成全体の内部の読みと外部の読みは、六つの座標のすべてで一致します。
ed : fst d ≡ ↑ d' ed = sym (pr-inj eq' .snd) em : fst m ≡ ↑ (maxOrd a' b') em = max-out a b m a' b' ea eb hM en : fst n ≡ ↑ (maxOrd c' d')
等式 en は第二の対にも同じ同定を与えるので、OrdIs をホストの最大値と座標へすべて輸送できるようになります。
en = max-out c d n c' d' ec ed hN
内側の補題は座標の比較を移送します。名指された第一座標の間の周囲の所属は、二つの名指しの同定に沿って輸送されると、ホストの順序での下関係になります。
inner : ⟨ fst a ∈ˢ fst c ⟩ ⊎ ((fst a ≡ fst c) × ⟨ fst b ∈ˢ fst d ⟩) → (a' ≺₁ c') ⊎ ((a' ≡ c') × (b' ≺₁ d')) inner (inl h) = inl (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) ea ec h) inner (inr (e , h)) = inr ( ↪-inj {a = K} (sym ea ∙ e ∙ ec)
相等の場合も同じく伝わります。名指された集合の等式を二つの名指しの間で巡らせると、K の名指しの単射性によって添字の等式になり、第二座標は従来どおり比較されます。
, subst2 (λ x y → ⟨ x ∈ˢ y ⟩) eb ed h )
第一の最大値が第二の最大値に属するなら、この所属を em と en に沿って輸送すると p ≺ₚ q の最大値が真に小さい枝が得られ、nk と矛盾します。
outer : ⟨ fst m ∈ˢ fst n ⟩ ⊎ ((fst m ≡ fst n) × ∥ ⟨ fst a ∈ˢ fst c ⟩ ⊎ ((fst a ≡ fst c) × ⟨ fst b ∈ˢ fst d ⟩) ∥₁) → Empty.⊥ outer (inl h) = nk (inl (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) em en h))
二つの最大値が等しいなら、基底集合の等式が名指しの単射性によって添字の等式になり、内側の補題がホストの順序の中で二つの対を比較して、再び拒否を退けます。
outer (inr (e , h)) = PT.rec Empty.isProp⊥ (λ w → nk (inr (↪-inj {a = K} (sym em ∙ e ∙ en) , inner w))) h
lt→≺ の証明では、ホストの対の三分法から三つの場合が生じます。求める狭義の枝はそのまま返せます。相等または逆向きの狭義の枝では、p ≺ₚ q を否定すると refute により仮定した Lt と矛盾するので、やはり求める比較が得られます。
lt→≺ : (p q : Pair) → Lt (code p) (code q) → p ≺ₚ q lt→≺ p q l = go (SQ.tri≺ K oκ p q) where refuted : ((p ≺ₚ q) → Empty.⊥) → p ≺ₚ q refuted nk = Empty.rec (PT.rec Empty.isProp⊥ (refute p q nk) l)
相等の場合、仮定した p ≺ₚ q は q ≺ₚ q へ輸送され、非反射性に反します。逆向きの狭義の場合、その仮定した比較を q ≺ₚ p と合成すると p ≺ₚ p が得られ、やはり不可能です。
go : TriW (p ≺ₚ q) (p ≡ q) (q ≺ₚ p) → p ≺ₚ q
go (lt k) = k
go (eq e) = refuted (λ k → SQ.irr≺ K oκ q (subst (λ w → w ≺ₚ q) e k))
go (gt h) = refuted (λ k → SQ.irr≺ K oκ p (SQ.trans≺ K oκ p q p k h))
逆の ≺→lt は、ホストの比較を対象言語の中に書き込みます。六つの証人は持ち上げられた座標と二つの持ち上げられた最大値であり、対の等式は定義的に成り立ち、最大値のデータは max-in が、順序のデータはホストの比較そのものが供給します。
≺→lt : (p q : Pair) → p ≺ₚ q → Lt (code p) (code q) ≺→lt (a' , b') (c' , d') k = ∣ upK a' , upK b' , upK c' , upK d' , upK (maxOrd a' b') , upK (maxOrd c' d') , ( refl , refl , max-in a' b' , max-in c' d' , ord k ) ∣₁ where
順序のデータは場合ごとに読まれます。狭義の所属はそのまま通り、相等の二つの場合は、最大値の名指しおよび座標の名指しに沿ってそれぞれ輸送されます。
ord : (a' , b') ≺ₚ (c' , d') → OrdIs (upK (maxOrd a' b')) (upK (maxOrd c' d')) (upK a') (upK b') (upK c') (upK d') ord (inl h) = ∣ inl h ∣₁ ord (inr (e , inl h)) = ∣ inr (cong ↑ e , ∣ inl h ∣₁) ∣₁ ord (inr (e , inr (f , h))) = ∣ inr (cong ↑ e , ∣ inr (cong ↑ f , h) ∣₁) ∣₁
x < y なら y < z との推移性から x < z を得ます。x = y なら、与えられた y < z をその等式に沿って輸送します。
private ≤→≺ : (x y z : ⟪ K ⟫) → SQ._≤₁_ K oκ x y → y ≺₁ z → x ≺₁ z ≤→≺ x y z (inl h) h' = SQ.trans₁ K oκ x y z h h' ≤→≺ x y z (inr e) h' = subst (λ w → w ≺₁ z) (sym e) h'
対になる補題は、x ≤ y と y = y' から、x が y' の後続に属することを導きます。狭義の場合は x ∈ y' から後続への所属が直接従います。等しい場合は x を y' と同一視すると、主張は y' が自身の後続に属することへ帰着します。
≤→∈suc : (x y y' : ⟪ K ⟫) → SQ._≤₁_ K oκ x y → y ≡ y' → ⟨ ↑ x ∈ˢ sucV (↑ y') ⟩ ≤→∈suc x y y' (inl h) e = ∈sucV-inl (subst (λ w → x ≺₁ w) e h) ≤→∈suc x y y' (inr q) e = subst (λ w → ⟨ ↑ w ∈ˢ sucV (↑ y') ⟩) (sym (q ∙ e)) (self∈sucV (↑ y'))
節の補題がここで順序から読み取られます。対 r が対 p より下なら、r の第一座標は p の最大値の後続の要素です。最大値が真に比較される場合は、たかだかの関係に続いて狭義の比較が行われます。
fst∈suc : (r p : Pair) → r ≺ₚ p → ⟨ ↑ (fst r) ∈ˢ sucV (↑ (maxOrd (fst p) (snd p))) ⟩ fst∈suc (a , b) (c , d) (inl h) = ∈sucV-inl (≤→≺ a (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .fst) h) fst∈suc (a , b) (c , d) (inr (e , _)) =
最大値が等しい場合は、第一座標は共有された最大値を超えず、二つの最大値は同一視されるので、所属は最大値がみずからの後続に属することから従います。
≤→∈suc a (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .fst) e
同じ議論を第二座標に適用すると snd∈suc が得られます。r の第二座標もまた、二つの最大値が狭義に比較される場合にも、等しい場合にも、p の最大値の後続に収まります。
snd∈suc : (r p : Pair) → r ≺ₚ p → ⟨ ↑ (snd r) ∈ˢ sucV (↑ (maxOrd (fst p) (snd p))) ⟩ snd∈suc (a , b) (c , d) (inl h) = ∈sucV-inl (≤→≺ b (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .snd) h) snd∈suc (a , b) (c , d) (inr (e , _)) =
この二つの評価から、(c, d) の任意の先行者の両座標が suc(max(c, d)) に属することが分かります。
≤→∈suc b (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .snd) e module Coll (κ : S) (oκ : IsOrd (fst κ)) where
これらの評価は Gödel 順序の各先行者切片を制御します。整礎性と推移性を合わせると、prodL κ 上の関係を順序数としての順序型へ崩壊できる状況が得られます。
open Order κ oκ
順序型へ崩壊される集合は P、すなわち積です。順序数 κ の要素の順序対の集合であり、すでに L の内部で分出されています。
P : S P = prodL κ
崩壊に用いられる関係は R、つまりその積の上の Gödel 順序です。P の二つの要素は、一方が他方より下で比較されるときに限り関係づけられます。
R : S R = godel P
Gödel 関係では直接従います。y R x なら、y と x はともにその積の要素です。
Rsub : (y x : S) → Holds R y x → ⟨ fst y ∈ fst P ⟩ × ⟨ fst x ∈ fst P ⟩ Rsub y x h = godel-out P y x h .fst , godel-out P y x h .snd .fst
順序型の仕組みはこの積のために一度実例化されます。その定義域は崩壊の添字集合であり、φ は各添字に対して、積の対応する要素が提示するホストの対を読み取ります。二つの座標は積の提示の読みによって切り詰めなしで回収されます。
module OT = Code P R Rsub using (Dom; Dom≡; isProp≺; toDom; up; up-mem; up-toDom; ↪; _≺_; ≺-in; ≺-out; module Conjuncts) φ : OT.Dom → Pair φ m = prodL-fst κ (OT.up m) (OT.up-mem m) .fst , prodL-fst κ (OT.up m) (OT.up-mem m) .snd .fst
この読みには等式が伴います。添字の内部の符号化は、二つの座標の周囲の順序対に等しいのです。この等式が、内部の順序と外部の順序の間のすべての比較の継ぎ目です。
φ-eq : (m : OT.Dom) → OT.↪ m ≡ code (φ m) φ-eq m = prodL-fst κ (OT.up m) (OT.up-mem m) .snd .snd
φ は単射です。二つの添字が同じホストの対を名指すなら、それらの符号化は一致し、定義域みずからの基準、すなわち符号化の相等が添字の相等を返します。したがって、異なる二つの積の添字が同じホストの対へ送られることはありません。
φ-inj : (m n : OT.Dom) → φ m ≡ φ n → m ≡ n φ-inj m n e = OT.Dom≡ (φ-eq m ∙ cong code e ∙ sym (φ-eq n))
順方向の移送は、内部の順序を外向きに読みます。二つの添字が L の内部で比較されれば、それらのホストの対は Gödel 順序で比較されます。証明は定義の等式と論理式の外向きの読みを引用し、二つのホストの対の上で移送 lt→≺ を適用します。
≺-fwd : (m n : OT.Dom) → m OT.≺ n → φ m ≺ₚ φ n ≺-fwd m n k = lt→≺ (φ m) (φ n) (subst2 Lt (φ-eq m) (φ-eq n) (godel-out P (OT.up m) (OT.up n) (OT.≺-out m n k) .snd .snd))
逆方向の移送は、ホストの順序を内向きに読み、論理式の内向きの読みと、同じ二つの対の上の移送 ≺→lt を引用します。二つの方向を合わせると、崩壊の添字の上の内部の関係は、φ を通して読んだホストの Gödel 順序にほかならないと言えます。
≺-bwd : (m n : OT.Dom) → φ m ≺ₚ φ n → m OT.≺ n ≺-bwd m n k = OT.≺-in m n (godel-in P (OT.up m) (OT.up n) (OT.up-mem m) (OT.up-mem n) (subst2 Lt (sym (φ-eq m)) (sym (φ-eq n)) (≺→lt (φ m) (φ n) k)))
整礎性は添字とともに伝わります。ホストの対の到達可能性は、対応する添字の到達可能性を供給し、その先行者は前方へ、真に小さい対のホストの対へ写されます。こうして外部の順序に沿う帰納が、内部の順序に沿う帰納になります。
wf : WellFounded OT._≺_ wf m = go (SQ.wf≺ K oκ (φ m)) where go : {n : OT.Dom} → Acc _≺ₚ_ (φ n) → Acc OT._≺_ n go {n} (acc r) = acc (λ n' k → go (r (φ n') (≺-fwd n' n k)))
推移性も同じように伝わります。内部の二段階を外向きに読み、ホストの順序の推移性で合成し、a から c への一段階として内向きに読み戻します。
≺-trans : {a b c : OT.Dom} → a OT.≺ b → b OT.≺ c → a OT.≺ c ≺-trans {a} {b} {c} k k' = ≺-bwd a c (SQ.trans≺ K oκ (φ a) (φ b) (φ c) (≺-fwd a b k) (≺-fwd b c k'))
三分法が移送された一式を完成させます。任意の二つの添字に対して、ホストの三分法がそれらの対を比較します。主張は内部の比較の三方向の和として述べられます。
tri : (a b : OT.Dom) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a)) tri a b = go (SQ.tri≺ K oκ (φ a) (φ b)) where go : TriW (φ a ≺ₚ φ b) (φ a ≡ φ b) (φ b ≺ₚ φ a) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
三つの場合はそれぞれ読み戻されます。二つの狭義の場合は逆方向の移送を通り、相等の場合は φ の単射性を通って、同じホストの対を名指す添字は等しくなります。
go (lt h) = inl (≺-bwd a b h) go (eq e) = inr (inl (φ-inj a b e)) go (gt h) = inr (inr (≺-bwd b a h))
整礎性と推移性から崩壊とその順序型を構成します。
module C = OT.Conjuncts wf ≺-trans using (module Inj; col; col-ord; col-out; colTable; colTable-in; colTable-pair; colʟ; otL; otL-out) module I = C.Inj tri using (code; col-inj; module Inverse) injL-ot : InjL P C.otL injL-ot = ∣ C.colTable , I.code ∣₁
三つの計数事実
続いて三分法が崩壊写像の単射性を与えるので、そのグラフが内部単射 P ↪ C.otL を証します。
incl : (a b : V ℓ) → ((z : V ℓ) → ⟨ z ∈ˢ a ⟩ → ⟨ z ∈ˢ b ⟩) → ⟪ a ⟫ ↪ ⟪ b ⟫
計数の補題は周囲の側から始まります。二つの周囲の集合の間の包含は小さな提示の上で働きます。部分集合の各添字は大きい集合の要素を名指し、その要素の大きい提示におけるファイバーが対応する添字を名指します。
incl a b sub = ι , ι-inj where ι : ⟪ a ⟫ → ⟪ b ⟫ ι m = fiber b (sub (⟪ a ⟫↪ m) (member a m)) .fst ι-inj : (m n : ⟪ a ⟫) → ι m ≡ ι n → m ≡ n
誘導された添字の写しは単射です。部分集合の二つの添字が名指す要素が大きい提示で同じ添字によって名指されるなら、名指しの等式が名指された要素の等式を強制し、部分集合みずからの単射性が添字の等式を返します。
ι-inj m n e = ↪-inj {a = a} (sym (fiber b (sub (⟪ a ⟫↪ m) (member a m)) .snd) ∙ cong ⟪ b ⟫↪ e ∙ fiber b (sub (⟪ a ⟫↪ n) (member a n)) .snd) opaque
L 内の符号化された単射は外側で読み取れます。そのグラフ条件から、定義域と終域の小さな提示の間の単射が定まります。さらに任意の無限順序数 a に対する ω ⊆ a と合わせることで、内部単射を通常の基数比較へ結びつけます。
coded→ambient : (a b : S) → Σ[ F ∈ S ] InjCode F a b → ⟪ fst a ⟫ ↪ ⟪ fst b ⟫ coded→ambient a b (F , sv , dm , ij , ran) = Sm.small , Sm.small-inj where module Sm = Small F a b sv dm ij ran ω⊆ : (a : V ℓ) → IsOrd a → (⟨ a ∈ˢ ω ⟩ → Empty.⊥) → (z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ a ⟩
ω の包含は、順序数 a での三分法から従います。無限性の仮定により a は ω に属せず、a が ω に等しいときは所属が輸送され、ω が a の内側にあるときは推移性がすべての所属を中継します。
ω⊆ a oa a∉ω z z∈ω = go (ord-tri a oa ω ω-ord) where go : ⟨ a ∈ˢ ω ⟩ ⊎ ((a ≡ ω) ⊎ ⟨ ω ∈ˢ a ⟩) → ⟨ z ∈ˢ a ⟩ go (inl h) = Empty.rec (a∉ω h) go (inr (inl e)) = subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈ω
その最後の場合は、z ∈ ω と ω ∈ a に推移性を適用するものです。包含を手にすると、第二の計数の事実は排除となります。無限の順序数は、ω の要素、すなわち有限の順序数への内部の単射を許しません。
go (inr (inr ω∈a)) = oa .fst z∈ω ω∈a no-fin : (a b : S) → IsOrd (fst a) → (⟨ fst a ∈ˢ ω ⟩ → Empty.⊥) → IsOrd (fst b) → ⟨ fst b ∈ˢ ω ⟩ → InjL a b → Empty.⊥ no-fin a b oa a∉ω ob b∈ω = PT.rec Empty.isProp⊥ (λ c → finite-excl-ω (fst b) ob b∈ω (λ x → h c x , h c x)
反証の最後の部分は、ω が a に含まれるという事実を引用します。ω ⊆ a なので二つの補題が合成され、ω から b への単射は a を経由すると ω から有限集合 b への単射になります。包含写像 ι は where 節で一度定められます。
(λ x y e → ι .snd x y (coded→ambient a b c .snd (ι .fst x) (ι .fst y) (cong fst e)))) where ι : ⟪ ω ⟫ ↪ ⟪ fst a ⟫ ι = incl ω (fst a) (ω⊆ (fst a) oa a∉ω)
写像 h は包含 ω ↪ a の後で符号化された単射を評価します。
h : Σ[ F ∈ S ] InjCode F a b → ⟪ ω ⟫ → ⟪ fst b ⟫ h c x = coded→ambient a b c .fst (ι .fst x)
符号化された単射を直積へ持ち上げる
積上の写像を構成するため、a 上で単値であり、定義域が a、単射的で、値が b に入るグラフ F を固定します。これらが符号化された単射 a ↪ b の四条件です。
module ProdMap (a b F : S) (sv : ⟨ (F ∷ a ∷ []) ⊨ svAt zero ⟩) (dm : ⟨ (F ∷ a ∷ []) ⊨ domAt zero (suc zero) ⟩)
写像 h は包含 ω ↪ a の後で符号化された単射を評価します。積上の写像を構成するため、a 上で単値であり、定義域が a、単射的で、値が b に入るグラフ F を固定します。これらが符号化された単射 a ↪ b の四条件です。
(ij : ⟨ (F ∷ a ∷ []) ⊨ injAt zero ⟩) (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → ⟨ fst y ∈ fst b ⟩) where
抽出のモジュールは、グラフから実際の関数を読み取ります。toFun が定義域の各要素での値を計算し、toFun-graph がその対がグラフに属することを証明し、toFun-inj がグラフの単射性を関数へ移します。
module E = Extract F a sv dm using (toFun; toFun-graph; toFun-inj)
二つの述語が対象を記述します。Mem p は p が積 prodL a の要素であることを、Comp p は p が a の二つの要素 x と y に分解され、その順序対が p の基底集合に等しいことを述べます。
Mem : S → Type (ℓ-suc ℓ) Mem p = ⟨ fst p ∈ˢ fst (prodL a) ⟩ Comp : S → Type (ℓ-suc ℓ) Comp p = Σ[ x ∈ S ] Σ[ y ∈ S ] (⟨ fst x ∈ˢ fst a ⟩ × ⟨ fst y ∈ˢ fst a ⟩ × (fst p ≡ pr (fst x) (fst y)))
積の要素の成分は一意であり、isPropComp がそれを証明します。第一射影は順序対の単射性によって同一視され、第二射影は内側の補題で比較されます。
isPropComp : (p : S) → isProp (Comp p) isPropComp p (x , y , _ , _ , e) (x' , y' , _ , _ , e') = Σ≡Prop inner (Σ≡Prop (λ v → snd (isL v)) (pr-inj (sym e ∙ e') .fst)) where inner : (x : S)
内側の補題は第二成分を比較します。同じ第一座標と対にされた候補 y と y' は等しくなります。対の等式がそれらの基底集合を同じ集合と同一視し、構成可能性と所属の成分は命題だからです。
→ isProp (Σ[ y ∈ S ] (⟨ fst x ∈ˢ fst a ⟩ × ⟨ fst y ∈ˢ fst a ⟩ × (fst p ≡ pr (fst x) (fst y)))) inner x (y , _ , _ , e) (y' , _ , _ , e') = Σ≡Prop (λ w → isProp× (snd (fst x ∈ˢ fst a)) (isProp× (snd (fst w ∈ˢ fst a)) (setIsSet _ _)))
最後の成分は基底集合の相等によって処理され、一意性が完成します。Comp p は命題なので、切り詰められた存在は実際の分解へ消去できます。
(Σ≡Prop (λ v → snd (isL v)) (pr-inj (sym e ∙ e') .snd))
読み comp は、積の切り詰められた所属を実際の分解へ変えます。その消去を許すのは、証明されたばかりの一意性です。そして値の写像 val が、a の各要素 x に対して、符号化された単射 F が割り当てる要素を計算します。
comp : (p : S) → Mem p → Comp p comp p mp = PT.rec (isPropComp p) (λ z → z) (prodL-out a p mp) opaque val : (x : S) → ⟨ fst x ∈ˢ fst a ⟩ → S val x mx = E.toFun (x , mx)
グラフの補題は、計算された値が入力とともにグラフの内部で対にされることを証明します。すなわち x と val x の順序対が F に属するのです。この割り当ての記録は a のすべての要素について保たれます。
val-graph : (x : S) (mx : ⟨ fst x ∈ˢ fst a ⟩)
→ ⟨ pr (fst x) (fst (val x mx)) ∈ fst F ⟩
val-graph x mx = E.toFun-graph (x , mx)
単射性の補題は、グラフの単射性を計算された値へ移します。a の二つの要素に割り当てられた値の基底集合が等しければ、要素そのものも等しいのです。これが、対の上の持ち上げられた写像を単射にする鍵です。
val-inj : (x : S) (mx : ⟨ fst x ∈ˢ fst a ⟩) (x' : S) (mx' : ⟨ fst x' ∈ˢ fst a ⟩) → fst (val x mx) ≡ fst (val x' mx') → fst x ≡ fst x' val-inj x mx x' mx' = E.toFun-inj ij (x , mx) (x' , mx')
持ち上げられた写像 fn は、積の要素に座標ごとに F を適用します。第一座標の像と第二座標の像の内部の順序対です。
fn : (p : S) → Mem p → S fn p mp = prʟ (val (comp p mp .fst) (comp p mp .snd .snd .fst)) (val (comp p mp .snd .fst) (comp p mp .snd .snd .snd .fst))
像は b の上の積の中に収まります。値域の節により二つの成分の値はともに b の要素であり、したがってその内部の対は prodL b に属します。内部の対と周囲の対の同一視は、みずからの第一射影の補題に沿って輸送されます。
into : (p : S) (mp : Mem p) → ⟨ fst (fn p mp) ∈ˢ fst (prodL b) ⟩ into p mp = subst (λ w → ⟨ w ∈ˢ fst (prodL b) ⟩) (sym (prʟ-fst (val x mx) (val y my))) (prodL-in b (val x mx) (val y my) (ran x (val x mx) (val-graph x mx)) (ran y (val y my) (val-graph y my)))
p の分解は座標 x,y と、x ∈ a および y ∈ a の証明を同時に与えます。val は a の要素についてのみ定義されるため、これらの所属証明もデータの一部です。
where x = comp p mp .fst y = comp p mp .snd .fst mx = comp p mp .snd .snd .fst my = comp p mp .snd .snd .snd .fst
連鎖の型は、グラフの論理式が証明すべき内容をまとめます。p は x と y の対、q は x' と y' の対であり、F のグラフには二つの第一座標の対と二つの第二座標の対が含まれるのです。
Chain : S → S → S → S → S → S → Type (ℓ-suc ℓ) Chain q p x y x' y' = (fst p ≡ pr (fst x) (fst y)) × (fst q ≡ pr (fst x') (fst y')) × ⟨ pr (fst x) (fst x') ∈ fst F ⟩ × ⟨ pr (fst y) (fst y') ∈ fst F ⟩
グラフの論理式 mapFo は x,y,x',y' を存在量化し、p=(x,y)、q=(x',y')、および F の二つの適用という四つの主張を連言します。
opaque mapFo : Formula S 2 mapFo = ∃̇ (∃̇ (∃̇ (∃̇ ( prAtL i5 i3 i2 ∧̇ (prAtL i4 i1 i0
最後の二つの原子は適用の節です。F のグラフには第一座標どうしの対と第二座標どうしの対が含まれ、これはまさに、F が x を x' へ、y を y' へ写すということです。
∧̇ (appC F i3 i1 ∧̇ appC F i2 i0))))))
妥当性は、具体的な六項目の文脈に対して確かめられます。四つの証人を新しいものから順に加え、対 q と対 p を続けた文脈であり、スロット 0 が y'、スロット 5 が p となって四つの原子の添字と一致します。
private env₄ : S → S → S → S → S → S → S ^ 6 env₄ q p x y x' y' = y' ∷ x' ∷ y ∷ x ∷ q ∷ p ∷ []
最初の妥当性の補題は p の対の原子を読みます。文脈における対の原子の充足は、p の基底集合と x、y の順序対との間の等式です。
at1 : (q p x y x' y' : S) → ⟨ env₄ q p x y x' y' ⊨ prAtL i5 i3 i2 ⟩ ≡ (fst p ≡ pr (fst x) (fst y)) at1 q p x y x' y' = cong ⟨_⟩ (prAtL-adequate i5 i3 i2 (env₄ q p x y x' y'))
第二の妥当性の補題は、証人 x' と y' に対して q について同じことをします。この二つの等式が、連鎖の対の部分の錨です。
at2 : (q p x y x' y' : S) → ⟨ env₄ q p x y x' y' ⊨ prAtL i4 i1 i0 ⟩ ≡ (fst q ≡ pr (fst x') (fst y')) at2 q p x y x' y' = cong ⟨_⟩ (prAtL-adequate i4 i1 i0 (env₄ q p x y x' y'))
三つ目の妥当性の補題は第一の適用の原子を読みます。L での充足は、二つの第一座標の対の F のグラフへの周囲の所属と同一視されます。
at3 : (q p x y x' y' : S) → ⟨ env₄ q p x y x' y' ⊨ appC F i3 i1 ⟩ ≡ ⟨ pr (fst x) (fst x') ∈ fst F ⟩ at3 q p x y x' y' = cong ⟨_⟩ (appC-adequate F i3 i1 (env₄ q p x y x' y'))
四つ目は第二座標に対して同じことをし、四つの原子のすべてが、集合の要素についての通常の主張へ翻訳されます。
at4 : (q p x y x' y' : S) → ⟨ env₄ q p x y x' y' ⊨ appC F i2 i0 ⟩ ≡ ⟨ pr (fst y) (fst y') ∈ fst F ⟩ at4 q p x y x' y' = cong ⟨_⟩ (appC-adequate F i2 i0 (env₄ q p x y x' y'))
外向きの方向は、四重に入れ子になった存在量化を順に消費し、切り詰められた連鎖を組み立てます。四つの証人と、周囲の読みへ輸送された四つの原子です。
mapFo-out : (q p : S) → ⟨ (q ∷ p ∷ []) ⊨ mapFo ⟩ → ∥ Σ[ x ∈ S ] Σ[ y ∈ S ] Σ[ x' ∈ S ] Σ[ y' ∈ S ] Chain q p x y x' y' ∥₁ mapFo-out q p = PT.rec squash₁ (λ { (x , hx) → PT.rec squash₁ (λ { (y , hy) → PT.rec squash₁ (λ { (x' , hx') → PT.map (λ { (y' , (h1 , (h2 , (h3 , h4)))) → x , y , x' , y'
各原子はみずからの妥当性のパスに沿って輸送されるため、連鎖が記録するのは充足の判断ではなく、通常の等式と通常の所属です。
, ( transport (at1 q p x y x' y') h1 , transport (at2 q p x y x' y') h2 , transport (at3 q p x y x' y') h3 , transport (at4 q p x y x' y') h4 ) }) hx' }) hy }) hx })
内向きの方向は、連鎖から論理式を組み立て直します。四つの証人を入れ子の存在量化の証人として入れ、四つの原子を妥当性のパスに沿って逆向きに輸送します。
mapFo-in : (q p x y x' y' : S) → Chain q p x y x' y' → ⟨ (q ∷ p ∷ []) ⊨ mapFo ⟩ mapFo-in q p x y x' y' (h1 , h2 , h3 , h4) = ∣ x , ∣ y , ∣ x' , ∣ y' , ( transport (sym (at1 q p x y x' y')) h1 , ( transport (sym (at2 q p x y x' y')) h2
最後の二つの適用原子が四つの主張からなる入れ子の連言を完成させ、mapFo の証人が得られます。
, ( transport (sym (at3 q p x y x' y')) h3 , transport (sym (at4 q p x y x' y')) h4 ))) ∣₁ ∣₁ ∣₁ ∣₁
一意性は、グラフの論理式が値を定めることを述べます。グラフの中で p と対にされる任意の q は、正準な像 fn p mp に等しくなります。証明は切り詰められた連鎖を対の等式の中で消費し、目標は h-集合における等式です。
only : (p : S) (mp : Mem p) (q : S) → ⟨ (q ∷ p ∷ []) ⊨ mapFo ⟩ → q ≡ fn p mp only p mp q h = PT.rec (isSetS q (fn p mp)) step (mapFo-out q p h) where x = comp p mp .fst y = comp p mp .snd .fst
要素 p の四つの成分には、像の補題と同じように一度名前が与えられ、一意性の計算がそれらを直接参照できます。
mx = comp p mp .snd .snd .fst my = comp p mp .snd .snd .snd .fst e = comp p mp .snd .snd .snd .snd
連鎖の等式は q を (x₁',y₁') と書き、固定した分解は p を (x,y) と書きます。単値性により x₁' は val x と、y₁' は val y と同一視されるので、q は正準な像 (val x,val y) です。
step : Σ[ x₁ ∈ S ] Σ[ y₁ ∈ S ] Σ[ x₁' ∈ S ] Σ[ y₁' ∈ S ] Chain q p x₁ y₁ x₁' y₁' → q ≡ fn p mp step (x₁ , y₁ , x₁' , y₁' , (e₁ , e₂ , h3 , h4)) = Σ≡Prop (λ v → snd (isL v)) (e₂ ∙ cong₂ pr ex ey ∙ sym (prʟ-fst (val x mx) (val y my)))
順序対の単射性が対の等式を二つに分けます。x₁ の基底集合は x のそれに等しく、y₁ の基底集合は y のそれに等しいのです。
where x₁≡x : fst x₁ ≡ fst x x₁≡x = pr-inj (sym e₁ ∙ e) .fst y₁≡y : fst y₁ ≡ fst y y₁≡y = pr-inj (sym e₁ ∙ e) .snd
二つのグラフへの所属は、F の単値性を通して読まれます。x₁ が x を名指すことが分かれば、x₁ と対にされた項目の第一射影は、記録された値 val x mx と一致せざるを得ません。
ex : fst x₁' ≡ fst (val x mx) ex = svAt-out zero (F ∷ a ∷ []) sv x x₁' (val x mx) (subst (λ w → ⟨ pr w (fst x₁') ∈ fst F ⟩) x₁≡x h3) (val-graph x mx) ey : fst y₁' ≡ fst (val y my) ey = svAt-out zero (F ∷ a ∷ []) sv y y₁' (val y my)
第二座標もまったく同じように扱われ、みずからの所属と、みずからに記録された値が用いられます。
(subst (λ w → ⟨ pr w (fst y₁') ∈ fst F ⟩) y₁≡y h4) (val-graph y my)
したがって mapFo は座標ごとの像 fn を定義します。各積要素はこのグラフ値をもち、into がその値を prodL b に入れます。
M : DefinableMap M = record { dom = prodL a ; cod = prodL b ; fn = fn ; into = into ; graph = mapFo ; defines = λ p mp → mapFo-in (fn p mp) p (comp p mp .fst) (comp p mp .snd .fst)
定義の節は連鎖であり、p の正準な像のところで実例化されます。二つの値、積の要素の対の等式、そして二つのグラフの補題が、グラフが像とその入力について成り立つことを証明します。
(val (comp p mp .fst) (comp p mp .snd .snd .fst)) (val (comp p mp .snd .fst) (comp p mp .snd .snd .snd .fst)) ( comp p mp .snd .snd .snd .snd , prʟ-fst _ _ , val-graph (comp p mp .fst) (comp p mp .snd .snd .fst)
一意性定理により別のグラフ値はありえないため、この論理式は prodL a 上の実際の関数を表します。
, val-graph (comp p mp .snd .fst) (comp p mp .snd .snd .snd .fst) ) ; only = only }
持ち上げられた写像の単射性は直接証明されます。像が基底集合として等しい二つの積の要素は、それ自身も等しくなければなりません。証明は各要素をその成分から組み立て直します。
inj : (p : S) (mp : Mem p) (p' : S) (mp' : Mem p') → fst (fn p mp) ≡ fst (fn p' mp') → fst p ≡ fst p' inj p mp p' mp' e = e₀ ∙ cong₂ pr ex ey ∙ sym e₀' where x = comp p mp .fst
二つの要素の成分にはそれぞれ一度名前が与えられ、二つの分解を座標ごとに比較できます。
y = comp p mp .snd .fst mx = comp p mp .snd .snd .fst my = comp p mp .snd .snd .snd .fst e₀ = comp p mp .snd .snd .snd .snd x' = comp p' mp' .fst
仮定された像の相等は内部の対の相等であり、その単射性がそれを、第一の像どうしの相等と第二の像どうしの相等に分けます。
y' = comp p' mp' .snd .fst mx' = comp p' mp' .snd .snd .fst my' = comp p' mp' .snd .snd .snd .fst e₀' = comp p' mp' .snd .snd .snd .snd q : (fst (val x mx) ≡ fst (val x' mx')) × (fst (val y my) ≡ fst (val y' my'))
各成分の等式は値の写像の単射性に渡され、第一座標の相等と第二座標の相等が得られます。対の等式の二つの座標はこれらに沿って輸送されます。
q = pr-inj (sym (prʟ-fst (val x mx) (val y my)) ∙ e ∙ prʟ-fst (val x' mx') (val y' my')) ex : fst x ≡ fst x' ex = val-inj x mx x' mx' (fst q) ey : fst y ≡ fst y' ey = val-inj y my y' my' (snd q)
定義可能な写像とその単射性が内部の単射として組み上がります。L の内部で prodL a は prodL b へ単射します。
injL : InjL (prodL a) (prodL b) injL = Inj.injL M inj
InjL は命題的に切り詰められているため、グラフを大域的に選ばずに符号化された単射 a ↪ b を持ち上げられます。
prod-inj : (a b : S) → InjL a b → InjL (prodL a) (prodL b) prod-inj a b = PT.rec squash₁ (λ { (F , sv , dm , ij , ran) → ProdMap.injL a b F sv dm ij ran })
無限基数の平方律
無限順序数に加わる頂点を吸収するには、その後続をもとの順序数へ単射すれば十分です。
module Shift (mL : S) (om : IsOrd (fst mL)) (m∉ω : ⟨ fst mL ∈ˢ ω ⟩ → Empty.⊥) where
mL の基底にある順序数を m と書きます。所属と有限性の判定はこの集合について行い、mL はそれが L の要素である証拠を保持します。
private m : V ℓ m = fst mL
移し変えの定義域は内部の後続 D = sucʟ mL です。L の内部での順序数の後続であり、m の要素と m 自身の両方を含みます。
D : S D = sucʟ mL
L の二つの要素の相等は、その基底集合の相等です。構成可能性の成分は命題だからです。この小さな等式は、移し変えの内部のあらゆる同一視で使われます。
S≡ : {x y : S} → fst x ≡ fst y → x ≡ y S≡ = Σ≡Prop (λ v → snd (isL v))
m は無限なので、ω のすべての要素は m に属します。この包含は計数の事実から引用されたもので、有限の要素の後続が m の内側にとどまる理由でもあります。
ω⊆m : (z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ m ⟩ ω⊆m = ω⊆ m om m∉ω
移し変えの定義域への所属を述べ、最初の判定を定義します。要素は ω に属するか、その所属が反証されるかのいずれかです。この選言は本当の場合分けであり、排中律が与えるものです。
Mem : S → Type (ℓ-suc ℓ) Mem x = ⟨ fst x ∈ˢ fst D ⟩ Fin? : S → Type (ℓ-suc ℓ) Fin? x = ⟨ fst x ∈ˢ ω ⟩ ⊎ (⟨ fst x ∈ˢ ω ⟩ → Empty.⊥)
第二の判定は後続の要素を分けます。sucʟ mL の要素は m に属するか m と等しいかであり、これが後続への所属の意味そのものです。
Top? : S → Type (ℓ-suc ℓ) Top? x = ⟨ fst x ∈ˢ m ⟩ ⊎ (fst x ≡ m)
最初の判定は排中律の一つの実例であり、x の ω への所属の命題に適用されます。
fin? : (x : S) → Fin? x fin? x = lem (fst x ∈ˢ ω)
第二の判定も排中律の実例であり、後続の消去によって洗練されます。sucʟ mL の要素は m に属するか m と等しいかであり、所属が反証されれば等しいことだけが残ります。
top? : (x : S) → Mem x → Top? x top? x h = go (lem (fst x ∈ˢ m)) where go : ⟨ fst x ∈ˢ m ⟩ ⊎ (⟨ fst x ∈ˢ m ⟩ → Empty.⊥) → Top? x go (inl k) = inl k
反証された場合では、消去が後続の切り詰められた所属を消費します。二つの結果は排他的です。ある要素が m に属し、かつ m に等しいことはあり得ません。それは m がみずからに属することになり、所属の非反射性によって退けられるからです。
go (inr nk) = inr (∈sucV-elim {A = m} {x = fst x} (setIsSet (fst x) m) (subst (λ w → ⟨ fst x ∈ˢ w ⟩) (sucʟ-fst mL) h) (λ k → Empty.rec (nk k)) (λ q → q)) not-both : (x : S) → ⟨ fst x ∈ˢ m ⟩ → fst x ≡ m → Empty.⊥ not-both x k q = ∈-irrefl m (subst (λ w → ⟨ w ∈ˢ m ⟩) q k)
有限の場合と頂点の場合は重なりません。x が ω に属し、しかも m に等しいなら、その等しさに沿って所属を移送することで m ∈ ω が得られ、m が無限であるという仮定に反します。
ω-fin : (x : S) → ⟨ fst x ∈ˢ ω ⟩ → fst x ≡ m → Empty.⊥ ω-fin x k q = m∉ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) q k)
後続が空集合になることはありません。実際、a は sucV a に属します。もし sucV a = ∅ なら、この所属を等しさに沿って移送することで、空集合の要素が得られてしまいます。
suc≢∅ : (a : V ℓ) → sucV a ≡ ∅ → Empty.⊥ suc≢∅ a e = ∅-empty a (∈∈ₛ {a = a} {b = ∅} .fst (subst (λ w → ⟨ a ∈ˢ w ⟩) e (self∈sucV a)))
三つの場合が、移し変えの値を定義します。有限の要素はみずからの内部の後続へ送られ、m の非有限の要素はみずからへ送られ、頂点の要素 m は L の空集合へ送られます。これらは、二つの判定が区別する三つの選択肢にほかなりません。
value : (x : S) → Fin? x → Top? x → S value x (inl _) _ = sucʟ x value x (inr _) (inl _) = x value x (inr _) (inr _) = ∅ʟ
値は m の中に収まることが保証されます。有限の要素については、その後続が極限の性質によって ω の要素となり、ω は m に含まれます。m の要素については、所属がその判定そのものであり、空集合は ω の、したがって m の要素です。
value-in : (x : S) (f : Fin? x) (t : Top? x) → ⟨ fst (value x f t) ∈ˢ m ⟩ value-in x (inl k) _ = subst (λ w → ⟨ w ∈ˢ m ⟩) (sym (sucʟ-fst x)) (ω⊆m (sucV (fst x)) (ω-limit (fst x) k)) value-in x (inr _) (inl k) = k value-in x (inr _) (inr _) = ω⊆m ∅ (#∈ω zero)
グラフの論理式の証人の型が宣言されます。x が有限で y はその後続、x が非有限で m に属し y は x に等しい、あるいは x が頂点 m に等しく y は空である、の三つの選択肢です。三つは切り詰めの下にあり、それぞれがみずからの所属と等式を運びます。
Wit : (y x : S) → Type (ℓ-suc ℓ)
Wit y x = ∥ (⟨ fst x ∈ˢ ω ⟩ × (fst y ≡ sucV (fst x)))
⊎ ( ((⟨ fst x ∈ˢ ω ⟩ → Empty.⊥) × ⟨ fst x ∈ˢ m ⟩ × (fst y ≡ fst x))
⊎ ((fst x ≡ m) × (fst y ≡ ∅)) ) ∥₁
グラフの論理式は対象言語で述べられます。その第一の選言肢は、x が内部の ω に属し y がその後続であることを、後続の節によって読み取ります。第二の選言肢はまず、x が有限であることを否定します。
opaque graph : Formula S 2 graph = ((var (suc zero) ∈̇ con ωʟ) ∧̇ sucAtL (suc zero) zero) ∨̇ ( ( (¬̇ (var (suc zero) ∈̇ con ωʟ)) ∧̇ ((var (suc zero) ∈̇ con mL) ∧̇ (var zero ≐ var (suc zero))) )
その内側の二つの守られた選択肢が第二と第三の選言肢を完成させます。m の非有限の要素はみずからと対にされ、頂点の要素は L の空集合と対にされます。
∨̇ ((var (suc zero) ≐ con mL) ∧̇ (var zero ≐ con ∅ʟ)) )
後続の節の妥当性が一度記録されます。二項目の文脈での後続の原子の充足は、y と周囲の後続 sucV x との間の等式です。
private sa : (y x : S) → ⟨ (y ∷ x ∷ []) ⊨ sucAtL (suc zero) zero ⟩ ≡ (fst y ≡ sucV (fst x)) sa y x = cong ⟨_⟩ (sucAtL-adequate (suc zero) zero (y ∷ x ∷ []))
論理式を外向きに読むと、命題的切り詰めの下の論理和を、やはり命題である証人型へ除去します。後続の節は妥当性によって変換し、中間の節の反証は命題リサイズによって持ち上げられた宇宙から必要なレベルへ戻します。頂点の節はすでに必要な形です。
graph-out : (y x : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → Wit y x graph-out y x = PT.rec squash₁ (λ { (inl (k , e)) → ∣ inl (k , transport (sa y x) e) ∣₁ ; (inr h) → PT.map (λ { (inl (n , (k , e))) → inr (inl ((λ hx → lower (n hx)) , k , e))
第三の選言肢は頂点の場合の二つの等式だけを運ぶので、その翻訳は直接です。
; (inr (q , e)) → inr (inr (q , e)) }) h })
三つの内向きの補題が、それぞれの証人から論理式を組み立て直します。有限の要素では、後続の等式が妥当性に沿って逆向きに輸送され、第一の選言肢に入ります。
in-fin : (y x : S) → ⟨ fst x ∈ˢ ω ⟩ → fst y ≡ sucV (fst x) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ in-fin y x k e = ∣ inl (k , transport (sym (sa y x)) e) ∣₁
m の非有限な要素については、x ∈ ω の反証を対象レベルの否定へ持ち上げます。これを x ∈ m および y = x と合わせると、中間の選言肢が得られます。
in-mid : (y x : S) → (⟨ fst x ∈ˢ ω ⟩ → Empty.⊥) → ⟨ fst x ∈ˢ m ⟩ → fst y ≡ fst x → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ in-mid y x n k e = ∣ inr ∣ inl ((λ hx → lift (n hx)) , (k , e)) ∣₁ ∣₁
頂点の要素では、頂点の場合の二つの等式が第三の選言肢に直接組み立てられます。
in-top : (y x : S) → fst x ≡ m → fst y ≡ ∅ → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ in-top y x q e = ∣ inr ∣ inr (q , e) ∣₁ ∣₁
移し変えの関数は、二つの判定を通して定義されます。判定が入力を分類する仕方に応じて、値は後続、要素そのもの、あるいは空集合です。
private fn : (x : S) → Mem x → S fn x h = value x (fin? x) (top? x h)
定義の節は三つの場合すべてで確かめられます。有限の場合は後続の等式を引用し、中間の場合は定義的であり、頂点の場合は空集合と頂点の要素を対にします。
defines' : (x : S) (f : Fin? x) (t : Top? x) → ⟨ (value x f t ∷ x ∷ []) ⊨ graph ⟩ defines' x (inl k) _ = in-fin (sucʟ x) x k (sucʟ-fst x) defines' x (inr n) (inl k) = in-mid x x n k refl defines' x (inr n) (inr q) = in-top ∅ʟ x q refl
一意性はグラフを逆向きに読みます。グラフの中で x と対にされる任意の y は、選ばれた値に等しくなります。証明は切り詰められた選言を、h-集合における等式という目標の中へ消費します。
only' : (x : S) (f : Fin? x) (t : Top? x) (y : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ value x f t only' x f t y hy = PT.rec (isSetS y (value x f t)) (go f t) (graph-out y x hy) where go : (f : Fin? x) (t : Top? x)
場合分けの関数は、展開された選択肢と選ばれた判定を受け取ります。有限の場合に有限の肯定が組になるとき、後続の等式と内部の対の等式は、後続の第一射影の同定に沿って輸送されれば一致します。
→ (⟨ fst x ∈ˢ ω ⟩ × (fst y ≡ sucV (fst x))) ⊎ ( ((⟨ fst x ∈ˢ ω ⟩ → Empty.⊥) × ⟨ fst x ∈ˢ m ⟩ × (fst y ≡ fst x)) ⊎ ((fst x ≡ m) × (fst y ≡ ∅)) ) → y ≡ value x f t go (inl k) _ (inl (_ , e)) = S≡ (e ∙ sym (sucʟ-fst x))
続く五つの節では、選ばれた有限の場合または非有限な要素の場合を、グラフの証人と照合します。有限という選択は、中間の証人に含まれる反証とも頂点の等式とも矛盾します。非有限な要素という選択は、有限の証人とは矛盾し、中間の証人とはその等式によって一致し、m の要素は m 自身に等しくなれないことから頂点の証人を排除します。
go (inl k) _ (inr (inl (n , _ , _))) = Empty.rec (n k) go (inl k) _ (inr (inr (q , _))) = Empty.rec (ω-fin x k q) go (inr n) (inl k) (inl (k' , _)) = Empty.rec (n k') go (inr n) (inl k) (inr (inl (_ , _ , e))) = S≡ e go (inr n) (inl k) (inr (inr (q , _))) = Empty.rec (not-both x k q)
選ばれた入力が頂点なら、有限の証人はその非有限性と矛盾し、中間の証人は m の要素が m 自身に等しくなれないことと矛盾します。頂点の証人からは、空集合を値とする等式によって必要な等しさが直接得られます。
go (inr n) (inr q) (inl (k' , _)) = Empty.rec (n k') go (inr n) (inr q) (inr (inl (_ , k , _))) = Empty.rec (not-both x k q) go (inr n) (inr q) (inr (inr (_ , e))) = S≡ e
以上のデータにより、sucʟ mL から mL への定義可能な関数が定まります。各入力には m に属するシフト値が割り当てられ、上の論理式がそのグラフになります。
M : DefinableMap M = record { dom = D ; cod = mL ; fn = fn ; into = λ x h → value-in x (fin? x) (top? x h) ; graph = graph
排中律は各入力について二つの判定を与えます。先の存在性と一意性の議論により、このグラフがちょうど選ばれた値について成り立つことが分かります。
; defines = λ x h → defines' x (fin? x) (top? x h) ; only = λ x h → only' x (fin? x) (top? x h) }
単射性は、二つの入力について場合を比較して証明します。両方が有限なら、シフト後の値の等しさはそれぞれの後続の等しさなので、順序数の後続の単射性から元の二つの順序数が等しいと分かります。
inj' : (x : S) (f : Fin? x) (t : Top? x) (x' : S) (f' : Fin? x') (t' : Top? x') → fst (value x f t) ≡ fst (value x' f' t') → fst x ≡ fst x' inj' x (inl k) _ x' (inl k') _ e = ord-suc-inj (fst x) (fst x') (mem-ord {A = ω} ω-ord (fst x) k) (sym (sucʟ-fst x) ∙ e ∙ sucʟ-fst x')
有限な入力が非有限な要素と同じシフト値をもつことはありません。その等しさから、後者の値、したがって後者自身が ω に属することになるからです。頂点の入力とも値を共有できません。そうすると後続が空集合に等しくなってしまいます。
inj' x (inl k) _ x' (inr n') (inl _) e = Empty.rec (n' (subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym (sucʟ-fst x) ∙ e) (ω-limit (fst x) k))) inj' x (inl k) _ x' (inr n') (inr _) e = Empty.rec (suc≢∅ (fst x) (sym (sucʟ-fst x) ∙ e)) inj' x (inr n) (inl _) x' (inl k') _ e =
有限と非有限の順序を逆にした場合も、同じ矛盾になります。二つの非有限な要素は、値が等しければ直ちに等しくなります。一方、非有限な要素は頂点と同じ値をもてません。空集合に等しければ ω に属することになるからです。
Empty.rec (n (subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym (sucʟ-fst x') ∙ sym e) (ω-limit (fst x') k'))) inj' x (inr n) (inl _) x' (inr n') (inl _) e = e inj' x (inr n) (inl _) x' (inr n') (inr _) e = Empty.rec (n (subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym e) (#∈ω zero))) inj' x (inr n) (inr _) x' (inl k') _ e =
頂点の入力について、有限な入力の値と等しければ後続が空集合になり、非有限な要素の値と等しければその要素が空集合、したがって有限な順序数になってしまいます。両方の入力が頂点なら、それぞれを m と結ぶ等式から両者が等しいと分かります。したがって、このシフトは L の内部で単射です。
Empty.rec (suc≢∅ (fst x') (sym (sucʟ-fst x') ∙ sym e)) inj' x (inr n) (inr _) x' (inr n') (inl _) e = Empty.rec (n' (subst (λ w → ⟨ w ∈ˢ ω ⟩) e (#∈ω zero))) inj' x (inr n) (inr q) x' (inr n') (inr q') e = q ∙ sym q' injL : InjL (sucʟ mL) mL
定義可能なシフトと先の分類により、符号化された単射 sucʟ mL ↪ mL が得られます。さらに、ある集合の二つの要素が同じファイバー添字で表されるなら両者は等しい、という基本的な事実を用います。添字の等しさに提示写像を作用させると、表された要素の等しさが復元されます。
injL = Inj.injL M (λ x h x' h' → inj' x (fin? x) (top? x h) x' (fin? x') (top? x' h')) opaque fiber-inj : (g : V ℓ) {x y : V ℓ} (mx : ⟨ x ∈ˢ g ⟩) (my : ⟨ y ∈ˢ g ⟩) → fiber g mx .fst ≡ fiber g my .fst → x ≡ y fiber-inj g mx my e = sym (fiber g mx .snd) ∙ cong ⟪ g ⟫↪ e ∙ fiber g my .snd
構成可能な無限順序数 a が内部の基数でもあるとき、帰納目標はその直積平方 a × a から a への符号化された単射です。この主張を Goal a としてまとめることで、所属に関する帰納法を a より下の対象へ一様に適用できます。
Goal : V ℓ → Type (ℓ-suc ℓ) Goal a = (la : ⟨ isL a ⟩) → IsOrd a → IsCardinalL (a , la) → (⟨ a ∈ˢ ω ⟩ → Empty.⊥) → InjL (prodL (a , la)) (a , la)
帰納の段階は、集合 a、a の各要素に対する帰納仮定、そして四つの仮定を受け取ります。構成可能性、順序数性、内部の基数性、無限性です。基数性の仮定は、κ がみずからの要素へ内部的に単射することを排除するもので、崩壊の計数が用いる形そのものです。
module Step (a : V ℓ) (ih : (a' : V ℓ) → ⟨ a' ∈ˢ a ⟩ → Goal a') (la : ⟨ isL a ⟩) (oa : IsOrd a) (carda : IsCardinalL (a , la)) (a∉ω : ⟨ a ∈ˢ ω ⟩ → Empty.⊥) where
台となる順序数が a である構成可能集合を κ と書きます。これにより、内部の構成を行うたびに、周囲の順序数のデータとそれが L に属することの証明を一緒に扱えます。
κ : S κ = a , la
ここから、Gödel 順序を備えた κ × κ と、その整列順序を崩壊して得られる順序数を考えます。目標は、この崩壊の各始切片がなお κ より下に抑えられることを示すことです。
open Order κ oa open Coll κ oa
順序数 a は有限順序数ではないので、すべての有限順序数を含みます。さらに後続について閉じていることが必要です。m ∈ a に対し、三分法は sucV m が a より下、a と等しい、または a より上のいずれかであるとします。続く場合分けで後二者を排除します。
ω⊆a : (z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ a ⟩ ω⊆a = ω⊆ a oa a∉ω suc∈ : (m : V ℓ) → ⟨ m ∈ˢ a ⟩ → ⟨ sucV m ∈ˢ a ⟩ suc∈ m m∈a = go (ord-tri (sucV m) (suc-ord om) a oa) where
m は順序数 a の要素なので、それ自身も順序数です。また、構成可能集合 a に属することから m も構成可能であり、内部の論域の要素 mL を定めます。
om : IsOrd m om = mem-ord {A = a} oa m m∈a mL : S mL = ordL m om
sucV m と a に三分法を適用します。第一の場合は、求める所属そのものです。sucV m = a なら、さらに m と ω を比較することで、矛盾を有限の場合と、続いて扱う二つの無限の場合に分けます。
go : ⟨ sucV m ∈ˢ a ⟩ ⊎ ((sucV m ≡ a) ⊎ ⟨ a ∈ˢ sucV m ⟩) → ⟨ sucV m ∈ˢ a ⟩ go (inl h) = h go (inr (inl e)) = Empty.rec (fin (ord-tri m om ω ω-ord)) where fin : ⟨ m ∈ˢ ω ⟩ ⊎ ((m ≡ ω) ⊎ ⟨ ω ∈ˢ m ⟩) → Empty.⊥
m が ω の要素なら、その後続も ω の要素となり、基数 a が ω の内側に入って無限性の仮定と矛盾します。m が ω に等しいか ω を含む場合は、要素 m のところで a の内部の基数性を適用すると、移し変えの単射 sucʟ mL ↪ mL、すなわち基数のある要素への内部の単射が退けられます。
fin (inl m∈ω) = a∉ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) e (ω-limit m m∈ω)) fin (inr r) = carda mL m∈a (subst (λ w → InjL w mL) sucL≡κ (Shift.injL mL om m∉ω)) where m∉ω : ⟨ m ∈ˢ ω ⟩ → Empty.⊥
局所的な非有限性は、同じ三分法から読み取られます。m が ω に等しいなら、仮定された所属が ω をみずからの内側に置き、ω が m に属するなら、推移性が再び ω をみずからの内側に置きます。どちらも所属の非反射性と矛盾します。
m∉ω h = rr r where rr : (m ≡ ω) ⊎ ⟨ ω ∈ˢ m ⟩ → Empty.⊥ rr (inl e') = ∈-irrefl ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) e' h) rr (inr ω∈m) = ∈-irrefl ω (ω-ord .fst ω∈m h)
等式 sucV m = a は内部の後続 sucʟ mL を κ と同一視するので、シフトから、基数性に反する κ から m への単射が得られます。三分法の残る場合では、a ∈ sucV m は a ∈ m または a = m を意味します。どちらからも順序数の自己所属が導かれるため、不可能です。
sucL≡κ : sucʟ mL ≡ κ sucL≡κ = Σ≡Prop (λ v → snd (isL v)) (sucʟ-fst mL ∙ e) go (inr (inr h)) = Empty.rec* (∈sucV-elim {A = m} {x = a} {P = Empty.⊥* {ℓ-suc ℓ}} Empty.isProp⊥* h (λ a∈m → lift (∈-irrefl a (oa .fst a∈m m∈a)))
後続についての閉性が得られたので、以下で必要となるより小さい順序数に帰納仮定を適用できます。より一般に、無限順序数 γ が a より下にあるなら、γ の内部基数代表を選び、その代表に帰納仮定を適用して prodL γ ↪ γ を得ます。
(λ a≡m → lift (∈-irrefl m (subst (λ w → ⟨ m ∈ˢ w ⟩) a≡m m∈a)))) prod-into : (γ : S) → IsOrd (fst γ) → ⟨ fst γ ∈ˢ a ⟩ → (⟨ fst γ ∈ˢ ω ⟩ → Empty.⊥) → InjL (prodL γ) γ prod-into γ oγ γ∈a γ∉ω = PT.rec squash₁ build (cardOf γ oγ) where
基数の代表は、切り詰められた形でデータを渡します。順序数 μ は内部の基数であり γ に含まれ、γ から μ へ、μ から γ への単射が伴います。関数 build はこのデータを積の単射へ変えます。
build : Σ[ μ ∈ S ] ( IsOrd (fst μ) × IsCardinalL μ × ((z : V ℓ) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst γ ⟩) × InjL γ μ × InjL μ γ ) → InjL (prodL γ) γ
単射は三つの単射を合成します。積の単射が γ ↪ μ を座標ごとに持ち上げ、帰納仮定が内部の基数 μ において適用されて prodL μ ↪ μ を与え、さらに μ ↪ γ によって結果が γ の中へ合成されます。
build (μ , oμ , cardμ , μ⊆γ , γ↪μ , μ↪γ) = injl-trans (prodL γ) (prodL μ) γ (prod-inj γ μ γ↪μ) (injl-trans (prodL μ) μ γ (ih (fst μ) μ∈a (snd μ) oμ cardμ μ∉ω) μ↪γ) where μ∈a : ⟨ fst μ ∈ˢ a ⟩
代表 μ も a より下にあります。μ ∈ γ なら、γ ∈ a と推移性から μ ∈ a が従います。μ = γ なら、所属をその等しさに沿って移送します。残る γ ∈ μ は不可能です。包含 μ ⊆ γ によって γ ∈ γ が導かれるからです。
μ∈a = go (ord-tri (fst μ) oμ (fst γ) oγ) where go : ⟨ fst μ ∈ˢ fst γ ⟩ ⊎ ((fst μ ≡ fst γ) ⊎ ⟨ fst γ ∈ˢ fst μ ⟩) → ⟨ fst μ ∈ˢ a ⟩ go (inl h) = oa .fst h γ∈a go (inr (inl e)) = subst (λ w → ⟨ w ∈ˢ a ⟩) (sym e) γ∈a
代表 μ も無限でなければなりません。もし μ ∈ ω なら、無限順序数 γ に対する ω ↪ γ と γ ↪ μ を合成して、ω を有限順序数 μ へ単射できてしまいます。これは不可能です。後で用いるため、Seg p b は r ≺ p であり崩壊値が b である先行者 r を記録します。
go (inr (inr h)) = Empty.rec (∈-irrefl (fst γ) (μ⊆γ (fst γ) h)) μ∉ω : ⟨ fst μ ∈ˢ ω ⟩ → Empty.⊥ μ∉ω h = no-fin γ μ oγ γ∉ω oμ h γ↪μ Seg : OT.Dom → V ℓ → Type (ℓ-suc ℓ) Seg p b = Σ[ r ∈ OT.Dom ] ((r OT.≺ p) × (C.col r ≡ b))
節は一意です。崩壊の値が等しい p の二つの先行者は等しくなります。崩壊の写しは添字の上で単射であり、この命題が以降の消去のために一度記録されます。
isPropSeg : (p : OT.Dom) (b : V ℓ) → isProp (Seg p b) isPropSeg p b (r , _ , e) (r' , _ , e') = Σ≡Prop (λ r → isProp× (OT.isProp≺ r p) (setIsSet _ _)) (I.col-inj r r' (e ∙ sym e'))
崩壊の値のすべての要素は、崩壊の外向きの読みと証明されたばかりの一意性によって、その節を確定します。ついで対の最大値が名指されます。その二つの座標のホストの順序における大きい方です。
seg : (p : OT.Dom) (b : V ℓ) → ⟨ b ∈ˢ C.col p ⟩ → Seg p b seg p b h = PT.rec (isPropSeg p b) (λ z → z) (C.col-out p b h) mx : OT.Dom → ⟪ K ⟫ mx p = maxOrd (φ p .fst) (φ p .snd)
p の二つの座標の最大値が表す周囲の順序数を mV p とします。崩壊された Gödel 順序で r ≺ p なら、r の第一座標はこの最大値の後続より下にあります。これは Gödel 順序が与える第一座標の上界です。
mV : OT.Dom → V ℓ mV p = ↑ (mx p) opaque seg-fst : (p r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .fst) ∈ˢ sucV (mV p) ⟩ seg-fst p r k = fst∈suc (φ r) (φ p) (≺-fwd r p k)
すべての r ≺ p について、第二座標も同じ上界を満たします。そこで gfin p = sucV (mV p) を両座標に共通の台として用います。有限の場合の仮定 mV p ∈ ω のもとでは、この台自身も有限順序数です。
seg-snd : (p r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .snd) ∈ˢ sucV (mV p) ⟩
seg-snd p r k = snd∈suc (φ r) (φ p) (≺-fwd r p k)
gfin : OT.Dom → V ℓ
gfin p = sucV (mV p)
opaque
各先行者 r ≺ p について、二つの座標の上界から gfin p の提示における二つの添字が選ばれ、h p r はその順序対です。mV p が有限なら、この対は r を有限順序数の平方の中に符号化します。
h : (p r : OT.Dom) (k : r OT.≺ p) → ⟪ gfin p ⟫ × ⟪ gfin p ⟫ h p r k = fiber (gfin p) (seg-fst p r k) .fst , fiber (gfin p) (seg-snd p r k) .fst
二つの符号 h p r と h p r' が等しければ、その等しさに第一射影を作用させることで、第一の添字が等しいと分かります。これは符号から r の座標を復元する前半です。
h-fst : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p) → h p r k ≡ h p r' k' → fiber (gfin p) (seg-fst p r k) .fst ≡ fiber (gfin p) (seg-fst p r' k') .fst h-fst p r r' k k' e = cong fst e
同じ符号の等しさに第二射影を作用させると、第二の添字も等しいと分かります。したがって、ファイバー対の等しさは二つの成分をそれぞれ決定します。
h-snd : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
→ h p r k ≡ h p r' k'
→ fiber (gfin p) (seg-snd p r k) .fst
≡ fiber (gfin p) (seg-snd p r' k') .fst
h-snd p r r' k k' e = cong snd e
第一のファイバー添字が等しければ、それらのファイバーが表す周囲の順序数も等しくなります。K の提示写像は単射なので、第一座標 φ r .fst と φ r' .fst が等しいと従います。
step-e1 : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p) → h p r k ≡ h p r' k' → φ r .fst ≡ φ r' .fst step-e1 p r r' k k' e = ↪-inj {a = K} (fiber-inj (gfin p) (seg-fst p r k) (seg-fst p r' k') (h-fst p r r' k k' e))
第二の移送の補題は第二の座標についても同じことをし、ファイバーの対の相等がもとの対の両座標を確定します。崩壊の有限の場合に必要なのはまさにこれです。
step-e2 : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p) → h p r k ≡ h p r' k' → φ r .snd ≡ φ r' .snd step-e2 p r r' k k' e = ↪-inj {a = K} (fiber-inj (gfin p) (seg-snd p r k) (seg-snd p r' k') (h-snd p r r' k k' e))
二つのファイバー対の符号が等しければ、φ r と φ r' の二つの座標はそれぞれ等しくなります。対の外延性でこれらの座標の等しさをまとめ、さらに φ の単射性を用いると r = r' が得られます。したがって、p の先行者の符号化は単射です。示すべき有限の場合は、p の最大座標が ω に属するなら C.col p も ω に属する、という主張です。
step-inj : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p) → h p r k ≡ h p r' k' → r ≡ r' step-inj p r r' k k' e = φ-inj r r' (pair≡ (step-e1 p r r' k k' e) (step-e2 p r r' k k' e)) col-fin : (p : OT.Dom) → ⟨ mV p ∈ˢ ω ⟩ → ⟨ C.col p ∈ˢ ω ⟩
証明は三分法によって崩壊の値と ω を比較し、まず有限の台に名前を与えます。g は p の周囲の最大値の後続であり、すべての先行者の二つの座標が収まると示された集合です。
col-fin p m∈ω = go (ord-tri (C.col p) (C.col-ord p) ω ω-ord) where g : V ℓ g = sucV (mV p) og : IsOrd g
mV p ∈ ω なので、この最大値は順序数であり、その後続 g も順序数です。ω の極限性から g ∈ ω が従うため、g は有限順序数です。これらは、ω から g × g への単射を排除するために必要な仮定です。
og = suc-ord (ω-mem-ord (mV p) m∈ω) g∈ω : ⟨ g ∈ˢ ω ⟩ g∈ω = ω-limit (mV p) m∈ω
反証は、ω が崩壊の値に含まれると仮定します。すると ω のすべての添字が col p の節を名指します。包含が名指された要素を崩壊の内側に置き、節の補題が先行者を復元するのです。
refute : ((z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ C.col p ⟩) → Empty.⊥ refute sub = finite-excl-ω g og g∈ω f f-inj where s : (x : ⟪ ω ⟫) → Seg p (⟪ ω ⟫↪ x) s x = seg p (⟪ ω ⟫↪ x) (sub (⟪ ω ⟫↪ x) (member ω x))
各 x ∈ ω に対し、崩壊値が x である p の一意な先行者を s x とします。写像 f は x を、その先行者の二つの座標を符号化するファイバー添字の対、したがって有限な平方 g × g の要素へ送ります。このような符号が等しければ、もとの ω の要素も等しいことを示せばよいのです。
f : ⟪ ω ⟫ → ⟪ g ⟫ × ⟪ g ⟫ f x = h p (s x .fst) (s x .snd .fst) f-inj : (x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y f-inj x y e = ↪-inj {a = ω} (sym (s x .snd .snd)
単射性は三つの等式の合成として証明されます。x の節の崩壊の値は x に等しく、二つの節は証明されたばかりの有限の場合の単射によって先行者として一致し、y の節の崩壊の値は y に等しい。合成すると、x と y が一致することが迫られます。
∙ cong C.col (step-inj p (s x .fst) (s y .fst) (s x .snd .fst) (s y .snd .fst) e) ∙ s y .snd .snd)
これで三分法から C.col p ∈ ω が従います。C.col p = ω なら、すでに排除した包含 ω ⊆ C.col p が得られます。ω ∈ C.col p の場合も、順序数 C.col p の推移性から同じ包含が得られます。一般の逆崩壊を構成するため、先行者の上界 p と構成可能な台 g を固定します。
go : ⟨ C.col p ∈ˢ ω ⟩ ⊎ ((C.col p ≡ ω) ⊎ ⟨ ω ∈ˢ C.col p ⟩) → ⟨ C.col p ∈ˢ ω ⟩ go (inl k) = k go (inr (inl e)) = Empty.rec (refute (λ z z∈ω → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈ω)) go (inr (inr ω∈c)) = Empty.rec (refute (λ z z∈ω → C.col-ord p .fst z∈ω ω∈c)) module Inv (p : OT.Dom) (g : S)
各 r ≺ p について、φ r が表す二つの座標がとも g の台に属すると仮定します。この二つの上界により、r が表す対は内部の積 prodL g に属します。この積が逆崩壊の終域になります。
(bfst : (r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .fst) ∈ˢ fst g ⟩) (bsnd : (r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .snd) ∈ˢ fst g ⟩) where
崩壊の値のすべての要素 x はみずからの節を確定します。節は一意なので、切り詰められた所属は消去され、崩壊の値が x の基底集合である先行者 r が得られます。
private pre : (x : S) → ⟨ fst x ∈ˢ C.col p ⟩ → Σ[ r ∈ OT.Dom ] (C.col r ≡ fst x) pre x mx = seg p (fst x) mx .fst , seg p (fst x) mx .snd .snd
x ∈ C.col p から選ばれた先行者 r について、提示の等式は OT.↪ r を、φ r が表す二つの座標の順序対と同一視します。したがって prodL g への所属は二つの座標の上界に帰着し、bfst が第一の上界を与えます。
bound : (x : S) (mx : ⟨ fst x ∈ˢ C.col p ⟩) → ⟨ OT.↪ (pre x mx .fst) ∈ˢ fst (prodL g) ⟩ bound x mx = subst (λ w → ⟨ w ∈ˢ fst (prodL g) ⟩) (sym (φ-eq (seg p (fst x) mx .fst))) (prodL-in g (upK (φ (seg p (fst x) mx .fst) .fst)) (upK (φ (seg p (fst x) mx .fst) .snd)) (bfst _ (seg p (fst x) mx .snd .fst))
bsnd が第二座標の所属を与えます。二つの上界を合わせると、表された順序対が g × g に属することが分かり、必要な終域の証明が完成します。
(bsnd _ (seg p (fst x) mx .snd .fst)))
したがって、p より下の始切片上の崩壊には prodL g への定義可能な逆写像があります。C.col p の各要素は一意な先行者へ戻り、異なる崩壊値は異なる対へ戻ります。これにより、内部の単射 C.colʟ p ↪ prodL g が得られます。主帰納では、各 p について C.col p ∈ a を示します。まず、その最大座標に三分法を適用します。
open I.Inverse (C.colʟ p) (prodL g) pre bound public using ( fn; graph; at; only; M; inj; injL ) renaming ( SourceMem to Mem ) colIn : (p : OT.Dom) → ⟨ C.col p ∈ˢ a ⟩ colIn p = go (ord-tri (mV p) (ord↑ (mx p)) ω ω-ord) where
対の最大値が有限なら、有限の場合によって崩壊の値も有限であり、ω が a に含まれることで a の中に入ります。そうでなければ最大値は無限で、崩壊の値と a の三分法が検討されます。
go : ⟨ mV p ∈ˢ ω ⟩ ⊎ ((mV p ≡ ω) ⊎ ⟨ ω ∈ˢ mV p ⟩) → ⟨ C.col p ∈ˢ a ⟩ go (inl m∈ω) = ω⊆a (C.col p) (col-fin p m∈ω) go (inr inf) = go' (ord-tri (C.col p) (C.col-ord p) a oa) where m∉ω : ⟨ mV p ∈ˢ ω ⟩ → Empty.⊥
無限の場合に mV p ∈ ω と仮定して矛盾を導きます。mV p = ω なら、この所属を等しさに沿って移送すると ω ∈ ω が得られます。一方 ω ∈ mV p なら、ω の推移性で二つの所属を合成すると、やはり ω ∈ ω が得られます。非反射性が両方を排除するので、mV p は有限順序数ではありません。
m∉ω h = rr inf where rr : (mV p ≡ ω) ⊎ ⟨ ω ∈ˢ mV p ⟩ → Empty.⊥ rr (inl e) = ∈-irrefl ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) e h) rr (inr ω∈m) = ∈-irrefl ω (ω-ord .fst ω∈m h)
台 g は最大値の後続であり、最大値が順序数 κ の要素であるため g も順序数です。ついでこの順序数は L の要素 gL としてまとめられます。
g : V ℓ
g = sucV (mV p)
og : IsOrd g
og = suc-ord (ord↑ (mx p))
gL : S
台は、上で証明した後続の閉性によって a に属し、さらに無限です。g が ω に属すれば、g の要素である最大値も推移性によって ω に属することになり、確立されたばかりの無限性と矛盾します。
gL = ordL g og g∈a : ⟨ g ∈ˢ a ⟩ g∈a = suc∈ (mV p) (member K (mx p)) g∉ω : ⟨ g ∈ˢ ω ⟩ → Empty.⊥ g∉ω h = m∉ω (ω-ord .fst (self∈sucV (mV p)) h)
各 r ≺ p について、上界 seg-fst と seg-snd は r の二つの座標をとも g = sucV (mV p) に入れます。したがって逆崩壊の構成により、C.colʟ p から prodL gL への内部の単射が得られます。
module IV = Inv p gL (seg-fst p) (seg-snd p) using (injL)
逆崩壊の単射と prod-into gL を合成すると、C.colʟ p ↪ gL が得られます。後者は gL に帰納仮定を直接適用したものではありません。prod-into はまず gL の内部基数代表 μ を選び、μ で帰納仮定を適用し、μ と gL の間の単射に沿って、得られた平方の単射を移します。
col↪g : InjL (C.colʟ p) gL col↪g = injl-trans (C.colʟ p) (prodL gL) gL IV.injL (prod-into gL og g∈a g∉ω) absurd : ((z : V ℓ) → ⟨ z ∈ˢ a ⟩ → ⟨ z ∈ˢ C.col p ⟩) → Empty.⊥ absurd sub = carda gL g∈a (injl-trans κ (C.colʟ p) gL (inclusion-coded κ (C.colʟ p) sub) col↪g)
基数が崩壊の値に含まれるなら、その包含と gL への単射を合成することで、κ がみずからの要素 gL へ単射することになり、κ の内部の基数性と矛盾します。したがって崩壊の値と a の三分法に残るのは直接の所属だけです。
go' : ⟨ C.col p ∈ˢ a ⟩ ⊎ ((C.col p ≡ a) ⊎ ⟨ a ∈ˢ C.col p ⟩) → ⟨ C.col p ∈ˢ a ⟩
go' (inl h) = h
go' (inr (inl e)) = Empty.rec (absurd (λ z z∈a → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈a))
go' (inr (inr h)) = Empty.rec (absurd (λ z z∈a → C.col-ord p .fst z∈a h))
result : InjL (prodL κ) κ
まず積を崩壊の順序型 C.otL へ単射します。この順序型の各要素 z は、ある b : OT.Dom に対する C.col b と等しく、colIn b によってその崩壊値は a に属します。したがって C.otL ⊆ κ です。最初の単射と、この符号化された包含を合成すると、必要な内部の単射 prodL κ ↪ κ が得られます。
result = injl-trans P C.otL κ injL-ot (inclusion-coded C.otL κ ot⊆a) where ot⊆a : (z : V ℓ) → ⟨ z ∈ˢ fst C.otL ⟩ → ⟨ z ∈ˢ a ⟩ ot⊆a z hz = PT.rec (snd (z ∈ˢ a)) (λ { (b , e) → subst (λ w → ⟨ w ∈ˢ a ⟩) e (colIn b) }) (C.otL-out z hz)
これで所属関係に関する整礎帰納法から平方則が得られます。内部の基数であり ω ∈ κ を満たす順序数 κ に対し、κ が有限順序数ではないことを示せば、上で構成した帰納段階から内部の単射 prodL κ ↪ κ が得られます。
square-law-L : (κ : S) → IsOrd (fst κ) → IsCardinalL κ → ⟨ ω ∈ˢ fst κ ⟩ → InjL (prodL κ) κ square-law-L κ oκ cκ ω∈κ = WF.WFI.induction regularityV {P = Goal} Step.result (fst κ) (snd κ) oκ cκ
最後に、κ が ω に属することはありません。もし属するなら、順序数 ω の推移性により ω ∈ κ と κ ∈ ω から ω ∈ ω が従い、非反射性に反します。これで帰納段階に必要な無限性の仮定が得られます。
(λ κ∈ω → ∈-irrefl ω (ω-ord .fst ω∈κ κ∈ω))