---
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: /llms.txt
license: CC-BY-NC-SA-4.0
---
# L の内部にある極限段階の順序

`Lset ω` の要素には、外側ですでに狭義整列順序が与えられています。ここでの問いは、その比較を `L` の内部の論理式からどのように使えるようにするかです。答えは三つの異なる形を順に通ります。メタ水準の比較、その比較の対象言語による記述、そして有限段階の記述が与えられた後に、その関係を実現する構成可能集合です。

```agda
{-# OPTIONS --cubical --safe --guardedness #-}
```

この章のすべての構成は、レベル `ℓ-suc ℓ` における一つの明示的な排中律の実例に相対しています。先の章では、この仮定から極限段階の要素が最初に現れる有限段階を得ました。この章では、用いる分出と上界の結果にも同じ実例を渡します。この仮定は必要な箇所で命題を判定しますが、任意の族に対する選択関数を与えません。

```agda
open import Base.Prelude
open import Base.Classical using ( LEM )
```

宇宙レベル `ℓ` と、いま説明した排中律の実例を固定します。この時点では、後で作る内部関係はまだ条件つきです。有限段階の順序を表す論理式と、その意味論の二方向を与えた後に、モジュール `Described` の内部で定義されます。次章がその実例を与え、後続の構成が使えるように `codeOrder` を公開します。

```agda
module L.Choice.LimitStageOrder {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

対象言語は、構文と階層における意味を混同せずに比較を記述しなければなりません。論理式は変数、定数、所属、結合子、量化子を使います。定数領域は構成可能な台なので、定数はすでに特定の構成可能集合を指します。後で必要となる二つの基本的な判定は、符号化の補題から得られます。順序対の等式は二つの成分を決定し、数項の符号化も単射です。さらに `#mono` は `k < m` を、`# k` が `# m` に属するという事実へ移します。したがって集合論的所属は、有限添字の狭義比較を忠実に表せます。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; var; con; _∈̇_; _∧̇_; _∨̇_; ¬̇_; _⇒̇_; ∃̇_; ∀̇_; ∀̇∈ )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′ )
```

ここで用いる構造は構成可能宇宙です。その台の要素は、集合と構成可能性の証拠をひとまとめにします。推移性により、その集合の各要素にも同じ種類の証拠が得られます。このため、通常の階層における所属の証人を対象言語の環境へ移せます。とくに、`finiteStage n` は `Lset (# n)` という段階であり、極限段階は
`Lset ω` です。数項と順序数に関する事実により、添字と、それが名指す段階を区別できます。包装された段階と定数 `ωʟ` によって、論理式は構造の内部からこの階層について語れます。

```agda
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 ( ωʟ )
```

三つの橋によって、意味論上の比較を `L` の集合へ変えます。まず `smallDom` は、小さな族を一つの共通な構成可能集合に入れますが、その上界が族の像と一致するとは主張しません。次に分出は、その上界から一変数の論理式を満たす要素だけを正確に取り出します。最後に、順序対、関係への所属、階層列を記述する符号化論理式には、充足を対応する集合の事実へ移す妥当性の法則があります。これらにより、共通の領域を見つける問題と、その領域上で正確な関係を述べる問題を分けて扱えます。

```agda
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 )
```

表現すべき比較は、外側ですでに定義されています。後続段階では、`before (suc n)` が `before n` によってより前の点を並べ、`finiteStage n` の二つの部分集合を最初の相違で比較します。`precedes R A x y` の証人は `A` に属し、`y` に属して `x` には属さず、より前のすべての点で `x` と `y` が一致することを記録します。その存在は命題的に切り詰められています。型 `Limit` は `Lset ω` の要素を包装し、その最小出現段階が `limitOrder` の第一の鍵になります。対応する `before` の比較を使うのは、段階が等しい場合だけです。得られる関係集合の二つの表現方向は、`Adequacy.Keys` が要求する形に正確に一致します。

```agda
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 )
```

`limitOrder` は `SWO` の構造として与えられています。比較そのものに加え、三分性、非反射性、推移性、整礎性を備えます。内部化の議論はこれらの法則を証明し直しません。後では、最初の三つを一つの目的に使います。対象言語の選言から読み戻せるのが命題的に切り詰められた狭義比較だけであるとき、三分性が候補となる枝を示し、非反射性と推移性が両立しない枝を退けます。

```agda
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; Tri; lt; eq; gt )
```

極限の比較は、後で必要となる辞書式の形をしています。第一の選択肢は、最初の要素のレベルが小さいことを述べます。第二の選択肢は、二つのレベルが一致し、その共通レベルの
`before` によって基礎集合を比較します。自然数の三分性が第一の鍵を分析し、`subst2` は等式が符号化されたレベルや端点を同定するとき、二項関係を運びます。付随する `Lift` と `lower` は宇宙レベルをそろえるだけであり、命題的な切り詰めを取り除く操作ではありません。

```agda
import FOL.Absoluteness
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Nat.Order using ( _<_; _≟_ )
import Cubical.Data.Nat.Order as NatOrder
```

対象言語の存在量化と選言は、それぞれ命題的に切り詰められた存在と枝の選択として解釈されます。したがって、その証人を使えるのは、不可能性、階層の集合の等式、別の切り詰めなど、目標が命題である場合だけです。ただし、この章に現れるすべての存在型が切り詰められているわけではありません。型が明示的なデータを要求する場合、包装された台の要素や共通上界はそのまま見えます。また、命題的切り詰めから狭義比較を復元する議論は一般的な除去原理ではなく、`limitOrder` の三分性と順序法則に特有のものです。

```agda
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
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` は、構成可能構造の命題値の所属です。基礎となる階層の集合どうしでは、`fst x ∈ fst y` が周囲の所属を表します。論理式の内部では `_∈̇_` は所属を表す構文上の原子にすぎません。次に導入する充足判定が、第三の形に最初の二つの意味を与えます。この層の区別により、順序を記述する論理式を、その実現集合が内部で整列順序をなすという証明と取り違えずに済みます。

```agda
open hPropStructure 𝒮ʟ
```

判定 `_⊨_` は、周囲の階層構造を構成可能クラスに制限して得られる内側の充足関係です。その台は集合と構成可能性の証拠からなるので、定数も量化される値も構成可能な対象を範囲とします。原子的所属は第一射影を通して解釈され、推移性により、構成可能な限界の要素を再び台の要素として包装できます。したがって充足は、対象言語の論理式から、その基礎集合についての通常の所属事実へ至る正確な橋になります。

```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 : ℕ) → fst (towerS k) ≡ 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 : ℕ) → fst (numS k) ≡ # k
  numS-fst k = refl
```

環境の位置 `i` の基礎集合が `# j` であるとします。補題 `towerGraph` は、新しい位置に `towerS j` を置き、`LsetGraphAt` が二つの位置を関係づけることを証明します。その内容は階層列の仕様そのものです。数項 `# j` に対応する値は段階 `Lset (# j)` です。したがって同じ補題が、真のレベルにおける存在と、そのレベルを用いた最小性の検証の双方に、実際の塔の証人を与えます。

```agda
towerGraph : ∀ {n} (j : ℕ) (δ : S ^ n) (i : Fin n) → fst (lookup i δ) ≡ # 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
  private
    aIn : ⟨ fst a ∈ Lset (# k) ⟩
    aIn = subst (λ j → ⟨ fst a ∈ Lset (# j) ⟩) qk (level-in a)
```

`levelData a` の第二射影は、以下の議論で必要となる最小性を与えます。`a` の基礎集合がすでに `Lset (# m)` に属し、しかも`m < k` なら、等式 `qk` によって後者は
`m < level a` に移され、この最小性に反します。`levelData` が要求する比較は一つ上の宇宙にあるので、ここでは
`lift` で包みます。これは宇宙水準の調整にすぎず、命題的切り詰めとは関係ありません。

```agda
    aMin : (m : ℕ) → ⟨ fst a ∈ Lset (# m) ⟩ → m < k → Empty.⊥
    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) (γ : S ^ n) where
    private
      Body : S → Type (ℓ-suc ℓ)
      Body c = ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩
             × ⟨ fst (lookup x γ) ∈ fst c ⟩
```

内向きの読みでは、`b` が数項 `# k` を表し、`x` が `a` の基礎集合を表すと仮定します。結論は `LevelAt` の三つの成分からなります。`b` の値が `ω` に属すること、`b` における階層の値が `x` の値を含むこと、そして `b` の各要素が添字づける階層の値はそれを含まないことです。証明はこれらを `hω`、`hex`、`hmin` と名付け、存在性と最小性を分けて示します。

```agda
    LevelAt-in : fst (lookup b γ) ≡ # k → fst (lookup x γ) ≡ fst a
               → ⟨ γ ⊨ LevelAt b x ⟩
    LevelAt-in qb qx = hω , (hex , hmin)
      where
      hω : ⟨ fst (lookup b γ) ∈ ω ⟩
```

第一の成分は、すべての数項が `ω` に属するという基本的事実から従います。等式 `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 : ⟨ fst (lookup x γ) ∈ fst (towerS k) ⟩
        hm = subst (λ u → ⟨ fst (lookup x γ) ∈ 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 (PT.rec Empty.isProp⊥ step
        (∈#-elim k (fst u) (subst (λ w → ⟨ fst u ∈ w ⟩) qb u∈)))
        where
```

明示的な復号として `m < k` と `fst u ≡ # m` を固定します。グラフの証明 `hg` は、`c` が何らかの候補であること以上を保証します。数項 `# m` の順序数性を運んで `Lset-only` に渡すと、`c` の基礎集合は `Lset (fst u)` と同一視されます。したがって論理式は、存在証人の背後に任意の集合を隠すことはできません。階層のグラフが対応する有限段階を決定します。

```agda
        step : Σ[ m ∈ ℕ ] ((m < k) × (fst u ≡ # m)) → Empty.⊥
        step (m , (hm , qu)) = aMin m inStage hm
          where
          qc : fst c ≡ Lset (fst u)
          qc = Lset-only zero (suc zero) (c ∷ u ∷ γ) hg
```

仮定された所属を三つの同一視に沿って運びます。まず `qc` により`x` の値を `Lset (fst u)` に入れ、次に `qx` によりその値を`a` の基礎集合へ置き換え、最後に `qu` により `fst u` を
`# m` へ置き換えます。得られるのは
`fst a ∈ Lset (# m)` であり、`m < k` のもとで `aMin` がまさに排除する主張です。したがって `k` より小さい数項が添字づける有限段階には `a` は含まれません。

```agda
            (subst IsOrd (sym qu) (numeral-ord m))
          inStage : ⟨ fst a ∈ Lset (# m) ⟩
          inStage = subst (λ w → ⟨ fst a ∈ Lset w ⟩) qu
            (subst (λ w → ⟨ w ∈ Lset (fst u) ⟩) qx
              (subst (λ w → ⟨ fst (lookup x γ) ∈ w ⟩) qc hmem))
```

外向きの読みでは `LevelAt b x` を仮定し、引き続き `x` の値を固定した要素 `a` の基礎集合と同一視します。目標は、`b` にある候補が真の数項
`# k` であると示すことです。候補が `ω` に属することから自然数の添字が得られるのは、命題的切り詰めのもとでだけです。目標は累積階層における等式であり、`setIsSet` によってその等式型は命題だと分かるため、切り詰められた数項データをそこへ除去できます。

```agda
    LevelAt-out : ⟨ γ ⊨ LevelAt b x ⟩ → fst (lookup x γ) ≡ fst a
                → fst (lookup b γ) ≡ # k
    LevelAt-out (hω , (hex , hmin)) qx =
      PT.rec (setIsSet (fst (lookup b γ)) (# 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 : ℕ) → fst (lookup b γ) ≡ # m → k < m → Empty.⊥
      notAbove m qb hk = lower (hmin (numS k)
        (subst (λ w → ⟨ w ∈ fst (lookup b γ) ⟩) (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 → ⟨ fst (lookup x γ) ∈ 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 : ℕ) → fst (lookup b γ) ≡ # m → m < k → Empty.⊥
      notBelow m qb hm = PT.rec Empty.isProp⊥ atTower hex
        where
        atTower : Σ[ c ∈ S ] Body c → Empty.⊥
        atTower (c , (hg , hmem)) = aMin m inStage hm
```

この証人について、`Lset-only` はまず `c` の基礎集合を `b` の値が添字づける階層段階と同一視します。必要な順序数性は `numeral-ord m`
から得て、`b` の値が `# m` であるという等式に沿って運びます。得られた等式を `cong Lset qb` と合成すると、具体的な同一視
`fst c ≡ Lset (# m)` が得られます。

```agda
          where
          qc : fst c ≡ 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 : ⟨ fst a ∈ Lset (# m) ⟩
          inStage = subst (λ w → ⟨ w ∈ Lset (# m) ⟩) qx
            (subst (λ w → ⟨ fst (lookup x γ) ∈ w ⟩) qc hmem)
```

最後に、`ω` への所属から復号された数項を同定します。明示された復号データは`j : Lift ℕ` と、`# (lower j)` から `b` の値への等式を含みます。その等式を逆にすると `qb` が得られます。自然数の比較から
`lower j ≡ k` が得られれば、それに数項写像を施して等式を合成することで、必要な `fst (lookup b γ) ≡ # k` に到達します。

```agda
      named : Σ[ j ∈ Lift ℕ ] (# (lower j) ≡ fst (lookup b γ))
            → fst (lookup b γ) ≡ # k
      named (j , qj) = qb ∙ cong #_ (decide (lower j ≟ k))
        where
        qb : fst (lookup b γ) ≡ # (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) = Empty.rec (notBelow (lower j) qb h)
        decide (NatOrder.eq e) = e
        decide (NatOrder.gt h) = Empty.rec (notAbove (lower j) qb h)
```

## 最初の相違を内部で述べる

論理式で集合を比較するには、構成可能な台の外部の要素を、まず意味論的な台`S` の要素として提示しなければなりません。`A : S` で、その基礎集合に `z`が属するなら、構成可能性の推移性により、`A` に格納された証明から `z` が構成可能であるという証明が得られます。`memS` は `z` をこの継承された証明とともに包装します。これは依存的な台の要素を作るのであって、集合論的な順序対を作るのではありません。

```agda
opaque
  memS : (A : S) (z : V ℓ) → ⟨ z ∈ fst A ⟩ → S
  memS A z h = z , isL-trans {x = fst A} {y = z} h (snd A)
```

射影等式 `memS-fst` は、この包装が議論中の集合を保つことを述べます。`memS A z h` の基礎集合は `z` です。この等式自体は反射性で成り立ちますが、補題として明示することで、後の運搬は包装を展開せずに、量化された台の要素とそれが表す外部の集合との間を行き来できます。

```agda
  memS-fst : (A : S) (z : V ℓ) (h : ⟨ z ∈ fst A ⟩) → fst (memS A z h) ≡ 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) (γ : S ^ n)
                (R : V ℓ → V ℓ → hProp (ℓ-suc ℓ))
                (Rrep : (u v : S) → ⟨ pr (fst u) (fst v) ∈ fst (lookup r γ) ⟩
                      → ⟨ R (fst u) (fst v) ⟩)
                (Rfill : (u v : S) → ⟨ R (fst u) (fst v) ⟩
```

まず台を固定します。相違点より前の要素についての各主張は、環境の `A` にある値が表す構成可能集合に制限されます。したがって、比較が基礎関係の働く段階の外へ出ることはありません。

```agda
                       → ⟨ pr (fst u) (fst v) ∈ fst (lookup r γ) ⟩)
                where
  private
    Aʟ : S
    Aʟ = lookup A γ
```

環境の `x` にある値が表す集合を `xv` と書きます。これにより、各節で環境からの参照を繰り返さずに、左側の集合への所属を述べられます。

```agda
    xv : V ℓ
    xv = fst (lookup x γ)
```

同様に、`yv` は環境の `y` にある値が与える集合を表します。この二つの名前の順序は重要です。最初の相違点は右側の集合に属し、左側の集合には属さないからです。

```agda
    yv : V ℓ
    yv = fst (lookup y γ)
```

最初の相違点より前では、二つの集合は所属について同じ答えを与えなければなりません。`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) → ⟨ fst w ∈ fst Aʟ ⟩
               → ⟨ (w ∷ z ∷ γ) ⊨ appAt (sh2 r) zero (suc zero) ⟩
               → Both (fst w)
```

証人自身は台と `yv` に属し、`xv` には属さなければなりません。また、基礎関係でそれより前にある台の要素はすべて一致条件を満たします。したがって、この向きは `xv` が `yv` に先行することを表します。ここでは与えられた基礎関係に順序法則を仮定していないため、「最初」という読みは、その関係が実際に順序である場合に限って正当化されます。

```agda
    Body : S → Type (ℓ-suc ℓ)
    Body z = ⟨ fst z ∈ fst Aʟ ⟩
           × ( ⟨ fst z ∈ yv ⟩
             × ( (⟨ fst z ∈ xv ⟩ → Lift {j = ℓ-suc ℓ} Empty.⊥) × Agreeing z ) )
```

論理式を外へ読むには、その命題的に切り詰められた存在を命題 `precedes R A xv yv` へ消去します。示された各モデル内の証人をホスト側の定義の証人へ移せば十分です。目標もその命題的切り詰めだけを保持するからです。

```agda
  PrecedesAt-out : ⟨ γ ⊨ PrecedesAt r A x y ⟩
                 → ⟨ precedes R (fst Aʟ) xv yv ⟩
  PrecedesAt-out = PT.rec squash₁ atZ
    where
    atZ : Σ[ z ∈ S ] Body z → ⟨ precedes R (fst Aʟ) xv yv ⟩
```

`z` の底の集合がホスト側の証人となり、最初の三つの成分が台への所属と向きづけられた相違をすでに与えます。残る課題は、それより前にある任意のホスト側の要素 `w` で両側が一致することを示すことです。

```agda
    atZ (z , (z∈A , (z∈y , (z∉x , hag)))) =
      ∣ fst z , (z∈A , (z∈y , ((λ h → lower (z∉x h)) , ag))) ∣₁
      where
      ag : Agrees R (fst Aʟ) xv yv (fst z)
      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' : ⟨ fst wS ∈ fst Aʟ ⟩
        w∈A' = subst (λ u → ⟨ u ∈ fst Aʟ ⟩) (sym (memS-fst Aʟ w w∈A)) w∈A
```

いまの仮定はホスト側で `R w z` を述べています。`w` を `wS` とそろえた後、`Rfill` はこの事実を順序対の関係集合への所属として書き込みます。これは適用アトムを示すために必要な情報そのものです。

```agda
        hp : ⟨ pr (fst wS) (fst z) ∈ fst (lookup r γ) ⟩
        hp = Rfill wS z
          (subst (λ u → ⟨ R u (fst z) ⟩) (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 (fst Aʟ) xv yv ⟩
                → ⟨ γ ⊨ PrecedesAt r A x y ⟩
  PrecedesAt-in = PT.rec squash₁ atZ
    where
    atZ : Σ[ z ∈ V ℓ ] Witness R (fst Aʟ) 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
```

射影 `fst zS` はもとの `z` に等しいです。この等式に沿って運ぶと、まとめられた証人も台に属することが分かります。したがって、まとめる操作は表示だけを変え、数学的な役割は変えません。

```agda
      zS = memS Aʟ z z∈A
      qz : fst zS ≡ z
      qz = memS-fst Aʟ z z∈A
      z∈A' : ⟨ fst zS ∈ fst Aʟ ⟩
      z∈A' = subst (λ u → ⟨ u ∈ fst Aʟ ⟩) (sym qz) z∈A
```

同じ射影の等式に沿って、`yv` への所属と `xv` への非所属も運びます。あとは論理式の関係についての仮定を `R` へ読み戻せば、ホスト側の一致の仮定を使えます。

```agda
      z∈y' : ⟨ fst zS ∈ yv ⟩
      z∈y' = subst (λ u → ⟨ u ∈ yv ⟩) (sym qz) z∈y
      z∉x' : ⟨ fst zS ∈ xv ⟩ → Lift {j = ℓ-suc ℓ} Empty.⊥
      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 (fst w) w∈A hR
        where
        hp : ⟨ pr (fst w) (fst zS) ∈ fst (lookup r γ) ⟩
        hp = subst ⟨_⟩ (appAt-adequate (sh2 r) zero (suc zero) (w ∷ zS ∷ γ)) happ
        hR : ⟨ R (fst w) z ⟩
```

ここで `Rrep` は関係集合への所属を `R (fst w) zS` として読み戻します。第二の端点を `fst zS` から `z` へ運ぶと、もとの一致の証明が要求する仮定が得られ、`Both` の二つの所属の含意が従います。

```agda
        hR = subst (λ u → ⟨ R (fst w) u ⟩) qz (Rrep w zS hp)
```

## 順序を合成する

要素 `a : Limit` は、その底の集合が `Lset ω` に属するという証明を持ちます。この構成可能な段階への所属から必要な `isL` の証拠が得られ、同じ底の集合をモデル要素 `limitEl a` とみなせます。

```agda
opaque
  limitEl : Limit → S
  limitEl a = fst a , Lset→isL ω ω-ord (fst a) (snd a)
```

まとめる操作は集合を変えません。`limitEl a` を射影すると、定義により `fst a` が戻ります。この等式は後で、モデル内で作った順序対を表現定理に現れる周囲の順序対とそろえます。

```agda
  limitEl-fst : (a : Limit) → fst (limitEl a) ≡ fst a
  limitEl-fst a = refl
```

関係を `L` の内部に置くには、関係する二つの端点を、それ自身がモデル要素である順序対で表さなければなりません。`prS` は任意の二つの構成可能な端点に対して、その内部順序対を与えます。

```agda
  prS : S → S → S
  prS a b = prʟ a b
```

`prS` の射影則は、その底の集合を二つの端点の底の集合からなる周囲の順序対と同一視します。したがって、内部の対構成と外部の関係への所属は同じ集合について述べています。

```agda
  prS-fst : (a b : S) → fst (prS a b) ≡ pr (fst a) (fst b)
  prS-fst a b = prʟ-fst a b
```

分出によって比較を満たす順序対を選ぶ前に、候補となるすべての対を含む集合サイズの共通の上界が必要です。`Lset ω` の要素を小さなファイバーで表示し、各要素を構成可能なものとしてまとめ、その二つの小さなファイバーの積で順序対を添字づけます。

```agda
pairsBound : Σ[ D ∈ S ] ((u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst D ⟩)
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 (fst p)) (ixL (snd p)) ∈ˢ D ⟩)
  d = smallDom (⟪ Lset ω ⟫ × ⟪ Lset ω ⟫) (λ p → prʟ (ixL (fst p)) (ixL (snd p)))
```

任意の `u,v : Limit` に対し、それぞれの底の集合は `Lset ω` の小さなファイバー内に表示添字を持ちます。その添字から作った順序対は共通の上界に属し、射影の等式に沿って運ぶことで、周囲の順序対 `pr (fst u) (fst v)` の所属が得られます。

```agda
  onPair : (u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst (d .fst) ⟩
  onPair u v = subst (λ t → ⟨ t ∈ fst (d .fst) ⟩)
    (prʟ-fst (ixL (fu .fst)) (ixL (fv .fst)) ∙ cong₂ pr (fu .snd) (fv .snd))
    (d .snd (fu .fst , fv .fst))
    where
```

二つのファイバーの証人は、上で使う表示添字と、そこで示される要素をそれぞれ `fst u`、`fst v` と同一視する等式を取り出します。この等式があるため、小さな表示で実際のすべての極限段階の端点を扱えます。

```agda
    fu = ∈-asFiber {a = fst u} {b = Lset ω} (snd u)
    fv = ∈-asFiber {a = fst v} {b = Lset ω} (snd v)
```

論理式から読み取れるのが、極限上の狭義比較の命題的切り詰めだけである場合があります。`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) = Empty.rec (PT.rec Empty.isProp⊥
    (λ k → SWO.irr∙ limitOrder b (subst (λ t → t ≺ˡ b) q k)) h)
  decide (gt k) = Empty.rec (PT.rec Empty.isProp⊥
    (λ j → SWO.irr∙ limitOrder a (SWO.trans∙ limitOrder a b a j k)) h)
```

`level a` の定義的性質により、`fst a` は `finiteStage (level a)` に属します。等式 `level a ≡ k` に沿ってこの所属を `finiteStage k` へ運ぶと、有限段階の比較を使う際に必要な段階の境界がちょうど得られます。

```agda
levelStage : (a : Limit) (k : ℕ) → level a ≡ k → ⟨ fst a ∈ finiteStage k ⟩
levelStage a k q = subst (λ j → ⟨ fst a ∈ 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) (γ : S ^ n) (m : ℕ)
               → fst (lookup b γ) ≡ # m
               → ⟨ fst (lookup x γ) ∈ finiteStage m ⟩
```

内向きの仮定は、第二の端点も同じ有限段階に属することと、実際の比較 `before m x y` が成り立つことをさらに要求し、そこから `BeforeAt` の充足を与えます。したがって、この枠組みは有限段階の関係を構成せず、その順序法則も導きません。

```agda
               → ⟨ fst (lookup y γ) ∈ finiteStage m ⟩
               → ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩
               → ⟨ γ ⊨ BeforeAt b x y ⟩)
  (BeforeAt-out : ∀ {n} (b x y : Fin n) (γ : S ^ n) (m : ℕ)
                → fst (lookup b γ) ≡ # m
```

外向きの仮定も同じ数項と段階の境界を持ち、充足を `before m x y` として読み戻します。両方向を満たす論理式だけがこの枠組みを具体化できます。実際の `BeforeAt` と、そこから得られる `codeOrder` は `EarliestDisagreement` によって与えられ、この時点で無条件に得られるものではありません。

```agda
                → ⟨ fst (lookup x γ) ∈ finiteStage m ⟩
                → ⟨ fst (lookup y γ) ∈ finiteStage m ⟩
                → ⟨ γ ⊨ BeforeAt b x y ⟩
                → ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩)
  where
```

`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) (γ : S ^ n)
               (u v : Limit) (ku kv : ℕ)
               (qu : level u ≡ ku) (qv : level v ≡ kv)
               (qx : fst (lookup x γ) ≡ fst u)
               (qy : fst (lookup y γ) ≡ fst v)
```

二つの `Level` の具体例は、単に便利な名前を与えるだけではありません。それぞれが、対応する実際の端点とその最小レベルについて、`LevelAt` の検証済みの読みを与えます。外向きに読むとき、この橋によって見かけだけの数項証人が排除されます。

```agda
               where
    private
      module Lu = Level u ku qu
      module Lv = Level v kv qv
```

`Split c d` はレベルが異なる枝の意味内容です。`c` が左端点の最小レベルの数項、`d` が右端点の最小レベルの数項であり、さらに `c ∈ d` が成り立つことを述べます。最後の条件によって、左のレベルが右のレベルより小さいという向きが定まります。

```agda
      Split : S → S → Type (ℓ-suc ℓ)
      Split c d = ⟨ (d ∷ c ∷ γ) ⊨ LevelAt (suc zero) (sh2 x) ⟩
                × ( ⟨ (d ∷ c ∷ γ) ⊨ LevelAt zero (sh2 y) ⟩
                  × ⟨ fst c ∈ fst d ⟩ )
```

`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` が要求する所属 `fst (numS ku) ∈ fst (numS kv)` が得られます。

```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) (fst u) (fst v) ⟩ → 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 (fst u) (fst v) ⟩) 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 : fst c ≡ # ku
```

それぞれの数項の同一視は、正しく拡張された環境で得られます。第一の `LevelAt` は二つの新しい証人を越えて `x` を参照し、第二の `LevelAt` は `y` を参照します。この束縛子の整合により、最後の不等式が証人自身ではなく、もとの二つの端点の真のレベルを比較していることが保証されます。

```agda
        qc = Lu.LevelAt-out (suc zero) (sh2 x) (d ∷ c ∷ γ) hx qx
        qd : fst d ≡ # 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) (fst u) (fst v) ⟩
      same-out c (hx , (hy , hb)) = e , below
        where
        qc : fst c ≡ # ku
```

一つ目の証明は `c` の台となる集合を数項 `# ku` と同定し、二つ目はそれを `# kv` と同定します。数項符号化の単射性から `ku = kv` が従い、これを `ku` と `kv` を定める段階番号の等式と合成すると `level v = level u` が得られます。したがって、段階番号の一致は対象言語の論理式に等式として書かれるのではなく、共通の証人から復元されます。

```agda
        qc = Lu.LevelAt-out zero (suc x) (c ∷ γ) hx qx
        qc' : fst c ≡ # 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 : ⟨ fst (lookup x γ) ∈ finiteStage ku ⟩
        xIn = subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qx) (levelStage u ku qu)
        yIn : ⟨ fst (lookup y γ) ∈ finiteStage ku ⟩
        yIn = subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qy)
          (levelStage v ku (e ∙ qu))
```

ここで、`c` が表す数項のもとで抽象的な仮定 `BeforeAt-out` を適用できます。まず環境の二つの値に対する `before ku` が得られ、それらを `fst u` と `fst v` に、さらに `ku` を `level u` に置き換えると、極限段階の順序の同段階枝に必要な有限段階の比較になります。この議論では、仮定された段階の境界外で `BeforeAt` に意味があるとは仮定していません。

```agda
        below : ⟨ before (level u) (fst u) (fst v) ⟩
        below = subst (λ j → ⟨ before j (fst u) (fst v) ⟩) (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) (fst u) (fst v) ⟩
                 → ⟨ γ ⊨ 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) (fst u) (fst v) ⟩)
                  → ⟨ γ ⊨ 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 = PT.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) = PT.rec squash₁
          (λ { (c , hd) → PT.rec squash₁ (atSplit c) hd }) h
        decide (inr h) = PT.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 (fst u) (fst v)` に対応づけます。

```agda
  codeOrder-fill : (u v : Limit) → u ≺ˡ v
                 → ⟨ pr (fst u) (fst v) ∈ fst codeOrder ⟩
  codeOrder-fill u v h =
    subst (λ t → ⟨ t ∈ fst codeOrder ⟩) 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 : fst (prS (limitEl u) (limitEl v)) ≡ pr (fst u) (fst v)
    qz = prS-fst (limitEl u) (limitEl v)
```

対応づけの等式は二つの明確な段階から得られます。モデル内の対の射影は二つの射影からなる外部の順序対であり、各 `limitEl` は元の極限段階の要素の台となる集合へ射影されます。これらを合成することで、表現を変えても端点もその順番も変わらないことが保証されます。

```agda
       ∙ cong₂ pr (limitEl-fst u) (limitEl-fst v)
```

第一の分出の課題には `pairsBound` の定義的な性質を使います。極限段階の任意の二要素から作る順序対は、この上界に含まれます。包含の証明を使う前に、モデル内で符号化された対を対応する外部の順序対にそろえます。正確な比較条件は `Cond₀` が与えるため、上界の逆向きの特徴づけは不要です。

```agda
    inBound : ⟨ fst (prS (limitEl u) (limitEl v)) ∈ fst (pairsBound .fst) ⟩
    inBound = subst (λ t → ⟨ t ∈ fst (pairsBound .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 (fst u) (fst v)` が `codeOrder` に属することから始まります。分出条件からは、対と比較の条件を満たす二成分が命題的切り詰めの中で得られ、それらを読んでも最初は `∥ u ≺ˡ v ∥₁` だけが得られます。最後に、すでに証明された狭義整列順序 `limitOrder` の三分律で等しい場合と逆向きの比較を排除し、`strictLimit` によって切り詰められていない結論を得ます。

```agda
  codeOrder-rep : (u v : Limit)
                → ⟨ pr (fst u) (fst v) ∈ fst codeOrder ⟩ → u ≺ˡ v
  codeOrder-rep u v h = strictLimit u v
    (PT.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 : fst (prS (limitEl u) (limitEl v)) ≡ pr (fst u) (fst v)
    qz = prS-fst (limitEl u) (limitEl v)
       ∙ cong₂ pr (limitEl-fst u) (limitEl-fst v)
```

与えられた所属は外部の順序対についてのものですが、分出の仕様は `prS` が作るモデル要素に適用されます。対を対応づける等式により両者の台となる集合は等しいので、所属をモデル内の表現へ移せます。この表現の変更を行って初めて、そのモデル要素が作る環境で対象言語の条件を読み取れます。

```agda
    inSet : ⟨ fst (prS (limitEl u) (limitEl v)) ∈ fst codeOrder ⟩
    inSet = subst (λ t → ⟨ t ∈ fst codeOrder ⟩) (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 (fst c) (fst d)` の等式へ変わります。先の対応づけは、同じ候補を `pr (fst u) (fst v)` と同定しています。二つの等式を合成すると二つの順序対が等しいことが得られ、`LimitOrdAt` を読むために必要な端点の等式を導けます。

```agda
      qcd : pr (fst u) (fst v) ≡ pr (fst c) (fst d)
      qcd = sym qz
        ∙ subst ⟨_⟩ (prAtL-adequate (sh2 zero) (suc zero) zero
            (d ∷ c ∷ prS (limitEl u) (limitEl v) ∷ [])) hpr
      split : (fst u ≡ fst c) × (fst v ≡ fst d)
```

順序対符号化の単射性により、対の等式は `fst u = fst c` と `fst v = fst d` に分かれます。成分の位置と順番は保たれるため、左端と右端が入れ替わることはありません。これらの等式を逆向きにすると、`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) = PT.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
    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) ∈ fst Ps ⟩ → a ≺ₚ b)
      (Pfill : (a b : ⟪ A ⟫) → a ≺ₚ b → ⟨ pr (Ad.ix a) (Ad.ix b) ∈ fst Ps ⟩)
      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 (fst u) (fst v)` がその集合に属することの両方向を与えます。読み取り方向では、`strictLimit` と既存の狭義整列順序を用いて、命題的切り詰めから比較を復元します。`EarliestDisagreement` が有限段階についての仮定を満たしますが、この章は `codeOrder` が整列順序をなすことを対象言語で主張せず、選択公理も証明しません。