---
title: "段階順序の内部の表"
module: L.Choice.OrderTable
lang: ja
site: "Bedrock"
description: "段階順序の内部の表"
stage: "正準整列順序と選択公理"
reading_order: 78
canonical: https://bedrock.institute/ja/L.Choice.OrderTable.html
html: L.Choice.OrderTable.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/OrderTable.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, FOL.ZFModel, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Full, L.Recursion, L.Coding.Model, L.Coding.Expressions, L.Coding.HierarchySequence, L.Choice.StageOrders, L.WellOrder.Base]
routes: [choice-completion]
translations: [https://bedrock.institute/en/L.Choice.OrderTable.md, https://bedrock.institute/zh/L.Choice.OrderTable.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 段階順序の内部の表

構成可能な順序数の段階添字 `α` では、先の構成によって `Lset α` の要素上のホスト側の狭義整列順序がすでに得られています。本章の目的は、その二項比較を `L` の内部の集合として表現し、モデルで解釈される論理式がその関係を量化できるようにすることです。結果は、一段階の再帰について妥当な対象言語の記述が与えられることを前提とし、`α` が順序数かつ構成可能である場合に適用されます。ここで表現するのは既存の順序の基礎となる関係であり、この関係が整列順序であるという対象言語の主張はまだ与えません。

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

この章で用いる古典的仮定は、構成が置かれる宇宙レベルでの排中律だけです。先に得た段階順序がすでにこれを必要とし、後で用いる置換と分出もこれから得られます。切り詰め、輸送、外延的な一意性についての局所的な議論が、別の古典的仮定を加えることはありません。

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

モジュールの境界で `lem : LEM (ℓ-suc ℓ)` を固定することで、この依存は一貫したものになります。したがって以下の構成はすべて、同じレベルつきの仮定を受け継ぎ、任意の大きさでの排中律を暗黙に用いることはありません。

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

ここでは二つの議論の水準を区別する必要があります。表現される関係はホストの型理論で定義され、その再帰的な記述は `L` で解釈される一階論理式です。所属に沿う帰納が各段階を結びます。その動機は任意の依存型族に値を取れるので、後で表と関係を同時に運ぶ組が命題であることは、再帰の正当性の前提ではありません。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction )
```

最終的な関係は構成可能モデルの中にありますが、その端点はまずホスト集合 `Lset α` の要素として現れます。順序数性 `oα` を固定すると、`Lset→isL` によって各端点をモデル要素としてまとめられます。この変換が使うのは `α` の順序数性であり、`α` 自身が構成可能であるという別の証明ではありません。`α` の構成可能性の証人は、後で異なる役割を果たします。段階の添字自身をモデル要素 `A` としてまとめ、置換公理の定義域と分出公理のパラメータにするためです。順序数の要素に関する法則が小さい添字の順序数性を与え、対の符号化の単射性と外延性が、それぞれ端点の復元と要素による集合の同一視を与えます。

```agda
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd; isPropIsOrd )
open import L.Ordinal {ℓ} using ( mem-ord )
open import L.Axioms.Basic {ℓ} using ( extensionalL )
```

この構成では、二つの集合存在原理を異なる目的に用います。命題的切り詰めのもとの存在と外延的な一意性によって各グラフの繊維を可縮にした後、置換がすべての小さい添字での関係の値を一つの表に集めます。分出は一つの共通の包含集合から現在の関係を切り出します。したがって、上界より下の表と上界での関係は同時に作られますが、その存在を与える議論は別々です。

```agda
open import L.Axioms.Full {ℓ} lem using ( hasReplacementL; hasSeparationL )
open import L.Recursion {ℓ} lem using ( mereFunct; smallDom )
open import L.Coding.Model {ℓ} using ( domAt-intro; prʟ; prʟ-fst )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-in; extAt-out; extAt-in-both )
open import L.Coding.HierarchySequence {ℓ} lem using ( module RecShape )
```

順序そのものは、`Mem (Lset α)` 上の狭義整列順序 `orderAt α oα` としてすでに得られています。本章ではその基礎となる比較、三分性、非反射性、推移性を用い、後には同じ順序を段階の小さな提示へ運びます。新しい比較規則や整礎性の証明をここで導入することはありません。

```agda
open import L.Choice.StageOrders {ℓ} lem using ( Mem; relOf; orderAt; memOf; carry )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; Tri; lt; eq; gt )
```

後で現れる多くの等式は、第二成分が所属の証明である依存対を比較します。所属と順序数性は命題なので、底の集合の等しさからまとめられた要素の等しさが定まり、証明書を取り替えても別の数学的端点は生じません。そのため、対の成分の等式に沿って比較を輸送しても、証明を余分な選択に変えることはありません。

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop; _×_ )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
```

命題的切り詰めは、証人を選ばず存在だけを必要とするすべての箇所を示します。小さな提示の役割は別です。大きいかもしれない所属の繊維を小さな添字型で提示し、その埋め込みから表される要素を返します。一方は選択を隠し、他方は大きさを制御するので、この二つを区別することが大切です。

```agda
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
  using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber )
```

ここから先、命題と量化は `L` の所属構造で読みます。したがって、モデルの要素があるクラスを実現するという主張は、その要素の所属についての命題として表され、メタ理論の内包によって別の外部集合を作ることではありません。

```agda
open hPropStructure 𝒮ʟ
```

後で用いる内部の集合記法は、候補の集合が、ある論理式を満たす対象をちょうど要素にもつことを述べます。これは集合の外延的な仕様であり、集合の存在そのものは、再帰の適切な箇所で置換または分出から得なければなりません。

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

論理式の充足は、絶対性を通してホスト側の述語と比較されます。論理式そのものが `orderAt` を含むのではありません。妥当性の等式が、その解釈された真理値を、符号化された比較対からなるホスト側のクラスと同一視します。

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

以下の論理式は、既存の環境の外側に二つの新しい束縛を導入します。この非公開のずらしは、古い各変数の添字を二つの束縛の先へ移して意味を保ちます。これにより、値、添字、表という数学的な役割が、拡張された環境でも変わりません。

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

## 比較を切り詰めから取り戻す

モデルのクラスは命題に値を取る必要がありますが、`relOf (orderAt α oα) a b` の証人が一意であるとは証明されていません。そこで `Ordering` は、その証人の命題的切り詰めだけを保ちます。これにより比較はクラスの所属に適した論理的な形になり、比較が証人をもつかどうかは保たれます。

```agda
Ordering : (α : V ℓ) → IsOrd α → Mem (Lset α) → Mem (Lset α) → hProp (ℓ-suc ℓ)
Ordering α oα a b = ∥ relOf (orderAt α oα) a b ∥₁ , squash₁
```

この特定の比較については、後で切り詰めを除去できます。その理由は、すでに構成された狭義順序の三分性です。`a` と `b` が順方向に関係する場合、等しい場合、逆方向に関係する場合に分けると、後の二つは切り詰められた順方向の比較と矛盾します。これは狭義全順序の比較に固有の性質であり、命題的切り詰め一般から証人を取り出す方法ではありません。

```agda
strict : (α : V ℓ) (oα : IsOrd α) (a b : Mem (Lset α))
       → ⟨ Ordering α oα a b ⟩ → relOf (orderAt α oα) a b
strict α oα a b h = decide (SWO.tri∙ W a b)
  where
  W = orderAt α oα
```

順方向の分岐では、三分性が必要な切り詰められていない証人をすでに与えるので、切り詰められた仮定を開く必要はありません。等しい分岐では、その証人を空の型へだけ除去します。`a ≡ b` に沿って輸送すれば `a` が自分自身に先行することになり、非反射性に反するからです。必要な結果は、この矛盾から得られます。

```agda
  decide : Tri (relOf W a b) (a ≡ b) (relOf W b a) → relOf W a b
  decide (lt k) = k
  decide (eq q) = Empty.rec (PT.rec Empty.isProp⊥
    (λ k → SWO.irr∙ W a (subst (relOf W a) (sym q) k)) h)
  decide (gt k) = Empty.rec (PT.rec Empty.isProp⊥
```

逆方向の分岐では、仮に順方向の証人があれば、それを逆方向の比較と推移性で合成することで、やはり `a` が自分自身に先行してしまいます。ここでも切り詰めを開くのは、この矛盾を示すためだけです。したがって `strict` は比較の証人を返しますが、比較の証人の型が命題であることや、優先される証明を選ぶことは示しません。

```agda
    (λ j → SWO.irr∙ W a (SWO.trans∙ W a b a j k)) h)
```

## 段階における関係

添字 `α` に対して `Related α z` は、命題的切り詰めのもとで、`z` が `Lset α` の二つの要素の Kuratowski 対であり、その二要素が段階順序で関係づけられていることを述べます。順序数性の証明書はクラスの内側で量化されるので、このクラスは `α` が順序数であるという選ばれた証明に依存しません。端点の分解と比較の証人は、それぞれの切り詰めの境界内にとどまります。

```agda
Related : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Related α z = ∃[ oα ∶ IsOrd α ] (∃[ a ∶ Mem (Lset α) ] (∃[ b ∶ Mem (Lset α) ]
  ((z ≡ pr (fst a) (fst b)) , setIsSet z (pr (fst a) (fst b))) ⊓ Ordering α oα a b))
```

モデルの集合 `r` がこのクラスを実現するとは、すべてのモデル要素 `z` について、`r` への所属と `Related α` が双方向に一致することです。外向きの含意は無関係な要素や形の違う要素を排除し、内向きの含意は関係するすべての対を含めます。構成可能性は推移的であり、構成可能な集合の各要素もモデルの要素としてまとめられるので、ここではモデル要素だけを量化すれば十分です。

```agda
Realizes : V ℓ → S → hProp (ℓ-suc ℓ)
Realizes α r = ∀[ z ∶ S ] ((fst z ∈ fst r) ⇒ Related α (fst z))
                        ⊓ (Related α (fst z) ⇒ (fst z ∈ fst r))
```

`IsRel α r` は、この正確な所属仕様の証拠の型です。これは `r` がホスト側で定義されたクラスを実現することを述べるだけで、`r` に狭義順序の構造を加えず、関係が対象言語の整列順序の論理式を満たすとも主張しません。

```agda
IsRel : V ℓ → S → Type (ℓ-suc ℓ)
IsRel α r = ⟨ Realizes α r ⟩
```

実現の証明に含まれる二つの含意は、「`z` が `r` に属する」という命題と「`z` が `α` で関係する」という命題の間のパスを定めます。この点ごとのパスが、任意の実現集合への所属と意味論的なクラスを交換するときの書き換え原理になります。

```agda
rel-path : (α : V ℓ) (r : S) → IsRel α r
         → (z : S) → (fst z ∈ fst r) ≡ Related α (fst z)
rel-path α r p z =
  ⇔toPath {P = fst z ∈ fst r} {Q = Related α (fst z)} (p z .fst) (p z .snd)
```

`r` と `r'` がともにこのクラスを実現するなら、両者の所属命題は点ごとに一致し、`L` の外延性が二つの集合を同一視します。ここで示す一意性は実現集合の一意性です。`Related` の中で切り詰められた順序数性の証明書、端点の分解、比較の証人が一意に選ばれることを意味しません。

```agda
rel-unique : (α : V ℓ) (r r' : S) → IsRel α r → IsRel α r' → r ≡ r'
rel-unique α r r' p q = extensionalL
  (λ z → rel-path α r p z ∙ sym (rel-path α r' q z))
```

順方向の読みは、指定された要素 `a,b` と実際の段階順序の比較から始まります。二つの底の集合が符号化された対を作り、順序数性の証明書、まとめられた二要素、切り詰められた比較が `Related` の証人を与えます。証人は切り詰めの内側で構成されるので、切り詰められた情報から選択を取り出してはいません。

```agda
module _ (α : V ℓ) (oα : IsOrd α) (a b : Mem (Lset α)) where
  related-in : relOf (orderAt α oα) a b → ⟨ Related α (pr (fst a) (fst b)) ⟩
  related-in h = ∣ oα , ∣ a , ∣ b , (refl , ∣ h ∣₁) ∣₁ ∣₁ ∣₁
```

逆方向の読みは、意図的に狭い形をしています。入力の対象はすでに固定された端点 `a,b` の符号化された対として提示されています。この提示があるからこそ、存在的に表された対を二つの端点と比較し、その段階順序の比較を復元できます。任意の関係する対象を、選ばれた端点の対へ分解するものではありません。

```agda
  related-out : ⟨ Related α (pr (fst a) (fst b)) ⟩ → relOf (orderAt α oα) a b
  related-out h = strict α oα a b (PT.rec squash₁ atOrd h)
    where
    atPair : (o : IsOrd α) (a' b' : Mem (Lset α))
           → (pr (fst a) (fst b) ≡ pr (fst a') (fst b'))
```

切り詰められた記録が端点 `a',b'` と順序数性の証明 `o` を与えるとします。二つの符号化された対の等しさから `a` と `a'`、`b` と `b'` がそれぞれ同一視され、順序数性が命題であることから `o` と固定された証明 `oα` が同一視されます。この三つの同一視に沿って記録された比較を輸送すると、固定された端点での切り詰められた比較が得られます。

```agda
           → ⟨ Ordering α o a' b' ⟩ → ⟨ Ordering α oα a b ⟩
    atPair o a' b' q = PT.map
      (λ k → subst2 (relOf (orderAt α oα)) (sym ea) (sym eb)
        (subst (λ o' → relOf (orderAt α o') a' b') (isPropIsOrd α o oα) k))
      where
```

対の符号化の単射性は、まず底にある端点の集合の等しさを復元します。各端点は、集合とそれが `Lset α` に属する証明からなる依存対です。その証明は命題なので、第一成分の等しさは要素全体の等しさへ持ち上がります。これにより、比較を正しい依存型の中で輸送できます。

```agda
      ea : a ≡ a'
      ea = Σ≡Prop (λ x → snd (x ∈ Lset α)) (pr-inj q .fst)
      eb : b ≡ b'
      eb = Σ≡Prop (λ x → snd (x ∈ Lset α)) (pr-inj q .snd)
```

外側の順序数性の証明書は明示されていますが、各端点は命題的切り詰めのもとでしか存在しません。そこで切り詰めを一層ずつ、命題 `Ordering α oα a b` へ除去します。この目標の中では一時的な代表を使えますが、どちらの端点も選ばれたデータとして外へ出ることはありません。

```agda
    atOrd : Σ[ o ∈ IsOrd α ] ⟨ ∃[ a' ∶ Mem (Lset α) ] (∃[ b' ∶ Mem (Lset α) ] ((pr (fst a) (fst b) ≡ pr (fst a') (fst b'))
                 , setIsSet _ (pr (fst a') (fst b'))) ⊓ Ordering α o a' b') ⟩
          → ⟨ Ordering α oα a b ⟩
    atOrd (o , h₁) = PT.rec squash₁
      (λ { (a' , h₂) → PT.rec squash₁
```

二つの一時的な端点を開いた後、対を整列する議論が `a,b` での切り詰められた比較を与え、`strict` がその特定の比較から必要な証人を復元します。この合成によって逆方向の読みが得られますが、三分性で正当化された比較の証人を除き、存在に関する切り詰めの境界はすべて保たれます。

```agda
        (λ { (b' , (q , hr)) → atPair o a' b' q hr }) h₂ }) h₁
```

## クラスを実現する任意の集合を二つの形で読む

有用な表現補題は、再帰が最後に構成する関係だけでなく、`Related α` を実現する任意の `r` について述べられます。これにより、小さい段階の表にすでに記録された関係の値を直ちに読めます。順序数性の証明 `oα` を固定すると、`Lset α` の各要素は構成可能であり、モデルの要素としてまとめられます。

```agda
module _ (α : V ℓ) (oα : IsOrd α) (r : S) (hr : IsRel α r) where
  private
    memL : Mem (Lset α) → S
    memL c = fst c , Lset→isL α oα (fst c) (snd c)
```

まとめられた端点からモデル内部で作る順序対と、その底の集合からホスト側で作る Kuratowski 対は命題的に等しいですが、定義的に同じものとは扱いません。この等しさに「`r` に属する」を作用させると、最初の輸送の橋が得られます。

```agda
    atRel : (a b : Mem (Lset α))
          → (fst (prʟ (memL a) (memL b)) ∈ fst r)
          ≡ (pr (fst a) (fst b) ∈ fst r)
    atRel a b = cong (λ x → x ∈ fst r) (prʟ-fst (memL a) (memL b))
```

同じ対の等しさに `Related α` を作用させると、意味論の側のもう一つの橋が得られます。二つの橋を合わせることで、内部の順序対に実現の証明を使い、その結果を底の集合の素の対について述べ直せます。逆向きにも同様です。

```agda
    atRelated : (a b : Mem (Lset α))
              → ⟨ Related α (fst (prʟ (memL a) (memL b))) ⟩
              ≡ ⟨ Related α (pr (fst a) (fst b)) ⟩
    atRelated a b = cong (λ x → ⟨ Related α x ⟩) (prʟ-fst (memL a) (memL b))
```

埋める向きは、二つの要素のホスト側の比較から始まります。`Related` の順方向の読みがそれを符号化された対の関係へ変え、実現の証明が関係を `r` への所属へ変え、対の橋が主張をホスト側の対へ戻します。したがって、`orderAt` で比較されるすべての対は、任意の実現集合に属します。

```agda
  rel-fill : (a b : Mem (Lset α)) → relOf (orderAt α oα) a b
           → ⟨ pr (fst a) (fst b) ∈ fst r ⟩
  rel-fill a b h = subst ⟨_⟩ (atRel a b)
    (hr (prʟ (memL a) (memL b)) .snd
      (transport (sym (atRelated a b)) (related-in α oα a b h)))
```

読む向きは同じ経路を逆にたどります。ホスト側の対の所属を内部の対の所属へ輸送し、実現の証明を外向きに読んで `Related` の事実を得て、固定されたホスト側の対へ戻します。最後に `related-out` が、切り詰められていない段階順序の比較を返します。

```agda
  rel-rep : (a b : Mem (Lset α))
          → ⟨ pr (fst a) (fst b) ∈ fst r ⟩ → relOf (orderAt α oα) a b
  rel-rep a b h = related-out α oα a b
    (transport (atRelated a b)
      (hr (prʟ (memL a) (memL b)) .fst (subst ⟨_⟩ (sym (atRel a b)) h)))
```

後の議論には、依存的な要素の対ではなく、小さな提示 `⟪ Lset α ⟫` を用いるものがあります。その提示の添字は底の集合へ埋め込まれ、`Mem (Lset α)` の要素を作るために必要な所属の証明を備えています。

```agda
  private
    atIx : ⟪ Lset α ⟫ → Mem (Lset α)
    atIx m = ⟪ Lset α ⟫↪ m , memOf (Lset α) m
```

この提示に沿って `orderAt` を運ぶと、小さな添字型上の狭義順序が得られます。これは埋め込みを通して見た同じ比較なので、対応する表現定理に新たな順序論の議論は必要ありません。

```agda
  open SWO (carry (Lset α) (orderAt α oα)) using () renaming ( _<∙_ to _≺ᶜ_ )
```

提示の添字 `u,v` について、運ばれた比較は、まず対応する段階要素の比較として読まれます。先の埋める定理が、埋め込まれた端点の Kuratowski 対を `r` に入れます。これが、比較から所属へ向かう小さい添字での形です。

```agda
  ixRel-fill : (u v : ⟪ Lset α ⟫) → u ≺ᶜ v
             → ⟨ pr (⟪ Lset α ⟫↪ u) (⟪ Lset α ⟫↪ v) ∈ fst r ⟩
  ixRel-fill u v = rel-fill (atIx u) (atIx v)
```

逆に、埋め込まれた端点の対が `r` に属するなら、先の定理によって対応する段階要素の比較として読めます。運ばれた順序の定義から、これは小さな提示における `u` と `v` の狭義比較そのものです。

```agda
  ixRel-rep : (u v : ⟪ Lset α ⟫)
            → ⟨ pr (⟪ Lset α ⟫↪ u) (⟪ Lset α ⟫↪ v) ∈ fst r ⟩ → u ≺ᶜ v
  ixRel-rep u v = rel-rep (atIx u) (atIx v)
```

## 表が記録するもの

最初の表の条件は、記録された値の健全性です。添字 `c` が `B` より下にあり、符号化された項目 `(c,r)` が `h` に属するなら、`r` は `Related c` を実現しなければなりません。この条件は第一成分が `B` の外にある項目について何も述べないので、それだけでは表の定義域を特徴づけられません。

```agda
Values : S → V ℓ → Type (ℓ-suc ℓ)
Values h B = (c r : S) → ⟨ fst c ∈ B ⟩
           → ⟨ pr (fst c) (fst r) ∈ fst h ⟩ → IsRel (fst c) r
```

第二の条件は、上界より下で全域であることです。各 `c ∈ B` には記録された値 `r` が何か存在しますが、その存在には命題的切り詰めが施されています。したがって `Entries` は命題的なステップの議論に必要な情報だけを与え、各添字で一つの値を選ぶ大域的な関数は与えません。

```agda
Entries : S → V ℓ → Type (ℓ-suc ℓ)
Entries h B = (c : S) → ⟨ fst c ∈ B ⟩
            → ∥ (Σ[ r ∈ S ] ⟨ pr (fst c) (fst r) ∈ fst h ⟩) ∥₁
```

第三の条件は上界の外の項目を排除します。`h` に属するすべての符号化された対の第一成分が `B` に属します。これを `Entries` と合わせると、完成した表から近似を組み立て直すために必要な正確な定義域が得られます。記録された値の健全性を順方向に示す証明には最初の二条件だけが必要なので、`Domain` は分けておきます。

```agda
Domain : S → V ℓ → Type (ℓ-suc ℓ)
Domain h B = (c r : S) → ⟨ pr (fst c) (fst r) ∈ fst h ⟩ → ⟨ fst c ∈ B ⟩
```

## ステップをパラメータとする

再帰的な構成はここで、同じ意味をもつ二つの論理式を仮定します。`Cond b f` は、近似の表がグラフの内部で束縛されるときに用いる変数スロットの形です。`Cond₀ B F` は、固定された順序数と完成した表を分出のパラメータにするときに用いる定数の形です。最初の妥当性の等式は、順序数性と `Values`、`Entries` を仮定し、調べる各対象について変数形式の充足を対応する `Related` と同一視します。

```agda
module Described
  (Cond : ∀ {n} → Fin n → Fin n → Formula S (suc n))
  (Cond₀ : S → S → Formula S 1)
  (cond-spec : ∀ {n} (b f : Fin n) (γ : S ^ n) → IsOrd (fst (lookup b γ))
             → Values (lookup f γ) (fst (lookup b γ))
```

変数形式の仮定は点ごとであり、実際に双方向です。論理式を満たす符号化対象を関係する対として読む向きと、関係することから充足を構成する向きの両方を含みます。必要なのは、順序数より下の項目の正しさと、命題的切り詰めのもとの存在だけです。ここでは正確な定義域を仮定しないので、上界の外にありうる項目はこの意味論的な同一視に関与しません。

```agda
             → Entries (lookup f γ) (fst (lookup b γ))
             → (z : S)
             → ((z ∷ γ) ⊨ Cond b f) ≡ Related (fst (lookup b γ)) (fst z))
  (cond₀-spec : (b f : S) → IsOrd (fst b)
              → Values f (fst b) → Entries f (fst b)
```

順序数と表が固定されたモデル要素になった後、定数形式の等式が同じ点ごとの同値を与えます。分出で用いる定義論理式は、関係の要素の候補のために一つだけ自由スロットを残すので、この第二の提示が必要です。この等式は二つの文脈の意味を同一視しますが、`Cond` と `Cond₀` が構文的に等しいとは主張しません。

```agda
              → (z : S) → ((z ∷ []) ⊨ Cond₀ b f) ≡ Related (fst b) (fst z))
  where
```

変数形式の条件を与えると、`StepAt v b f` は候補の値を外延的に指定します。ある対象がスロット `v` の値に属することと、`Cond b f` を満たすことがちょうど一致します。これは双方向の所属仕様であり、存在定理ではありません。この仕様を実現する実際の集合は、後の再帰で置換と分出を用いて作られます。

```agda
  StepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
  StepAt v b f = extAt v (Cond b f)
```

候補の値、順序数の添字、小さい段階の表の三つのスロットを固定し、順序数性、値の健全性、命題的切り詰めのもとの項目の存在を満たす環境を与えます。これらの仮定のもとで、妥当性の等式は条件に共通の点ごとの意味を与えます。続く二つの読みはこれを逆向きに用います。外延的なステップ仕様から候補の値についての `IsRel` の証明を得る向きと、すでにある `IsRel` の証明からその仕様を満たす向きです。後の章で具体的な実例が与えられるまでは、構成全体がこの仮定されたステップ記述に相対したままです。

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

順序数の上界、正しい表、各小さい引数での要素を固定すると、条件の変数形式には正確な数学的意味が与えられます。ある集合がこの条件を満たすことと、その段階の順序が関係づける順序対の一つであることは同値です。この同値が、対象言語の一段階とホスト側の関係を結ぶ意味論的な橋になります。

```agda
      same : (z : S) → ((z ∷ γ) ⊨ Cond b f) ≡ Related (fst (lookup b γ)) (fst z)
      same = cond-spec b f γ ob vals ents
```

候補の値が外延的な一段階を満たすとします。その値への所属から条件が従い、さらに関係づけられていることが従います。逆に、関係づけられていることから条件が従い、そこから所属が従います。この二つの含意を合わせると、候補が選んだ順序数での関係を実現することになります。

```agda
    step-rel : ⟨ γ ⊨ StepAt v b f ⟩ → IsRel (fst (lookup b γ)) (lookup v γ)
    step-rel h z =
        (λ hz → subst ⟨_⟩ (same z) (extAt-out v (Cond b f) γ h z hz))
      , (λ hz → extAt-in v (Cond b f) γ h z (subst ⟨_⟩ (sym (same z)) hz))
```

同じ議論は逆向きにも使えます。ある集合がすでに段階の関係を実現していれば、その二つの所属に関する含意を意味論的同値に沿って運び、外延的な一段階を証明できます。したがって、順序数と表についての仮定がそろえば、一段階の論理式と関係の実現は同じ情報を表します。

```agda
    step-table : IsRel (fst (lookup b γ)) (lookup v γ) → ⟨ γ ⊨ StepAt v b f ⟩
    step-table sp = extAt-in-both v (Cond b f) γ
      (λ z hz → subst ⟨_⟩ (sym (same z)) (sp z .fst hz))
      (λ z h → sp z .snd (subst ⟨_⟩ (same z) h))
```

## 近似とグラフ

ここで一般の再帰の形をこの一段階に特殊化します。近似とは、指定された定義域をもち、記録した各要素で一段階の条件を満たす集合符号化された表です。グラフは、そのような近似が現在の引数での値を支えることを述べ、順序対を値とするグラフは引数とその値を一緒に記録します。導入規則と除去規則を使えば、命題的切り詰めの存在から証人を選ぶことなく、以後はこの意味に沿って議論できます。

```agda
  module A = RecShape StepAt
  open A using ( ApproxAt; GraphAt; ApproxAt-dom; ApproxAt-value; ApproxAt-step
               ; ApproxAt-in; GraphOf; Graph-in; Graph-out
               ; PairGraphAt; PairOf; PairGraph-in; PairGraph-out )
```

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

近似が正しい値だけを記録することを示すため、その表と定義域を固定し、引数の候補 `u` を考えます。帰納に用いる性質は、`u` が構成可能な順序数なら、記録された各対 `(u,r)` の値 `r` が `u` での関係を実現する、というものです。記録されたすべての値を対象にするため、単値性を仮定していません。

```agda
  module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) where
    private
      Value : V ℓ → Type (ℓ-suc ℓ)
      Value u = ⟨ isL u ⟩ → IsOrd u → (r : S)
              → ⟨ pr u (fst r) ∈ fst (lookup f γ) ⟩ → IsRel u r
```

記録された引数 `c` の基礎の集合について、所属に沿う帰納を行います。この原理は命題だけでなく任意の依存型族に対する再帰原理なので、先ほどの Type 値の性質にも適用できます。近似の定義域には別に順序数性を仮定し、記録された一つの引数より下の要素が同じ定義域にとどまることを保証します。

```agda
    approx-val : ⟨ γ ⊨ ApproxAt f a ⟩ → IsOrd (fst (lookup a γ))
               → (c : S) → IsOrd (fst c) → (r : S)
               → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst c) r
    approx-val h oa c = ∈-induction {P = Value} go (fst c) (snd c)
      where
```

帰納の一段階で、`r` を `u` に記録された値とします。近似自身が、この要素は同じ表から計算される再帰の一段階を満たすと述べています。この一段階を `u` での関係の実現として読むには、`u` より下に制限した表の正しさと完全性が必要です。この二つを、帰納仮定と定義域の情報がそれぞれ与えます。

```agda
      go : (u : V ℓ) → ((t : V ℓ) → ⟨ t ∈ u ⟩ → Value t) → Value u
      go u IH hu ou r p = step-rel zero (suc zero) (sh2 f) (r ∷ d ∷ γ) ou vals ents
        (ApproxAt-step f a γ h d r p)
        where
        d : S
```

引数 `u` をその構成可能性の証明と組にすると、モデルの要素として扱えます。`(u,r)` が記録されているので、近似の正確な定義域の節から、`u` が近似の順序数領域に属することが分かります。ここで、一つの表要素についての事実が、より小さい再帰呼出しすべてに必要な上界へ変わります。

```agda
        d = u , hu
        u∈a : ⟨ u ∈ fst (lookup a γ) ⟩
        u∈a = ApproxAt-dom f a γ h d r p
        vals : Values (lookup f γ) u
        vals e t e∈ q =
```

`e∈u` を満たす要素 `(e,t)` については、帰納仮定が `t` は `e` での関係を実現すると示します。また、順序数の要素であることから `e` も順序数です。完全性は別の仕方で得られます。近似の順序数領域の推移性により、`e∈u` と `u` が領域に属することから `e` も領域に属し、近似がそこで何らかの値の存在を命題的切り詰めのもとで与えます。これで `u` での再帰の一段階に必要な前提がすべてそろいます。同じ引数に二つの値が記録されていれば、どちらも同じクラスを実現するので後に外延的一意性から同一視できますが、ここでは別の名前をもつ一意性補題は導入しません。

```agda
          IH (fst e) e∈ (snd e) (mem-ord {A = u} ou (fst e) e∈) t q
        ents : Entries (lookup f γ) u
        ents e e∈ = ApproxAt-value f a γ h e (oa .fst {x = u} {y = fst e} e∈ u∈a)
```

## グラフが決定する値

グラフの主張が含む、それを支える近似の証人は命題的切り詰めの中にあります。しかし、求める結論である「表示された値が順序数の引数での関係を実現する」は命題です。したがって、その結論へ切り詰めを除去できます。ここで得られるのはグラフの値の正しさであり、一意性にはさらに二つの実現集合を外延性で比較する必要があります。

```agda
  module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where
    graph-only : ⟨ γ ⊨ GraphAt w b ⟩ → IsOrd (fst (lookup b γ))
               → IsRel (fst (lookup b γ)) (lookup w γ)
    graph-only h ob = PT.rec (snd (Realizes (fst (lookup b γ)) (lookup w γ)))
      read (Graph-out w b γ h)
```

この命題の目標の中でグラフの証人を開くと、近似 `f` と上界での外側の一段階が得られます。`f` が上界より下の各引数で正しい値と要素をもつと分かれば、その一段階を関係の実現として読めます。この二つの事実は新たに仮定するのではなく、近似から取り出します。

```agda
      where
      read : GraphOf w b γ → IsRel (fst (lookup b γ)) (lookup w γ)
      read (f , (ha , hs)) = step-rel (suc w) (suc b) zero (f ∷ γ) ob vals ents hs
        where
        vals : Values f (fst (lookup b γ))
```

`f` が記録する各値の正しさは、直前の所属に沿う帰納の結果を順序数の上界の各要素に適用して得ます。その要素が順序数であることは `mem-ord` が保証します。上界より下での完全性は、近似の正確な定義域の仕様にある値の存在の向きです。したがって、外側の一段階から求める実現が得られます。

```agda
        vals c r c∈ p = approx-val zero (suc b) (f ∷ γ) ha ob c
          (mem-ord {A = fst (lookup b γ)} ob (fst c) c∈) r p
        ents : Entries f (fst (lookup b γ))
        ents = ApproxAt-value zero (suc b) (f ∷ γ) ha
```

逆向きには、順序数の上界上で正しく、その下の各点に要素をもち、第一成分が上界の外にある対を記録しない表 `h` から始めます。候補となる現在の値が上界での関係を実現するなら、これらの資料で `h` をグラフが隠している近似として示し、グラフの外側の一段階も検証できます。

```agda
    graph-table : (h : S) → IsOrd (fst (lookup b γ))
                → Values h (fst (lookup b γ)) → Entries h (fst (lookup b γ))
                → Domain h (fst (lookup b γ))
                → IsRel (fst (lookup b γ)) (lookup w γ) → ⟨ γ ⊨ GraphAt w b ⟩
    graph-table h ob vals ents dom sp = Graph-in w b γ h approx
```

外側の一段階は、実現の仮定を逆向きの意味論的な橋に通せば直ちに得られます。残るのは近似です。その定義域は正確でなければならず、ある第一成分が表の何らかの要素に現れることと、その第一成分が上界より下にあることが同値である必要があります。二つの向きは異なる表の仮定を使うため、正しさ、完全性、有界性は混同されません。

```agda
      (step-table (suc w) (suc b) zero (h ∷ γ) ob vals ents sp)
      where
      onDom : (c : S)
            → (⟨ ∃[ r ∶ S ] pr (fst c) (fst r) ∈ fst h ⟩
               → ⟨ fst c ∈ fst (lookup b γ) ⟩)
```

何らかの値が `c` に記録されているとき、その値の証人は命題的切り詰めの中にあります。結論である「`c` が上界に属する」は命題なので、そこへ切り詰めを除去し、有界性から結論を得られます。逆に、完全性は上界内の各 `c` に、単に存在する記録値を与えます。二つの向きを合わせると、近似が必要とする正確な定義域になります。

```agda
            × (⟨ fst c ∈ fst (lookup b γ) ⟩
               → ⟨ ∃[ r ∶ S ] pr (fst c) (fst r) ∈ fst h ⟩)
      onDom c = (λ hr → PT.rec (snd (fst c ∈ fst (lookup b γ)))
                          (λ { (r , p) → dom c r p }) hr)
              , ents c
```

近似の第二の節は、記録された各対 `(c,r)` で再帰の一段階を検査します。同じ表 `h` を使いますが、`c` より下に関係する情報だけを使います。したがって、既存の各要素を局所的に見て、`c` が順序数であること、その下の記録値がすべて正しいこと、さらに各小さい引数に要素があることを示します。

```agda
      onStep : (c r : S) → ⟨ pr (fst c) (fst r) ∈ fst h ⟩
             → ⟨ (r ∷ c ∷ h ∷ γ) ⊨ StepAt zero (suc zero) (suc (suc zero)) ⟩
      onStep c r p = step-table zero (suc zero) (suc (suc zero)) (r ∷ c ∷ h ∷ γ)
        oc vals' ents' (vals c r c∈ p)
        where
```

まず有界性から、記録された対の第一成分 `c` が周囲の上界より下にあることが分かります。その上界は順序数なので、`c` も順序数です。これで正しさの仮定を `c` より下に制限できます。要素 `(e,t)` が実際に記録されていれば、有界性が `e` を周囲の上界に置くため、もとの正しさを適用できます。

```agda
        c∈ : ⟨ fst c ∈ fst (lookup b γ) ⟩
        c∈ = dom c r p
        oc : IsOrd (fst c)
        oc = mem-ord {A = fst (lookup b γ)} ob (fst c) c∈
        vals' : Values h (fst c)
```

局所的な正しさと局所的な完全性の由来は対称ではありません。正しさには要素が記録されているという事実だけで十分であり、有界性から周囲の領域への所属を回収できます。完全性は `e∈c` から始まり、周囲の順序数の推移性と `c` が上界より下にあることから `e` も上界より下にあると示し、もとの完全性から `e` での要素を得ます。

```agda
        vals' e t _ q = vals e t (dom e t q) q
        ents' : Entries h (fst c)
        ents' e e∈ = ents e (ob .fst {x = fst c} {y = fst e} e∈ c∈)
```

正確な定義域の同値と各要素での局所的な一段階は、近似をなす二つの連言です。これらをまとめると、`h` はグラフに隠された近似の証人になります。すでに確かめた外側の一段階と合わせて、正しく完全で有界な表からグラフの主張への向きが完成します。

```agda
      approx : ⟨ (h ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
      approx = ApproxAt-in zero (suc b) (h ∷ γ)
        (domAt-intro zero (suc b) (h ∷ γ) onDom) onStep
```

## 順序対を値とするグラフ

置換公理は、完全な表の項目を値とするグラフに作用します。そこで `PairGraphAt` は、表示された値が現在の添字とある関係集合との Kuratowski 対であり、その関係集合がその添字で `GraphAt` を満たすことを述べます。二つの読みは、関係集合の証人を命題的切り詰めの内側に保ちます。これが、関係集合を値とする再帰と、添字つきの項目からなる置換の像との橋になります。

## 表と上界における関係

クラス `Recorded B` は、`B` より下の表がもつべき要素を記述します。ある対象がこのクラスに属するとは、モデル要素 `c` と `r` が命題的切り詰めのもとで存在し、`c` が `B` に属し、`r` が `c` での関係を実現し、その対象が二つの基礎の集合の順序対に等しいことです。定義そのものは `B` が順序数であることを要求せず、このクラスを順序数の上界で使うときに順序数性が働きます。

```agda
  Recorded : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
  Recorded B z = ∃[ c ∶ S ] (fst c ∈ B) ⊓ (∃[ r ∶ S ]
    ((z ≡ pr (fst c) (fst r)) , setIsSet z (pr (fst c) (fst r)))
    ⊓ Realizes (fst c) r)
```

モデルの集合が `B` の表であるとは、その集合への所属が各点で `Recorded B` への所属と同値であることです。二つの向きがともに必要です。一方は無関係な対象や領域外の対象を排除し、他方は `c∈B` かつ `r` が `c` での関係を実現する各対 `(c,r)` を含めます。したがって `IsTable` は、正しい要素についての閉性だけでなく正確な表現を述べます。

```agda
  IsTable : V ℓ → S → Type (ℓ-suc (ℓ-suc ℓ))
  IsTable B h = (z : S) → (fst z ∈ fst h) ≡ Recorded B (fst z)
```

`α` での再帰データは、モデル内の二つの集合を含みます。一つは `α` より下の正しい要素すべてを正確に表す表であり、もう一つは `α` 自身での関係を実現する集合です。より大きい引数を扱うとき、第一成分は近似を検査するための既存の表を与え、第二成分は後の表に記録する関係の値を与えます。この束は所属に沿う再帰が返すデータです。その型が命題であるという証明はなく、また必要でもありません。所属に沿う帰納は任意の Type 値の族を受け取るからです。

```agda
  Bundle : V ℓ → Type (ℓ-suc (ℓ-suc ℓ))
  Bundle α = Σ[ h ∈ S ] Σ[ r ∈ S ] (IsTable α h × IsRel α r)
```

上界 `B` に対する正確な表 `h` を固定します。その仕様を具体的な要素に使うには、モデル要素の内部の順序対と、それらの基礎の集合からなるホスト側の Kuratowski 対をそろえる必要があります。内部対の射影則に沿って表の所属同値を運ぶと、基礎の順序対 `(c,r)` で使える形になります。

```agda
  module _ (B : V ℓ) (oB : IsOrd B) (h : S) (sp : IsTable B h) where
    private
      atPair : (c r : S)
             → (pr (fst c) (fst r) ∈ fst h) ≡ Recorded B (pr (fst c) (fst r))
      atPair c r = subst (λ x → (x ∈ fst h) ≡ Recorded B x) (prʟ-fst c r)
```

正確な表の仕様を内部の順序対に適用し、その同値を先ほどの射影則を通して読みます。周囲の読みでは `B` を順序数として固定していますが、この同定そのものが使うのは表の仕様と順序対の表現だけであり、追加の順序数論的議論はありません。

```agda
        (sp (prʟ c r))
```

これで実際の表要素 `(c,r)` を二つの面から同時に読めます。正確性から記録された形への分解が得られ、そこから定義域の事実 `c∈B` と、値の正しさである「`r` が `c` での関係を実現する」を回収します。この読みを各要素に適用すると、`Domain h B` と `Values h B` が得られます。

```agda
    table-out : Domain h B × Values h B
    table-out = (λ c r p → read c r p .fst) , (λ c r _ p → read c r p .snd)
      where
      read : (c r : S) → ⟨ pr (fst c) (fst r) ∈ fst h ⟩
           → ⟨ fst c ∈ B ⟩ × IsRel (fst c) r
```

`Recorded` が与える分解は命題的切り詰めの中にあるため、その除去先は命題でなければなりません。ここでの目標は、`B` への所属と関係の実現との積です。所属も実現も命題であり、その積も命題です。除去を正当化するのはこの局所的な目標であって、束全体についての性質ではありません。

```agda
      read c r p = PT.rec isPropBoth outer (subst ⟨_⟩ (atPair c r) p)
        where
        isPropBoth : isProp (⟨ fst c ∈ B ⟩ × IsRel (fst c) r)
        isPropBoth = isProp× (snd (fst c ∈ B)) (snd (Realizes (fst c) r))
```

命題への除去の内側で、記録された分解が別の対 `(d,t)` を使うとします。Kuratowski 対 `(c,r)` と `(d,t)` の等しさから、第一の基礎成分どうしと第二の基礎成分どうしがそれぞれ等しいと分かります。第一の等しさは定義域への所属を運び、第二の等しさは読みたい値と分解に現れた実現値をそろえます。

```agda
        inner : (d t : S) → ⟨ fst d ∈ B ⟩
              → (pr (fst c) (fst r) ≡ pr (fst d) (fst t)) → IsRel (fst d) t
              → ⟨ fst c ∈ B ⟩ × IsRel (fst c) r
        inner d t d∈ q hr =
            subst (λ x → ⟨ x ∈ B ⟩) (sym (pr-inj q .fst)) d∈
```

第一成分の等しさに沿って `d∈B` を `c∈B` へ運べます。第二の基礎の集合の等しさはモデル要素 `r` と `t` の等しさへ持ち上がります。構成可能性の証明は命題であり、追加の選択を含まないからです。添字の等しさと値の等しさに同時に沿って実現を運べば、ちょうど `(c,r)` での実現が得られます。

```agda
          , subst2 IsRel (sym (pr-inj q .fst)) (sym rt) hr
          where
          rt : r ≡ t
          rt = Σ≡Prop (λ x → snd (isL x)) (pr-inj q .snd)
```

記録された外側の証人は、まず `B` に属する添字 `d` と、その実現値についてのさらに切り詰められた証人を与えます。最終的に求める二つの事実は命題なので、二層の命題的切り詰めを順に除去できます。先ほどの端点の等しさに関する議論が、最も内側の分解を処理します。

```agda
        outer : Σ[ d ∈ S ] ( ⟨ fst d ∈ B ⟩
                  × ⟨ ∃[ t ∶ S ] ((pr (fst c) (fst r) ≡ pr (fst d) (fst t))
                        , setIsSet _ (pr (fst d) (fst t))) ⊓ Realizes (fst d) t ⟩ )
              → ⟨ fst c ∈ B ⟩ × IsRel (fst c) r
        outer (d , (d∈ , hs)) = PT.rec isPropBoth
```

実現値の候補 `t` ごとに、順序対の等しさから証人を `c` と `r` について求める事実へ変換できます。結果には `t` が残らないため、この切り詰めの使用は表から値を選んでいません。与えられた要素が必要な定義域と実現の性質をもつ、という命題だけを証明しています。

```agda
          (λ { (t , (q , hr)) → inner d t d∈ q hr }) hs
```

表を読む逆向きは直接的です。`c∈B` と、`c` での関係を実現するモデル要素 `r` が与えられれば、対 `(c,r)` は `Recorded` が要求する命題的切り詰められた証人をもちます。表の正確性により、そのクラスへの所属を `h` への所属へ変え、内部対の射影則が二つの表現をそろえます。

```agda
    table-in : (c r : S) → ⟨ fst c ∈ B ⟩ → IsRel (fst c) r
             → ⟨ pr (fst c) (fst r) ∈ fst h ⟩
    table-in c r c∈ hr = subst ⟨_⟩ (sym (atPair c r))
      ∣ c , (c∈ , ∣ r , (refl , hr) ∣₁) ∣₁
```

順序数 `α` での関係を分出によって得る前に、関係しうるすべての順序対を含む一つの `L` の集合が必要です。求める上界は、`Related α` の各対象を含むモデル集合 `D` を返します。これは共通の容器にすぎず、無関係な要素を含んでもよいため、この時点では正確性を主張しません。

```agda
  bound : (α : V ℓ) (oα : IsOrd α)
        → Σ[ D ∈ S ] ((z : S) → ⟨ Related α (fst z) ⟩ → ⟨ fst z ∈ fst D ⟩)
  bound α oα = d .fst , confine
    where
    ixL : ⟪ Lset α ⟫ → S
```

`Lset α` の小さい提示は、その全要素に添字を与えます。各添字が提示する基礎の集合を、構成可能な段階への所属から得た構成可能性の証明と組にして、モデル要素にします。これにより、提示された各端点について内部の順序対を作れます。

```agda
    ixL m = ⟪ Lset α ⟫↪ m , Lset→isL α oα (⟪ Lset α ⟫↪ m) (memOf (Lset α) m)
```

提示の添字の対は小さい添字型をなします。それらに対応する内部順序対の族へ共通領域の原理を適用すると、その族の各要素を含むモデル集合 `D` が得られます。この原理が与えるのは包含だけであり、正確な像を計算せず、段階の順序に従って対を選別することもありません。

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

共通の上界は提示の添字だけでなく、`Lset α` の通常の要素 `a,b` にも使えなければなりません。各要素をそのファイバー添字で表し、対応する内部順序対について上界を使い、提示された対とホスト側の対 `pr(fst a,fst b)` との等しさに沿って所属を運びます。したがって、段階の任意の二要素からなる順序対は `D` に属します。

```agda
    onPair : (a b : Mem (Lset α)) → ⟨ pr (fst a) (fst b) ∈ fst (d .fst) ⟩
    onPair a b = subst (λ x → ⟨ x ∈ fst (d .fst) ⟩)
      (prʟ-fst (ixL (fa .fst)) (ixL (fb .fst))
        ∙ cong₂ pr (fa .snd) (fb .snd))
      (d .snd (fa .fst , fb .fst))
```

`a` と `b` の所属証明は、それぞれを小さい提示の要素と同定します。得られるファイバーの等しさが二つの端点をそろえ、順序対を作る操作の合同性がホスト側の二つの対を同定します。内部対の射影則と合わせると、直前の所属の輸送に必要な等しさになります。

```agda
      where
      fa = ∈-asFiber {a = fst a} {b = Lset α} (snd a)
      fb = ∈-asFiber {a = fst b} {b = Lset α} (snd b)
```

`Related α` の任意の対象を取ります。その定義は、命題的に切り詰められた三重の存在量化を通して、順序数性の証明、`Lset α` の二要素 `a,b`、および対象をその順序対と同定する等しさを与えます。段階順序の比較そのものも、さらに命題的切り詰めの内側にあります。目標である `D` への所属は命題なので、三つの存在量化の切り詰めを順に除去できます。この粗い上界に必要なのは二つの端点と対の等しさだけであり、切り詰められた比較の事実さえ使いません。

```agda
    confine : (z : S) → ⟨ Related α (fst z) ⟩ → ⟨ fst z ∈ fst (d .fst) ⟩
    confine z = PT.rec (snd (fst z ∈ fst (d .fst)))
      (λ { (_ , h₁) → PT.rec (snd (fst z ∈ fst (d .fst)))
        (λ { (a , h₂) → PT.rec (snd (fst z ∈ fst (d .fst)))
          (λ { (b , (q , _)) →
```

回収した二つの端点からなる順序対は、先の結果によりすでに `D` に属します。回収した対の等しさの逆向きにこの所属を運ぶと、もとの対象が `D` に属すると分かります。証人は命題の証明の内部にとどまるため、この上界は各対象の端点を選んでいません。

```agda
            subst (λ x → ⟨ x ∈ fst (d .fst) ⟩) (sym q) (onPair a b) }) h₂ }) h₁ })
```

表と現在の関係を、所属に沿う再帰で同時に構成します。実際の入力範囲は構成可能な順序数であり、`α` には `L` に属することの証明と順序数性の証明の両方が伴います。再帰の値は先ほどの束であり、後ではその仕様を通して使うよう定義を閉じています。この再帰は Type 値の族に適用でき、`Bundle α` が命題であることには依存しません。

```agda
  opaque
    tableAt : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → Bundle α
    tableAt = ∈-induction {P = λ α → ⟨ isL α ⟩ → IsOrd α → Bundle α}
      (build (PairGraphAt zero (suc zero)) refl)
      where
```

`α` での帰納の一段階では、`α` の各要素 `δ` について、その構成可能性と順序数性が与えられれば対応する束がある、と再帰的に仮定します。ここでの課題は、`α` より下の表と `α` での関係を作ることです。順序対を値とするグラフの論理式を、意図した論理式との等しさとともに明示的な引数として保ちます。これは数学的仮定を増やさず、置換の議論がまさにそのグラフを使うことを保証します。

```agda
      build : (φ : Formula S 2) → φ ≡ PairGraphAt zero (suc zero)
            → (α : V ℓ)
            → ((δ : V ℓ) → ⟨ δ ∈ α ⟩ → ⟨ isL δ ⟩ → IsOrd δ → Bundle δ)
            → ⟨ isL α ⟩ → IsOrd α → Bundle α
      build φ qφ α IH hα oα = rep .fst .fst , (sep .fst .fst , (spec , rspec))
```

順序数 `α` とその構成可能性の証明を組にして、モデル要素 `A` を作ります。これは順序対を値とするグラフを考える内部の定義域です。その要素は、順序数性を示せば所属に沿う再帰仮定を適用できる、より小さい集合にちょうど当たります。

```agda
        where
        A : S
        A = α , hα
```

順序数 `α` の各要素 `c` はそれ自身も順序数です。この継承された順序数性は不可欠です。再帰的構成の定義域は任意の構成可能な要素ではなく、構成可能な順序数だからです。この順序数性の証明を得る際に命題的切り詰めは使いません。

```agda
        ordOf : (c : S) → ⟨ fst c ∈ α ⟩ → IsOrd (fst c)
        ordOf c c∈ = mem-ord {A = α} oα (fst c) c∈
```

`c∈α` のとき、モデル要素 `c` はすでに構成可能性の証明をもち、順序数の要素であることから順序数性も得られます。これは帰納仮定を適用するために必要な入力そのものです。結果として、`c` より下の正確な表と `c` での関係の実現集合をともに含む、`c` での完全な束が得られます。

```agda
        bun : (c : S) → ⟨ fst c ∈ α ⟩ → Bundle (fst c)
        bun c c∈ = IH (fst c) c∈ (snd c) (ordOf c c∈)
```

`c` での再帰的な束から、現在の関係の成分を取り出し、`c` での値とします。これは具体的なモデル要素であり、表の命題的切り詰められた `Entries` から取り出した証人ではありません。定義域内の各構成可能な順序数での関係をその下の表と一緒に再帰が運ぶのは、この具体的な値を利用するためです。

```agda
        value : (c : S) → ⟨ fst c ∈ α ⟩ → S
        value c c∈ = bun c c∈ .snd .fst
```

その成分とともに保存された仕様は、選んだ値が `Related c` を実現すると述べます。これは帰納仮定が与える意味論的な正しさそのものです。この事実だけでは、その値が順序対を値とするグラフを満たすことも、`c` との対が完成した表に属することも主張できません。

```agda
        relOK : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) → IsRel (fst c) (value c c∈)
        relOK c c∈ = bun c c∈ .snd .snd .snd
```

底の順序数が `α` に属する各 `c` について、帰納法の仮定はすでに `c` における関係集合を与えています。置換公理では、どの添字がその関係を生んだかを残す必要があるため、候補となる値は関係集合だけではなく、`c` とその関係集合との内部順序対です。

```agda
        entry : (c : S) → ⟨ fst c ∈ α ⟩ → S
        entry c c∈ = prʟ c (value c c∈)
```

次に、この候補が置換公理で用いるグラフ上にあることを示します。順序対を作る前に、選んだ関係集合が `c` における再帰グラフを満たさなければなりません。`c` における束は、その下の表とそこで実現された関係をともに与えます。また、順序数 `α` に `c` が属することから `c` 自身も順序数なので、表からグラフを得る一般の議論を適用できます。

```agda
        below : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) (k : S)
              → ⟨ (value c c∈ ∷ k ∷ c ∷ []) ⊨ GraphAt zero (suc (suc zero)) ⟩
        below c c∈ k = graph-table zero (suc (suc zero))
          (value c c∈ ∷ k ∷ c ∷ []) (bun c c∈ .fst) (ordOf c c∈)
          (reads .snd) ents (reads .fst) (relOK c c∈)
```

下方の表の正確な仕様から、この議論に必要な三つの事実のうち二つが得られます。`c` より下で記録された各値は対応する関係を実現し、添字が `c` の外にある順序対は記録されません。残るのは完全性、すなわち `c` の各要素に何らかの記録値があることです。

```agda
          where
          reads : Domain (bun c c∈ .fst) (fst c) × Values (bun c c∈ .fst) (fst c)
          reads = table-out (fst c) (ordOf c c∈) (bun c c∈ .fst)
                    (bun c c∈ .snd .snd .fst)
          ents : Entries (bun c c∈ .fst) (fst c)
```

`e` が `c` の要素なら、周囲の順序数の推移性により `e ∈ c ∈ α` から `e ∈ α` が従います。したがって帰納法の仮定は `e` における実現関係を与え、`c` における表の正確な仕様は、`e` とその関係との順序対を下方の表へ入れます。この証人は、表の完全性が要求するとおり、命題的切り詰めの中で返されます。

```agda
          ents e e∈ = ∣ value e e∈' , table-in (fst c) (ordOf c c∈) (bun c c∈ .fst)
                         (bun c c∈ .snd .snd .fst) e (value e e∈') e∈ (relOK e e∈') ∣₁
            where
            e∈' : ⟨ fst e ∈ α ⟩
            e∈' = oα .fst {x = fst c} {y = fst e} e∈ c∈
```

これで、関係値についての再帰グラフの証明と、内部順序対の標準的な同一視とを組み合わせられます。その結果、候補の項目は `c` において順序対グラフの論理式を満たし、`α` より下の各添字について関数性の存在側が得られます。

```agda
        holds : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) → ⟨ (entry c c∈ ∷ c ∷ []) ⊨ φ ⟩
        holds c c∈ = PairGraph-in zero (suc zero) (entry c c∈ ∷ c ∷ []) φ qφ
          (value c c∈) (prʟ-fst c (value c c∈)) (below c c∈ (entry c c∈))
```

関数性には、順序対全体としての値の一意性も必要です。別の `k` が `c` において順序対グラフを満たすなら、その論理式を読むことで、命題的切り詰めの中に、関係集合 `r`、`k` の底の集合と順序対 `(c,r)` との同一視、そして `r` のグラフの証明が得られます。構成可能な台における等しさは命題なので、この切り詰められた情報を求める等しさへ消去できます。

```agda
        only : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) (k : S)
             → ⟨ (k ∷ c ∷ []) ⊨ φ ⟩ → k ≡ entry c c∈
        only c c∈ k h = PT.rec (isSetS k (entry c c∈)) read
          (PairGraph-out zero (suc zero) (k ∷ c ∷ []) φ qφ h)
          where
```

グラフの証明は、`r` が `c` における関係クラスを実現することを述べます。一方、帰納法の仮定は、`c` で選ばれた値も同じクラスを実現することを述べます。したがって、実現関係集合の外延的な一意性により、`r` は選ばれた値と同一視されます。一意性を用いるのはグラフの正しさを確立した後であり、下方の表に単値性を仮定しているのではありません。

```agda
          read : PairOf zero (suc zero) (k ∷ c ∷ []) φ qφ → k ≡ entry c c∈
          read (r , (q , hg)) = Σ≡Prop (λ x → snd (isL x))
            ( q
            ∙ cong (pr (fst c)) (cong fst (rel-unique (fst c) r (value c c∈)
                (graph-only zero (suc (suc zero)) (r ∷ k ∷ c ∷ []) hg (ordOf c c∈))
```

与えられた `k` と `(c,r)` との同一視、二つの関係集合の等しさ、そして構成可能な順序対の標準的な射影パスを順に合成すると、`k` と候補項目の底の集合が同一視されます。構成可能性は命題なので、この底での等しさは台における等しさへ持ち上がり、一意性の証明が完了します。

```agda
                (relOK c c∈)))
            ∙ sym (prʟ-fst c (value c c∈)) )
```

各 `c ∈ α` について、ここまでの存在性と一意性は、グラフの値とその充足証明からなるファイバーの一点を一意に定めます。この一意存在の証人は命題的に切り詰められていますが、可縮性そのものは命題です。したがって `mereFunct` は新たな選択を行わずに、この証人を置換公理が要求する可縮なファイバーへ変換します。

```agda
        fc : (c : S) → ⟨ c ∈ˢ A ⟩
           → isContr (Σ[ k ∈ S ] ⟨ (k ∷ c ∷ []) ⊨ φ ⟩)
        fc c c∈ = mereFunct φ c ∣ entry c c∈ , (holds c c∈ , only c c∈) ∣₁
```

したがって置換公理は、内部の定義域 `α` 上で順序対グラフの値を集められます。その結論は、構成可能な集合と、その像についての正確な所属仕様とからなる可縮型です。つまり一意に指定された像集合が得られるのであって、その集合の要素が可縮型をなすという主張ではありません。

```agda
        rep : isContr (SetOf (λ z → ∃[ c ∶ S ] (c ∈ˢ A) ⊓ ((z ∷ c ∷ []) ⊨ φ)))
        rep = hasReplacementL A φ fc
```

表 `H` は、この可縮な置換結果の中心が与える構成可能な集合です。それに伴う所属仕様も引き続き利用でき、`H` が意図した添字と関係との順序対だけを正確に記録することを次に証明します。

```agda
        H : S
        H = rep .fst .fst
```

必要な表の仕様は二つの命題の等しさです。一方は `H` への所属であり、他方は、`α` より下の添字と、そこでの関係を実現する集合との順序対であることです。この等しさは二つの含意から得ます。順方向では置換による所属を読み、逆方向ではそのような記録順序対を置換グラフの値へ戻します。

```agda
        spec : IsTable α H
        spec z = ⇔toPath toRec fromRec
          where
          toRec : ⟨ fst z ∈ fst H ⟩ → ⟨ Recorded α (fst z) ⟩
          toRec hz = PT.rec squash₁
```

順方向では、置換による所属から、`α` より下の添字 `c` と、`z` がそこで順序対グラフを満たすという証明が、命題的切り詰めの中で得られます。先ほどの一意性により `z` は `c` における標準的な項目と同一視され、その関係成分はすでに `c` でのクラスを実現すると分かっています。これらから必要な記録順序対の証人が得られ、命題的切り詰めの境界も保たれます。

```agda
            (λ { (c , (c∈ , hp)) → ∣ c , (c∈ , ∣ value c c∈
               , ( cong fst (only c c∈ z hp) ∙ prʟ-fst c (value c c∈)
                 , relOK c c∈ ) ∣₁) ∣₁ })
            (subst ⟨_⟩ (rep .fst .snd z) hz)
```

逆向きの含意では、記録順序対の証人に含まれる関係集合 `r` は、`c` における関係クラスを実現する任意の集合でよく、先に再帰的に選んだ値とは限りません。標準的な項目についてすでに得た順序対グラフの証明を再利用するため、まず切り詰められた証人を命題である充足の目標へ消去し、次に二つの項目の等しさに沿ってその証明を移します。

```agda
          fromRec : ⟨ Recorded α (fst z) ⟩ → ⟨ fst z ∈ fst H ⟩
          fromRec hz = subst ⟨_⟩ (sym (rep .fst .snd z)) (PT.map
            (λ { (c , (c∈ , hr)) → c , (c∈ , PT.rec (snd ((z ∷ c ∷ []) ⊨ φ))
              (λ { (r , (q , hs)) → subst (λ t → ⟨ (t ∷ c ∷ []) ⊨ φ ⟩)
                (sym (Σ≡Prop (λ x → snd (isL x))
```

この移送パスは、記録された証人に伴う `z` の等しさから始まり、外延的な一意性によって `r` を標準的な関係値に置き換え、内部順序対の標準的な射影パスで終わります。構成可能性の証明は命題なので、底の集合の等しさから台における等しさが定まります。このパスに沿って移されたグラフの証明により `z` は置換の像に入り、逆向きの含意が完了します。

```agda
                  (q ∙ cong (pr (fst c)) (cong fst
                     (rel-unique (fst c) r (value c c∈) hs (relOK c c∈)))
                     ∙ sym (prʟ-fst c (value c c∈)))))
                (holds c c∈) }) hr) }) hz)
```

ここで表の正確な仕様から、`H` が `α` より下で記録するすべての値の正しさが得られます。`c ∈ α` で順序対 `(c,r)` が `H` に属するなら、その仕様を読むことで `r` が `c` における関係クラスを実現すると分かります。この段階では新たな帰納法や一意性の議論は不要です。

```agda
        tvals : Values H α
        tvals = table-out α oα H spec .snd
```

完全性は各点ごとに得られます。各 `c ∈ α` について、`c` における再帰値が必要なクラスを実現すると分かっているので、表の仕様は `c` とその値との順序対を `H` に入れます。得られる存在命題は命題的に切り詰められており、各添字に項目があることを保証しますが、特定の項目を完全性の主張に含めるものではありません。

```agda
        tents : Entries H α
        tents c c∈ = ∣ value c c∈
                    , table-in α oα H spec c (value c c∈) c∈ (relOK c c∈) ∣₁
```

この表から、`α` におけるステップ条件の定数形を読むために必要な、値の正しさと完全性が得られました。分出公理は、先に構成した共通の上界の中でその条件を適用します。その結果、上界に属して条件を満たす要素だけを正確にもつ、仕様によって一意な構成可能部分集合が得られます。`α` における関係の候補は共通の上界そのものではなく、この部分集合です。

```agda
        sep : isContr (SetOf (λ x → (x ∈ˢ bound α oα .fst)
                                  ⊓ ((x ∷ []) ⊨ Cond₀ A H)))
        sep = hasSeparationL (bound α oα .fst) (Cond₀ A H)
```

分出された集合が意図したクラスを実現することを示すため、まずその要素を一つ取ります。分出の仕様から、共通の上界への所属と定数条件の充足がともに得られますが、この向きで必要なのは後者だけです。条件の妥当性により、その充足は `Related α` へ変換され、所属から関係クラスへの含意が得られます。

```agda
        rspec : IsRel α (sep .fst .fst)
        rspec z =
            (λ hz → subst ⟨_⟩ (cond₀-spec A H oα tvals tents z)
                      (subst ⟨_⟩ (sep .fst .snd z) hz .snd))
          , (λ hz → subst ⟨_⟩ (sym (sep .fst .snd z))
```

逆に、`Related α` を満たす要素は、共通の上界がもつ閉じ込めの性質により、その上界に属します。また、妥当性の逆方向は同じ関係の事実を定数条件の充足へ変換します。この二成分が分出の仕様を満たすので、その要素は分出された集合に入り、両方向の正確な実現が完成します。

```agda
                      ( bound α oα .snd z hz
                      , subst ⟨_⟩ (sym (cond₀-spec A H oα tvals tents z)) hz ))
```

構成可能性と順序数性の証明をともに備えた段階添字 `α` について、再帰的な束は下方の表と、いま分出によって得た関係集合とを含みます。関係 `relL` は後者を選びます。したがって、その適用範囲は `L` で用いる構成可能な順序数段階の添字であり、構成可能性の証人を伴わない任意の順序数ではありません。

```agda
  relL : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → S
  relL α hα oα = tableAt α hα oα .snd .fst
```

それに伴う仕様も同じ束から得られます。この仕様は、`relL` への所属がクラス `Related α` と正確に一致すること、すなわち各要素が関係づけられた順序対を表し、関係づけられた各順序対がそこに属することを述べます。したがって後の議論では、置換と分出の構成を開き直さず、この同値を直接用いられます。

```agda
  relL-spec : (α : V ℓ) (hα : ⟨ isL α ⟩) (oα : IsOrd α) → IsRel α (relL α hα oα)
  relL-spec α hα oα = tableAt α hα oα .snd .snd .snd
```

## 要素は順序が関係づける順序対である

`Lset α` の二要素 `a` と `b` について、埋める向きは一般の実現補題を `relL` に特殊化します。したがって、すでに構成されている狭義整列順序 `orderAt α` によるホスト側の比較から、二つの底の集合を符号化した順序対が `relL` に属することが従います。

```agda
  module _ (α : V ℓ) (hα : ⟨ isL α ⟩) (oα : IsOrd α) where
    relL-fill : (a b : Mem (Lset α)) → relOf (orderAt α oα) a b
              → ⟨ pr (fst a) (fst b) ∈ fst (relL α hα oα) ⟩
    relL-fill = rel-fill α oα (relL α hα oα) (relL-spec α hα oα)
```

読む向きは、同じ二つの段階要素について逆を与えます。二要素の符号化順序対が `relL` に属することから、`orderAt α` におけるホスト側の比較が復元されます。二方向を合わせると、後の最小性の議論で用いる関係グラフが各要素対ごとに表現されます。ここでは新たな名前の比較を構成せず、このグラフが整列順序であるという対象言語の主張も行いません。

```agda
    relL-rep : (a b : Mem (Lset α))
             → ⟨ pr (fst a) (fst b) ∈ fst (relL α hα oα) ⟩
             → relOf (orderAt α oα) a b
    relL-rep = rel-rep α oα (relL α hα oα) (relL-spec α hα oα)
```

## まとめ

構成可能な順序数の段階の添字 `α` では、ホスト型理論がすでに `Lset α` の要素上の狭義整列順序 `orderAt α oα` を与えています。`Ordering` はその比較に命題的切り詰めを施して命題値の述語にし、`Related` は関係する端点の順序対をホスト側で定義されたクラスとしてまとめます。三分性によって `strict` が比較を復元できるのは、端点が指定されている場合だけです。その後、`IsRel`、`relL-fill`、`relL-rep` が、この比較と実現集合への所属との正確な点ごとの対応を与えます。

実現集合は間接的に得られます。近似はその定義域より下の値が単に存在することだけを記録し、所属に沿う帰納は単値性を仮定せず、記録された各値が自身の引数でのクラスを実現することを示します。順序対グラフの繊維を比較するときに初めて、実現集合の外延的な一意性が競合する値を同一視します。`mereFunct` は得られた命題的切り詰めのもとの一意存在を可縮性へ変え、置換公理が `α` より下の添字つき項目を集め、分出公理が共通の包含集合から `α` での関係を切り出します。再帰的な束は完成した下方の表と現在の関係をともに運びますが、再帰はこの束が命題であることを要求しません。

構成全体は、`Described` に与えられる二つの妥当な対象言語のステップ形式に相対したままです。後の章が具体的な記述を与え、このパラメータを解消します。ここで `relL` を利用できるのは、`α` に `isL` と `IsOrd` の証拠がともに備わる場合だけです。これは既存の順序の関係グラフを表現するものであり、新たな名前の比較を完成させることも、そのグラフが整列順序であると対象言語で証明することもありません。