---
title: "最初の相違の関係からなる内部の族"
module: L.Choice.EarliestDisagreement
lang: ja
site: "Bedrock"
description: "最初の相違の関係からなる内部の族"
stage: "正準整列順序と選択公理"
reading_order: 82
canonical: https://bedrock.institute/ja/L.Choice.EarliestDisagreement.html
html: L.Choice.EarliestDisagreement.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/EarliestDisagreement.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Stage, L.Axioms.Basic, L.Axioms.Full, L.Recursion, L.Axioms.Infinity, L.Choice.FiniteStageOrders, L.Choice.LimitStageOrder, L.Coding.HierarchySequence, L.Hierarchy, L.Coding.Model, L.Coding.Expressions, FOL.Absoluteness, FOL.ZFModel]
routes: [choice-completion]
translations: [https://bedrock.institute/en/L.Choice.EarliestDisagreement.md, https://bedrock.institute/zh/L.Choice.EarliestDisagreement.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 最初の相違の関係からなる内部の族

各有限段階で、`before n` は二つの集合を最初に相違する要素によって比較する。本章では、この関係を `L` 内の集合 `relAt n` で表し、それらを数項で添字づけられた族にまとめ、その族での参照を対象言語の論理式 `BeforeAt` で表す。この論理式によって `Described` を具体化すると `codeOrder` が得られ、後の名前比較でコードの比較関係として使われる。本章自身は名前を比較せず、その比較の整礎性も証明しない。

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

この構成で排中律を使うのは、直後にモジュールへ与える明示的な仮定を通してだけである。したがって、この章から公開される各結果には古典的仮定が明示されたままになる。

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

宇宙レベル `ℓ` を固定し、`LEM (ℓ-suc ℓ)` を仮定する。以下の集合、論理式、命題値関係はすべて、この選択で定まるレベルに属する。

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

累積階層上の一階論理式によって関係を記述する。関係の要素には順序対を用い、後にはその単射性によって、符号化された要素から比較される二集合を復元する。

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

第 `n` 有限段階は `Lset (# n)` であり、`# n` は階層内のフォン・ノイマン数項である。その順序数性と構成可能性により、この段階とその各要素を `L` のモデルの対象として扱える。

```agda
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd; Lset-mono )
open import L.Ordinal {ℓ} using
  ( numeral-ord; #∈ω; ∈#-elim; #∈#-elim; mem-ord; boundingOrd )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
```

二つの集合構成は異なる役割を担う。分出は一つの段階の関係を上界から切り出し、置換は後で内部の `ω` に沿ってそれらの関係を集める。有限近似そのものは `finSet` と `finSetL` によって構成する。

```agda
open import L.Axioms.Basic {ℓ}
  using ( extensionalL; LsetS; ∅ʟ; finSet; finSet-in; finSet-out; module FinOf )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL; hasReplacementL )
open import L.Recursion {ℓ} lem using ( smallDom; mereFunct )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
```

数学的な再帰はすでに定まっている。`before zero` は空であり、`before (suc n)` は `before n` で先行する点を順序づけ、`finiteStage n` 上の最初の相違によって次の有限段階の要素を比較する。`PrecedesAt` はこの後続段階を対象言語で表し、`RecShape` はその有限近似を組織する。

```agda
open import L.Choice.FiniteStageOrders {ℓ} lem
  using ( before; precedes; Agrees; Witness; finiteStage )
open import L.Choice.LimitStageOrder {ℓ} lem
  using ( PrecedesAt; module Precedes; module Described )
open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt; module RecShape )
```

対象言語の適用と外延性によって、ある集合が関係値を並べた表の値であることを論理式で述べられる。まず一回の再帰段階を記述するために使い、後には完成した族を数項の位置で読み取るために使う。

```agda
open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; appAt; appAt-adequate; appC; appC-adequate; domAt-intro )
open import L.Coding.Expressions {ℓ} using ( numL; extAt; extAt-out; extAt-in; extAt-in-both )
```

証明では集合と順序対の等式に沿う移送を繰り返し用いる。また、自然数の狭義順序に関する帰納によって、近似に記録された各値が一意に定まることを示す。

```agda
import FOL.Absoluteness
import FOL.ZFModel
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Nat.Order using
```

この帰納で使うのは自然数の `<` の整礎性である。すべての小さい添字で値を同定してから、`k` における値を決定する。これは `before` 自身の整礎性とは別の事柄である。

```agda
  ( _<_; <-trans; <-asym; pred-≤-pred; <-wellfounded; _≟_ )
import Cubical.Data.Nat.Order as NatOrder
open import Cubical.Induction.WellFounded using ( module WFI )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Data.FinData.Properties using ( toℕ<n; enum; toℕ∘enum )
```

以下では、いくつかの証人は命題的切り詰めの下でだけ得られる。この証人は存在を保証するが、標準的なデータを選び出さない。所属、`before`、または `V` における集合の等式のように、目標が命題である場合に消去できる。

```agda
open import Cubical.Data.FinData.Base using ( toℕ )
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 )
```

集合には、その要素の表示を通してアクセスする。この表示により、有限段階の全要素を走って順序対を構成でき、内部の `ω` は最終的な族全体の定義域を与える。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet using ( #_; ω )
```

以下では、論理式を構成可能集合がもつ命題値構造で解釈する。

```agda
open hPropStructure 𝒮ʟ
```

台 `S` は、集合と、それが `L` に属するという証明からなる。したがって内部関係を構成するには、基礎となる集合とその構成可能性の証明の両方が必要である。

```agda
module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )
```

絶対性は、この構造での充足を基礎となる集合についての対応する主張に結びつける。記法 `γ ⊨ φ` は、付値 `γ` が対象言語の論理式 `φ` を満たすことを表す。

```agda
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
```

二つの新しい変数を束縛すると、既存の各 de Bruijn 位置は二つ後ろへ移る。写像 `sh2` はこの移動を記録し、新しい束縛子の下でも各自由変数が同じ対象を指すようにする。

```agda
private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)
```

二つ分の移動を二度適用して `sh4` を得る。これは四つの束縛子の下で必要な調整である。

```agda
  sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n))))
  sh4 i = sh2 (sh2 i)
```

同様に、`sh6` は六つの束縛子の下で元の参照を保つ。これらの移動が変えるのは de Bruijn 位置だけであり、論理式の数学的内容ではない。

```agda
  sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n))))))
  sh6 i = sh2 (sh4 i)
```

対象 `stageS n` は有限段階 `Lset (# n)` を構成可能な台の要素としてまとめる。この包みを不透明にしておけば、後の議論は構成可能性証明の具体的な形に依存しない。

```agda
opaque
  stageS : ℕ → S
  stageS n = LsetS (# n) (numeral-ord n)
```

等式 `stageS-fst` は、この包みが担う数学的集合だけを明らかにする。その第一成分は `finiteStage n` である。

```agda
  stageS-fst : (n : ℕ) → fst (stageS n) ≡ finiteStage n
  stageS-fst n = refl
```

対象 `numS k` も同様に、フォン・ノイマン数項 `# k` とその構成可能性の証明をまとめる。

```agda
  numS : ℕ → S
  numS k = # k , numL k
```

等式 `numS-fst` により、後の論理式は隣に保存された証明を展開せずに、基礎となる数項を読み取れる。

```agda
  numS-fst : (k : ℕ) → fst (numS k) ≡ # k
  numS-fst k = refl
```

`z` が構成可能集合 `A` に属するなら、`L` の推移性によって `z` も構成可能である。包み `memS A z h` はこの帰結を記録し、`z` をモデルの要素として使えるようにする。

```agda
  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 A z h` の第一成分は元の集合 `z` のままであり、追加された成分は `L` への所属証明だけを与える。

```agda
  memS-fst : (A : S) (z : V ℓ) (h : ⟨ z ∈ fst A ⟩) → fst (memS A z h) ≡ z
  memS-fst A z h = refl
```

モデル要素 `a` と `b` に対し、`prS a b` はそれらの順序対を `L` の内部で作る。以下の関係集合は、まさにこの形の対象を要素にもつ。

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

構成可能性の証明を忘れると、通常の順序対 `pr (fst a) (fst b)` が得られる。この等式が、内部の所属命題を基礎となる集合上の関係 `before` に結びつける。

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

特に、`finiteStage n` の各要素 `x` は台 `S` に持ち上げられる。その段階自身が、この持ち上げに必要な構成可能性の証明を与える。

```agda
stageEl : (n : ℕ) (x : V ℓ) → ⟨ x ∈ finiteStage n ⟩ → S
stageEl n x h = x , Lset→isL (# n) (numeral-ord n) x h
```

## 各段階の関係を `L` の要素にする

分出によって関係を表すには、まず可能な要素をすべて含む一つの集合が必要である。そこで `pairsAt n` は構成可能な上界 `D` を与え、`u` と `v` がともに `finiteStage n` に属するとき `pr u v` を含むようにする。

```agda
pairsAt : (n : ℕ)
        → Σ[ D ∈ S ] ((u v : V ℓ) → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
                     → ⟨ pr u v ∈ fst D ⟩)
pairsAt n = d .fst , onPair
  where
```

有限段階の表示された要素には、その所属証明がすでに付いている。写像 `ixL` は、そこから得られる構成可能性証明を添え、各要素を `S` の要素にする。

```agda
  ixL : ⟪ finiteStage n ⟫ → S
  ixL m = ⟪ finiteStage n ⟫↪ m
        , Lset→isL (# n) (numeral-ord n) (⟪ finiteStage n ⟫↪ m)
            (∈∈ₛ {a = ⟪ finiteStage n ⟫↪ m} {b = finiteStage n} .snd
              (∈ₛ⟪ finiteStage n ⟫↪ m))
```

二つの表示の積は、段階の要素からなるすべての対を添字づける。それらの内部順序対に `smallDom` を適用すると、この添字族全体が一つの構成可能集合 `D` に収まる。

```agda
  d : Σ[ D ∈ S ] ((p : ⟪ finiteStage n ⟫ × ⟪ finiteStage n ⟫)
                  → ⟨ prʟ (ixL (fst p)) (ixL (snd p)) ∈ˢ D ⟩)
  d = smallDom (⟪ finiteStage n ⟫ × ⟪ finiteStage n ⟫)
        (λ p → prʟ (ixL (fst p)) (ixL (snd p)))
```

任意の `u,v ∈ finiteStage n` に対し、その所属証明から表示の添字 `fu` と `fv` が得られる。上界はその添字位置の順序対を含み、復元した成分の等式に沿って移送すれば、`pr u v` 自身の所属が得られる。

```agda
  onPair : (u v : V ℓ) → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
         → ⟨ pr u v ∈ fst (d .fst) ⟩
  onPair u v hu hv = 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))
```

二つのファイバー `fu` と `fv` は、表示の添字と、そこで表された要素をそれぞれ `u`、`v` と同定する等式を正確に記録する。

```agda
    where
    fu = ∈-asFiber {a = u} {b = finiteStage n} hu
    fv = ∈-asFiber {a = v} {b = finiteStage n} hv
```

同じ台 `A` 上で、各 `R' w z` から `R w z` が従うとする。このとき `R` に関する最初の相違の証人から `R'` に関する証人も得られる。向きが反転するのは、先行点での関係が一致条件の仮定として現れるためである。

```agda
precedes-map : (R R' : V ℓ → V ℓ → hProp (ℓ-suc ℓ)) (A x y : V ℓ)
             → ((w z : V ℓ) → ⟨ w ∈ A ⟩ → ⟨ z ∈ A ⟩ → ⟨ R' w z ⟩ → ⟨ R w z ⟩)
             → ⟨ precedes R A x y ⟩ → ⟨ precedes R' A x y ⟩
precedes-map R R' A x y f = PT.map step
  where
```

相違点 `z`、その `A` と `y` への所属、および `x` に属さないことは変わらない。変換が必要なのは、`z` より前で `x` と `y` が一致するという証明だけである。

```agda
  step : Σ[ z ∈ V ℓ ] Witness R A x y z → Σ[ z ∈ V ℓ ] Witness R' A x y z
  step (z , (z∈A , (z∈y , (z∉x , ag)))) =
    z , (z∈A , (z∈y , (z∉x , ag')))
    where
    ag' : Agrees R' A x y z
```

先行点 `w` では、仮定 `R' w z` をまず `R w z` に写し、それを元の一致証明に渡す。これにより `R'` に関する必要な一致が得られる。

```agda
    ag' w w∈A hR' = ag w w∈A (f w z w∈A z∈A hR')
```

分出条件は、候補となる関係要素だけを自由変数として受け取る。前の関係と前の段階を存在量化し、等式によって与えられた定数に固定し、二つの端点を現在の段階の中で動かす。

```agda
RelCond : (R A A' : S) → Formula S 1
RelCond R A A' =
  ∃̇ ( (var zero ≐ con R)
    ∧̇ ∃̇ ( (var zero ≐ con A)
         ∧̇ ∃̇∈ (con A') ( ∃̇∈ (con A')
```

残る連言は、候補を二端点の順序対と同定し、与えられた直前の段階と関係に関して `PrecedesAt` が成り立つことを述べる。これは後で再帰ステップに使う後続段階の比較である。ただし、ここでの `RelCond` は直前の段階と関係を定数で固定するのに対し、再帰の論理式は関係を近似から取得し、対応する段階を階層グラフによって同定する。

```agda
              ( prAtL (sh2 (sh2 zero)) (suc zero) zero
              ∧̇ PrecedesAt (sh2 (suc zero)) (sh2 zero) (suc zero) zero ) ) ) )
```

ここで表現集合を再帰的に定義する。ゼロでは関係は空であり、後続では大きい方の有限段階の全要素対を含む上界から分出を始める。

```agda
opaque
  relAt : ℕ → S
  relAt zero    = ∅ʟ
  relAt (suc n) =
    hasSeparationL (pairsAt (suc n) .fst)
```

この上界から、`RelCond (relAt n) (stageS n) (stageS (suc n))` は、前の関係に基づく後続節によって比較される端点の対だけを選び出す。

```agda
      (RelCond (relAt n) (stageS n) (stageS (suc n))) .fst .fst
```

等式 `relAt-zero` は基底の場合を明示する。これにより、ゼロ段階の関係に属するとされる要素を、後で空集合への所属へ帰着できる。

```agda
  relAt-zero : relAt zero ≡ ∅ʟ
  relAt-zero = refl
```

後続段階で `relAt (suc n)` に属することは二つの部分からなる。候補が順序対の上界に属し、さらに `relAt n`、前の段階、現在の段階で定まる分出論理式を満たすことである。

```agda
  relAt-mem : (n : ℕ) (z : S)
            → (z ∈ˢ relAt (suc n))
            ≡ ( (z ∈ˢ pairsAt (suc n) .fst)
              ⊓ ((z ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n))) )
  relAt-mem n =
```

この同値は分出が与える正確な仕様である。後の証明では、所属から論理式を取り出す向きと、上界の証明と論理式の証明から所属を組み立てる向きの両方で用いる。

```agda
    hasSeparationL (pairsAt (suc n) .fst)
      (RelCond (relAt n) (stageS n) (stageS (suc n))) .fst .snd
```

述語 `Rel n a b` は、順序対 `pr a b` が表現集合 `relAt n` に属することの略記である。続く表現補題は、段階の要素について、この述語が `before n a b` と同値であることを示す。

```agda
Rel : ℕ → V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Rel n a b = pr a b ∈ fst (relAt n)
```

これらの補題の証明では、五つの要素からなる環境で `PrecedesAt` を解釈する。外側の束縛による移動の後で、`s1` と `s2` が端点と段階の位置を指定する。

```agda
private
  s1 : Fin 5
  s1 = suc zero
  s2 : Fin 5
  s2 = sh2 zero
```

残る位置 `s3` と `s4` は、それぞれ前の関係と符号化された順序対を指す。これらに一度名前を付けることで、意味論的な議論を `RelCond` の四つの役割に対応させたままにできる。

```agda
  s3 : Fin 5
  s3 = sh2 (suc zero)
  s4 : Fin 5
  s4 = sh2 (sh2 zero)
```

関係集合の任意の要素を同定するには、その二つの成分を復元する必要があります。そこで `RelOf k zv` は、`finiteStage k` に属する `x,y`、`zv` をその順序対と同定する等式、そして `before k x y` の証明を要求します。この証人型は選ばれた成分を含むので、それ自体は命題とは限りません。

```agda
RelOf : (k : ℕ) → V ℓ → Type (ℓ-suc ℓ)
RelOf k zv = Σ[ x ∈ S ] Σ[ y ∈ S ]
  ( ⟨ fst x ∈ finiteStage k ⟩
  × ( ⟨ fst y ∈ finiteStage k ⟩
    × ( (zv ≡ pr (fst x) (fst y)) × ⟨ before k (fst x) (fst y) ⟩ ) ) )
```

`relAt k` への所属からこのような成分が得られるのは命題的切り詰めの下だけです。関係は適切な表示の存在を記録しますが、その一つを標準的に選びません。逆向きには、明示された成分とその比較から順序対を関係へ書き込めます。

```agda
relAt-out : (k : ℕ) (zv : V ℓ) → ⟨ zv ∈ fst (relAt k) ⟩ → ∥ RelOf k zv ∥₁
relAt-in  : (k : ℕ) (zv : V ℓ) → RelOf k zv → ⟨ zv ∈ fst (relAt k) ⟩
```

基底の場合は `before zero` を反映します。`relAt zero` は空なので、要素があると仮定すれば矛盾が得られます。後続の場合、所属からまず分出条件が得られ、その存在証人は命題的切り詰めを通してのみ利用できます。

```agda
relAt-out zero zv h = Empty.rec
  (∅-empty zv (∈∈ₛ {a = zv} {b = ∅} .fst
    (subst (λ t → ⟨ zv ∈ fst t ⟩) relAt-zero h)))
relAt-out (suc n) zv h = PT.rec squash₁
  (λ { (r , (qr , ha)) → PT.rec squash₁
```

切り詰められた証人を順に開くと、候補となる直前の関係、その有限段階、そして順序対の二成分が現れます。最後の再構成へこれらを渡す間も結果を切り詰めたままにするため、特定の表示が選択済みデータとして外へ出ることはありません。

```agda
    (λ { (a , (qa , hx)) → PT.rec squash₁
      (λ { (x , (x∈ , hy)) → PT.map (atY r a x qr qa x∈) hy }) hx }) ha }) cond
  where
  zS : S
  zS = memS (relAt (suc n)) zv h
```

`zv ∈ relAt (suc n)` と `L` の推移性により、基礎集合 `zv` を `L` の要素として包めます。これによって、いま調べている要素そのものにおいて対象言語の分出条件を解釈できます。

```agda
  qz : fst zS ≡ zv
  qz = memS-fst (relAt (suc n)) zv h
```

分出の定義的性質により、仮定した所属は `RelCond` の充足へ変わります。したがって以後は、有界な順序対集合への所属だけでなく、その条件の数学的内容を用いて議論できます。

```agda
  cond : ⟨ (zS ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n)) ⟩
  cond = subst ⟨_⟩ (relAt-mem n zS)
    (subst (λ t → ⟨ t ∈ fst (relAt (suc n)) ⟩) (sym qz) h) .snd
```

候補の成分 `x,y` について、残る本体は二つのことを述べます。調べている要素がその順序対であることと、直前の段階上の最初の相違によって `x` が `y` に先行することです。後者はまだ `r` が表す関係を使います。その関係を `relAt n` と同定することは、外側の証人が担います。

```agda
  Body : (r a x y : S) → Type (ℓ-suc ℓ)
  Body r a x y =
      ⟨ (y ∷ x ∷ a ∷ r ∷ zS ∷ []) ⊨ prAtL s4 s1 zero ⟩
    × ⟨ (y ∷ x ∷ a ∷ r ∷ zS ∷ []) ⊨ PrecedesAt s3 s2 s1 zero ⟩
```

後続段階から `x` を選んだ後、`AtY` は同じ段階からの `y` の選択と、順序対および比較の事実を記録します。二つの選択を分けることで、`RelCond` の入れ子になった存在構造に対応します。

```agda
  AtY : (r a x : S) → Type (ℓ-suc ℓ)
  AtY r a x = Σ[ y ∈ S ] (⟨ fst y ∈ fst (stageS (suc n)) ⟩ × Body r a x y)
```

すべての証人がそろうと、段階の等式によって二成分はいずれも `finiteStage (suc n)` に属します。残るのは、調べている要素をその順序対と同定し、表された関係による比較を `before (suc n)` へ移すことです。続く補題がこの二つの変換を行います。

```agda
  atY : (r a x : S) → fst r ≡ fst (relAt n) → fst a ≡ fst (stageS n)
      → ⟨ fst x ∈ fst (stageS (suc n)) ⟩ → AtY r a x → RelOf (suc n) zv
  atY r a x qr qa x∈ (y , (y∈ , (hpr , hprec))) =
    x , (y , ( subst (λ t → ⟨ fst x ∈ t ⟩) (stageS-fst (suc n)) x∈
             , ( subst (λ t → ⟨ fst y ∈ t ⟩) (stageS-fst (suc n)) y∈
```

与えられた関係を `relAt n` と同定する等式により、そこに記録された任意の先行する対を `Rel n` として読めます。これは、一般的な `PrecedesAt` の主張をここで構成した具体的な関係で解釈するために必要な一方向です。

```agda
               , (sym qz ∙ qpair , below) ) ) )
    where
    Rrep : (s t : S) → ⟨ pr (fst s) (fst t) ∈ fst (lookup s3 (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) ⟩
         → ⟨ Rel n (fst s) (fst t) ⟩
    Rrep s t p = subst (λ w → ⟨ pr (fst s) (fst t) ∈ w ⟩) qr p
```

逆向きの輸送は `Rel n` の証明を与えられた関係へ書き戻します。両方向がそろうことで、`PrecedesAt` の妥当性定理は二つの表示を同じ基底関係として扱えます。

```agda
    Rfill : (s t : S) → ⟨ Rel n (fst s) (fst t) ⟩
          → ⟨ pr (fst s) (fst t) ∈ fst (lookup s3 (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) ⟩
    Rfill s t p = subst (λ w → ⟨ pr (fst s) (fst t) ∈ w ⟩) (sym qr) p
```

これら二つの表示写像を固定すると、`Precedes` モジュールが対象言語の論理式とホスト側の述語 `precedes` を結ぶ意味論的な橋を与えます。この橋が扱うのは一回の比較だけであり、ここで順序の性質を証明するものではありません。

```agda
    module P = Precedes s3 s2 s1 zero (y ∷ x ∷ a ∷ r ∷ zS ∷ [])
                        (Rel n) Rrep Rfill
```

`PrecedesAt` を読み出すと、論理式から与えられた段階上の `precedes` 比較が得られます。段階の等式はその台を `finiteStage n` と同定します。これは `before (suc n)` の再帰的定義が用いる台です。

```agda
    onStage : ⟨ precedes (Rel n) (finiteStage n) (fst x) (fst y) ⟩
    onStage = subst (λ w → ⟨ precedes (Rel n) w (fst x) (fst y) ⟩)
      (qa ∙ stageS-fst n) (P.PrecedesAt-out hprec)
```

一致の節の内部では、基底関係を使うたびに `before n` から `relAt n` への所属へ変換する必要があります。帰納的に得た書き込み補題がこの変換を行い、`precedes-map` からちょうど後続の関係 `before (suc n)` が得られます。

```agda
    below : ⟨ before (suc n) (fst x) (fst y) ⟩
    below = precedes-map (Rel n) (before n) (finiteStage n) (fst x) (fst y)
      (λ w t hw ht hb → relAt-in n (pr w t)
        (stageEl n w hw , (stageEl n t ht , (hw , (ht , (refl , hb))))))
      onStage
```

順序対の論理式の妥当性により、包まれた要素は `pr (fst x) (fst y)` と同定されます。この等式を包装の等式と合成すると、元の `zv` に必要な等式が得られます。

```agda
    qpair : fst zS ≡ pr (fst x) (fst y)
    qpair = subst ⟨_⟩ (prAtL-adequate s4 s1 zero (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) hpr
```

`k = 0` のとき、`RelOf` の証人はすでに不可能な `before zero` の証明を含むため、書き込み方向は矛盾から従います。後続の場合、目的の順序対を有界な順序対集合へ入れ、それが分出条件を満たすことを示します。

```agda
relAt-in zero zv (x , (y , (x∈ , (y∈ , (qq , hb))))) = Empty.rec* hb
relAt-in (suc n) zv (x , (y , (x∈ , (y∈ , (qq , hb))))) =
  subst (λ t → ⟨ t ∈ fst (relAt (suc n)) ⟩) (prS-fst x y ∙ sym qq)
    (subst ⟨_⟩ (sym (relAt-mem n (prS x y))) (inBound , cond))
  where
```

二つの段階所属の仮定から、その順序対は `pairsAt (suc n)` に入ります。これは分出に必要な境界であり、有限段階の要素からなる対だけが `relAt (suc n)` に入り得ます。

```agda
  inBound : ⟨ prS x y ∈ˢ pairsAt (suc n) .fst ⟩
  inBound = subst (λ t → ⟨ t ∈ fst (pairsAt (suc n) .fst) ⟩) (sym (prS-fst x y))
    (pairsAt (suc n) .snd (fst x) (fst y) x∈ y∈)
```

逆向きの構成では、環境に実際の直前の関係 `relAt n` が入っているため、それを `Rel n` と解釈する写像は恒等写像で足ります。したがって同じ意味論的な橋を使い、ホスト側の比較から `PrecedesAt` を構成できます。

```agda
  module P = Precedes s3 s2 s1 zero
                      (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ [])
                      (Rel n) (λ _ _ p → p) (λ _ _ p → p)
```

仮定 `before (suc n) x y` は、`before n` を基底とする最初の相違へ展開されます。同じ一致条件を内部の関係で表すため、記録された各先行対を `relAt-out` で読み出します。目標の `before n w t` は命題なので、命題的切り詰めを除去できます。

```agda
  held : ⟨ precedes (Rel n) (finiteStage n) (fst x) (fst y) ⟩
  held = precedes-map (before n) (Rel n) (finiteStage n) (fst x) (fst y)
    (λ w t hw ht hR → PT.rec (snd (before n w t)) (readBack w t)
      (relAt-out n (pr w t) hR))
    hb
```

復元された `RelOf` の証人は `w,t` とは別の成分を名指すかもしれませんが、その順序対の等式は `pr w t` と等しいことを述べます。順序対の単射性が二成分をそれぞれ同定し、記録された `before n` の証明を必要な端点へ移せます。

```agda
    where
    readBack : (w t : V ℓ) → RelOf n (pr w t) → ⟨ before n w t ⟩
    readBack w t (p , (q , (p∈ , (q∈ , (qq' , hbf))))) =
      subst2 (λ s u → ⟨ before n s u ⟩)
        (sym (pr-inj qq' .fst)) (sym (pr-inj qq' .snd)) hbf
```

変換されたホスト側の比較は `PrecedesAt-in` の仮定を満たします。これにより、直前の段階と関係を所定の変数に置いた分出論理式の比較節が得られます。

```agda
  hprec : ⟨ (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ [])
          ⊨ PrecedesAt s3 s2 s1 zero ⟩
  hprec = P.PrecedesAt-in
    (subst (λ w → ⟨ precedes (Rel n) w (fst x) (fst y) ⟩) (sym (stageS-fst n))
      held)
```

候補の要素は `prS x y` として構成されているため、順序対を認識する論理式を満たします。その妥当性の等式が、内部の構成を論理式の要求する基礎の順序対へ結び付けます。

```agda
  hpr : ⟨ (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ []) ⊨ prAtL s4 s1 zero ⟩
  hpr = subst ⟨_⟩
    (sym (prAtL-adequate s4 s1 zero
      (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ []))) (prS-fst x y)
```

`stageS (suc n)` の表示等式により、`finiteStage (suc n)` の既知の各要素を論理式が用いる段階対象へ輸送できます。追加の閉包性は必要ありません。

```agda
  onStage : (w : V ℓ) → ⟨ w ∈ finiteStage (suc n) ⟩
          → ⟨ w ∈ fst (stageS (suc n)) ⟩
  onStage w hw = subst (λ t → ⟨ w ∈ t ⟩) (sym (stageS-fst (suc n))) hw
```

ここまでに構成した証人は分出条件全体を満たします。直前の関係と段階を同定し、`x,y` を後続段階に置き、順序対と最初の相違の両方を確立します。入れ子の存在量化は命題的切り詰めの下で導入され、存在を主張するだけで標準的な証人を選びません。

```agda
  cond : ⟨ (prS x y ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n)) ⟩
  cond = ∣ relAt n , (refl
       , ∣ stageS n , (refl
       , ∣ x , (onStage (fst x) x∈
       , ∣ y , (onStage (fst y) y∈ , (hpr , hprec)) ∣₁) ∣₁) ∣₁) ∣₁
```

実用的な読み出しのインターフェースは、両端点が `finiteStage n` に属すると分かっている順序対 `pr u v` から始まります。切り詰められた表示を除去する先は命題 `before n u v` だけなので、標準的な表示がなくても問題はありません。

```agda
relAt-rep : (n : ℕ) (u v : V ℓ)
          → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
          → ⟨ pr u v ∈ fst (relAt n) ⟩ → ⟨ before n u v ⟩
relAt-rep n u v hu hv h = PT.rec (snd (before n u v)) read (relAt-out n (pr u v) h)
  where
```

復元した表示が成分 `p,q` を用いていても、その順序対が `pr u v` と等しいことから `p=u` と `q=v` が従います。この二つの等式に沿って輸送すれば、記録された比較が目的の比較になります。

```agda
  read : RelOf n (pr u v) → ⟨ before n u v ⟩
  read (p , (q , (p∈ , (q∈ , (qq , hbf))))) =
    subst2 (λ s t → ⟨ before n s t ⟩)
      (sym (pr-inj qq .fst)) (sym (pr-inj qq .snd)) hbf
```

逆に、`u,v` の段階所属と `before n u v` の証明から、`pr u v` に対する明示的な `RelOf` の証人が得られます。書き込み補題がその対を `relAt n` に記録し、対ごとの表示の逆方向が完成します。

```agda
relAt-fill : (n : ℕ) (u v : V ℓ)
           → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
           → ⟨ before n u v ⟩ → ⟨ pr u v ∈ fst (relAt n) ⟩
relAt-fill n u v hu hv h = relAt-in n (pr u v)
  (stageEl n u hu , (stageEl n v hv , (hu , (hv , (refl , h)))))
```

## 参照対象すべてに一般的なステップ

再帰的な記述は関係をデータとして受け取る必要があり、`relAt` を直接参照できません。`Held r a b` が必要な解釈を与えます。すなわち、`r` が `a,b` の順序対を含むとき、かつそのときに限り、`r` は `a` を `b` に関係付けます。

```agda
Held : S → V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Held r a b = pr a b ∈ fst r
```

一回の再帰ステップでは、まず現在の添字の `∈` に関する最大要素 `c` を探します。その添字が後続数項 `# (suc n)` なら、この要素は直前の数項 `# n` です。零ではそのような要素が存在しないため、別の基底論理式を置かなくても、ステップが定める関係には要素がありません。

```agda
opaque
 RelBodyAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
 RelBodyAt z b f =
   ∃̇ ( (var zero ∈̇ var (suc b))
     ∧̇ ( ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero))
```

`c` が得られると、論理式は近似から `c` に記録された関係を読み取ります。階層のグラフは `Lset (fst c)` と現在の添字における `Lset` を同定し、二つの候補となる端点は後者の中を動きます。現在の添字が数項と同定されたときに限って、これらは有限段階になります。

```agda
       ∧̇ ∃̇ ( appAt (sh2 f) (suc zero) zero
            ∧̇ ∃̇ ( LsetGraphAt zero (suc (suc zero))
                 ∧̇ ∃̇ ( LsetGraphAt zero (sh4 b)
                      ∧̇ ∃̇∈ (var zero)
                           ( ∃̇∈ (var (suc zero))
```

最も内側の節は、候補の項目が二端点の順序対であることを要求し、近似から読み出した関係を使って、直前の段階上で `PrecedesAt` により両者を比較します。こうして、特定の `relAt n` を名指すことなく再帰の後続ステップを記述します。

```agda
                               ( prAtL (sh6 z) (suc zero) zero
                               ∧̇ PrecedesAt (suc (suc (suc (suc zero))))
                                             (suc (suc (suc zero)))
                                             (suc zero) zero ) ) ) ) ) ) )
```

`StepOf` はこの論理式のメタレベルでの意味です。現在の添字の最大要素となる候補 `c`、そこで記録された関係値 `r`、端点 `x,y` という四つのモデル要素を選びます。候補となる項目 `zv` は、すでに述語の引数です。現在の添字が数項と同定されて初めて、`c` はその直前の数項と同定されます。

```agda
StepOf : ∀ {n} → Fin n → Fin n → S ^ n → V ℓ → Type (ℓ-suc ℓ)
StepOf b f γ zv =
  Σ[ c ∈ S ] Σ[ r ∈ S ] Σ[ x ∈ S ] Σ[ y ∈ S ]
    ( ⟨ fst c ∈ fst (lookup b γ) ⟩
    × ( ((d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩ → ⟨ fst c ∈ fst d ⟩ → Empty.⊥)
```

付随する条件は、`c` が現在の添字に属してそこで `∈` に関する最大要素であること、近似が `c` で `r` を記録すること、二端点が現在の値で添字づけられた階層の段階に属すること、`zv` がその順序対であること、そして `precedes (Held r)` が `Lset (fst c)` 上で二端点を比較することを述べます。これは一回の再帰ステップに必要な数学的データであり、有限性は後で数項の等式から得られます。

```agda
      × ( ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
        × ( ⟨ fst x ∈ Lset (fst (lookup b γ)) ⟩
          × ( ⟨ fst y ∈ Lset (fst (lookup b γ)) ⟩
            × ( (zv ≡ pr (fst x) (fst y))
              × ⟨ precedes (Held r) (Lset (fst c)) (fst x) (fst y) ⟩ ) ) ) ) ) )
```

ここから、任意の変数 `z,b,f` と任意の環境について意味論的な対応を示します。`lookup b γ` の台となる集合が順序数であるという仮定は、階層グラフが記述する段階を対応する `Lset` の値と同定するために使われます。

```agda
module _ {n : ℕ} (z b f : Fin n) (γ : S ^ n)
         (ob : IsOrd (fst (lookup b γ))) where
  private
    Body : (c r A A' x y : S) → Type (ℓ-suc ℓ)
    Body c r A A' x y =
```

六つの存在証人が環境を拡張した後、最も内側の本体には二つの決定的な事実が残ります。`z` が指す値が `x,y` の順序対であることと、復元された段階と関係について二端点が `PrecedesAt` を満たすことです。

```agda
        ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) ⊨ prAtL (sh6 z) (suc zero) zero ⟩
      × ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
          ⊨ PrecedesAt (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                       (suc zero) zero ⟩
```

第一の端点 `x` を固定すると、`AtY` は残る端点 `y`、その現在の段階への所属、そして最も内側の二つの事実をまとめます。この型は、論理式の入れ子になった存在の読みの一層に対応します。

```agda
    AtY : (c r A A' x : S) → Type (ℓ-suc ℓ)
    AtY c r A A' x = Σ[ y ∈ S ] (⟨ fst y ∈ fst A' ⟩ × Body c r A A' x y)
```

`MaxOf c` は所属順序での最大性を表します。`d` も現在の添字に属するなら、`c ∈ d` は不可能です。`c` 自身が添字に属することと合わせると、`c` は所属順序で最大になります。後続数項では直前の数項であり、零では `c` の所属という前提の時点ですでに証人がありません。

```agda
    MaxOf : (c : S) → Type (ℓ-suc ℓ)
    MaxOf c = (d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩ → ⟨ fst c ∈ fst d ⟩
            → Empty.⊥
```

論理式の証人を `StepOf` へ変換するため、`c` の所属と最大性、近似の項目 `(c,r)`、直前および現在の段階を同定する等式、そして `x` の現在の段階への所属を仮定します。最後の `AtY` の証人が `y` と二つの内側の事実を与えます。

```agda
    atY : (c r A A' x : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
        → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
        → fst A ≡ Lset (fst c) → fst A' ≡ Lset (fst (lookup b γ))
        → ⟨ fst x ∈ fst A' ⟩
        → AtY c r A A' x → StepOf b f γ (fst (lookup z γ))
```

段階の等式は、論理式における `x,y` の所属を `Lset (lookup b γ)` への所属へ変換し、`StepOf` の要求に合わせます。順序対の等式とホスト側の `precedes` 比較は、続く二つの妥当性の議論から得られます。

```agda
    atY c r A A' x c∈ cmax hf qA qA' x∈ (y , (y∈ , (hpr , hprec))) =
      c , (r , (x , (y , (c∈ , (cmax , (hf
        , ( subst (λ t → ⟨ fst x ∈ t ⟩) qA' x∈
          , ( subst (λ t → ⟨ fst y ∈ t ⟩) qA' y∈
            , (qpair , hprec') ) ) ) ) ) ) ) )
```

ここでは関係変数を直接 `Held r` と解釈するため、二つの表示写像は恒等写像です。したがって `Precedes` の橋は、すでに構成した `relAt` の族に頼らずに対象言語の比較を読み出せます。

```agda
      where
      module P = Precedes (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                          (suc zero) zero (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
                          (Held r) (λ _ _ p → p) (λ _ _ p → p)
```

`PrecedesAt` を読み出すと、論理式で束縛された段階対象上の比較が得られます。その段階を同定する等式によって台を `Lset (fst c)` へ輸送すると、ちょうど `StepOf` が要求する比較になります。

```agda
      hprec' : ⟨ precedes (Held r) (Lset (fst c)) (fst x) (fst y) ⟩
      hprec' = subst (λ t → ⟨ precedes (Held r) t (fst x) (fst y) ⟩) qA
        (P.PrecedesAt-out hprec)
```

`prAtL` の妥当性により、`z` が指す値は復元された二端点の順序対と同定されます。これがメタレベルのステップ証人に必要な順序対の等式です。

```agda
      qpair : fst (lookup z γ) ≡ pr (fst x) (fst y)
      qpair = subst ⟨_⟩
        (prAtL-adequate (sh6 z) (suc zero) zero
          (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)) hpr
```

第一の端点 `x` を取り出した後も、残る端点は命題的に存在することしか分かりません。`AtX` はこの中間状態、すなわち `x` の段階所属と命題的に切り詰められた `AtY` の証人を記録します。

```agda
    AtX : (c r A A' : S) → Type (ℓ-suc ℓ)
    AtX c r A A' = Σ[ x ∈ S ] (⟨ fst x ∈ fst A' ⟩ × ∥ AtY c r A A' x ∥₁)
```

目的の結論自体も命題的に切り詰められているため、隠された `y` の証人を命題の外で選ぶことなく利用できます。その切り詰めの上で各点の変換を写すことで、論理式が与える存在の強さをそのまま保ちます。

```agda
    atX : (c r A A' : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
        → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
        → fst A ≡ Lset (fst c) → fst A' ≡ Lset (fst (lookup b γ))
        → AtX c r A A' → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atX c r A A' c∈ cmax hf qA qA' (x , (x∈ , hy)) =
```

内側の変換は復元したデータから明示的な `StepOf` の証人を一つ組み立て、`PT.map` がそれを命題的切り詰めの下へ戻します。これで、標準的な直前要素や端点の証人を作ることなく、外向きの意味論的な読みが完了します。

```agda
      PT.map (atY c r A A' x c∈ cmax hf qA qA' x∈) hy
```

`c` が添字づける段階を復元した後、残る内側の量化は現在の添字が指す段階を同定します。`AtA'` は、構成可能集合 `A'`、それがそこで段階のグラフを満たす証拠、さらに内側にある証人 `x` と `y` の命題的に切り詰められた存在をまとめます。この切り詰めは証人の存在を保ちますが、特定の証人の対を選びません。

```agda
    AtA' : (c r A : S) → Type (ℓ-suc ℓ)
    AtA' c r A = Σ[ A' ∈ S ]
      ( ⟨ (A' ∷ A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (sh4 b) ⟩
      × ∥ AtX c r A A' ∥₁ )
```

`A'` から先へ進むため、論証はすでに得られた `c` の情報、表の項目 `(c,r)`、そして `A` と `c` が添字づける段階との同一視を保ちます。`AtX` に隠された証人を意味論的な一ステップとして解釈するには、その前に `A'` を現在の順序数添字が指す段階と同定しなければなりません。

```agda
    atA' : (c r A : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
         → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
         → fst A ≡ Lset (fst c)
         → AtA' c r A → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atA' c r A c∈ cmax hf qA (A' , (hg , hx)) =
```

段階のグラフが、まさにこの同一視を与えます。その関数性定理 `Lset-only` に添字の順序数性を適用すると、`fst A' ≡ Lset (fst (lookup b γ))` が得られます。そこで、命題的に切り詰められた `AtX` を、命題的に切り詰められたステップの結論へ除去できます。

```agda
      PT.rec squash₁ (atX c r A A' c∈ cmax hf qA qA') hx
      where
      qA' : fst A' ≡ Lset (fst (lookup b γ))
      qA' = Lset-only zero (sh4 b) (A' ∷ A ∷ r ∷ c ∷ γ) hg ob
```

量化を一つ外へ戻ると、`AtA` は `c` が添字づける段階について同じ役割を果たします。これは、対応する段階のグラフを満たす構成可能集合 `A` と、続きとなる `AtA'` の命題的に切り詰められた存在からなります。

```agda
    AtA : (c r : S) → Type (ℓ-suc ℓ)
    AtA c r = Σ[ A ∈ S ]
      ( ⟨ (A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩
      × ∥ AtA' c r A ∥₁ )
```

この層を解釈するには、まず `A` がどの段階であるかを示す等式が必要です。その等式が得られれば、内側の層と同様に、切り詰められた続きから切り詰められたステップへ除去できます。

```agda
    atA : (c r : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
        → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
        → AtA c r → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atA c r c∈ cmax hf (A , (hg , hA')) =
      PT.rec squash₁ (atA' c r A c∈ cmax hf qA) hA'
```

`c` は `b` が指す順序数に属するので、`mem-ord` により `c` 自身も順序数です。この順序数における段階のグラフの関数性から、`fst A ≡ Lset (fst c)` が得られます。この同定に段階の単調性は使いません。

```agda
      where
      qA : fst A ≡ Lset (fst c)
      qA = Lset-only zero (suc (suc zero)) (A ∷ r ∷ c ∷ γ) hg
        (mem-ord {A = fst (lookup b γ)} ob (fst c) c∈)
```

さらに外側の証人は、近似表が `c` に記録する関係です。`AtR` は、構成可能集合 `r`、表が項目 `(c,r)` を含むことを述べる適用論理式の充足、そして必要な二つの段階を復元する続きの命題的切り詰めを記録します。

```agda
    AtR : (c : S) → Type (ℓ-suc ℓ)
    AtR c = Σ[ r ∈ S ]
      ( ⟨ (r ∷ c ∷ γ) ⊨ appAt (sh2 f) (suc zero) zero ⟩ × ∥ AtA c r ∥₁ )
```

`appAt` の妥当性は、その充足判断を順序対 `(c,r)` についての周囲の所属命題へ変換します。この表の項目が得られると、命題的に切り詰められた `AtA` の続きから、命題的に切り詰められた意味論的ステップへ除去できます。

```agda
    atR : (c : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
        → AtR c → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atR c c∈ cmax (r , (happ , hA)) = PT.rec squash₁ (atA c r c∈ cmax hf) hA
      where
      hf : ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
```

具体的に復元される事実は、`pr (fst c) (fst r) ∈ fst (lookup f γ)` です。これは `StepOf` が必要とするメタレベルの形であり、`f` が指す近似が添字 `c` に関係 `r` を割り当てることを表します。

```agda
      hf = subst ⟨_⟩ (appAt-adequate (sh2 f) (suc zero) zero (r ∷ c ∷ γ)) happ
```

最も外側で、`AtC` は順序数添字の要素 `c` を選び、その添字には `c ∈ d` を満たす要素 `d` がないと主張します。したがって `c` は所属関係に関する添字の極大要素です。後で添字が非零のフォン・ノイマン数項と同定されると、この条件がその直前の数項を同定します。残る命題的に切り詰められた成分は、関係と段階のデータを供給します。

```agda
    AtC : Type (ℓ-suc ℓ)
    AtC = Σ[ c ∈ S ]
      ( ⟨ fst c ∈ fst (lookup b γ) ⟩
      × ( ⟨ (c ∷ γ) ⊨ ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ⟩
        × ∥ AtR c ∥₁ ) )
```

論理式の有界否定は持ち上げられた宇宙で解釈されます。それを降ろすと通常の関数 `MaxOf c` が得られ、添字に属しかつ `c ∈ d` を満たすとされる任意の `d` から矛盾を導けます。すると、切り詰められた関係の証人を先ほどの各層を通して除去できます。

```agda
    atC : AtC → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atC (c , (c∈ , (hmax , hr))) = PT.rec squash₁ (atR c c∈ cmax) hr
      where
      cmax : MaxOf c
      cmax d hd hc = lower (hmax d hd hc)
```

これらの入れ子になった解釈により、ステップ本体を読み出す向きが得られます。逆向きには、同じ本体の論理式を局所的に展開し、明示的な `StepOf` の証人を存在節と有界節へ戻します。

```agda
  opaque
   unfolding RelBodyAt
```

`RelBodyAt` の充足から始めると、最外側の存在量化が与えるのは `c` の命題的に切り詰められた存在だけです。各層の読みは同じ制限のもとで残りのデータを復元し、最後に `∥ StepOf b f γ (fst (lookup z γ)) ∥₁` を得ます。これはステップの存在を示しますが、入れ子の量化に対する標準的な証人を選びません。

```agda
   RelBody-out : ⟨ γ ⊨ RelBodyAt z b f ⟩
               → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
   RelBody-out = PT.rec squash₁ atC
```

逆に、明示的な `StepOf` の証人は、`c`、関係 `r`、比較される対象 `x,y`、それらの段階への所属、順序対の等式、直前の段階での比較をすでに含みます。`RelBody-in` は二つの中間段階を再構成し、このデータを入れ子の論理式へ入れます。存在節は命題的に切り詰められるため、結論は充足を主張しますが、内部の証人からなる標準的な組を保存しません。

```agda
   RelBody-in : StepOf b f γ (fst (lookup z γ)) → ⟨ γ ⊨ RelBodyAt z b f ⟩
   RelBody-in (c , (r , (x , (y , (c∈ , (cmax , (hf , (x∈ , (y∈
              , (qpair , hprec))))))))))
     = ∣ c , (c∈ , (hmax , ∣ r , (happ , ∣ A , (hgA , ∣ A' , (hgA'
       , ∣ x , (x∈ , ∣ y , (y∈ , (hpr , hprec')) ∣₁) ∣₁) ∣₁) ∣₁) ∣₁)) ∣₁
```

最初に再構成する事実は、`c` が順序数だということです。順序数の各要素は順序数なので、これは `c ∈ fst (lookup b γ)` とその集合の順序数性から従います。また、`c` を添字とする構成可能段階を作るためにちょうど必要な条件でもあります。

```agda
     where
     oc : IsOrd (fst c)
     oc = mem-ord {A = fst (lookup b γ)} ob (fst c) c∈
```

この順序数性を用いて、`LsetS` は `Lset (fst c)` を模型の要素 `A` としてまとめます。最初の相違による比較は、この直前の添字が指す段階で評価されます。

```agda
     A : S
     A = LsetS (fst c) oc
```

現在の添字について仮定した順序数性から、同様に `Lset (fst (lookup b γ))` を `A'` としてまとめます。この二つ目の段階が、順序対として現在の関係の要素になる二対象を含む集合の上界を与えます。

```agda
     A' : S
     A' = LsetS (fst (lookup b γ)) ob
```

次に、意味論的な極大性の関数を対象言語の有界全称否定で表します。添字に属する各 `d` について、`c ∈ d` の証明は `cmax` によって矛盾へ送られ、さらに論理式の充足が属する宇宙へ持ち上げられます。

```agda
     hmax : ⟨ (c ∷ γ) ⊨ ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ⟩
     hmax d hd hc = lift (cmax d hd hc)
```

`StepOf` の表の項目は、`pr (fst c) (fst r) ∈ fst (lookup f γ)` という周囲の形をしています。`appAt` の妥当性を与える経路の逆向きに沿ってこの事実を輸送すると、本体の論理式が必要とする適用原子の充足になります。

```agda
     happ : ⟨ (r ∷ c ∷ γ) ⊨ appAt (sh2 f) (suc zero) zero ⟩
     happ = subst ⟨_⟩
       (sym (appAt-adequate (sh2 f) (suc zero) zero (r ∷ c ∷ γ))) hf
```

選んだ `A` は定義により `c` が添字づける段階です。したがって階層の表示定理は、`c` の順序数性と表される値の反射律から、対応する段階グラフの節を証明します。

```agda
     hgA : ⟨ (A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩
     hgA = Lset-defines zero (suc (suc zero)) (A ∷ r ∷ c ∷ γ) oc refl
```

同じ表示定理が、今度は現在の添字で `A'` のグラフ節を証明します。必要な順序数性は仮定 `ob` そのものなので、論理式は `A'` を `x` と `y` を含む段階として正確に認識します。

```agda
     hgA' : ⟨ (A' ∷ A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (sh4 b) ⟩
     hgA' = Lset-defines zero (sh4 b) (A' ∷ A ∷ r ∷ c ∷ γ) ob refl
```

`StepOf` の等式は、`z` が指す候補値を `x` と `y` の Kuratowski 対と同定します。`prAtL` の妥当性を与える経路の逆向きに沿う輸送により、この等式を対象言語の対形成節の充足へ変換します。

```agda
     hpr : ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) ⊨ prAtL (sh6 z) (suc zero) zero ⟩
     hpr = subst ⟨_⟩
       (sym (prAtL-adequate (sh6 z) (suc zero) zero
         (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ))) qpair
```

残るのは、直前の段階における比較の翻訳です。ここでの `Precedes` のインスタンスは基底関係を `Held r`、すなわち順序対が `r` に属するという命題として解釈します。この解釈は対象言語の適用論理式が求める所属命題とすでに同じなので、二つの表現写像はいずれも恒等関数です。

```agda
     module P = Precedes (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                         (suc zero) zero (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
                         (Held r) (λ _ _ p → p) (λ _ _ p → p)
```

この解釈を固定すると、`PrecedesAt-in` は `StepOf` がもつ意味論的な最初の相違による比較を `PrecedesAt` の充足へ変換します。これで `RelBodyAt` のすべての節が満たされ、意味論的ステップから対象言語の論理式へ戻る橋が完成します。

```agda
     hprec' : ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
              ⊨ PrecedesAt (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                           (suc zero) zero ⟩
     hprec' = P.PrecedesAt-in hprec
```

ここまでの本体は一つの候補となる順序対を分類するだけです。一つの関係値はそのような候補をちょうどすべて集めなければならないため、次の構成ではこの一ステップの条件を集合全体へ外延的に拡張します。

## 近似とグラフ

`RelStepAt v b f` は、`v` が指す集合の要素が `RelBodyAt` を満たす対象とちょうど一致することを述べます。候補は新しい零番の変数に束縛され、添字 `b,f` はその束縛子の下で移動します。したがって二つの包含が得られます。候補関係の各要素は意味論的ステップを実現し、そのようなステップを実現する各対象は候補関係に属します。

```agda
opaque
  RelStepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
  RelStepAt v b f = extAt v (RelBodyAt zero (suc b) (suc f))
```

`fst (lookup b γ)` が順序数であれば、この外延的記述の読みが成り立ちます。本体の論理式は、ステップの証人に現れる二つの構成可能段階を同定するためにこの仮定を使います。

```agda
module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n)
         (ob : IsOrd (fst (lookup b γ))) where
  opaque
   unfolding RelStepAt
```

順向きの包含は、`v` が指す集合の要素 `w` から出発し、`w` における本体の論理式を読み、`∥ StepOf b f γ (fst w) ∥₁` を得ます。本体は存在量化によって直前の添字、記録された関係、比較される成分を見つけるため、結果は命題的に切り詰められています。

```agda
   RelStep-out : ⟨ γ ⊨ RelStepAt v b f ⟩ → (w : S)
               → ⟨ fst w ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ (fst w) ∥₁
   RelStep-out h w hw = RelBody-out zero (suc b) (suc f) (w ∷ γ) ob
     (extAt-out v (RelBodyAt zero (suc b) (suc f)) γ h w hw)
```

逆向きの包含は、`w` に対する明示的な意味論的ステップから始めます。`RelBody-in` がそれを本体の充足へ変換し、外延的記述の逆向きの含意から `w` が `v` の指す集合に属することが従います。

```agda
   RelStep-back : ⟨ γ ⊨ RelStepAt v b f ⟩ → (w : S) → StepOf b f γ (fst w)
                → ⟨ fst w ∈ fst (lookup v γ) ⟩
   RelStep-back h w s = extAt-in v (RelBodyAt zero (suc b) (suc f)) γ h w
     (RelBody-in zero (suc b) (suc f) (w ∷ γ) ob s)
```

導入原理はその正確な逆を述べます。`RelStepAt` を証明するには、候補関係の各要素に対して命題的に切り詰められたステップを与え、各明示的ステップ証人に対して所属を証明すれば十分です。この二つの関数が外延性の二つの包含です。

```agda
   RelStep-in : ((w : S) → ⟨ fst w ∈ fst (lookup v γ) ⟩
                 → ∥ StepOf b f γ (fst w) ∥₁)
              → ((w : S) → StepOf b f γ (fst w)
                 → ⟨ fst w ∈ fst (lookup v γ) ⟩)
              → ⟨ γ ⊨ RelStepAt v b f ⟩
```

第一の包含では、命題的に切り詰められた各ステップを `RelBody-in` で写し、命題である充足判断へ除去します。第二の包含では、`RelBody-out` が命題的に切り詰められたステップを生み、それを与えられた逆向きの関数に渡して、命題である所属判断へ除去します。命題的切り詰めを除去できるのは、どちらの目標も命題だからです。

```agda
   RelStep-in into back = extAt-in-both v (RelBodyAt zero (suc b) (suc f)) γ
     (λ w hw → PT.rec (snd ((w ∷ γ) ⊨ RelBodyAt zero (suc b) (suc f)))
       (RelBody-in zero (suc b) (suc f) (w ∷ γ) ob) (into w hw))
     (λ w h → PT.rec (snd (fst w ∈ fst (lookup v γ))) (back w)
       (RelBody-out zero (suc b) (suc f) (w ∷ γ) ob h))
```

この外延的ステップによって、一般的な再帰形状の構成を具体化します。得られる `ApproxAt` は、添字より前の部分を定義域とし、各点でのステップ節が `RelStepAt` に従う表を記述します。`RelGraphAt` は、その近似に支えられた現在の添字での値を記述します。後で添字を数項と同定したとき、この表は有限になります。

```agda
module A = RecShape RelStepAt
open A using ( ApproxAt; ApproxAt-value; ApproxAt-step
             ; ApproxAt-in; GraphOf; PairOf )
     renaming ( GraphAt to RelGraphAt; Graph-in to RelGraph-in
              ; Graph-out to RelGraph-out; PairGraphAt to PairRelGraphAt
```

同じ構成は、近似のグラフとその対にした形についての導入原理と除去原理も与えます。局所名 `RelGraphAt` と `PairRelGraphAt` は、この一般的な仕組みがここでは再帰的に定義された関係値に用いられることを示します。

```agda
              ; PairGraph-in to PairRelGraph-in
              ; PairGraph-out to PairRelGraph-out )
```

ここまでの論理式は再帰の形を記述するだけで、その値をまだ同定していません。次の課題は、この形を満たす任意の表が、先に構成した集合 `relAt m` を正確に記録することを示すことです。そのため、記録された値の正しさと標準的な項目の存在を分けて扱います。

## 再帰に対するステップ

`Values g k` は正しさの条件です。各 `m < k` について、`g` が `# m` と任意の模型要素 `w` を組にした項目を含むなら、`w` の台集合は `relAt m` の台集合に等しくなります。これは、すでに記録された添字における集合値の一意性を述べますが、一意な証明や証人の組を選ぶものではありません。

```agda
Values : S → ℕ → Type (ℓ-suc ℓ)
Values g k = (m : ℕ) → m < k → (w : S)
           → ⟨ pr (# m) (fst w) ∈ fst g ⟩ → fst w ≡ fst (relAt m)
```

`Entries g k` はそれを補う完全性の条件です。各 `m < k` について、標準的な項目 `(# m, relAt m)` が `g` に現れることを要求します。`Values` と `Entries` を合わせると、表がすべての小さい添字をもち、その各添字で意図した集合値だけを記録することが分かります。

```agda
Entries : S → ℕ → Type (ℓ-suc ℓ)
Entries g k = (m : ℕ) → m < k → ⟨ pr (# m) (fst (relAt m)) ∈ fst g ⟩
```

比較 `before k x y` が成り立つなら、`k` は後続数です。零では関係が空なので比較から矛盾が従い、`suc m` では直前の数 `m` と必要な等式がただちに得られます。この補題により、後で `relAt k` の要素を `StepOf` が必要とする直前の数のデータへ戻せます。

```agda
before-suc : (k : ℕ) (x y : V ℓ) → ⟨ before k x y ⟩ → Σ[ m ∈ ℕ ] (k ≡ suc m)
before-suc zero    x y h = Empty.rec* h
before-suc (suc m) x y h = m , refl
```

`v` が指す候補関係、`b` が指す添字、`f` が指す表を固定します。等式 `qb` は添字を数項 `# k` と同定し、`vals` と `ents` は表が `k` より下で正しく完全であることを主張します。これらの仮定のもとで、添字における意味論的ステップを `relAt k` への所属と正確に比較できます。

```agda
module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) (k : ℕ)
         (qb : fst (lookup b γ) ≡ # k)
         (vals : Values (lookup f γ) k) (ents : Entries (lookup f γ) k) where
  private
    ob : IsOrd (fst (lookup b γ))
```

数項 `# k` は順序数です。この事実を `qb : fst (lookup b γ) ≡ # k` に沿って逆向きに輸送すると、`fst (lookup b γ)` が順序数であることが分かり、先に得たステップ本体の読みと書き入れの補題を使えるようになります。

```agda
    ob = subst IsOrd (sym qb) (numeral-ord k)
```

候補値 `x` に対する明示的な `StepOf` の証人を考えます。その極大要素 `c` は添字に属し、`qb` によって `fst c ∈ # k` と読み替えられます。数項への所属を除去すると、命題的切り詰めのもとで自然数 `m < k` と等式 `fst c ≡ # m` が復元されます。ここで切り詰めを除去できるのは、目標の所属 `x ∈ relAt k` が命題だからです。

```agda
    into : (x : V ℓ) → StepOf b f γ x → ⟨ x ∈ fst (relAt k) ⟩
    into x (c , (r , (xx , (yy , (c∈ , (cmax , (hf , (xx∈ , (yy∈
           , (qx , hprec)))))))))) =
      PT.rec (snd (x ∈ fst (relAt k))) atC
        (∈#-elim k (fst c) (subst (λ t → ⟨ fst c ∈ t ⟩) qb c∈))
```

このような `m` に対しては、`relAt k` の導入補題により必要な所属を証明します。対応する `RelOf k x` の証人は、同じ成分 `xx` と `yy`、それらの `finiteStage k` への所属、`x` をその順序対と同定する等式、そして比較 `before k xx yy` を用います。したがって残る仕事は、極大要素 `c` が実際に `k` の直前の数に対応することを示し、それに従って表に記録された比較を翻訳することです。

```agda
      where
      atC : Σ[ m ∈ ℕ ] ((m < k) × (fst c ≡ # m)) → ⟨ x ∈ fst (relAt k) ⟩
      atC (m , (hm , qc)) = relAt-in k x
        (xx , (yy , (xxk , (yyk , (qx , below)))))
        where
```

`c` は `# m` によって符号化され、しかも `# k` の要素の中で極大なので、`k = suc m` でなければなりません。三分律で `suc m` と `k` を比較すると、等しい場合には求める等式が得られ、二つの狭義不等号の場合は、それぞれ既知の `m` と `k` の関係または極大性に矛盾します。

```agda
        ksuc : k ≡ suc m
        ksuc = decide (suc m ≟ k)
          where
          decide : NatOrder.Trichotomy (suc m) k → k ≡ suc m
          decide (NatOrder.lt hlt) = Empty.rec
```

もし `suc m < k` なら、数項 `#(suc m)` 自身が `# k` に属します。また `c = # m` なので、`c ∈ #(suc m)` でもあります。この二つの所属は、添字の中に `c` より真に大きい要素があることを示し、極大性の節に矛盾します。

```agda
            (cmax (numS (suc m))
              (subst (λ t → ⟨ fst (numS (suc m)) ∈ t ⟩) (sym qb)
                (subst (λ t → ⟨ t ∈ # k ⟩) (sym (numS-fst (suc m)))
                  (#mono (suc m) k hlt)))
              (subst (λ t → ⟨ fst c ∈ t ⟩) (sym (numS-fst (suc m)))
```

反対に `k < suc m` なら、後続を外すことで `k ≤ m` が得られ、既知の `m < k` と両立しません。したがって等しい場合だけが残り、三分律から得た等式を反転すると、以下で必要な向きの `k ≡ suc m` が得られます。

```agda
                (subst (λ t → ⟨ t ∈ # (suc m) ⟩) (sym qc)
                  (#mono m (suc m) NatOrder.≤-refl))))
          decide (NatOrder.eq e) = sym e
          decide (NatOrder.gt hgt) = Empty.rec (<-asym hm (pred-≤-pred hgt))
```

ステップの証人はすでに、`xx` が `Lset (fst (lookup b γ))` に属することを与えています。`qb` に沿って輸送すると、この集合は `Lset (# k)`、すなわち `finiteStage k` と同定され、`RelOf k x` が必要とする第一の段階所属の成分が得られます。

```agda
        xxk : ⟨ fst xx ∈ finiteStage k ⟩
        xxk = subst (λ t → ⟨ fst xx ∈ Lset t ⟩) qb xx∈
```

順序対の二つの端点は、いずれも `k` で添字づけられた段階に属さなければならない。第二の端点については、上界を `# k` と同一視する等式により、`Lset (fst (lookup b γ))` への所属を `finiteStage k` への所属に移す。

```agda
        yyk : ⟨ fst yy ∈ finiteStage k ⟩
        yyk = subst (λ t → ⟨ fst yy ∈ Lset t ⟩) qb yy∈
```

前者の数項で添字づけられた表の項目は、関係 `r` を記録している。第一成分を `fst c` から `# m` に移すと、正しさの仮定 `vals` によって `r` の台集合が `relAt m` と同一視される。

```agda
        rval : fst r ≡ fst (relAt m)
        rval = vals m hm r
          (subst (λ t → ⟨ pr t (fst r) ∈ fst (lookup f γ) ⟩) qc hf)
```

ステップの証人は初め、`Lset (fst c)` 上で `r` が保持する関係を用いて二つの端点を比較する。等式 `fst c ≡ # m` と `fst r ≡ fst (relAt m)` により、これは `precedes (Rel m) (finiteStage m)` に書き換えられる。

```agda
        atM : ⟨ precedes (Rel m) (finiteStage m) (fst xx) (fst yy) ⟩
        atM = subst (λ t → ⟨ precedes (λ s u → pr s u ∈ t) (finiteStage m)
                              (fst xx) (fst yy) ⟩) rval
          (subst (λ t → ⟨ precedes (Held r) (Lset t) (fst xx) (fst yy) ⟩) qc
            hprec)
```

再帰的な比較を得るため、`precedes-map` は基底関係 `Rel m` を `before m` に置き換える。基底関係は一致条件の前提に現れるため、必要な仮定の向きは逆であり、`before m` から `relAt m` への所属へ進む。こうしてまず `before (suc m)` が得られ、等式 `k ≡ suc m` から `before k` が従う。

```agda
        below : ⟨ before k (fst xx) (fst yy) ⟩
        below = subst (λ j → ⟨ before j (fst xx) (fst yy) ⟩) (sym ksuc)
          (precedes-map (Rel m) (before m) (finiteStage m) (fst xx) (fst yy)
            (λ w t hw ht hbf → relAt-fill m w t hw ht hbf) atM)
```

逆方向では、`RelOf k` で記述された要素を意味論的なステップの証人へ変換する。二つの端点はすでに与えられており、残る仕事は前者の添字とその関係の項目を復元し、その前者が上界の最大要素であることを示すことである。

```agda
    from : (x : V ℓ) → RelOf k x → StepOf b f γ x
    from x (xx , (yy , (xx∈ , (yy∈ , (qx , hbf))))) =
      numS m , (relAt m , (xx , (yy , (c∈ , (cmax , (hf , (xxb , (yyb
        , (qx , hprec)))))))))
      where
```

`k` が零なら `before k` の証明は存在しない。したがって補題 `before-suc` は、比較が後者段階で生じるような自然数 `m` を取り出す。

```agda
      m : ℕ
      m = before-suc k (fst xx) (fst yy) hbf .fst
```

同じ後者の分析から等式 `k ≡ suc m` も得られる。この等式が、段階 `k` での比較と、段階 `m` のデータを基底とする再帰のステップを結びつける。

```agda
      qk : k ≡ suc m
      qk = before-suc k (fst xx) (fst yy) hbf .snd
```

`k` は `suc m` なので、前者は `m < k` を満たす。この上界により、添字 `m` における近似表の正しさと完全性の仮定をともに利用できる。

```agda
      hm : m < k
      hm = subst (λ j → m < j) (sym qk) NatOrder.≤-refl
```

前者を表す数項は、`b` に保存された上界の要素でなければならない。不等式 `m < k` から `# m ∈ # k` が得られ、`numS m` と上界についての等式がこの所属を必要な形へ移す。

```agda
      c∈ : ⟨ fst (numS m) ∈ fst (lookup b γ) ⟩
      c∈ = subst (λ t → ⟨ fst (numS m) ∈ t ⟩) (sym qb)
        (subst (λ t → ⟨ t ∈ # k ⟩) (sym (numS-fst m)) (#mono m k hm))
```

さらに、`# m` が `# k` の要素のうち最大であることを示す必要がある。`d ∈ # k` と `# m ∈ d` が与えられると、数項の消去は命題的切り詰めの中で `d` を `j < k` を満たすある `# j` として表す。この二つの所属から `m < j` と `j ≤ m` が同時に従う。

```agda
      cmax : (d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩
           → ⟨ fst (numS m) ∈ fst d ⟩ → Empty.⊥
      cmax d hd hc = PT.rec Empty.isProp⊥ step
        (∈#-elim k (fst d) (subst (λ t → ⟨ fst d ∈ t ⟩) qb hd))
        where
```

`d ≡ # j` という分岐では、`d` が `# k = # (suc m)` に属することから `j ≤ m` が得られる。一方、`# m` が `d` に属することから狭義不等式 `m < j` が得られるので、自然数順序の非対称性がこの分岐を退ける。

```agda
        step : Σ[ j ∈ ℕ ] ((j < k) × (fst d ≡ # j)) → Empty.⊥
        step (j , (hj , qd)) = <-asym mj (pred-≤-pred (subst (λ i → j < i) qk hj))
          where
          mj : m < j
          mj = #∈#-elim m j
```

`m < j` の導出には、フォン・ノイマン数項の所属と狭義順序との正確な対応を用いる。`numS m` の等式と `d ≡ # j` により、仮定された所属をまず `# m ∈ # j` に書き換え、その後で数項の所属を復号する。

```agda
            (subst (λ t → ⟨ t ∈ # j ⟩) (numS-fst m)
              (subst (λ t → ⟨ fst (numS m) ∈ t ⟩) qd hc))
```

`m < k` であるため、完全性 `ents` は標準的な表の項目 `(# m , relAt m)` を与える。`# m` を `numS m` の台集合として書き換えると、意味論的なステップの証人が要求する項目が得られる。

```agda
      hf : ⟨ pr (fst (numS m)) (fst (relAt m)) ∈ fst (lookup f γ) ⟩
      hf = subst (λ t → ⟨ pr t (fst (relAt m)) ∈ fst (lookup f γ) ⟩)
        (sym (numS-fst m)) (ents m hm)
```

`RelOf k` の記録は第一の端点を `finiteStage k`、すなわち `Lset (# k)` に置く。上界の等式で `# k` を書き換えると、その端点は `Lset (fst (lookup b γ))` に属し、`StepOf` の要件を満たす。

```agda
      xxb : ⟨ fst xx ∈ Lset (fst (lookup b γ)) ⟩
      xxb = subst (λ t → ⟨ fst xx ∈ Lset t ⟩) (sym qb) xx∈
```

同じ移送によって、第二の端点も上界が定める段階に置かれる。二つの端点条件により、復元されたステップは任意の集合上の比較ではなく、有界な関係にとどまる。

```agda
      yyb : ⟨ fst yy ∈ Lset (fst (lookup b γ)) ⟩
      yyb = subst (λ t → ⟨ fst yy ∈ Lset t ⟩) (sym qb) yy∈
```

`RelOf k` に保存された比較をまず `k ≡ suc m` に沿って書き換え、再帰節 `precedes (before m) (finiteStage m)` を現す。意味論的なステップを得るには、さらにその基底関係を `before m` から `relAt m` への所属へ置き換えなければならない。

```agda
      hprec : ⟨ precedes (Held (relAt m)) (Lset (fst (numS m)))
                 (fst xx) (fst yy) ⟩
      hprec = subst (λ t → ⟨ precedes (Held (relAt m)) (Lset t)
                              (fst xx) (fst yy) ⟩) (sym (numS-fst m))
        (precedes-map (before m) (Rel m) (finiteStage m) (fst xx) (fst yy)
```

ここで `precedes-map` は、`relAt m` への所属から `before m` へ戻る向きの `relAt-rep` を用いる。一致条件の前提における反変性により、`Rel m` を基底とする比較が得られる。最後に数項の等式で段階を `Lset (fst (numS m))` に書き換え、`StepOf` の最後の欄を得る。

```agda
          (λ w t hw ht hR → relAt-rep m w t hw ht hR)
          (subst (λ j → ⟨ before j (fst xx) (fst yy) ⟩) qk hbf))
```

補題 `step-rel` は、添字 `k` でステップ論理式を満たす任意の集合が `relAt k` に等しいことを示す。外延性により、この集合の等式は二つの所属の含意に帰着する。順方向では、`RelStep-out` が命題的に切り詰められたステップの証人を与え、`into` がその任意の証人を `relAt k` への所属へ送る。

```agda
  step-rel : ⟨ γ ⊨ RelStepAt v b f ⟩ → fst (lookup v γ) ≡ fst (relAt k)
  step-rel h = cong fst (extensionalL {a = lookup v γ} {b = relAt k} pt)
    where
    fwd : (x : S) → ⟨ fst x ∈ fst (lookup v γ) ⟩ → ⟨ fst x ∈ fst (relAt k) ⟩
    fwd x hx = PT.rec (snd (fst x ∈ fst (relAt k))) (into (fst x))
```

ここでは `relAt k` への所属が命題なので、命題的切り詰めを除去できる。特定の前者や順序対の証人を選ぶことはなく、もとの要素が実現された関係に属するという事実だけを保つ。

```agda
      (RelStep-out v b f γ ob h x hx)
```

逆向きの所属の含意では、`relAt-out` がその要素について命題的に切り詰められた `RelOf k` の記述を与える。写像 `from` がそこから `StepOf` の証人を復元し、`RelStep-back` がその要素をステップ論理式を満たす集合へ入れる。

```agda
    bwd : (x : S) → ⟨ fst x ∈ fst (relAt k) ⟩ → ⟨ fst x ∈ fst (lookup v γ) ⟩
    bwd x hx = PT.rec (snd (fst x ∈ fst (lookup v γ)))
      (λ ro → RelStep-back v b f γ ob h x (from (fst x) ro))
      (relAt-out k (fst x) hx)
```

各構成可能な要素について、二つの含意は二つの所属命題の間の同値を与える。命題外延性がその同値をパスに変え、集合の外延性が各点のパスを必要な台集合の等式にまとめる。

```agda
    pt : (x : S) → (fst x ∈ fst (lookup v γ)) ≡ (fst x ∈ fst (relAt k))
    pt x = ⇔toPath (fwd x) (bwd x)
```

逆向きの補題 `rel-step` は、候補となる値と `relAt k` の等式から出発してステップ論理式を示す。導入規則には所属の二方向が必要である。第一の方向では、`toStep` が候補の値の各要素に、命題的に切り詰められた意味論的ステップを対応させる。

```agda
  rel-step : fst (lookup v γ) ≡ fst (relAt k) → ⟨ γ ⊨ RelStepAt v b f ⟩
  rel-step q = RelStep-in v b f γ ob toStep backStep
    where
    toStep : (w : S) → ⟨ fst w ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ (fst w) ∥₁
    toStep w hw = PT.map (from (fst w))
```

この等式により、まず候補の要素を `relAt k` へ移す。`relAt k` の外向きの表現が与えるのは、命題的に切り詰められた `RelOf k` の記録だけであり、`PT.map from` はその切り詰めを保ったまま、あり得る要素をステップの証人へ変換する。

```agda
      (relAt-out k (fst w) (subst (λ t → ⟨ fst w ∈ t ⟩) q hw))
```

第二の所属の向きは、明示的な `StepOf` の証人から始まる。写像 `into` が `relAt k` への所属を示し、仮定した等式の逆向きに沿って、その所属を候補の値へ戻す。

```agda
    backStep : (w : S) → StepOf b f γ (fst w) → ⟨ fst w ∈ fst (lookup v γ) ⟩
    backStep w st = subst (λ t → ⟨ fst w ∈ t ⟩) (sym q) (into (fst w) st)
```

## 近似が記録するすべての値

補題 `entryOf` は、値の正しさを項目の完全性へ変える。`j < k` なら近似は `# j` で何らかの値をもち、そこに記録されたすべての値が `relAt j` に等しければ、標準的な対 `(# j , relAt j)` 自身が近似に属する。

```agda
entryOf : ∀ {n} (f a : Fin n) (γ : S ^ n) (k : ℕ)
        → fst (lookup a γ) ≡ # k → ⟨ γ ⊨ ApproxAt f a ⟩
        → (j : ℕ) → j < k
        → ((u : S) → ⟨ pr (# j) (fst u) ∈ fst (lookup f γ) ⟩
           → fst u ≡ fst (relAt j))
```

`ApproxAt` の定義域の完全性は、命題的切り詰めのもとで、数項 `# j` におけるある値 `u` の存在を与える。目標は標準的な対が近似に属するという命題なので、この切り詰めを除去して、仮定した `u` の正しさを利用できる。

```agda
        → ⟨ pr (# j) (fst (relAt j)) ∈ fst (lookup f γ) ⟩
entryOf f a γ k qa h j hj vs =
  PT.rec (snd (pr (# j) (fst (relAt j)) ∈ fst (lookup f γ))) named
    (ApproxAt-value f a γ h (numS j)
      (subst (λ t → ⟨ fst (numS j) ∈ t ⟩) (sym qa)
```

定義域についての論証は `j < k` に基づく。数項の単調性から `# j ∈ # k` が得られ、`numS j` と上界の等式によって、その所属を `ApproxAt-value` が要求する形へ移す。結論は、命題的切り詰めのもとで何らかの記録値が存在すると述べるだけであり、特定の値を選ばない。

```agda
        (subst (λ t → ⟨ t ∈ # k ⟩) (sym (numS-fst j)) (#mono j k hj))))
  where
  named : Σ[ u ∈ S ] ⟨ pr (fst (numS j)) (fst u) ∈ fst (lookup f γ) ⟩
        → ⟨ pr (# j) (fst (relAt j)) ∈ fst (lookup f γ) ⟩
  named (u , p) =
```

そのような値の分岐では、数項の等式により、記録された対をまず `(# j , u)` の形に整える。正しさの仮定から `fst u ≡ fst (relAt j)` が得られ、第二成分を置換することで、記録された所属を標準的な対の所属へ変換する。

```agda
    subst (λ t → ⟨ pr (# j) t ∈ fst (lookup f γ) ⟩) (vs u p') p'
    where
    p' : ⟨ pr (# j) (fst u) ∈ fst (lookup f γ) ⟩
    p' = subst (λ t → ⟨ pr t (fst u) ∈ fst (lookup f γ) ⟩) (numS-fst j) p
```

上界が `# k` である近似を固定する。帰納の動機 `Val m` は、`m < k` なら、キー `# m` に記録されたすべての構成可能な値 `w` の台集合が `relAt m` に等しいと述べる。

```agda
module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) (k : ℕ)
         (qa : fst (lookup a γ) ≡ # k) (h : ⟨ γ ⊨ ApproxAt f a ⟩) where
  private
    Val : ℕ → Type (ℓ-suc ℓ)
    Val m = (m < k) → (w : S) → ⟨ pr (# m) (fst w) ∈ fst (lookup f γ) ⟩
```

この動機は一つの値を選ぶのではなく、記録され得るすべての値を量化する。その結論は二つの台集合の等式であり、表の項目を書き換えるためにも、近似の値の一意性を示すためにも、ちょうど必要な形である。

```agda
          → fst w ≡ fst (relAt m)
```

正しさは、自然数の狭義順序に関する整礎帰納法で示す。`m` における値を同一視するため、帰納仮定からすべての `j < m` における正しさを得て、`w` と `m` を表す数項で拡張した環境において候補の値 `w` に `step-rel` を適用する。ここで使うのは自然数の `<` の整礎性であり、`before` の整礎性ではない。

```agda
  approx-val : (m : ℕ) → Val m
  approx-val = WFI.induction <-wellfounded go
    where
    go : (m : ℕ) → ((j : ℕ) → j < m → Val j) → Val m
    go m IH hm w hw = step-rel zero (suc zero) (sh2 f) (w ∷ numS m ∷ γ) m
```

`(# m , w)` が記録されているという仮定から、`ApproxAt-step` は `w` が満たすステップ論理式を与える。このステップを `step-rel` によって `relAt m` と同一視するには、さらに小さいすべての添字について、記録値が正しいことと、各標準項目が存在することの二つを渡す。

```agda
      (numS-fst m) vals ents
      (ApproxAt-step f a γ h (numS m) w
        (subst (λ t → ⟨ pr t (fst w) ∈ fst (lookup f γ) ⟩)
          (sym (numS-fst m)) hw))
      where
```

`j < m` に対する正しさは、ちょうど添字 `j` における帰納仮定である。その適用に必要な `j < k` は、`j < m` と現在の仮定 `m < k` の推移性から得られる。

```agda
      vals : Values (lookup (sh2 f) (w ∷ numS m ∷ γ)) m
      vals j hj u hu = IH j hj (<-trans hj hm) u hu
```

`m` より下での完全性は `entryOf` から得られる。各 `j < m` について、推移性から再び `j < k` が得られ、帰納仮定は `j` に記録されたすべての値が `relAt j` に等しいという前提を与える。したがって添字 `j` の標準項目が存在する。

```agda
      ents : Entries (lookup (sh2 f) (w ∷ numS m ∷ γ)) m
      ents j hj = entryOf f a γ k qa h j (<-trans hj hm)
        (λ u p → IH j hj (<-trans hj hm) u p)
```

上界内のすべての添字で正しさが示されれば、`entryOf` から直ちに近似の完全性が得られる。したがって `approx-ent` は、各 `m < k` について標準的な対 `(# m , relAt m)` が記録表に含まれることを述べる。

```agda
  approx-ent : (m : ℕ) → m < k
             → ⟨ pr (# m) (fst (relAt m)) ∈ fst (lookup f γ) ⟩
  approx-ent m hm = entryOf f a γ k qa h m hm (approx-val m hm)
```

グラフ論理式は、`k` までの近似と最後のステップを命題的切り詰めのもとに隠している。補題 `rel-only` は、その切り詰めを命題である集合の等式へ除去し、`v` に保存された値が `relAt k` でなければならないことを述べる。

```agda
module _ {n : ℕ} (v b : Fin n) (γ : S ^ n) (k : ℕ)
         (qb : fst (lookup b γ) ≡ # k) where
  rel-only : ⟨ γ ⊨ RelGraphAt v b ⟩ → fst (lookup v γ) ≡ fst (relAt k)
  rel-only h = PT.rec (setIsSet (fst (lookup v γ)) (fst (relAt k))) read
    (RelGraph-out v b γ h)
```

表された各分岐で、グラフは近似 `g`、`g` が `ApproxAt` を満たす証明、そして添字 `k` におけるステップの証明を与える。先の整礎帰納法が `g` によって `k` より下に記録されたすべての値を同一視し、続いて `step-rel` が最後の値を `relAt k` と同一視する。

```agda
    where
    read : GraphOf v b γ → fst (lookup v γ) ≡ fst (relAt k)
    read (g , (ha , hs)) =
      step-rel (suc v) (suc b) zero (g ∷ γ) k qb
        (λ m hm w hw → approx-val zero (suc b) (g ∷ γ) k qb ha m hm w hw)
```

`step-rel` へのもう一つの入力は、同じ近似が `k` より下で完全であることである。これは `approx-ent` から得られ、値についての定理を用いて、存在だけが知られている各項目を対応する標準項目へ置き換える。

```agda
        (λ m hm → approx-ent zero (suc b) (g ∷ γ) k qb ha m hm)
        hs
```

## 近似を具体的に構成する

以下で使う有限族を `finSet` で集めるには、まずその全要素を共通の構成可能段階に置きます。より一般に、`smallStage` は任意の小さな族 `g : X → S` の各要素が属する段階に順序数の上界を取り、すべての `fst (g x)` が `Lset σ` に属するような順序数 `σ` を返します。

```agda
smallStage : (X : Type ℓ) (g : X → S)
           → Σ[ σ ∈ V ℓ ] (IsOrd σ × ((x : X) → ⟨ fst (g x) ∈ Lset σ ⟩))
smallStage X g = bd .fst , (bd .snd .fst , mem)
  where
  bd = boundingOrd X (λ x → stage (fst (g x)) (g x .snd))
```

各 `g x` はすでに自身の生成段階に属している。上界となる順序数はそれらすべての生成段階より上にあるので、`Lset` の単調性によって各所属を共通の段階 `Lset σ` へ移せる。

```agda
         (λ x → stage-ord (fst (g x)) (g x .snd))
  mem : (x : X) → ⟨ fst (g x) ∈ Lset (bd .fst) ⟩
  mem x = Lset-mono {α = bd .fst} {β = stage (fst (g x)) (g x .snd)}
    (bd .snd .snd x) (stage-mem (fst (g x)) (g x .snd))
```

上界 `k` を固定すると、有限添字型 `Fin k` は `k` より小さい自然数をちょうど列挙する。族 `famOf k` は添字 `i` に、数項 `# (toℕ i)` と実現された関係 `relAt (toℕ i)` を二成分とする構成可能な順序対を対応させる。

```agda
private
  famOf : (k : ℕ) → Fin k → S
  famOf k i = prS (numS (toℕ i)) (relAt (toℕ i))
```

持ち上げた `Fin k` により、この有限添字型を `smallStage` が要求する宇宙に置く。`famOf k` に共通段階の補題を適用すると、すべての順序対を含む一つの順序数段階が得られ、後で `finSetL` が必要とする構成可能性の前提が満たされる。

```agda
  famBnd : (k : ℕ) → Σ[ σ ∈ V ℓ ] (IsOrd σ
         × ((i : Lift {ℓ-zero} {ℓ} (Fin k)) → ⟨ fst (famOf k (lower i)) ∈ Lset σ ⟩))
  famBnd k = smallStage (Lift {ℓ-zero} {ℓ} (Fin k)) (λ i → famOf k (lower i))
```

`famOf k i` の台集合は順序対全体であり、その第一成分だけではない。等式 `famEq` は構成可能な対と数項の表現を展開し、それを `pr (# (toℕ i)) (fst (relAt (toℕ i)))` と同一視する。

```agda
  famEq : (k : ℕ) (i : Fin k)
        → fst (famOf k i) ≡ pr (# (toℕ i)) (fst (relAt (toℕ i)))
  famEq k i = prS-fst (numS (toℕ i)) (relAt (toℕ i))
            ∙ cong (λ t → pr t (fst (relAt (toℕ i)))) (numS-fst (toℕ i))
```

近似 `approxSet k` は `finSet` によって構成され、`Fin k` で添字づけられた台の順序対の族を有限集合に集める。証明 `finSetL` はそれらの共通段階を用いて、この有限集合が `L` の要素であることを示す。この構成では置換公理を用いない。

```agda
opaque
  approxSet : ℕ → S
  approxSet k = finSet k (λ i → fst (famOf k i))
    , FinOf.finSetL (famBnd k .fst) (famBnd k .snd .fst) k
        (λ i → fst (famOf k i)) (λ i → famBnd k .snd .snd (lift i))
```

射影の等式により、`approxSet k` の台集合がまさにこの `finSet` であることが分かる。したがって後続の所属補題では、有限集合の導入規則と除去規則を用いて、その項目がちょうど `j < k` を満たす対 `(# j , relAt j)` であることを示せる。

```agda
  approxSet-fst : (k : ℕ) → fst (approxSet k) ≡ finSet k (λ i → fst (famOf k i))
  approxSet-fst k = refl
```

有限近似は意図された各項目を含む。`j < k` ならば、`# j` と `relAt j` の順序対は `approxSet k` に属する。これは `approxSet` の有限集合構成がもつ性質であり、置換を用いたものではない。

```agda
approx-mem-in : (k j : ℕ) → j < k
              → ⟨ pr (# j) (fst (relAt j)) ∈ fst (approxSet k) ⟩
approx-mem-in k j hj =
  subst (λ t → ⟨ t ∈ fst (approxSet k) ⟩)
    (cong (λ i → pr (# i) (fst (relAt i))) (toℕ∘enum j hj))
```

不等式から `enum j hj : Fin k` が得られる。等式 `famEq` は有限族の対応する要素を求める順序対と同一視し、`finSet-in` はそれを `finSet` で構成され `finSetL` により `L` に属すると保証された集合へ書き込む。

```agda
    (subst (λ t → ⟨ pr (# (toℕ (enum j hj))) (fst (relAt (toℕ (enum j hj)))) ∈ t ⟩)
      (sym (approxSet-fst k))
      (finSet-in k (λ i → fst (famOf k i))
        (pr (# (toℕ (enum j hj))) (fst (relAt (toℕ (enum j hj)))))
        ∣ enum j hj , famEq k (enum j hj) ∣₁))
```

逆に、`approxSet k` への所属から得られるのは、その要素がある `j < k` で添字付けられた意図どおりの項目であるという命題的切り詰めだけである。したがって、この補題は現れる順序対を正確に記述するが、標準的な添字の証人を選ぶものではない。

```agda
approx-mem-out : (k : ℕ) (y : V ℓ) → ⟨ y ∈ fst (approxSet k) ⟩
               → ∥ Σ[ j ∈ ℕ ] ((j < k) × (y ≡ pr (# j) (fst (relAt j)))) ∥₁
approx-mem-out k y h = PT.map named
  (finSet-out k (λ i → fst (famOf k i)) y
    (subst (λ t → ⟨ y ∈ t ⟩) (approxSet-fst k) h))
```

列挙された添字 `i : Fin k` を自然数 `toℕ i` に移し、同時に `toℕ<n i` を得る。所属から得た等式を逆向きにして `famEq` と合成すると、元の要素から標準的な順序対への必要な等式が得られる。

```agda
  where
  named : Σ[ i ∈ Fin k ] (fst (famOf k i) ≡ y)
        → Σ[ j ∈ ℕ ] ((j < k) × (y ≡ pr (# j) (fst (relAt j))))
  named (i , q) = toℕ i , (toℕ<n i , (sym q ∙ famEq k i))
approxVals : (k : ℕ) → Values (approxSet k) k
```

この所属の記述から値の正しさが従う。第一成分が `# m` の項目が `k` より下に現れるなら、その第二成分は `relAt m` の台となる集合である。`V` の集合どうしの等しさは命題なので、添字を包む命題的切り詰めを除去できる。

```agda
approxVals k m hm u hu = PT.rec (setIsSet (fst u) (fst (relAt m))) named
  (approx-mem-out k (pr (# m) (fst u)) hu)
  where
  named : Σ[ j ∈ ℕ ] ((j < k) × (pr (# m) (fst u) ≡ pr (# j) (fst (relAt j))))
        → fst u ≡ fst (relAt m)
```

順序対の単射性は等式を二つの成分に分ける。さらに数項の単射性が復元された添字を `m` と同一視するので、第二成分の等式を `relAt j` から `relAt m` へ移せる。

```agda
  named (j , (hj , q)) = pr-inj q .snd
    ∙ cong (λ i → fst (relAt i)) (sym (#-inj′ (pr-inj q .fst)))
```

値の正しさと対になるのが項目の完全性である。各 `m < k` について、標準的な順序対 `(# m, relAt m)` が表に含まれる。これは上の有限集合の所属補題から直ちに従う。

```agda
approxEnts : (k : ℕ) → Entries (approxSet k) k
approxEnts k m hm = approx-mem-in k m hm
```

`f` が `approxSet k` を、`a` が数項 `# k` を表す環境を固定する。残る課題は、この具体的な有限表が抽象的な近似の論理式を満たすことの確認である。

```agda
module _ (k : ℕ) {n : ℕ} (f a : Fin n) (γ : S ^ n)
         (qf : fst (lookup f γ) ≡ fst (approxSet k))
         (qa : fst (lookup a γ) ≡ # k) where
  private
    onDom : (x : S)
```

定義域の条件には二つの向きがある。表に現れる第一成分は `# k` に属さなければならず、`# k` の各要素は何らかの表項目の第一成分として現れなければならない。第二成分についての存在主張は命題的切り詰めとして解釈される。

```agda
          → (⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
             → ⟨ fst x ∈ fst (lookup a γ) ⟩)
          × (⟨ fst x ∈ fst (lookup a γ) ⟩
             → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩)
    onDom x = fwd , bwd
```

第一の向きでは、ある第二成分が `x` とともに表の項目をなすことだけを仮定する。目標の `x ∈ # k` は命題なので、存在証人の命題的切り詰めを除去してから、`approx-mem-out` でその順序対を調べられる。

```agda
      where
      fwd : ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
          → ⟨ fst x ∈ fst (lookup a γ) ⟩
      fwd = PT.rec (snd (fst x ∈ fst (lookup a γ))) atY
        where
```

その項目を `approxSet k` へ移すと、`approx-mem-out` から命題的切り詰められた `j < k` と、第 `j` の標準的な順序対との等式が得られる。求める添字への所属は命題なので、ここでも命題的切り詰めを除去できる。

```agda
        atY : Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
            → ⟨ fst x ∈ fst (lookup a γ) ⟩
        atY (y , p) = PT.rec (snd (fst x ∈ fst (lookup a γ))) named
          (approx-mem-out k (pr (fst x) (fst y))
            (subst (λ t → ⟨ pr (fst x) (fst y) ∈ t ⟩) qf p))
```

第一成分の等式は、`x` の台となる集合が `# j` であることを述べる。`a` を `# k` と解釈する等式を用いると、目標はこの集合が `# k` に属することへ帰着する。

```agda
          where
          named : Σ[ j ∈ ℕ ]
                    ((j < k) × (pr (fst x) (fst y) ≡ pr (# j) (fst (relAt j))))
                → ⟨ fst x ∈ fst (lookup a γ) ⟩
          named (j , (hj , q)) = subst (λ t → ⟨ fst x ∈ t ⟩) (sym qa)
```

数項の単調性により `j < k` から `# j ∈ # k` が得られる。第一成分の等式に沿って移せば、元の `x` が求める定義域に属することが従う。

```agda
            (subst (λ t → ⟨ t ∈ # k ⟩) (sym (pr-inj q .fst)) (#mono j k hj))
```

逆向きでは、`# k` への所属を、与えられた要素が数項となるような自然数 `j < k` の命題的切り詰めとして読み出す。この切り詰められたデータを写せば、必要な表項目の命題的切り詰めが得られる。

```agda
      bwd : ⟨ fst x ∈ fst (lookup a γ) ⟩
          → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
      bwd hx = PT.map named
        (∈#-elim k (fst x) (subst (λ t → ⟨ fst x ∈ t ⟩) qa hx))
        where
```

明示的に得られた `j` に対し、第二成分として `relAt j` を選ぶ。項目の完全性により `(# j, relAt j)` は `approxSet k` に入り、有限表の解釈を与える等式と第一成分の等式に沿って移すことで、元の環境での所属が得られる。

```agda
        named : Σ[ j ∈ ℕ ] ((j < k) × (fst x ≡ # j))
              → Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
        named (j , (hj , q)) = relAt j
          , subst (λ t → ⟨ pr (fst x) (fst (relAt j)) ∈ t ⟩) (sym qf)
              (subst (λ t → ⟨ pr t (fst (relAt j)) ∈ fst (approxSet k) ⟩)
```

最後の移送で、読み出された数項 `# j` を元の第一成分へ戻す。これにより、意図された定義域の各要素に対応する項目が存在し、定義域条件の後半が完成する。

```agda
                (sym q) (approx-mem-in k j hj))
```

残るのは各点での再帰条件の確認である。有限表に現れる各順序対が `RelStepAt` を満たすことを示し、第二成分が第一成分における再帰で定まる関係の値であることを保証する。

```agda
    onStep : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
           → ⟨ (y ∷ x ∷ γ) ⊨ RelStepAt zero (suc zero) (sh2 f) ⟩
    onStep x y p = PT.rec (snd ((y ∷ x ∷ γ) ⊨ RelStepAt zero (suc zero) (sh2 f)))
      named
      (approx-mem-out k (pr (fst x) (fst y))
```

まず表への所属を `approxSet k` へ移し、`approx-mem-out` で読み取る。得られる標準形は命題的切り詰められているが、`RelStepAt` の充足は命題なので、この切り詰めを除去できる。

```agda
        (subst (λ t → ⟨ pr (fst x) (fst y) ∈ t ⟩) qf p))
      where
      named : Σ[ j ∈ ℕ ]
                ((j < k) × (pr (fst x) (fst y) ≡ pr (# j) (fst (relAt j))))
            → ⟨ (y ∷ x ∷ γ) ⊨ RelStepAt zero (suc zero) (sh2 f) ⟩
```

復元された第 `j` の項目について、`rel-step` が再帰の一歩を再構成する。各 `i < j` に必要な仮定は `approxSet k` の値の正しさと項目の完全性から得られ、`<` の推移性が `i < j < k` をそれらの補題に必要な境界へ変える。

```agda
      named (j , (hj , q)) =
        rel-step zero (suc zero) (sh2 f) (y ∷ x ∷ γ) j (pr-inj q .fst)
          (λ i hi u hu → approxVals k i (<-trans hi hj) u
            (subst (λ t → ⟨ pr (# i) (fst u) ∈ t ⟩) qf hu))
          (λ i hi → subst (λ t → ⟨ pr (# i) (fst (relAt i)) ∈ t ⟩) (sym qf)
```

順序対の等式の第一成分は引数を `# j` と同一視し、第二成分は表の値を `relAt j` と同一視する。これらがちょうど `rel-step` に必要な両端の等式である。

```agda
            (approxEnts k i (<-trans hi hj)))
          (pr-inj q .snd)
```

この具体的な有限表が `ApproxAt` を満たすことが分かった。`onDom` は定義域がちょうど `# k` であることを示し、`onStep` は記録された各引数で再帰条件を示す。この近似の構成には置換を用いていない。

```agda
  approxSet-approx : ⟨ γ ⊨ ApproxAt f a ⟩
  approxSet-approx = ApproxAt-in f a γ (domAt-intro f a γ onDom) onStep
```

したがって、環境内で添字と候補値を表す成分がそれぞれ `# k` と `relAt k` に同一視されるなら、`relAt k` は数項 `# k` における再帰グラフを満たす。存在量化された近似の証人は有限集合 `approxSet k` である。

```agda
relAt-graph : ∀ {n} (v b : Fin n) (γ : S ^ n) (k : ℕ)
            → fst (lookup b γ) ≡ # k → fst (lookup v γ) ≡ fst (relAt k)
            → ⟨ γ ⊨ RelGraphAt v b ⟩
relAt-graph v b γ k qb qv = RelGraph-in v b γ (approxSet k)
  (approxSet-approx k zero (suc b) (approxSet k ∷ γ) refl qb)
```

グラフの導入は二つの事実を組み合わせる。`approxSet-approx` がすべての小さい引数を検証し、`rel-step` が `approxVals` と `approxEnts` を用いて `k` における現在の値を検証する。このように、同じ有限表が `relAt k` の保証に必要な先行情報をちょうど与える。

```agda
  (rel-step (suc v) (suc b) zero (approxSet k ∷ γ) k qb
    (approxVals k) (approxEnts k) qv)
```

## 順序族を `L` の要素にする

ここまでで、各有限段階の関係は段階ごとに検証された。先の一意性の議論で用いたのは自然数の順序 `<` に関する整礎帰納であり、`before` の整礎性を示したり用いたりしたわけではない。次は内部自然数上で置換を用い、すべての `(# k, relAt k)` を一つの `L` に属する集合グラフへ集める。

```agda
private
```

対にした再帰グラフと等しいことが証明された任意の論理式 `φ` に対し、`famBuild` は二つの正確な性質をもつ構成可能集合 `h` を返す。各標準的な順序対は `h` に属し、第一成分が `# k` と分かっている `h` の任意の要素の第二成分は `relAt k` に等しい。

```agda
  famBuild : (φ : Formula S 2) → φ ≡ PairRelGraphAt zero (suc zero)
           → Σ[ h ∈ S ]
               ( ((k : ℕ) → ⟨ pr (# k) (fst (relAt k)) ∈ fst h ⟩)
               × ((cS rS : S) (k : ℕ) → fst cS ≡ # k
                  → ⟨ pr (fst cS) (fst rS) ∈ fst h ⟩ → fst rS ≡ fst (relAt k)) )
```

置換を使うには、各 `c ∈ ωʟ` 上で論理式を満たす出力のファイバーが可縮でなければならない。`ωʟ` への所属から得られる数項表示は命題的切り詰めだけである。`PT.map` が明示的な各数項の場合を処理し、`mereFunct` が切り詰められた存在と値の一意性を可縮性へまとめる。

```agda
  famBuild φ qφ = r .fst .fst , (inFam , outFam)
    where
    fc : (c : S) → ⟨ c ∈ˢ ωʟ ⟩
       → isContr (Σ[ y ∈ S ] ⟨ (y ∷ c ∷ []) ⊨ φ ⟩)
    fc c c∈ = mereFunct φ c (PT.map atK c∈)
```

明示的な数項の場合 `fst c = # j` では、ファイバーの中心として `c` と `relAt j` の構成可能な順序対を取る。その `φ` の充足と、`φ` を満たすほかのすべての出力がこの中心に等しいことを示すが、命題的切り詰めの外で標準的な `j` を選ぶわけではない。

```agda
      where
      atK : Σ[ j ∈ Lift ℕ ] (# (lower j) ≡ fst c)
          → Σ[ y ∈ S ] ( ⟨ (y ∷ c ∷ []) ⊨ φ ⟩
                       × ((y' : S) → ⟨ (y' ∷ c ∷ []) ⊨ φ ⟩ → y' ≡ y) )
      atK (j , qj) = prS c (relAt (lower j)) , (holds , only)
```

数項の読み出しから得られる等式は向きが逆である。それを反転すると `fst c = # j` となり、`j` に再帰グラフの定理を適用するために必要な形が得られる。

```agda
        where
        qc : fst c ≡ # (lower j)
        qc = sym qj
```

選んだ順序対が `φ` を満たすことを示すには、`φ` と対にしたグラフとの等式で主張を `PairRelGraphAt` に帰着する。順序対の構成が外側の対の等式を与え、`relAt-graph` が `relAt j` に対するグラフの主張を与える。

```agda
        holds : ⟨ (prS c (relAt (lower j)) ∷ c ∷ []) ⊨ φ ⟩
        holds = PairRelGraph-in zero (suc zero)
          (prS c (relAt (lower j)) ∷ c ∷ []) φ qφ (relAt (lower j))
          (prS-fst c (relAt (lower j)))
          (relAt-graph zero (sh2 zero)
```

グラフの主張を添字 `j` で具体化する。添字を表す成分は反転した読み出しの等式により `# j` と同一視され、候補の関係は定義により `relAt j` である。これでファイバーの存在部分が完成する。

```agda
            (relAt (lower j) ∷ prS c (relAt (lower j)) ∷ c ∷ [])
            (lower j) qc refl)
```

一意性のため、`φ` を満たす別の出力 `y'` を取る。対にしたグラフを読むと `y'` の命題的切り詰められた分解が得られる。`S` における等しさは命題なので、これを目標 `y' = prS c (relAt j)` へ除去できる。

```agda
        only : (y' : S) → ⟨ (y' ∷ c ∷ []) ⊨ φ ⟩ → y' ≡ prS c (relAt (lower j))
        only y' h = PT.rec (isSetS y' (prS c (relAt (lower j)))) read
          (PairRelGraph-out zero (suc zero) (y' ∷ c ∷ []) φ qφ h)
          where
          read : PairOf zero (suc zero) (y' ∷ c ∷ []) φ qφ
```

明示的な分解は `y'` を `c` とあるグラフ値 `z` の順序対として表す。定理 `rel-only` は `z` の台となる集合を `relAt j` と同一視し、`L` への所属証明を伴う要素の外延的等しさが、得られた順序対の等式を `S` へ持ち上げる。

```agda
               → y' ≡ prS c (relAt (lower j))
          read (z , (q , hg)) = Σ≡Prop (λ t → snd (isL t))
            ( q
            ∙ cong (pr (fst c))
                (rel-only zero (sh2 zero) (z ∷ y' ∷ c ∷ []) (lower j) qc hg)
```

最後の等式は、台となる順序対を構成可能な順序対 `prS c (relAt j)` と比較する。これにより、読み出した数項における集合値の一意性が示されるが、グラフの証人そのものの一意性を主張するものではない。

```agda
            ∙ sym (prS-fst c (relAt (lower j))) )
```

ここで `ωʟ` 上の置換により、ある `c ∈ ωʟ` が存在して `φ` を満たすという命題的切り詰めが成り立つ出力 `y` を、ちょうど要素とする構成可能集合の可縮な型を得る。可縮性は得られる集合を一意にするが、存在する数項のデータは命題的切り詰めのままである。

```agda
    r : isContr (SetOf (λ y → ∃[ c ∶ S ] (c ∈ˢ ωʟ) ⊓ ((y ∷ c ∷ []) ⊨ φ)))
    r = hasReplacementL ωʟ φ fc
```

各標準的な順序対は置換で得た集合に属する。置換の仕様に証人 `numS k` を与え、その `ωʟ` への所属と `relAt k` に対する対グラフの証明を添える。その後、包装された順序対を `V` における台の順序対へ移す。

```agda
    inFam : (k : ℕ) → ⟨ pr (# k) (fst (relAt k)) ∈ fst (r .fst .fst) ⟩
    inFam k = subst (λ t → ⟨ t ∈ fst (r .fst .fst) ⟩) qe
      (subst ⟨_⟩ (sym (r .fst .snd (prS (numS k) (relAt k))))
        ∣ numS k , (inω , holds) ∣₁)
      where
```

必要な移送の等式は包装だけを展開する。`prS (numS k) (relAt k)` の台となる集合は、`# k` と `relAt k` の台となる集合との順序対である。`numS k` の等式がその第一成分を与える。

```agda
      qe : fst (prS (numS k) (relAt k)) ≡ pr (# k) (fst (relAt k))
      qe = prS-fst (numS k) (relAt k)
         ∙ cong (λ t → pr t (fst (relAt k))) (numS-fst k)
```

証人 `numS k` の台となる集合は `# k` であり、各数項は `ω` に属するので、`numS k` は内部自然数に属する。`#∈ω k` を `numS-fst` に沿って移せば、必要な所属が得られる。

```agda
      inω : ⟨ numS k ∈ˢ ωʟ ⟩
      inω = subst (λ t → ⟨ t ∈ ω ⟩) (sym (numS-fst k)) (#∈ω k)
```

残る証人は、包装された標準的な順序対が `φ` を満たすことを示す。対グラフの導入により、目標は順序対の等式と、`relAt k` が `# k` における再帰グラフを満たすという事実へ帰着する。

```agda
      holds : ⟨ (prS (numS k) (relAt k) ∷ numS k ∷ []) ⊨ φ ⟩
      holds = PairRelGraph-in zero (suc zero)
        (prS (numS k) (relAt k) ∷ numS k ∷ []) φ qφ (relAt k)
        (prS-fst (numS k) (relAt k))
        (relAt-graph zero (sh2 zero)
```

再帰グラフの定理を `k` で直接具体化する。等式 `numS-fst k` が入力を `# k` と同一視し、反射律が候補の出力を `relAt k` と同一視することで、標準項目の証明が完成する。

```agda
          (relAt k ∷ prS (numS k) (relAt k) ∷ numS k ∷ []) k (numS-fst k) refl)
```

逆向きの仕様では、ある順序対が置換で得た集合に属し、その第一成分が `# k` と分かっていると仮定する。目標は第二成分が `relAt k` に等しいことだけであり、これは命題値の結論なので、置換の所属に含まれる命題的切り詰めをそこへ除去できる。

```agda
    outFam : (cS rS : S) (k : ℕ) → fst cS ≡ # k
           → ⟨ pr (fst cS) (fst rS) ∈ fst (r .fst .fst) ⟩
           → fst rS ≡ fst (relAt k)
    outFam cS rS k qc h =
      PT.rec (setIsSet (fst rS) (fst (relAt k))) atD
```

置換の仕様から、包装された入力の順序対が `d` 上で `φ` を満たすような内部自然数 `d` が、命題的切り詰められた形で得られる。ここでは数項を選ばない。後の順序対の等式が、`d` の台となる集合を、すでに指定された `# k` と同一視する。

```agda
        (subst ⟨_⟩ (r .fst .snd (prS cS rS))
          (subst (λ t → ⟨ t ∈ fst (r .fst .fst) ⟩) (sym (prS-fst cS rS)) h))
      where
      atD : Σ[ d ∈ S ] ( ⟨ d ∈ˢ ωʟ ⟩ × ⟨ (prS cS rS ∷ d ∷ []) ⊨ φ ⟩ )
          → fst rS ≡ fst (relAt k)
```

対にしたグラフを読むと、再び命題的切り詰めの下で、関係の値 `z`、包装された要素を順序対 `(d,z)` と同一視する等式、そして `z` が `d` における再帰グラフを満たす証明が得られる。集合の等しさは命題なので、この切り詰めも除去できる。

```agda
      atD (d , (d∈ , hp)) = PT.rec (setIsSet (fst rS) (fst (relAt k))) read
        (PairRelGraph-out zero (suc zero) (prS cS rS ∷ d ∷ []) φ qφ hp)
        where
        read : PairOf zero (suc zero) (prS cS rS ∷ d ∷ []) φ qφ
             → fst rS ≡ fst (relAt k)
```

包装の等式を取り除くと、順序対の単射性により、与えられた第二成分が `z` と同一視される。第一成分の等式からグラフの添字が `# k` と分かれば、定理 `rel-only` がさらに `z` を `relAt k` と同一視する。

```agda
        read (z , (q , hg)) = pr-inj q' .snd
          ∙ rel-only zero (sh2 zero) (z ∷ prS cS rS ∷ d ∷ []) k qd hg
          where
          q' : pr (fst cS) (fst rS) ≡ pr (fst d) (fst z)
          q' = sym (prS-fst cS rS) ∙ q
```

必要な添字の等式は、同じ順序対の等式の第一成分から従う。その成分を反転すると `d` が元の第一成分と同一視され、さらにその第一成分についての仮定と合成して `fst d = # k` を得る。

```agda
          qd : fst d ≡ # k
          qd = sym (pr-inj q' .fst) ∙ qc
```

実際の対にした再帰グラフを `famBuild` に与えて得る構成可能集合を `beforeFam` と名付け、不透明に保つ。直後の仕様補題が、すべての標準項目と、既知の各数項における集合値の一意性を公開する。この構成が与えるのは内部の関係族であり、まだ名前の比較も最終的な整列順序の証明も行っていない。

```agda
opaque
  beforeFam : S
  beforeFam = famBuild (PairRelGraphAt zero (suc zero)) refl .fst
```

各自然数 `k` について、内部グラフ `beforeFam` は、数項 `# k` と実現された関係 `relAt k` の順序対を含みます。これはこの族への正向きの所属則です。すでに与えられた数項と関係を直接書き込むので、命題的切り詰めから数項の復号の証人を選ぶ必要はありません。

```agda
  beforeFam-in : (k : ℕ) → ⟨ pr (# k) (fst (relAt k)) ∈ fst beforeFam ⟩
  beforeFam-in = famBuild (PairRelGraphAt zero (suc zero)) refl .snd .fst
```

逆に、`beforeFam` のある項の第一成分が `# k` に等しいとします。このとき、その第二成分の台となる集合は `relAt k` の台となる集合に等しくなります。したがって、指定された数項でのグラフの集合値は一意です。しかし、これは標準的な復号の証人を与えるものでも、構成に含まれるすべての証明の一意性を主張するものでもありません。

```agda
  beforeFam-out : (cS rS : S) (k : ℕ) → fst cS ≡ # k
                → ⟨ pr (fst cS) (fst rS) ∈ fst beforeFam ⟩
                → fst rS ≡ fst (relAt k)
  beforeFam-out = famBuild (PairRelGraphAt zero (suc zero)) refl .snd .snd
```

## スロット内の数項における順序

論理式 `BeforeAt b x y` は、二段の主張によって関係 `r` を求めます。まず `appC` が、定数である族 `beforeFam` は `b` が指す値に `r` を割り当てると述べます。次に `appAt` が、`r` は `x` と `y` の指す対象の順序対を含むと述べます。続く定理では、`b` における値が数項 `# m` であると仮定し、以下に明記する段階所属の仮定のもとで、この内部の主張を `before m` と同定します。

```agda
opaque
  BeforeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
  BeforeAt b x y =
    ∃̇ ( appC beforeFam (suc b) zero ∧̇ appAt zero (suc x) (suc y) )
```

環境と自然数 `m` を固定します。`b` についての等式は、その値が数項 `# m` であることを述べ、二つの所属の仮定は `x` と `y` が指す値を `finiteStage m` に置きます。これらの仮定によって三つの変数が一つの有限段階での比較に結びつき、妥当性定理はこの制限された文脈でのみ述べられます。

```agda
module _ {n : ℕ} (b x y : Fin n) (γ : S ^ n) (m : ℕ)
         (qb : fst (lookup b γ) ≡ # m)
         (hx : ⟨ fst (lookup x γ) ∈ finiteStage m ⟩)
         (hy : ⟨ fst (lookup y γ) ∈ finiteStage m ⟩) where
  private
```

意味論的な目標は、`before m` によって `x` の指す値が `y` の指す値に先行するという、メタレベルの命題です。ここで示すのは一つの有限段階での比較の表現であり、整礎性について新たな主張をするものではありません。

```agda
    Goal : Type (ℓ-suc ℓ)
    Goal = ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩
```

充足する付値を読み出すため、存在量化が隠しているデータを一時的に明示します。それは、関係 `r`、族が `b` で `r` を値に取ることの証拠、そして `r` が `x,y` での順序対を含むことの証拠です。この型は明示的な組を記述しますが、存在量化の意味論がそれを与えるのは命題的切り詰めのもとだけなので、保持可能な証人や標準的な証人は得られません。

```agda
    AtR : Type (ℓ-suc ℓ)
    AtR = Σ[ r ∈ S ]
      ( ⟨ (r ∷ γ) ⊨ appC beforeFam (suc b) zero ⟩
      × ⟨ (r ∷ γ) ⊨ appAt zero (suc x) (suc y) ⟩ )
```

この形の明示的な組から、二つの適用の妥当性則によって、論理式の充足を通常の集合所属へ読み替えます。族についての法則は `r` の台となる集合を `relAt m` の台となる集合と同一視します。この等式に沿って順序対の所属を移送すると、`relAt-rep` がそれを `before m` へ読み戻します。最後の表現の段階で、先の二つの有限段階への所属の仮定がちょうど必要になります。

```agda
    atR : AtR → Goal
    atR (r , (happ , hmem)) =
      relAt-rep m (fst (lookup x γ)) (fst (lookup y γ)) hx hy
        (subst (λ t → ⟨ pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ t ⟩) qr
          (subst ⟨_⟩ (appAt-adequate zero (suc x) (suc y) (r ∷ γ)) hmem))
```

第一の適用の事実は、`beforeFam` が `b` に格納された項で値 `r` を取ることを内部的に述べています。その妥当性則により、当該の項と `r` の順序対が `beforeFam` に属するという外部の所属命題へ移ります。

```agda
      where
      hf : ⟨ pr (fst (lookup b γ)) (fst r) ∈ fst beforeFam ⟩
      hf = subst ⟨_⟩ (appC-adequate beforeFam (suc b) zero (r ∷ γ)) happ
```

`b` での項が `# m` に等しいと分かっているので、族の逆向きの法則は `r` の台となる集合を `relAt m` の台となる集合と同一視します。ここで使うのは、指定された数項での集合値の一意性であって、数項の復号を大域的に選択することではありません。

```agda
      qr : fst r ≡ fst (relAt m)
      qr = beforeFam-out (lookup b γ) r m qb hf
```

これで、正確な意味論的対応の二方向を証明できます。`BeforeAt` を局所的に展開すると、一つの存在量化と二つの適用の事実が現れますが、`b`、`x`、`y` についての仮定は両方の主張に引き続き含まれています。

```agda
  opaque
    unfolding BeforeAt
```

外向きの方向では、存在量化の充足から得られるのは、命題的切り詰めを受けた関係の組だけです。証明は、仮に明示された各組へ上の変換を適用することで、その切り詰めを命題である `Goal` へ直接消去します。中間の型の要素をデータとして取り出して保持することはありません。

```agda
    BeforeAt-out : ⟨ γ ⊨ BeforeAt b x y ⟩
                 → ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩
    BeforeAt-out h =
      PT.rec (snd (before m (fst (lookup x γ)) (fst (lookup y γ)))) atR h
```

内向きの方向では、`before m` の証明から論理式に必要な関係所属が得られます。適切な関係として `relAt m` を提示し、二つの適用の事実を証明した後、存在量化の意味論に従って組全体を命題的切り詰めの中に入れます。これはこの方向のために構成した証人であり、切り詰めから復元した標準的な証人ではありません。

```agda
    BeforeAt-in : ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩
                → ⟨ γ ⊨ BeforeAt b x y ⟩
    BeforeAt-in h = ∣ relAt m , (happ , hmem) ∣₁
      where
      happ : ⟨ (relAt m ∷ γ) ⊨ appC beforeFam (suc b) zero ⟩
```

族への適用は、`beforeFam` に既知の項 `(# m, relAt m)` があることから従います。その第一成分を `b` についての等式に沿って移送し、適用の妥当性を逆向きに使うと、必要な内部の適用事実が得られます。

```agda
      happ = subst ⟨_⟩
        (sym (appC-adequate beforeFam (suc b) zero (relAt m ∷ γ)))
        (subst (λ t → ⟨ pr t (fst (relAt m)) ∈ fst beforeFam ⟩) (sym qb)
          (beforeFam-in m))
```

第二の適用の事実は `relAt-fill` から得られます。二つの有限段階への所属の仮定と、仮定された `before m` の比較により、`x,y` での値の順序対が `relAt m` に属します。適用の妥当性を逆向きに読むことで、この所属を `appAt` の充足へ変えます。

```agda
      hmem : ⟨ (relAt m ∷ γ) ⊨ appAt zero (suc x) (suc y) ⟩
      hmem = subst ⟨_⟩
        (sym (appAt-adequate zero (suc x) (suc y) (relAt m ∷ γ)))
        (relAt-fill m (fst (lookup x γ)) (fst (lookup y γ)) hx hy h)
```

## フレームの仮定を解消する

二つの妥当性の方向により、`BeforeAt` は先の `Described` の枠組みへの入力になります。その枠組みは、まず二つの極限段階のコードが属する有限段階の番号を比較し、番号が等しいときには、この章で表現した段階内の `before` 関係を用います。さらに分出公理によって、この比較を内部関係 `codeOrder` として実現します。この具体化が与えるのはコード順序の部分であり、まだ名前を比較せず、最終的な内部整列順序も証明しません。

```agda
private
  module CodeOrder = Described BeforeAt BeforeAt-in BeforeAt-out
```

ここで得られるのは、関係集合 `codeOrder` と二つの表現則です。`codeOrder-fill` はメタレベルの `limitOrder` の比較をこの集合への所属に変え、`codeOrder-rep` はその所属を読み戻します。後の名前比較では、この三つの結果をコードの比較に使い、パラメータの比較関係は別に与えます。

```agda
open CodeOrder public using ( codeOrder; codeOrder-fill; codeOrder-rep )
```

## まとめ

各自然数 `n` について、`L` 内の集合 `relAt n` は `finiteStage n` の要素上で `before n` を表します。再帰グラフがこれらの値を検証し、置換公理を使うのは最後に `ωʟ` に沿って族全体を `beforeFam` へ集めるときだけです。有限近似には `finSet` と `finSetL` を使います。`b` が `# m` を指し、`x,y` の指す値が `finiteStage m` に属するなら、`BeforeAt b x y` はそれら二つの値を `before m` で比較することと同値です。`Described` を具体化して得られる `codeOrder`、`codeOrder-fill`、`codeOrder-rep` は後でコードの比較を与えますが、本章はまだ名前を比較せず、最終的な内部整列順序も証明しません。