--- title: "L の内部にある極限段階の順序" module: L.Choice.LimitStageOrder lang: ja site: "Bedrock" description: "L の内部にある極限段階の順序" stage: "正準整列順序と選択公理" reading_order: 81 canonical: https://bedrock.institute/ja/L.Choice.LimitStageOrder.html html: L.Choice.LimitStageOrder.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/LimitStageOrder.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Infinity, L.Axioms.Full, L.Recursion, L.Coding.Model, L.Coding.Expressions, L.Coding.HierarchySequence, L.Hierarchy, L.Choice.FiniteStageOrders, L.Choice.NameComparison, L.WellOrder.Base, FOL.Absoluteness] routes: [choice-completion] translations: [https://bedrock.institute/en/L.Choice.LimitStageOrder.md, https://bedrock.institute/zh/L.Choice.LimitStageOrder.md] agent_guide: https://bedrock.institute/llms.txt license: "CC-BY-NC-SA-4.0" --- ```agda {-# OPTIONS --cubical --safe --guardedness #-} ``` # L の内部にある極限段階の順序 ```agda open import Base.Prelude open import Base.Classical using ( LEM ) ``` 宇宙レベル `ℓ` と、いま説明した排中律の実例を固定する。この時点では、後で作る内部関係はまだ条件つきである。有限段階の順序を表す論理式と、その意味論の二方向を与えた後に、モジュール `Described` の内部で定義される。次章がその実例を与え、後続の構成が使えるように `codeOrder` を公開する。 ```agda module L.Choice.LimitStageOrder {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where ``` ```agda open import FOL.ZFStructure using ( module hPropView ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_; _∨̇_; ¬̇_; _⇒̇_; ∃̇_; ∀̇_; ∀̇∈ ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′ ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd ) open import L.Ordinal {ℓ} using ( numeral-ord; #∈ω; ∈#-elim; #∈#-elim; ω-ord ) open import L.Axioms.Basic {ℓ} using ( LsetS ) open import L.Axioms.Infinity {ℓ} lem using ( ωʟ ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL ) open import L.Recursion {ℓ} lem using ( smallDom ) open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; prAtL; prAtL-adequate; prʟ; prʟ-fst ) open import L.Coding.Expressions {ℓ} using ( numL ) open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt ) open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines ) open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; level; level-in; levelData; limitOrder ; before; precedes; Agrees; Witness; finiteStage ) open import L.Choice.NameComparison {ℓ} lem using ( module Adequacy ) open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; Tri; lt; eq; gt ) import FOL.Absoluteness ``` `Lset ω` の要素には、外側ですでに狭義整列順序が与えられている。ここでの問いは、その比較を `L` の内部の論理式からどのように使えるようにするかである。答えは三つの異なる形を順に通る。メタ水準の比較、その比較の対象言語による記述、そして有限段階の記述が与えられた後に、その関係を実現する構成可能集合である。 この章のすべての構成は、レベル `ℓ-suc ℓ` における一つの明示的な排中律の実例に相対している。先の章では、この仮定から極限段階の要素が最初に現れる有限段階を得た。この章では、用いる分出と上界の結果にも同じ実例を渡す。この仮定は必要な箇所で命題を判定するが、任意の族に対する選択関数を与えない。 対象言語は、構文と階層における意味を混同せずに比較を記述しなければならない。論理式は変数、定数、所属、結合子、量化子を使う。定数領域は構成可能な台なので、定数はすでに特定の構成可能集合を指す。後で必要となる二つの基本的な判定は、符号化の補題から得られる。順序対の等式は二つの成分を決定し、数項の符号化も単射である。さらに `#mono` は `k < m` を、`# k` が `# m` に属するという事実へ移す。したがって集合論的所属は、有限添字の狭義比較を忠実に表せる。 ここで用いる構造は構成可能宇宙である。その台の要素は、集合と構成可能性の証拠をひとまとめにする。推移性により、その集合の各要素にも同じ種類の証拠が得られる。このため、通常の階層における所属の証人を対象言語の環境へ移せる。とくに、`finiteStage n` は `Lset (# n)` という段階であり、極限段階は `Lset ω` である。数項と順序数に関する事実により、添字と、それが名指す段階を区別できる。包装された段階と定数 `ωʟ` によって、論理式は構造の内部からこの階層について語れる。 三つの橋によって、意味論上の比較を `L` の集合へ変える。まず `smallDom` は、小さな族を一つの共通な構成可能集合に入れるが、その上界が族の像と一致するとは主張しない。次に分出は、その上界から一変数の論理式を満たす要素だけを正確に取り出す。最後に、順序対、関係への所属、階層列を記述する符号化論理式には、充足を対応する集合の事実へ移す妥当性の法則がある。これらにより、共通の領域を見つける問題と、その領域上で正確な関係を述べる問題を分けて扱える。 表現すべき比較は、外側ですでに定義されている。後続段階では、`before (suc n)` が `before n` によってより前の点を並べ、`finiteStage n` の二つの部分集合を最初の相違で比較する。`precedes R A x y` の証人は `A` に属し、`y` に属して `x` には属さず、より前のすべての点で `x` と `y` が一致することを記録する。その存在は命題的に切り詰められている。型 `Limit` は `Lset ω` の要素を包装し、その最小出現段階が `limitOrder` の第一の鍵になる。対応する `before` の比較を使うのは、段階が等しい場合だけである。得られる関係集合の二つの表現方向は、`Adequacy.Keys` が要求する形に正確に一致する。 `limitOrder` は `SWO` の構造として与えられている。比較そのものに加え、三分性、非反射性、推移性、整礎性を備える。内部化の議論はこれらの法則を証明し直さない。後では、最初の三つを一つの目的に使う。対象言語の選言から読み戻せるのが命題的に切り詰められた狭義比較だけであるとき、三分性が候補となる枝を示し、非反射性と推移性が両立しない枝を退ける。 極限の比較は、後で必要となる辞書式の形をしている。第一の選択肢は、最初の要素のレベルが小さいことを述べる。第二の選択肢は、二つのレベルが一致し、その共通レベルの `before` によって基礎集合を比較する。自然数の三分性が第一の鍵を分析し、`subst2` は等式が符号化されたレベルや端点を同定するとき、二項関係を運ぶ。付随する `Lift` と `lower` は宇宙レベルをそろえるだけであり、命題的な切り詰めを取り除く操作ではない。 ```agda open import Cubical.Data.Nat.Order using ( _<_; _≟_ ) import Cubical.Data.Nat.Order as NatOrder ``` 対象言語の存在量化と選言は、それぞれ命題的に切り詰められた存在と枝の選択として解釈される。したがって、その証人を使えるのは、不可能性、階層の集合の等式、別の切り詰めなど、目標が命題である場合だけである。ただし、この章に現れるすべての存在型が切り詰められているわけではない。型が明示的なデータを要求する場合、包装された台の要素や共通上界はそのまま見える。また、命題的切り詰めから狭義比較を復元する議論は一般的な除去原理ではなく、`limitOrder` の三分性と順序法則に特有のものである。 ```agda open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Properties ``` 上界の補題を使うには、`Lset ω` の要素に小さな添字型が必要である。ファイバー `⟪ Lset ω ⟫` がその添字を与え、`∈-asFiber` は与えられた所属証明を、像が元の要素になる添字へ変える。したがって二つのファイバーの積は、極限段階の要素からなるすべての順序対を添字づける。後で作る `pairsBound` はこれらの対をすべて含むが、正確な関係が得られるのは分出の後である。 ```agda using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈∈ₛ; ∈ₛ⟪_⟫↪_ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_; ω ) ``` ここでは三つの所属記号が別々の役割をもつ。台の要素に対する `x ∈ˢ y` は、構成可能構造の命題値の所属である。基礎となる階層の集合どうしでは、`x .fst ∈ y .fst` が周囲の所属を表す。論理式の内部では `_∈̇_` は所属を表す構文上の原子にすぎない。次に導入する充足判定が、第三の形に最初の二つの意味を与える。この層の区別により、順序を記述する論理式を、その実現集合が内部で整列順序をなすという証明と取り違えずに済む。 ```agda open hPropView 𝒮ʟ ``` 判定 `_⊨_` は、周囲の階層構造を構成可能クラスに制限して得られる内側の充足関係である。その台は集合と構成可能性の証拠からなるので、定数も量化される値も構成可能な対象を範囲とする。原子的所属は第一射影を通して解釈され、推移性により、構成可能な限界の要素を再び台の要素として包装できる。したがって充足は、対象言語の論理式から、その基礎集合についての通常の所属事実へ至る正確な橋になる。 ```agda module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ) ``` `limitOrder` がもつ比較を `_≺ˡ_` と書く。二つの極限段階の要素を、まず最小出現レベルで比較し、それが一致するときは共通の有限段階における最初の相違で比較する。残る目標は条件つきである。各有限段階の `before` 関係を所定の領域で表現する対象言語の論理式が与えられたと仮定し、`Described` の内部で集合 `codeOrder` を作る。そして `u` と `v` の順序対がこの集合に属することと`u ≺ˡ v` が成り立つことを同値にする。次章が必要な有限段階の論理式を与え、実際に使える実例を得る。 ```agda open SWO limitOrder using () renaming ( _<∙_ to _≺ˡ_ ) ``` 束縛変数は de Bruijn 位置で表される。二つの入れ子になった束縛を開くと、外側の環境にある各位置は二つの新しい項目を越える必要があり、`sh2` がその移動を正確に記録する。最初の相違を表す論理式が候補となる相違点と、その下にある点を順に束縛するとき、また異なるレベルの枝が二つのレベル数項を束縛するときに使う。この移動は既存の自由変数の参照位置だけを変え、その変数が指す集合や関係を変えない。 ```agda private sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i) ``` 環境が含むのは、裸の階層集合ではなく構成可能な台の要素である。そこで自然数 `k` に対し、`towerS k` は段階 `Lset (# k)` とその構成可能性の証拠を包装する。定義は不透明なので、後の証明は階層の構成を展開せず、公開された射影等式を通して使う。この不透明性は簡約を制御するだけであり、数学的な仮定を加えない。 ```agda opaque towerS : ℕ → S towerS k = LsetS (# k) (numeral-ord k) ``` 等式 `towerS-fst k` は、この台の要素の基礎集合を `Lset (# k)` と同一視する。同じ段階に対する二つの見方を結ぶ点である。論理式は包装された要素 `towerS k` を受け取り、外側の階層の補題は基礎となる階層集合への所属を述べる。後の証明は、二つの見方の間で所属事実を運ぶたびにこの等式を通る。 ```agda towerS-fst : (k : ℕ) → (towerS k) .fst ≡ Lset (# k) towerS-fst k = refl ``` 添字そのものにも別の台の要素が必要である。`numS k` は数項 `# k` と、それが構成可能であることの証拠を包装する。`numS k` と `towerS k` を区別することで、前者が順序数添字を指し、後者がその添字で指定される構成可能段階を指すという違いが明確になる。`LevelAt` は階層列の記述を通して、この二つの対象を結ぶ。 ```agda numS : ℕ → S numS k = # k , numL k ``` 射影等式 `numS-fst k` は、包装された数項から `# k` を取り出す。`towerS-fst k` と合わせることで、同じ自然数を二つの役割で整合的に使える。一方では環境におけるレベルの値であり、他方では証人が示す段階の添字である。これらの等式が、対象言語の値と、数項や段階についての外側の事実との間の輸送を正当化する。 ```agda numS-fst : (k : ℕ) → (numS k) .fst ≡ # k numS-fst k = refl ``` 環境の位置 `i` の基礎集合が `# j` であるとする。補題 `towerGraph` は、新しい位置に `towerS j` を置き、`LsetGraphAt` が二つの位置を関係づけることを証明する。その内容は階層列の仕様そのものである。数項 `# j` に対応する値は段階 `Lset (# j)` である。したがって同じ補題が、真のレベルにおける存在と、そのレベルを用いた最小性の検証の双方に、実際の塔の証人を与える。 ```agda towerGraph : ∀ {n} (j : ℕ) (δ : Vec S n) (i : Fin n) → (lookup i δ) .fst ≡ # j → ⟨ (towerS j ∷ δ) ⊨ LsetGraphAt zero (suc i) ⟩ towerGraph j δ i q = Lset-defines zero (suc i) (towerS j ∷ δ) (subst IsOrd (sym q) (numeral-ord j)) (towerS-fst j ∙ cong Lset (sym q)) ``` ## レベルを内部で述べる 論理式 `LevelAt b x` が第一の鍵の記述を始める。まず位置 `b` の値が `ω` に属することを要求するので、その値は数項として復号できる。次に、その数項において `LsetGraphAt` が記述する値の存在を求め、位置 `x` の値が得られた段階に属することを要求する。これらの節により `b` は `x` の出現段階となり、残る節がそれを最小にする。 ```agda LevelAt : ∀ {n} → Fin n → Fin n → Formula S n LevelAt b x = (var b ∈̇ con ωʟ) ∧̇ ( ∃̇ ( LsetGraphAt zero (suc b) ∧̇ (var (suc x) ∈̇ var zero) ) ∧̇ ∀̇∈ (var b) (∀̇ ( LsetGraphAt zero (suc zero) ``` 最小性は、候補となる数項 `b` の直前の要素だけでなく、すべての要素 `u` にわたって表される。そのような `u` で記述される各段階に、位置 `x` の値は属してはならない。`# k` の要素はちょうど小さい数項なので、候補 `b = # k` は `0` から`k-1` までのすべての段階を排除する。二つの入れ子の束縛が `x` の位置の移動を説明する。意味論上、これらの全称節は関数型である。近くにある数項所属の命題的に切り詰められた復号は、命題を目標とするときだけ使われ、小さい添字を一つ選び出すことはない。 ```agda ⇒̇ ¬̇ (var (sh2 x) ∈̇ var zero) )) ) ``` `LevelAt` の二つの読みを証明するため、実際の極限段階の要素 `a`、自然数 `k`、そして `k` をその最小出現レベルと同定する等式 `qk : level a ≡ k` を固定する。`levelData a` の正の成分を `qk` に沿って運ぶと `aIn` が得られる。これは `a` の基礎集合が `Lset (# k)` に属するという事実である。負の成分は、`m < k` である任意の `m` に対し、`Lset (# m)` への所属が不可能であることを述べる。これらは、論理式が真のレベルを認識するために必要な存在と最小性の事実であり、さらに論理式が認識したどのレベルも `# k` に等しいことを示すために使われる。
```agda module Level (a : Limit) (k : ℕ) (qk : level a ≡ k) where ```
```agda private aIn : ⟨ a .fst ∈ Lset (# k) ⟩ aIn = subst (λ j → ⟨ a .fst ∈ Lset (# j) ⟩) qk (level-in a) ``` `levelData a` の第二射影は、以下の議論で必要となる最小性を与える。`a` の基礎集合がすでに `Lset (# m)` に属し、しかも`m < k` なら、等式 `qk` によって後者は `m < level a` に移され、この最小性に反する。`levelData` が要求する比較は一つ上の宇宙にあるので、ここでは `lift` で包む。これは宇宙水準の調整にすぎず、命題的切り詰めとは関係ない。 ```agda aMin : (m : ℕ) → ⟨ a .fst ∈ Lset (# m) ⟩ → m < k → ⊥₀ aMin m h hm = levelData a .snd .snd m h (lift (subst (λ j → m < j) (sym qk) hm)) ``` `LevelAt` の二つの読みは、任意の環境にある任意の位置 `b` と`x` について証明される。外向きに論理式を読むためには、存在量化が隠している情報に名前を付けると便利である。それは、`b` の値において階層のグラフを満たす台の要素 `c` と、`x` の値が `c` の基礎集合に属するという証明である。私的な型 `Body` は、命題的切り詰めを施す前のこの証人データにほかならない。
```agda module _ {n : ℕ} (b x : Fin n) (γ : Vec S n) where ```
```agda private Body : S → Type (ℓ-suc ℓ) Body c = ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩ × ⟨ (lookup x γ) .fst ∈ c .fst ⟩ ``` 内向きの読みでは、`b` が数項 `# k` を表し、`x` が `a` の基礎集合を表すと仮定する。結論は `LevelAt` の三つの成分からなる。`b` の値が `ω` に属すること、`b` における階層の値が `x` の値を含むこと、そして `b` の各要素が添字づける階層の値はそれを含まないことである。証明はこれらを `hω`、`hex`、`hmin` と名付け、存在性と最小性を分けて示す。 ```agda LevelAt-in : (lookup b γ) .fst ≡ # k → (lookup x γ) .fst ≡ a .fst → ⟨ γ ⊨ LevelAt b x ⟩ LevelAt-in qb qx = hω , (hex , hmin) where hω : ⟨ (lookup b γ) .fst ∈ ω ⟩ ``` 第一の成分は、すべての数項が `ω` に属するという基本的事実から従う。等式 `qb` は位置 `b` に格納された値を `# k` と同一視する。そこで `#∈ω k` をこの等式の逆向きに運べば、必要な所属が得られる。この運搬は、明示された数項についての事実を、環境の位置についての同じ事実へ結び付ける。 ```agda hω = subst (λ u → ⟨ u ∈ ω ⟩) (sym qb) (#∈ω k) ``` 存在の成分には、包装された有限段階 `towerS k` を証人として選ぶ。補題 `towerGraph` は `qb` を用いて、この証人が `b` における階層の値であることを示す。その基礎集合は `towerS-fst k` によって `Lset (# k)` なので、残る課題は `qx` で端点をそろえた後の既知の所属 `aIn` である。 ```agda hex : ⟨ γ ⊨ ∃̇ ( LsetGraphAt zero (suc b) ∧̇ (var (suc x) ∈̇ var zero) ) ⟩ hex = ∣ towerS k , (towerGraph k γ b qb , hm) ∣₁ where hm : ⟨ (lookup x γ) .fst ∈ (towerS k) .fst ⟩ hm = subst (λ u → ⟨ (lookup x γ) .fst ∈ u ⟩) (sym (towerS-fst k)) ``` `aIn` はすでに、`a` の基礎集合が `Lset (# k)` に属することを述べている。これを `qx` の逆向きに運ぶと、所属する要素が `a` の基礎集合から `x` の位置の値へ変わる。先の射影に沿う運搬と合わせれば `hm` が得られ、命題的切り詰めの中の存在証人が完成する。 ```agda (subst (λ u → ⟨ u ∈ Lset (# k) ⟩) (sym qx) aIn) ``` この有界全称は大域的な最小性を表す。`b` の値の要素 `u`、`u` において階層のグラフを満たす候補 `c`、および `x` の値が `c` に属するという仮定が与えられたとき、矛盾を導かなければならない。`qb` によって `u` の所属を `# k` への所属に書き換えると、`∈#-elim` は命題的切り詰めのもとで、ある `m < k` と `u = # m` を与える。目標は空の型で命題なので、この切り詰めは除去できる。得られた矛盾を持ち上げるのは、対象言語の否定が置かれた宇宙レベルに合わせるためだけである。 ```agda hmin : ⟨ γ ⊨ ∀̇∈ (var b) (∀̇ ( LsetGraphAt zero (suc zero) ⇒̇ ¬̇ (var (sh2 x) ∈̇ var zero) )) ⟩ hmin u u∈ c hg hmem = lift (rec₁ isProp⊥ step (∈#-elim k (u .fst) (subst (λ w → ⟨ u .fst ∈ w ⟩) qb u∈))) where ``` 明示的な復号として `m < k` と `u .fst ≡ # m` を固定する。グラフの証明 `hg` は、`c` が何らかの候補であること以上を保証する。数項 `# m` の順序数性を運んで `Lset-only` に渡すと、`c` の基礎集合は `Lset (u .fst)` と同一視される。したがって論理式は、存在証人の背後に任意の集合を隠すことはできない。階層のグラフが対応する有限段階を決定する。 ```agda step : Σ[ m ∶ ℕ ] ((m < k) × (u .fst ≡ # m)) → ⊥₀ step (m , (hm , qu)) = aMin m inStage hm where qc : c .fst ≡ Lset (u .fst) qc = Lset-only zero (suc zero) (c ∷ u ∷ γ) hg ``` 仮定された所属を三つの同一視に沿って運ぶ。まず `qc` により`x` の値を `Lset (u .fst)` に入れ、次に `qx` によりその値を`a` の基礎集合へ置き換え、最後に `qu` により `u .fst` を `# m` へ置き換える。得られるのは `a .fst ∈ Lset (# m)` であり、`m < k` のもとで `aMin` がまさに排除する主張である。したがって `k` より小さい数項が添字づける有限段階には `a` は含まれない。 ```agda (subst IsOrd (sym qu) (numeral-ord m)) inStage : ⟨ a .fst ∈ Lset (# m) ⟩ inStage = subst (λ w → ⟨ a .fst ∈ Lset w ⟩) qu (subst (λ w → ⟨ w ∈ Lset (u .fst) ⟩) qx (subst (λ w → ⟨ (lookup x γ) .fst ∈ w ⟩) qc hmem)) ``` 外向きの読みでは `LevelAt b x` を仮定し、引き続き `x` の値を固定した要素 `a` の基礎集合と同一視する。目標は、`b` にある候補が真の数項 `# k` であると示すことである。候補が `ω` に属することから自然数の添字が得られるのは、命題的切り詰めのもとでだけである。目標は累積階層における等式であり、`setIsSet` によってその等式型は命題だと分かるため、切り詰められた数項データをそこへ除去できる。 ```agda LevelAt-out : ⟨ γ ⊨ LevelAt b x ⟩ → (lookup x γ) .fst ≡ a .fst → (lookup b γ) .fst ≡ # k LevelAt-out (hω , (hex , hmin)) qx = rec₁ (setIsSet ((lookup b γ) .fst) (# k)) named hω where ``` まず、復号された添字 `m` が真のレベルより上にある場合を排除する。つまり`k < m` であり、`b` の値が `# m` だと仮定する。`#mono` により `# k` は `# m` に属するので、包装 `numS k` と `towerS k` を使えば、`LevelAt` の最小性の節を実際の有限段階 `Lset (# k)` で適用できる。この節は`x` の値がそこにないと述べるが、これは `aIn` と矛盾する。節が返す矛盾は持ち上げられており、`lower` はこの宇宙の持ち上げだけを除く。これは命題リサイズであって、命題的切り詰めではない。 ```agda notAbove : (m : ℕ) → (lookup b γ) .fst ≡ # m → k < m → ⊥₀ notAbove m qb hk = lower (hmin (numS k) (subst (λ w → ⟨ w ∈ (lookup b γ) .fst ⟩) (sym (numS-fst k)) (subst (λ w → ⟨ # k ∈ w ⟩) (sym qb) (#mono k m hk))) (towerS k) (towerGraph k (numS k ∷ γ) zero (numS-fst k)) ``` この最小性の節に渡す最後の引数は、まさにこれから反証される正の所属である。`aIn` から始め、`qx` の逆向きによって `a` の基礎集合を `x` の値へ置き換え、さらに `towerS-fst k` の逆向きによって `Lset (# k)` をその台の包装の基礎集合へ置き換える。こうして論理式と外部の最小レベルの議論は、同じ有限段階の同じ要素について語る。 ```agda (subst (λ w → ⟨ (lookup x γ) .fst ∈ w ⟩) (sym (towerS-fst k)) (subst (λ w → ⟨ w ∈ Lset (# k) ⟩) (sym qx) aIn))) ``` 次に、復号された添字が真のレベルより下にある場合を排除する。`m < k` なら、`LevelAt` の存在成分は命題的切り詰めのもとで、`b` において階層のグラフを満たし、`x` の値を含む台の要素 `c` を与える。これは `Body` と名付けたデータそのものである。目標は矛盾なので、切り詰めを空の型へ除去できる。明示された各証人は、`a` がすでに第 `m` 有限段階に現れることを強いる。 ```agda notBelow : (m : ℕ) → (lookup b γ) .fst ≡ # m → m < k → ⊥₀ notBelow m qb hm = rec₁ isProp⊥ atTower hex where atTower : Σ[ c ∶ S ] Body c → ⊥₀ atTower (c , (hg , hmem)) = aMin m inStage hm ``` この証人について、`Lset-only` はまず `c` の基礎集合を `b` の値が添字づける階層段階と同一視する。必要な順序数性は `numeral-ord m` から得て、`b` の値が `# m` であるという等式に沿って運ぶ。得られた等式を `cong Lset qb` と合成すると、具体的な同一視 `c .fst ≡ Lset (# m)` が得られる。 ```agda where qc : c .fst ≡ Lset (# m) qc = Lset-only zero (suc b) (c ∷ γ) hg (subst IsOrd (sym qb) (numeral-ord m)) ∙ cong Lset qb ``` 証人に含まれる所属は、これで具体的な有限段階において読める。`qc` に沿って運ぶと `x` の値が `Lset (# m)` に属することになり、さらに `qx` に沿って運ぶとその値は `a` の基礎集合になる。したがって `a` は第 `m` 有限段階にすでに現れており、`m < k` と合わせると `aMin` に反する。ゆえに候補の添字は真のレベルより下ではない。 ```agda inStage : ⟨ a .fst ∈ Lset (# m) ⟩ inStage = subst (λ w → ⟨ w ∈ Lset (# m) ⟩) qx (subst (λ w → ⟨ (lookup x γ) .fst ∈ w ⟩) qc hmem) ``` 最後に、`ω` への所属から復号された数項を同定する。明示された復号データは`j : Lift ℕ` と、`# (lower j)` から `b` の値への等式を含む。その等式を逆にすると `qb` が得られる。自然数の比較から `lower j ≡ k` が得られれば、それに数項写像を施して等式を合成することで、必要な `(lookup b γ) .fst ≡ # k` に到達する。 ```agda named : Σ[ j ∶ Lift ℕ ] (# (lower j) ≡ (lookup b γ) .fst) → (lookup b γ) .fst ≡ # k named (j , qj) = qb ∙ cong #_ (decide (lower j ≟ k)) where qb : (lookup b γ) .fst ≡ # (lower j) ``` 自然数の三分律が、必要な等式をちょうど与える。`lower j < k` の場合は `notBelow` に反し、`k < lower j` の場合は `notAbove` に反し、等しい場合はその証明をそのまま返す。したがって二つの読みは真理値の水準で対応する。真の最小有限段階は `LevelAt` を満たし、この論理式が固定された要素 `a` について報告する候補は、その真のレベルでなければならない。 ```agda qb = sym qj decide : NatOrder.Trichotomy (lower j) k → lower j ≡ k decide (NatOrder.lt h) = ⊥₀-rec (notBelow (lower j) qb h) decide (NatOrder.eq e) = e decide (NatOrder.gt h) = ⊥₀-rec (notAbove (lower j) qb h) ```
## 最初の相違を内部で述べる 論理式で集合を比較するには、構成可能な台の外部の要素を、まず意味論的な台`S` の要素として提示しなければならない。`A : S` で、その基礎集合に `z`が属するなら、構成可能性の推移性により、`A` に格納された証明から `z` が構成可能であるという証明が得られる。`memS` は `z` をこの継承された証明とともに包装する。これは依存的な台の要素を作るのであって、集合論的な順序対を作るのではない。 ```agda opaque memS : (A : S) (z : V ℓ) → ⟨ z ∈ A .fst ⟩ → S memS A z h = z , isL-trans {x = A .fst} {y = z} h (A .snd) ``` 射影等式 `memS-fst` は、この包装が議論中の集合を保つことを述べる。`memS A z h` の基礎集合は `z` である。この等式自体は反射性で成り立つが、補題として明示することで、後の運搬は包装を展開せずに、量化された台の要素とそれが表す外部の集合との間を行き来できる。 ```agda memS-fst : (A : S) (z : V ℓ) (h : ⟨ z ∈ A .fst ⟩) → (memS A z h) .fst ≡ z memS-fst A z h = refl ``` `PrecedesAt` は、`r` に格納された関係と `A` に格納された台に相対して、最初の相違による比較の一段階を表す。`x` と `y` にある集合について、台の要素 `z` で、`y` には属するが `x` には属さないものを要求する。この向きが比較を決める。決定点では右側の集合の所属値が一、左側の集合の所属値が零なので、`x` が `y` に先立つ。 ```agda PrecedesAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n PrecedesAt r A x y = ∃̇ ( (var zero ∈̇ var (suc A)) ∧̇ ( (var zero ∈̇ var (suc y)) ∧̇ ( ¬̇ (var zero ∈̇ var (suc x)) ``` この証人はさらに、`r` の関係が定める最初の相違でなければならない。台 `A`の各 `w` について、その関係が `w` を `z` より前に置くなら、`w` の `x` への所属と `y` への所属は両方向で一致しなければならない。論理式は `appAt` を通して関係を調べる。意味論的には、`w` と `z` の集合論的な順序対が `r` に格納された関係集合に属するかを問うている。`z` を束縛する存在量化子と `w` を束縛する全称量化子が、以前の変項を二つずらす理由である。 ```agda ∧̇ ∀̇∈ (var (suc A)) ( appAt (sh2 r) zero (suc zero) ⇒̇ ( ((var zero ∈̇ var (sh2 x)) ⇒̇ (var zero ∈̇ var (sh2 y))) ∧̇ ((var zero ∈̇ var (sh2 y)) ⇒̇ (var zero ∈̇ var (sh2 x))) ) ) ) ) ) ``` モジュール `Precedes` は、この論理式を読むために必要なデータを正確に述べる。四つの位置と環境に加えて、メタレベルの関係 `R` を固定する。法則 `Rrep` は `r` にある関係集合への集合論的な順序対の所属を `R` の事実として読み、`Rfill` はその事実を所属へ書き戻す。これらの法則が構成可能な端点だけを扱えば十分なのは、量化された端点はすでに`S` に属し、外部の台の要素も `memS` で包装できるからである。ここでは `R` に順序公理を仮定しない。この論理式は一段階の比較の定義を表すだけであり、特定の関係が整列順序であるという後の証明には依存しない。
```agda module Precedes {n : ℕ} (r A x y : Fin n) (γ : Vec S n) (R : V ℓ → V ℓ → hProp (ℓ-suc ℓ)) (Rrep : (u v : S) → ⟨ pr (u .fst) (v .fst) ∈ (lookup r γ) .fst ⟩ → ⟨ R (u .fst) (v .fst) ⟩) (Rfill : (u v : S) → ⟨ R (u .fst) (v .fst) ⟩ → ⟨ pr (u .fst) (v .fst) ∈ (lookup r γ) .fst ⟩) where ```
まず台を固定する。相違点より前の要素についての各主張は、環境の `A` にある値が表す構成可能集合に制限される。したがって、比較が基礎関係の働く段階の外へ出ることはない。 ```agda private Aʟ : S Aʟ = lookup A γ ``` 環境の `x` にある値が表す集合を `xv` と書く。これにより、各節で環境からの参照を繰り返さずに、左側の集合への所属を述べられる。 ```agda xv : V ℓ xv = (lookup x γ) .fst ``` 同様に、`yv` は環境の `y` にある値が与える集合を表す。この二つの名前の順序は重要である。最初の相違点は右側の集合に属し、左側の集合には属さないからである。 ```agda yv : V ℓ yv = (lookup y γ) .fst ``` 最初の相違点より前では、二つの集合は所属について同じ答えを与えなければならない。`Both w` はこの同値を正確に記録し、`w` の `xv` への所属から `yv` への所属を導き、その逆も導く。 ```agda Both : V ℓ → Type (ℓ-suc ℓ) Both w = (⟨ w ∈ xv ⟩ → ⟨ w ∈ yv ⟩) × (⟨ w ∈ yv ⟩ → ⟨ w ∈ xv ⟩) ``` 相違の証人の候補 `z` に対して、`Agreeing z` は、符号化された基礎関係によって `z` より前に置かれる台の各要素 `w` を調べる。アトム `appAt r w z` は、関係集合が `w` と `z` の順序対を含むことを意味し、その仮定のもとで `xv` と `yv` は `w` において一致しなければならない。 ```agda Agreeing : S → Type (ℓ-suc ℓ) Agreeing z = (w : S) → ⟨ w .fst ∈ Aʟ .fst ⟩ → ⟨ (w ∷ z ∷ γ) ⊨ appAt (sh2 r) zero (suc zero) ⟩ → Both (w .fst) ``` 証人自身は台と `yv` に属し、`xv` には属さなければならない。また、基礎関係でそれより前にある台の要素はすべて一致条件を満たす。したがって、この向きは `xv` が `yv` に先行することを表す。ここでは与えられた基礎関係に順序法則を仮定していないため、「最初」という読みは、その関係が実際に順序である場合に限って正当化される。 ```agda Body : S → Type (ℓ-suc ℓ) Body z = ⟨ z .fst ∈ Aʟ .fst ⟩ × ( ⟨ z .fst ∈ yv ⟩ × ( (⟨ z .fst ∈ xv ⟩ → Lift {j = ℓ-suc ℓ} ⊥₀) × Agreeing z ) ) ``` 論理式を外へ読むには、その命題的に切り詰められた存在を命題 `precedes R A xv yv` へ消去する。示された各モデル内の証人をホスト側の定義の証人へ移せば十分である。目標もその命題的切り詰めだけを保持するからである。 ```agda PrecedesAt-out : ⟨ γ ⊨ PrecedesAt r A x y ⟩ → ⟨ precedes R (Aʟ .fst) xv yv ⟩ PrecedesAt-out = rec₁ squash₁ atZ where atZ : Σ[ z ∶ S ] Body z → ⟨ precedes R (Aʟ .fst) xv yv ⟩ ``` `z` の底の集合がホスト側の証人となり、最初の三つの成分が台への所属と向きづけられた相違をすでに与える。残る課題は、それより前にある任意のホスト側の要素 `w` で両側が一致することを示すことである。 ```agda atZ (z , (z∈A , (z∈y , (z∉x , hag)))) = ∣ z .fst , (z∈A , (z∈y , ((λ h → lower (z∉x h)) , ag))) ∣₁ where ag : Agrees R (Aʟ .fst) xv yv (z .fst) ag w w∈A hR = subst Both (memS-fst Aʟ w w∈A) (hag wS w∈A' happ) ``` `w` は構成可能な台に属するので構成可能性を受け継ぎ、モデルの要素 `wS` としてまとめられる。その射影の等式に沿って、もとの台への所属の証明を、対象言語の有界な節が要求する形へ運ぶ。 ```agda where wS : S wS = memS Aʟ w w∈A w∈A' : ⟨ wS .fst ∈ Aʟ .fst ⟩ w∈A' = subst (λ u → ⟨ u ∈ Aʟ .fst ⟩) (sym (memS-fst Aʟ w w∈A)) w∈A ``` いまの仮定はホスト側で `R w z` を述べている。`w` を `wS` とそろえた後、`Rfill` はこの事実を順序対の関係集合への所属として書き込む。これは適用アトムを示すために必要な情報そのものである。 ```agda hp : ⟨ pr (wS .fst) (z .fst) ∈ (lookup r γ) .fst ⟩ hp = Rfill wS z (subst (λ u → ⟨ R u (z .fst) ⟩) (sym (memS-fst Aʟ w w∈A)) hR) happ : ⟨ (wS ∷ z ∷ γ) ⊨ appAt (sh2 r) zero (suc zero) ⟩ happ = subst ⟨_⟩ ``` `appAt` の妥当性により、この順序対の所属の主張は、`wS` と `z` で拡張した環境における充足へ変換される。これで対象言語の一致の仮定を適用できる。 ```agda (sym (appAt-adequate (sh2 r) zero (suc zero) (wS ∷ z ∷ γ))) hp ``` 逆向きは、`precedes` にある命題的に切り詰められた証人から始まる。`PrecedesAt` の充足自体が命題なので、この切り詰めを消去し、各ホスト側の証人を対象言語の存在証人へ変換できる。 ```agda PrecedesAt-in : ⟨ precedes R (Aʟ .fst) xv yv ⟩ → ⟨ γ ⊨ PrecedesAt r A x y ⟩ PrecedesAt-in = rec₁ squash₁ atZ where atZ : Σ[ z ∶ V ℓ ] Witness R (Aʟ .fst) xv yv z ``` ホスト側の証人 `z` を、台への所属、右側への所属、左側からの排除、より前の点での一致とともに取り出す。台への所属から `z` の構成可能性が得られるので、`zS` を論理式の量化された証人として使える。 ```agda → ⟨ γ ⊨ PrecedesAt r A x y ⟩ atZ (z , (z∈A , (z∈y , (z∉x , ag)))) = ∣ zS , (z∈A' , (z∈y' , (z∉x' , hag))) ∣₁ where zS : S ``` 射影 `zS .fst` はもとの `z` に等しい。この等式に沿って運ぶと、まとめられた証人も台に属することが分かる。したがって、まとめる操作は表示だけを変え、数学的な役割は変えない。 ```agda zS = memS Aʟ z z∈A qz : zS .fst ≡ z qz = memS-fst Aʟ z z∈A z∈A' : ⟨ zS .fst ∈ Aʟ .fst ⟩ z∈A' = subst (λ u → ⟨ u ∈ Aʟ .fst ⟩) (sym qz) z∈A ``` 同じ射影の等式に沿って、`yv` への所属と `xv` への非所属も運ぶ。あとは論理式の関係についての仮定を `R` へ読み戻せば、ホスト側の一致の仮定を使える。 ```agda z∈y' : ⟨ zS .fst ∈ yv ⟩ z∈y' = subst (λ u → ⟨ u ∈ yv ⟩) (sym qz) z∈y z∉x' : ⟨ zS .fst ∈ xv ⟩ → Lift {j = ℓ-suc ℓ} ⊥₀ z∉x' h = lift (z∉x (subst (λ u → ⟨ u ∈ xv ⟩) qz h)) hag : Agreeing zS ``` 台に属するモデル要素 `w` が与えられると、`appAt` の妥当性はまず充足を、`w` と `zS` の順序対が符号化された関係に属するという主張へ読み替える。これは外向きの証明で用いた移行の逆向きである。 ```agda hag w w∈A happ = ag (w .fst) w∈A hR where hp : ⟨ pr (w .fst) (zS .fst) ∈ (lookup r γ) .fst ⟩ hp = subst ⟨_⟩ (appAt-adequate (sh2 r) zero (suc zero) (w ∷ zS ∷ γ)) happ hR : ⟨ R (w .fst) z ⟩ ``` ここで `Rrep` は関係集合への所属を `R (w .fst) zS` として読み戻す。第二の端点を `zS .fst` から `z` へ運ぶと、もとの一致の証明が要求する仮定が得られ、`Both` の二つの所属の含意が従う。 ```agda hR = subst (λ u → ⟨ R (w .fst) u ⟩) qz (Rrep w zS hp) ```
## 順序を合成する 要素 `a : Limit` は、その底の集合が `Lset ω` に属するという証明を持つ。この構成可能な段階への所属から必要な `isL` の証拠が得られ、同じ底の集合をモデル要素 `limitEl a` とみなせる。 ```agda opaque limitEl : Limit → S limitEl a = a .fst , Lset→isL ω ω-ord (a .fst) (a .snd) ``` まとめる操作は集合を変えない。`limitEl a` を射影すると、定義により `a .fst` が戻る。この等式は後で、モデル内で作った順序対を表現定理に現れる周囲の順序対とそろえる。 ```agda limitEl-fst : (a : Limit) → (limitEl a) .fst ≡ a .fst limitEl-fst a = refl ``` 関係を `L` の内部に置くには、関係する二つの端点を、それ自身がモデル要素である順序対で表さなければならない。`prS` は任意の二つの構成可能な端点に対して、その内部順序対を与える。 ```agda prS : S → S → S prS a b = prʟ a b ``` `prS` の射影則は、その底の集合を二つの端点の底の集合からなる周囲の順序対と同一視する。したがって、内部の対構成と外部の関係への所属は同じ集合について述べている。 ```agda prS-fst : (a b : S) → (prS a b) .fst ≡ pr (a .fst) (b .fst) prS-fst a b = prʟ-fst a b ``` 分出によって比較を満たす順序対を選ぶ前に、候補となるすべての対を含む集合サイズの共通の上界が必要である。`Lset ω` の要素を小さなファイバーで表示し、各要素を構成可能なものとしてまとめ、その二つの小さなファイバーの積で順序対を添字づける。 ```agda pairsBound : Σ[ D ∶ S ] ((u v : Limit) → ⟨ pr (u .fst) (v .fst) ∈ D .fst ⟩) pairsBound = d .fst , onPair where ixL : ⟪ Lset ω ⟫ → S ixL m = ⟪ Lset ω ⟫↪ m , Lset→isL ω ω-ord (⟪ Lset ω ⟫↪ m) ``` 各表示添字は実際に `Lset ω` の要素を表す。所属の橋は表示についての事実を通常の所属へ変え、その段階への所属から `ixL` がまとめるために必要な構成可能性の証明が得られる。 ```agda (∈∈ₛ {a = ⟪ Lset ω ⟫↪ m} {b = Lset ω} .snd (∈ₛ⟪ Lset ω ⟫↪ m)) ``` この小さな積に `smallDom` を適用すると、内部で作られたすべての順序対を含む構成可能集合が得られる。これは共通の上界にすぎず、余分な対象を含んでもかまわない。正確な比較関係は、その中で分出を行うことによって得られる。 ```agda d : Σ[ D ∶ S ] ((p : ⟪ Lset ω ⟫ × ⟪ Lset ω ⟫) → ⟨ prʟ (ixL (p .fst)) (ixL (p .snd)) ∈ˢ D ⟩) d = smallDom (⟪ Lset ω ⟫ × ⟪ Lset ω ⟫) (λ p → prʟ (ixL (p .fst)) (ixL (p .snd))) ``` 任意の `u,v : Limit` に対し、それぞれの底の集合は `Lset ω` の小さなファイバー内に表示添字を持つ。その添字から作った順序対は共通の上界に属し、射影の等式に沿って運ぶことで、周囲の順序対 `pr (u .fst) (v .fst)` の所属が得られる。 ```agda onPair : (u v : Limit) → ⟨ pr (u .fst) (v .fst) ∈ (d .fst) .fst ⟩ onPair u v = subst (λ t → ⟨ t ∈ (d .fst) .fst ⟩) (prʟ-fst (ixL (fu .fst)) (ixL (fv .fst)) ∙ cong₂ pr (fu .snd) (fv .snd)) (d .snd (fu .fst , fv .fst)) where ``` 二つのファイバーの証人は、上で使う表示添字と、そこで示される要素をそれぞれ `u .fst`、`v .fst` と同一視する等式を取り出す。この等式があるため、小さな表示で実際のすべての極限段階の端点を扱える。 ```agda fu = ∈-asFiber {a = u .fst} {b = Lset ω} (u .snd) fv = ∈-asFiber {a = v .fst} {b = Lset ω} (v .snd) ``` 論理式から読み取れるのが、極限上の狭義比較の命題的切り詰めだけである場合がある。`strictLimit` は、すでに証明された狭義整列順序 `limitOrder` の三分律を先に調べて比較を復元する。三分律が `a ≺ˡ b` を与える場合、選ぶべきものはもうない。 ```agda strictLimit : (a b : Limit) → ∥ a ≺ˡ b ∥₁ → a ≺ˡ b strictLimit a b h = decide (SWO.tri∙ limitOrder a b) where decide : Tri (a ≺ˡ b) (a ≡ b) (b ≺ˡ a) → a ≺ˡ b decide (lt k) = k ``` 切り詰められた順向きの比較があるなら、三分律の残る二つの場合は不可能である。`a = b` なら、運ぶことで自己比較が得られる。`b ≺ˡ a` なら、隠された順向きの比較と推移性から再び自己比較が得られる。非反射性がどちらの命題も否定するため、命題的切り詰めは矛盾へだけ除去されている。 ```agda decide (eq q) = ⊥₀-rec (rec₁ isProp⊥ (λ k → SWO.irr∙ limitOrder b (subst (λ t → t ≺ˡ b) q k)) h) decide (gt k) = ⊥₀-rec (rec₁ isProp⊥ (λ j → SWO.irr∙ limitOrder a (SWO.trans∙ limitOrder a b a j k)) h) ``` `level a` の定義的性質により、`a .fst` は `finiteStage (level a)` に属する。等式 `level a ≡ k` に沿ってこの所属を `finiteStage k` へ運ぶと、有限段階の比較を使う際に必要な段階の境界がちょうど得られる。 ```agda levelStage : (a : Limit) (k : ℕ) → level a ≡ k → ⟨ a .fst ∈ finiteStage k ⟩ levelStage a k q = subst (λ j → ⟨ a .fst ∈ Lset (# j) ⟩) q (level-in a) ``` `Described` は条件つきの枠組みである。`before m` を記述するための論理式 `BeforeAt` と内向きの規則を受け取る。この規則を使えるのは、`b` にある値が `# m` を表し、第一の端点が `finiteStage m` に属する場合に限られる。
```agda module Described (BeforeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n) (BeforeAt-in : ∀ {n} (b x y : Fin n) (γ : Vec S n) (m : ℕ) → (lookup b γ) .fst ≡ # m → ⟨ (lookup x γ) .fst ∈ finiteStage m ⟩ → ⟨ (lookup y γ) .fst ∈ finiteStage m ⟩ → ⟨ before m ((lookup x γ) .fst) ((lookup y γ) .fst) ⟩ → ⟨ γ ⊨ BeforeAt b x y ⟩) (BeforeAt-out : ∀ {n} (b x y : Fin n) (γ : Vec S n) (m : ℕ) → (lookup b γ) .fst ≡ # m → ⟨ (lookup x γ) .fst ∈ finiteStage m ⟩ → ⟨ (lookup y γ) .fst ∈ finiteStage m ⟩ → ⟨ γ ⊨ BeforeAt b x y ⟩ → ⟨ before m ((lookup x γ) .fst) ((lookup y γ) .fst) ⟩) where ```
内向きの仮定は、第二の端点も同じ有限段階に属することと、実際の比較 `before m x y` が成り立つことをさらに要求し、そこから `BeforeAt` の充足を与える。したがって、この枠組みは有限段階の関係を構成せず、その順序法則も導かない。 外向きの仮定も同じ数項と段階の境界を持ち、充足を `before m x y` として読み戻す。両方向を満たす論理式だけがこの枠組みを具体化できる。実際の `BeforeAt` と、そこから得られる `codeOrder` は `EarliestDisagreement` によって与えられ、この時点で無条件に得られるものではない。 `LimitOrdAt` の第一の枝は、レベルが異なる場合を扱う。二つの数項候補を束縛し、それぞれが `x` と `y` の最小レベルであることを示したうえで、`x` の数項が `y` の数項に属することを要求する。これは自然数としてのレベルの狭義不等式を表す。 ```agda opaque LimitOrdAt : ∀ {n} → Fin n → Fin n → Formula S n LimitOrdAt x y = ∃̇ ( ∃̇ ( LevelAt (suc zero) (sh2 x) ∧̇ ( LevelAt zero (sh2 y) ∧̇ (var (suc zero) ∈̇ var zero) ) ) ) ``` 第二の枝は、一つの共通の数項を束縛してレベルが等しい場合を扱う。二つの `LevelAt` の節が同じ数項を最小レベルとして特定し、その後、仮定された `BeforeAt` がその有限段階の内部で端点を比較する。一つの証人を共有することで、対象言語の等号を別に加えずに等しさを表せる。 ```agda ∨̇ ∃̇ ( LevelAt zero (suc x) ∧̇ ( LevelAt zero (suc y) ∧̇ BeforeAt zero (suc x) (suc y) ) ) ``` この論理式の妥当性を示すため、環境の二つの位置 `x` と `y` を固定し、その値を実際の `u,v : Limit` と同一視する。明示された添字 `ku,kv` と真のレベルとの等式により、自然数の比較、数項の所属、段階への所属の間を明確に移れる。
```agda module Order {n : ℕ} (x y : Fin n) (γ : Vec S n) (u v : Limit) (ku kv : ℕ) (qu : level u ≡ ku) (qv : level v ≡ kv) (qx : (lookup x γ) .fst ≡ u .fst) (qy : (lookup y γ) .fst ≡ v .fst) where ```
二つの `Level` の具体例は、単に便利な名前を与えるだけではない。それぞれが、対応する実際の端点とその最小レベルについて、`LevelAt` の検証済みの読みを与える。外向きに読むとき、この橋によって見かけだけの数項証人が排除される。 ```agda private module Lu = Level u ku qu private module Lv = Level v kv qv ``` `Split c d` はレベルが異なる枝の意味内容である。`c` が左端点の最小レベルの数項、`d` が右端点の最小レベルの数項であり、さらに `c ∈ d` が成り立つことを述べる。最後の条件によって、左のレベルが右のレベルより小さいという向きが定まる。 ```agda private Split : S → S → Type (ℓ-suc ℓ) Split c d = ⟨ (d ∷ c ∷ γ) ⊨ LevelAt (suc zero) (sh2 x) ⟩ × ( ⟨ (d ∷ c ∷ γ) ⊨ LevelAt zero (sh2 y) ⟩ × ⟨ c .fst ∈ d .fst ⟩ ) ``` `Same c` はレベルが等しい枝の意味内容である。同じ `c` が両方の端点の最小レベルを記述しなければならず、その後に限って `BeforeAt c x y` が共通の有限段階内での比較を与える。 ```agda Same : S → Type (ℓ-suc ℓ) Same c = ⟨ (c ∷ γ) ⊨ LevelAt zero (suc x) ⟩ × ( ⟨ (c ∷ γ) ⊨ LevelAt zero (suc y) ⟩ × ⟨ (c ∷ γ) ⊨ BeforeAt zero (suc x) (suc y) ⟩ ) ``` `ku < kv` と仮定する。二つの存在証人には、モデル要素としてまとめた真の数項 `# ku` と `# kv` を選ぶ。二つの `LevelAt-in` によって、これらの数項が、そろえられた端点の実際の最小レベルを記述することが確かめられる。 ```agda split-in : ku < kv → Split (numS ku) (numS kv) split-in hlt = Lu.LevelAt-in (suc zero) (sh2 x) (numS kv ∷ numS ku ∷ γ) (numS-fst ku) qx , ( Lv.LevelAt-in zero (sh2 y) (numS kv ∷ numS ku ∷ γ) ``` 自然数の狭義不等式から、数項の単調性により `# ku ∈ # kv` が得られる。二つのまとめられた数項の射影等式に沿って運ぶと、`Split` が要求する所属 `(numS ku) .fst ∈ (numS kv) .fst` が得られる。 ```agda (numS-fst kv) qy , subst2 (λ s t → ⟨ s ∈ t ⟩) (sym (numS-fst ku)) (sym (numS-fst kv)) (#mono ku kv hlt) ) ``` 同じレベルの枝では、等式 `level v ≡ level u` により、一つの数項 `# ku` で両方の端点を記述できる。左側の `LevelAt` の読みは `qu` を直接使い、右側の読みはこの等式を使って `v` のレベルも同じ添字 `ku` で表す。 ```agda same-in : (e : level v ≡ level u) → ⟨ before (level u) (u .fst) (v .fst) ⟩ → Same (numS ku) same-in e h = Lu.LevelAt-in zero (suc x) (numS ku ∷ γ) (numS-fst ku) qx , ( Level.LevelAt-in v ku (e ∙ qu) zero (suc y) (numS ku ∷ γ) ``` 条件つきの仮定 `BeforeAt-in` を使えるのは、必要な境界を先に示した後だけである。レベルの等式によって参照された二つの端点はどちらも `finiteStage ku` に置かれ、`numS ku` の射影等式によって、共通の数項として与えた値が確かに `# ku` を表すことが分かる。 ```agda (numS-fst ku) qy , BeforeAt-in zero (suc x) (suc y) (numS ku ∷ γ) ku (numS-fst ku) (subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qx) (levelStage u ku qu)) (subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qy) ``` 最後に、与えられた比較を添字 `level u` から `ku` へ運び、その二つの端点を環境の値とそろえる。二つの段階への所属の証明と合わせると、`BeforeAt-in` のすべての仮定が満たされ、`Same (numS ku)` が完成する。 ```agda (levelStage v ku (e ∙ qu))) (subst2 (λ s t → ⟨ before ku s t ⟩) (sym qx) (sym qy) (subst (λ j → ⟨ before j (u .fst) (v .fst) ⟩) qu h)) ) ``` `Split c d` を外へ読むとき、まず二つの `LevelAt-out` の補題によって `c` を `# ku`、`d` を `# kv` と同一視する。これらの同一視に沿って `c ∈ d` を運び、数項の所属を消去すると `ku < kv` が得られる。保存されたレベルの等式により、これは `level u < level v` へ変わる。 ```agda split-out : (c d : S) → Split c d → level u < level v split-out c d (hx , (hy , hlt)) = subst2 _<_ (sym qu) (sym qv) (#∈#-elim ku kv (subst2 (λ s t → ⟨ s ∈ t ⟩) qc qd hlt)) where qc : c .fst ≡ # ku ``` それぞれの数項の同一視は、正しく拡張された環境で得られる。第一の `LevelAt` は二つの新しい証人を越えて `x` を参照し、第二の `LevelAt` は `y` を参照する。この束縛子の整合により、最後の不等式が証人自身ではなく、もとの二つの端点の真のレベルを比較していることが保証される。 ```agda qc = Lu.LevelAt-out (suc zero) (sh2 x) (d ∷ c ∷ γ) hx qx qd : d .fst ≡ # kv qd = Lv.LevelAt-out zero (sh2 y) (d ∷ c ∷ γ) hy qy ``` 同じ段階の枝では、一つのモデル要素 `c` が `u` と `v` の双方に対する候補の段階番号を表す。二つの `LevelAt` の証明を読み取ると、実際の段階番号が一致することと、与えられた有限段階の論理式がその共通段階での `u` と `v` の比較を表すことが得られる。 ```agda same-out : (c : S) → Same c → (level v ≡ level u) × ⟨ before (level u) (u .fst) (v .fst) ⟩ same-out c (hx , (hy , hb)) = e , below where qc : c .fst ≡ # ku ``` 一つ目の証明は `c` の台となる集合を数項 `# ku` と同定し、二つ目はそれを `# kv` と同定する。数項符号化の単射性から `ku = kv` が従い、これを `ku` と `kv` を定める段階番号の等式と合成すると `level v = level u` が得られる。したがって、段階番号の一致は対象言語の論理式に等式として書かれるのではなく、共通の証人から復元される。 ```agda qc = Lu.LevelAt-out zero (suc x) (c ∷ γ) hx qx qc' : c .fst ≡ # kv qc' = Lv.LevelAt-out zero (suc y) (c ∷ γ) hy qy e : level v ≡ level u e = qv ∙ sym (#-inj′ (sym qc ∙ qc')) ∙ sym qu ``` 仮定された `BeforeAt` の読み取り方向を使うには、比較する二つの集合が同じ有限段階に属することが必要である。`u` の段階所属から `ku` における事実が得られ、新しく得た段階番号の等式によって `v` も同じ段階に置かれる。さらに環境の等式が、この二つの集合を `x` と `y` にある値に同定する。 ```agda xIn : ⟨ (lookup x γ) .fst ∈ finiteStage ku ⟩ xIn = subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qx) (levelStage u ku qu) yIn : ⟨ (lookup y γ) .fst ∈ finiteStage ku ⟩ yIn = subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qy) (levelStage v ku (e ∙ qu)) ``` ここで、`c` が表す数項のもとで抽象的な仮定 `BeforeAt-out` を適用できる。まず環境の二つの値に対する `before ku` が得られ、それらを `u .fst` と `v .fst` に、さらに `ku` を `level u` に置き換えると、極限段階の順序の同段階枝に必要な有限段階の比較になる。この議論では、仮定された段階の境界外で `BeforeAt` に意味があるとは仮定していない。 ```agda below : ⟨ before (level u) (u .fst) (v .fst) ⟩ below = subst (λ j → ⟨ before j (u .fst) (v .fst) ⟩) (sym qu) (subst2 (λ s t → ⟨ before ku s t ⟩) qx qy (BeforeAt-out zero (suc x) (suc y) (c ∷ γ) ku qc xIn yIn hb)) ``` `LimitOrdAt` の二つの数学的な枝の意味は、その妥当性の法則によって保たれる。段階番号が異なる場合は数項を比較し、同じ場合は与えられた有限段階の論理式を使う。不透明な境界により、この定義を使うたびにその二つの法則を経由する。したがって、`Described` 内のすべての結果は三つの入力を仮定した条件つきである。 ```agda opaque unfolding LimitOrdAt ``` まず、`u` が `v` より真に早い有限段階で初めて現れるとする。対象言語で用いる二つの証人はモデル内の数項 `# ku` と `# kv` である。それぞれの `LevelAt` の証明が二対象の段階番号を同定し、最初の数項が二つ目に属することが `ku < kv` を表す。これらのデータが `LimitOrdAt` の異なる段階の枝を成する。 ```agda LimitOrdAt-in : u ≺ˡ v → ⟨ γ ⊨ LimitOrdAt x y ⟩ LimitOrdAt-in h = decide-in h where lower-in : ku < kv → ⟨ γ ⊨ LimitOrdAt x y ⟩ lower-in hlt = ∣ inl ∣ numS ku , ∣ numS kv , split-in hlt ∣₁ ∣₁ ∣₁ ``` 段階番号が一致する場合は、一つの数項 `# ku` が二つの `LevelAt` の主張を同時に保証する。外部比較の有限段階部分は、その共通段階における `BeforeAt` の論理式へ書き込まれる。一つの証人を共有すること自体が二つの段階番号の一致を表すので、対象言語で二つの段階番号の数項の等式を書く必要はない。 ```agda inner-in : (e : level v ≡ level u) → ⟨ before (level u) (u .fst) (v .fst) ⟩ → ⟨ γ ⊨ LimitOrdAt x y ⟩ inner-in e k = ∣ inr ∣ numS ku , same-in e k ∣₁ ∣₁ ``` 外部の極限比較は、ちょうどこの二つの選択肢からなる。第一の枝にある `Lift` は命題の宇宙だけを持ち上げており、`lower` はそのリサイズを戻して通常の自然数の不等式を取り出す。`ku` と `kv` の定義等式で添字をそろえれば、異なる段階の枝を構成できる。 ```agda decide-in : Lift {ℓ-zero} {ℓ-suc ℓ} (level u < level v) ⊎ ((level v ≡ level u) × ⟨ before (level u) (u .fst) (v .fst) ⟩) → ⟨ γ ⊨ LimitOrdAt x y ⟩ decide-in (inl k) = lower-in (subst2 _<_ qu qv (lower k)) ``` 外部比較の第二の選択肢には、共通段階の構成に必要な二つの要素、すなわち段階番号の等式とその段階での `before` 比較がすでに含まれている。これらを同段階の構成へ渡すと、書き込み方向が完成する。したがって `LimitOrdAt-in` は既存の極限順序の辞書式定義に従うものであり、新しい順序を導入するものではない。 ```agda decide-in (inr (e , k)) = inner-in e k ``` `LimitOrdAt` の読み取りは、二つの枝の選択が命題的切り詰めの中にある状態から始まるため、最初に得られる比較も命題的切り詰められている。異なる段階の枝では、二つの存在証人を `split-out` で読み、数項の所属を実際の段階番号の狭義不等式へ戻す。その不等式を外部の極限比較の第一の枝に入れ、切り詰めの内側に保つ。 ```agda LimitOrdAt-out : ⟨ γ ⊨ LimitOrdAt x y ⟩ → ∥ u ≺ˡ v ∥₁ LimitOrdAt-out = rec₁ squash₁ decide where atSplit : (c : S) → Σ[ d ∶ S ] Split c d → ∥ u ≺ˡ v ∥₁ atSplit c (d , hs) = ∣ inl (lift (split-out c d hs)) ∣₁ ``` 同じ段階の枝では、`same-out` が実際の段階番号の等式と、その有限段階における `before` の比較を返す。この二つがそのまま外部の極限比較の第二の枝になる。この場合、段階番号の不等式は導かれず、順序情報はすべて段階内の比較から得られる。 ```agda atSame : Σ[ c ∶ S ] Same c → ∥ u ≺ˡ v ∥₁ atSame (c , hs) = ∣ inr (same-out c hs) ∣₁ ``` 意味論的な選言は、各証人を調べる前に二つの数学的場合を分ける。左側には入れ子になった二つの段階番号の存在証人と数項の所属があり、右側には一つの共通段階と有限段階の論理式がある。この形は、まず段階番号を比較し、同じなら段階内を比較する極限順序の辞書式構造に対応する。 ```agda decide : ⟨ γ ⊨ ∃̇ ( ∃̇ ( LevelAt (suc zero) (sh2 x) ∧̇ ( LevelAt zero (sh2 y) ∧̇ (var (suc zero) ∈̇ var zero) ) ) ) ⟩ ⊎ ⟨ γ ⊨ ∃̇ ( LevelAt zero (suc x) ∧̇ ( LevelAt zero (suc y) ``` 各存在証人は、命題的切り詰められた目標に対してだけ除去される。異なる段階の場合は二つの候補を局所的に取り出して `atSplit` を適用し、同じ段階の場合は一つの共通候補を取り出して `atSame` を適用する。証人はその比較を正当化するために局所的に使われ、段階番号の数項の選択が切り詰めの外へ出ることはない。 ```agda ∧̇ BeforeAt zero (suc x) (suc y) ) ) ⟩ → ∥ u ≺ˡ v ∥₁ decide (inl h) = rec₁ squash₁ (λ { (c , hd) → rec₁ squash₁ (atSplit c) hd }) h decide (inr h) = rec₁ squash₁ atSame h ```
## 順序を集合にする 比較を関係集合へ変えるには、分出条件が候補の要素を順序対として認識しなければならない。`Cond₀` は候補の成分 `c` と `d` を束縛し、候補がそれらの符号化された順序対であることと、`LimitOrdAt c d` が成り立つことを要求する。したがって、この条件は要素の対としての形と、表現される比較の向きの両方を述べる。 ```agda Cond₀ : Formula S 1 Cond₀ = ∃̇ ( ∃̇ ( prAtL (sh2 zero) (suc zero) zero ∧̇ LimitOrdAt (suc zero) zero ) ) ``` `Described` の具体例の内部では、極限段階の要素のすべての対を含む共通の上界に `Cond₀` を用いて分出を行う。得られるモデル要素 `codeOrder` は、その上界のうち比較条件を満たす候補をちょうど含む。その存在は、与えられた `BeforeAt` の論理式と二つの妥当性の方向を条件としており、具体的な実現は次の章で与えられる。 ```agda opaque codeOrder : S codeOrder = hasSeparationL (pairsBound .fst) Cond₀ .fst .fst ``` 分出の仕様は、所属について直接使える特徴づけを与える。候補が `codeOrder` に属することは、それが `pairsBound` に属し、かつ `Cond₀` を満たすことと同値である。上界そのものは余分な要素を含み得るので、集合としての包含だけを与える。正確さを担うのは第二の連言であり、順序対を同定して対応する極限比較を検証する。 ```agda codeOrder-mem : (z : S) → (z ∈ˢ codeOrder) ≡ ((z ∈ˢ pairsBound .fst) ⊓ ((z ∷ []) ⊨ Cond₀)) codeOrder-mem = hasSeparationL (pairsBound .fst) Cond₀ .fst .snd ``` `z`、`c`、`d` を固定すると、`Inner` は分出の論理式に必要な二つの事実をまとめる。すなわち、`z` が `c` と `d` の符号化された順序対であることと、`LimitOrdAt` によって `c` が `d` より前にあることである。二つを一緒に保持することで、比較に使う端点が候補の対に符号化された成分そのものであることが明確になる。 ```agda private Inner : S → S → S → Type (ℓ-suc ℓ) Inner z c d = ⟨ (d ∷ c ∷ z ∷ []) ⊨ prAtL (sh2 zero) (suc zero) zero ⟩ × ⟨ (d ∷ c ∷ z ∷ []) ⊨ LimitOrdAt (suc zero) zero ⟩ ``` `Outer z` は、入れ子になった二つの存在量化の証人の形を明示する。第一の成分 `c` に、`Inner z c d` を満たす第二の成分 `d` の命題的切り詰められた存在が伴う。この入れ子は `Cond₀` の意味論と一致し、証人間の依存を保ちながら、`z` の標準的な分解を選ぶことはない。 ```agda Outer : S → Type (ℓ-suc ℓ) Outer z = Σ[ c ∶ S ] ∥ (Σ[ d ∶ S ] Inner z c d) ∥₁ ``` 実際の成分と `Inner` の二つの事実があれば、それらの成分を入れ子になった存在量化へ順に入れることで分出条件を満たせる。対象言語の存在は適切な成分があることだけを記録するため、二つの存在証人はいずれも命題的に切り詰められている。得られる集合への所属も命題なので、分出にはこれで十分である。 ```agda cond-in : (z c d : S) → Inner z c d → ⟨ (z ∷ []) ⊨ Cond₀ ⟩ cond-in z c d hi = ∣ c , ∣ d , hi ∣₁ ∣₁ ``` 逆に、`Cond₀` の充足はすでに `Outer` が記録する切り詰められた入れ子の形をしている。そのため読み取りでは、どちらの成分も選ばずに証拠をそのまま保てる。この点により、後の所属の証明は、命題的切り詰められた存在の範囲にとどまったまま分出条件を展開できる。 ```agda cond-out : (z : S) → ⟨ (z ∷ []) ⊨ Cond₀ ⟩ → ∥ Outer z ∥₁ cond-out z h = h ``` 書き込み則は外部の比較 `u ≺ˡ v` から始め、二つの台となる集合の通常の順序対が `codeOrder` に属することを目指す。まず、モデルの実際の要素である `limitEl u` と `limitEl v`、およびそれらのモデル内で符号化された対を用いる。最後に一つの等式で、この内部表現を `pr (u .fst) (v .fst)` に対応づける。 ```agda codeOrder-fill : (u v : Limit) → u ≺ˡ v → ⟨ pr (u .fst) (v .fst) ∈ codeOrder .fst ⟩ codeOrder-fill u v h = subst (λ t → ⟨ t ∈ codeOrder .fst ⟩) qz (subst ⟨_⟩ (sym (codeOrder-mem (prS (limitEl u) (limitEl v)))) ``` 分出の仕様により、所属の目標は二つの数学的な課題へ帰着する。モデル内で符号化された対が共通の上界に属することと、`limitEl u` と `limitEl v` を二つの証人として `Cond₀` が成り立つことである。これらを満たすと分出の仕様から所属が得られ、二つの対の表現を結ぶ等式に沿って元の目標へ移せる。 ```agda (inBound , cond-in (prS (limitEl u) (limitEl v)) (limitEl u) (limitEl v) (hpr , hord))) where qz : (prS (limitEl u) (limitEl v)) .fst ≡ pr (u .fst) (v .fst) qz = prS-fst (limitEl u) (limitEl v) ``` 対応づけの等式は二つの明確な段階から得られる。モデル内の対の射影は二つの射影からなる外部の順序対であり、各 `limitEl` は元の極限段階の要素の台となる集合へ射影される。これらを合成することで、表現を変えても端点もその順番も変わらないことが保証される。 ```agda ∙ cong₂ pr (limitEl-fst u) (limitEl-fst v) ``` 第一の分出の課題には `pairsBound` の定義的な性質を使う。極限段階の任意の二要素から作る順序対は、この上界に含まれる。包含の証明を使う前に、モデル内で符号化された対を対応する外部の順序対にそろえる。正確な比較条件は `Cond₀` が与えるため、上界の逆向きの特徴づけは不要である。 ```agda inBound : ⟨ (prS (limitEl u) (limitEl v)) .fst ∈ (pairsBound .fst) .fst ⟩ inBound = subst (λ t → ⟨ t ∈ (pairsBound .fst) .fst ⟩) (sym qz) (pairsBound .snd u v) ``` `Cond₀` の対を表す連言は、`prAtL` の妥当性によって示される。モデル内の対はすでに必要な順序対へ射影されるので、その妥当性の法則が射影の等式を対アトムの充足へ変換する。こうして、上界で使う集合論的な順序対と、分出条件で使う対象言語の記述が結びつく。 ```agda hpr : ⟨ (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ []) ⊨ prAtL (sh2 zero) (suc zero) zero ⟩ hpr = subst ⟨_⟩ (sym (prAtL-adequate (sh2 zero) (suc zero) zero (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ []))) (prS-fst (limitEl u) (limitEl v)) ``` 比較を表す連言は、候補の対とその二成分を含む環境で `LimitOrdAt-in` を使って与える。成分を `limitEl u` と `limitEl v` に選べば、必要な対応の等式は反射律であり、元の仮定 `u ≺ˡ v` が比較を与える。これで条件つき表現の順方向が完成する。 ```agda hord : ⟨ (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ []) ⊨ LimitOrdAt (suc zero) zero ⟩ hord = Order.LimitOrdAt-in (suc zero) zero (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ []) u v (level u) (level v) refl refl (limitEl-fst u) (limitEl-fst v) h ``` 読み取り則は、`pr (u .fst) (v .fst)` が `codeOrder` に属することから始まる。分出条件からは、対と比較の条件を満たす二成分が命題的切り詰めの中で得られ、それらを読んでも最初は `∥ u ≺ˡ v ∥₁` だけが得られる。最後に、すでに証明された狭義整列順序 `limitOrder` の三分律で等しい場合と逆向きの比較を排除し、`strictLimit` によって切り詰められていない結論を得る。 ```agda codeOrder-rep : (u v : Limit) → ⟨ pr (u .fst) (v .fst) ∈ codeOrder .fst ⟩ → u ≺ˡ v codeOrder-rep u v h = strictLimit u v (rec₁ squash₁ atC (cond-out (prS (limitEl u) (limitEl v)) ``` 書き込み方向と同様に、モデル内で符号化された対を二つの台となる集合の外部の順序対と同定する。その表現へ所属を移すと、`codeOrder-mem` が分出の二つの連言を示し、第二の連言として `Cond₀` の充足が得られる。端点と比較の情報はすべて分出条件にあるので、ここから先は上界の連言を使う必要がない。 ```agda (subst ⟨_⟩ (codeOrder-mem (prS (limitEl u) (limitEl v))) inSet .snd))) where qz : (prS (limitEl u) (limitEl v)) .fst ≡ pr (u .fst) (v .fst) qz = prS-fst (limitEl u) (limitEl v) ∙ cong₂ pr (limitEl-fst u) (limitEl-fst v) ``` 与えられた所属は外部の順序対についてのものであるが、分出の仕様は `prS` が作るモデル要素に適用される。対を対応づける等式により両者の台となる集合は等しいので、所属をモデル内の表現へ移せる。この表現の変更を行って初めて、そのモデル要素が作る環境で対象言語の条件を読み取れる。 ```agda inSet : ⟨ (prS (limitEl u) (limitEl v)) .fst ∈ codeOrder .fst ⟩ inSet = subst (λ t → ⟨ t ∈ codeOrder .fst ⟩) (sym qz) h ``` 具体的な証人 `c` と `d` に対して、まず対アトムから、それらが元の順序対に符号化された端点であることを示す。得られた端点の等式を必要な向きにすると、`LimitOrdAt-out` が付随する比較の論理式を命題的切り詰められた `u ≺ˡ v` として読み取れる。したがって比較の連言は対の連言から独立には読めない。後者が、論理式がどの外部の極限段階の要素を比較しているかを同定する。 ```agda atD : (c d : S) → Inner (prS (limitEl u) (limitEl v)) c d → ∥ u ≺ˡ v ∥₁ atD c d (hpr , hord) = Order.LimitOrdAt-out (suc zero) zero (d ∷ c ∷ prS (limitEl u) (limitEl v) ∷ []) u v (level u) (level v) refl refl (sym (split .fst)) (sym (split .snd)) hord where ``` 対アトムの妥当性により、その充足は候補の台となる集合と `pr (c .fst) (d .fst)` の等式へ変わる。先の対応づけは、同じ候補を `pr (u .fst) (v .fst)` と同定している。二つの等式を合成すると二つの順序対が等しいことが得られ、`LimitOrdAt` を読むために必要な端点の等式を導ける。 ```agda qcd : pr (u .fst) (v .fst) ≡ pr (c .fst) (d .fst) qcd = sym qz ∙ subst ⟨_⟩ (prAtL-adequate (sh2 zero) (suc zero) zero (d ∷ c ∷ prS (limitEl u) (limitEl v) ∷ [])) hpr split : (u .fst ≡ c .fst) × (v .fst ≡ d .fst) ``` 順序対符号化の単射性により、対の等式は `u .fst = c .fst` と `v .fst = d .fst` に分かれる。成分の位置と順番は保たれるため、左端と右端が入れ替わることはない。これらの等式を逆向きにすると、`LimitOrdAt` の読み取り定理が要求する対応の仮定になる。 ```agda split = pr-inj qcd ``` 外側の読み取りは、`Cond₀` が束縛する順序どおりに入れ子の証人を処理する。まず `c` を取り、次に命題的切り詰めの中で `d` と `Inner` の証拠を扱う。各除去の目標は `atD` が作る命題的切り詰められた比較なので、全過程で切り詰めの制約が守られる。可能なすべての分解をその命題へ写した後、`strictLimit` が最後の切り詰められていない比較を与える。 ```agda atC : Outer (prS (limitEl u) (limitEl v)) → ∥ u ≺ˡ v ∥₁ atC (c , hd) = rec₁ squash₁ (λ { (d , hi) → atD c d hi }) hd ``` ## 符号用のスロットを埋める `CodeKeys` は、任意の構成可能な台 `A` 上の名前比較で、この条件つきのコード関係を利用する一つの方法を記録する。`A` とその構成可能性の証明に加えて、`A` の要素からなる小さい型上の狭義整列順序 `w` を固定する。名前比較の妥当性の結果は、パラメータには `w` を、コードには現在の `Described` の具体例を使える。この入れ子のモジュールは表現定理から得られる再利用可能な帰結であり、主要な構成はこれに依存しない。
```agda module CodeKeys (A : V ℓ) (pA : ⟨ isL A ⟩) (w : SWO ⟪ A ⟫) where ```
```agda private module Ad = Adequacy A pA w ``` `w` の狭義関係には局所的な記号を与え、コードに使う極限段階の比較 `u ≺ˡ v` とパラメータの比較を区別する。二つの関係は異なる台の上にあり、別々の内部関係集合によって表される。妥当性の法則は同じ形であるが、数学的な入力は互いに独立である。 ```agda open SWO w using () renaming ( _<∙_ to _≺ₚ_ ) ``` モデル内の関係 `Ps` がパラメータ順序を双方向に表すなら、`AtParams` はそれを `codeOrder` およびコード順序の二つの表現則とともに `Adequacy.Keys` に渡す。表現される二つの関係は数学的には独立のままである。実際の後続経路では、`EarliestDisagreement` が `Described` を具体化して `codeOrder`、`codeOrder-fill`、`codeOrder-rep` を公開し、`InternalWellOrder` がこの三つを、別に表現されたパラメータ順序とともに `NameComparisonAdequacy.At.Least` へ直接渡する。 ```agda module AtParams (Ps : S) (Prep : (a b : ⟪ A ⟫) → ⟨ pr (Ad.ix a) (Ad.ix b) ∈ Ps .fst ⟩ → a ≺ₚ b) (Pfill : (a b : ⟪ A ⟫) → a ≺ₚ b → ⟨ pr (Ad.ix a) (Ad.ix b) ∈ Ps .fst ⟩) where open Ad.Keys codeOrder Ps codeOrder-rep codeOrder-fill Prep Pfill public ```
## 残る仮定を正確に述べる `Described` に残る入力は、論理式 `BeforeAt` とその二つの読みである。これらの読みが必要とされるのは、最初の値が数項 `# m` であり、二つの端点がともに `finiteStage m` に属する場合だけである。その仮定のもとで、論理式の充足は `before m` による端点の比較と同値になる。モジュール `EarliestDisagreement` は、まさにこのデータを与える。`relAt m` が `before m` を表現し、`beforeFam` が表現された関係を内部自然数に沿って集め、その `BeforeAt` が与えられた数項での関係を取り出してから二つの端点に適用する。これらの結果で `Described` を具体化すると、公開された関係集合 `codeOrder` と、その二つの表現則 `codeOrder-fill` および `codeOrder-rep` が得られる。 ## まとめ `LevelAt` は、与えられた極限段階の要素が最初に現れる有限段階を符号化する数項を同定し、`PrecedesAt` は、すでに表現された任意の基礎関係に相対して、最初の相違による一回の比較を表現する。所定の範囲における `BeforeAt` の双方向の読みが与えられると、`Described` は `LimitOrdAt` の中で異なる段階の比較と同じ段階の比較を組み合わせ、候補となるすべての順序対に上界を与え、分出によって条件つきの関係集合 `codeOrder` を得る。各 `u,v : Limit` に対し、書き込み則と読み取り則は、`u ≺ˡ v` と `pr (u .fst) (v .fst)` がその集合に属することの両方向を与える。読み取り方向では、`strictLimit` と既存の狭義整列順序を用いて、命題的切り詰めから比較を復元する。`EarliestDisagreement` が有限段階についての仮定を満たすが、この章は `codeOrder` が整列順序をなすことを対象言語で主張せず、選択公理も証明しない。