--- title: "符号化された単射の合成と包含" module: L.InjectionComposition lang: ja site: "Bedrock" description: "符号化された単射の合成と包含" stage: "順序数，単射，基数" reading_order: 91 canonical: https://bedrock.institute/ja/L.InjectionComposition.html html: L.InjectionComposition.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/InjectionComposition.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, V.Presentation, L.Constructible, L.Ordinal, L.Ordinal.SquareLaw, L.Recursion, L.Axioms.Full, L.Coding.Model, L.Coding.Injection, L.Cardinal, L.DefinableInjection] routes: [cardinal-tools] translations: [https://bedrock.institute/en/L.InjectionComposition.md, https://bedrock.institute/zh/L.InjectionComposition.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 : LEM (ℓ-suc ℓ)` を仮定する。この仮定は該当するレベルの各命題に判定を与え、以下の構成の明示的なパラメータとして保たれる。 ```agda module L.InjectionComposition {ℓ : 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; pr-inj ) open import V.Presentation {ℓ} using ( member; fiber; ↪-inj ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd ) open import L.Ordinal {ℓ} using ( ω-ord; #∈ω ) import L.Ordinal.SquareLaw {ℓ} lem as SQ open import L.Recursion {ℓ} lem using ( smallDom ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL ) open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-in; svAt-out; domAt; domAt-in; domAt-out; domAt-intro ) open import L.Coding.Model {ℓ} using ( appC; appC-adequate ) public open import L.Coding.Injection {ℓ} lem using ( injAt; injAt-out; injAt-in; module Small ) open import L.Cardinal {ℓ} lem using ( InjCode; InjL ) open import L.DefinableInjection {ℓ} lem using ( DefinableMap ) renaming ( module Inj to DefinableInj ) ``` 本章は、`L` の内部で符号化された単射の構成を二つ発展させ、一つの排除を証明する。第一に、二つの符号化された単射の合成である。ある中間の `y` が `(x, y)` を最初のグラフに、`(y, z)` を第二のグラフに持つとき、合成のグラフは `x` を `z` に関係付ける。第二に、集合の包含は、小さい方の集合上の恒等写像によって符号化される。そのグラフは、等号で定義される順序対の集合、すなわち `y = x` を満たす対 `(x, y)` の全体である。最後に、`ω` から有限順序数の平方への単射は存在しない。 ```agda open import Cubical.HITs.PropositionalTruncation using ( rec2 ) ``` グラフの性質と適用は、モデル言語の論理式によって表される。各変数の枠は要素の列に対して読まれ、充足が構造の意味論となる。二つの構造が現れる。周囲の階層が集合を供給し、構成可能構造がグラフの住み、読まれる台を供給する。 周囲の集合の順序対は、二つの成分が復元できる対の演算で符号化される。等しい符号は等しい成分をもつ。小さな集合には提示が伴い、階層へ埋め込まれた索引型によって、提示された要素についての事実が索引についての事実へ移る。構成可能性は、所属に沿って下方閉な述語である。構成可能な集合の要素は構成可能である。 四つの材料が本章を支える。序数 `ω` と、その要素がちょうど数項であるという事実。数項と有限集合の間の有限の対応辞と、その抽象的な追跡論法。小さな定義域の原理、すなわち構成可能集合の小さな族を一つの段階で抑えるもの。そして `L` 内部の分出であり、任意の複雑さの論理式に使えるので、以下のどの関係も共有の上界から刻み出される。 ```agda open SQ using ( module FiniteBase ) ``` `L` の内部では、言語の適用のアトムは定数のもとで読まれる。グラフに引数を適用したものは再び論理式であり、この読みは忠実である。単射の三つの論理条件は、これらのアトムのもとでそれぞれ導入と除去の形をもつ。符号化された単射は、定義域と終域の提示の間の本物の関数として読み戻すこともできる。 単射の符号とは、グラフに四条件のすべてを合わせたものである。すなわち、定義域の上で読まれる論理式としての一価性・定義域の全域性・単射性と、メタ言語で述べられる値域の条項である。内部単射の関係 `InjL` は、そのようなグラフと四条件が、単に、存在すると主張する。定義可能な単射の構成は、定義の論理式とともに与えられた写像をそのような符号へ変える。 内部の存在は命題的切り詰めによって主張される。主張は証人を選ばずに成り立ち、切り詰められた主張は命題へしか消去できない。空の型と自然数が、後の有限の議論を両側から抑える。 集合間のパスは提示型間の同値を与え、それに沿って関数と単射を移せる。単射性の証明では、`retEq e x` が往復のパス `invEq e (equivFun e x) ≡ x` を与え、復元した原像を元の入力と同一視できる。周囲の階層は、本章のすべての所属の主張が読まれる台である。 ```agda open import Cubical.Foundations.Equiv using ( retEq ) open import Cubical.Foundations.Univalence using ( pathToEquiv ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) ``` 階層は後続も極限も同じように構成する。後続の演算は集合に一つの要素を加え、無限集合 `ω` は数項、有限順序数ごとに一つを集める。 ```agda open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) module IS = InfinitySet {ℓ} open IS using ( sucV; #_; ω ) ``` 提示は索引型と階層への埋め込みを対にし、その繊維が要素と索引の間で事実を運ぶ。命題値の存在量化子が、合成が使う定義域の条件を述べる。 ```agda open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ ) ``` 構成可能な台は、本章のすべての集合の住む名前で開かれる。絶対性の展開からは二つの読みが来る。構成可能構造での充足、これを局所の使用のために改名したもの、そしてその持ち上げられた形、すなわちアトムを定数の列のもとで評価する形である。以下のグラフの適用はすべて、この持ち上げられた読みを通す。 ```agda open hPropView 𝒮ʟ using ( S ) module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL using () renaming ( _⊨ᵐ_ to _⊨_ ) ``` 有限の側は、数項の対応辞と抽象的な追跡を開く。どちらも、本章が具体化するだけの形で述べられている。 ```agda open FiniteBase using ( ω-mem→numeral; toFin; toFin-inj; fromFin; fromFin-inj ) open FiniteBase using ( module AbstractChase ) ``` ## 共通の構成可能な上界 分出で関係を刻むには、候補となる要素が一つの構成可能集合の中になければならない。共有の装置は任意の小さな添字族 `g : I → S` を受け取り、各 `g i` を含む構成可能集合を返す。後の `PairBound` で初めて、選んだ定義域と終域から生じる順序対に具体化する。
```agda module StageBound (I : Type ℓ) (g : I → S) where ```
```agda opaque bnd : S bnd = smallDom I g .fst ``` 読み手は上界の目的をそのまま述べる。族の各構成員は、周囲の要素として読めば上界に属する。後で `Relation` に入れられる各対は、この読み手を通して上界に入る。 ```agda below : (i : I) → ⟨ (g i) .fst ∈ bnd .fst ⟩ below = smallDom I g .snd ```
## 有限な終域の排除 後に使う有限の排除は次の形を取る。`ω` から有限順序数の平方への単射は存在しない。道は `ω` の内部の所属をほとんど避ける。使うのは、`ω` の各要素が単にある数項であること、各数項が有限集合を提示し対応辞が両方向で単射であること、そして抽象的な追跡である。各有限の提示から固定された型への単射と、その固定型からある有限の提示の平方への単射が与えられれば、大きい有限集合から小さい有限集合への単射が導かれる。 `ω` 自身についての事実であり、所属の述語が支える強さでのものである。`ω` の要素は、単に、ある数項であり、数項 `n` の後続は再び数項、したがって再び要素である。`γ` とその数項の同一視は後続に沿って輸送される。 ```agda ω-limit : (γ : V ℓ) → ⟨ γ ∈ ω ⟩ → ⟨ sucV γ ∈ ω ⟩ ω-limit γ γ∈ω = rec₁ ((sucV γ ∈ ω) .snd) go (ω-mem→numeral γ γ∈ω) where go : Σ[ n ∶ ℕ ] (γ ≡ # n) → ⟨ sucV γ ∈ ω ⟩ go (n , p) = subst (λ w → ⟨ sucV w ∈ ω ⟩) (sym p) (#∈ω (suc n)) ``` 数項は `ω` の提示へ埋め込まれる。道すじは直接である。数項 `m` の提示の索引は、その数項の要素を名指す。その数項は `ω` に属し、`ω` の推移性により、名指された要素も `ω` に属する。`ω` の提示のその要素での繊維を取れば、それを提示する `ω` の提示の索引が得られる。 ```agda numeral-into-ω : (m : ℕ) → ⟪ # m ⟫ → ⟪ ω ⟫ numeral-into-ω m i = fiber ω (ω-ord .fst (member (# m) i) (#∈ω m)) .fst ``` 埋め込みは単射である。同じ数項の二つの索引が `ω` の提示の中で等しい値をもつなら、二つの繊維の同一視が、像の等しさをその数項の内部の提示された要素の等しさへ変える。そして数項自身の提示は単射なので、二つの索引は一致する。 ```agda numeral-into-ω-inj : (m : ℕ) (i₁ i₂ : ⟪ # m ⟫) → numeral-into-ω m i₁ ≡ numeral-into-ω m i₂ → i₁ ≡ i₂ numeral-into-ω-inj m i₁ i₂ e = ↪-inj {a = # m} (sym (fiber ω (ω-ord .fst (member (# m) i₁) (#∈ω m)) .snd) ∙ cong (⟪ ω ⟫↪) e ``` `ω` の側で使われる単射の事実は、数項の提示の単射性だけである。 ```agda ∙ fiber ω (ω-ord .fst (member (# m) i₂) (#∈ω m)) .snd) ``` 追跡は、提示の索引型についてのメタ理論の主張であり、内部の単射の関係ではない。仮定は二つである。第一に、各数項 `n` について、提示の型 `⟪ # n ⟫` と有限集合 `Fin n` の間に両方向の単射があり、それぞれの向きがそれ自身として単射であること。第二に、すべての `⟪ # m ⟫` から固定された型 `⟪ ω ⟫` への単射があること。結論は、`⟪ ω ⟫` から `⟪ # n ⟫ × ⟪ # n ⟫` への単射は不可能だ、ということである。 ```agda no-inj-finite-ω : (n : ℕ) → (f : ⟪ ω ⟫ → ⟪ # n ⟫ × ⟪ # n ⟫) → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → ⊥₀ no-inj-finite-ω n f finj = ``` 抽象的な議論が消費するのは、対応辞と、固定型への単射の族である。その中心は鳩の巣の数え上げである。`Fin (suc (n · n))` から `Fin (n · n)` への単射は存在せず、追跡は仮定された単射をまさにその形へ帰着させる。 ```agda AbstractChase.NoInj.no-inj (λ n → ⟪ # n ⟫) toFin toFin-inj fromFin fromFin-inj (⟪ ω ⟫) ``` 本章が渡すべきは、数項の対応辞と `ω` の提示への埋め込みだけである。 ```agda (numeral-into-ω) (numeral-into-ω-inj) n f finj ``` この条項は排除を任意の有限順序数へ持ち上げる。しかも追跡の形のまま、提示の索引型の水準にとどまる。ここで固定された型は `⟪ ω ⟫`、有限の提示は诸 `⟪ # n ⟫` である。 ```agda finite-excl-ω : (β : V ℓ) → IsOrd β → ⟨ β ∈ ω ⟩ → (f : ⟪ ω ⟫ → ⟪ β ⟫ × ⟪ β ⟫) → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → ⊥₀ finite-excl-ω β oβ β∈ω f finj = rec₁ isProp⊥ go (ω-mem→numeral β β∈ω) ``` `β` を `ω` の順序数の要素とし、`ω` の提示から `β` の提示の平方への関数が単射だとする。主張は矛盾であり、 ```agda where ``` `β` の `ω` への所属は、`β` と同一視される数項を単に与える。したがって数項の場合を反証すれば十分で、切り詰めは空の型へ消去される。空の型は命題である。 ```agda go : Σ[ n ∶ ℕ ] (β ≡ # n) → ⊥₀ go (n , p) = no-inj-finite-ω n f' finj' where ``` この同一視は集合の間のパスであり、パスを平方すると二つの平方の提示の間の同値が得られる。仮定された関数はこの同値と合成され、その単射性は同値の単位則に沿って移る。輸送された関数が二つの入力を同一視するなら、元の関数も同一視する。 ```agda e : ⟪ β ⟫ × ⟪ β ⟫ ≃ ⟪ # n ⟫ × ⟪ # n ⟫ e = pathToEquiv (cong (λ w → ⟪ w ⟫ × ⟪ w ⟫) p) f' : ⟪ ω ⟫ → ⟪ # n ⟫ × ⟪ # n ⟫ f' x = equivFun e (f x) finj' : (x y : ⟪ ω ⟫) → f' x ≡ f' y → x ≡ y ``` こうして追跡は数項に適用され、その矛盾は述べた鳩の巣の形、すなわち `Fin (suc (n · n))` から `Fin (n · n)` への単射である。 ```agda finj' x y e' = finj x y (sym (retEq e (f x)) ∙ cong (invEq e) e' ∙ retEq e (f y)) ``` ## 有界な順序対グラフとしての関係 `L` の二つの集合の間の関係は、符号化された順序対の集合になる。上界はどの論理式が現れるより先に、対を数え上げる。索引型は、定義域からの提示の索引と終域からの索引の積である。
```agda module PairBound (D C : S) where ```
```agda Ix : Type ℓ Ix = ⟪ D .fst ⟫ × ⟪ C .fst ⟫ ``` 各提示の索引は台の要素として実現される。それは提示された集合であり、構成可能な集合 `D` または `C` の要素なので、所属に沿って構成可能性が降ろされる。 ```agda private toD : ⟪ D .fst ⟫ → S toD m = ⟪ D .fst ⟫↪ m , isL-trans {x = D .fst} {y = ⟪ D .fst ⟫↪ m} (member (D .fst) m) (D .snd) toC : ⟪ C .fst ⟫ → S ``` それぞれの側で、索引ごとに一つの L 要素である。 ```agda toC k = ⟪ C .fst ⟫↪ k , isL-trans {x = C .fst} {y = ⟪ C .fst ⟫↪ k} (member (C .fst) k) (C .snd) ``` この族は、索引の各対を、実現された二要素の符号化された順序対へ送る。共有の上界の装置がこの族に一度だけ施され、一つの構成可能集合が `D` と `C` から生じうるすべての符号化された対を含む。 ```agda pw : Ix → S pw (m , k) = prʟ (toD m) (toC k) module SB = StageBound Ix pw ``` 上界は装置から読み出され、以降は所属を通してのみ使われる。以下でその構成は必要とされない。 ```agda bnd : S bnd = SB.bnd ``` 読み手は上界を提示の外へ広げる。`D` の任意の要素 `x` と `C` の任意の要素 `z` は、索引で与えられなくても、その符号化された対が上界の中にある。以降のどの構成も、この形で上界に触れる。 ```agda below : (x z : S) → ⟨ x .fst ∈ D .fst ⟩ → ⟨ z .fst ∈ C .fst ⟩ → ⟨ pr (x .fst) (z .fst) ∈ bnd .fst ⟩ below x z mx mz = subst (λ w → ⟨ w ∈ bnd .fst ⟩) pa (SB.below i) where ``` `D` と `C` は提示されているので、二つの要素はそれぞれ繊維をもつ。提示された集合がその要素と同一視される索引である。二つの繊維は独立に取られる。 ```agda fD : Σ[ m ∶ ⟪ D .fst ⟫ ] (⟪ D .fst ⟫↪ m ≡ x .fst) fD = fiber (D .fst) mx fC : Σ[ k ∶ ⟪ C .fst ⟫ ] (⟪ C .fst ⟫↪ k ≡ z .fst) fC = fiber (C .fst) mz ``` 二つの索引は上界の族の一つの索引となり、その索引での族の値は提示された要素たちの符号化された対で、二つの繊維のパスに沿って `x` と `z` の符号化された対と等しくなる。その等しさに沿って所属を輸送すれば、読み手は完了する。 ```agda i : Ix i = fD .fst , fC .fst pa : (pw i) .fst ≡ pr (x .fst) (z .fst) pa = prʟ-fst (toD (fD .fst)) (toC (fC .fst)) ∙ cong₂ pr (fD .snd) (fC .snd) ```
上界から関係を刻むのに三つのデータが要る。三つの枠をもつ論理式と、対の上の述語 `P`、そして両方向の妥当性である。論理式の読みの順は値、添字、対である。環境 `y ∷ x ∷ e` のもとで、論理式は `P x y` として読まれる。
```agda module Relation (D C : S) (φ : Formula S 3) (P : S → S → hProp (ℓ-suc ℓ)) (read : (x y e : S) → ⟨ (y ∷ x ∷ e ∷ []) ⊨ φ ⟩ → ⟨ P x y ⟩) (fill : (x y e : S) → ⟨ P x y ⟩ → ⟨ (y ∷ x ∷ e ∷ []) ⊨ φ ⟩) where ```
刻むための論理式は、二つの枠を存在量化し、さらに与えられた論理式に加えて、第三の枠が最初の二つの順序対を符号化することを対象言語の中で主張する。共有の上界での分出をこの一枠の論理式に施すと、関係が `L` の要素として返る。 ```agda opaque fo : Formula S 1 fo = ∃̇ (∃̇ (prAtL (suc (suc zero)) (suc zero) zero ∧̇ φ)) rel : S rel = hasSeparationL (PairBound.bnd D C) fo .fst .fst ``` 逆の読みは、所属を一つの対についての切り詰められたデータへ変える。関係の要素 `e` は分出の仕様により刻むための論理式を満たす。二つの存在量化が解けて成分 `x` と `y` が現れ、`e` がその対を符号化することの証明が、妥当性によって符号化の演算自身の形に戻され、論理式の部分は `P x y` へ読み替えられる。 ```agda out : (e : S) → ⟨ e .fst ∈ rel .fst ⟩ → ∥ Σ[ x ∶ S ] Σ[ y ∶ S ] ((e .fst ≡ pr (x .fst) (y .fst)) × ⟨ P x y ⟩) ∥₁ out e h = rec₁ squash₁ (λ { (x , hx) → map₁ (λ { (y , q , hy) → x , y , subst ⟨_⟩ (prAtL-adequate (suc (suc zero)) (suc zero) zero (y ∷ x ∷ e ∷ [])) q ``` すべて切り詰められており、この関係が後に消費される形と一致する。 ```agda , read x y e hy }) hx }) (subst ⟨_⟩ (hasSeparationL (PairBound.bnd D C) fo .fst .snd e) h .snd) ``` 順方向は述語から所属を作る。 ```agda into : (x y : S) → ⟨ x .fst ∈ D .fst ⟩ → ⟨ y .fst ∈ C .fst ⟩ → ⟨ P x y ⟩ → ⟨ pr (x .fst) (y .fst) ∈ rel .fst ⟩ into x y mx my h = subst (λ w → ⟨ w ∈ rel .fst ⟩) (prʟ-fst x y) (subst ⟨_⟩ (sym (hasSeparationL (PairBound.bnd D C) fo .fst .snd (prʟ x y))) ( subst (λ w → ⟨ w ∈ (PairBound.bnd D C) .fst ⟩) (sym (prʟ-fst x y)) ``` `x` と `y` の符号化された対は、上界の読み手によって共有の上界に入る。論理式の符号化の条項は符号化の演算の計算で成り立ち、与えられた論理式は妥当性で成り立つ。分出が所属を証明し、符号化の定義的な等しさに沿って輸送される。 ```agda (PairBound.below D C x y mx my) , ∣ x , ∣ y , subst ⟨_⟩ (sym (prAtL-adequate (suc (suc zero)) (suc zero) zero (y ∷ x ∷ prʟ x y ∷ []))) (prʟ-fst x y) , fill x y (prʟ x y) h ∣₁ ∣₁ )) ``` `x` と `y` の本来の符号化された対に対しては、逆の読みは切り詰めのない結論へ鋭くなる。 ```agda pair-out : (x y : S) → ⟨ pr (x .fst) (y .fst) ∈ rel .fst ⟩ → ⟨ P x y ⟩ pair-out x y h = rec₁ ((P x y) .snd) (λ { (x' , y' , q , h') → subst2 (λ a b → ⟨ P a b ⟩) (Σ≡Prop (λ v → (isL v) .snd) (sym (pr-inj (sym (prʟ-fst x y) ∙ q) .fst))) ``` その証人は `e` をある `x'` と `y'` の符号化された対として提示する。符号化の単射性により、`x'` の底の要素は `x` のそれと、`y'` の底の要素は `y` のそれと同一視される。さらに構成可能性は命題なので、これらの底の等しさは台の要素の等しさへ持ち上がる。述語は、ちょうど `P x y` の場所へ輸送される。 ```agda (Σ≡Prop (λ v → (isL v) .snd) (sym (pr-inj (sym (prʟ-fst x y) ∙ q) .snd))) h' }) (out (prʟ x y) (subst (λ w → ⟨ w ∈ rel .fst ⟩) (sym (prʟ-fst x y)) h)) ```
## 符号化された単射の合成 最初の終域が第二の定義域であるとき、二つの符号化された単射は合成できる。合成物もまたグラフであり、その検証は置換をやり直さない。二つの入力グラフはすでに集合として存在し、合成物は共有の上界の中で分出された一つの関係である。モジュールは二つのグラフと、それぞれ三つの読みの条件を受け取る。
```agda module Comp (D E C F H : S) (svF : ⟨ (F ∷ D ∷ []) ⊨ svAt zero ⟩) (dmF : ⟨ (F ∷ D ∷ []) ⊨ domAt zero (suc zero) ⟩) (ijF : ⟨ (F ∷ D ∷ []) ⊨ injAt zero ⟩) (ranF : (x y : S) → ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩ → ⟨ y .fst ∈ E .fst ⟩) (svH : ⟨ (H ∷ E ∷ []) ⊨ svAt zero ⟩) (dmH : ⟨ (H ∷ E ∷ []) ⊨ domAt zero (suc zero) ⟩) (ijH : ⟨ (H ∷ E ∷ []) ⊨ injAt zero ⟩) (ranH : (y z : S) → ⟨ pr (y .fst) (z .fst) ∈ H .fst ⟩ → ⟨ z .fst ∈ C .fst ⟩) where ```
三つの読みの条件に加えて、各グラフは値域の条項をモジュールの独立な仮定として運ぶ。最初のグラフの各符号化された対の値は中間の集合にあり、第二のグラフの各対の値は最終の終域にある。 この二つの条項は、論理式としてではなくメタ言語で述べられる。 「符号と定義域」の各対は、三つの論理条件が要求する二枠の環境にすぎない。枠 0 にグラフ、枠 1 に定義域である。環境はグラフごとに一つである。 ```agda private γF : Vec S 2 γF = F ∷ D ∷ [] γH : Vec S 2 γH = H ∷ E ∷ [] ``` 結びの関係は次を言う。対象言語が中間の `y` で、`(x, y)` が最初のグラフに、`(y, z)` が第二のグラフにあるものを生み出せるなら、`x` と `z` は関係する。その切り詰めは存在量化子の意味論から受け継がれる。量化子は命題値であり、論理式の充足が運ぶ証人は、量化子に組み込まれた切り詰めの分だけである。 ```agda private Chain : S → S → Type (ℓ-suc ℓ) Chain x z = ∥ Σ[ y ∶ S ] (⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩ × ⟨ pr (y .fst) (z .fst) ∈ H .fst ⟩) ∥₁ ``` 刻むための論理式には、中間の値の上の一つの存在量化だけがある。その内側で二つの適用のアトムが連言される。最初のグラフは、値の枠に中間値、添字の枠に `x` を置いて読まれ、第二のグラフは、値の枠に `z`、添字の枠に中間値を置いて読まれる。これが `(x, y) ∈ F` と `(y, z) ∈ H` の対象言語としての形である。 ```agda opaque body : Formula S 3 body = ∃̇ (appC F (suc (suc zero)) zero ∧̇ appC H zero (suc zero)) ``` 適用アトムの妥当性が、各連言を本来の所属へ運ぶ。第一は `(x, y)` における最初のグラフへの所属へ、第二は `(y, z)` における第二のグラフへの所属へ。残るのは、切り詰められた形の結びの証人である。 ```agda read : (x z p : S) → ⟨ (z ∷ x ∷ p ∷ []) ⊨ body ⟩ → Chain x z read x z p = map₁ (λ { (y , hf , hh) → y , subst ⟨_⟩ (appC-adequate F (suc (suc zero)) zero (y ∷ z ∷ x ∷ p ∷ [])) hf , subst ⟨_⟩ (appC-adequate H zero (suc zero) (y ∷ z ∷ x ∷ p ∷ [])) hh }) ``` 逆方向は、結びの証人を同じ妥当性を逆にたどって対象言語へ戻す。二つの向きは、論理式と結びの関係が互いを表現することを言う。 ```agda fill : (x z p : S) → Chain x z → ⟨ (z ∷ x ∷ p ∷ []) ⊨ body ⟩ fill x z p = map₁ (λ { (y , hf , hh) → y , subst ⟨_⟩ (sym (appC-adequate F (suc (suc zero)) zero (y ∷ z ∷ x ∷ p ∷ []))) hf , subst ⟨_⟩ (sym (appC-adequate H zero (suc zero) (y ∷ z ∷ x ∷ p ∷ []))) hh }) ``` 有界関係の装置は一度だけ具体化され、その述語として結びの関係が与えられる。以下のすべてはこの一つの実例から読み出される。 ```agda module Composite = Relation D C body (λ x z → Chain x z , squash₁) read fill ``` 合成のグラフは、分出された関係そのものである。 ```agda K : S K = Composite.rel K-out : (x z : S) → ⟨ pr (x .fst) (z .fst) ∈ K .fst ⟩ → ∥ Σ[ y ∶ S ] (⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩ × ⟨ pr (y .fst) (z .fst) ∈ H .fst ⟩) ∥₁ ``` 逆の読みはそのまま引き継がれる。合成の中の符号化された対は、単に、`(x, y)` が最初のグラフに、`(y, z)` が第二のグラフにあるような中間の `y` を与える。以下の四つの検証はすべて、この一つの読み手が駆動する。 ```agda K-out = Composite.pair-out ``` 順方向の読みは合成の法則である。二つの対がそれぞれ二つのグラフにある中間の `y` が与えられれば、切り詰められた証人が装置に渡され、装置は `x` と `z` の符号化された対を合成の中に置く。 ```agda K-in : (x y z : S) → ⟨ x .fst ∈ D .fst ⟩ → ⟨ z .fst ∈ C .fst ⟩ → ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩ → ⟨ pr (y .fst) (z .fst) ∈ H .fst ⟩ → ⟨ pr (x .fst) (z .fst) ∈ K .fst ⟩ K-in x y z mx mz hf hh = Composite.into x z mx mz ∣ y , hf , hh ∣₁ ``` 合成は次に、四条件を自分の力で満たさねばならない。環境は合成のグラフと最初の定義域を対にする。まず一価性である。 ```agda γK : Vec S 2 γK = K ∷ D ∷ [] svK : ⟨ γK ⊨ svAt zero ⟩ ``` 合成が `x` を二つの値 `y` と `y'` に対にするとする。切り詰められた二つの結びを解くと中間の `w` と `w'` が現れ、`(x, w)` と `(x, w')` が最初のグラフにある。 ```agda svK = svAt-in zero γK (λ x y y' p q → rec₁ (setIsSet (y .fst) (y' .fst)) (λ { (w , (hf , hh)) → rec₁ (setIsSet (y .fst) (y' .fst)) (λ { (w' , (hf' , hh')) → svAt-out zero γH svH w y y' hh ``` 最初のグラフの一価性が `w` と `w'` を同一視し、その同一視は第二のグラフの対へ輸送され、第二の一価性が `y` と `y'` を同一視する。目標は h-集合の中のパス、すなわち命題なので、二度の切り詰めの消去は正当である。 ```agda (subst (λ t → ⟨ pr t (y' .fst) ∈ H .fst ⟩) (sym (svAt-out zero γF svF x w w' hf hf')) hh') }) (K-out x y' q) }) (K-out x y p)) ``` 次に単射性を検証する。ここで二つのグラフの使う順序が重要である。第二のグラフの単射性を先に使い、最初のグラフの単射性を後に使う。 ```agda ijK : ⟨ γK ⊨ injAt zero ⟩ ``` 合成が `y` に `x` と `x'` の両方を送るとする。切り詰められた二つの結びが中間の `w` と `w'` を与える。`(x, w)` と `(x', w')` は最初のグラフにあり、`(w, y)` と `(w', y)` は第二のグラフにある。 ```agda ijK = injAt-in zero γK (λ y x x' p q → rec₁ (setIsSet (x .fst) (x' .fst)) (λ { (w , (hf , hh)) → rec₁ (setIsSet (x .fst) (x' .fst)) (λ { (w' , (hf' , hh')) → injAt-out zero γF ijF w x x' hf ``` 共通の値 `y` における第二のグラフの単射性が `w` と `w'` を同一視し、今や共通の中間における最初のグラフの単射性が `x` と `x'` を同一視する。 ```agda (subst (λ t → ⟨ pr (x' .fst) t ∈ F .fst ⟩) (sym (injAt-out zero γH ijH y w w' hh hh')) hf') }) (K-out x' y q) }) (K-out x y p)) ``` 合成の定義域における全域性は同値である。`x` が最初の定義域に属するのは、合成の値をもつとき、そのときに限る。二つの向きが導入の形に渡される。 ```agda dmK : ⟨ γK ⊨ domAt zero (suc zero) ⟩ dmK = domAt-intro zero (suc zero) γK (λ x → fwd x , bwd x) ``` 一つの向きは、最初のグラフの定義域の条件をそのまま消去する。 ```agda where fwd : (x : S) → ⟨ ∃[ y ∶ S ] (pr (x .fst) (y .fst) ∈ K .fst) ⟩ → ⟨ x .fst ∈ D .fst ⟩ fwd x = rec₁ ((x .fst ∈ D .fst) .snd) (λ { (y , p) → rec₁ ((x .fst ∈ D .fst) .snd) ``` `x` が合成の値をもつなら、結びの証人が中間の `w` を示し、`(x, w)` が最初のグラフにある。定義域のアトム自身の消去をその対に施せば、`x` が `D` の中に置かれる。この向きで第二のグラフは役に立たない。 ```agda (λ { (w , (hf , _)) → domAt-out zero (suc zero) γF dmF x w hf }) (K-out x y p) }) ``` もう一つの向きは、二つの導入をつなぐ。`D` の `x` が与えられると、最初のグラフの定義域の導入が中間の `w` を与え、`(x, w)` が最初のグラフにあり、その値域の条項が `w` を中間の集合に置く。 ```agda bwd : (x : S) → ⟨ x .fst ∈ D .fst ⟩ → ⟨ ∃[ y ∶ S ] (pr (x .fst) (y .fst) ∈ K .fst) ⟩ bwd x mx = rec₁ squash₁ (λ { (w , hf) → rec₁ squash₁ (λ { (z , hh) → ∣ z , K-in x w z mx (ranH w z hh) hf hh ∣₁ }) ``` 第二のグラフの定義域の導入は `w` で `(w, z)` をもつ `z` を産み、第二のグラフの値域の条項が `z` を `C` に置く。そして合成の法則が `x` と `z` の対を合成の中に置く。どちらの段階も切り詰められ、結論もそうである。 ```agda (domAt-in zero (suc zero) γH dmH w (ranF x w hf)) }) (domAt-in zero (suc zero) γF dmF x mx) ``` 値域の条件は、第二のグラフの値域の条項を中間の値に適用したものである。合成の対を解けば結びの証人が現れ、その第二成分が第二のグラフの中で中間と `z` を対にするので、条項が `z` を `C` の中に置く。 ```agda ranK : (x z : S) → ⟨ pr (x .fst) (z .fst) ∈ K .fst ⟩ → ⟨ z .fst ∈ C .fst ⟩ ranK x z h = rec₁ ((z .fst ∈ C .fst) .snd) (λ { (w , (_ , hh)) → ranH w z hh }) (K-out x z h) ``` 三つの読みの条件と値域の条項が揃うのは、符号化された単射を提示の間の関数として読み戻すための条件にちょうど合う。したがって合成もこの読みを認める。このモジュールがそれを非公開で担う。公開されて渡るのはグラフと四条件だけなので、この読みにそれ以外は要らない。 ```agda private module Sm = Small K D C svK dmK ijK ranK ```
## 包含の符号化 包含には新しい構成は要らない。`D` が `C` に含まれるなら、`D` 上の恒等写像はもともと `C` への写像である。符号化されるのはその写像のグラフであり、対象言語では値の枠と添字の枠の間の等号として書かれる。モジュールは二つの集合と点ごとの包含を受け取る。
```agda module InclGraph (D C : S) (sub : (z : V ℓ) → ⟨ z ∈ D .fst ⟩ → ⟨ z ∈ C .fst ⟩) where ```
定義可能な写像のレコードは、定義域上の恒等で満たされる。 ```agda private M : DefinableMap M = record { dom = D ; cod = C ; fn = λ x _ → x ``` 関数は各要素を自分自身へ送り、点ごとの包含がすべての値が `C` に着地することを証明する。 ```agda ; into = λ x mx → sub (x .fst) mx ``` グラフの論理式は二つの枠の間の等号であり、それが関数自身の値について成り立つことは定義的である。解の一意性には、等号の底の等しさを使う。どんな解も等式を満たすが、それは底の要素の間の等しさであり、構成可能性が命題なので、この底の等しさは台の要素の等しさへ持ち上がる。関数の値と無関係な解が除かれるのは、このためである。 ```agda ; graph = var zero ≐ var (suc zero) ; defines = λ _ _ → refl ; only = λ _ _ _ h → Σ≡Prop (λ w → (isL w) .snd) h } ``` 共有の構成はこの写像を三つの読みの条件をもつグラフへ変えるが、底の関数が単射であることの証明を外部から要求する。恒等写像の場合これは直接である。仮定は二つの入力の像を等しくするが、恒等写像のもとで像の等しさは入力の等しさである。したがって、等式をそのまま返す渡された継続が、求める証明にちょうどなる。 ```agda module I = DefinableInj M (λ _ _ _ _ e → e) using ( F; code ) opaque G : S G = I.F ``` グラフと四条件のすべてが、`D` から `C` への単射の符号として一緒に渡される。利用者は包みを一つの単位として受け取り、開く必要はない。 ```agda opaque unfolding G code : InjCode G D C code = I.code ``` 同じグラフが、共有の読みを通して、`D` と `C` の提示の間の関数として読み戻される。この読みは非公開のモジュールが担う。公開されて渡る結果はグラフとその四条件であり、この読みに必要なのはそれだけである。 ```agda private module Sm = Small G D C (code .fst) (code .snd .fst) (code .snd .snd .fst) (code .snd .snd .snd) ``` 導かれた関数は `incl` と名付けられ、その道すじが重要である。`D` の提示の索引は底の要素を名指し、その要素は `D` に属し、したがって包含によって `C` に属する。関数は次に、`C` 自身の提示のその要素での繊維を取る。すなわち、その要素を提示する `C` の索引である。索引を直接輸送するのではなく、要素と繊維を通して取り戻す。 ```agda opaque incl : ⟪ D .fst ⟫ → ⟪ C .fst ⟫ incl = Sm.small ```
## 内部存在の水準における包含と合成 これまでの構成はグラフを産む。内部の単射関係が要求するのは、グラフが存在することだけである。持ち上げは直接である。包含は恒等グラフを証人として与え、主張はその周りで切り詰められる。基数の議論が包含を受け取るのは、この形である。 ```agda inclusion-coded : (a b : S) → ((z : V ℓ) → ⟨ z ∈ a .fst ⟩ → ⟨ z ∈ b .fst ⟩) → InjL a b inclusion-coded a b sub = ∣ I.G , I.code ∣₁ where module I = InclGraph a b sub ``` 合成も同様に持ち上がる。`rec2` は二つの証人を局所的に取り出して合成を作り、結果を再び切り詰めるので、代表を大域的に選ぶ必要はない。 ```agda injl-trans : (a b c : S) → InjL a b → InjL b c → InjL a c injl-trans a b c = rec2 squash₁ step where ``` 二重の消去は、二つの証人を局所的に解きほぐし、検証済みの構成で合成を組み立て、結果を改めて切り詰める。代表の大域的な選択は行わない。二つの証人は、構成の仮定として存在するだけで、保持されることはない。 ```agda step : Σ[ F ∶ S ] InjCode F a b → Σ[ H ∶ S ] InjCode H b c → InjL a c step (F , svF , dmF , ijF , ranF) (H , svH , dmH , ijH , ranH) = ∣ K.K , (K.svK , K.dmK , K.ijK , K.ranK) ∣₁ ``` 合成のモジュールが検証のすべてを担うので、この水準では合成の法則は一行である。 ```agda where module K = Comp a b c F H svF dmF ijF ranF svH dmH ijH ranH ``` 主要な実例は、順序数 `C` の要素 `D` から始まる。仮定は `D` が順序数 `C` に属することだけである。`C` の推移性により、`D` の各要素が `C` の要素であることが従い、これが符号化の必要とする点ごとの包含にほかならない。モジュールはこの対に対して包含の構成を開くので、そのグラフ・符号・導かれた写像が一つの名のもとで使える。
```agda module OrdIncl (C : S) (oC : IsOrd (C .fst)) (D : S) (D∈C : ⟨ D .fst ∈ C .fst ⟩) where ```
```agda open InclGraph D C (λ _ z∈D → oC .fst z∈D D∈C) public ```
## まとめ 三つの結果が内部の基数の議論に仕える。有限の排除は、`ω` から任意の有限順序数の平方への単射が存在しないことを示す。`ω` の要素は単に数項であり、提示の型 `⟪ # n ⟫` と有限集合 `Fin n` の間には両方向それぞれに単射があり、抽象的な追跡は、有限の平方への単射の存在を仮定すると、大きい有限集合から小さい有限集合への単射を導く。合成は二つの符号化された単射を一つにし、結びの関係を通して一価性・定義域における全域性・単射性・値域の条項を検証する。包含は恒等グラフによって点ごとの包含を符号化された単射へ変える。存在の水準では、どちらの操作も切り詰められた内部の関係へ持ち上がるので、基数の上界の構成と比較を、`L` の中に住むグラフだけを通して行える。