---
title: "数えられた始集合から Skolem 包を数える"
module: L.GCH.HullCounting
lang: ja
site: "Bedrock"
description: "数えられた始集合から Skolem 包を数える"
stage: "GCH の証明"
reading_order: 117
canonical: https://bedrock.institute/ja/L.GCH.HullCounting.html
html: L.GCH.HullCounting.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/HullCounting.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Axioms.Full, L.Axioms.Infinity, L.Axioms.Numerals, L.Coding.Model, L.Coding.Expressions, L.Coding.CodeConstructibility, L.Coding.Injection, L.Cardinal, L.InjectionComposition, L.DefinableInjection, L.GCH.LeastWitnessMap, L.GCH.CardinalSquareLaw, L.Stage, L.Coding.EnvironmentSet, L.GCH.AdequateStages, L.Coding.SatisfactionGraphSet, L.GCH.SkolemHull, L.GCH.ConstructibleHull, L.GCH.StageCountingTools, L.GCH.FiniteSequenceCoding]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.HullCounting.md, https://bedrock.institute/zh/L.GCH.HullCounting.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
小さな集合を定義可能な最小の証人について閉じても、無限基数による上界は保たれるはずです。この章では、始集合が無限基数へ単射するなら、その Skolem 包も同じ基数へ単射することを `L` の内部で示します。

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

排中律は、和集合の要素が左側に属するかどうかなどの局所的な判定を与えます。古典的推論は一つの明示的な仮定として入り、得られる上界はその仮定を正確に記録します。

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

宇宙レベル `ℓ` と、レベル `ℓ-suc ℓ` の命題に対する排中律を固定します。内部集合、符号化されたグラフ、切り詰められた証人は、すべてこの固定した仮定のもとで構成されます。

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

符号化されたグラフは、等号と所属をもつ一階言語で表します。連言、選言、否定、存在量化によって場合を記述し、充足関係は周囲の累積階層で解釈します。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ¬̇_; ∃̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

議論では順序数段階とその構成可能な要素との間を行き来します。推移性により要素も `L` にとどまり、順序数の所属と段階の累積性により、各対象を定義可能な選択に十分大きい段階へ入れられます。

```agda
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-layer; layer-trans )
open import L.Ordinal {ℓ} using ( mem-ord; #∈ω )
open import L.Ordinal.Stages {ℓ} lem using ( Lset-cumul; ord∈Lset-suc )
```

数え上げに用いる写像は、それ自身が `L` の集合でなければなりません。分出で部分グラフを作り、対と和集合で符号を構成し、妥当性によって適用、一価性、定義域の内部論理式を集合論的な意味と結びつけます。

```agda
open import L.Axioms.Basic {ℓ} using ( LsetS; ∅ʟ )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Axioms.Numerals {ℓ} using ( pairʟ; unionʟ )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; appAt; appAt-adequate; svAt-out; domAt-in )
```

内部の単射は、定義域が正確で、一価かつ単射的であり、値域に上界をもつ構成可能なグラフによって証されます。`InjCode` は具体的なグラフを保ち、`InjL` はその存在命題だけを保ちます。

```agda
open import L.Coding.Expressions {ℓ} using ( numL; tagAtL; tagAtL-adequate )
open import L.Coding.CodeConstructibility {ℓ}
  using ( sglʟ; sglʟ-in; sglʟ-out; cupʟ; cupʟ-inl; cupʟ-inr; cupʟ-out )
open import L.Coding.Injection {ℓ} lem using ( injAt-out; module Extract )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
```

数え上げの証明では内部の単射を合成します。定義可能な写像は一意な値をもつ論理式を構成可能なグラフにし、最小証人の選択は Skolem 閉包にそのような写像を与え、内部の積はタグ付きの対を収めます。

```agda
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
open import L.GCH.LeastWitnessMap {ℓ} lem using ( module Least )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( prodL; prodL-in; module Relation )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )
```

最小の証人は一つの共通する構成可能段階の中で選びます。有界順序数がパラメータをそこへ集め、強化された十分な段階であることが充足関係を安定させ、充足グラフが選択を `L` の集合として記録します。

```agda
open import L.Stage {ℓ} lem using ( LeastOrd; isPropLeastOrd; leastOrd; stage; stage-ord; stage-mem )
open import L.Ordinal using ( boundingOrd )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet; envSet-in )
open import L.GCH.AdequateStages {ℓ} lem using ( Superadequate )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )
```

Skolem 包は、始集合から最小証人による閉包を反復して得られます。その構成可能な提示が選択に必要な段階の上界を与え、凝縮が包を対応する構成可能構造と同一視します。

```agda
open import L.GCH.SkolemHull {ℓ} lem using ( module Frame; module HullStage )
open import L.GCH.ConstructibleHull {ℓ} lem using ( module Condense′; module Telescope )
open import L.GCH.StageCountingTools {ℓ} lem
  using ( isPropInjCode; injcode-resp; injFo; module InjFo; pinAt; pin-in; pin-out; seq-map; Lω
        ; limit-stage-counted )
```

各閉包段階は論理式の符号と有限なパラメータ列で添字づけられます。論理式の形は可算であり、無限基数上の有限列は平方則で抑えられ、整礎帰納法が数え上げに現れる内部基数についてその平方則を与えます。

```agda
open import L.GCH.FiniteSequenceCoding {ℓ} lem using ( seqL; seqL-in; seq-count )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( prod-inj; ω⊆; Goal; module Step )
open import L.Cardinal {ℓ} lem using ( IsCardinalL )
open import V.Hierarchy {ℓ} using ( regularityV )
import Cubical.Induction.WellFounded as WF
```

グラフの二つの引数がそれぞれ等しさで同一視されるとき、二項の移送によってグラフへの所属証明を両方の同一視に沿って一度に移せます。したがって等しさによる置換は符号化された関係と両立します。

```agda
open import Cubical.Foundations.Prelude using ( subst2 )
```

タグ `0` と `1` は異なるので、タグ付き単射の二つの分岐は交わりません。命題値のファイバーをもつ依存対の等しさは第一成分の等しさに帰着するため、構成可能性の証明は数え上げに影響しません。

```agda
open import Cubical.Data.Nat.Properties using ( znots; snotz )
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.HLevels using ( isProp×; isSetΣSndProp )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
```

von Neumann 数項をタグに用い、`ω` がそれらを集め、後続が有限な進み方を表します。空集合は単元集合からの単射の値となり、命題的切り詰めは代表を選ばずに存在を記録します。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; ω; sucV )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅ )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
```

符号化された単射の存在は命題的に切り詰められます。数え上げに必要なのは証人となるグラフの存在だけだからです。したがって除去は命題に対してのみ行い、結果がグラフの選び方に依存しないようにします。

```agda
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

周囲の集合について、`x ∈ˢ y` は `x` が `y` に属するという命題です。符号化された関数の定義域と値域の条件は、最終的に底集合上のこの関係へ帰着します。

```agda
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
```

構成可能モデルの台を `S` と書きます。その要素は周囲の集合と、それが `L` に属することの証明との対です。この証明は命題なので、底集合が構成可能な要素を等しさまで一意に定めます。

```agda
module SL = hPropStructure 𝒮ʟ using ( S )
open SL using ( S )
```

構成可能な定数をもつ論理式は `L` の内部で評価でき、周囲の階層へも射影できます。推移性により二つの読み方は一致するので、内部で証明したグラフの主張を底集合間の通常の所属として使えます。

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

`Holds F x y` は、`x` と `y` の底集合の順序対が底のグラフ `F` に属することを意味します。これは、議論に現れる各符号化された適用論理式が表す周囲の関係です。

```agda
Holds : S → S → S → Type (ℓ-suc ℓ)
Holds F x y = ⟨ pr (fst x) (fst y) ∈ fst F ⟩
```

要素 `nn k : S` は、周囲の von Neumann 数項 `# k` とその構成可能性の証明との対です。とくに `nn 0` と `nn 1` は、`L` の外へ出ることなく内部のタグとして働きます。

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

`S` の二つの要素の底集合が等しければ、要素そのものも等しくなります。第二成分は構成可能性の証明だけなので、証明無関係性によって第一成分の等しさを依存対の等しさへ持ち上げられます。

```agda
S≡ : {x y : S} → fst x ≡ fst y → x ≡ y
S≡ = Σ≡Prop (λ v → snd (isL v))
```

台 `S` は h-集合です。第一成分が属する累積階層は h-集合であり、構成可能性の証明からなる各ファイバーは命題なので、`S` のすべての等式型は命題になります。

```agda
isSetS : isSet S
isSetS = isSetΣSndProp setIsSet (λ v → snd (isL v))
```

最初の二つの変数の枠の De Bruijn 索引に名前が付けられます。この章の符号化された論理式は、一度に多くとも八つの枠しか扱わないからです。

```agda
private
  i0 : ∀ {k} → Fin (suc k)
  i0 = zero
  i1 : ∀ {k} → Fin (suc (suc k))
  i1 = suc i0
```

`i2`、`i3`、`i4` は、それぞれ変数位置 2、3、4 を表します。各添字は直前の添字の後続であり、多相的な末尾の長さ `k` によって、さらに変数が利用できる場合にもその位置が有効に保たれます。

```agda
  i2 : ∀ {k} → Fin (suc (suc (suc k)))
  i2 = suc i1
  i3 : ∀ {k} → Fin (suc (suc (suc (suc k))))
  i3 = suc i2
  i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))
```

`i4` の定義式を与えた後、同じ後続のパターンで位置 5 と 6 を定めます。これらの名前により、入れ子になった束縛子が生む位置のずれを符号化された論理式の型で確認できます。

```agda
  i4 = suc i3
  i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k))))))
  i5 = suc i4
  i6 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc k)))))))
  i6 = suc i5
```

第七の枠が最後であり、この八つの索引が本章で使うすべての変数の位置を覆います。

```agda
  i7 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc k))))))))
  i7 = suc i6
```

順序数はその自身の段階に含まれます。順序数の各要素はそれ自身順序数であり、累積的な構成が、順序数のすべての要素をその順序数が索引づける段階の中に置きます。

```agda
ord⊆Lset : (α : V ℓ) → IsOrd α → (z : V ℓ) → ⟨ z ∈ α ⟩ → ⟨ z ∈ Lset α ⟩
ord⊆Lset α oα z z∈α =
  Lset-cumul z α oz oα z∈α (ord∈Lset-suc z oz)
  where
  oz : IsOrd z
```

`z ∈ α` であり `α` が順序数なので、`z` 自身も順序数です。これにより `z` はその後続段階に属し、さらに `z ∈ α` に沿って累積性を用いると `z ∈ Lset α` が得られます。

```agda
  oz = mem-ord {A = α} oα z z∈α
```

構成可能集合 `D₁` と `D₂` を固定します。それらの内部の二項和集合は二つの単射をまとめる共通の定義域であり、その所属原理から二つの包含と切り詰められた場合分けが得られます。

```agda
module Union2 (D₁ D₂ : S) where
```

この和は、二つの集合の内部の和です。

```agda
  D : S
  D = cupʟ D₁ D₂
```

左側の要素は、和の左の規則によって含められます。

```agda
  in₁ : (z : S) → ⟨ fst z ∈ fst D₁ ⟩ → ⟨ fst z ∈ fst D ⟩
  in₁ z = cupʟ-inl D₁ D₂ (fst z)
```

右側の要素は対称的に含められます。

```agda
  in₂ : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → ⟨ fst z ∈ fst D ⟩
  in₂ z = cupʟ-inr D₁ D₂ (fst z)
```

`z ∈ D₁ ∪ D₂` なら、`z` が左側または右側に属することだけが得られます。この選言は命題的に切り詰められています。所属は、ある提示添字が `z` を名指すことを保ちますが、具体的な添字は保たないからです。

```agda
  out : (z : S) → ⟨ fst z ∈ fst D ⟩ → ∥ ⟨ fst z ∈ fst D₁ ⟩ ⊎ ⟨ fst z ∈ fst D₂ ⟩ ∥₁
  out z = cupʟ-out D₁ D₂ (fst z)
```

`κ` をタグ `0` と `1` を含む構成可能集合とし、`E₁` と `E₂` がそれぞれ `D₁` と `D₂` から `κ` への単射を符号化するとします。値にタグを付けると、`D₁ ∪ D₂` から `κ × κ` への一つの単射にまとめられます。この構成では `κ` が順序数である必要はありません。

```agda
module TagUnion (κ : S) (0∈κ : ⟨ # 0 ∈ fst κ ⟩) (1∈κ : ⟨ # 1 ∈ fst κ ⟩)
                (D₁ D₂ E₁ E₂ : S) (c₁ : InjCode E₁ D₁ κ) (c₂ : InjCode E₂ D₂ κ) where
```

`D = D₁ ∪ D₂` と書きます。どちらか一方の集合の要素は `D` に属し、`D` の各要素からは、二つの集合のいずれかに由来するという切り詰められた証明が得られます。

```agda
  open Union2 D₁ D₂ public using ( D; in₁; in₂; out )
```

それぞれの符号化された単射は、その底にある関数と、グラフが符号化の言う通りにちょうど成立する証明を抽出します。

```agda
  module X₁ = Extract E₁ D₁ (fst c₁) (fst (snd c₁)) using ( toFun; toFun-graph )
  module X₂ = Extract E₂ D₂ (fst c₂) (fst (snd c₂)) using ( toFun; toFun-graph )
```

`Mem z` は `z` が和集合の定義域 `D` に属するという命題です。入力にこの証明を添えることで、場合分けされた関数を評価するために必要な定義域の証拠がちょうど得られます。

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem z = ⟨ fst z ∈ fst D ⟩
```

左の定義域への所属は排中律で判定でき、この判定こそ、タグ付きの単射を作るための場合分けです。

```agda
  Case : S → Type (ℓ-suc ℓ)
  Case z = ⟨ fst z ∈ fst D₁ ⟩ ⊎ (⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥)
```

排中律は、和のすべての要素が左の定義域から来たかどうかを判定します。

```agda
  decide : (z : S) → Case z
  decide z = lem (fst z ∈ fst D₁)
```

左の定義域に属さない要素は、右の定義域に属します。和の中の所属は二つの側に分かれ、左側は仮定された失敗と矛盾します。

```agda
  off : (z : S) → Mem z → (⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥) → ⟨ fst z ∈ fst D₂ ⟩
  off z m no = PT.rec (snd (fst z ∈ fst D₂))
    (λ { (inl h) → Empty.rec (no h) ; (inr h) → h }) (out z m)
```

それぞれの側の値はタグ付きの像です。数項のタグ 0 か 1 を、抽出された関数の値と対にします。こうして二つの単射は、重ならないタグ付きの値域に着地します。

```agda
  val : (z : S) → Mem z → Case z → S
  val z m (inl h)  = prʟ (nn 0) (X₁.toFun (z , h))
  val z m (inr no) = prʟ (nn 1) (X₂.toFun (z , off z m no))
```

`z ∈ D` に対し、関数 `fn` は `z ∈ D₁` かどうかを判定します。左の場合は `(0,E₁(z))` を返し、補集合にあたる右の場合は `(1,E₂(z))` を返します。

```agda
  fn : (z : S) → Mem z → S
  fn z m = val z m (decide z)
```

周囲での意味 `Wit y z` には二つの分岐があります。左の分岐では `z ∈ D₁` であり、`(z,v) ∈ E₁` を満たす `v` が単に存在して、`y` の底集合が `(0,v)` に等しくなります。

```agda
  Wit : (y z : S) → Type (ℓ-suc ℓ)
  Wit y z =
      (⟨ fst z ∈ fst D₁ ⟩
        × ∥ Σ[ v ∈ S ] (Holds E₁ z v × (fst y ≡ pr (# 0) (fst v))) ∥₁)
    ⊎ ((⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥)
```

右の分岐では `z ∉ D₁` であり、`(z,v) ∈ E₂` を満たす `v` が単に存在して、底集合について `y = (1,v)` となります。異なるタグにより、別々の分岐から得た出力が等しくなることはありません。

```agda
        × ∥ Σ[ v ∈ S ] (Holds E₂ z v × (fst y ≡ pr (# 1) (fst v))) ∥₁)
```

グラフは二つの枠をもつ論理式として書かれます。`D₁` への所属と最初の符号の上の存在量化の連言、あるいはその所属の否定と第二の符号の上の存在量化の連言です。存在量化子の内側では、単射された値とタグの等式が符号化のアトムです。

```agda
  opaque
    fo : Formula S 2
    fo = ((var i1 ∈̇ con D₁) ∧̇ ∃̇ (appC E₁ i2 i0 ∧̇ tagAtL i1 0 i0))
       ∨̇ ((¬̇ (var i1 ∈̇ con D₁)) ∧̇ ∃̇ (appC E₂ i2 i0 ∧̇ tagAtL i1 1 i0))
```

二つの符号化のアトムを読むには、その妥当性の補題を使います。適用のアトムの充足は所属 `Holds E z v` になり、タグのアトムの充足は、`y` とタグ付きの対との等式になります。

```agda
    private
      rd : (E : S) (k : ℕ) (y z v : S)
         → ⟨ (v ∷ y ∷ z ∷ []) ⊨ appC E i2 i0 ⟩ → ⟨ (v ∷ y ∷ z ∷ []) ⊨ tagAtL i1 k i0 ⟩
         → Holds E z v × (fst y ≡ pr (# k) (fst v))
      rd E k y z v ha ht =
```

二つの妥当性の同値に沿って移送すると、充足の証人は `Wit` が要求する成分、すなわちグラフ所属 `Holds E z v` と、`y` をタグ `k` の付いた対と同一視する等しさになります。

```agda
          subst ⟨_⟩ (appC-adequate E i2 i0 (v ∷ y ∷ z ∷ [])) ha
        , subst ⟨_⟩ (tagAtL-adequate i1 k i0 (v ∷ y ∷ z ∷ [])) ht
```

逆に、`Holds E z v` と底集合についての等しさ `y = (k,v)` から、妥当性に沿って逆向きに移送すると適用の原子式の充足が得られます。

```agda
      wr : (E : S) (k : ℕ) (y z v : S)
         → Holds E z v → fst y ≡ pr (# k) (fst v)
         → ⟨ (v ∷ y ∷ z ∷ []) ⊨ appC E i2 i0 ⟩ × ⟨ (v ∷ y ∷ z ∷ []) ⊨ tagAtL i1 k i0 ⟩
      wr E k y z v ha ht =
          subst ⟨_⟩ (sym (appC-adequate E i2 i0 (v ∷ y ∷ z ∷ []))) ha
```

同じ逆向きの移送により、タグ付き対の等しさはタグ原子式の充足になります。二つの証明を合わせると、存在量化子のもとにある連言が再構成されます。

```agda
        , subst ⟨_⟩ (sym (tagAtL-adequate i1 k i0 (v ∷ y ∷ z ∷ []))) ht
```

`fo` の充足証明は二つの選言肢に分けて読みます。左からは `z ∈ D₁` と 0 のタグが付いた切り詰められた `E₁` の証人が得られ、右からは `z ∉ D₁` と 1 のタグが付いた対応する `E₂` の証人が得られます。各切り詰めの内側で `rd` を適用すると、`Wit y z` の切り詰められた要素が得られます。

```agda
    fo-out : (y z : S) → ⟨ (y ∷ z ∷ []) ⊨ fo ⟩ → ∥ Wit y z ∥₁
    fo-out y z = PT.map
      (λ { (inl (h , hv)) → inl (h , PT.map (λ { (v , (ha , ht)) → v , rd E₁ 0 y z v ha ht }) hv)
         ; (inr (h , hv)) → inr ((λ z∈ → lower (h z∈))
             , PT.map (λ { (v , (ha , ht)) → v , rd E₂ 1 y z v ha ht }) hv) })
```

グラフの内向きの読み出しは、ホスト側の証人を場合ごとに充足へ変えます。左の場合は、所属と切り詰められた項目を、適用とタグの符号化の妥当性の等式に沿って運び、右の場合は、所属しないことの反駁を対象言語の否定へ持ち上げてから同じことをします。

```agda
    fo-in : (y z : S) → Wit y z → ⟨ (y ∷ z ∷ []) ⊨ fo ⟩
    fo-in y z (inl (h , hv)) =
      ∣ inl (h , PT.map (λ { (v , (ha , ht)) → v , wr E₁ 0 y z v ha ht }) hv) ∣₁
    fo-in y z (inr (h , hv)) =
      ∣ inr ((λ z∈ → lift (h z∈))
```

右の場合の残りが第二の選言肢を完成させます。`E₂` の項目は、タグを `0` から `1` に替えるだけで左と同じように運ばれます。二つの選言肢は切り詰められた存在へ注入され、導入は終わりです。

```agda
          , PT.map (λ { (v , (ha , ht)) → v , wr E₂ 1 y z v ha ht }) hv) ∣₁
```

符号化されたそれぞれの関係は一価です。第一成分を共有する項目は第二成分も共有します。これが注入の符号の最初の連言項で、適用の符号化の妥当性を通して読み出されます。

```agda
  private
    sv₁ : (x y y' : S) → Holds E₁ x y → Holds E₁ x y' → fst y ≡ fst y'
    sv₁ = svAt-out zero (E₁ ∷ D₁ ∷ []) (fst c₁)
    sv₂ : (x y y' : S) → Holds E₂ x y → Holds E₂ x y' → fst y ≡ fst y'
    sv₂ = svAt-out zero (E₂ ∷ D₂ ∷ []) (fst c₂)
```

符号化された関係はさらに単射でもあります。第二成分を共有する項目は、第一成分の基礎の集合が等しくなります。範囲の条項はここからはじまり、関係のどの値も基数の中にあると述べます。

```agda
    ij₁ : (y x x' : S) → Holds E₁ x y → Holds E₁ x' y → fst x ≡ fst x'
    ij₁ = injAt-out zero (E₁ ∷ D₁ ∷ []) (fst (snd (snd c₁)))
    ij₂ : (y x x' : S) → Holds E₂ x y → Holds E₂ x' y → fst x ≡ fst x'
    ij₂ = injAt-out zero (E₂ ∷ D₂ ∷ []) (fst (snd (snd c₂)))
    ran₁ : (x y : S) → Holds E₁ x y → ⟨ fst y ∈ fst κ ⟩
```

二つ目の値域条件により、二つの単射符号から読み出すデータがそろいます。各関係について一価性、単射性、そしてすべての値が `κ` に属することが得られ、タグ付き写像はこれらの性質から構成されます。

```agda
    ran₁ = snd (snd (snd c₁))
    ran₂ : (x y : S) → Holds E₂ x y → ⟨ fst y ∈ fst κ ⟩
    ran₂ = snd (snd (snd c₂))
```

証人は要素についての二つの場合から構成します。`z ∈ D₁` なら `E₁` から取り出した関数の値を使い、そうでなければ、そこから得られる `z ∈ D₂` に対して `E₂` から取り出した関数の値を使います。どちらの場合も、取り出しによりグラフの項目と、タグ付きの対を選んだ値と同一視する等式の両方が得られます。

```agda
  wit : (z : S) (m : Mem z) (c : Case z) → Wit (val z m c) z
  wit z m (inl h)  = inl (h , ∣ X₁.toFun (z , h)
    , (X₁.toFun-graph (z , h) , prʟ-fst (nn 0) (X₁.toFun (z , h))) ∣₁)
  wit z m (inr no) = inr (no , ∣ X₂.toFun (z , off z m no)
    , (X₂.toFun-graph (z , off z m no) , prʟ-fst (nn 1) (X₂.toFun (z , off z m no))) ∣₁)
```

左の場合の一意性は、三つの等式を合成します。項目の第二成分が、切り詰められた証人が名指す値に等しいこと。`E₁` の一価性が二つの関数の値を同一視すること。そして対の第一射影の等式が、値がちょうどタグつきの項目であることを述べます。

```agda
  only : (z : S) (m : Mem z) (c : Case z) (y : S) → Wit y z → fst y ≡ fst (val z m c)
  only z m (inl h) y (inl (_ , hv)) = PT.rec (setIsSet _ _)
    (λ { (v , (hg , hy)) →
       hy ∙ cong (pr (# 0)) (sv₁ z v (X₁.toFun (z , h)) hg (X₁.toFun-graph (z , h)))
          ∙ sym (prʟ-fst (nn 0) (X₁.toFun (z , h))) }) hv
```

交差する場合はそのまま反駁されます。`D₁` の中の要素が、`D₁` の外で記録された証人をもつことはできず、逆もまた然りです。右と右の場合は、`E₂` とタグ `1`、そして外れた要素での関数の値を使って、左とまったく同じように処理されます。

```agda
  only z m (inl h) y (inr (no , _)) = Empty.rec (no h)
  only z m (inr no) y (inl (h , _)) = Empty.rec (no h)
  only z m (inr no) y (inr (_ , hv)) = PT.rec (setIsSet _ _)
    (λ { (v , (hg , hy)) →
       hy ∙ cong (pr (# 1)) (sv₂ z v (X₂.toFun (z , off z m no)) hg (X₂.toFun-graph (z , off z m no)))
```

最後の等式が、タグの同定と対の第一射影の等式を合成し、一意性が完成します。こうして、どちらの場合でも証人はその値を決定します。

```agda
          ∙ sym (prʟ-fst (nn 1) (X₂.toFun (z , off z m no))) }) hv
```

値は内部の直積に落ちます。数項 `0` か `1` と関数の値の対は、その第一射影の等式を通して提示され、二つの数項が `κ` の中にあり、範囲の条項によって関数の値も `κ` の中にあるので、`prodL-in` がそれを受け入れます。

```agda
  into : (z : S) (m : Mem z) (c : Case z) → ⟨ fst (val z m c) ∈ˢ fst (prodL κ) ⟩
  into z m (inl h) = subst (λ w → ⟨ w ∈ˢ fst (prodL κ) ⟩) (sym (prʟ-fst (nn 0) (X₁.toFun (z , h))))
    (prodL-in κ (nn 0) (X₁.toFun (z , h)) 0∈κ (ran₁ z (X₁.toFun (z , h)) (X₁.toFun-graph (z , h))))
  into z m (inr no) = subst (λ w → ⟨ w ∈ˢ fst (prodL κ) ⟩) (sym (prʟ-fst (nn 1) (X₂.toFun (z , off z m no))))
    (prodL-in κ (nn 1) (X₂.toFun (z , off z m no)) 1∈κ
```

右の場合は `E₂` と数項 `1` から範囲の事実を供給し、タグつきの値がどちらも直積の中にあることが揃います。

```agda
      (ran₂ z (X₂.toFun (z , off z m no)) (X₂.toFun-graph (z , off z m no))))
```

これらの材料から、通常の和集合 `D` から内部直積 `prodL κ` への写像を定めます。値は左側を優先する場合分けで選ばれ、`into` がそのタグ付きの値が直積に属することを証明します。

```agda
  Dmap : DefinableMap
  Dmap = record
    { dom = D ; cod = prodL κ ; fn = fn
    ; into = λ z m → into z m (decide z)
    ; graph = fo
```

定義の条項が証人をグラフの導入に渡し、一意性が、どのグラフの項目も、決められた場合の値へ、台の等しさに沿って変換します。これで定義可能な写像は完成です。

```agda
    ; defines = λ z m → fo-in (fn z m) z (wit z m (decide z))
    ; only = λ z m y h → S≡ (PT.rec (setIsSet _ _) (only z m (decide z) y) (fo-out y z h)) }
```

タグつきの写像の単射性は、二つの入力について決められた場合を比較することで証明します。場合分けには四つの組み合わせがあり、タグつきの対の構造がそれをきれいに分けます。

```agda
  inj : (z : S) (m : Mem z) (z' : S) (m' : Mem z') → fst (fn z m) ≡ fst (fn z' m') → fst z ≡ fst z'
  inj z m z' m' = go (decide z) (decide z')
    where
    go : (c : Case z) (c' : Case z') → fst (val z m c) ≡ fst (val z' m' c') → fst z ≡ fst z'
    go (inl h) (inl h') q = ij₁ (X₁.toFun (z , h)) z z' (X₁.toFun-graph (z , h))
```

同じタグの場合は、対の等式を `pr-inj` で逆にたどります。タグが一致するので、値の等式が二つの関数の値を同一視し、これが単射性の条項が消費する議論そのものです。

```agda
      (subst (λ w → ⟨ pr (fst z') w ∈ fst E₁ ⟩) (sym (snd p)) (X₁.toFun-graph (z' , h')))
      where
      p : (# 0 ≡ # 0) × (fst (X₁.toFun (z , h)) ≡ fst (X₁.toFun (z' , h')))
      p = pr-inj (sym (prʟ-fst (nn 0) (X₁.toFun (z , h))) ∙ q ∙ prʟ-fst (nn 0) (X₁.toFun (z' , h')))
    go (inl h) (inr no') q = Empty.rec (znots (#-inj 0 1 (fst
```

タグが異なる二つの場合はいずれも不可能です。二つの値が等しければ数項 `0` と数項 `1` が等しくなってしまい、二つの向きはそれぞれ `znots` と `snotz` に反します。両方の入力が右側の場合は、`E₂` の単射性がそれらを同一視します。

```agda
      (pr-inj (sym (prʟ-fst (nn 0) (X₁.toFun (z , h))) ∙ q ∙ prʟ-fst (nn 1) (X₂.toFun (z' , off z' m' no')))))))
    go (inr no) (inl h') q = Empty.rec (snotz (#-inj 1 0 (fst
      (pr-inj (sym (prʟ-fst (nn 1) (X₂.toFun (z , off z m no))) ∙ q ∙ prʟ-fst (nn 0) (X₁.toFun (z' , h')))))))
    go (inr no) (inr no') q = ij₂ (X₂.toFun (z , off z m no)) z z' (X₂.toFun-graph (z , off z m no))
      (subst (λ w → ⟨ pr (fst z') w ∈ fst E₂ ⟩) (sym (snd p)) (X₂.toFun-graph (z' , off z' m' no')))
```

右と右の場合の対の等式は、タグの一致と関数の値の一致に分かれ、単射性が消費するのは後者です。

```agda
      where
      p : (# 1 ≡ # 1) × (fst (X₂.toFun (z , off z m no)) ≡ fst (X₂.toFun (z' , off z' m' no')))
      p = pr-inj (sym (prʟ-fst (nn 1) (X₂.toFun (z , off z m no))) ∙ q
                  ∙ prʟ-fst (nn 1) (X₂.toFun (z' , off z' m' no')))
```

得られたグラフは、通常の和集合 `D₁ ∪ D₂` から `prodL κ` への符号化された単射です。写像は値のタグで二つの枝を区別し、両方に属する要素は第一の枝で扱います。

```agda
  injL : InjL D (prodL κ)
  injL = Inj.injL Dmap inj
```

二つの前提は、それぞれの単射グラフを命題的切り詰めのもとでしか与えません。二つの切り詰めを命題 `InjL (D₁ ∪ D₂) (prodL κ)` へ消去すると、どの証人グラフの組にもタグ付き構成を適用でき、必要な符号化単射の単なる存在が得られます。

```agda
tag-union : (κ : S) → ⟨ # 0 ∈ fst κ ⟩ → ⟨ # 1 ∈ fst κ ⟩
          → (D₁ D₂ : S) → InjL D₁ κ → InjL D₂ κ
          → InjL (unionʟ (pairʟ D₁ D₂)) (prodL κ)
tag-union κ h0 h1 D₁ D₂ = PT.rec2 squash₁
  (λ { (E₁ , c₁) (E₂ , c₂) → TagUnion.injL κ h0 h1 D₁ D₂ E₁ E₂ c₁ c₂ })
```

最小の前者の構成は、一般的な形で述べられます。順序数 `γ`、関係 `G`、定義域 `D`、そして段階 `γ` で抑えられた前者の集合 `P` を受け取り、`D` のすべての要素が `P` の中に `G` の前者を「単に」もつとします。課題は、その一つを正準に選ぶことです。

```agda
module LeastPre (γ : V ℓ) (oγ : IsOrd γ) (G D P : S)
  (inP : (p z : S) → Holds G p z → ⟨ fst p ∈ fst P ⟩)
  (P⊆L : (p : S) → ⟨ fst p ∈ fst P ⟩ → ⟨ fst p ∈ Lset γ ⟩)
  (have : (z : S) → ⟨ fst z ∈ fst D ⟩ → ∥ Σ[ p ∈ S ] Holds G p z ∥₁) where
```

定義域への所属は型として記録され、議論が要素とともにそれを運べるようにします。

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem z = ⟨ fst z ∈ fst D ⟩
```

グラフの論理式は、定数 `G` の適用の条項です。対の上で成立することは、ちょうどその対が関係に属することを意味します。

```agda
  private
    graphFo : Formula S 2
    graphFo = appC G i0 i1
```

存在仮定を共通の段階へ移しますが、前者を大域的に選ぶことはしません。切り詰めのもとで存在する各前者は `P` に属し、したがって `Lset γ` に属します。さらに妥当性の等式が、その関係への所属をグラフ論理式の充足へ変えます。

```agda
    have-γ : (z : S) → Mem z
           → ∥ Σ[ p ∈ S ] (⟨ fst p ∈ Lset γ ⟩ × ⟨ (p ∷ z ∷ []) ⊨ graphFo ⟩) ∥₁
    have-γ z m = PT.map
      (λ { (p , h) → p , P⊆L p (inP p z h)
                       , subst ⟨_⟩ (sym (appC-adequate G i0 i1 (p ∷ z ∷ []))) h })
```

もとの切り詰められた存在が、輸送が消費する証人を供給します。

```agda
      (have z m)
```

段階順序による構成は、定義域の各要素に対して `Lset γ` にある最小の `G` 前者を選びます。また、定義可能なグラフと、各入力をその選ばれた値に対応させる所属の読み出しも与えます。

```agda
    module Ls = Least γ oγ D graphFo have-γ using ( fn; fn-holds; Dmap; T; T-in; T-out )
```

選ばれた最小の前者が、この構成の値を与える関数です。

```agda
  fn : (z : S) → Mem z → S
  fn = Ls.fn
```

値はその入力で関係を満たします。内部の充足は、値と入力を対にした環境での適用の条項へと運び戻されます。

```agda
  fn-holds : (z : S) (m : Mem z) → Holds G (fn z m) z
  fn-holds z m = subst ⟨_⟩ (appC-adequate G i0 i1 (fn z m ∷ z ∷ [])) (Ls.fn-holds z m)
```

定義可能な写像は、余域を `P` として記録されます。値の所属は、既存の仮定の内向きの方向が保証します。

```agda
  Dmap : DefinableMap
  Dmap = record Ls.Dmap { cod = P ; into = λ z m → inP (fn z m) z (fn-holds z m) }
```

最小の前者の関数のグラフは `L` の要素であり、段階の機構がその所属の記述とともに返します。

```agda
  T : S
  T = Ls.T
```

内向きの読み出しは、入力と選ばれた値の対がグラフの項目であることを示します。

```agda
  T-in : (z : S) (m : Mem z) → ⟨ pr (fst z) (fst (fn z m)) ∈ fst T ⟩
  T-in = Ls.T-in
```

外向きの読み出しは、すべての項目から、入力と、第二成分を選ばれた値と同一視する等式を復元します。のちの議論が候補を比較するときに使うのはこれです。

```agda
  T-out : (z e : S) → ⟨ pr (fst z) (fst e) ∈ fst T ⟩
        → Σ[ m ∈ Mem z ] (fst e ≡ fst (fn z m))
  T-out = Ls.T-out
```

関係が関数的であるという追加の仮定のもとで、最小の前者の関数は単射になります。モジュールが携えるのは、この一つの仮定だけです。

```agda
  module Functional
    (funct : (p z z' : S) → Holds G p z → Holds G p z' → fst z ≡ fst z') where
```

二つの入力が同じ値を共有すれば、その値は両方の入力で関係を満たします。二つ目の充足が値の等式に沿って輸送され、関数性が二つの入力を同一視します。

```agda
    inj : (z : S) (m : Mem z) (z' : S) (m' : Mem z')
        → fst (fn z m) ≡ fst (fn z' m') → fst z ≡ fst z'
    inj z m z' m' q = funct (fn z m) z z' (fn-holds z m)
      (subst (λ w → ⟨ pr w (fst z') ∈ fst G ⟩) (sym q) (fn-holds z' m'))
```

この単射性は、定義域から前者の集合への、符号化された単射としてまとめられます。

```agda
    injL : InjL D P
    injL = Inj.injL Dmap inj
```

点の構成は、高々一要素の定義域を扱います。`0 ∈ κ` だけを仮定し、`a` から作った単集合の各要素を零番の数項へ送り、`κ` への符号化された単射を得ます。

```agda
module Point (κ : S) (0∈κ : ⟨ # 0 ∈ fst κ ⟩) (a : S) where
```

`Y` を `a` から作られる構成可能な単集合とします。議論で使うのは、その所属の導入則と除去則だけです。

```agda
  Y : S
  Y = sglʟ a
```

要素 `a` はそれ自身の単集合に属します。一元集合の構成の導入の読み出しによるものです。

```agda
  Y-in : ⟨ fst a ∈ fst Y ⟩
  Y-in = sglʟ-in a (fst a) refl
```

消去の読み出しは、単集合がそれ以外を含まないと言います。どの要素も、基礎の集合は `a` です。

```agda
  Y-out : (z : S) → ⟨ fst z ∈ fst Y ⟩ → fst z ≡ fst a
  Y-out z = sglʟ-out a (fst z)
```

グラフは、二つの自由スロットをもつ原子論理式で記述されます。この論理式は値のスロットを内部の空集合と等置し、その底の集合は数項 `0` です。

```agda
  fo : Formula S 2
  fo = var i0 ≐ con ∅ʟ
```

定義可能な写像は、ただ一つの入力を零番の数項へ送ります。余域への所属は、既存の事実 `0∈κ` です。

```agda
  Dmap : DefinableMap
  Dmap = record
    { dom = Y ; cod = κ ; fn = λ _ _ → nn 0
    ; into = λ _ _ → 0∈κ
    ; graph = fo
```

グラフは定義どおりに成立します。原子文が数項をそれ自身と等置するからです。一意性は、単集合の二つの要素が同じ基礎の集合を提示することから成立します。

```agda
    ; defines = λ z m → refl
    ; only = λ z m y h → S≡ h }
```

単射性は、二つの外向きの読み出しを合成します。どちらの入力も `a` と同じ基礎の集合を提示するので、台の要素として両者は等しいのです。

```agda
  inj : (z : S) (m : ⟨ fst z ∈ fst Y ⟩) (z' : S) (m' : ⟨ fst z' ∈ fst Y ⟩)
      → fst (nn 0) ≡ fst (nn 0) → fst z ≡ fst z'
  inj z m z' m' _ = Y-out z m ∙ sym (Y-out z' m')
```

単集合から基数への単射は、ほかの計数の部品と同じ形でまとめられます。

```agda
  injL : InjL Y κ
  injL = Inj.injL Dmap inj
```

## 有限な閉包の各段階を数える

計数定理では、後者に閉じた順序数 `lam`、`Lset lam` に含まれる始点集合 `X`、そして `X` が構成可能であることを固定します。初等性と超妥当性の仮定は、`X` から生成される Skolem 包に必要な閉包と最小証人の性質を与えます。

```agda
module Count (lam : V ℓ) (ordλ : IsOrd lam)
  (succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : V ℓ) (X⊆L : (x : V ℓ) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
  (elem : Frame.A.Elementary lam ordλ succλ X X⊆L ∅∈λ)
```

計数の目標は、`ω` の外にある内部の基数 `κ` と、始点からそれへの符号化された単射です。課題は、同じ基数で包全体を数えることです。

```agda
  (sup : Superadequate lam)
  (X-isL : ⟨ isL X ⟩)
  (κ : S) (oκ : IsOrd (fst κ)) (cκ : IsCardinalL κ) (κ∉ω : ⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
  (base : InjL (X , X-isL) κ) where
```

この包は有限反復 `hullStep n` の和集合として表されます。一回の閉包は `Φ` によって定まり、その非自明な枝は、論理式の鍵と現在の反復上の有限なパラメータ環境による最小証人を記録します。

```agda
  module Cn = Condense′ lam ordλ succλ X X⊆L ∅∈λ elem sup X-isL
    using ( hullStep; hullL; hullStep⊆Hull )
  module B = Telescope.Build lam ordλ succλ X X⊆L ∅∈λ
    using ( A; Body
          ; LeastWitness; leastWitnessFo; leastWitness-in; leastWitness-out
```

最小証人に付随するデータから、自然数の長さ、現在の集合への有限な割り当て、その符号化された環境、そして論理式の鍵が `Lset ω` に属することが得られます。一意性は、鍵と環境を固定した後に成立します。

```agda
          ; LeastWitnessData; leastWitness-data; leastWitness-unique; witFo-leastWitness
          ; Φ; Φ-out; λ-isL; ω-num; pack )
  module SM = SatGraph B.A using ( pairs; pairs-out; valOf )
```

有限反復には所属の導入則と除去則があり、各反復は包全体に含まれます。さらに包全体は `Lset lam` に含まれます。これらの包含により、計数構成で使う各集合は固定した周囲の段階内に保たれます。

```agda
  module It = Telescope.HullIter.It lam ordλ succλ X X⊆L ∅∈λ X-isL B.pack
    using ( Num; iter; iter-in; iter-out; iterUnion-out; ω-num )
  module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ using ( Hull⊆L )
  open Cn using ( hullStep; hullL )
```

`κ` は順序数であり `ω` に属さないので、すべての有限数項を含みます。この結論に内部基数性は使われず、内部基数性は別に平方法則で必要になります。

```agda
  num∈κ : (k : ℕ) → ⟨ # k ∈ fst κ ⟩
  num∈κ k = ω⊆ (fst κ) oκ κ∉ω (# k) (#∈ω k)
```

無限基数の平方に関する議論から、符号化された単射 `pairκ : InjL (prodL κ) κ` が得られます。ここでは `κ` の順序数性、内部基数性、`ω` に属さないことの三つをすべて使います。結論は単射であり、全単射ではありません。

```agda
  pairκ : InjL (prodL κ) κ
  pairκ = WF.WFI.induction regularityV {P = Goal} Step.result (fst κ) (snd κ) oκ cκ κ∉ω
```

段階 `Lω = Lset ω` は、単射の合成によって `κ` へ入ります。極限段階の計数がまず `Lω ↪ ωʟ` を与え、`κ` の順序数性と非有限性から得られる `ω ⊆ κ` が `ωʟ ↪ κ` を与えます。

```agda
  Lω↪κ : InjL Lω κ
  Lω↪κ = injl-trans Lω ωʟ κ limit-stage-counted
    (inclusion-coded ωʟ κ (λ z hz → ω⊆ (fst κ) oκ κ∉ω z hz))
```

一回の閉包を数えるため、`Lset lam` に含まれる構成可能な集合 `Z` と、`InjCode E Z κ` を満たす実際のグラフ `E` を固定します。目標は、この選ばれた段階の単射から、符号化単射の単なる存在 `InjL (Φ Z) κ` を構成することです。

```agda
  module OneStep (Z : S) (Z⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
                 (E : S) (cE : InjCode E Z κ) where
```

`ΦZ = Φ Z` は一回の閉包です。その所属の記述には三つの枝があります。`Z` の既存の要素、空集合という予備の場合、または論理式の鍵と `Z` 上の有限なパラメータ環境によって定まる最小証人です。

```agda
    ΦZ : S
    ΦZ = B.Φ Z
```

新しい部分をまず分出します。`D₂` は `ΦZ` のうち `Z` に属さない要素を集めます。`L` の内部の分出により、新しい部分も構成可能です。

```agda
    opaque
      D₂ : S
      D₂ = hasSeparationL ΦZ (¬̇ (var i0 ∈̇ con Z)) .fst .fst
```

その所属の仕様は、分出が計算した内容を正確に述べます。`D₂` への所属とは、`ΦZ` への所属と `Z` への所属の否定を合わせたものです。

```agda
      D₂-spec : (z : S) → (fst z ∈ fst D₂)
              ≡ ((fst z ∈ fst ΦZ) ⊓ ((z ∷ []) ⊨ ¬̇ (var i0 ∈̇ con Z)))
      D₂-spec z = hasSeparationL ΦZ (¬̇ (var i0 ∈̇ con Z)) .fst .snd z
```

導入規則は所属の反証を対象レベルへ持ち上げます。したがって `ΦZ` の要素と、それが `Z` に属さないことの証明が揃えば `D₂` に入れます。

```agda
    opaque
      D₂-in : (z : S) → ⟨ fst z ∈ fst ΦZ ⟩ → (⟨ fst z ∈ fst Z ⟩ → Empty.⊥) → ⟨ fst z ∈ fst D₂ ⟩
      D₂-in z h no = subst ⟨_⟩ (sym (D₂-spec z)) (h , λ z∈ → lift (no z∈))
```

消去の規則は、仕様を通して `D₂` の所属を展開し、対象レベルの反証を通常の含意へと降ろします。

```agda
      D₂-out : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → ⟨ fst z ∈ fst ΦZ ⟩ × (⟨ fst z ∈ fst Z ⟩ → Empty.⊥)
      D₂-out z h = r .fst , λ z∈ → lower (r .snd z∈)
        where
        r : ⟨ fst z ∈ fst ΦZ ⟩
          × ⟨ (z ∷ []) ⊨ ¬̇ (var i0 ∈̇ con Z) ⟩
```

展開された主張は一つの対です。`ΦZ` への所属と、否定された原子の充足です。

```agda
        r = subst ⟨_⟩ (D₂-spec z) h
```

新しい部分の内側から、空集合と等しい要素が `D∅` として分出されます。

```agda
    opaque
      D∅ : S
      D∅ = hasSeparationL D₂ (var i0 ≐ con ∅ʟ) .fst .fst
```

その仕様は同じ二重の型です。`D₂` への所属と、空集合との等式です。

```agda
      D∅-spec : (z : S) → (fst z ∈ fst D∅)
              ≡ ((fst z ∈ fst D₂) ⊓ ((z ∷ []) ⊨ var i0 ≐ con ∅ʟ))
      D∅-spec z = hasSeparationL D₂ (var i0 ≐ con ∅ʟ) .fst .snd z
```

`D₂` の要素で空集合と等しいものは、二つのデータとともに `D∅` に入ります。

```agda
    opaque
      D∅-in : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → fst z ≡ ∅ → ⟨ fst z ∈ fst D∅ ⟩
      D∅-in z h e = subst ⟨_⟩ (sym (D∅-spec z)) (h , e)
```

その消去は、仕様をそのまま読んだものです。`D₂` への所属と、空集合との等式です。

```agda
      D∅-out : (z : S) → ⟨ fst z ∈ fst D∅ ⟩ → ⟨ fst z ∈ fst D₂ ⟩ × (fst z ≡ ∅)
      D∅-out z h = subst ⟨_⟩ (D∅-spec z) h
```

残りの部分 `Dw` は、`D₂` のうち空集合と異なる要素を集めます。

```agda
    opaque
      Dw : S
      Dw = hasSeparationL D₂ (¬̇ (var i0 ≐ con ∅ʟ)) .fst .fst
```

その仕様は前のものと鏡像で、等式の代わりに否定された等式が置かれます。

```agda
      Dw-spec : (z : S) → (fst z ∈ fst Dw)
              ≡ ((fst z ∈ fst D₂) ⊓ ((z ∷ []) ⊨ ¬̇ (var i0 ≐ con ∅ʟ)))
      Dw-spec z = hasSeparationL D₂ (¬̇ (var i0 ≐ con ∅ʟ)) .fst .snd z
```

導入には、`D₂` への所属と、空集合との相等の反証が要ります。

```agda
    opaque
      Dw-in : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → (fst z ≡ ∅ → Empty.⊥) → ⟨ fst z ∈ fst Dw ⟩
      Dw-in z h ne = subst ⟨_⟩ (sym (Dw-spec z)) (h , λ q → lift (ne q))
```

消去は `D₂` への所属と、対象レベルから降ろされた反証を返します。

```agda
      Dw-out : (z : S) → ⟨ fst z ∈ fst Dw ⟩ → ⟨ fst z ∈ fst D₂ ⟩ × (fst z ≡ ∅ → Empty.⊥)
      Dw-out z h = r .fst , λ q → lower (r .snd q)
        where
        r : ⟨ fst z ∈ fst D₂ ⟩
          × ⟨ (z ∷ []) ⊨ ¬̇ (var i0 ≐ con ∅ʟ) ⟩
```

二つの和集合が後で必要となる上界を与えます。`U₁` は `Z` と真に新しい部分 `D₂` を含み、`U₃` は空集合の部分 `D∅` と空でない証人の部分 `Dw` を含みます。続く補題は、これらの和集合への必要な包含を証明します。

```agda
        r = subst ⟨_⟩ (Dw-spec z) h
    module U₁ = Union2 Z D₂ using ( D; in₁; in₂ )
    module U₃ = Union2 D∅ Dw using ( D; in₁; in₂ )
```

閉包の段階は第一の和集合で覆われます。`ΦZ` の各要素 `z` は `Z` に属するか属さないかが排中律で決まり、いずれの場合も `ΦZ` が構成可能なので `z` も構成可能です。

```agda
    ΦZ⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst ΦZ ⟩ → ⟨ z ∈ˢ fst U₁.D ⟩
    ΦZ⊆ z h = go (lem (z ∈ fst Z))
      where
      zS : S
      zS = z , isL-trans {x = fst ΦZ} {y = z} h (snd ΦZ)
```

二つの場合は、和集合への二つの包含によって `U₁` に入ります。すでに `Z` に属する要素には第一の包含を使い、そうでなければ `D₂-in` で新しい部分への所属を示してから第二の包含を使います。

```agda
      go : ⟨ z ∈ fst Z ⟩ ⊎ (⟨ z ∈ fst Z ⟩ → Empty.⊥) → ⟨ z ∈ fst U₁.D ⟩
      go (inl hz) = U₁.in₁ zS hz
      go (inr no) = U₁.in₂ zS (D₂-in zS h no)
```

新しい部分は第二の和集合で覆われます。これも空集合との等式についての排中律によるものです。

```agda
    D₂⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst D₂ ⟩ → ⟨ z ∈ˢ fst U₃.D ⟩
    D₂⊆ z h = go (lem ((z ≡ ∅) , setIsSet z ∅))
      where
      zS : S
      zS = z , isL-trans {x = fst D₂} {y = z} h (snd D₂)
```

空集合と等しい要素は `D∅` から入り、異なる要素は `Dw` から入ります。

```agda
      go : (z ≡ ∅) ⊎ (z ≡ ∅ → Empty.⊥) → ⟨ z ∈ fst U₃.D ⟩
      go (inl e)  = U₃.in₁ zS (D∅-in zS h e)
      go (inr ne) = U₃.in₂ zS (Dw-in zS h ne)
```

`D∅` の各要素は `∅` に等しいですが、`D∅` 自体は空であるかもしれません。数項 `0` が `κ` に属するので、包含の符号化から `L` の内部で `D∅ ↪ κ` が得られます。

```agda
    D∅↪κ : InjL D∅ κ
    D∅↪κ = inclusion-coded D∅ κ
      (λ z hz → subst (λ w → ⟨ w ∈ fst κ ⟩)
        (sym (D∅-out (z , isL-trans {x = fst D∅} {y = z} hz (snd D∅)) hz .snd)) (num∈κ 0))
```

第二の和集合が証人の符号化の準備をします。`U₂` は、段階 `ω` で生まれる要素と、`Z` の要素の有限列をつなぎます。

```agda
    module U₂ = Union2 Lω (seqL Z) using ( D; in₁; in₂ )
```

`PB` を `U₂ = Lω ∪ seqL Z` の平方とします。`s ∈ Lω` かつ `e ∈ seqL Z` である実際の証人符号 `(s,e)` はすべて `PB` に属します。ただし `PB` は一様な上界であり、有効な証人符号でない対も含みます。

```agda
    PB : S
    PB = prodL U₂.D
```

最小証人の論理式を固定した基 `Z` に釘付けします。得られる五変数の論理式 `pin₅` は、枠 `(e,s,z,p,q)` において、`z` が環境 `e` と鍵 `s` によって定まる最小証人であるとき、かつそのときに限り満たされます。最後の二つのスロットは周囲の枠が運びます。

```agda
    opaque
      pin₅ : Formula S 5
      pin₅ = pinAt Z B.leastWitnessFo
```

内向きには、パラメータの環境 `e` と鍵 `s` による `z` の最小証人が、五スロットの文脈での釘付けされた論理式の充足を与えます。

```agda
      pin₅-in : (e s z p q : S) → B.LeastWitness Z e s z
              → ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩
      pin₅-in e s z p q h =
        pin-in Z B.leastWitnessFo (e ∷ s ∷ z ∷ p ∷ q ∷ [])
          (B.leastWitness-in Z e s z p q h)
```

外向きには、釘付けされた論理式の充足が最小証人へと展開されます。釘付けをほどくのは釘付けの補題です。

```agda
      pin₅-out : (e s z p q : S) → ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩
               → B.LeastWitness Z e s z
      pin₅-out e s z p q h =
        B.leastWitness-out Z e s z p q
          (pin-out Z B.leastWitnessFo (e ∷ s ∷ z ∷ p ∷ q ∷ []) h)
```

数える関係は命題的に切り詰められています。`GW p z` は、鍵 `s` と環境 `e` が存在し、`p = (s,e)` であり、`z` がそれらによって定まる最小証人であることを単に述べます。

```agda
    GW : (p z : S) → Type (ℓ-suc ℓ)
    GW p z = ∥ Σ[ s ∈ S ] Σ[ e ∈ S ]
               ((fst p ≡ pr (fst s) (fst e)) × B.LeastWitness Z e s z) ∥₁
```

同じ関係は論理式としても書かれます。二つの存在量化子が鍵と環境を束縛し、対の原子が `p` を確定し、釘付けされた論理式が証人の条件を運びます。

```agda
    opaque
      se₃ : Formula S 3
      se₃ = ∃̇ (∃̇ (prAtL i3 i1 i0 ∧̇ pin₅))
```

内向きには、対の等式と最小証人が与えられれば、二つの証人を入れ、対の原子をその妥当性に沿って対象言語へ輸送します。

```agda
      se₃-in : (z p q s e : S) → fst p ≡ pr (fst s) (fst e)
             → B.LeastWitness Z e s z → ⟨ (z ∷ p ∷ q ∷ []) ⊨ se₃ ⟩
      se₃-in z p q s e qp h =
        ∣ s , ∣ e , ( subst ⟨_⟩ (sym (prAtL-adequate i3 i1 i0 (e ∷ s ∷ z ∷ p ∷ q ∷ []))) qp
                    , pin₅-in e s z p q h ) ∣₁ ∣₁
```

外向きには、二つの存在量化子を一度に一つずつ消費します。最初の段階で外側の量化子をはぎ、項目 `s` と切り詰められた残りを取っておきます。

```agda
      se₃-out : (z p q : S) → ⟨ (z ∷ p ∷ q ∷ []) ⊨ se₃ ⟩ → GW p z
      se₃-out z p q = PT.rec squash₁ at₁
        where
        at₂ : (s : S) → Σ[ e ∈ S ] ( ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ prAtL i3 i1 i0 ⟩
                                   × ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩ ) → GW p z
```

二つ目の存在量化子を開くと、対を表す原子式の妥当性から `p = (s,e)` が得られ、釘付けされた論理式の外向きの読みから最小証人の条件が得られます。これらの証人を、`GW` を定義する命題的切り詰めの中へ戻します。

```agda
        at₂ s (e , (qp , h)) = ∣ s , e
          , ( subst ⟨_⟩ (prAtL-adequate i3 i1 i0 (e ∷ s ∷ z ∷ p ∷ q ∷ [])) qp
            , pin₅-out e s z p q h ) ∣₁
        at₁ : Σ[ s ∈ S ] ∥ Σ[ e ∈ S ] ( ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ prAtL i3 i1 i0 ⟩
                                      × ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩ ) ∥₁ → GW p z
```

`GW p z` は命題なので、残る外側の切り詰めをそこへ消去できます。`se₃-in` と `se₃-out` を合わせると、ホスト側の関係 `GW` と、それを表す対象言語の論理式の充足との間の二つの含意が得られます。

```agda
        at₁ (s , h) = PT.rec squash₁ (at₂ s) h
```

有界分出により、`L` の内部に関係 `G` を構成します。その項目は、`p ∈ PB`、`z ∈ Dw`、`GW p z` を満たす順序対 `(p,z)` です。したがって `G` は、最小証人の関係を選んだ符号の池と空でない新しい部分の間に制限します。

```agda
    private
      module WitnessGraph = Relation PB Dw ((var i1 ∈̇ con PB) ∧̇ se₃)
        (λ p z → (fst p ∈ fst PB) ⊓ (GW p z , squash₁))
        (λ p z q h → h .fst , se₃-out z p q (h .snd))
        (λ p z q h → h .fst , PT.rec (snd ((z ∷ p ∷ q ∷ []) ⊨ se₃))
```

記述の条件の外向きの読みは、論理式そのものの外向きの読みであり、返ってくるのはまさに `GW` のデータです。

```agda
          (λ { (s , e , qp , hw) → se₃-in z p q s e qp hw }) (h .snd))
```

`G` は、順序対 `(p,z)` の集合として表された構成可能な関係です。`PB` の候補符号が `Dw` の要素について最小証人のデータを運ぶとき、`G` はその符号と要素を関係づけます。

```agda
    G : S
    G = WitnessGraph.rel
```

内向きには、`PB` の符号 `p` が、ある鍵と環境を通して `z` とともに最小証人を名指すなら、`G` に属します。

```agda
    G-in : (p z : S) → ⟨ fst p ∈ fst PB ⟩ → ⟨ fst z ∈ fst Dw ⟩
         → (s e : S) → fst p ≡ pr (fst s) (fst e)
         → B.LeastWitness Z e s z → Holds G p z
    G-in p z hp hz s e qp h =
      WitnessGraph.into p z hp hz (hp , ∣ s , e , qp , h ∣₁)
```

逆に、`Holds G p z` から `p ∈ PB` と、命題的に切り詰められた証人データ `GW p z` の両方が得られます。切り詰めの外で鍵と環境を選ぶわけではありません。

```agda
    G-out : (p z : S) → Holds G p z → ⟨ fst p ∈ fst PB ⟩ × GW p z
    G-out = WitnessGraph.pair-out
```

この関係が `Dw` 上で全域的なのは切り詰められた意味においてです。各 `z ∈ Dw` には `Holds G p z` を満たす `p` が単に存在します。`z ∈ ΦZ` を外向きに読むと、`z` が閉包に入った三つの可能な理由が現れます。

```agda
    have : (z : S) → ⟨ fst z ∈ fst Dw ⟩ → ∥ Σ[ p ∈ S ] Holds G p z ∥₁
    have z hz = PT.rec squash₁ body (B.Φ-out Z z (D₂-out z (Dw-out z hz .fst) .fst))
      where
      body : B.Body Z z → ∥ Σ[ p ∈ S ] Holds G p z ∥₁
      body (inl h) = Empty.rec (D₂-out z (Dw-out z hz .fst) .snd h)
```

そのうちの二つはすでに分出によって排除されています。`z` は `Z` の古い要素でも空集合でもあり得ません。残るのは証人の場合であり、証人の論理式の外向きの補題を通して読まれます。

```agda
      body (inr (inl e)) = Empty.rec (Dw-out z hz .snd e)
      body (inr (inr hw)) = PT.rec squash₁ read (B.witFo-leastWitness z Z hw)
        where
        read : Σ[ e ∈ S ] Σ[ s ∈ S ] B.LeastWitness Z e s z
             → ∥ Σ[ p ∈ S ] Holds G p z ∥₁
```

証人の枝は、環境 `e`、鍵 `s`、最小証人を与えます。そのデータ補題から、自然数の長さ `n`、メタレベルの割り当て `g : Fin n → ⟪Z⟫`、`e` を `g` の符号化された環境と同一視する等式、そして `s ∈ Lset ω` が得られます。

```agda
        read (e , s , hw') = PT.map at (B.leastWitness-data Z e s z hw')
          where
          at : B.LeastWitnessData Z e s → Σ[ p ∈ S ] Holds G p z
          at (n , g , qe , hs) = prʟ s e
            , G-in (prʟ s e) z
```

符号 `p` は鍵と環境の内部の対です。その `PB` への所属は項目ごとに築かれます。鍵は `Lset ω` に属するため `Lω` から入り、環境は `Z` への長さ `n` の割り当ての環境であるため `Z` の有限列から入ります。そして関係がこの対を受け入れます。

```agda
                (subst (λ w → ⟨ w ∈ fst PB ⟩) (sym (prʟ-fst s e))
                  (prodL-in U₂.D s e (U₂.in₁ s hs)
                    (U₂.in₂ e (seqL-in Z n e
                      (subst (λ w → ⟨ w ∈ˢ fst (envSet Z n) ⟩) (sym qe) (envSet-in Z g))))))
                hz s e (prʟ-fst s e) hw'
```

## 証人キーに対する一意性

必要な関数性は、計数に必要な逆向きの形をしています。一つの固定した符号 `p` が `z` と `z'` の両方に関係するなら、`z` と `z'` の底の集合は等しくなります。同じ要素に異なる符号があることは依然として許されます。

```agda
    funct : (p z z' : S) → Holds G p z → Holds G p z' → fst z ≡ fst z'
    funct p z z' h h' = PT.rec2 (setIsSet (fst z) (fst z')) read (G-out p z h .snd) (G-out p z' h' .snd)
      where
      read : Σ[ s ∈ S ] Σ[ e ∈ S ]
               ((fst p ≡ pr (fst s) (fst e)) × B.LeastWitness Z e s z)
```

二つの関係は外向きに読まれ、それぞれ鍵、環境、対の等式、そして最小証人を返します。

```agda
           → Σ[ s₂ ∈ S ] Σ[ e₂ ∈ S ]
               ((fst p ≡ pr (fst s₂) (fst e₂)) × B.LeastWitness Z e₂ s₂ z')
           → fst z ≡ fst z'
      read (s , e , q , hw) (s₂ , e₂ , q₂ , hw₂) =
        B.leastWitness-unique Z e s z z' hw hw₂'
```

二つの読み出しは、同じ固定した `p` をそれぞれ `(s,e)` と `(s₂,e₂)` として表します。順序対の符号化の単射性が、二つの鍵と二つの環境を底の集合の水準で同一視し、証明無関連性がそれらを対応する `S` の要素の等式へ持ち上げます。

```agda
        where
        ee : (fst s₂ ≡ fst s) × (fst e₂ ≡ fst e)
        ee = pr-inj (sym q₂ ∙ q)
        hw₂' : B.LeastWitness Z e s z'
        hw₂' = subst2 (λ e' s' → B.LeastWitness Z e' s' z')
```

それらの同一視に沿って二つ目の最小証人の証明を輸送すると、二つの証明は同じ鍵と環境に関するものになります。そこで最小証人の一意性から `fst z ≡ fst z'` が得られます。

```agda
          (S≡ {x = e₂} {y = e} (snd ee)) (S≡ {x = s₂} {y = s} (fst ee)) hw₂
```

符号の池には誕生の段階があります。`γG` は `PB` が階層に現れる段階です。

```agda
    γG : V ℓ
    γG = stage (fst PB) (snd PB)
```

その段階は順序数で添字づけられており、計数の補題が要求するのはこれです。

```agda
    oγG : IsOrd γG
    oγG = stage-ord (fst PB) (snd PB)
```

池はその誕生の段階に含まれます。段階の推移性によるものです。`γG` で生まれた集合の要素は `Lset γG` に属します。

```agda
    PB⊆Lγ : (p : S) → ⟨ fst p ∈ fst PB ⟩ → ⟨ fst p ∈ Lset γG ⟩
    PB⊆Lγ p hp = layer-trans (Lset-layer γG) {x = fst PB} {y = fst p} hp (stage-mem (fst PB) (snd PB))
```

これらの仮定によって `LeastPre` を具体化します。各 `z ∈ Dw` には `PB` にある関係づけられた符号が単に存在し、固定した一つの符号はそのような `z` を高々一つ定めます。最小選択が各要素について一つの符号を選び、`InjL Dw PB` を与えます。証人符号が初めから一意だったとは主張せず、ここで数えたのは空でない新しい部分だけで、閉包一段階全体の結論ではありません。

```agda
    module LP = LeastPre γG oγG G Dw PB (λ p z h → G-out p z h .fst) PB⊆Lγ have
      using ( module Functional )
```

最小原像の構成は、真に新しい証人を `PB` へ単射します。各 `z ∈ Dw` には関連する符号が単に存在し、段階順序がその最小のものを選びます。選択前の符号は一意である必要はありません。単射性は、一つの固定した符号が高々一つの証人しか表さないことから従います。

```agda
    Dw↪PB : InjL Dw PB
    Dw↪PB = LP.Functional.injL funct
```

単射 `Z ↪ κ` を有限列の各成分に作用させると、`seqL Z ↪ seqL κ` が得られます。これを有限列の数え上げと合成して `seqL Z ↪ κ` を得ます。後者に必要なのは `κ` が無限順序数であることだけで、内部の基数である必要はありません。

```agda
    seq↪κ : InjL (seqL Z) κ
    seq↪κ = injl-trans (seqL Z) (seqL κ) κ (seq-map Z κ E cE) (seq-count κ oκ κ∉ω)
```

まず `U₂.D = Lω ∪ seqL Z` を数えます。二つの集合にタグを付けて `κ × κ` へ単射し、`pairκ` でその積を `κ` へ折りたたみます。`PB = U₂.D × U₂.D` なので、`prod-inj` がこの単射を `PB ↪ κ × κ` へ持ち上げ、`pairκ` をもう一度使うと `PB ↪ κ` が得られます。二回の折りたたみは平方則を用いるため、内部の基数性に依存します。

```agda
    PB↪κ : InjL PB κ
    PB↪κ = injl-trans PB (prodL κ) κ
      (prod-inj U₂.D κ
        (injl-trans U₂.D (prodL κ) κ (tag-union κ (num∈κ 0) (num∈κ 1) Lω (seqL Z) Lω↪κ seq↪κ) pairκ))
      pairκ
```

二つの単射を合成すれば、真に新しい証人の数え上げが得られます。そのような証人はそれぞれある `p ∈ PB` で符号化され、`PB` は `κ` へ単射するので、`Dw` も `κ` へ単射します。

```agda
    Dw↪κ : InjL Dw κ
    Dw↪κ = injl-trans Dw PB κ Dw↪PB PB↪κ
```

新しい部分 `D₂` は `D∅ ∪ Dw` に含まれます。`D∅` は空集合に等しい新しい要素だけを含み、それ自身が空の場合もあります。`Dw` は空でない証人の要素を含みます。二つの数え上げにタグを付けて `κ × κ` へ入れ、`pairκ` で折りたたすと `D₂ ↪ κ` が得られます。

```agda
    D₂↪κ : InjL D₂ κ
    D₂↪κ = injl-trans D₂ U₃.D κ (inclusion-coded D₂ U₃.D D₂⊆)
      (injl-trans U₃.D (prodL κ) κ (tag-union κ (num∈κ 0) (num∈κ 1) D∅ Dw D∅↪κ Dw↪κ) pairκ)
```

`ΦZ` の各要素は `Z ∪ D₂` に属します。与えられたグラフ `E` が `Z` を数え、先の構成が `D₂` を数えます。この二つの単射にタグを付けて `κ × κ` へ写し、`pairκ` と合成すると `ΦZ ↪ κ` が得られます。

```agda
    result : InjL ΦZ κ
    result = injl-trans ΦZ U₁.D κ (inclusion-coded ΦZ U₁.D ΦZ⊆)
      (injl-trans U₁.D (prodL κ) κ (tag-union κ (num∈κ 0) (num∈κ 1) Z D₂ ∣ E , cE ∣₁ D₂↪κ) pairκ)
```

`step-count` は `Z ↪ κ` の切り詰められた証人を、命題 `ΦZ ↪ κ` へ除去します。したがって示しているのは `κ` による濃度の上界であり、可算性ではありません。また、出力の単射を証すグラフを選択しません。

```agda
  step-count : (Z : S) → ((z : V ℓ) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
             → InjL Z κ → InjL (B.Φ Z) κ
  step-count Z Z⊆ = PT.rec squash₁ (λ { (E , cE) → OneStep.result Z Z⊆ E cE })
```

有限閉包の各反復の要素は、すべて周囲の段階 `Lset lam` の中にあります。これは、反復が包に含まれ、包の要素がすべて段階の中にあることから従います。

```agda
  iter⊆L : (n : ℕ) (z : V ℓ) → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ Lset lam ⟩
  iter⊆L n z hz = HSH.Hull⊆L z (Cn.hullStep⊆Hull n z hz)
```

自然数についての帰納法により、有限な各反復について個別の内部単射が得られます。基底の場合は始集合の仮定された単射を使い、後続の場合は `step-count` を適用します。これらの証人は命題的に切り詰められたままなので、同時に選んでその和集合を数えることはできません。

```agda
  counted : (n : ℕ) → InjL (hullStep n) κ
  counted zero    = base
  counted (suc n) = step-count (hullStep n) (iter⊆L n) (counted n)
```

`HoldsAt n σ` は、ある構成可能なグラフ `F ∈ Lset σ` が単射 `hullStep n ↪ κ` を符号化するという、命題的に切り詰められた主張です。符号を含む段階と、その符号が数える正確な反復の両方を記録します。

```agda
  HoldsAt : ℕ → V ℓ → hProp (ℓ-suc ℓ)
  HoldsAt n σ = ∥ Σ[ F ∈ S ] (⟨ fst F ∈ Lset σ ⟩ × InjCode F (hullStep n) κ) ∥₁ , squash₁
```

各 `n` に対し、`HoldsAt n` を満たす最小の順序数段階を `ls n` とします。`counted n` が与える切り詰められた単射から存在が従い、得られる最小性の主張は命題なので、最小順序数を選択できます。

```agda
  opaque
    ls : (n : ℕ) → LeastOrd (HoldsAt n)
    ls n = PT.rec (isPropLeastOrd (HoldsAt n)) from (counted n)
      where
      from : Σ[ F ∈ S ] InjCode F (hullStep n) κ → LeastOrd (HoldsAt n)
```

`hullStep n ↪ κ` を符号化するグラフ `F` が与えられると、`F` を含む正準な段階は順序数であり、そこで `HoldsAt n` を証します。したがって候補となる段階の類は要素をもち、`leastOrd` がその最小の要素を返します。

```agda
      from (F , code) = leastOrd (HoldsAt n)
        ∣ stage (fst F) (snd F) , stage-ord (fst F) (snd F)
        , ∣ F , stage-mem (fst F) (snd F) , code ∣₁ ∣₁
```

メタレベルの自然数で添字づけられた最小段階の族 `n ↦ ls n` には、一つの共通する順序数の上界 `γ` があります。有界化定理により、各 `ls n` はこの共通順序数より真に下に置かれます。

```agda
  opaque
    γ : V ℓ
    γ = boundingOrd (Lift {ℓ-zero} {ℓ} ℕ) (λ n → ls (lower n) .fst) (λ n → ls (lower n) .snd .fst) .fst
```

上界 `γ` 自身も順序数です。したがって `Lset γ` は、個別の単射符号を集められる正当な構成可能段階です。

```agda
    oγ : IsOrd γ
    oγ = boundingOrd (Lift {ℓ-zero} {ℓ} ℕ) (λ n → ls (lower n) .fst) (λ n → ls (lower n) .snd .fst) .snd .fst
```

各自然数 `n` について、最小段階 `ls n` は共通の上界 `γ` に属します。この狭義の上界が、構成可能階層の単調性に必要な条件です。

```agda
    bnd-in : (n : ℕ) → ⟨ ls n .fst ∈ γ ⟩
    bnd-in n = boundingOrd (Lift {ℓ-zero} {ℓ} ℕ) (λ n → ls (lower n) .fst) (λ n → ls (lower n) .snd .fst)
                 .snd .snd (lift n)
```

より小さい段階でのコードは、共通の段階でのコードになります。反復の符号化は、段階の単調性によって `Lset γ` の中へ運ばれます。

```agda
  code-at-γ : (n : ℕ) → ⟨ HoldsAt n γ ⟩
  code-at-γ n = PT.map raise (ls n .snd .snd .fst)
    where
    raise : Σ[ F ∈ S ] (⟨ fst F ∈ Lset (ls n .fst) ⟩ × InjCode F (hullStep n) κ)
          → Σ[ F ∈ S ] (⟨ fst F ∈ Lset γ ⟩ × InjCode F (hullStep n) κ)
```

この輸送は、コードをそのより大きな段階での所属と対にします。コード自体はそのままで、動くのは段階の証人だけです。

```agda
    raise (F , h , code) = F , Lset-mono {α = γ} {β = ls n .fst} (bnd-in n) h , code
```

底集合が共通の段階 `Lset γ` である構成可能集合を `Lγ` とします。これは、有限な各反復の単射符号を含む一つの内部の定義域です。

```agda
  opaque
    Lγ : S
    Lγ = LsetS γ oγ
```

その底の集合は、定義により段階 `Lset γ` です。

```agda
    Lγ-fst : fst Lγ ≡ Lset γ
    Lγ-fst = refl
```

反復そのものも、一つの構成可能な集合に集められます。`Iter` は、各内部の数項と、それが索引づける閉包の反復とを対にします。

```agda
    Iter : S
    Iter = It.iter
```

反復集合の導入により、数項とその反復の各対は要素になります。

```agda
    Iter-in : (n : ℕ) → ⟨ pr (# n) (fst (hullStep n)) ∈ fst Iter ⟩
    Iter-in = It.iter-in
```

逆に、すべての要素は、単に、そのような対です。したがって `Iter` の中の所属は、数え上げられた反復だけを指認し、それ以外は何も指認しません。

```agda
    Iter-out : (y : S) → ⟨ fst y ∈ fst Iter ⟩ → ∥ Σ[ n ∈ ℕ ] (fst y ≡ pr (# n) (fst (hullStep n))) ∥₁
    Iter-out = It.iter-out
```

内部の数項 `n` における構成可能なコード `F` の表の証人は、二つの事実からなります。`F` が共通の段階に属すること、そして単に、`n` に記録された反復 `Zn` で、`F` が `Zn` から `κ` への単射を符号化することがあることです。

```agda
  TabWit : (F n : S) → Type (ℓ-suc ℓ)
  TabWit F n = ⟨ fst F ∈ Lset γ ⟩ × ∥ Σ[ Zn ∈ S ] (Holds Iter n Zn × InjCode F Zn κ) ∥₁
```

`tabBody` には、符号 `F`、内部の数項 `n`、使われない関係パラメータのための三つの自由な位置があります。`F ∈ Lset γ` を主張し、`Iter(n,Zn)` が成り立ち、`F` が単射 `Zn ↪ κ` を符号化するような反復 `Zn` を存在量化します。この存在量化子は `S` 上で非有界です。

```agda
  opaque
    tabBody : Formula S 3
    tabBody = (var i1 ∈̇ con Lγ) ∧̇ ∃̇ (appC Iter i1 i0 ∧̇ injFo κ i2 i0)
```

表の本体を読み戻すには、適用のアトムの妥当性と単射の論理式の読みを使い、充足を二成分の表の証人へ変換します。

```agda
    tab-read : (F n q : S) → ⟨ (n ∷ F ∷ q ∷ []) ⊨ tabBody ⟩ → TabWit F n
    tab-read F n q (hF , h) = subst (λ w → ⟨ fst F ∈ w ⟩) Lγ-fst hF
      , PT.map (λ { (Zn , hI , hc) → Zn
          , subst ⟨_⟩ (appC-adequate Iter i1 i0 (Zn ∷ n ∷ F ∷ q ∷ [])) hI
          , InjFo.read κ i2 i0 (Zn ∷ n ∷ F ∷ q ∷ []) hc }) h
```

逆に、`TabWit F n` の証人から `tabBody` の充足が得られます。段階への所属を `Lγ` への所属へ移送し、反復関係と単射符号を、適用論理式と単射論理式の妥当性によって逆向きに変換します。

```agda
    tab-fill : (F n q : S) → TabWit F n → ⟨ (n ∷ F ∷ q ∷ []) ⊨ tabBody ⟩
    tab-fill F n q (hF , h) = subst (λ w → ⟨ fst F ∈ w ⟩) (sym Lγ-fst) hF
      , PT.map (λ { (Zn , hI , hc) → Zn
          , subst ⟨_⟩ (sym (appC-adequate Iter i1 i0 (Zn ∷ n ∷ F ∷ q ∷ []))) hI
          , InjFo.fill κ i2 i0 (Zn ∷ n ∷ F ∷ q ∷ []) hc }) h
```

`tabBody` が定める関係を、`Lγ × ω` の構成可能な部分集合として集めます。その要素は表の証人条件を満たす対 `(F,n)` です。`tabBody` に現れる存在量化子は非有界ですが、ここで使えるのは完全な分出なので、この論理式で分出できます。

```agda
  private
    module TableGraph = Relation Lγ ωʟ tabBody
      (λ F n → TabWit F n , isProp× (snd (fst F ∈ Lset γ)) squash₁) tab-read tab-fill
```

この構成可能な関係を `Gt` と書きます。対 `(F,n)` がこれに属するのは、`F ∈ Lset γ` であり、`n` に記録された反復 `Zn` で、`F` が `Zn` から `κ` への単射を符号化するものが単に存在するとき、かつそのときに限ります。

```agda
  Gt : S
  Gt = TableGraph.rel
```

`F ∈ Lset γ`、`n ∈ ω`、`Iter(n,Zn)` が成り立ち、`F` が `Zn ↪ κ` を符号化するなら、対 `(F,n)` は `Gt` に属します。この関係の特徴づけでは、反復 `Zn` は命題的切り詰めの下でのみ保持されます。

```agda
  Gt-in : (F n Zn : S) → ⟨ fst F ∈ Lset γ ⟩ → ⟨ fst n ∈ fst ωʟ ⟩
        → Holds Iter n Zn → InjCode F Zn κ → Holds Gt F n
  Gt-in F n Zn hF hn hI code = TableGraph.into F n
    (subst (λ w → ⟨ fst F ∈ w ⟩) (sym Lγ-fst) hF) hn (hF , ∣ Zn , hI , code ∣₁)
```

除去は、表の項目を二成分の証人へ読み戻します。

```agda
  Gt-out : (F n : S) → Holds Gt F n → TabWit F n
  Gt-out = TableGraph.pair-out
```

`ω` の中のどの内部の数項にも項目があります。それが記録する反復はある有限の閉包段階であり、そのコードは上の輸送によって共通の段階の中に存在します。

```agda
  have-code : (n : S) → ⟨ fst n ∈ fst ωʟ ⟩ → ∥ Σ[ F ∈ S ] Holds Gt F n ∥₁
  have-code n hn = PT.rec squash₁ at (It.ω-num n hn)
    where
    at : It.Num n → ∥ Σ[ F ∈ S ] Holds Gt F n ∥₁
    at (k , qk) = PT.map
```

そしてコードが表の中に導入されます。反復の同一視は数項の等式に沿って運ばれ、項目は、数項とその固有の反復の対を記録します。

```agda
      (λ { (F , hF , code) → F
         , Gt-in F n (hullStep k) hF hn
             (subst (λ w → ⟨ pr w (fst (hullStep k)) ∈ fst Iter ⟩) (cong fst qk) (Iter-in k)) code })
      (code-at-γ k)
```

`Gt` に最小原像の選択を適用し、定義域を `ω`、符号の上界を `Lγ` とします。各内部数項について段階順序で最小の関連する単射符号を選び、対 `(n,eS(n))` を構成可能な表 `Te` に集めます。一つの共通段階内でのこの定義可能な選択により、切り詰められた族 `counted n` から代表を直接選ぶ必要がなくなります。

```agda
  module Tb = LeastPre γ oγ Gt ωʟ Lγ
    (λ F n h → subst (λ w → ⟨ fst F ∈ w ⟩) (sym Lγ-fst) (Gt-out F n h .fst))
    (λ F hF → subst (λ w → ⟨ fst F ∈ w ⟩) Lγ-fst hF)
    have-code
    using ( T; fn; T-in; T-out; fn-holds )
```

`Te` は選ばれた項目からなる構成可能なグラフです。その定義域は内部の `ω` であり、各数項での値は `Gt` によってその数項と関係づけられる最小の符号です。

```agda
  Te : S
  Te = Tb.T
```

最小項目の関数は、`ω` の中の各内部の数項に対して、そこに記録された反復の単射を符号化する最小の表の項目を割り当てます。

```agda
  eS : (n : S) → ⟨ fst n ∈ fst ωʟ ⟩ → S
  eS = Tb.fn
```

各 `n ∈ ω` について、順序対 `(n,eS(n))` は `Te` に属します。したがって `Te` は、選ばれた符号を数項 `n` での値として記録します。

```agda
  Te-in : (n : S) (m : ⟨ fst n ∈ fst ωʟ ⟩) → ⟨ pr (fst n) (fst (eS n m)) ∈ fst Te ⟩
  Te-in = Tb.T-in
```

逆に、`(n,F) ∈ Te` なら `n ∈ ω` であり、`F` の底集合は選ばれた項目 `eS(n)` の底集合に等しくなります。`n ∈ ω` の所属証明は命題値なので、それによって別の表の値が生じることはありません。

```agda
  Te-out : (n F : S) → ⟨ pr (fst n) (fst F) ∈ fst Te ⟩
         → Σ[ m ∈ ⟨ fst n ∈ fst ωʟ ⟩ ] (fst F ≡ fst (eS n m))
  Te-out = Tb.T-out
```

選ばれた項目 `eS(n)` は `TabWit` の第二成分を満たします。`n` に記録された反復 `Zn` が単に存在し、`eS(n)` は単射 `Zn ↪ κ` を符号化します。この存在は表の特徴づけに存在性だけが含まれるため、切り詰められたままです。

```agda
  e-wit : (n : S) (m : ⟨ fst n ∈ fst ωʟ ⟩)
        → ∥ Σ[ Zn ∈ S ] (Holds Iter n Zn × InjCode (eS n m) Zn κ) ∥₁
  e-wit n m = Gt-out (eS n m) n (Tb.fn-holds n m) .snd
```

自然数 `k` の正準な数項に対しては、切り詰めが消去されます。その数項における表の項目は、反復 `hullStep k` から `κ` への単射を符号化します。`InjCode` が命題であるため、この消去は正当です。

```agda
  e-code : (k : ℕ) → InjCode (eS (nn k) (#∈ω k)) (hullStep k) κ
  e-code k = PT.rec (isPropInjCode (eS (nn k) (#∈ω k)) (hullStep k) κ) read (e-wit (nn k) (#∈ω k))
    where
    F : S
    F = eS (nn k) (#∈ω k)
```

まず、記録された反復が特定されます。反復の集合の要素は、単に、数項の成分と反復の成分の両方を読み取れる対であり、対の等式が記録された反復を特定します。

```agda
    read : Σ[ Zn ∈ S ] (Holds Iter (nn k) Zn × InjCode F Zn κ) → InjCode F (hullStep k) κ
    read (Zn , hI , code) = PT.rec (isPropInjCode F (hullStep k) κ) at
      (Iter-out (prʟ (nn k) Zn) (subst (λ w → ⟨ w ∈ fst Iter ⟩) (sym (prʟ-fst (nn k) Zn)) hI))
      where
      at : Σ[ k' ∈ ℕ ] (fst (prʟ (nn k) Zn) ≡ pr (# k') (fst (hullStep k'))) → InjCode F (hullStep k) κ
```

数項の等式は `k'` が `k` であることを強制し、コードは、二つの反復の同一視に沿って運ばれます。コード自体は変わりません。

```agda
      at (k' , q) = injcode-resp F F Zn (hullStep k) κ refl
        (snd ee ∙ cong (λ j → fst (hullStep j)) (sym (#-inj k k' (fst ee)))) code
        where
        ee : (# k ≡ # k') × (fst Zn ≡ fst (hullStep k'))
        ee = pr-inj (sym (prʟ-fst (nn k) Zn) ∙ q)
```

`FinWit p z` は、内部の数項 `n ∈ ω`、値 `v`、表の項目 `F` を単に記録します。その等式とグラフ所属は `p=(n,v)`、`Te(n)=F`、`F(z)=v` を表します。したがって `z` を数えるための対の符号は `F` ではなく `p` です。

```agda
  FinWit : (p z : S) → Type (ℓ-suc ℓ)
  FinWit p z = ∥ Σ[ n ∈ S ] Σ[ v ∈ S ] Σ[ F ∈ S ]
      ((fst p ≡ pr (fst n) (fst v)) × ⟨ fst n ∈ fst ωʟ ⟩ × Holds Te n F × Holds F z v) ∥₁
```

`inner₆` は二つの適用の主張の連言です。表 `Te` は `n` を項目 `F` へ写し、その項目は `z` を `v` へ写します。環境 `F,v,n,z,p,q` では、これらはちょうど `Holds Te n F` と `Holds F z v` です。

```agda
  opaque
    inner₆ : Formula S 6
    inner₆ = appC Te i2 i0 ∧̇ appAt i0 i3 i1
```

二つのアトムの埋め込みには、その妥当性の補題を使います。これにより、証人の記録が、一つの環境のもとで二つの適用のアトムの充足を産み出します。

```agda
    inner₆-in : (F v n z p q : S) → Holds Te n F → Holds F z v
              → ⟨ (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []) ⊨ inner₆ ⟩
    inner₆-in F v n z p q ht hv =
        subst ⟨_⟩ (sym (appC-adequate Te i2 i0 (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []))) ht
      , subst ⟨_⟩ (sym (appAt-adequate i0 i3 i1 (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []))) hv
```

二つのアトムを読むには、同じ妥当性の補題を順方向に使います。これで表の充足とグラフの所属が回復します。

```agda
    inner₆-out : (F v n z p q : S) → ⟨ (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []) ⊨ inner₆ ⟩
               → Holds Te n F × Holds F z v
    inner₆-out F v n z p q (ht , hv) =
        subst ⟨_⟩ (appC-adequate Te i2 i0 (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ [])) ht
      , subst ⟨_⟩ (appAt-adequate i0 i3 i1 (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ [])) hv
```

`nv₃` の自由変数は `z,p,q` であり、`n`、`v`、`F` の順に存在量化します。本体は `p=(n,v)`、`n ∈ ω`、`Te(n)=F`、`F(z)=v` を述べ、自由変数 `q` は使われません。

```agda
  opaque
    nv₃ : Formula S 3
    nv₃ = ∃̇ (∃̇ (prAtL i3 i1 i0 ∧̇ ((var i1 ∈̇ con ωʟ) ∧̇ ∃̇ inner₆)))
```

`p=(n,v)`、`n ∈ ω`、`Te(n)=F`、`F(z)=v` が与えられると、三つの証人 `n`、`v`、`F` が入れ子の存在量化子を満たします。対の妥当性が対の原子式を与え、`inner₆-in` が二つの適用の原子式を与えます。

```agda
    nv₃-in : (z p q n v F : S) → fst p ≡ pr (fst n) (fst v) → ⟨ fst n ∈ fst ωʟ ⟩
           → Holds Te n F → Holds F z v → ⟨ (z ∷ p ∷ q ∷ []) ⊨ nv₃ ⟩
    nv₃-in z p q n v F qp hn ht hv =
      ∣ n , ∣ v , ( subst ⟨_⟩ (sym (prAtL-adequate i3 i1 i0 (v ∷ n ∷ z ∷ p ∷ q ∷ []))) qp
                  , ( hn , ∣ F , inner₆-in F v n z p q ht hv ∣₁ ) ) ∣₁ ∣₁
```

`nv₃` を読むには、まず `n` の切り詰められた証人を除去し、次に `v` の切り詰められた証人を除去します。`n` と `v` を固定すると、`Inner n v` は対の原子式、所属 `n ∈ ω`、そして `inner₆` を満たす項目 `F` の三つ目の切り詰められた存在を保持します。

```agda
    nv₃-out : (z p q : S) → ⟨ (z ∷ p ∷ q ∷ []) ⊨ nv₃ ⟩ → FinWit p z
    nv₃-out z p q = PT.rec squash₁ at₁
      where
      Inner : (n v : S) → Type (ℓ-suc ℓ)
      Inner n v = ⟨ (v ∷ n ∷ z ∷ p ∷ q ∷ []) ⊨ prAtL i3 i1 i0 ⟩
```

最も内側の切り詰められた存在が与えるのは表の項目 `F` であり、すでに固定されている値 `v` ではありません。対の妥当性が対の原子式を `p=(n,v)` に変換し、`inner₆-out` が `Te(n)=F` と `F(z)=v` を復元します。これらのデータが `FinWit p z` を構成します。

```agda
                × ( ⟨ fst n ∈ fst ωʟ ⟩ × ∥ Σ[ F ∈ S ] ⟨ (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []) ⊨ inner₆ ⟩ ∥₁ )
      at₃ : (n v : S) → Inner n v → FinWit p z
      at₃ n v (qp , (hn , h)) = PT.map
        (λ { (F , hi) → n , v , F
           , ( subst ⟨_⟩ (prAtL-adequate i3 i1 i0 (v ∷ n ∷ z ∷ p ∷ q ∷ [])) qp
```

`n` と `v` を固定すると、最も内側の変換から `FinWit p z` が得られ、外側の二つの除去が `v` と `n` の切り詰められた選択を順に処理します。したがって `nv₃` の充足から、周囲の関係が要求する切り詰められた組がちょうど得られます。

```agda
             , hn , inner₆-out F v n z p q hi ) }) h
      at₂ : (n : S) → Σ[ v ∈ S ] Inner n v → FinWit p z
      at₂ n (v , h) = at₃ n v h
      at₁ : Σ[ n ∈ S ] ∥ Σ[ v ∈ S ] Inner n v ∥₁ → FinWit p z
      at₁ (n , h) = PT.rec squash₁ (at₂ n) h
```

最終の関係は、`prodL κ` と `hullL` の直積から分出によって得られます。これを定める論理式は `nv₃` であり、その三つの存在証人は、内部自然数 `n`、値 `v`、表の項目 `F` です。`p = (n,v)`、`n ∈ ω`、表が `n` で `F` を記録し、`F` が `z` で `v` を記録するとき、かつそのときに限り、この関係は `p` と `z` を結びます。

```agda
  private
    module FinalGraph = Relation (prodL κ) hullL nv₃ (λ p z → FinWit p z , squash₁)
      (λ p z q → nv₃-out z p q)
      (λ p z q → PT.rec (snd ((z ∷ p ∷ q ∷ []) ⊨ nv₃))
        (λ { (n , v , F , qp , hn , ht , hv) → nv₃-in z p q n v F qp hn ht hv }))
```

分離された集合は `Gf` と名付けられ、最終のグラフの構成可能な台になります。

```agda
  Gf : S
  Gf = FinalGraph.rel
```

`Gf` への所属を導入するには、`p ∈ prodL κ`、`z ∈ hullL`、内部自然数 `n ∈ ω`、値 `v`、表の項目 `F` を取ります。等式 `p = (n,v)` と、`Te` が `n` で `F` を記録し、`F` が `z` で `v` を記録するという二つのグラフ所属が、定義関係に必要な証人をちょうど与えます。

```agda
  Gf-in : (p z n v F : S) → ⟨ fst p ∈ fst (prodL κ) ⟩ → ⟨ fst z ∈ fst hullL ⟩
        → fst p ≡ pr (fst n) (fst v) → ⟨ fst n ∈ fst ωʟ ⟩ → Holds Te n F → Holds F z v
        → Holds Gf p z
  Gf-in p z n v F hp hz qp hn ht hv = FinalGraph.into p z hp hz ∣ n , v , F , qp , hn , ht , hv ∣₁
```

逆に、`Gf-out` はグラフへの所属を、命題的に切り詰められた記録 `FinWit p z` に変えます。この記録の切り詰めは、集合への所属や集合の等しさのような命題値の結論を示すときに消去できます。

```agda
  Gf-out : (p z : S) → Holds Gf p z → FinWit p z
  Gf-out = FinalGraph.pair-out
```

表の項目が記録する値はすべて `κ` に属します。`Te(n,F)` から、表の読みは `F` を `n` で選ばれた項目と同一視します。`e-wit` は、その選ばれた項目について、ある反復 `Zn` と `Zn` から `κ` への単射符号を与えます。`F(z)=v` を表の項目の同一視に沿って移せば、その符号の値域条件から `v ∈ κ` が従います。

```agda
  entry-ran : (n F z v : S) → Holds Te n F → Holds F z v → ⟨ fst v ∈ fst κ ⟩
  entry-ran n F z v ht hv = PT.rec (snd (fst v ∈ fst κ))
    (λ { (Zn , _ , code) → snd (snd (snd code)) z v
          (subst (λ w → ⟨ pr (fst z) (fst v) ∈ w ⟩) (Te-out n F ht .snd) hv) })
    (e-wit n (Te-out n F ht .fst))
```

`Gf` によって関係付けられる第一成分はすべて `prodL κ` に属します。その記録は第一成分を `(n,v)` と表し、`n ∈ ω` かつ `v ∈ κ` を与えます。有限でない順序数 `κ` は `ω` を含むので `n ∈ κ` でもあり、両方の座標が `κ` に属します。したがって `(n,v) ∈ prodL κ` です。

```agda
  inPκ : (p z : S) → Holds Gf p z → ⟨ fst p ∈ fst (prodL κ) ⟩
  inPκ p z h = PT.rec (snd (fst p ∈ fst (prodL κ)))
    (λ { (n , v , F , (qp , hn , ht , hv)) →
       subst (λ w → ⟨ w ∈ fst (prodL κ) ⟩) (sym qp)
         (prodL-in κ n v (ω⊆ (fst κ) oκ κ∉ω (fst n) hn) (entry-ran n F z v ht hv)) })
```

この議論を `Gf-out` が返す切り詰められた記録に適用すると、`inPκ` が得られます。すなわち、`Gf(p,z)` が成り立つなら、その第一成分 `p` は `prodL κ` に属します。

```agda
    (Gf-out p z h)
```

包の各要素には、それと関係する符号が単に存在します。反復の合併の特徴づけにより、`z` はある有限段階 `hullStep n` に属します。選ばれたグラフ `F = eS (# n)` について、`e-code n` はその定義域が `hullStep n` であることを正確に述べます。したがって、その全域性条件から、`F(z)=v` を満たす値 `v` が単に得られます。

```agda
  have-fin : (z : S) → ⟨ fst z ∈ fst hullL ⟩ → ∥ Σ[ p ∈ S ] Holds Gf p z ∥₁
  have-fin z hz = PT.rec squash₁ at (It.iterUnion-out z hz)
    where
    at : Σ[ n ∈ ℕ ] ⟨ fst z ∈ fst (hullStep n) ⟩ → ∥ Σ[ p ∈ S ] Holds Gf p z ∥₁
    at (n , hn) = PT.map val (domAt-in zero (suc zero) (F ∷ hullStep n ∷ []) (fst (snd (e-code n))) z hn)
```

`e-code n` の全域性条件は、値 `v` とグラフ所属 `F(z)=v` を与えます。標準数項 `# n` とこの値を対にすると、候補となる符号 `p = (# n,v)` が得られます。

```agda
      where
      F : S
      F = eS (nn n) (#∈ω n)
      val : Σ[ v ∈ S ] Holds F z v → Σ[ p ∈ S ] Holds Gf p z
      val (v , hv) = prʟ (nn n) v
```

導入は記録の全体を組み立てます。対は、数項の所属とコードの値域の条項によって積の中にあり、表自身の所属によって `z` と関係付けられます。

```agda
        , Gf-in (prʟ (nn n) v) z (nn n) v F
            (subst (λ w → ⟨ w ∈ fst (prodL κ) ⟩) (sym (prʟ-fst (nn n) v))
              (prodL-in κ (nn n) v (num∈κ n) (snd (snd (snd (e-code n))) z v hv)))
            hz (prʟ-fst (nn n) v) (#∈ω n) (Te-in (nn n) (#∈ω n)) hv
```

最小逆像の選択に必要な関数性は、候補となる符号から包へ向かいます。同じ `p` が `z` と `z'` の両方に関係するなら、`z = z'` です。この性質により、包の要素をその最小符号へ送る選択写像は単射になります。二つの関係の証人はいずれも切り詰められた記録ですが、ここでの目標は集合の等しさという命題なので、その切り詰めを消去できます。

```agda
  funct-fin : (p z z' : S) → Holds Gf p z → Holds Gf p z' → fst z ≡ fst z'
  funct-fin p z z' h h' = PT.rec2 (setIsSet (fst z) (fst z')) read (Gf-out p z h) (Gf-out p z' h')
    where
    read : Σ[ n ∈ S ] Σ[ v ∈ S ] Σ[ F ∈ S ]
             ((fst p ≡ pr (fst n) (fst v)) × ⟨ fst n ∈ fst ωʟ ⟩ × Holds Te n F × Holds F z v)
```

二つの記録を展開すると、`n,v,F` と `n',v',F'` がそれぞれ得られます。各記録は一つの対の等式、すなわち `p=(n,v)` または `p=(n',v')` と、三つの事実を含みます。その添字が `ω` に属すること、表がその添字で対応する項目を記録すること、そしてその項目が対応する包の要素で表示された値を記録することです。

```agda
         → Σ[ n' ∈ S ] Σ[ v' ∈ S ] Σ[ F' ∈ S ]
             ((fst p ≡ pr (fst n') (fst v')) × ⟨ fst n' ∈ fst ωʟ ⟩ × Holds Te n' F' × Holds F' z' v')
         → fst z ≡ fst z'
    read (n , v , F , (qp , hn , ht , hv)) (n' , v' , F' , (qp' , hn' , ht' , hv')) =
      PT.rec (setIsSet (fst z) (fst z'))
```

二つの対の等式から、まず `n=n'` と `v=v'` が得られます。次に、表の読みが `F` と `F'` を同じ選択項目 `eS n m` にそろえます。証人 `e-wit n m` は、この項目について、ある反復 `Zn` とその単射符号を与えます。二つのグラフ所属をこの共通の項目へ移し、さらに第二の値を `v'=v` に沿って移すと、単射性条件から `z=z'` が従います。

```agda
        (λ { (Zn , _ , code) →
           injAt-out zero (eS n m ∷ Zn ∷ []) (fst (snd (snd code))) v z z'
             (subst (λ w → ⟨ pr (fst z) (fst v) ∈ w ⟩) (Te-out n F ht .snd) hv)
             (subst2 (λ u w → ⟨ pr (fst z') u ∈ w ⟩) (sym (snd ee)) qF hv') })
        (e-wit n m)
```

順序対の単射性が、同一視を数項の成分と値の成分に分解します。そして表の読みが、数項が `ω` の中にあることを証明します。

```agda
      where
      ee : (fst n ≡ fst n') × (fst v ≡ fst v')
      ee = pr-inj (sym qp ∙ qp')
      m : ⟨ fst n ∈ fst ωʟ ⟩
      m = Te-out n F ht .fst
```

数項と `ω` への所属の二つの対は等しくなります。`ω` への所属が命題であり、数項の等式が底の集合の等式だからです。

```agda
      pth : _≡_ {A = Σ[ c ∈ S ] ⟨ fst c ∈ fst ωʟ ⟩} (n' , Te-out n' F' ht' .fst) (n , m)
      pth = Σ≡Prop (λ c → snd (fst c ∈ fst ωʟ)) (S≡ {x = n'} {y = n} (sym (fst ee)))
```

`F'` に対する表の読みを二つの内部自然数の添字の等しさに沿って移すと、`F'` は選択項目 `eS n m` と同一視されます。`F` に対する対応する読みと合わせると、二つのグラフ所属は同じ単射グラフの中に置かれます。

```agda
      qF : fst F' ≡ fst (eS n m)
      qF = Te-out n' F' ht' .snd ∙ (λ i → fst (eS (fst (pth i)) (snd (pth i))))
```

`γf` を、構成可能集合 `prodL κ` に対応する順序数段階とします。これにより、すべての候補符号を含む共通の段階 `Lset γf` が得られ、標準的な段階順序でそれらの逆像を比較できます。

```agda
  γf : V ℓ
  γf = stage (fst (prodL κ)) (snd (prodL κ))
```

その段階は、すべての段階と同じく順序数です。

```agda
  oγf : IsOrd γf
  oγf = stage-ord (fst (prodL κ)) (snd (prodL κ))
```

段階の定義的性質により、集合 `prodL κ` は `Lset γf` に属します。`Lset γf` は推移的なので、`prodL κ` の各要素も `Lset γf` に属します。したがって `prodL κ ⊆ Lset γf` です。

```agda
  prodκ⊆Lγ : (p : S) → ⟨ fst p ∈ fst (prodL κ) ⟩ → ⟨ fst p ∈ Lset γf ⟩
  prodκ⊆Lγ p hp =
    layer-trans (Lset-layer γf) {x = fst (prodL κ)} {y = fst p} hp (stage-mem (fst (prodL κ)) (snd (prodL κ)))
```

各 `z ∈ hullL` に対し、`Gf(p,z)` を満たす `p ∈ prodL κ` のうち、段階順序で最小のものを選びます。必要な三つの事実は、上で示したものです。関係する各 `p` は `prodL κ` に属し、この台は `Lset γf` に含まれ、各包の要素には関係する `p` が単に存在します。`funct-fin` により、一つの `p` が異なる二つの包の要素に関係することはないので、得られる最小逆像写像は内部で符号化された単射 `hullL ↪ prodL κ` になります。

```agda
  module LF = LeastPre γf oγf Gf hullL (prodL κ) inPκ prodκ⊆Lγ have-fin using ( module Functional )
```

最小逆像の構成は包から `prodL κ` への符号化された単射を与え、平方則は `prodL κ` から `κ` への符号化された単射を与えます。両者を合成すると、命題的に切り詰められた主張 `InjL hullL κ` が得られます。これは内部で符号化された単射であり、全射も基数の等しさも主張せず、崩壊像についても何も述べません。したがって、構成可能包のすべての要素には、内部で互いに異なる `κ` の符号があります。

```agda
  hull↪κ : InjL hullL κ
  hull↪κ = injl-trans hullL (prodL κ) κ (LF.Functional.injL funct-fin) pairκ
```