--- title: "符号化された単射" module: L.Coding.Injection lang: ja site: "Bedrock" description: "符号化された単射" stage: "順序数，単射，基数" reading_order: 88 canonical: https://bedrock.institute/ja/L.Coding.Injection.html html: L.Coding.Injection.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Injection.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Model, V.Presentation] routes: [cardinal-tools] translations: [https://bedrock.institute/en/L.Coding.Injection.md, https://bedrock.institute/zh/L.Coding.Injection.md] agent_guide: https://bedrock.institute/llms.txt license: "CC-BY-NC-SA-4.0" --- ```agda {-# OPTIONS --cubical --safe --guardedness #-} ``` # 符号化された単射 ```agda open import Base.Prelude open import Base.Classical using ( LEM ) ``` この構成自体は構成的である。周囲の議論は `LEM (ℓ-suc ℓ)` を仮定しているが、以下の証明はそれを使わない。グラフの値の存在は切り詰められているが、一価性により像のファイバー全体が命題になるため、選択原理なしに切り詰めを消去してその一意な要素を得られる。 ```agda module L.Coding.Injection {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where ``` ```agda open import FOL.ZFStructure using ( module hPropView ) open import FOL.Syntax using ( Formula; var; _≐_; _⇒̇_; ∀̇_ ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; svAt; svAt-out; domAt; domAt-in ) open import V.Presentation {ℓ} using ( member; fiber; ↪-inj ) ``` 後の基数論では、対象言語が量化できるグラフと、集合の小さな要素型の間の実際の単射という二つの表現を往復する。この溝は三層で埋める。まず対象言語には、グラフが単射であることを言う論理式、すでにある一価性の条項の鏡像が必要になる。次に、一価性とちょうどの定義域を仮定すれば、グラフは値が構成可能モデルの要素にとどまる本物の関数として読める。最後にその関数は、指定された定義域と値域の標準的な小さな提示へ移る。本章は単射性の論理式を加え、Cantor-Bernstein と GCH の構成が使う二段階の読み戻しを実行する。 `S` を構成可能モデルの台とする。`S` の要素は `V ℓ` の周囲の集合と、その構成可能性の証明からなるため、グラフについての主張は第一射影について述べられる。適用、一価性、正確な定義域を表す論理式は、内部の充足をこれらの射影されたグラフの事実と結び付ける。 第二の読み戻しには標準的な提示の道具が必要である。集合はインデックス型とインデックス付けの写しで提示され、`member` はインデックスを明示的な所属証明に変え、`fiber` は逆に実際のインデックスを返す。切り詰められた存在ではない。`Σ≡Prop` は第二成分が命題のとき、依存対の等しさを第一成分の等しさへ帰着させる。像のファイバーも模型の台の対もこの仕方で扱われる。 ```agda open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ ) ``` ここでの真理値は、命題であることの証明を添えた命題であり、充足関係は `hProp` 上の論理結合子を直接使う。充足の判断 `_⊨_` は構成可能な構造 `𝒮ʟ` に対して述べられるので、`γ ⊨ svAt zero` のような判断は、妥当性の同一視を通して射影された集合についての主張になる。 ```agda open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ ) open hPropView 𝒮ʟ using ( S ) ``` 有界絶対性は、構成可能モデルでの充足を、割り当てを `fst` で射影した後の充足と結び付ける。この橋は妥当性定理を適用する箇所で用いられるが、それだけで `Extract.toFun` が単射になるわけではない。単射性は後で独立な仮定 `ij` として加わる。 ```agda module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL using () renaming ( _⊨ᵐ_ to _⊨_ ) ``` ## 対象言語における単射性 妥当性の観点では、## 対象言語における単射性 一価的なグラフは引数を固定して値を比較する。同じ第一成分を持つ二つの項目の第二成分は一致する、というものである。単射性はその鏡像で、値を固定して引数を比較する。具体的には、`(x, y)` と `(x', y)` がともにグラフに属するなら、`x` と `x'` の第一成分は等しくなければならない。これを対象言語の論理式として述べることで、基数論はモデルの内部で単射なグラフを量化できるようになる。 論理式は割り当て `x′ ∷ x ∷ y ∷ γ` を束縛する。スロット 0 は `x′`、1 は `x`、2 は `y` で、もとのグラフのスロット `f` は `f + 3` になる。二つの前提は `(x,y)` と `(x′,y)` がそのグラフに属すことを述べ、結論は `x` と `x′` を等置する。したがって出力を固定して入力を比較し、一価性とちょうど対をなす。 ```agda injAt : ∀ {n} → Fin n → Formula S n injAt f = ∀̇ (∀̇ (∀̇ ( appAt (suc (suc (suc f))) (suc zero) (suc (suc zero)) ⇒̇ (appAt (suc (suc (suc f))) zero (suc (suc zero)) ⇒̇ (var (suc zero) ≐ var zero))))) ``` 読み戻しでは変数の添字 `f` と模型要素からなる割り当て `γ` を固定する。`Holds₀ x y` は射影された事実で、`x` と `y` の底の集合の順序対が底のグラフ、すなわち変数 `f` が `γ` から選ぶ項目に属すということである。以下の両方向は、適用の条項の充足の判断をこの `Holds₀` と比べるもので、妥当性のパスが議論の要になる。
```agda module _ {n : ℕ} (f : Fin n) (γ : Vec S n) where ```
```agda private Holds₀ : S → S → Type (ℓ-suc ℓ) Holds₀ x y = ⟨ pr (x .fst) (y .fst) ∈ (lookup f γ) .fst ⟩ at₁ : (y x x' : S) ``` パス `at₁` は、拡張された割り当て `x' ∷ x ∷ y ∷ γ` での最初の適用条項の妥当性を記録する。そこでの充足は、対 `(x, y)` のグラフへの所属という射影された事実と同一視される。この同一視は命題どうしの等しさであり、所定の変数の添字での `appAt-adequate` によって与えられるので、どちらの方向へも輸送できる。 ```agda → ((x' ∷ x ∷ y ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc zero) (suc (suc zero))) ≡ (pr (x .fst) (y .fst) ∈ (lookup f γ) .fst) at₁ y x x' = appAt-adequate (suc (suc (suc f))) (suc zero) (suc (suc zero)) (x' ∷ x ∷ y ∷ γ) at₂ : (y x x' : S) ``` パス `at₂` はもう一つの条項についての同じ主張である。変数 `0` と `2` での適用の充足は、対 `(x', y)` のグラフへの所属という射影された事実と等しくなる。二つのパスの違いは、対の符号にどちらの第一成分を入れるかだけで、これこそ単射性が利用する非対称である。 ```agda → ((x' ∷ x ∷ y ∷ γ) ⊨ appAt (suc (suc (suc f))) zero (suc (suc zero))) ≡ (pr (x' .fst) (y .fst) ∈ (lookup f γ) .fst) at₂ y x x' = appAt-adequate (suc (suc (suc f))) zero (suc (suc zero)) (x' ∷ x ∷ y ∷ γ) injAt-out : ⟨ γ ⊨ injAt f ⟩ ``` 外向きの `injAt-out` は、論理式が `γ` で成り立つ証明と二つの所属の事実 `Holds₀ x y`、`Holds₀ x' y` から出発する。三つの量化子を具体化すると、拡張された割り当てでの含意の本体の充足証明が得られ、所属の事実を `at₁` と `at₂` の逆向きに輸送して、二つの前件の条項の充足証明に変える。最後の `x .fst ≡ x' .fst` はモデルの等しさの中で読み取る。 ```agda → (y x x' : S) → Holds₀ x y → Holds₀ x' y → x .fst ≡ x' .fst injAt-out h y x x' p q = h y x x' (subst ⟨_⟩ (sym (at₁ y x x')) p) (subst ⟨_⟩ (sym (at₂ y x x')) q) injAt-in : ((y x x' : S) → Holds₀ x y → Holds₀ x' y → x .fst ≡ x' .fst) → ⟨ γ ⊨ injAt f ⟩ ``` 内向きの `injAt-in` は同じ輸送を順方向に行う。`Holds₀` についての射影された単射性を仮定として与えると、二つの所属の事実を `at₁` と `at₂` そのものに沿って輸送して二つの前件の充足を得、仮定が論理式の結論の求める等しさを出す。二つの方向を合わせて、この論理式が単射性に対して過不足なく妥当であることが分かる。 ```agda injAt-in h y x x' p q = h y x x' (subst ⟨_⟩ (at₁ y x x') p) (subst ⟨_⟩ (at₂ y x x') q) ```
## モデルに値を取る単射を取り出す グラフが一価でちょうどの定義域を持つと仮定すると、定義域の各要素はグラフの中に何らかの像を持つが、それはもっぱら存在するだけの像である。定義域への所属が与えるのは命題の切り詰めであって、選ばれた証人ではない。一価性がこの状況を変える。入力を固定すると、「出力と、その対がグラフに属する証明」の組の型が命題であることが示され、切り詰められた値はいつでも命題へ消去できる。したがってグラフはモデルに値を取る本物の関数を与え、単射性まで仮定すれば本物の単射になる。この第一の読み戻しは値を台の要素のまま保つ形で、後の証明がコード化されたグラフを参照し続けるときに使われる。 この節は、グラフ `F` と定義域 `D` を模型の要素として、二つの充足の仮定とともに取る。変数ゼロでのグラフの一価性と、`D` のすべての要素が `F` の下で値を持つと言うちょうどの定義域の条項である。環境 `γ` はそれらを、充足の判断が期待する固定の順序でまとめる。
```agda module Extract (F D : S) (sv : ⟨ (F ∷ D ∷ []) ⊨ svAt zero ⟩) (dm : ⟨ (F ∷ D ∷ []) ⊨ domAt zero (suc zero) ⟩) where ```
```agda γ : Vec S 2 γ = F ∷ D ∷ [] ``` `Holds x y` は、底の対が底のグラフに属すという射影された所属である。ファイバー `Fib x` は出力 `y` にこの証明を添えた組で、その要素はグラフが `x` で取る候補の値であり、それぞれが本当に値であることの証明書を伴う。 ```agda Holds : S → S → Type (ℓ-suc ℓ) Holds x y = ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩ Fib : S → Type (ℓ-suc ℓ) Fib x = Σ[ y ∶ S ] Holds x y isPropFib : (x : S) → isProp (Fib x) ``` `Fib x` が命題であることを示すには、`(y,p)` と `(y′,q)` を比較する。一価性からまずパス `y .fst ≡ y′ .fst` が得られる。内側の `Σ≡Prop` は、`S` の要素の第二成分である `isL` の証明が命題であることを使い、このパスを `y ≡ y′` へ持ち上げる。外側の `Σ≡Prop` は、グラフ所属の証明が命題であることを使い、その等しさを `Fib x` の二要素の等しさへ持ち上げる。これは別々の二つの証明無関係性の段階であり、周囲の集合の等しさが構成可能性だけから従うという意味ではない。 ```agda isPropFib x (y , p) (y' , q) = Σ≡Prop (λ w → (pr (x .fst) (w .fst) ∈ F .fst) .snd) (Σ≡Prop (λ z → (isL z) .snd) (svAt-out zero γ sv x y y' p q)) toVal : (x : S) → ∥ Fib x ∥₁ → Fib x toVal x = rec₁ (isPropFib x) (λ z → z) ``` `Fib x` が命題なので、`toVal` は値の切り詰められた存在 `∥ Fib x ∥₁` を実際のファイバーへ消去できる。選択がここに隠れていそうで、そうではない。命題の切り詰めは命題値の任意の対象へ消去できるので、排中律も代表的な元の選出も要らない。定義域 `Dom` は入力に `D` への所属の射影された証明を添えてまとめ、`fib` は `domAt-in` から得た各入力の切り詰められた像を `toVal` に通す。 ```agda Dom : Type (ℓ-suc ℓ) Dom = Σ[ x ∶ S ] ⟨ x .fst ∈ D .fst ⟩ fib : (u : Dom) → Fib (u .fst) fib (x , m) = toVal x (domAt-in zero (suc zero) γ dm x m) toFun : Dom → S ``` 関数 `toFun` は定義域の要素を、その一意なファイバーに含まれる出力 `y : S` へ送る。捨てるのは付随するグラフ所属の証明だけで、出力はモデルの要素のままなので構成可能性の証明書を保持する。定理 `toFun-graph` は、捨てた所属の証拠をファイバーの第二成分として取り出す。 ```agda toFun u = (fib u) .fst toFun-graph : (u : Dom) → Holds (u .fst) (toFun u) toFun-graph u = (fib u) .snd ```
```agda module _ (ij : ⟨ γ ⊨ injAt zero ⟩) where ```
```agda toFun-inj : (u v : Dom) → (toFun u) .fst ≡ (toFun v) .fst ``` グラフの単射性まで仮定すると、`toFun-inj` は値の等しさを引数の等しさに変える。`toFun u` と `toFun v` の底の集合が等しければ、`u` のグラフの等式をそのパスに沿って輸送して、両方の項目が同じ値、すなわち `toFun v` について語るようにし、`injAt-out` が二つの引数を比較して `u .fst` と `v .fst` の第一成分の等しさを返す。結果は射影された第一成分について述べられ、後続の基数論が `Dom` の要素を比較するときの形である。 ```agda → (u .fst) .fst ≡ (v .fst) .fst toFun-inj u v e = injAt-out zero γ ij (toFun v) (u .fst) (v .fst) (subst (λ w → ⟨ pr ((u .fst) .fst) w ∈ F .fst ⟩) e (toFun-graph u)) (toFun-graph v) ```
## 小さな台に制限する 関数 `toFun` は「模型の要素と所属の証明」の対に作用するが、この台は基数の議論で数えることができない。最後の段階では両端を標準的な小さな提示に置き換える。定義域は `D` のインデックス型に、値域は呼び出し側が指定する集合 `C` のインデックス型になり、呼び出し側はグラフのどの値も `C` に属すことを証明するだけで済む。グラフの三つの条項、一価性、ちょうどの定義域、単射性は、ここでまとめて仮定する。提示の層がもたらすのは明示性である。標準的な埋め込みのファイバーが命題値であるため、`D` や `C` への所属はインデックスから読み出せ、インデックスへ読み戻せる。 パラメータは、ここで働く三つの構成可能集合、グラフ `F`、定義域 `D`、値域 `C` を名指す。最初の三つの仮定は、Extract と toFun-inj が使った充足の主張そのものである。最後の `ran` が新しいもので、入力 `x` と、対 `(x, y)` がグラフに属すような値 `y` に対して、`y` の底の集合が `C` の底の集合に属すことを証明書として与える。これは値域の制限を呼び出し側の仮定として述べたもので、この節自身はグラフが特定の値域を持って作られたと仮定しない。
```agda module Small (F D C : S) (sv : ⟨ (F ∷ D ∷ []) ⊨ svAt zero ⟩) (dm : ⟨ (F ∷ D ∷ []) ⊨ domAt zero (suc zero) ⟩) (ij : ⟨ (F ∷ D ∷ []) ⊨ injAt zero ⟩) (ran : (x y : S) → ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩ → ⟨ y .fst ∈ C .fst ⟩) where ```
内側のモジュールは、`F` と `D` と先の二つの充足の証明で Extract を改めて開くので、前節の構成はすべて接頭辞付きの名前で使える。そして `toS` は `D` の標準的な提示のインデックス `m` を模型の要素に変える。第一成分は提示された集合そのものであり、第二成分はその構成可能性の証明書で、`isL-trans` により、明示的な所属 `member (D .fst) m` と `D` 自身が構成可能である証明書から得られる。推移性はまさに必要な原理である。構成可能集合の要素は構成可能である。 ```agda module E = Extract F D sv dm toS : ⟪ D .fst ⟫ → S toS m = ⟪ D .fst ⟫↪ m , isL-trans {x = D .fst} {y = ⟪ D .fst ⟫↪ m} (member (D .fst) m) (D .snd) ``` 各小さなインデックスは、Extract の意味でも定義域の要素と見なされねばならず、`at` がその組を与える。模型の要素 `toS m` と明示的な所属の証明 `member (D .fst) m` である。`at m` を `E.toFun` でグラフに通すと値が得られ、値域の仮定がこの値が `C` に属すことを証明する。標準的な提示での所属 `⟪ C .fst ⟫↪ k ≡ (E.toFun (at m)) .fst` は、命題値のファイバーを持つ埋め込みのファイバーなので、`fiber` は切り詰められた存在ではなく、実際のインデックス `k` とパスの組を返す。 ```agda at : ⟪ D .fst ⟫ → E.Dom at m = toS m , member (D .fst) m fib : (m : ⟪ D .fst ⟫) → Σ[ k ∶ ⟪ C .fst ⟫ ] (⟪ C .fst ⟫↪ k ≡ (E.toFun (at m)) .fst) fib m = fiber (C .fst) ``` パスを捨てると `small` が得られる。`D` のインデックス型から `C` のインデックス型への関数で、各定義域のインデックスは、グラフの下での像に対応するインデックスへ送られる。ここで二つの表現が合流する。`small` は固定された宇宙レベルの型の間の写しであり、数え上げの議論が求める形そのものであり、保持されたパスを通してグラフと結び付いている。 ```agda (ran (toS m) (E.toFun (at m)) (E.toFun-graph (at m))) small : ⟪ D .fst ⟫ → ⟪ C .fst ⟫ small m = (fib m) .fst small-inj : (m n : ⟪ D .fst ⟫) → small m ≡ small n → m ≡ n small-inj m n e = ↪-inj {a = D .fst} {m = m} {n = n} ``` `small` の単射性は、インデックスの等しさを提示の中を通して辿ることで証明される。`small m ≡ small n` から、`(fib m) .snd` を逆向きにたどって `m` での提示された値を得、埋め込みの下での合同が等しさを運び、`(fib n) .snd` が `n` での提示された値に着く。三つのパスを正にこの方向でつなぐことで、二つの値の底の集合が等しくなる。続いて Extract の単射性が二つの入力の底の集合の等しさを与え、`↪-inj`、すなわち定義域の提示の埋め込みのインデックス上の単射性が `m ≡ n` を結論する。ここでは二つの異なる単射性の事実が働いており、一つはグラフについて、もう一つは標準的な埋め込みについてで、どちらも他方で代用できない。 ```agda (E.toFun-inj ij (at m) (at n) (sym ((fib m) .snd) ∙ cong ⟪ C .fst ⟫↪ e ∙ (fib n) .snd)) ```
## まとめ `injAt` は符号化グラフの単射性をモデル内部で表す。一価性と正確な定義域から `Extract.toFun` はグラフを `L` に値を取る関数として読み、独立な仮定 `ij` を加えて初めて `Extract.toFun-inj` が得られる。指定された値域条件の下で、`Small.small` はこの単射を定義域と値域の標準的な小さな要素型へ移す。切り詰めの段階では像のファイバーの一意性を、提示の段階では埋め込みのファイバーが命題であることを使う。