計数の目標は、`ω` の外にある内部の基数 `κ` と、始点からそれへの符号化された単射である。課題は、同じ基数で包全体を数えることである。
この包は有限反復 `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 ∈ˢ Z .fst ⟩ → ⟨ 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) → (z .fst ∈ D₂ .fst)
≡ ((z .fst ∈ ΦZ .fst) ⊓ ((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) → ⟨ z .fst ∈ ΦZ .fst ⟩ → (⟨ z .fst ∈ Z .fst ⟩ → ⊥₀) → ⟨ z .fst ∈ D₂ .fst ⟩
D₂-in z h nmem = subst ⟨_⟩ (sym (D₂-spec z)) (h , λ z∈ → lift (nmem z∈))
```
消去の規則は、仕様を通して `D₂` の所属を展開し、対象レベルの反証を通常の含意へと降ろす。
```agda
D₂-out : (z : S) → ⟨ z .fst ∈ D₂ .fst ⟩ → ⟨ z .fst ∈ ΦZ .fst ⟩ × (⟨ z .fst ∈ Z .fst ⟩ → ⊥₀)
D₂-out z h = r .fst , λ z∈ → lower (r .snd z∈)
where
r : ⟨ z .fst ∈ ΦZ .fst ⟩
× ⟨ (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) → (z .fst ∈ D∅ .fst)
≡ ((z .fst ∈ D₂ .fst) ⊓ ((z ∷ []) ⊨ var i0 ≐ con ∅ʟ))
D∅-spec z = hasSeparationL D₂ (var i0 ≐ con ∅ʟ) .fst .snd z
```
`D₂` の要素で空集合と等しいものは、二つのデータとともに `D∅` に入る。
```agda
opaque
D∅-in : (z : S) → ⟨ z .fst ∈ D₂ .fst ⟩ → z .fst ≡ ∅ → ⟨ z .fst ∈ D∅ .fst ⟩
D∅-in z h e = subst ⟨_⟩ (sym (D∅-spec z)) (h , e)
```
その消去は、仕様をそのまま読んだものである。`D₂` への所属と、空集合との等式である。
```agda
D∅-out : (z : S) → ⟨ z .fst ∈ D∅ .fst ⟩ → ⟨ z .fst ∈ D₂ .fst ⟩ × (z .fst ≡ ∅)
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) → (z .fst ∈ Dw .fst)
≡ ((z .fst ∈ D₂ .fst) ⊓ ((z ∷ []) ⊨ ¬̇ (var i0 ≐ con ∅ʟ)))
Dw-spec z = hasSeparationL D₂ (¬̇ (var i0 ≐ con ∅ʟ)) .fst .snd z
```
導入には、`D₂` への所属と、空集合との相等の反証が要る。
```agda
opaque
Dw-in : (z : S) → ⟨ z .fst ∈ D₂ .fst ⟩ → (z .fst ≡ ∅ → ⊥₀) → ⟨ z .fst ∈ Dw .fst ⟩
Dw-in z h ne = subst ⟨_⟩ (sym (Dw-spec z)) (h , λ q → lift (ne q))
```
消去は `D₂` への所属と、対象レベルから降ろされた反証を返す。
```agda
Dw-out : (z : S) → ⟨ z .fst ∈ Dw .fst ⟩ → ⟨ z .fst ∈ D₂ .fst ⟩ × (z .fst ≡ ∅ → ⊥₀)
Dw-out z h = r .fst , λ q → lower (r .snd q)
where
r : ⟨ z .fst ∈ D₂ .fst ⟩
× ⟨ (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 ∈ˢ ΦZ .fst ⟩ → ⟨ z ∈ˢ U₁.D .fst ⟩
ΦZ⊆ z h = go (FOL.Semantics.decideMembership 𝒮ᵥ lem z (Z .fst))
where
zS : S
zS = z , isL-trans {x = ΦZ .fst} {y = z} h (ΦZ .snd)
```
二つの場合は、和集合への二つの包含によって `U₁` に入る。すでに `Z` に属する要素には第一の包含を使い、そうでなければ `D₂-in` で新しい部分への所属を示してから第二の包含を使う。
```agda
go : Dec ⟨ z ∈ Z .fst ⟩ → ⟨ z ∈ U₁.D .fst ⟩
go (yes hz) = U₁.in₁ zS hz
go (no nz) = U₁.in₂ zS (D₂-in zS h nz)
```
新しい部分は第二の和集合で覆われる。これも空集合との等式についての排中律によるものである。
```agda
D₂⊆ : (z : V ℓ) → ⟨ z ∈ˢ D₂ .fst ⟩ → ⟨ z ∈ˢ U₃.D .fst ⟩
D₂⊆ z h = go (FOL.Semantics.decideEquality 𝒮ᵥ lem z ∅)
where
zS : S
zS = z , isL-trans {x = D₂ .fst} {y = z} h (D₂ .snd)
```
空集合と等しい要素は `D∅` から入り、異なる要素は `Dw` から入る。
```agda
go : Dec (z ≡ ∅) → ⟨ z ∈ U₃.D .fst ⟩
go (yes e) = U₃.in₁ zS (D∅-in zS h e)
go (no 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 = D∅ .fst} {y = z} hz (D∅ .snd)) 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 ]
((p .fst ≡ pr (s .fst) (e .fst)) × 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) → p .fst ≡ pr (s .fst) (e .fst)
→ 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 = 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) = 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 → (p .fst ∈ PB .fst) ⊓ (GW p z , squash₁))
(λ p z q h → h .fst , se₃-out z p q (h .snd))
(λ p z q h → h .fst , rec₁ (((z ∷ p ∷ q ∷ []) ⊨ se₃) .snd)
```
記述の条件の外向きの読みは、論理式そのものの外向きの読みであり、返ってくるのはまさに `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) → ⟨ p .fst ∈ PB .fst ⟩ → ⟨ z .fst ∈ Dw .fst ⟩
→ (s e : S) → p .fst ≡ pr (s .fst) (e .fst)
→ 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 → ⟨ p .fst ∈ PB .fst ⟩ × GW p z
G-out = WitnessGraph.pair-out
```
この関係が `Dw` 上で全域的なのは切り詰められた意味においてである。各 `z ∈ Dw` には `Holds G p z` を満たす `p` が単に存在する。`z ∈ ΦZ` を外向きに読むと、`z` が閉包に入った三つの可能な理由が現れる。
```agda
have : (z : S) → ⟨ z .fst ∈ Dw .fst ⟩ → ∥ Σ[ p ∶ S ] Holds G p z ∥₁
have z hz = 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) = ⊥₀-rec (D₂-out z (Dw-out z hz .fst) .snd h)
```
そのうちの二つはすでに分出によって排除されている。`z` は `Z` の古い要素でも空集合でもあり得ない。残るのは証人の場合であり、証人の論理式の外向きの補題を通して読まれる。
```agda
body (inr (inl e)) = ⊥₀-rec (Dw-out z hz .snd e)
body (inr (inr hw)) = 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') = 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 ∈ PB .fst ⟩) (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 ∈ˢ (envSet Z n) .fst ⟩) (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' → z .fst ≡ z' .fst
funct p z z' h h' = rec2 (setIsSet (z .fst) (z' .fst)) read (G-out p z h .snd) (G-out p z' h' .snd)
where
read : Σ[ s ∶ S ] Σ[ e ∶ S ]
((p .fst ≡ pr (s .fst) (e .fst)) × B.LeastWitness Z e s z)
```
二つの関係は外向きに読まれ、それぞれ鍵、環境、対の等式、そして最小証人を返す。
```agda
→ Σ[ s₂ ∶ S ] Σ[ e₂ ∶ S ]
((p .fst ≡ pr (s₂ .fst) (e₂ .fst)) × B.LeastWitness Z e₂ s₂ z')
→ z .fst ≡ z' .fst
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 : (s₂ .fst ≡ s .fst) × (e₂ .fst ≡ e .fst)
ee = pr-inj (sym q₂ ∙ q)
hw₂' : B.LeastWitness Z e s z'
hw₂' = subst2 (λ e' s' → B.LeastWitness Z e' s' z')
```
それらの同一視に沿って二つ目の最小証人の証明を輸送すると、二つの証明は同じ鍵と環境に関するものになる。そこで最小証人の一意性から `z .fst ≡ z' .fst` が得られる。
```agda
(S≡ {x = e₂} {y = e} (ee .snd)) (S≡ {x = s₂} {y = s} (ee .fst)) hw₂
```
符号の池には誕生の段階がある。`γG` は `PB` が階層に現れる段階である。
```agda
γG : V ℓ
γG = stage (PB .fst) (PB .snd)
```
その段階は順序数で添字づけられており、計数の補題が要求するのはこれである。
```agda
oγG : IsOrd γG
oγG = stage-ord (PB .fst) (PB .snd)
```
池はその誕生の段階に含まれる。段階の推移性によるものである。`γG` で生まれた集合の要素は `Lset γG` に属する。
```agda
PB⊆Lγ : (p : S) → ⟨ p .fst ∈ PB .fst ⟩ → ⟨ p .fst ∈ Lset γG ⟩
PB⊆Lγ p hp = layer-trans (Lset-layer γG) {x = PB .fst} {y = p .fst} hp (stage-mem (PB .fst) (PB .snd))
```
これらの仮定によって `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 ∈ˢ Z .fst ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
→ InjL Z κ → InjL (B.Φ Z) κ
step-count Z Z⊆ = rec₁ squash₁ (λ { (E , cE) → OneStep.result Z Z⊆ E cE })
```
有限閉包の各反復の要素は、すべて周囲の段階 `Lset lam` の中にある。これは、反復が包に含まれ、包の要素がすべて段階の中にあることから従う。
```agda
iter⊆L : (n : ℕ) (z : V ℓ) → ⟨ z ∈ˢ (hullStep n) .fst ⟩ → ⟨ 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 0 = 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 ] (⟨ F .fst ∈ Lset σ ⟩ × InjCode F (hullStep n) κ) ∥₁ , squash₁
```
各 `n` に対し、`HoldsAt n` を満たす最小の順序数段階を `ls n` とする。`counted n` が与える切り詰められた単射から存在が従い、得られる最小性の主張は命題なので、最小順序数を選択できる。
```agda
opaque
ls : (n : ℕ) → LeastOrd (HoldsAt n)
ls n = 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 (F .fst) (F .snd) , stage-ord (F .fst) (F .snd)
, ∣ F , stage-mem (F .fst) (F .snd) , 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 = map₁ raise (ls n .snd .snd .fst)
where
raise : Σ[ F ∶ S ] (⟨ F .fst ∈ Lset (ls n .fst) ⟩ × InjCode F (hullStep n) κ)
→ Σ[ F ∶ S ] (⟨ F .fst ∈ 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 : Lγ .fst ≡ Lset γ
Lγ-fst = refl
```
反復そのものも、一つの構成可能な集合に集められる。`Iter` は、各内部の数項と、それが索引づける閉包の反復とを対にする。
```agda
Iter : S
Iter = It.iter
```
反復集合の導入により、数項とその反復の各対は要素になる。
```agda
Iter-in : (n : ℕ) → ⟨ pr (# n) ((hullStep n) .fst) ∈ Iter .fst ⟩
Iter-in = It.iter-in
```
逆に、すべての要素は、単に、そのような対である。したがって `Iter` の中の所属は、数え上げられた反復だけを指認し、それ以外は何も指認しない。
```agda
Iter-out : (y : S) → ⟨ y .fst ∈ Iter .fst ⟩ → ∥ Σ[ n ∶ ℕ ] (y .fst ≡ pr (# n) ((hullStep n) .fst)) ∥₁
Iter-out = It.iter-out
```
内部の数項 `n` における構成可能なコード `F` の表の証人は、二つの事実からなる。`F` が共通の段階に属すること、そして単に、`n` に記録された反復 `Zn` で、`F` が `Zn` から `κ` への単射を符号化することがあることである。
```agda
TabWit : (F n : S) → Type (ℓ-suc ℓ)
TabWit F n = ⟨ F .fst ∈ 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 → ⟨ F .fst ∈ w ⟩) Lγ-fst hF
, 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 → ⟨ F .fst ∈ w ⟩) (sym Lγ-fst) hF
, 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× ((F .fst ∈ Lset γ) .snd) 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) → ⟨ F .fst ∈ Lset γ ⟩ → ⟨ n .fst ∈ ωʟ .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 → ⟨ F .fst ∈ 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) → ⟨ n .fst ∈ ωʟ .fst ⟩ → ∥ Σ[ F ∶ S ] Holds Gt F n ∥₁
have-code n hn = rec₁ squash₁ at (It.ω-num n hn)
where
at : It.Num n → ∥ Σ[ F ∶ S ] Holds Gt F n ∥₁
at (k , qk) = map₁
```
そしてコードが表の中に導入される。反復の同一視は数項の等式に沿って運ばれ、項目は、数項とその固有の反復の対を記録する。
```agda
(λ { (F , hF , code) → F
, Gt-in F n (hullStep k) hF hn
(subst (λ w → ⟨ pr w ((hullStep k) .fst) ∈ Iter .fst ⟩) (cong (λ p → p .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 → ⟨ F .fst ∈ w ⟩) (sym Lγ-fst) (Gt-out F n h .fst))
(λ F hF → subst (λ w → ⟨ F .fst ∈ 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) → ⟨ n .fst ∈ ωʟ .fst ⟩ → S
eS = Tb.fn
```
各 `n ∈ ω` について、順序対 `(n,eS(n))` は `Te` に属する。したがって `Te` は、選ばれた符号を数項 `n` での値として記録する。
```agda
Te-in : (n : S) (m : ⟨ n .fst ∈ ωʟ .fst ⟩) → ⟨ pr (n .fst) ((eS n m) .fst) ∈ Te .fst ⟩
Te-in = Tb.T-in
```
逆に、`(n,F) ∈ Te` なら `n ∈ ω` であり、`F` の底集合は選ばれた項目 `eS(n)` の底集合に等しくなる。`n ∈ ω` の所属証明は命題値なので、それによって別の表の値が生じることはない。
```agda
Te-out : (n F : S) → ⟨ pr (n .fst) (F .fst) ∈ Te .fst ⟩
→ Σ[ m ∶ ⟨ n .fst ∈ ωʟ .fst ⟩ ] (F .fst ≡ (eS n m) .fst)
Te-out = Tb.T-out
```
選ばれた項目 `eS(n)` は `TabWit` の第二成分を満たす。`n` に記録された反復 `Zn` が単に存在し、`eS(n)` は単射 `Zn ↪ κ` を符号化する。この存在は表の特徴づけに存在性だけが含まれるため、切り詰められたままである。
```agda
e-wit : (n : S) (m : ⟨ n .fst ∈ ωʟ .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 = 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) = rec₁ (isPropInjCode F (hullStep k) κ) at
(Iter-out (prʟ (nn k) Zn) (subst (λ w → ⟨ w ∈ Iter .fst ⟩) (sym (prʟ-fst (nn k) Zn)) hI))
where
at : Σ[ k' ∶ ℕ ] ((prʟ (nn k) Zn) .fst ≡ pr (# k') ((hullStep k') .fst)) → InjCode F (hullStep k) κ
```
数項の等式は `k'` が `k` であることを強制し、コードは、二つの反復の同一視に沿って運ばれる。コード自体は変わらない。
```agda
at (k' , q) = injcode-resp F F Zn (hullStep k) κ refl
(ee .snd ∙ cong (λ j → (hullStep j) .fst) (sym (#-inj k k' (ee .fst)))) code
where
ee : (# k ≡ # k') × (Zn .fst ≡ (hullStep k') .fst)
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 ]
((p .fst ≡ pr (n .fst) (v .fst)) × ⟨ n .fst ∈ ωʟ .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) → p .fst ≡ pr (n .fst) (v .fst) → ⟨ n .fst ∈ ωʟ .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 = 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
× ( ⟨ n .fst ∈ ωʟ .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)) = 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) = 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 → rec₁ (((z ∷ p ∷ q ∷ []) ⊨ nv₃) .snd)
(λ { (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) → ⟨ p .fst ∈ (prodL κ) .fst ⟩ → ⟨ z .fst ∈ hullL .fst ⟩
→ p .fst ≡ pr (n .fst) (v .fst) → ⟨ n .fst ∈ ωʟ .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 → ⟨ v .fst ∈ κ .fst ⟩
entry-ran n F z v ht hv = rec₁ ((v .fst ∈ κ .fst) .snd)
(λ { (Zn , _ , code) → ((code .snd) .snd) .snd z v
(subst (λ w → ⟨ pr (z .fst) (v .fst) ∈ 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 → ⟨ p .fst ∈ (prodL κ) .fst ⟩
inPκ p z h = rec₁ ((p .fst ∈ (prodL κ) .fst) .snd)
(λ { (n , v , F , (qp , hn , ht , hv)) →
subst (λ w → ⟨ w ∈ (prodL κ) .fst ⟩) (sym qp)
(prodL-in κ n v (ω⊆ (κ .fst) oκ κ∉ω (n .fst) 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) → ⟨ z .fst ∈ hullL .fst ⟩ → ∥ Σ[ p ∶ S ] Holds Gf p z ∥₁
have-fin z hz = rec₁ squash₁ at (It.iterUnion-out z hz)
where
at : Σ[ n ∶ ℕ ] ⟨ z .fst ∈ (hullStep n) .fst ⟩ → ∥ Σ[ p ∶ S ] Holds Gf p z ∥₁
at (n , hn) = map₁ val (domAt-in zero (suc zero) (F ∷ hullStep n ∷ []) (((e-code n) .snd) .fst) 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 ∈ (prodL κ) .fst ⟩) (sym (prʟ-fst (nn n) v))
(prodL-in κ (nn n) v (num∈κ n) ((((e-code n) .snd) .snd) .snd 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' → z .fst ≡ z' .fst
funct-fin p z z' h h' = rec2 (setIsSet (z .fst) (z' .fst)) read (Gf-out p z h) (Gf-out p z' h')
where
read : Σ[ n ∶ S ] Σ[ v ∶ S ] Σ[ F ∶ S ]
((p .fst ≡ pr (n .fst) (v .fst)) × ⟨ n .fst ∈ ωʟ .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 ]
((p .fst ≡ pr (n' .fst) (v' .fst)) × ⟨ n' .fst ∈ ωʟ .fst ⟩ × Holds Te n' F' × Holds F' z' v')
→ z .fst ≡ z' .fst
read (n , v , F , (qp , hn , ht , hv)) (n' , v' , F' , (qp' , hn' , ht' , hv')) =
rec₁ (setIsSet (z .fst) (z' .fst))
```
二つの対の等式から、まず `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 ∷ []) (((code .snd) .snd) .fst) v z z'
(subst (λ w → ⟨ pr (z .fst) (v .fst) ∈ w ⟩) (Te-out n F ht .snd) hv)
(subst2 (λ u w → ⟨ pr (z' .fst) u ∈ w ⟩) (sym (ee .snd)) qF hv') })
(e-wit n m)
```
順序対の単射性が、同一視を数項の成分と値の成分に分解する。そして表の読みが、数項が `ω` の中にあることを証明する。
```agda
where
ee : (n .fst ≡ n' .fst) × (v .fst ≡ v' .fst)
ee = pr-inj (sym qp ∙ qp')
m : ⟨ n .fst ∈ ωʟ .fst ⟩
m = Te-out n F ht .fst
```
数項と `ω` への所属の二つの対は等しくなる。`ω` への所属が命題であり、数項の等式が底の集合の等式だからである。
```agda
pth : let
left : Σ[ c ∶ S ] ⟨ c .fst ∈ ωʟ .fst ⟩
left = n' , Te-out n' F' ht' .fst
right : Σ[ c ∶ S ] ⟨ c .fst ∈ ωʟ .fst ⟩
right = n , m
in left ≡ right
pth = Σ≡Prop (λ c → (c .fst ∈ ωʟ .fst) .snd) (S≡ {x = n'} {y = n} (sym (ee .fst)))
```
`F'` に対する表の読みを二つの内部自然数の添字の等しさに沿って移すと、`F'` は選択項目 `eS n m` と同一視される。`F` に対する対応する読みと合わせると、二つのグラフ所属は同じ単射グラフの中に置かれる。
```agda
qF : F' .fst ≡ (eS n m) .fst
qF = Te-out n' F' ht' .snd ∙ (λ i → (eS ((pth i) .fst) ((pth i) .snd)) .fst)
```
`γf` を、構成可能集合 `prodL κ` に対応する順序数段階とする。これにより、すべての候補符号を含む共通の段階 `Lset γf` が得られ、標準的な段階順序でそれらの逆像を比較できる。
```agda
γf : V ℓ
γf = stage ((prodL κ) .fst) ((prodL κ) .snd)
```
その段階は、すべての段階と同じく順序数である。
```agda
oγf : IsOrd γf
oγf = stage-ord ((prodL κ) .fst) ((prodL κ) .snd)
```
段階の定義的性質により、集合 `prodL κ` は `Lset γf` に属する。`Lset γf` は推移的なので、`prodL κ` の各要素も `Lset γf` に属する。したがって `prodL κ ⊆ Lset γf` である。
```agda
prodκ⊆Lγ : (p : S) → ⟨ p .fst ∈ (prodL κ) .fst ⟩ → ⟨ p .fst ∈ Lset γf ⟩
prodκ⊆Lγ p hp =
layer-trans (Lset-layer γf) {x = (prodL κ) .fst} {y = p .fst} hp (stage-mem ((prodL κ) .fst) ((prodL κ) .snd))
```
各 `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κ
```