---
title: "L の内部における構成可能階層"
module: L.Hierarchy
lang: ja
site: "Bedrock"
description: "L の内部における構成可能階層"
stage: "内部の符号化：表と一様な充足関係"
reading_order: 71
canonical: https://bedrock.institute/ja/L.Hierarchy.html
html: L.Hierarchy.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Hierarchy.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.HierarchySequence]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Hierarchy.md, https://bedrock.institute/zh/L.Hierarchy.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# L の内部における構成可能階層

`L` 内の一階のグラフは、指定した順序数までの外部の構成可能階層を記録します。表の値を外部の塔と照らして関数的かつ正確であると示し、そののち、これらの対を、それより前の段階をちょうど要素とする構成可能集合へ集めます。

本章は内部の階層を構成します。階層の順序数 `α` に対し、`hierL` の `α` での値は `L` の要素であり、その要素は「`α` の下の順序数 `β` と塔の値 `Lset β`」の順序対ちょうどです。一つのパターンが章全体で繰り返されます。**表**とは順序対の集合であり、集合 `B` の下で記録する値がすべてメタレベルの塔のそこでの値であるとき、`B` の上で**正しい**と言い、その下のすべての入力で値を記録しているとき**完備**と言います。正しくて完備な表こそ、グラフのステップ条件が読むものであり、そこから書き下せるものでもあります。だからステップと塔を結ぶ補題の組が、消去と導入の両方に仕えます。

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

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

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

本章は、モデル自身のレベルの後続で排中律の実例を一つ取り、そのもとで進みます。以下の構成はすべてこのモジュールの内部で述べられ、公理の章が渡す場所でだけこの仮定を帯びます。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
import FOL.Absoluteness
import FOL.ZFModel
```

ここでは二つの構造が現れます。周囲の階層はその構造 `𝒮ᵥ` を与え、本章はその所属の帰納と外延性を用います。構成可能な構造 `𝒮ʟ` は台 `S` を与えます。その要素は、階層の集合に「それが構成可能である」証明を添えたものであり、だから各台の要素 `x` には基礎の集合 `fst x` があります。

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV )
open import V.Coding {ℓ} using ( pr; pr-inj )
```

階層は、章を通して使う三つの道具を与えます。所属に沿う帰納、集合の外延性、そして順序対 `pr` と、その成分を取り戻す単射性です。この対は階層のレベルにあり、表の記録された項目も同じレベルにあります。

```agda
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; 𝒟ₒ; Lset; Lset-in; Lset-out; IsOrd )
```

構成可能の側からは、塔 `Lset` が来ます。これは階層の順序数を、そこでの構成可能段階へ送ります。ほかに、定義可能冪集合 `𝒟ₒ`、二つの所属の読み `Lset-in` と `Lset-out`、順序数性 `IsOrd`、そして「構成可能性が所属に沿って伝わる」事実です。塔の添字は順序数、すなわち階層の集合であり、型の大きさの添字である宇宙レベルでは決してありません。

```agda
open import L.Ordinal {ℓ} using ( mem-ord )
open import L.Axioms.Basic {ℓ} using ( LsetS; isL-𝒟ₒ )
open import L.Axioms.Full {ℓ} lem using ( hasReplacementL )
open import L.Recursion {ℓ} lem using ( mereFunct )
```

さらに三つの事実が章を支えます。順序数の要素は順序数であること。段階は `L` の要素として提示でき、それを `LsetS` と書き、構成可能集合の定義可能冪集合はまた構成可能であること。そして `L` の内部では置換が使え、その形は「一意に存在するとだけ分かっている値」を受け入れるものです。

モデルは自分自身の順序対 `prʟ` と、その第一射影を同定する読み `prʟ-fst`、そして定義域の条項 `domAt-intro` を与えます。

```agda
open import L.Coding.Model {ℓ} using ( prʟ; prʟ-fst; domAt-intro )
```

一つ前の符号化の章は、本章が組み立てる語彙を供給します。証人と三つの読みをもつステップ条件、定義域・値・ステップの条項をもつ近似、二つの読みをもつ塔のグラフ、そして順序対のグラフです。

```agda
open import L.Coding.HierarchySequence {ℓ} lem
  using ( StepAt; StepOf; PowOK; StepAt-in; StepAt-out; StepAt-back
        ; ApproxAt; ApproxAt-dom; ApproxAt-value; ApproxAt-step; ApproxAt-in
        ; LsetGraphAt; LsetGraph-in; LsetGraph-out; GraphOf
        ; PairGraphAt; PairOf; PairGraph-in; PairGraph-out )
```

命題の機構はいつものものです。切り詰められた存在、その注入と消去、第二成分が命題である対が第一成分の等しさで等しくなること、そして所属の各点での同値を集合のパスへ変える操作です。

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

階層そのものが型として現れます。その要素は本章が表にする集合であり、その所属は三つの条件が語る関係であり、その h-集合性により、表にされた二つの集合の等しさは命題になります。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
```

構成可能な構造の内側では、`S` が台であり、`⊨` が充足の判断です。`SetOf` は候補の集合と「それがクラスを実現する」という主張を組にします。record のフィールドが公理を述べるのはこの形です。

```agda
open hPropStructure 𝒮ʟ

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

充足は最後に、構成可能な構造で読まれます。章を通しての記法 `γ ⊨ φ` は、`L` から取った定数をもつ論理式を、台の要素の環境で判定します。

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

一つの private な補助は、変数の枠を二つ後ろへずらします。値を一つ、次に入力を一つ追加した環境の中でステップを判定するとき、古い枠はみな二つ後ろへ移ります。表自身の項目の内側からそのステップを判定する場面で、いつも現れます。

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

## 表が記録するもの

**表**とは順序対の集合であり、ここではつねに階層の対で取った対、すなわち入力と値の組です。界集合 `B` の上での表を三つの条件が特徴づけます。それらは補い合う条件であって、一つの主張の三つの読みではありません。`Values` は、`B` の下で記録された値がすべて塔のそこでの値であることを要求します。`Entries` は、`B` の下のすべての入力で正準な項目が記録されていることを要求します。`Domain` は、`B` の外が何も記録されていないことを要求します。

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

正しさは、記録された項目についての主張です。`B` の下の入力 `c` とある `z` の対が表の項目なら、`z` は塔の `c` での値です。所属 `fst c ∈ B` は階層での所属です。`B` が階層の集合だからです。表 `h` は台の要素であり、`fst h` がそれが提示する集合です。

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

完備さは、覆いについての鏡像の要求です。`B` の下の各入力 `c` で、正準な項目、すなわち `c` と塔の値 `Lset c` の対が記録されます。二つの条件から、正しくて完備な表は `B` の下で正準な項目ちょうどを記録し、歪んだものを一切含まないことが分かります。

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

条件を分けておくのは、応用ごとに必要な部分が異なるからです。近似についての帰納は最初の二つを使い、三つ目は使えません。近似の項目はそれ自身の定義域の下に落ちるのであって、帰納が立っている入力の下ではないからです。内部の階層は三つすべてを満たします。正しい対ちょうどの集合として作られるからです。`B` が何であるかにも注意してください。基礎の界集合、すなわち階層の集合です。意味論的な応用では、環境の枠を通して届き、台の要素の基礎の部分として現れます。その台の要素はさらに構成可能性を帯びており、`B` の順序数性はこれらの条件が供給しない独立の仮定です。ここで表にされる段階は階層の集合で、順序数で添字づけられます。ホストの宇宙レベルが表に現れることはありません。

## 外部の階層と照らすステップ

この節は、前章のステップ条件と塔を結びます。入力 `b` でのステップは、`b` の下の入力 `c` とそこで記録された値 `w` にわたって、`w` の定義可能冪集合の要素を集めます。塔が `b` で集める要素は同じもので、記録された `w` を `Lset c` に置き換えたものです。三つの private な事実が比較の準備をします。`ok` は横条件 `PowOK` を清算し、`below` は塔の分解をステップの証人に変え、`above` はステップの証人を塔の要素に変えます。

```agda
module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) where
  private
```

三つの枠は、値・入力・表を名指します。いずれも一つの環境 `γ` の台の要素から読まれます。

```agda
    ok : IsOrd (fst (lookup b γ)) → Values (lookup f γ) (fst (lookup b γ))
       → PowOK b f γ
```

横条件は一度だけ清算され、両方向に働きます。`PowOK` が要求するのは、記録されたそれぞれの値の定義可能冪集合が `L` の要素であることです。記録された値は塔の、`B` の下のある入力での値であり、その入力は `B` が順序数であるゆえに順序数であり、順序数で添字づけられた段階の定義可能冪集合は構成可能です。だからステップに必要なのは正しさと一つの順序数性の仮定だけで、二つの読み出しの主張にその条件は現れません。二つの方向が別々の名前を持つのは、別々に使われるからです。上向きは、記録された値の定義可能冪集合が `B` での塔の中に坐ることで、これが `Lset-in` です。下向きは塔そのものの分解 `Lset-out` であり、続いて、そこで現れる順序数をモデルの要素として名指します。これはクラスの推移性が与えます。

```agda
    ok ob vals c z rec = subst (λ u → ⟨ isL (𝒟ₒ u) ⟩)
      (sym (vals c z (rec .fst) (rec .snd)))
      (isL-𝒟ₒ (fst c) (mem-ord {A = fst (lookup b γ)} ob (fst c) (rec .fst)))
```

証明は二つの仮定を組み合わせます。証人 `rec` は `c` が入力の下にあると言い、それゆえ入力の順序数性から `c` は順序数です。正しさが記録された値を `c` での塔と同一視し、構成可能な段階の定義可能冪集合は構成可能、これが `isL-𝒟ₒ` です。二つの transport が、この二つの事実を同じ値の上に並べます。

```agda
    below : IsOrd (fst (lookup b γ)) → Entries (lookup f γ) (fst (lookup b γ))
          → (z : S)
          → Σ[ δ ∈ V ℓ ] (⟨ δ ∈ fst (lookup b γ) ⟩ × ⟨ fst z ∈ 𝒟ₒ (Lset δ) ⟩)
          → StepOf b f γ z
```

`below` は塔の分解をステップの証人に変えます。`b` での塔は各要素を分解します。要素 `z` は、`b` の下のある `δ` での段階の定義可能冪集合に坐っています。証人が名指すべきは、入力の下の入力と、その冪集合が `z` を含むような記録された値です。

```agda
    below ob ents z (δ , (δ∈ , hz)) =
      d , (LsetS δ oδ , ((δ∈ , ents d δ∈) , hz))
```

証人は、`δ` の台の要素である入力 `d` で与えられます。完備さにより、表はそこで正準な項目を記録します。そこの記録された値は `δ` での段階 (`L` の要素として提示されたもの) であり、分解によって `z` はその定義可能冪集合に属します。

```agda
      where
      oδ : IsOrd δ
      oδ = mem-ord {A = fst (lookup b γ)} ob δ δ∈
      d : S
      d = δ , isL-trans {x = fst (lookup b γ)} {y = δ} δ∈ (lookup b γ .snd)
```

二つの簿記の事実が構成を完成させます。`δ` の順序数性は `b` の順序数性から従います。順序数の要素は順序数だからです。そして `δ` は構成可能です。入力の基礎にある構成可能集合に属するからです。台の要素 `d` は、集合とこの証明書をひとまとめにします。

```agda
    above : Values (lookup f γ) (fst (lookup b γ)) → (z : S) → StepOf b f γ z
          → ⟨ fst z ∈ Lset (fst (lookup b γ)) ⟩
```

`above` は鏡像です。ステップの証人が要素を塔の中へ置きます。証人が名指すのは、入力の下の入力 `c`、そこで記録された値 `w`、そして `z` が `w` の定義可能冪集合に属することです。

```agda
    above vals z (c , (w , (rec , hz))) =
      Lset-in (fst (lookup b γ)) (fst c) (fst z) (rec .fst)
        (subst (λ u → ⟨ fst z ∈ 𝒟ₒ u ⟩) (vals c w (rec .fst) (rec .snd)) hz)
```

正しさが記録された `w` を `c` での塔と同一視するので、`z` はその段階の定義可能冪集合に属します。さらに塔の上向きの読みが、証人が携える `c` の順序数性を使って、`z` を `b` での塔の中へ置きます。

```agda
  step-Lset : ⟨ γ ⊨ StepAt v b f ⟩ → IsOrd (fst (lookup b γ))
            → Values (lookup f γ) (fst (lookup b γ))
            → Entries (lookup f γ) (fst (lookup b γ))
            → fst (lookup v γ) ≡ Lset (fst (lookup b γ))
```

上向きの補題はこう読みます。ステップ条件が環境で成立し、入力が順序数であり、表がその上で正しくて完備なら、値の枠で記録された値は入力での塔に等しい、と。

```agda
  step-Lset h ob vals ents =
    extensionalV {a = fst (lookup v γ)} {b = Lset (fst (lookup b γ))} pt
    where
```

階層の、同じ要素をもつ二つの集合は等しく、これが周囲の階層の外延性です。証明は各点の同値 `pt` を示し、パスの組み立てを外延性に任せます。

```agda
    fwd : (x : V ℓ) → ⟨ x ∈ fst (lookup v γ) ⟩
        → ⟨ x ∈ Lset (fst (lookup b γ)) ⟩
    fwd x hx = PT.rec (snd (x ∈ Lset (fst (lookup b γ)))) (above vals z)
      (StepAt-out v b f γ h (ok ob vals) z hx)
```

前向き：記録された値の要素 `x` は、ステップ条件が成立しているのでステップの証人を与えます。証人は「`x` が塔に属する」という命題へ消去され、`above` が証人からその命題を証明します。

```agda
      where
      z : S
      z = x , isL-trans {x = fst (lookup v γ)} {y = x} hx (lookup v γ .snd)
```

`above` を適用するには、`x` を台の要素として必要とします。その構成可能性は、記録された値の構成可能性から従います。`x` はその要素だからです。

```agda
    bwd : (x : V ℓ) → ⟨ x ∈ Lset (fst (lookup b γ)) ⟩
        → ⟨ x ∈ fst (lookup v γ) ⟩
    bwd x hx = PT.rec (snd (x ∈ fst (lookup v γ))) put
      (Lset-out (fst (lookup b γ)) x hx)
```

後ろ向き：塔は各要素 `x` を分解し、その定義可能冪集合が `x` を含むような、入力の下の段階を示します。分解は「`x` が記録された値に属する」という命題へ消去されます。

```agda
      where
      z : S
      z = x , isL-trans {x = Lset (fst (lookup b γ))} {y = x} hx
                (LsetS (fst (lookup b γ)) ob .snd)
```

ここでも `x` を台に載せる必要があります。その構成可能性は、入力での段階への所属から従います。その段階の `L` 要素としての提示が、順序数性 `ob` を取った `LsetS` です。

```agda
      put : Σ[ δ ∈ V ℓ ] (⟨ δ ∈ fst (lookup b γ) ⟩ × ⟨ x ∈ 𝒟ₒ (Lset δ) ⟩)
          → ⟨ x ∈ fst (lookup v γ) ⟩
      put s = StepAt-back v b f γ h (ok ob vals) z (below ob ents z s)
```

分解は `below` によってステップの証人に変えられ、ステップ条件の後ろ向きの読み `StepAt-back` が、証人を記録された値への所属に変えます。

```agda
    pt : (x : V ℓ) → (x ∈ fst (lookup v γ)) ≡ (x ∈ Lset (fst (lookup b γ)))
    pt x = ⇔toPath (fwd x) (bwd x)
```

各要素について、記録された値への所属と塔への所属は同じ命題です。二つの方向が同値を与え、外延性がそれを要素ごとに集合の等しさへ引き上げます。

```agda
  step-table : IsOrd (fst (lookup b γ))
             → Values (lookup f γ) (fst (lookup b γ))
             → Entries (lookup f γ) (fst (lookup b γ))
             → fst (lookup v γ) ≡ Lset (fst (lookup b γ))
             → ⟨ γ ⊨ StepAt v b f ⟩
```

下向きの補題は流れを逆にします。入力の順序数性、正しさ、完備さ、そして記録された値が塔であるという事実が与えられれば、ステップ条件は成立します。

```agda
  step-table ob vals ents q = StepAt-in v b f γ (ok ob vals) into back
    where
```

ステップ条件は、その二方向から導入されます。各要素への証人の存在と、すべての証人の健全性です。横条件は `ok` が両方のために一度に供給します。

```agda
    into : (z : S) → ⟨ fst z ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ z ∥₁
    into z hz = PT.map (below ob ents z)
      (Lset-out (fst (lookup b γ)) (fst z)
        (subst (λ u → ⟨ fst z ∈ u ⟩) q hz))
```

記録された値の要素 `z` は、まず同定 `q` に沿って塔へ運ばれ、塔によって分解されます。`below` がその分解を証人に変えます。証人は存在すれば十分です。

```agda
    back : (z : S) → StepOf b f γ z → ⟨ fst z ∈ fst (lookup v γ) ⟩
    back z s = subst (λ u → ⟨ fst z ∈ u ⟩) (sym q) (above vals z s)
```

逆に、証人は `above` によって `z` を塔の中に置き、輸送は `q` に沿って逆向きに走ります。

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

帰納は一回、入力の上で、メタ言語の中で行われます。近似とその定義域は固定したままです。動機はこう言います。近似がこの入力で記録するどんな値も、メタレベルの塔のそこでの値に等しい、と。動機は記録された**すべての**値を量化します。だから一価性がどこにも仮定として現れないのです。同じ入力で記録された二つの値は、どちらも同じ塔の値に釘づけになり、等しくなります。記録された値の一意性は、仮定ではなく帰納から読み出されます。

帰納のステップは、記録された値に対する `step-Lset` です。入力の下での正しさは、そのまま逐語的に帰納の仮定です。入力の下での完備さを使うのが、近似の値の条項を費やす場所です。この入力より下の入力は近似の定義域の下にもあります。定義域は順序数であり、順序数は推移的だからです。だから近似はそこで値を持ち、帰納の仮定がそれを塔の値と同一視します。その値は「単に」取り出されるだけで十分です。それについて証明するのは一つの所属だからです。

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

動機 `Value u` はこう言います。構成可能な `u` に対し、表の、第一成分が `u` である項目はすべて、塔の `u` での値を記録している、と。「`u` が構成可能」という前提が帯びられるのは、表の項目が台の要素で、その第一成分が構成可能集合だからです。帰納は、順序数への所属からこの前提を供給します。

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

定理は、`x` の基礎の集合の上で帰納を実行します。`x` は、記録された値が問題になっている入力です。所属に沿う帰納は階層で直接使えます。`u` の動機を証明するには、`u` のすべての要素の動機を証明します。`a` についての順序数性の仮定は、帰納のステップの内側で消費されます。

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

帰納のステップは、近似自身のステップ条項に `step-Lset` を適用することです。ステップは、値 `z` と入力 `u` を追加した環境で判定されるので、ステップの三つの枠は二つ後ろへずれます。これが `sh2` の仕事です。結論はそのまま動機です。記録された `z` は `u` での塔です。

```agda
      where
      d : S
      d = u , hu
      u∈a : ⟨ u ∈ fst (lookup a γ) ⟩
      u∈a = ApproxAt-dom f a γ h d z p
```

値と入力は、台の要素として旅をします。`d` は `u` に構成可能性 `hu` を包んでいます。近似の定義域の条項が、`u` が入力 `a` の下にあることを証明します。帰納がこのステップに届くのは、これがあればこそです。

```agda
      ou : IsOrd u
      ou = mem-ord {A = fst (lookup a γ)} oa u u∈a
```

`u` の順序数性は `a` の順序数性から従います。`u` は `a` の要素だからです。ステップがその立つ入力について必要とするのは、これです。

```agda
      vals : Values (lookup f γ) u
      vals c y c∈ q = IH (fst c) c∈ (snd c) y q
```

`u` の下での正しさは、そのまま逐語的に帰納の仮定です。`u` の要素 `c` に対し、第一成分が `c` である記録された対は、`c` での塔を記録します。`c` の構成可能性は帰納とともに届きます。帰納が所属からそれを供給するからです。

```agda
      ents : Entries (lookup f γ) u
      ents c c∈ = PT.rec
        (snd (pr (fst c) (Lset (fst c)) ∈ fst (lookup f γ))) named
        (ApproxAt-value f a γ h c (oa .fst {x = u} {y = fst c} c∈ u∈a))
```

`u` の下での完備さは、近似の値の条項を費やす場所です。`u` の下の `c` に対し、順序数 `a` の中の推移性が `c` が `a` の下にあることを与え、近似はそこで何らかの値を記録します。項目は単に存在するだけでよく、消去の対象は「正準な項目が記録される」という命題です。

```agda
        where
        named : Σ[ y ∈ S ] ⟨ pr (fst c) (fst y) ∈ fst (lookup f γ) ⟩
              → ⟨ pr (fst c) (Lset (fst c)) ∈ fst (lookup f γ) ⟩
        named (y , q) = subst (λ t → ⟨ pr (fst c) t ∈ fst (lookup f γ) ⟩)
          (IH (fst c) c∈ (snd c) y q) q
```

単に与えられただけの記録された値は、帰納の仮定によって塔と同定されます。輸送の後には、正準な項目が記録されています。完備さが求めるのはこれです。

## グラフは正しい値だけを認める

塔のグラフは、枠での値が入力での塔の値であると言います。そしてそれを、近似を通して言います。入力でのステップがその値であるような近似が、単に存在する、と。ほどけば、必要な材料はすべて手もとにあります。入力の下での正しさは、今完了した帰納から来ます。入力の下での完備さは、近似の値の条項から来て、同じ帰納によって運ばれます。最後にもう一度 `step-Lset` を適用すれば、記録された値は塔と同定されます。ゆえにグラフはその値を**決定**します。順序数でそれを満たすものは何であれ、メタレベルの塔のそこでの値です。

この読みが変数の枠の上に立つのは飾りではありません。実例化はそれぞれ異なる具体的な環境に住み、一方で述べた主張を他方へ運ぶには、全体の塔の記述を内側に抱えた充足を通さねばなりません。

```agda
module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where
  Lset-only : ⟨ γ ⊨ LsetGraphAt w b ⟩ → IsOrd (fst (lookup b γ))
            → fst (lookup w γ) ≡ Lset (fst (lookup b γ))
```

主張は、塔のグラフの値と入力の枠での充足と、入力の順序数性を受け取り、記録された値が塔であると結論します。グラフについて仮定するのは、それが成立することだけです。

```agda
  Lset-only h ob = PT.rec
    (setIsSet (fst (lookup w γ)) (Lset (fst (lookup b γ)))) read
    (LsetGraph-out w b γ h)
    where
```

グラフは、単なる証人へほどけます。すなわち、近似と、その充足と、値でのステップです。消去が正当なのは、目標が二つの h-集合の等しさ、つまり命題だからです。証人そのものが必要になるのは、その命題の内側だけです。

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

証人が渡すのは、入力の上の近似 `f`、その充足 `ha`、そして値でのステップ `hs` です。ステップの補題は、`f` で拡張した環境で適用されます。近似が新しく増えた枠ゼロを占め、値と入力は一つずつ後ろへ移ります。

```agda
      where
      vals : Values f (fst (lookup b γ))
      vals c z _ p = approx-val zero (suc b) (f ∷ γ) ha ob c z p
```

ステップの補題にとっての正しさは、前節の帰納を近似 `ha` に適用したものです。`f` が入力の下で記録する値はすべて、塔のそこでの値です。

```agda
      ents : Entries f (fst (lookup b γ))
      ents c c∈ = PT.rec (snd (pr (fst c) (Lset (fst c)) ∈ fst f)) named
        (ApproxAt-value zero (suc b) (f ∷ γ) ha c c∈)
```

完備さは近似の値の条項から来ます。下の各入力で、ある項目が単に記録されます。消去の対象は「正準な項目が記録される」という命題なので、欠けている証人は決して要りません。

```agda
        where
        named : Σ[ y ∈ S ] ⟨ pr (fst c) (fst y) ∈ fst f ⟩
              → ⟨ pr (fst c) (Lset (fst c)) ∈ fst f ⟩
        named (y , q) = subst (λ t → ⟨ pr (fst c) t ∈ fst f ⟩)
          (approx-val zero (suc b) (f ∷ γ) ha ob c y q) q
```

単に与えられただけの記録された値は、同じ帰納によってもう一度塔と同定され、輸送の後に記録されているのは正準な項目ちょうどです。

## 表は近似である

逆方向には証人が要りますが、正しくて完備な表がまさにそれです。`graph-table` は、そのような表を塔のグラフの充足に変えます。前章の条項を埋めるだけで、それ以上のことは何もしません。

近似の定義域の連言は、入力が定義域にあるという二つの言い方の間の同値であり、`Domain` と `Entries` がその二方向を証明します。`c` で記録された項目が `c` を界の下へ置き、`c` が界の下にあるときには `c` での正準な項目が記録されます。記録された組 `(c, y)` でのステップの連言は、`c` に対する `step-table` です。順序数の推移性が、表の正しさと完備さを `c` の下の入力へ制限します。ステップの補題がそこで消費するのはこれです。グラフが問う値は入力全体でのステップであり、これも `step-table` が、記録された値と塔の同定を入力にして与えます。

主張は、表 `h`、入力の順序数性、入力の上での表の三条件、そして記録された値が塔であるという主張を受け取ります。

```agda
module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where
  graph-table : (h : S) → IsOrd (fst (lookup b γ))
              → Values h (fst (lookup b γ)) → Entries h (fst (lookup b γ))
              → Domain h (fst (lookup b γ))
              → fst (lookup w γ) ≡ Lset (fst (lookup b γ))
```

塔のグラフが値と入力の枠で成立すると結論します。

```agda
              → ⟨ γ ⊨ LsetGraphAt w b ⟩
  graph-table h ob vals ents dom q = LsetGraph-in w b γ h approx
    (step-table (suc w) (suc b) zero (h ∷ γ) ob vals ents q)
    where
```

塔のグラフは、一つの近似と外側のステップから導入されます。近似は表そのものであり、拡張された環境に置かれます。外側のステップは入力に対する `step-table` であり、その正しさ・完備さ・塔との同定は、まさに手もとの仮定です。

```agda
    onDom : (c : S)
          → (⟨ ∃[ y ∶ S ] pr (fst c) (fst y) ∈ fst h ⟩
             → ⟨ fst c ∈ fst (lookup b γ) ⟩)
          × (⟨ fst c ∈ fst (lookup b γ) ⟩
             → ⟨ ∃[ y ∶ S ] pr (fst c) (fst y) ∈ fst h ⟩)
```

近似の定義域の条項は、`c` が定義域にあるという二つの言い方の間の同値です。第一成分が `c` である項目が何か記録されていることと、`c` が入力の下にあること。両方向が要ります。近似の定義域の条件は、これらを逆の順で使うからです。

```agda
    onDom c = (λ hy → PT.rec (snd (fst c ∈ fst (lookup b γ))) named hy)
            , (λ c∈ → ∣ LsetS (fst c) (mem-ord {A = fst (lookup b γ)} ob (fst c) c∈)
                     , ents c c∈ ∣₁)
```

同値を右へ読むと、`c` での記録された項目と表の完備さが、正準な項目を示します。それは `L` の要素として提示された `c` での段階の記録であり、`c` の順序数性は入力の順序数性から来ます。左へ読むと、表の定義域の条件が `c` を入力の下へ置きます。

```agda
      where
      named : Σ[ y ∈ S ] ⟨ pr (fst c) (fst y) ∈ fst h ⟩
            → ⟨ fst c ∈ fst (lookup b γ) ⟩
      named (y , p) = dom c y p
```

補助の `named` は、証人に定義域の条件を読んだものです。第一成分が `c` である項目が存在するので、`c` は入力の下にあります。その内容は、表の第三の条件の一回の適用です。

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

ステップの連言は、記録されたそれぞれの組 `(c, y)` で証明されます。値 `y`、入力 `c`、表 `h` を追加した環境の中で、ステップ条件は表の枠を通して値の枠と入力の枠を結びます。`c` に対する `step-table` がまさにこれを確立し、同定 `fst y ≡ Lset (fst c)` は記録された組での正しさが供給します。

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

`c` についての二つの事実が、記録された組から読み取れます。その基礎の集合は入力の下にあり、これは定義域の条件から。そしてそれが順序数であることは、入力の順序数性からです。

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

`c` の下での正しさと完備さは、表自身の条件を `c` の下の入力に制限したものです。正しさは定義域の仮定を制限し、完備さは入力の推移性を使って、`c` の下の入力が入力の下にもあることを見ます。この推移性を使うのは、本章でここが二度目で最後です。

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

二つの連言を組み立てると、表そのものが近似になります。定義域の条項が今証明した同値であり、ステップの条項がその前のものです。正しくて完備な表が入力の下の階層の記録を含む、と言うのはこの意味です。

## 順序対のグラフ

表は**作られ**なければなりません。`L` の内側で使える作り手は置換だけであり、置換はグラフを要求します。置換は、関数グラフの記述のあとで表を集めます。表の項目は入力 `c` と値 `z` の順序対であり、`z` が `c` での塔のグラフを満たすとき、グラフはその項目について成立します。塔が渡り歩く台は定数に固定されています。一つの存在量化が塔の値を束縛し、対の読み出しが項目を「入力と束縛された値」の対と等置し、塔のグラフが、束縛された値が正しいことを言います。

この二つの読み出しは、文を**パラメータ**として受け取り、文自身の等式を仮定として受け取ります。本章の呼び出しでは `refl` です。枠組みは文に対して一般的です。渡された論理式が何であれ、それが順序対のグラフを綴っているという仮定のもとで、読み出しは語ります。等式は文とともに渡されるので、読み出しの適用にそれ以上の議論は要りません。

## 内部の階層

`Recorded` は、`α` における内部の階層が集めるべきクラスに名前を与えます。基礎の集合が `α` の下にある入力 `c` と、塔の `c` での値の対であり、そのほかには何もありません。`IsHier` は、モデルのある集合がこのクラスを要素ごとに実現することを言います。台の要素 `z` それぞれに対し、その集合への所属は、`z` がそのような対を提示するときにちょうど成立します。この主張の両方向が使われます。`HierOf` は、実現する集合をその仕様とともに集めます。構成が作るのはこの形であり、二つの読み出しが消費するのもこの形です。

二つの読み出しは、仕様を通して届く**変数**の実現集合の上に立ちます。これから作る構成が、自分の作っている集合にそれを適用できるようにするためです。外向きの読みは、階層の対の単射性をある要素に適用します。実現集合の項目は、`B` の下の入力と塔のそこでの値を名指します。内向きの読みは、正準な対をモデルの要素として示します。これはモデル自身の対の構成が与えますが、入力の順序数性も要ります。それがなければ、塔のそこでの値をそもそも名指せないからです。

そして構成です。順序数の上の、所属に沿う帰納が一回。`α` において、対のグラフは下のすべての入力で関数的です。帰納の仮定がその入力までの階層を渡し、`graph-table` がそれを塔のグラフの充足に変え、`Lset-only` がそれを満たすものはほかにないと言います。置換が対をモデルの集合に集めます。各入力の順序数性は `mem-ord` から来て、関数性の要求は `mereFunct` で満たされます。入力での値は判定ではなく構成だからです。

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

`Recorded B z` は命題であり、こう言います。基礎の集合が `B` の下にある台の要素 `c` のうち何かに対して、`z` の基礎の集合は `fst c` と塔の `c` での値の順序対である、と。二つの h-集合の等しさはそれ自体命題なので、これは命題の上での選言の集まりです。

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

`IsHier B h` は、`h` が提示する集合が、記録されたクラスを要素ごとに実現することを言います。各 `z` で、集合への所属と記録されていることは同じ命題です。どちらの方向も捨てられません。それぞれに使い道があるからです。所属だけがあればよしとすると、よそ者が入ります。記録だけがあればよしとすると、あるべき対が抜け落ちます。

```agda
HierOf : V ℓ → Type (ℓ-suc (ℓ-suc ℓ))
HierOf B = Σ[ h ∈ S ] IsHier B h
```

`HierOf B` は、実現する集合をその仕様とともに集めます。この対こそ、帰納がそれぞれの順序数で作るものであり、その二つの成分は、構成に対して誰もが問う二つの問いに答えます。それは何か。なぜそれが資格をもつのか。

```agda
module _ (B : V ℓ) (oB : IsOrd B) (h : S) (sp : IsHier B h) where
```

二つの読み出しは、仕様を伴う変数の実現集合に対して述べられます。これから作る構成が、帰納がいま立っている段階がどこであれ、自分の作っている集合にそれを適用できるようにするためです。

```agda
  hier-out : (c z : S) → ⟨ pr (fst c) (fst z) ∈ fst h ⟩
           → ⟨ fst c ∈ B ⟩ × (fst z ≡ Lset (fst c))
```

外向きの読みです。`c` と `z` の対が実現集合の要素なら、`c` は `B` の下にあり、`z` は塔の `c` での値です。どちらの結論も、その要素に仕様を適用したことから従います。

```agda
  hier-out c z p = PT.rec
    (isProp× (snd (fst c ∈ B)) (setIsSet (fst z) (Lset (fst c)))) read
    (subst ⟨_⟩ (sp k) p)
    where
```

その要素の所属は、仕様に沿って記録の命題へ運ばれます。それは切り詰められた存在です。消去の対象は命題の対、したがって命題なので、証人をここで消費してかまいません。

```agda
    k : S
    k = pr (fst c) (fst z)
      , isL-trans {x = fst h} {y = pr (fst c) (fst z)} p (h .snd)
```

その要素自身も、台の要素として名指す必要があります。基礎の集合の順序対は構成可能です。`h` が提示する構成可能集合に属するからです。

```agda
    read : Σ[ d ∈ S ] (⟨ fst d ∈ B ⟩
             × (pr (fst c) (fst z) ≡ pr (fst d) (Lset (fst d))))
         → ⟨ fst c ∈ B ⟩ × (fst z ≡ Lset (fst c))
    read (d , (d∈ , eq)) =
        subst (λ t → ⟨ t ∈ B ⟩) (sym (pr-inj eq .fst)) d∈
```

記録された命題は、`B` の下の `d` と、その要素が「`d` と塔の `d` での値」の対に等しいことを示します。階層の対の単射性がこの等式を分解します。第一成分の同定は `c` を `d` と同一視し、所属を「`c` が `B` の下にある」ことへ移します。第二成分の同定は `z` を塔の `d` での値と同一視し、最初の同定がそれを塔の `c` での値へ変えます。

```agda
      , (pr-inj eq .snd ∙ cong Lset (sym (pr-inj eq .fst)))

  hier-in : (c : S) → ⟨ fst c ∈ B ⟩ → ⟨ pr (fst c) (Lset (fst c)) ∈ fst h ⟩
  hier-in c c∈ = subst (λ t → ⟨ t ∈ fst h ⟩) (prʟ-fst c (LsetS (fst c) oc))
    (subst ⟨_⟩ (sym (sp k)) ∣ c , (c∈ , prʟ-fst c (LsetS (fst c) oc)) ∣₁)
```

内向きの読みです。正準な項目、すなわちモデル自身の「`c` と塔の `c` での値」の対は、要素です。仕様は、記録されたクラスが実現されると言い、典型的な対は `c` 自身を入力とする記録の命題の証人です。そして項目がモデルの対と等しいことは、その対の定義の読みから得られます。

```agda
    where
    oc : IsOrd (fst c)
    oc = mem-ord {A = B} oB (fst c) c∈
    k : S
    k = prʟ c (LsetS (fst c) oc)
```

`c` の順序数性は `B` の順序数性から来ます。それがあってはじめて、塔の `c` での値を `L` の要素として提示でき、モデルの対が第二成分として必要とするのはこれです。

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

帰納のステップ関数は、対のグラフを、自分自身の等式を携えた**変数の文**として保ちます。実例化先の閉じた文を書き出すのではありません。等式は文とともに渡されるので、以下のどの読み出しも呼び出しで `refl` を仮定として受け取ります。

```agda
    build : (φ : Formula S 2) → φ ≡ PairGraphAt zero (suc zero)
          → (α : V ℓ)
          → ((δ : V ℓ) → ⟨ δ ∈ α ⟩ → ⟨ isL δ ⟩ → IsOrd δ → HierOf δ)
          → ⟨ isL α ⟩ → IsOrd α → HierOf α
```

ステップは、文とその等式、順序数 `α`、その二つの証明書、そして帰納の仮定を受け取ります。`α` のすべての要素で階層はすでに作られています。ステップは、`α` での階層とその仕様を返さねばなりません。

```agda
    build φ qφ α IH hα oα = r .fst .fst , spec
      where
      A : S
      A = α , hα
```

`α` での階層は、実現者の第一成分であり、置換がそれを作ったのちに一度取り出されます。`A` は台の要素として提示された `α` で、置換が定義域を消費する形です。

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

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

`α` の下では、二つの補助構成がデータに名前を与えます。入力 `c` での値は `c` での段階であり、段階の提示によって `L` の要素です。`c` の順序数性は `α` の順序数性から来ます。`c` での項目は、モデル自身の「`c` とその値」の順序対で、記録されたクラスが求める形です。

```agda
      below : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) (k : S)
            → ⟨ (value c c∈ ∷ k ∷ c ∷ []) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩
      below c c∈ k = graph-table zero (suc (suc zero)) (value c c∈ ∷ k ∷ c ∷ [])
        (hc .fst) oc
```

塔のグラフは、`α` の要素 `c` のために記録された値で成立します。帰納の仮定を費やすのはここです。仮定は `c` での階層、すなわち入力 `c` の上で正しくて完備な表を渡します。これは `graph-table` が求めるものそのものです。環境には、値と、グラフ自身の量化子のための新しい枠と、入力が載ります。

```agda
        (λ d z _ p → hier-out (fst c) oc (hc .fst) (hc .snd) d z p .snd)
        (hier-in (fst c) oc (hc .fst) (hc .snd))
        (λ d z p → hier-out (fst c) oc (hc .fst) (hc .snd) d z p .fst)
        refl
```

表の三条件は、`c` での階層の仕様から読まれます。正しさは、記録されたすべての値が塔のそこでの値であると言い、完備さは正準な項目が記録されると言い、定義域の条件はほかには何も記録されないと言います。最後の引数 `refl` は、順序対のグラフ自身の等式です。

```agda
        where
        oc : IsOrd (fst c)
        oc = mem-ord {A = α} oα (fst c) c∈
        hc : HierOf (fst c)
        hc = IH (fst c) c∈ (snd c) oc
```

`c` の順序数性は `α` の順序数性から来ます。それがあれば、帰納の仮定は `c` での階層を、構成可能集合と仕様とともに渡します。

（holds)正準な項目はどれも、順序対のグラフを満たします。`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∈))
```

（only)`c` でグラフを満たすほかのどんな inhabitant も、正準な項目と等しくなります。グラフは、塔の値 `z` と、`(z, c)` で成立する塔のグラフへほどけます。塔のグラフはその値を決定し、対の単射性が二つの項目を同一視し、等式はこれらのパスの合成です。

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

対の証人は、塔の値 `z` と、`k` を「`c` と `z` の対」と同定する等式 `q` に分かれます。基礎の集合が等しければ台の要素は等しい。`Σ≡Prop` が目標をこれへ帰着させます。

```agda
        where
        read : PairOf zero (suc zero) (k ∷ c ∷ []) φ qφ → k ≡ entry c c∈
        read (z , (q , hg)) = Σ≡Prop (λ t → snd (isL t))
          ( q
```

`(z, c)` での塔のグラフは塔の値を決定します。値・正準な項目・入力を追加した環境で `Lset-only` を適用すれば、`z` は塔の `c` での値です。`c` の順序数性は `α` の順序数性から来ます。

```agda
          ∙ cong (pr (fst c))
              (Lset-only zero (suc (suc zero)) (z ∷ k ∷ c ∷ []) hg
                (mem-ord {A = α} oα (fst c) c∈))
          ∙ sym (prʟ-fst c (value c c∈)) )
```

三つのパスを合成すれば、`k` は「`c` と塔の `c` での値」の対であり、それは自分の定義の読みを通して読んだ正準な項目です。

（fc)`c` での関数性は、置換が求める可縮なファイバーです。正準な項目がグラフの inhabitant であり、どんな inhabitant もそれと等しくなります。`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∈) ∣₁
```

置換がすぐに項目を集めます。`α` の中の入力にわたって、各入力とその一意に定まる値の対がモデルの一つの集合となり、それがその対のクラスをちょうど実現するという主張とともに提示されます。`α` での内部の階層が `L` の集合として存在する瞬間は、ここです。

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

      spec : IsHier α (r .fst .fst)
      spec z = ⇔toPath toRec fromRec
        where
```

残るのは、集められた集合が記録されたクラスを実現することの確認です。仕様は、要素ごとに、収集された集合への所属と、記録された対であることとを比較します。比較の両方向を別々に証明し、各点の同値へ組み合わせます。

```agda
        toRec : ⟨ fst z ∈ fst (r .fst .fst) ⟩ → ⟨ Recorded α (fst z) ⟩
        toRec hz = PT.rec squash₁ conv (subst ⟨_⟩ (r .fst .snd z) hz)
          where
```

収集された集合への所属を外へ読み出します。置換の仕様がそれを、`α` の要素 `c` で、`c` での値が順序対のグラフを満たすという形に変えます。消去が正当なのは、記録されたクラスが命題だからです。

```agda
          conv : Σ[ c ∈ S ] (⟨ fst c ∈ α ⟩ × ⟨ (z ∷ c ∷ []) ⊨ φ ⟩)
               → ⟨ Recorded α (fst z) ⟩
          conv (c , (c∈ , hp)) = ∣ c , (c∈ , cong fst (only c c∈ z hp)
                                            ∙ prʟ-fst c (value c c∈)) ∣₁
```

証人に対しては、一意性が、`c` で記録された値が正準な項目に等しいと言い、正準な項目はモデルの「`c` と塔の `c` での値」の対に等しくなります。基礎の集合がそれに従い、これが「記録されている」ことの要求そのものです。

```agda
        fromRec : ⟨ Recorded α (fst z) ⟩ → ⟨ fst z ∈ fst (r .fst .fst) ⟩
        fromRec hz = subst ⟨_⟩ (sym (r .fst .snd z)) (PT.map conv hz)
          where
```

内側へ読みます。記録された対は、`α` の下の入力と塔のそこでの値を示します。順序対のグラフはその入力の正準な項目で成立し、収集された集合はその項目を含みます。

```agda
          conv : Σ[ c ∈ S ] (⟨ fst c ∈ α ⟩
                   × (fst z ≡ pr (fst c) (Lset (fst c))))
               → Σ[ c ∈ S ] (⟨ fst c ∈ α ⟩ × ⟨ (z ∷ c ∷ []) ⊨ φ ⟩)
```

証人は、記録された提示からグラフの提示へ変換されます。入力はそのままで、基礎の集合が典型的な対と等しいという等式が、そこでの順序対のグラフの充足になります。

```agda
          conv (c , (c∈ , eq)) = c , (c∈
            , subst (λ t → ⟨ (t ∷ c ∷ []) ⊨ φ ⟩) (sym zeq) (holds c c∈))
            where
            zeq : z ≡ entry c c∈
            zeq = Σ≡Prop (λ t → snd (isL t))
```

この等式は、`z` が `c` の正準な項目と同じ集合を提示すると言います。したがって対の要素たちは等しく、`holds` をこのパスに沿って運べば、`z` と `c` での順序対のグラフの充足が得られます。

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

hierL : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → S
hierL α hα oα = hierAt α hα oα .fst
```

ある順序数での内部の階層とは、帰納が作る実現集合を `L` の要素として提示したものです。それは構成可能な順序数ごとに存在します。つまり、モデルは今や、自分の各順序数に対して、「その順序数の下の順序数と塔のそこでの値」の順序対をちょうど要素とする集合を含むのです。

```agda
hierL-spec : (α : V ℓ) (hα : ⟨ isL α ⟩) (oα : IsOrd α)
           → IsHier α (hierL α hα oα)
hierL-spec α hα oα = hierAt α hα oα .snd
```

仕様は構成とともに渡ります。帰納が渡す実現集合は、その順序数で `IsHier` を両方向に満たします。内部の階層のその後のすべての使用は、この説明と照らして検査されます。

## 外部の階層はグラフを満たす

内部の階層は、`graph-table` と `Lset-only` によって作られました。それぞれの順序数で、帰納の仮定が下の表を渡し、二つの補題がそれを成立したグラフと一意な値に変えます。最後の主張は、今度は逆に走ります。仕様 `hierL-spec` が入力の上での表の条件を渡し、`Lset-defines` がそれを `graph-table` に渡します。塔のグラフは記録された値で成立し、隣にある `Lset-only` は、満たすものがほかにないと言います。こうして内部のグラフとメタレベルの塔は、構成可能な順序数ごとに両方向で一致します。

```agda
module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where
  Lset-defines : IsOrd (fst (lookup b γ))
               → fst (lookup w γ) ≡ Lset (fst (lookup b γ))
               → ⟨ γ ⊨ LsetGraphAt w b ⟩
```

主張は、入力の順序数性と、記録された値が塔のそこでの値であるという主張を受け取り、塔のグラフが成立すると結論します。これは前節の内向きの読みであり、構成可能な順序数ごとに内部の階層が存在するので、それぞれの場所で使えます。

```agda
  Lset-defines ob q = graph-table w b γ H ob
    (λ c z _ p → hier-out (fst (lookup b γ)) ob H sp c z p .snd)
    (hier-in (fst (lookup b γ)) ob H sp)
    (λ c z p → hier-out (fst (lookup b γ)) ob H sp c z p .fst)
    q
```

ここで名指される集合は、入力での内部の階層であり、その仕様が三つの表の条件として読まれます。正しさと完備さは `hier-out` の二方向です。内部の表の項目は、入力が下にあり、値が塔のそこでの値であることを示し、下のすべての入力で正準な項目が記録されます。定義域の条件は `hier-in` の側の対応物です。記録されるのはそのような対だけです。

証明は、入力での内部の階層を名指し、その仕様を両方向に読み出します。正しさは、内部の表が入力の下で記録する値がすべて塔のそこでの値であると言い、完備さは正準な項目が記録されていると言い、定義域の条件が表を閉じます。最後の仮定 `q` が、記録された値を塔と同定します。この四つの入力は、`graph-table` が消費するものそのものです。

```agda
    where
    H : S
    H = hierL (fst (lookup b γ)) (lookup b γ .snd) ob
    sp : IsHier (fst (lookup b γ)) H
    sp = hierL-spec (fst (lookup b γ)) (lookup b γ .snd) ob
```

入力での内部の階層が存在するのは、入力が構成可能な順序数だからです。そしてその仕様は、帰納が証明した所属の同値そのものです。この二つの事実を合わせれば、塔がすべての段階で、モデルの内部に、ほかには何も伴わずに記録されていると言えます。

## まとめ

`approx-val` は、入力の上の所属に沿う帰納を一回使って、近似が記録するすべての値がメタレベルの塔のその入力での値に等しいことを証明します。一価性の仮定はどこにもありません。同じ入力で記録された二つの値が等しいことは、ここから直接読み出せます。`Lset-only` と `Lset-defines` は、グラフと塔の間の二方向であり、後者が `hierL` を作るときに使われます。`hierL` はある順序数での内部の階層、`L` の要素であり、その要素は「その順序数の下の順序数と塔のそこでの値」の順序対ちょうどです。仕様は、帰納が証明した所属の同値です。

ここで表にされる段階は順序数で添字づけられ、順序数は階層の集合です。ホストの宇宙レベルは型の大きさの添字であり、塔の添字になることはありません。