Bedrockこの章を読むか、対話型目次と依存グラフで別のルートを選べます。
対話型目次 · 依存グラフそこで宇宙レベル ℓ とホスト側の仮定 lem : LEM (ℓ-suc ℓ) を固定する。ここから得られる各定理は、その型にこの仮定を明示的に保つ。固定した段階での議論は、定義可能性、推移性、Δ₀ 絶対性だけを構成的に使う。古典的な依存が実際に現れるのは、任意の定数、始集合、または選ばれた像の値に、正準な最小段階の添字を割り当てるときである。
module L.Axioms.Separation {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
有界な分出公理が求めるのは、構成可能集合 a のホスト側の部分型だけではない。a に属し、与えられた Δ₀ 論理式を満たす x だけを要素とする、構成可能モデルの要素を求める。有界な置換公理は、関数的な Δ₀ 関係の値からなる集合を求める。どちらの証明でも、関係するデータを一つの順序数段階へ入れ、その段階で定義可能部分集合を作り、この段階内の計算を構成可能モデル全体での充足関係と比較する。
初めから二つの論理の層を区別する必要がある。論理式とその量化子は、モデルが解釈する対象言語に属する。真理値が決定可能であるという主張はホスト理論に属する。後続宇宙レベルの排中律を仮定する。この仮定は、構成可能集合を含む最小の層を割り当てる操作を通して証明に入る。これは L の内部で主張される公理でも、選択原理でもない。
対象言語によって、第一の有界性が正確に定まる。論理式 φ : Formula S n はモデルの台 S の要素を定数として含むことができ、n 個の自由変数の位置をもつ。証明 Δ₀ φ は、φ に現れるすべての量化子が項によって有界であることを表す。所属の原子論理式は Δ₀ であり、連言と有界存在量化はこの性質を保つ。この三つの閉性によって、分出の論理式と像の論理式も Δ₀ になる。
もう一つの有界性は定数を制約する。BoundedTm P t と BoundedFo P φ は、項または論理式に現れるすべての定数がホスト側の述語 P を満たすことを表す。論理式の量化子が有界かどうかについては何も述べないので、mkBoundedFo は Δ₀ でない論理式にも適用できる。この証明を使うと、改名によって各定数を選んだ段階の添字に置き換えられ、写像に関する補題によって、その構文上の変更の前後で充足関係を比較できる。
なぜ定数を一つの段階へ移すのであろうか。段階 Lset σ には小さな提示があるため、その部分集合を定義する論理式は、この提示の添字を定数として使う。これに対して元の論理式は、S の任意の要素を定数として使う。改名した後では、DefOf (Lset σ) が、その論理式で選ばれる部分集合を周囲の累積階層の中で作り、構成可能性に関する結果がそれをモデルの要素として組み立てる。残る課題は、この段階で定義した部分集合の要素が、元の論理式が L で指定する要素と正確に一致することを証明することである。
階層に関する道具は、二つの規模の順序数上界を与える。bound2 は二つの段階の添字を一つの共通の順序数の中へ置き、boundingOrd は小さな型で添字づけられた族について同じことを行う。その後、段階の単調性によって所属を共通上界まで持ち上げる。操作 stage は、各構成可能集合に、それを含む最小の段階の添字を割り当てる。この構成では、この最小段階の操作だけが lem を使う。もう一方の端では、uniqueL がモデルの集合外延性を使い、各点での所属の仕様から一意性を証明する。
ここで使ういくつかの等しさは、役割が異なる。⇔toPath は命題外延性を使い、二方向の含意を命題値の真理値の間のパスへ変える。構成可能性の証明が命題をなすため、Σ≡Prop は基礎にある集合の等しさをモデル要素の等しさへ持ち上げる。集合外延性は、これとは別に uniqueL を通して使われる。最後に、命題的切り詰めは、選ばれた証人を保持せずに証人の存在だけを記録する。その除去子は、行き先が再び命題である場合にだけ使う。
小さな提示は、モデルの所属を、順序数による上界と段階での定義可能性に必要な小さな添字型へ結びつける。累積階層の集合 A に対して、型 ⟪ A ⟫ は提示された要素を添字づけ、⟪ A ⟫↪ は添字が名指す集合を返す。逆に、∈-asFiber は所属の証明 x ∈ A を、添字と、その提示された集合から x へのパスへ変える。この構成は、切り詰められていないファイバーのデータを局所的に使う。命題的切り詰めから代表を取り出すことはない。
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅ )
open import Cubical.HITs.CumulativeHierarchy.Properties
using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )
L 上の命題値構造の台を S とする。要素 x : S は、周囲の集合 x .fst と、その集合が構成可能であることの証明 x .snd からなる依存対である。したがって S はモデルの台の型であり、L という名の集合ではない。その等しさと所属は基礎にある集合から読み取られ、hProp に値を取る。
open hPropView 𝒮ʟ
これらの公理が最終的に要求するのは、この台がホスト側のクラス Q : S → hProp (ℓ-suc ℓ) を実現することである。型 SetOf Q は、モデル要素 b と、各 x : S に対するパス (x ∈ˢ b) ≡ Q x を組にする。分出公理では、Q x は始集合への所属と対象言語の充足判断を連言で結ぶ。たとえば論理式が x は定数 c に属すと述べるなら、求める外延は a と c の共通部分である。証明はこのクラスを L の集合によって実現する。クラスそのものを対象言語の論理式と同一視することも、ホスト理論の部分型がすでに L に属すと仮定することもない。
module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )
同じ対象言語の論理式を、二つの構造で読めるようになった。記法 γ ⊨v φ は、生の集合からなる割り当てのもとで、周囲の累積階層における充足関係を表す。一方、γ ⊨ φ は台が S である構造における充足関係を表す。この二つの判断を区別しておくことが必要である。固定した段階での構成は、まず周囲で定義された部分集合についての主張を証明し、その後、絶対性によって構成可能モデルで意図した充足判断を回復する。
module SemV = FOL.Semantics 𝒮ᵥ
open SemV.At (V ℓ) id using () renaming ( _⊨_ to _⊨v_ )
構成可能クラスは推移的である。構成可能集合の要素は再び構成可能である。これは有界量化子を扱うのにちょうど十分である。構成可能な境界項の解釈に属する周囲の証人は S の要素として組み直せ、内側の証人は基礎にある集合へ射影できる。したがって Δ₀ 論理式についての帰納から、その周囲での真理値と内側での真理値の間のパス abs₀ が得られる。これは Δ₀ 絶対性であり、L やいずれかの段階が任意の論理式について初等的であるという主張ではない。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL using ( abs₀ ) renaming ( _⊨ᵐ_ to _⊨_ )
置換による像
置換公理については、まず像をホスト側の述語として述べる。真理値 ReplImage a φ z は、ある x : S が存在して、x ∈ˢ a であり、対象言語の論理式 φ が割り当て x ∷ z ∷ [] で充足されるという事実だけを表す。ここでは始域の要素が第零の位置、値の候補が第一の位置を占める。このホスト側の添字付き存在は命題的切り詰めを使うため、どの始域の要素が z を生じたかを忘れる。これは、同じ像を一変数論理式によって定義するときに使う対象言語の有界存在 ∃̇∈ とは別のものである。この定義自体は、φ が Δ₀ であることも、関係が関数的であることも要求しない。
ReplImage : (a : S) (φ : Formula S 2) → S → hProp (ℓ-suc ℓ)
ReplImage a φ z = ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((x ∷ z ∷ []) ⊨ φ)
関数的な像を抑える
置換公理で新たに生じる問題は、可能な値をすべて含む一つの段階を見つけることである。FunctionalImage は任意のホスト側の関係 R を扱い、各 x ∈ˢ a についてファイバー Σ[ y ∶ S ] ⟨ R x y ⟩ が可縮であると仮定する。したがって、このファイバーには指定された中心があり、ほかのすべての関係する対はその中心に等しくなる。この仮定は、各始域の要素について存在と一意性をデータとして与える。中心を射影することは通常の依存関数の適用であり、ホスト側の選択公理も対象理論の選択公理も使わない。
module FunctionalImage (a : S) (R : S → S → hProp (ℓ-suc ℓ))
(fc : (x : S) → ⟨ x ∈ˢ a ⟩
→ isContr (Σ[ y ∶ S ] ⟨ R x y ⟩)) where
型 Mem は、始域の要素と、それが a に属するという証拠を組にする。可縮なファイバーについての仮定はこの証拠を入力として要求するので、単なる x : S だけでは足りない。S はすでに後続宇宙レベルにあるため、Mem は boundingOrd が要求する小さな添字型として直接使うには大きすぎる。基礎にある集合 a .fst の正準な小さな提示は、上界の構成に必要な始域の要素を小さな型で列挙する。
Mem : Type (ℓ-suc ℓ)
Mem = Σ[ x ∶ S ] ⟨ x ∈ˢ a ⟩
p : Mem に対して、可縮なファイバー fc (p .fst) (p .snd) はすでにその中心を含んでいる。関数 img は中心の値の成分を射影し、証明付きの各始域の要素に対して一つの確定したモデル要素を与える。これは各点で値を選んでいるように見えるが、切り詰められた存在を除去してはいない。中心は、与えられた依存関数 fc の明示的な成分だからである。
img : Mem → S
img p = fc (p .fst) (p .snd) .fst .fst
中心が含むのは選ばれた値だけではない。その第二成分は R (p .fst) (img p) が成り立つことを証明し、img-sat はこの事実に名前を与える。この区別には意味がある。img はその段階を抑えられる要素を与え、img-sat は、その選ばれた要素が与えられた始域の要素における関係の値であることを証明する。
img-sat : (p : Mem) → ⟨ R (p .fst) (img p) ⟩
img-sat p = fc (p .fst) (p .snd) .fst .snd
可縮性はまた、選ばれた中心を、ほかのすべての関係する対 (y , h) と同一視する。第一射影に合同性を適用すると img p ≡ y が得られる。これは構成可能性の証明も含む、モデル要素全体の等しさである。img p を共通の段階へ入れ、この等しさに沿って所属の証明を輸送すれば、R (p .fst) y を満たす任意の y を扱える。関数性は始域の要素ごとに使われる。異なる始域の要素から生じる値が互いに異なるという主張ではない。
img-uniq : (p : Mem) (y : S) → ⟨ R (p .fst) y ⟩ → img p ≡ y
img-uniq p y h = cong (λ p → p .fst) (fc (p .fst) (p .snd) .snd (y , h))
小さな添字の族を得るために、memS は添字 m : ⟪ a .fst ⟫ から始める。この添字が提示する集合は a .fst に属する。a は構成可能であり、構成可能クラスは推移的なので、この提示された集合も構成可能である。したがって、その集合と証明を組にして S の要素を作れる。さらに元の所属の証明を加えると Mem の要素となり、img とファイバーについての仮定を適用できる。
private
memS : ⟪ a .fst ⟫ → Mem
memS m = (⟪ a .fst ⟫↪ m
, isL-trans fm∈fa (a .snd)) , fm∈fa
where
局所的な証明 fm∈fa は、memS の所属の成分を与える。正準な提示は、まず小さな所属関係によって所属を述べ、∈∈ₛ がその事実を累積階層の命題値の所属へ変換する。fm∈fa と証明 a .snd に推移性を適用すると、memS の構成可能性の成分が得られる。したがって同じ所属の事実が、提示された集合を始集合の中に位置づけると同時に、それを構成可能なモデル要素として組み立てることを可能にする。
fm∈fa : ⟨ ⟪ a .fst ⟫↪ m ∈ a .fst ⟩
fm∈fa = ∈∈ₛ {a = ⟪ a .fst ⟫↪ m} {b = a .fst} .snd (∈ₛ⟪ a .fst ⟫↪ m)
これで、小さな型 ⟪ a .fst ⟫ を通して始集合を走査できる。各添字 m について、選ばれた値 img (memS m) を含む最小の段階の添字を取り、その順序数性を stage-ord で与える。構成的な操作 boundingOrd は、これらすべての添字より真に上にある一つの順序数を返す。共通上界の議論が使うのは stage-ord と stage-mem が与える事実であり、最小性は必要ない。ただし、標準的な stage の割り当てから最小性も得られる。a が空なら添字の族も空であるが、boundingOrd はそれでも順序数上界を返し、像に要素があるとは主張しない。
bImg = boundingOrd ⟪ a .fst ⟫
(λ m → stage ((img (memS m)) .fst) (img (memS m) .snd))
(λ m → stage-ord ((img (memS m)) .fst) (img (memS m) .snd))
この上界の結果の第一射影を βimg と名づける。これは順序数である段階の添字であり、段階そのものではない。対応する段階は、累積階層の集合 Lset βimg である。range∈βimg は、関係するすべての値の基礎にある集合がこの段階に属すことを述べる。Lset βimg をモデル要素として組み立てるのは別の操作であり、順序数性の証明を必要とする。
βimg : V ℓ
βimg = bImg .fst
bImg の第二射影は、上界の二つの部分を証明する。その第一の部分をここで βimg-ord として取り出し、βimg が順序数であることを示す。この証明によって、Lset βimg をモデル要素として組み立てられる。残る部分は、小さな始域の添字 m ごとに、選ばれた値の段階の添字が βimg に属することを与える。この比較を stage-mem と組み合わせると、選ばれた各像が Lset βimg に入る。さらに、提示された始域の要素から任意の始域の要素へ輸送し、img-uniq を使うことで、その要素と関係するすべての値へ結論を広げる。したがって、順序数性と値域の包含は、同じ上界の構成から取り出される別々の主張である。
βimg-ord : IsOrd βimg
βimg-ord = bImg .snd .fst
関係のすべての値を抑えるため、x ∈ˢ a、候補 y、および R x y の証明を固定する。始集合への所属により、x は a の標準的な小さい表示から得られる要素と同一視される。関数性はさらに、y をその表示された要素で選ばれた値と同一視する。その値は自身の標準的な段階に属し、その添字は βimg より真に小さいので、Lset-mono によって Lset βimg へ持ち上がる。最後に値の等式に沿って輸送すれば y の所属が得られる。したがって一つの段階 Lset βimg が、a の要素から関係によって得られるすべての値を含む。先に標準的な段階を選ぶ部分は lem に依存するが、ここでの最後の比較と上方への輸送は新たな古典原理を導入しない。
range∈βimg : (x : S) → ⟨ x ∈ˢ a ⟩ → (y : S) → ⟨ R x y ⟩
→ ⟨ y .fst ∈ Lset βimg ⟩
range∈βimg x x∈a y h = subst (λ w → ⟨ w .fst ∈ Lset βimg ⟩) image≡y
(Lset-mono {α = βimg} {β = stage ((img (memS m)) .fst) (img (memS m) .snd)}
(bImg .snd .snd m) (stage-mem ((img (memS m)) .fst) (img (memS m) .snd)))
所属のファイバーは、任意の始点と小さい表示を比較するための二つのデータを同時に与える。第一射影は a .fst の表示の添字 m である。これは単に要素が存在する集まりから選んだものではなく、所属の証明そのものに含まれるデータである。第二射影は、m が表示する集合と x .fst との等式を与える。モデル要素の第二成分 isL は命題値であり、同じ基礎集合をもつ二つの組を区別しないため、Σ≡Propはこの基礎集合の等式を memS m .fst ≡ x へ持ち上げる。
where
m = ∈-asFiber {a = x .fst} {b = a .fst} x∈a .fst
q : memS m .fst ≡ x
q = Σ≡Prop (λ z → (isL z) .snd)
(∈-asFiber {a = x .fst} {b = a .fst} x∈a .snd)
もとの関係の証明は x を始点とする。これを q の逆向きに沿って輸送すると、R (memS m .fst) y の証明になり、memS m において fc が選んだ中心と同じ値のファイバーに入る。そのファイバーは可縮なので、img-uniq は中心img (memS m) と y を同一視する。関数性が使われるのは、固定した一つの始点に対する二つの値を比較するためである。異なる始点の値が異なるとは主張しない。
image≡y : img (memS m) ≡ y
image≡y = img-uniq (memS m) y (subst (λ z → ⟨ R z y ⟩) (sym q) h)
固定した段階での構成
固定した段階での議論は、順序数の添字 σ とその証明 oσ から始まる。構成 DefC = DefOf (Lset σ) は、Lset σ の要素をその標準的な小さい表示を通して扱う。そして、表示の添字を定数とする論理式と、各一変数論理式が切り出す部分集合 defSet を与える。残る課題は、この段階に基づく定義を構成可能モデルでの充足と正確に比較することである。
module AtStage (σ : V ℓ) (oσ : IsOrd σ) where
module DefC = DefOf (Lset σ)
有界論理式の絶対性には、対象となるクラスの推移性が必要である。ここで DefC.M はLset σ の要素のクラスであり、layer-trans (Lset-layer σ) は、その要素の要素も再び段階内にあることをちょうど証明する。この証明は順序数性の証明 oσ を使わない。推移性は Lset-layer σ 自体から従う。この閉性によって、有界量化子の証人は制限された世界の内部に留まる。
Atrans : hPropView.Transitive 𝒮ᵥ DefC.M
Atrans = layer-trans (Lset-layer σ)
Atrans を DefC.Refine に与えると、有界論理式を比較する結果が使えるようになる。改名された記法 _⊨σ_ は、精緻化モジュールが与える周囲の V 値の読みを表す。段階の添字を、それが表示する要素として解釈し、得られた論理式を周囲の階層で評価する。特に Δ₀ 論理式について、RefC.abs-defSet は定義可能部分集合への所属をこの周囲の読みと同一視する。これが後の意味論的な橋の前半である。
module RefC = DefC.Refine Atrans
open RefC.Abs using () renaming ( _⊨ᵛ_ to _⊨σ_ )
述語 Below c は、基礎集合 c .fst が Lset σ に属することだけを表す。その役割は項や論理式に現れる定数を証明することであり、BoundedFo Below φ はφ の各定数についてこの証明を保持する。自由変数への付値や量化された証人を制約するものではない。充足する値が段階内にあることは、後で carveAt の別の仮定 cover が保証する。
Below : S → Type (ℓ-suc ℓ)
Below c = ⟨ c .fst ∈ Lset σ ⟩
付け替え RL は、Below を満たす各モデル定数を、小さい表示 ⟪ Lset σ ⟫ の添字へ変える。意味論側の二つの写像は、モデル要素から基礎集合を取る fst と、表示の添字からそれが指す集合を取る ⟪ Lset σ ⟫↪ である。c .fst ∈ Lset σ の証明に対して、∈-asFiber は必要な添字と、その添字が実際に c .fst を指すという等式を同時に返す。この二つの射影が、正しい付け替えに必要な可換三角形を与える。
module RL = Relabel {K = S} {K' = ⟪ Lset σ ⟫} {W = V ℓ}
(λ p → p .fst) ⟪ Lset σ ⟫↪ Below
(λ c p → ∈-asFiber {a = c .fst} {b = Lset σ} p .fst)
(λ c p → ∈-asFiber {a = c .fst} {b = Lset σ} p .snd)
この橋は、同じ数学的な付値に対する二つの充足命題を比較する。左辺では、まずRL.liftFo が φ の各定数を表示の添字へ付け替え、mapFo DefC.ι がその添字を表示される要素として解釈し、_⊨σ_ が周囲の階層で ⟪ Lset σ ⟫↪ m において評価する。右辺では、もとの論理式を構成可能モデルの内部で、組にした要素(⟪ Lset σ ⟫↪ m , xL) において評価する。定数の境界 h、Δ₀ の証明 dφ、構成可能性の証明 xL が、これらの視点の移動を正当化する。
satBridge : (φ : Formula S 1) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
(m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
→ ((⟪ Lset σ ⟫↪ m ∷ []) ⊨σ (mapFo DefC.ι (RL.liftFo φ h)))
≡ (((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ)
satBridge φ h dφ m xL =
最初の三つのパスは、連続する二つの定数解釈を整理する。最初の ⊨-map は段階の定数解釈 DefC.ι を展開する。二番目の適用を逆向きに使うと、同じ読みが表示写像 ⟪ Lset σ ⟫↪ を通す形になる。次に RL.liftFo-correct を cong によって充足の下へ移し、「添字へ付け替えてから再び指す」解釈を、fst による直接の解釈へ置き換える。この最後の段階は RL の可換三角形から得られる構文上の論理式の等式である。
⊨-map 𝒮ᵥ DefC.ι (λ p → p .fst) (RL.liftFo φ h)
(⟪ Lset σ ⟫↪ m ∷ [])
∙ sym (⊨-map 𝒮ᵥ ⟪ Lset σ ⟫↪ id (RL.liftFo φ h)
(⟪ Lset σ ⟫↪ m ∷ []))
∙ cong (λ ψ → (⟪ Lset σ ⟫↪ m ∷ []) ⊨v ψ) (RL.liftFo-correct φ h)
第四のパスは再び ⊨-map を使い、定数と環境をともに fst を通して読む周囲での充足を、モデル要素上の対応する論理式へ移す。この時点で、もとの論理式と、組にされた一要素環境がそろう。最後のパスは abs₀ を逆向きに使う。Δ₀ 絶対性により、基礎集合における周囲での真理が構成可能モデル内部での真理へ戻る。結果は hProp 間の等式なので、後の議論は証明をどちら向きにも輸送できる。
∙ ⊨-map 𝒮ᵥ (λ p → p .fst) id φ (⟪ Lset σ ⟫↪ m ∷ [])
∙ sym (abs₀ dφ ((⟪ Lset σ ⟫↪ m , xL) ∷ []))
必要な所属の仕様をここで直接述べられる。段階の表示の添字 m と、それが表す集合が構成可能であるという証明 xL に対し、持ち上げた論理式が切り出す定義可能部分集合への所属は、もとの論理式が L で充足されることに等しくなる。左辺はLset σ の小さい表示を使い、右辺は同じ表示された集合をモデル要素として組にする。この等式が、段階内の構成を分出が実現すべき述語へ結ぶ。
carveSat : (φ : Formula S 1) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
(m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
→ (⟪ Lset σ ⟫↪ m ∈ DefC.defSet (RL.liftFo φ h))
≡ (((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ)
carveSat φ h dφ m xL =
証明は二つの意味論的な等式の合成である。まず RefC.abs-defSet が、推移性と持ち上げられた Δ₀ の証明を用いて、DefC.defSet (RL.liftFo φ h) への所属を、表示された要素における mapFo DefC.ι (RL.liftFo φ h) の周囲での充足と同一視する。次に satBridge が、その周囲の命題を、もとの論理式の構成可能モデル内部での充足と同一視する。定義可能性によってまず周囲の階層へ到達し、モデルの絶対性が最後のつながりを与える、という順序が要点である。
RefC.abs-defSet (RL.liftFo φ h) (RL.Δ₀-liftFo h dφ) m ∙ satBridge φ h dφ m xL
演算 carve は DefC.defSet そのものであり、残りの構成で使うために安定した名前を与えたものである。不透明に指定しても集合は変わらず、新しい存在原理も加わらない。自動的な展開を止めるだけである。数学的には carve ψ は引き続き、段階の表示上の一変数論理式 ψ が Lset σ から選び出す部分集合である。続く補題が、この部分集合を使うために必要な所属と構成可能性の事実を与える。
opaque
carve : Formula ⟪ Lset σ ⟫ 1 → V ℓ
carve ψ = DefC.defSet ψ
論理式 ψ 自身が、carve ψ が Lset σ の定義可能部分集合であることを証言する。構成子 𝒟ₒ-intro が要求するのは、そのような論理式と、その defSet と対象集合との外延的な等式が単に存在することである。そこで明示的な組 (ψ , refl) を∣ ψ , refl ∣₁ として命題的切り詰めに入れる。その結果、所属命題carve ψ ∈ 𝒟ₒ (Lset σ) は、どの論理式が定義したかを保持しない。この補題は、後で 𝒟ₒ→isL が構成可能性を導くための前提を与える。この行は命題的切り詰めを導入するだけで、そこから論理式を除去して取り出すことはしない。
opaque
unfolding carve
carve∈𝒟ₒ : (ψ : Formula ⟪ Lset σ ⟫ 1) → ⟨ carve ψ ∈ 𝒟ₒ (Lset σ) ⟩
carve∈𝒟ₒ ψ = 𝒟ₒ-intro (Lset σ) (DefC.defSet ψ) ∣ ψ , refl ∣₁
DefC.defSet が作る定義可能部分集合は、すべて周囲の集合 Lset σ に含まれる。補題 carve⊆ は、この包含を不透明な名前について記録する。DefC.defSet⊆A によって y ∈ carve ψ から y ∈ Lset σ を得る。この包含は、y が構成可能モデルで何らかの論理式を満たすかどうかには依存しない。defSet が段階の表示された要素だけを走るという定義から従う。
carve⊆ : (ψ : Formula ⟪ Lset σ ⟫ 1) (y : V ℓ) → ⟨ y ∈ carve ψ ⟩
→ ⟨ y ∈ Lset σ ⟩
carve⊆ ψ y mem = DefC.defSet⊆A ψ y mem
carveSat の順向きの読みは、切り出された集合への所属をモデルでの充足へ変える。表示された要素が carve (RL.liftFo φ h) に属するなら、hProp の等式 carveSat に沿う置換によって、対応するモデル要素が φ を満たす証明が得られる。ここで新しい論理的含意を証明しているのではない。subst は、すでに得た等式の左端の要素を右端へ輸送するだけである。
imageOut : (φ : Formula S 1) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
(m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
→ ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo φ h) ⟩
→ ⟨ ((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ ⟩
imageOut φ h dφ m xL mem = subst ⟨_⟩ (carveSat φ h dφ m xL) mem
逆向きの読みは、同じ等式を反対向きにたどる。組にされた表示要素による φ の充足を sym (carveSat ...) に沿って輸送すると、切り出された集合への所属が得られる。imageOut と imageIn は合わせて点ごとの対応の両方向を与えるが、この時点では固定した段階に表示される要素だけが対象である。任意の充足するモデル要素をそこで表示できることは、後の cover の議論が保証する。
imageIn : (φ : Formula S 1) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
(m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
→ ⟨ ((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ ⟩
→ ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo φ h) ⟩
imageIn φ h dφ m xL sat = subst ⟨_⟩ (sym (carveSat φ h dφ m xL)) sat
充足は、モデル要素が携える証明成分には依存しない。各 isL x は命題なので、基礎集合の等式 u .fst ≡ v .fst は Σ≡Prop により u ≡ v へ持ち上がり、充足の証明は得られた一要素環境の等式に沿って輸送される。証明本体は dφ を参照しないため、この輸送は数学的には任意の論理式について成り立つ。Δ₀ の引数は証明で使われないまま文に残っており、証明は排中律も使わない。
opaque
⊨-transport : (φ : Formula S 1) (dφ : Δ₀ φ) (u v : S) → u .fst ≡ v .fst
→ ⟨ (u ∷ []) ⊨ φ ⟩ → ⟨ (v ∷ []) ⊨ φ ⟩
⊨-transport φ dφ u v p =
subst (λ z → ⟨ (z ∷ []) ⊨ φ ⟩) (Σ≡Prop (λ x → (isL x) .snd) p)
一つの段階で分出する
各添字 m : ⟪ Lset σ ⟫ は、段階の実際の要素を表示する。標準的な小さい所属の証明 ∈ₛ⟪ Lset σ ⟫↪ m は、∈∈ₛ の第二の向きによって周囲の命題⟪ Lset σ ⟫↪ m ∈ Lset σ へ変換される。σ は順序数なので、Lset→isL σ oσ はこの段階への所属を構成可能性の証明へ変え、表示された集合を S の要素として組にできるようにする。固定した段階の構成で oσ が使われるのはこの箇所である。
private
memberIsL : (m : ⟪ Lset σ ⟫) → ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩
memberIsL m = Lset→isL σ oσ (⟪ Lset σ ⟫↪ m)
(∈∈ₛ {a = ⟪ Lset σ ⟫↪ m} {b = Lset σ} .snd (∈ₛ⟪ Lset σ ⟫↪ m))
固定した段階での一般構成は、一変数論理式 χ、そのすべての定数が Below を満たす証明、Δ₀ の証明、および χ を満たす各モデル要素の基礎集合が Lset σ に属するという被覆条件を受け取る。目標は、充足述語を実現するものの可縮な型を与えることである。uniqueL はこの目標を、点ごとの所属仕様をもつ一つの明示的なモデル要素へ帰着する。命題外延性が各 z での二方向の含意を真理値のパスにし、集合外延性が実現する集合の一意性を与える。
carveAt : (χ : Formula S 1) (hχ : BoundedFo Below χ) (dχ : Δ₀ χ)
(cover : (z : S) → ⟨ (z ∷ []) ⊨ χ ⟩ → ⟨ z .fst ∈ Lset σ ⟩)
→ isContr (SetOf (λ z → (z ∷ []) ⊨ χ))
carveAt χ hχ dχ cover = uniqueL (λ z → (z ∷ []) ⊨ χ) (replElt , spec)
where
選ばれた実現要素の基礎集合は carve (RL.liftFo χ hχ) である。定数の境界 hχ により、各定数を段階へ付け替えることが正当化される。carve∈𝒟ₒ は、得られた defSet がLset σ の定義可能冪集合に属することを証明する。この所属に 𝒟ₒ→isL σ oσ を適用すると、モデル要素の第二成分が得られる。したがって定義可能性が構成可能な実現要素の存在を与え、その正確な外延は別に spec が証明する。
replElt : S
replElt = carve (RL.liftFo χ hχ)
, 𝒟ₒ→isL σ oσ (carve (RL.liftFo χ hχ)) (carve∈𝒟ₒ (RL.liftFo χ hχ))
仕様は各モデル要素 z について、z が replElt に属することと、z が χ を満たすこととの間のパスを与える。順向きの含意は z ∈ˢ replElt から始まる。replElt の基礎集合は切り出された集合なので、carve⊆ が z .fst を Lset σ に入れ、標準的な表示がその集合を指す添字 m を与える。切り出された集合への所属を表示された代表へ輸送すると、imageOut がそこでの充足を与え、⊨-transport が基礎集合の等式に沿ってそれを z へ戻す。この向きでは所属自体から必要な段階の境界が得られるため、被覆仮定は使わない。
spec : (z : S) → (z ∈ˢ replElt) ≡ ((z ∷ []) ⊨ χ)
spec z = ⇔toPath fwd bwd
where
fwd : ⟨ z ∈ˢ replElt ⟩ → ⟨ ((z ∷ []) ⊨ χ) ⟩
fwd z∈ = ⊨-transport χ dχ (⟪ Lset σ ⟫↪ m , xL) z q (imageOut χ hχ dχ m xL m∈)
これらの局所データは、標準的な表示へ移る過程を明示する。まず fz∈Lσ は、切り出された集合が段階に含まれることから従う。この所属に ∈-asFiber を適用すると、添字 m : ⟪ Lset σ ⟫ とパス q : ⟪ Lset σ ⟫↪ m ≡ z .fst が得られる。両者は一つの所属ファイバーの二つの射影なので、選択原理は使われない。パス qは互いに逆の向きに使われる。まず切り出された集合への所属を表示された集合へ移し、次に組にした代表での充足を z へ戻す。
where
fz∈Lσ = carve⊆ (RL.liftFo χ hχ) (z .fst) z∈
m = ∈-asFiber {a = z .fst} {b = Lset σ} fz∈Lσ .fst
q : ⟪ Lset σ ⟫↪ m ≡ z .fst
q = ∈-asFiber {a = z .fst} {b = Lset σ} fz∈Lσ .snd
仕様の順方向は、二つの段階で締めくくられる。層の中で表されたメンバーが、モデルの元として梱包され、その構成可能性は段階そのものから来る。そして、その表されたメンバーに対して証明された、刻まれた集合への所属が、名指しの等式に沿って、もとの元へ運ばれる。これで順方向は完成である。刻まれた集合の元は、モデルの中で、自分自身のもとで論理式を満たすのである。
xL = memberIsL m
m∈ : ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo χ hχ) ⟩
m∈ = subst (λ w → ⟨ w ∈ carve (RL.liftFo χ hχ) ⟩) (sym q) z∈
逆方向は、覆いの仮定から始まる。ここで覆いの仮定を使う。論理式を満たす各要素はこの段階に属すと仮定されているので、与えられた充足の証明を適用すると。すると、段階への所属の繊維が、標準的な代表の添字を取り戻す。
bwd : ⟨ ((z ∷ []) ⊨ χ) ⟩ → ⟨ z ∈ˢ replElt ⟩
bwd qz = subst (λ w → ⟨ w ∈ carve (RL.liftFo χ hχ) ⟩) q m∈
where
fz∈Lσ = cover z qz
m = ∈-asFiber {a = z .fst} {b = Lset σ} fz∈Lσ .fst
代表は一つの等式によって名指され、充足はその代表のところへ移される。充足が底の集合のみに依存するのであるから、底の集合のあいだの等式で十分である。代表は、それ自身の構成可能性を添えて、モデルの元として梱包され、論理式は、もとの元の代わりに、代表について成り立つ。
q : ⟪ Lset σ ⟫↪ m ≡ z .fst
q = ∈-asFiber {a = z .fst} {b = Lset σ} fz∈Lσ .snd
xL = memberIsL m
satz : ⟨ ((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ χ ⟩
satz = ⊨-transport χ dχ z (⟪ Lset σ ⟫↪ m , xL) (sym q) qz
ここで定義可能性の順方向を使う。代表は論理式を満たすので、代表は刻まれた集合に属する。そして名指しの等式が、この所属をもとの元へ運び戻す。両方向がそろい、仕様は、すべての元において、二つの命題の相等となる。刻まれた実現への所属と、モデルの中で論理式を満たすこととの相等である。
m∈ : ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo χ hχ) ⟩
m∈ = imageIn χ hχ dχ m xL satz
段階での分出は、先の構成を部分集合に特化したものである。仮定は、始集合がすでに段階の中にあるということ。その論理式は、「始集合への所属」と与えられた論理式との連言であり、所属の原子が有界であり、連言が有界性を保つので、有界な論理式である。定数も有界である。始集合が段階の下に供給され、論理式の定数には証明書が付いていたからである。こうして固定段階の定理は、モデルの欄の分出が求める、ちょうどあの可縮な実現を返す。
separateAt : (a : S) (fa∈σ : ⟨ a .fst ∈ Lset σ ⟩)
(φ : Formula S 1) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
→ isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)))
separateAt a fa∈σ φ h dφ =
carveAt ((var zero ∈̇ con a) ∧̇ φ) ((tt* , fa∈σ) , h) (δ-∧ δ-∈ dφ)
固定段階の定理の覆いの仮定は、最初の連言だけによって解除される。連言を満たす元は「始集合への所属」を満たし、始集合は段階の中にあり、段階は推移的である。ゆえにその元も段階の中にある。分出の述語における所属の連言が飾りではない数学的理由は、これである。切り出そうとしている層の内側へ、すべての候補を運び込むのが、この連言なのである。
(λ z q → layer-trans (Lset-layer σ) {x = a .fst} {y = z .fst} (q .fst) fa∈σ)
論理式を収める段階を求める
独立に選ばれた上界を比較するため、層の条件を順序数の添字でパラメータ化する。その数学的内容は先ほどと同じで、元の底の集合が添字の指す層に属するということである。こうして、先に選んだ一つの層を変数として扱い、後の探索で層について量化できるようになる。
Below′ : V ℓ → S → Type (ℓ-suc ℓ)
Below′ σ c = ⟨ c .fst ∈ Lset σ ⟩
最初の持ち上げの補題は、項の有界性を指標に沿って運ぶ。ある段階の指標が別の指標に先行すれば、第一の層の下にある定数はすべて、第二の層の下にもある。塔の狭い増大によるものである。そして項の有界性の証明書は、各定数ごとにこの点ごとの単調性を施すことで、より大きな指標へ運ばれる。項そのものは変わらず、有界性の証明だけが輸送される。
liftTmTo : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → ∀ {n} (t : Term S n)
→ BoundedTm (Below′ σ) t → BoundedTm (Below′ β) t
liftTmTo {σ} {β} σ∈β t h =
BoundedTm-mono {P = Below′ σ} {Q = Below′ β}
(λ (c : S) h' → Lset-mono {α = β} {β = σ} σ∈β {x = c .fst} h') t h
第二の持ち上げの補題は、論理式について同じことをする。すべての定数がある段階の指標の下にある論理式は、それより後のどんな指標の下でも、その性質を保つ。証明は、論理式のすべての定数の位置で、項の補題を施すものである。この二つの持ち上げの補題があれば、ある段階で得た有界性の証明を、残りのデータのために選んだ任意の後の段階へ輸送できる。
liftFoTo : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → ∀ {n} (φ : Formula S n)
→ BoundedFo (Below′ σ) φ → BoundedFo (Below′ β) φ
liftFoTo {σ} {β} σ∈β φ h =
BoundedFo-mono {P = Below′ σ} {Q = Below′ β}
(λ (c : S) h' → Lset-mono {α = β} {β = σ} σ∈β {x = c .fst} h') φ h
定数の上界の探索は項から始まり、二つの場合は明確に異なる。定数には、それ自身が初めて属する層を上界として、その添字の順序数性と定数の所属証明を添える。変数は定数を含まないため、空の層と自明な証明を返す。ここには上界を求めるべき定数がなく、変数の値が空集合に属すとは主張しない。
mkBoundedTm : ∀ {n} (t : Term S n) → Σ[ σ ∶ V ℓ ] (IsOrd σ × BoundedTm (Below′ σ) t)
mkBoundedTm (con c) = stage (c .fst) (c .snd)
, (stage-ord (c .fst) (c .snd) , stage-mem (c .fst) (c .snd))
mkBoundedTm (var i) = ∅ , (∅-ord , _)
二つの探索結果をまとめる操作は、一度だけ、一般的に述べられる。指標に沿って持ち上げられるどんな二種類の証明書にも対応する。入力は、結果の対である。おのおの、順序数の指標とその順序数性と、証明書。出力は、共通の指標における一つの結果で、二つの証明書がともにそこへ運ばれる。持ち上げの二つの操作がパラメータなので、同じ構成を、二つの項、二つの論理式、または項と論理式に適用できる。
private
mkBounded : ∀ {ℓc ℓd} {C : V ℓ → Type ℓc} {D : V ℓ → Type ℓd}
→ (liftC : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → C σ → C β)
→ (liftD : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → D σ → D β)
→ (r₁ : Σ[ σ ∶ V ℓ ] (IsOrd σ × C σ))
共通上界の構成は三段階からなる。二つの指標の限界を取る。それは両方の上にある順序数である。第一の指標がその限界に先行し、第二もそうであることを記録する。そして、この二つの包含関係に沿って、持ち上げの操作を施し、二つの証明書がともに共通の指標を述べるようにする。証明書について使われるのは、持ち上げられるという形だけであり、それ以外の性質は何も使わない。
→ (r₂ : Σ[ σ ∶ V ℓ ] (IsOrd σ × D σ))
→ Σ[ σ ∶ V ℓ ] (IsOrd σ × (C σ × D σ))
mkBounded liftC liftD r₁ r₂ = b .fst , (b .snd .fst ,
( liftC (b .snd .snd .fst) (r₁ .snd .snd)
, liftD (b .snd .snd .snd) (r₂ .snd .snd) ))
限界そのものは、順序数の章による、二つの順序数の合併である。どちらの順序数もそれに先行するような順序数である。これが、この再帰に必要な唯一の順序数論的事実であり、構成的なものである。古典的なパラメータが入り込むのはここではなく、もっと早く、各定数の最も早い段階が名指されたところなのである。
where
b = bound2 (r₁ .fst) (r₂ .fst) (r₁ .snd .fst) (r₂ .snd .fst)
論理式の上の探索は、構文を再帰する。二つの原子的な形は、それぞれの二つの項の限界をまとめる。命題の結合子は、その二つの部分論理式の限界をまとめる。いずれの場合も、仕事をするのは、先ほどのまとめ役であり、有界性の証明は共通の添字へ輸送される。
mkBoundedFo : ∀ {n} (φ : Formula S n) → Σ[ σ ∶ V ℓ ] (IsOrd σ × BoundedFo (Below′ σ) φ)
mkBoundedFo (t ∈̇ u) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftTmTo σ∈β u) (mkBoundedTm t) (mkBoundedTm u)
mkBoundedFo (t ≐ u) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftTmTo σ∈β u) (mkBoundedTm t) (mkBoundedTm u)
mkBoundedFo (φ ∧̇ ψ) = mkBounded (λ σ∈β → liftFoTo σ∈β φ) (λ σ∈β → liftFoTo σ∈β ψ) (mkBoundedFo φ) (mkBoundedFo ψ)
mkBoundedFo (φ ∨̇ ψ) = mkBounded (λ σ∈β → liftFoTo σ∈β φ) (λ σ∈β → liftFoTo σ∈β ψ) (mkBoundedFo φ) (mkBoundedFo ψ)
残りの場合は、その非対称が教訓的である。偽の論理式は定数を含まないので、空の段階が上界になる。非有界量化子の定数の上界は、本体の上界と同じである。量化子そのものは定数をひとつも導入しないので、再帰は、その下を何も触れずに通過する。有界量化子は、さらにその限定項を含む。その範囲を定める項が一つの定数を名指すので、項の限界と本体の限界とをまとめるのである。
mkBoundedFo (φ ⇒̇ ψ) = mkBounded (λ σ∈β → liftFoTo σ∈β φ) (λ σ∈β → liftFoTo σ∈β ψ) (mkBoundedFo φ) (mkBoundedFo ψ)
mkBoundedFo ⊥̇ = ∅ , (∅-ord , _)
mkBoundedFo (∃̇ φ) = mkBoundedFo φ
mkBoundedFo (∀̇ φ) = mkBoundedFo φ
mkBoundedFo (∀̇∈ t φ) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftFoTo σ∈β φ) (mkBoundedTm t) (mkBoundedFo φ)
有界存在は、有界全称量化子と同じふるまいをする。範囲を定める項の限界と、本体の限界とがまとめられる。この探索全体の性質のうち、二つの独立した概念を分けるものを強調しておく。この再帰が調べるのは定数だけである。だから、非有界な量化子を含む論理式に対しても、うまく行く。したがって、ここで産み出される証明書は、論理式が有界かどうかについて何も語らない。定数がある段階の下にあることと、量化子が有界であることは、終始、別々の概念なのである。
mkBoundedFo (∃̇∈ t φ) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftFoTo σ∈β φ) (mkBoundedTm t) (mkBoundedFo φ)
Δ₀ 分出公理
有界な分出が、いま、完全な形で述べられる。始集合と、量化子がすべて有界であるような一変数論理式に対して、「始集合の要素であり論理式を満たす」という述語は、モデルの元による可縮な実現をもつ。段階を定めた後、固定段階での分出定理を一度適用する。
separateΔ₀ : (a : S) (φ : Formula S 1) → Δ₀ φ
→ isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)))
separateΔ₀ a φ dφ = AtStage.separateAt σ oσ a fa∈σ φ h dφ
where
rφ = mkBoundedFo φ
この層は二つの上界から定まる。先に構成した探索が論理式の定数を抑える上界を与え、既に得られている層の割り当てが始集合を含む最初の層を与える。二つの添字を併合し、論理式の証明書をその層まで持ち上げる。これにより、論理式の定数と始集合は同じ上界の下に置かれる。
sa = stage (a .fst) (a .snd)
bb = bound2 (rφ .fst) sa (rφ .snd .fst) (stage-ord (a .fst) (a .snd))
σ = bb .fst
oσ = bb .snd .fst
h = liftFoTo {σ = rφ .fst} {β = σ} (bb .snd .snd .fst) φ (rφ .snd .snd)
始集合自身の位置は別に扱う。始集合はそれが初めて現れる層に属し、併合から得られる包含関係によって、この所属を共通の層まで持ち上げる。これが固定層の定理に必要な被覆の仮定であり、塔の単調性と層の割り当てに伴う証明書から直接得られる。
fa∈σ : ⟨ a .fst ∈ Lset σ ⟩
fa∈σ = Lset-mono {α = σ} {β = sa} (bb .snd .snd .snd) (stage-mem (a .fst) (a .snd))
Δ₀ 置換公理
有界な置換は、その関数性の仮定とともに述べられる。始集合と、量化子がすべて有界な二変数論理式を取り、各要素に対応する値の繊維が可縮であると仮定する。このとき、像の述語はモデルの元による可縮な実現をもつ。証明は述語の相等に沿って実現可能性を輸送する。関数性によって関連する値に共通の上界を与え、その上界を得た後は通常の分出によって像を集める。
replaceΔ₀ : (a : S) (φ : Formula S 2) → Δ₀ φ
→ ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∶ S ] ⟨ (x ∷ y ∷ []) ⊨ φ ⟩))
→ isContr (SetOf (ReplImage a φ))
replaceΔ₀ a φ dφ fc =
subst (λ Q → isContr (SetOf Q)) (sym Q≡)
関数像の上界に関する定理を、関係の第一の位置を始域とする順序で適用すると、共通の像の段階、その順序数性、覆いの事実が得られる。そして、その段階をモデルの元として梱包したところで、一変数の像の論理式に対して、完全な有界分出が施される。この論理式の有界性の証拠は、有界存在の場合のものである。加わった量化子は一つだけで、それが源によって有界にされているからである。
(separateΔ₀ (LsetS βimg βimg-ord) imageFo (δ-∃∈ dφ))
where
module I = FunctionalImage a (λ x y → (x ∷ y ∷ []) ⊨ φ) fc
open I using ( βimg; βimg-ord; range∈βimg )
一変数の像の論理式の意味は次のとおりである。それは、対象言語でこう言う。始集合のどこかのメンバーが、外側の候補と関係づけられる、と。そして有界存在が、そのメンバーを環境の最初の枠へ押し込む。ここでの有界存在は、対象言語自身の量化子である。一方、像の述語の外側の存在は、ホストレベルの切り詰められた存在である。二者は意味においては意味論を通して一致するが、同じ統語的な対象ではない。両者を区別することで、次の等式を正確に述べられる。
imageFo : Formula S 1
imageFo = ∃̇∈ (con a) φ
守衛つきの述語は、構成が検証できるものを集める。候補が、梱包された共通の像の段階の中にあり、一変数の像の論理式を満たす、ということ。段階への所属を表す連言は分出の上界を与え、もう一方の連言は実際の像を記述する。したがって、後で覆いの定理を用いて段階の条件を取り除ける。
BoundedImage : S → hProp (ℓ-suc ℓ)
BoundedImage y = (y ∈ˢ LsetS βimg βimg-ord) ⊓ ((y ∷ []) ⊨ imageFo)
二つの述語の相等は点ごとに成り立ち、その二方向は手間が違う。順方向。切り詰められた源の証人から、守衛つきの述語へ。消去が正当なのは、守衛つきの述語が命題だからである。覆いの事実が段階への所属を供給し、同じ始域の要素と充足の証明を、論理式が要求する位置の順序で切り詰めの中へ戻す。逆方向には、何も要らない。候補における像の論理式の充足は、その意味論により、ちょうどその候補における像の述語だからである。段階の連言は捨てられ、第二の連言がそのまま主張となる。始域が第一の位置を占めるため。変数の入れ替えは、どこにも要らないのである。
Q≡ : ReplImage a φ ≡ BoundedImage
Q≡ = funExt (λ y → ⇔toPath (into y) (λ p → p .snd))
where
into : (y : S) → ⟨ ReplImage a φ y ⟩ → ⟨ BoundedImage y ⟩
into y = rec₁ ((BoundedImage y) .snd) λ { (x , (x∈a , h)) →
ReplImage a φ に属する候補 y について、始域の要素 x、所属の証明 x∈a、充足の証明 h は、命題的切り詰めのもとでのみ与えられる。BoundedImage y は命題なので、rec₁ は、その二つの連言を構成する間にこれらのデータを使える。第一の成分は range∈βimg から得られる。関数性により、a の要素と関係するすべての値は Lset βimg に属する。第二の成分では、同じ x、x∈a、h を命題的切り詰めの中へ戻す。imageFo = ∃̇∈ (con a) φ の意味論により、これはちょうど y が imageFo を満たすことの証明である。したがって、始域の要素が切り詰められていないデータとして返されることはない。
これで ReplImage a φ y から BoundedImage y への含意が完成する。段階への所属の成分を捨てる逆向きの含意と合わせて Q≡ が得られ、sym Q≡ に沿う輸送によって replaceΔ₀ が証明される。正確には、仮定 lem : LEM (ℓ-suc ℓ)、φ の Δ₀ 証人、および各 x ∈ˢ a における値のファイバーの可縮性のもとで、結論は isContr (SetOf (ReplImage a φ)) である。これはここで述べた Δ₀ 置換定理である。この枝は新たな古典的原理を導入しないが、range∈βimg が用いる共通の段階の構成は lem に依存する。
range∈βimg x x∈a y h , ∣ x , (x∈a , h) ∣₁ }
まとめ
有界な分出と有界な置換は、同じ方針に従う。まず始集合と論理式の定数を一つの順序数層の下に置き、置換ではさらに関係するすべての値も同じ層の下に収める。次に定義可能性によってその層の内部で必要な部分集合を作り、変名と Δ₀ 絶対性によって、その所属関係を構成可能モデルにおける充足と同一視する。こうして、唯一のホスト側の仮定 lem : LEM (ℓ-suc ℓ) のもとで separateΔ₀ と replaceΔ₀ が得られる。