---
title: "凝縮を通して構造を移す"
module: L.GCH.CondensationTransfer
lang: ja
site: "Bedrock"
description: "凝縮を通して構造を移す"
stage: "GCH の証明"
reading_order: 107
canonical: https://bedrock.institute/ja/L.GCH.CondensationTransfer.html
html: L.GCH.CondensationTransfer.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/CondensationTransfer.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Semantics, V.Hierarchy, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.GCH.SkolemHull, L.GCH.HierarchyDescription, L.GCH.AdequateStages]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.CondensationTransfer.md, https://bedrock.institute/zh/L.GCH.CondensationTransfer.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

# 凝縮を通して構造を移す

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

ここで宇宙レベルとこの古典的パラメータを固定する。以下の集合はすべて、レベル `ℓ` の周囲の累積階層に属する。構成可能段階、Skolem 包、崩壊像も同じ累積階層の集合である。完全な初等性は、非有界な存在量化を含む論理式を移す。段階の絶対性、初等性、崩壊同型から作られた有界なインターフェースは、崩壊を通る Δ₀ の移送を外に示す。この二つの使い方を分けることが、凝縮の証明では欠かせない。

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

```agda
open import FOL.ZFStructure using ( module hPropView )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ∃̇_ )
open import FOL.Manipulation.ConstantMapping using ( mapFo; embed )
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using
  ( IsOrd; isL; Lset; Lset-out; Lset-mono; Lset→isL; 𝒟ₒ )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc; ord∈Lset→∈ )
open import L.Axioms.Basic {ℓ} using ( Lset-suc )
open import L.GCH.SkolemHull {ℓ} lem using
  ( module HullStage; Δ₀-isOrdAt; module Amb
  ; module Frame; _⊨ₚ_; embed-map; isOrd-at-p )
open import L.GCH.HierarchyDescription {ℓ} lem using ( levelFo; Δ₀-levelFo; level-sound; level-complete )
open import L.GCH.AdequateStages {ℓ} lem using ( Superadequate; Adequate; Lset∈suc )
```

本章では、初等的な Skolem 包が Mostowski 崩壊の後にどのような集合になるかを調べる。順序数の添字 `lam` において必要な仮定を与えると、崩壊像はある順序数 `β` が添字づける `Lset β` と同一視される。この結論は `β` と `lam` を比較せず、そのような添字の最小のものを選ばず、基数評価も与えない。証明はまず、構成可能段階の関係を有界な一階論理式で記述し、崩壊の前後で読めるようにする。

定理は `ℓ-suc ℓ` における排中律をパラメータとする。この一つの古典的仮定は、順序数段階、Skolem 包、階層の記述、十分な段階について先に得られた結果へ渡される。ここでの議論は選択原理を導入しない。存在論理式の充足と、強化された十分さが与える局所的な段階の証人は命題的切り詰めのままなので、行き先が再び命題である場合にだけ使われる。

以下で作る二つの問い合わせに必要なのは、対象言語の所属、等号、連言、非有界な存在量化だけである。論理式を周囲の階層、段階、Skolem 包の間で移すとき、その定数のアルファベットは変わる。`mapFo` は既存の定数を付け替え、`embed` は定数を含まない論理式を新しい定数アルファベット上の論理式とみなす。どちらも変数の位置や論理構造を変えない。

構成可能階層では、順序数の添字 `d` と、それが添字づける段階 `Lset d` を常に区別しなければならない。`lam` が順序数なら、`Lset lam` の要素は構成可能である。逆に、順序数 `d` が `Lset lam` に属するなら、階数の比較によって `d ∈ lam` が得られる。下向きの特徴づけ `Lset-out` が述べるのは、段階の要素が、ある `c ∈ lam` に対する `𝒟ₒ (Lset c)` から単に来るということだけであり、誕生段階を一つ選んで保持するわけではない。さらに、厳密な添字関係 `β ∈ α` があれば、単調性によって `Lset β` の要素を `Lset α` へ移せる。

中心となる論理式は `levelFo(a,p,z)` である。その Δ₀ の証拠により、有界絶対性を使い、崩壊に沿って移送できる。健全性は、`a`、`p`、`z` が構成可能であるとき、充足から `a ≡ Lset p` が従うことを述べる。補助的な上界 `z` は一意である必要がない。完全性は、`γ` が十分で、`p` が順序数であり、`p ∈ γ` であるとき、特定の三つ組 `(Lset p,p,Lset γ)` が論理式を満たすことを与える。周囲の理論は、Skolem 包上の移送と、そのような三つ組を作るための局所的な十分な添字を供給する。

有限ベクトルは論理式を評価する環境を記録し、積は証明で必要となる所属と等しさの事実を組み合わせる。この章に現れるいくつかの存在は、命題的切り詰めのもとにある。構成子 `∣_∣₁` は明示的な局所証人を切り詰めの中へ入れ、`rec₁` と `map₁` はそれを別の命題を得るためにだけ使う。とくに、強化された十分さが与える局所的な十分な添字が、大域的に選ばれた族になることはない。

`d` が順序数なら、集合論的後続 `sucV d` は次の順序数添字である。また、後続段階の等式 `Lset (sucV d) ≡ 𝒟ₒ (Lset d)` もこの添字を使う。この二つの事実は関係しているが、後続の添字と、その添字における段階は別の集合である。空集合が別に現れるのは、Skolem 包の構成が、周囲の添字にすでに属する予備の要素を必要とするためである。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; module InfinitySet )
open InfinitySet {ℓ} using ( sucV )
```

命題値の階層構造を開くと、台 `S` と周囲の所属の記法 `_∈ˢ_` が定まる。山括弧 `⟨_⟩` は、その真理値が運ぶ証明の型を取り出す。したがって、`d ∈ˢ lam`、構成可能段階への所属、崩壊像への所属は周囲の集合論における主張であり、論理式の内部で使う対象言語の原子 `_∈̇_` とは区別される。

```agda
open hPropView 𝒮ᵥ
```

周囲の意味論は、長さ `n` の環境を表す記法 `Vec S n` を与える。論理式のスロットはこのようなベクトルから読まれ、新しく束縛された存在の証人は先頭に置かれて、以前のスロットを外側へずらす。そのため、後で三重に入れ子になった証人は、外側から `z`、`p`、`a` の順に導入されても、最終的には `(a,p,z)` の順に読まれる。

```agda
module SemVᵃ = FOL.Semantics 𝒮ᵥ
```

## 階層の証人を特定する論理式

論理式 `isOrd-at-p` は、三項環境の中央のスロットだけを使う。第一の連言支は `p` が推移的であることを述べ、第二の連言支は `p` の各要素が推移的であることを述べる。ここに示す二つの関数は、その二つの有界な節を `IsOrd p` の二つの成分へ展開する。隣の値 `a` と `z` はこの補題では何の役割も果たさない。また、この補題は `levelFo` の残りを読み取らず、`a` を構成可能段階と同一視することもない。

```agda
isOrd-at-p-out : (a p z : S) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ₚ isOrd-at-p ⟩ → IsOrd p
isOrd-at-p-out a p z h =
    ( λ {x₁} {y} y∈x₁ x₁∈p → h .fst x₁ x₁∈p y y∈x₁ )
  , ( λ b b∈p {x₁} {y} y∈x₁ x₁∈b → h .snd b b∈p x₁ x₁∈b y y∈x₁ )
```

## 崩壊を通して階層の情報を移す

順序数 `lam` と、Skolem 包を含む周囲の構成可能段階 `Lset lam` を固定する。この添字は集合論的後続について閉じ、生成集合 `X` の各要素はこの段階に属する。また `∅ ∈ lam` は、Skolem 包の構成に必要な既定の要素を与える。この最初の仮定群の最後は完全な初等性である。パラメータが包から取られるなら、非有界量化子を含む論理式も含め、すべての論理式は包と周囲の段階で同じ真理値をもつ。

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

```agda
module Condense (lam : S) (ordλ : IsOrd lam)
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
  (elem : Frame.A.Elementary lam ordλ succλ X X⊆L ∅∈λ)
  (sup : Superadequate lam)
  (pixL : (x : S) → ⟨ x ∈ˢ HullStage.C.πX lam ordλ succλ X X⊆L ∅∈λ ⟩
        → ⟨ isL x ⟩)
  where
```

</summary>
<div class="submodule-fold-content">

さらに二つの仮定が、局所的な段階と構成可能な崩壊値を与える。`Superadequate lam` は、各 `d ∈ lam` が、`γ ∈ lam` を満たすある十分な順序数添字 `γ` に単に含まれることを述べる。命題的切り詰めは、特定の `γ` も最小のものも保持しない。仮定 `pixL` は各点についての主張である。崩壊像の各要素が構成可能であると言うだけで、崩壊像そのものが構成可能な集合であることも、それを特定の段階と同一視することも、まだ述べていない。

ここからは三つの構造を同時に使う。`Lset lam` 上の周囲の構造、Skolem 包の要素を台とする構造、そして推移的な崩壊像である。包の要素は、基礎となる集合と、それが `M` に属するという証明をともに携える。有界な論理式は最初の二つの構造の間で読め、崩壊を通して双方向に移せる。個々の所属の事実も崩壊の向こうへ送れる。これらの Δ₀ インターフェースを使うのは、完全な初等性によって非有界な存在問い合わせを処理した後だけである。

```agda
  module F = Frame lam ordλ succλ X X⊆L ∅∈λ using (module A; module Carry; module HS)
  module A = F.A using (SM; module SemM; inL)
  module Mse = A.SemM.At A.SM id using (_⊨_)
  module HS = F.HS using (module ASt; module C; module Condense; module H; M)
  module Cy = F.Carry elem using (atL; atM; member-push; push; pull)
```

包含 `Hull⊆L` は、Skolem 包の要素から周囲の段階へ渡る基本的な橋である。`x ∈ M` ならば `x ∈ Lset lam` が成り立つ。この事実は `A.inL` が必要とする段階への所属の証拠を与え、後では `isLλ` を通して、包から返された各証人を構成可能な集合にする。これは包が段階に各点で含まれるという主張であり、包そのものが段階の要素であるという主張ではない。

```agda
  open HS.H using ( Hull⊆L )
```

以上のデータから定まる Skolem 包を `M` と書く。`Hull⊆L` により、その各要素は `Lset lam` に属する。しかし、この記法だけから `M` 全体の構成可能性や新たな閉性が従うわけではない。したがって、以下で崩壊を使うたびに、その引数が `M` に属するという前提を保つ。

```agda
  M : S
  M = HS.M
```

Mostowski 崩壊写像を `π`、その推移的な像を `πX` と書く。Skolem 包の要素上で、`π` は所属関係を保存し、有界な真理を像における読みに移す。ここからの課題は、`πX` に十分な段階の閉性と被覆の性質を示し、この推移的集合がちょうど一つの段階 `Lset β` であることを導くことである。

```agda
  π : S → S
  π = HS.C.π
```

`lam` が順序数なので、`Lset lam` への所属から構成可能性が得られる。補助関数 `isLλ` は、まさにこの含意をまとめたものである。Skolem 包の問い合わせから返された三つの成分すべてにこれを適用してから `level-sound` を使う。`levelFo` の充足だけでは、その健全性定理が要求する構成可能性の仮定は得られないからである。

```agda
  isLλ : (x : S) → ⟨ x ∈ˢ Lset lam ⟩ → ⟨ isL x ⟩
  isLλ = Lset→isL lam ordλ
```

次の二つの基本的な所属の補題が、周囲の段階に置く証人を準備する。まず `d ∈ lam` とする。後続についての閉性から `sucV d ∈ lam` が得られ、段階全体 `Lset d` は `Lset (sucV d)` の一つの要素であり、`Lset-mono` がその要素を `Lset lam` へ移す。結論 `Lset d ∈ Lset lam` は集合の間の所属であり、一つの段階が別の段階に各点で含まれるという意味ではない。

```agda
  Lset∈Lλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ Lset d ∈ˢ Lset lam ⟩
  Lset∈Lλ d d∈λ = Lset-mono {α = lam} {β = sucV d} (succλ d d∈λ) (Lset∈suc d)
```

さらに `d` が順序数なら、`ord∈Lset-suc` は添字 `d` 自身を `Lset (sucV d)` に入れ、同じ単調性の一歩がそれを `Lset lam` へ移す。二つの補題を合わせると、`d` と `Lset d` という別々の段階要素が得られる。周囲の段階の内部で階層の論理式を証明するときには両方が必要であり、どちらの所属も、その出発点となった添字関係 `d ∈ lam` と混同してはならない。

```agda
  ord∈Lλ : (d : S) → IsOrd d → ⟨ d ∈ˢ lam ⟩ → ⟨ d ∈ˢ Lset lam ⟩
  ord∈Lλ d od d∈λ =
    Lset-mono {α = lam} {β = sucV d} (succλ d d∈λ) (ord∈Lset-suc d od)
```

Skolem 包の要素 `d` について、順序数性を崩壊の向こうへ送れる。`Amb.isOrdAt-in` は、定数を含まない有界な論理式 `isOrdAt` によって `IsOrd d` を表す。`Cy.push` はこの Δ₀ の真理を包の環境から `π d` を含む環境へ移し、`Amb.isOrdAt-out` が結果を `IsOrd (π d)` として読み取る。有界性の証拠がこの移送を制御し、`Cy.push` がまとめている比較は、最終的には Skolem 包の初等的な包含と崩壊同型に基づく。

```agda
  ord-push : (d : S) (d∈M : ⟨ d ∈ˢ M ⟩) → IsOrd d → IsOrd (π d)
  ord-push d d∈M od =
    Amb.isOrdAt-out (π d)
      (Cy.push Δ₀-isOrdAt ((d , d∈M) ∷ []) (Amb.isOrdAt-in d od))
```

同じ有界な記述は逆向きにも移せる。`IsOrd (π d)` から出発すると、`Cy.pull` が `isOrdAt` の真理をもとの Skolem 包の要素へ戻し、それを `IsOrd d` として読み取れる。したがって、崩壊は `M` の要素について順序数性を保存し、反映する。これは仮定 `d ∈ M` のもとでの局所的な同値であり、任意の周囲の集合に対する `π` の振る舞いを述べるものではない。

```agda
  ord-pull : (d : S) (d∈M : ⟨ d ∈ˢ M ⟩) → IsOrd (π d) → IsOrd d
  ord-pull d d∈M oπd =
    Amb.isOrdAt-out d
      (Cy.pull Δ₀-isOrdAt ((d , d∈M) ∷ []) (Amb.isOrdAt-in (π d) oπd))
```

最初の存在問い合わせは、指定された段階 `Lset d` を Skolem 包の内部で取り戻すためのものである。三つの非有界な存在量化によって環境 `(a,d′,z)` が得られる。埋め込まれた核は `levelFo(a,d′,z)` を要求し、第二の連言支の等式が、返された中央の座標を `d′ ≡ dM` として固定する。Δ₀ なのは `levelFo` だけである。その外側の問い合わせ `findA` は有界ではないので、証人を周囲の段階から Skolem 包へ移すには、Δ₀ 絶対性だけでなく完全な初等性を使う。この等式が `findA` と後の問い合わせ `findP` を分ける。後者が返す添字 `p′` は、外側で準備した `p` と等しい必要がない。

```agda
  findA : A.SM → Formula A.SM 0
  findA dM = ∃̇ (∃̇ (∃̇ (embed levelFo ∧̇ (var (suc zero) ≐ con dM))))
```

補題 `stageA` は、後で初等性によって Skolem 包へ引き戻す周囲の証人を作る。順序数 `d` を含む十分な添字 `γ`、基礎にある集合が `d` に等しい包の代表 `dM`、そして `d`、`Lset d`、`Lset γ` がそれぞれ `Lset lam` の要素であるという証拠を受け取る。完全性が `levelFo(Lset d,d,Lset γ)` を与え、有界絶対性がこの核を段階の構造で読み、対象言語の等式には `dM` の基礎にある集合から `d` へのパスを使う。その後、三つの非有界な存在の節は、命題的切り詰めのもとで `Lset γ`、`d`、`Lset d` によって順に証明される。ここでは `γ` が最小であるとは主張しない。

```agda
  stageA : (d γ : S) (od : IsOrd d) (adγ : Adequate γ) (d∈γ : ⟨ d ∈ˢ γ ⟩)
         → (dM : A.SM) → dM .fst ≡ d
         → ⟨ d ∈ˢ Lset lam ⟩ → ⟨ Lset d ∈ˢ Lset lam ⟩ → ⟨ Lset γ ∈ˢ Lset lam ⟩
         → ⟨ [] HS.ASt.AbsL.⊨ᵐ mapFo A.inL (findA dM) ⟩
  stageA d γ od adγ d∈γ dM ed d∈ Ld∈ Lγ∈ =
```

周囲で用いる証人は、十分な上界 `Lset γ`、指定された添字 `d`、そしてその段階 `Lset d` である。最終的な環境は `(Lset d,d,Lset γ)` となるので、完全性が段階の記述の連言支を与える。等式の連言支には `sym ed` が必要である。問い合わせは返された添字が `dM` の解釈に等しいことを求めるが、`ed` はその解釈を `d` と同一視する逆向きのパスだからである。各存在証人は命題的切り詰めのもとに置かれ、この三つ組を正準的に選ぶことなく、その存在だけを保つ。

```agda
    ∣ (Lset γ , Lγ∈) , ∣ (d , d∈) , ∣ (Lset d , Ld∈) , (sat , sym ed) ∣₁ ∣₁ ∣₁
    where
    δ : Vec HS.ASt.SL 3
    δ = (Lset d , Ld∈) ∷ (d , d∈) ∷ (Lset γ , Lγ∈) ∷ []
```

段階の記述に関する完全性が、ここでの数学的な核を与える。`γ` が十分であり、`d` が順序数で、`d ∈ γ` なので、三つ組 `(Lset d,d,Lset γ)` は周囲の階層で `levelFo` を満たす。十分さは記述に使う表を共通の上界に入れ、順序数性は `d` を正当な段階の添字にし、`d ∈ γ` はその添字を上界の下に置く。残る課題は、この同じ Δ₀ の事実を `Lset lam` 上の構造で読むことである。

```agda
    amb : ⟨ (Lset d ∷ d ∷ Lset γ ∷ []) ⊨ₚ levelFo ⟩
    amb = level-complete γ adγ d od d∈γ
```

次に、周囲での真理を `Lset lam` 上の段階構造での真理として表す。この時点ではまだ Skolem 包へ移していない。`Cy.atL` を逆向きに使うと、Δ₀ 論理式 `levelFo` を、その段階の三つの要素のもとで読める。続いてパス `embed-map` が、内容を持たない定数の改名を `embed levelFo` と同一視する。周囲の問い合わせは Skolem 包の要素を定数として使うが、`levelFo` 自身の定数域は空だからである。したがって `sat` は `stageA` が必要とする埋め込まれた核をちょうど与える。完全な初等性を使うのは、非有界な問い合わせ全体を組み立てた後である。

```agda
    sat : ⟨ δ HS.ASt.AbsL.⊨ᵐ mapFo A.inL (embed levelFo) ⟩
    sat = subst (λ ψ → ⟨ δ HS.ASt.AbsL.⊨ᵐ ψ ⟩) (sym (embed-map A.inL levelFo))
            (subst ⟨_⟩ (sym (Cy.atL Δ₀-levelFo δ)) amb)
```

第二の問い合わせも段階の記述を満たす三つ組 `(u,a,z)` を求めるが、付加条件が異なる。中央の座標を指定された添字と同一視する代わりに、`yM` と名づけられた Skolem 包の要素が第一座標 `u` に属することを要求する。したがって求めるのは、`y` を含む正しく記述された構成可能段階であり、その添字は固定されない。被覆の議論に必要なのは、まさにこの条件である。

```agda
  findP : A.SM → Formula A.SM 0
  findP yM = ∃̇ (∃̇ (∃̇ (embed levelFo ∧̇ (con yM ∈̇ var zero))))
```

補題 `stageP` は、この所属の問い合わせに対する周囲の証人を準備する。順序数 `p`、`p` を含む十分な段階 `γ`、`y` を名づける Skolem 包の要素 `yM`、および `y ∈ Lset p` から始める。さらに三つの所属の仮定が `p`、`Lset p`、`Lset γ` をそれぞれ `Lset lam` に入れるので、三つの存在証人をすべて段階構造で使える。ここで `p` は、一つの外部証人を作るためだけに使われる。`findP` には中央の座標を固定する等式がないため、後で初等性が返す内部の添字は別の `p′` でもかまわない。

```agda
  stageP : (y p γ : S) (op : IsOrd p) (adγ : Adequate γ) (p∈γ : ⟨ p ∈ˢ γ ⟩)
         → (yM : A.SM) → yM .fst ≡ y → ⟨ y ∈ˢ Lset p ⟩
         → ⟨ p ∈ˢ Lset lam ⟩ → ⟨ Lset p ∈ˢ Lset lam ⟩ → ⟨ Lset γ ∈ˢ Lset lam ⟩
         → ⟨ [] HS.ASt.AbsL.⊨ᵐ mapFo A.inL (findP yM) ⟩
  stageP y p γ op adγ p∈γ yM ey y∈Lp p∈ Lp∈ Lγ∈ =
```

同じ周囲の三つ組 `(Lset p,p,Lset γ)` が段階の記述を証明するが、最後の連言支は今度は `yM` の解釈が `Lset p` に属することを記録する。この平行な構成により、二つの問い合わせの数学的な違いが明確になる。`findA` は指定された添字を保ち、`findP` は指定された点の所属を保つ。したがって第二の場合、完全な初等性は別の内部添字を返してもかまわない。

```agda
    ∣ (Lset γ , Lγ∈) , ∣ (p , p∈) , ∣ (Lset p , Lp∈) , (sat , mem) ∣₁ ∣₁ ∣₁
    where
    δ : Vec HS.ASt.SL 3
    δ = (Lset p , Lp∈) ∷ (p , p∈) ∷ (Lset γ , Lγ∈) ∷ []
```

完全性が、二つの問い合わせに共通する核を与える。`γ` の十分さ、`p` の順序数性、および `p ∈ γ` から、三つ組 `(Lset p,p,Lset γ)` が周囲の階層で `levelFo` を満たすことを示す。完全性が何を示し、何を示さないかを区別する必要がある。この外側で準備した特定の三つ組を検証するが、公式を満たすすべての三つ組が `p` を使うとは述べず、後で得る内部の添字を一意にもしない。

```agda
    amb : ⟨ (Lset p ∷ p ∷ Lset γ ∷ []) ⊨ₚ levelFo ⟩
    amb = level-complete γ adγ p op p∈γ
```

前の問い合わせと同じく、この時点での移送は周囲の階層と `Lset lam` 上の段階構造との間だけで行われる。`Cy.atL` の逆向きは、`levelFo` の Δ₀ の証拠を使い、三つの基礎集合での周囲の充足を、それらの段階内の表示での充足として読む。続いて `embed-map` のパスが、定数を持たない核を、周囲の Skolem 包の問い合わせが使う定数域へ移す。これは `stageP` が必要とする第一の連言支である。この有界な一歩では、非有界な量化子を一つも移していない。

```agda
    sat : ⟨ δ HS.ASt.AbsL.⊨ᵐ mapFo A.inL (embed levelFo) ⟩
    sat = subst (λ ψ → ⟨ δ HS.ASt.AbsL.⊨ᵐ ψ ⟩) (sym (embed-map A.inL levelFo))
            (subst ⟨_⟩ (sym (Cy.atL Δ₀-levelFo δ)) amb)
```

残る連言支は、`yM` の解釈が `Lset p` に属することを述べる。その基礎集合は `yM .fst` であり、パス `ey : yM .fst ≡ y` によって、与えられた所属 `y ∈ Lset p` を逆向きにその解釈へ移せる。この小さな書き換えが、添字を固定せずに指定された点を問い合わせへ入れる。後で初等性が三つ組 `(u,p′,z)` を返すとき、保持される結論は `y ∈ u` であり、`p′` と現在の `p` の間の等式はない。

```agda
    mem : ⟨ (A.inL yM) .fst ∈ˢ Lset p ⟩
    mem = subst (λ w → ⟨ w ∈ˢ Lset p ⟩) (sym ey) y∈Lp
```

集合 `d` に対して、`Witness d` は命題的切り詰めのもとで三つの事実を記録する。ある上界 `z` が Skolem 包に属し、指定された段階 `Lset d` が Skolem 包に属し、さらに `(Lset d,d,z)` が周囲の階層で `levelFo` を満たすことである。この型自体は任意の `d` に対して作れるが、以下の構成には `IsOrd d` と `d ∈ M` の両方が必要である。包みを切り詰めたままにしても、後で必要となる命題値の閉性と等式の結論には十分であり、十分な上界を選択済みのデータとして扱うこともない。

```agda
  Witness : S → Type (ℓ-suc ℓ)
  Witness d = ∥ Σ[ z ∶ S ] ( ⟨ z ∈ˢ M ⟩ × ⟨ Lset d ∈ˢ M ⟩
                           × ⟨ (Lset d ∷ d ∷ z ∷ []) ⊨ₚ levelFo ⟩ ) ∥₁
```

構成はまず、Skolem 包の要素 `d` を周囲の段階へ入れる。`Hull⊆L` から `d ∈ Lset lam` が得られる。しかし強化された十分さが受け取るのは、構成可能段階の任意の要素ではなく、順序数 `lam` の要素である。次に示す局所的な事実 `d∈λ` が、まさにこの隔たりを埋める。それが得られると、`sup d d∈λ` は `d` より上の十分な段階を供給するだけである。行き先の `Witness d` 自体が命題なので、外側の `rec₁` はこの命題的に切り詰められた供給を利用できる。

```agda
  witness : (d : S) → IsOrd d → ⟨ d ∈ˢ M ⟩ → Witness d
  witness d od d∈M = rec₁ squash₁ step1 (sup d d∈λ)
    where
    d∈Lλ : ⟨ d ∈ˢ Lset lam ⟩
    d∈Lλ = Hull⊆L d d∈M
```

添字への所属を取り戻すため、`d ∈ Lset lam` に段階の反映補題を適用する。その仮定を見ると、この一歩が成り立つ理由が明確である。モジュールのパラメータにより `lam` は順序数であり、呼び出し側の仮定により `d` も順序数である。この二つの順序数性のもとでのみ、`lam` での段階への `d` の所属から `d ∈ lam` が従う。これは順序数の添字どうしの比較であり、任意の集合に対する一般的な階数原理ではない。

```agda
    d∈λ : ⟨ d ∈ˢ lam ⟩
    d∈λ = ord∈Lset→∈ lam ordλ d od d∈Lλ
```

ここで後続についての閉性により、添字の関係を `stageA` が必要とする第二の段階所属へ変える。`d ∈ lam` から、先の補題 `Lset∈Lλ` は `Lset d ∈ Lset lam` を与える。このとき段階 `Lset d` 全体が、外側の段階の一つの要素として現れる。これと `d∈Lλ` を合わせると、`d` に関係する二つの座標が準備できる。最後の上界 `Lset γ` の所属は、強化された十分さが `γ` を供給した後で別に導く。

```agda
    Ld∈Lλ : ⟨ Lset d ∈ˢ Lset lam ⟩
    Ld∈Lλ = Lset∈Lλ d d∈λ
```

強化された十分さは、命題的切り詰めのもとで、`γ ∈ lam`、`d ∈ γ`、`Adequate γ` を満たす添字 `γ` を返す。そのような三つ組ごとに `step1` は `Witness d` を構成する。まず周囲の段階で問い合わせ全体を立て、初等性によってその切り詰められた存在の答えを Skolem 包の中で得て、その答えを切り詰められた証人の目標へだけ除去する。したがって、除去子の内部では一時的な `γ` を使えるが、`γ` の選択が定理のデータとして外へ出ることはない。

```agda
    step1 : Σ[ γ ∶ S ] (⟨ γ ∈ˢ lam ⟩ × ⟨ d ∈ˢ γ ⟩ × Adequate γ) → Witness d
    step1 (γ , γ∈λ , d∈γ , adγ) =
      rec₁ squash₁ takeZ hullSat
      where
      Lγ∈Lλ : ⟨ Lset γ ∈ˢ Lset lam ⟩
```

与えられた関係 `γ ∈ lam` から、最後の周囲の段階への所属が得られる。`γ` に `Lset∈Lλ` を適用すると `Lset γ ∈ Lset lam` となる。これで `Lset d`、`d`、`Lset γ` はすべて段階構造の正当な要素となり、`stageA` の完全性の証人をそこで述べられる。この `γ` の使用には、最小性も一意性も必要ない。

```agda
      Lγ∈Lλ = Lset∈Lλ γ γ∈λ
```

固定添字の問い合わせが名づける定数は、単なる周囲の集合ではなく、Skolem 包の台の要素でなければならない。`d` と、与えられた `d ∈ M` の証明を組にすると `dM : A.SM` が得られる。その基礎集合は定義により `d` そのものなので、`stageA` に渡す等式の証明は反射律である。この包装は新しい代表を作らず、崩壊も使わない。既存の Skolem 包の要素を、初等性が述べられている言語で提示するだけである。

```agda
      dM : A.SM
      dM = d , d∈M
```

ここで `findA` に完全な初等性を使う。先の `stageA` の呼び出しは、改名された問い合わせが `Lset lam` 上の段階構造で成り立つことを示した。`elem` の対称方向は、その充足を Skolem 包の構造へ移す。`elem` は任意の論理式に適用できるため、この一歩では三つの非有界な存在量化子も一緒に移せる。したがって、Δ₀ の核 `levelFo` にだけ用いた `Cy.atL` とは区別しなければならない。得られる `hullSat` は、適切な三つ組が Skolem 包に存在することだけを述べる。

```agda
      hullSat : ⟨ [] Mse.⊨ findA dM ⟩
      hullSat = subst ⟨_⟩ (sym (elem 0 (findA dM) []))
        (stageA d γ od adγ d∈γ dM refl d∈Lλ Ld∈Lλ Lγ∈Lλ)
```

`findA` の答えを必要な証人へ変えるため、外側の二つの座標 `z` と `d′` が除去子の中ですでに展開されたとする。すると最も内側の存在量化子は、Skolem 包の要素 `a`、`(a,d′,z)` での埋め込まれた核の充足、および等式 `d′ .fst ≡ d` を与える。補助関数 `finishA` は、この切り詰められていない分岐を、`M` 内の上界、指定された `Lset d` の `M` への所属、および `(Lset d,d,fst z)` での周囲の充足へ変換する。この変換が使うのは健全性であり、存在証人の一意性ではない。

```agda
      finishA : (z d' : A.SM)
              → Σ[ a ∶ A.SM ]
                  ( ⟨ (a ∷ d' ∷ z ∷ []) Mse.⊨ embed levelFo ⟩
                  × (d' .fst ≡ d) )
              → Σ[ w ∶ S ] ( ⟨ w ∈ˢ M ⟩ × ⟨ Lset d ∈ˢ M ⟩
```

まず、埋め込まれた核を周囲の階層で読み直す。`levelFo` は Δ₀ なので、有界な比較 `Cy.atM` は Skolem 包の構造における `(a,d′,z)` での充足を、基礎集合 `(a,fst .fst d′,fst z)` での周囲の充足と同一視する。この有界な一歩は、存在証人を展開した後に得られた核だけに作用する。非有界な問い合わせを除去するものでも、それだけで第一の座標を構成可能段階と同一視するものでもない。

```agda
                           × ⟨ (Lset d ∷ d ∷ w ∷ []) ⊨ₚ levelFo ⟩ )
      finishA z d' (a , sat , ed) = z .fst , z .snd , Ld∈M , amb'
        where
        amb : ⟨ (a .fst ∷ d' .fst ∷ z .fst ∷ []) ⊨ₚ levelFo ⟩
        amb = subst ⟨_⟩ (Cy.atM Δ₀-levelFo (a ∷ d' ∷ z ∷ [])) sat
```

`levelFo` の健全性定理は、三つの基礎集合がそれぞれ構成可能であることを要求する。三つとも Skolem 包の要素なので、`Hull⊆L` によりそれぞれ `Lset lam` に属する。さらに `lam` が順序数であるため、`isLλ` がこれら三つの所属を必要な構成可能性の証明へ変える。この別々の仮定と周囲での充足 `amb` を `level-sound` に渡すと、`a .fst` は `Lset (d′ .fst)` と同一視される。公式の充足だけでは、この同一視を正当化できない。

```agda
        ea : a .fst ≡ Lset d
        ea = level-sound (a .fst) (d' .fst) (z .fst)
               (isLλ (a .fst) (Hull⊆L (a .fst) (a .snd)))
               (isLλ (d' .fst) (Hull⊆L (d' .fst) (d' .snd)))
               (isLλ (z .fst) (Hull⊆L (z .fst) (z .snd))) amb
```

ここで `findA` の等式の連言支が、意図された役割を果たす。健全性から `a .fst ≡ Lset (d′ .fst)` が得られ、`ed : d′ .fst ≡ d` に `Lset` を作用させると `Lset (d′ .fst) ≡ Lset d` が得られる。二つのパスを合成すれば `ea : a .fst ≡ Lset d` である。したがって、返された第一の座標は、もともと指定した添字での段階である。この等式の連言支がなければ、同じ健全性の議論から分かるのは、返された何らかの添字での段階だということだけである。

```agda
             ∙ cong Lset ed
```

返された座標 `a` は、Skolem 包への所属 `a .snd` をすでに伴っている。この命題を `ea` に沿って移すと `Lset d ∈ M` が得られる。これが、指定された Skolem 包の順序数 `d` に対して求めていた閉性である。これは、強化された十分さ、完全な初等性、有界絶対性、および段階の記述の健全性から導かれる。`M` に対する別の閉性公理を仮定しておらず、この部分の議論では Mostowski 崩壊もまだ使っていない。

```agda
        Ld∈M : ⟨ Lset d ∈ˢ M ⟩
        Ld∈M = subst (λ w → ⟨ w ∈ˢ M ⟩) ea (a .snd)
```

証人の包みには、向きの整った段階の記述も残す必要がある。`(a,fst .fst d′,fst z)` での周囲の充足から始め、中央の座標を `ed` に沿って移し、第一の座標を `ea` に沿って移す。すると `(Lset d,d,fst z)` での充足が得られ、これはちょうど `Witness d` の第三のフィールドである。これを `z .snd` および新しく得た `Lset d ∈ M` と合わせると、切り詰められていない一つの分岐ができ、後で命題的切り詰めの中へ戻される。

```agda
        amb' : ⟨ (Lset d ∷ d ∷ z .fst ∷ []) ⊨ₚ levelFo ⟩
        amb' = subst (λ v → ⟨ (v ∷ d ∷ z .fst ∷ []) ⊨ₚ levelFo ⟩) ea
          (subst (λ p → ⟨ (a .fst ∷ p ∷ z .fst ∷ []) ⊨ₚ levelFo ⟩) ed amb)
```

`z` と `d′` を固定すると、最も内側の存在量化子が保つのは、適切な `a` が単に存在することだけである。明示的な各 `a` から `finishA` によって `d` に対する必要な切り詰められた証人が得られるので、切り詰めの内部で写すことで必要な存在性だけを保てる。選ばれた `a` が外へ現れることはなく、残る座標も同じ命題的な制限のもとで扱われる。

```agda
      takeD : (z : A.SM)
            → Σ[ d' ∶ A.SM ]
                ⟨ (d' ∷ z ∷ []) Mse.⊨ ∃̇ (embed levelFo ∧̇ (var (suc zero) ≐ con dM)) ⟩
            → Witness d
      takeD z (d' , hd) = map₁ (finishA z d') hd
```

最も外側の証人 `z` がすでに固定された後、次の切り詰めが隠しているのは中央の座標 `d′` である。これを命題 `Witness d` へ除去し、局所的な各 `d′` を先の構成へ渡す。`step1` ですでに用いた外側の除去が、証人 `z` を処理する。したがって、強化された十分さと三つの存在量化子から得られる証人は、すべて命題である結論の内部にとどまる。十分な上界も包内の三つ組も、大域的なデータとして選ばれない。

```agda
      takeZ : Σ[ z ∶ A.SM ]
                ⟨ (z ∷ []) Mse.⊨ ∃̇ (∃̇ (embed levelFo ∧̇ (var (suc zero) ≐ con dM))) ⟩
            → Witness d
      takeZ (z , hz) = rec₁ squash₁ (takeD z) hz
```

ここで、崩壊と構成可能段階の局所的な整合性を述べられる。`d` が Skolem 包の順序数なら、`commute` は `Lset d` が再び包に属することと、この段階を崩壊すると `Lset (π d)` が得られることを同時に証明する。証明は `Witness d` を命題の積へ除去する。包への所属は命題を値にとり、周囲の二つの集合の等しさも、周囲の累積階層が h-集合であるため命題である。したがって、その積は命題的切り詰めを除去できる正当な目標である。

```agda
  commute : (d : S) → IsOrd d → (d∈M : ⟨ d ∈ˢ M ⟩)
          → ⟨ Lset d ∈ˢ M ⟩ × (π (Lset d) ≡ Lset (π d))
  commute d od d∈M =
    rec₁ (isProp× ((Lset d ∈ˢ M) .snd) (isSetS (π (Lset d)) (Lset (π d))))
           go (witness d od d∈M)
```

証人を局所的に開くと、`Lset d` が包に属するという成分が、最初の結論をそのまま与える。残る二つのデータ、包の要素 `z` と `levelFo(Lset d,d,z)` の充足は、等式の証明に使うために残す。この分担は `commute` の二つの結論に対応している。`d` が添字づける段階について Skolem 包が閉じていることは `Witness d` から直接得られるが、その段階と崩壊との整合性は、段階の有界な記述からさらに証明する必要がある。

```agda
    where
    go : Σ[ z ∶ S ] ( ⟨ z ∈ˢ M ⟩ × ⟨ Lset d ∈ˢ M ⟩
                    × ⟨ (Lset d ∷ d ∷ z ∷ []) ⊨ₚ levelFo ⟩ )
       → ⟨ Lset d ∈ˢ M ⟩ × (π (Lset d) ≡ Lset (π d))
    go (z , z∈M , Ld∈M , amb) = Ld∈M , eq
```

等式の証明では、まず有界な記述を崩壊の向こうへ移す。環境は、Skolem 包の三つの要素 `Lset d`、`d`、`z` と、それぞれの所属の証明からなる。`levelFo` は定数を含まない Δ₀ 論理式なので、`Cy.push` は各座標をその崩壊値で置き換え、`levelFo(π (Lset d),π d,π z)` の充足を与える。これは先に順序数性へ使ったのと同じ局所的な Δ₀ 移送を、今度は構成可能段階を記述する三変数の論理式へ適用したものである。

```agda
      where
      pushed : ⟨ (π (Lset d) ∷ π d ∷ π z ∷ []) ⊨ₚ levelFo ⟩
      pushed = Cy.push Δ₀-levelFo ((Lset d , Ld∈M) ∷ (d , d∈M) ∷ (z , z∈M) ∷ []) amb
```

移送された論理式を健全性によって読むには、崩壊された三つの座標がすべて構成可能でなければならない。各座標は Skolem 包の要素の崩壊なので、`πX-intro` によって崩壊像に属し、点ごとの仮定 `pixL` が必要な構成可能性の証明を与える。これにより健全性は、崩壊された第一座標を、第二座標が添字づける構成可能段階と同一視できる。

`π (Lset d) ≡ Lset (π d)`。

補助的な値 `π z` はこの記述を検証するために必要であるが、得られる等式には現れない。

```agda
      eq : π (Lset d) ≡ Lset (π d)
      eq = level-sound (π (Lset d)) (π d) (π z)
             (pixL (π (Lset d)) (HS.C.πX-intro (Lset d) Ld∈M))
             (pixL (π d) (HS.C.πX-intro d d∈M))
             (pixL (π z) (HS.C.πX-intro z z∈M))
```

移送された充足は、以上の健全性の議論における最後の前提である。その結論は `commute` の仮定とともに読む必要がある。この等式が成り立つのは、Skolem 包に属する順序数 `d` についてである。これは演算 `π` と `Lset` の間の大域的な等式ではない。この局所性で十分なのは、以下の二つの適用では、まず関係する包内の順序数を取り戻し、その後で整合性の等式を使うからである。

```agda
             pushed
```

抽象的な凝縮の議論が要求する第一の性質は、崩壊像が自身の順序数に対応する段階について閉じていることである。崩壊像の順序数 `δ` が与えられたとき、`levelIn` は `Lset δ` もその像に属することを示さなければならない。要素の特徴づけ `πX-member` は、命題的切り詰めのもとで、`π d ≡ δ` を満たす Skolem 包の要素 `d` を与える。目標そのものが所属命題 `Lset δ ∈ πX` なので、この命題的に切り詰められた原像を局所的に開ける。

```agda
  levelIn : (δ : S) → IsOrd δ → ⟨ δ ∈ˢ HS.C.πX ⟩ → ⟨ Lset δ ∈ˢ HS.C.πX ⟩
  levelIn δ oδ δ∈πX =
    rec₁ ((Lset δ ∈ˢ HS.C.πX) .snd) go (HS.C.πX-member δ δ∈πX)
    where
    go : Σ[ d ∶ S ] (⟨ d ∈ˢ M ⟩ × (π d ≡ δ)) → ⟨ Lset δ ∈ˢ HS.C.πX ⟩
```

このような原像 `d` が得られれば、求める像への所属は `Lset d` から導ける。実際、`Lset d` が Skolem 包に属するという証明を `πX-intro` に渡すと、`π (Lset d)` が崩壊像に属するという証明が得られる。最後の輸送では、整合性の等式 `π (Lset d) ≡ Lset (π d)` に続いて、原像の等式 `π d ≡ δ` に `Lset` を施した等式を使う。残る課題は、`d` が順序数であり、`Lset d` が包に属することを示すことである。

```agda
    go (d , d∈M , e) =
      subst (λ w → ⟨ w ∈ˢ HS.C.πX ⟩) (cm .snd ∙ cong Lset e)
            (HS.C.πX-intro (Lset d) (cm .fst))
      where
      od : IsOrd d
```

整合性の補題を使う前に、原像の順序数性を復元する。仮定 `IsOrd δ` を `π d ≡ δ` に沿って逆向きに輸送すると `IsOrd (π d)` が得られ、`ord-pull` がこの事実を崩壊の手前へ反映して `IsOrd d` を与える。議論の順序に注意してほしい。原像の記述だけから分かるのは、`d` が Skolem 包の要素だということである。その順序数性は、`δ` の順序数性と、有界な順序数論理式に対する反映から得られる。

```agda
      od = ord-pull d d∈M (subst IsOrd (sym e) oδ)
```

これで `commute` の仮定がすべて揃った。その第一成分は `Lset d` を Skolem 包に入れ、第二成分は `π (Lset d) ≡ Lset (π d)` を与える。後者を、`e : π d ≡ δ` に `Lset` を施した `cong Lset e` と合成すると、この崩壊された段階は `Lset δ` と同一視され、輸送によって求める像への所属が得られる。したがって、崩壊像が順序数 `δ` を含むなら `Lset δ` も含む。順序数でない集合や像の外の順序数について、閉性を主張しているわけではない。

```agda
      cm : ⟨ Lset d ∈ˢ M ⟩ × (π (Lset d) ≡ Lset (π d))
      cm = commute d od d∈M
```

第二の性質は被覆である。Skolem 包の各要素 `y` に対して、`π y ∈ Lset γ` を満たす順序数 `γ` が崩壊像の中に単に存在することを求める。その順序数、像への所属、そしてこの段階への所属は、一つの命題的切り詰めのもとに保たれる。したがって各 `y` には被覆する段階が存在するが、そのような段階の族を選ぶことも、添字の最小性や `lam` との大小関係を主張することもない。

```agda
  cover : (y : S) → ⟨ y ∈ˢ M ⟩
        → ∥ Σ[ γ ∶ S ] (IsOrd γ × ⟨ γ ∈ˢ HS.C.πX ⟩ × ⟨ π y ∈ˢ Lset γ ⟩) ∥₁
  cover y y∈M = rec₁ squash₁ go (Lset-out lam y (Hull⊆L y y∈M))
    where
    Goal : Type (ℓ-suc ℓ)
```

目標 `Goal` 自体が命題的切り詰めである。この点は二度使われる。`Lset-out` が与える `y` の分解と、強化された十分さが与える十分な添字は、共通の行き先が命題なので、ともに局所的に利用できる。どちらの段階でも最終的な被覆の添字は固定されない。その添字は、所属の問い合わせ `findP` に対する内部の答えから得られる。

```agda
    Goal = ∥ Σ[ γ ∶ S ] (IsOrd γ × ⟨ γ ∈ˢ HS.C.πX ⟩ × ⟨ π y ∈ˢ Lset γ ⟩) ∥₁
```

構成は、まず構成可能階層の中で `y` の位置を定めることから始まる。Skolem 包の各要素は `Lset lam` に属するので、`Lset-out` は命題的切り詰めのもとで、`y` が `Lset c` の定義可能部分集合となる添字 `c ∈ lam` を与える。`p = sucV c` と置く。後続に関する閉性によって `p` を `lam` に戻すと、強化された十分さは、`p` を含む十分な添字 `γ ∈ lam` を、やはり切り詰めのもとで与える。準備した添字 `p` は `y` を含む外側の段階を用意するが、Skolem 包が後で返す添字そのものではない。

```agda
    go : Σ[ c ∶ S ] (⟨ c ∈ˢ lam ⟩ × ⟨ y ∈ˢ 𝒟ₒ (Lset c) ⟩) → Goal
    go (c , c∈λ , y∈D) = rec₁ squash₁ go₂ (sup p p∈λ)
      where
      p : S
      p = sucV c
```

最初の補助事実は、`lam` の後続に関する閉性の仮定を `c ∈ lam` に適用し、`p = sucV c` に対する `p ∈ lam` を得る。この関係には二つの用途がある。一方では `p` に強化された十分さを適用し、他方では、後で作る周囲の証人において、順序数 `p` と段階 `Lset p` の両方を `Lset lam` の中へ置く。添字に関するこの一つの閉性の仮定が、これらすべてを支えている。

```agda
      p∈λ : ⟨ p ∈ˢ lam ⟩
      p∈λ = succλ c c∈λ
```

準備した添字は順序数でもなければならない。`lam` は順序数で `c ∈ lam` なので、`mem-ord` から `IsOrd c` が得られ、フォン・ノイマン後続についての順序数の閉性から `IsOrd (sucV c)`、すなわち `IsOrd p` が従う。ここでは後続の二つの役割を区別している。`succλ` は後続を外側の添字に入れ、`suc-ord` はその後続自体が順序数であることを示す。

```agda
      op : IsOrd p
      op = suc-ord (mem-ord {A = lam} ordλ c c∈λ)
```

誕生段階の情報は `y ∈ 𝒟ₒ (Lset c)` を与える。後続段階の等式は、この定義可能冪集合の段階を `Lset (sucV c)` と同一視するので、輸送によって `y ∈ Lset p` が得られる。これが `c` からその後続へ進む理由である。分解によって `y` は `c` の段階上の定義可能部分集合として位置づけられるが、`findP` が必要とするのは構成可能段階への通常の所属である。

```agda
      y∈Lp : ⟨ y ∈ˢ Lset p ⟩
      y∈Lp = subst (λ w → ⟨ y ∈ˢ w ⟩) (sym (Lset-suc c)) y∈D
```

強化された十分さの証人を局所的に開くと、添字 `γ ∈ lam`、関係 `p ∈ γ`、性質 `Adequate γ` が得られる。これらは、外側で準備した添字 `p` に完全性を適用するために必要な仮定そのものである。組 `yM = (y,y∈M)` はここで `y` を包の台の要素とみなし、`findP` の定数パラメータとして使えるようにする。ここからの構成では、先のように指定された添字を固定する問い合わせではなく、`y` の所属を固定する問い合わせを使う。

```agda
      go₂ : Σ[ γ ∶ S ] (⟨ γ ∈ˢ lam ⟩ × ⟨ p ∈ˢ γ ⟩ × Adequate γ) → Goal
      go₂ (γ , γ∈λ , p∈γ , adγ) = rec₁ squash₁ takeZ hullSat
        where
        yM : A.SM
        yM = y , y∈M
```

十分な添字 `γ` における完全性は、三つ組 `(Lset p,p,Lset γ)` を使って `findP` の周囲での答えを作り、先に得た所属が `y` をその第一座標に入れる。必要な三つの台への所属は、`ord∈Lλ p`、`Lset∈Lλ p`、`Lset∈Lλ γ` がそれぞれ与える。`findP` は非有界な存在量化を含むので、この答え全体を Skolem 包へ移すには完全な初等性を使う。その結果、`yM` が正しく記述されたある段階に属するという、包内部の存在主張が得られる。

```agda
        hullSat : ⟨ [] Mse.⊨ findP yM ⟩
        hullSat = subst ⟨_⟩ (sym (elem 0 (findP yM) []))
          (stageP y p γ op adγ p∈γ yM refl y∈Lp
            (ord∈Lλ p op p∈λ) (Lset∈Lλ p p∈λ) (Lset∈Lλ γ γ∈λ))
```

内部の主張を局所的に開くと、Skolem 包の三つの要素 `u`、`a`、`z` が得られる。それらの基礎集合は `levelFo(u,fst .fst a,fst z)` を満たし、同じ答えは `y ∈ u .fst` も記録している。ここから、崩壊像に属し、その段階が `π y` を含む順序数を得なければならない。局所的な各答えから明示的な依存和を作れるが、その和はただちに命題的切り詰めのもとへ戻されるので、被覆の添字が選択済みのデータとして外へ出ることはない。

```agda
        finishP : (z a : A.SM)
                → Σ[ u ∶ A.SM ]
                    ( ⟨ (u ∷ a ∷ z ∷ []) Mse.⊨ embed levelFo ⟩
                    × ⟨ y ∈ˢ u .fst ⟩ )
                → Σ[ β ∶ S ] (IsOrd β × ⟨ β ∈ˢ HS.C.πX ⟩
```

出力の証人は、局所的に `β = π p′` とする。ここで `p′` は、包の中央の座標 `a` の基礎にある集合である。`p′` が順序数だと分かれば、`ord-push` により `π p′` も順序数となり、`a` が持つ `p′ ∈ M` の証明から、`πX-intro` によって `π p′` が崩壊像に入る。残る成分は `π y ∈ Lset (π p′)` である。これを得るには、まず論理式への答えを周囲の階層で読み、その後で所属を局所的な整合性の等式と結びつける。

```agda
                              × ⟨ π y ∈ˢ Lset β ⟩)
        finishP z a (u , sat , y∈u) =
          π p′ , ord-push p′ (a .snd) op′ , HS.C.πX-intro p′ (a .snd) , πy∈
          where
          amb : ⟨ (u .fst ∷ a .fst ∷ z .fst ∷ []) ⊨ₚ levelFo ⟩
```

内部の充足の証明が扱うのは、包の構造における `embed levelFo` である。その核 `levelFo` は Δ₀ 論理式なので、`Cy.atM` はこの証明を、同じ三つの基礎集合 `(u,fst .fst a,fst z)` における `levelFo` の周囲での充足として読む。この段階では、どの座標も崩壊されない。その役割は、Skolem 包の内部意味論を離れ、`isOrd-at-p-out` と `level-sound` を適用できる周囲での主張を取り戻すことである。

```agda
          amb = subst ⟨_⟩ (Cy.atM Δ₀-levelFo (u ∷ a ∷ z ∷ [])) sat
```

Skolem 包の内部で返された中央の座標を `p′ = a .fst` とする。これは、周囲で準備した後続 `p = sucV c` と等しい必要がない。周囲の三つ組は `findP yM` が充足可能であることを示したが、`findP` が固定するのは `yM` の第一座標への所属だけであり、中央の座標を固定する等式は含まない。したがって完全な初等性が命題的切り詰めのもとで与えるのは、ある内部添字 `p′` にすぎず、残りの証明はこの返された添字を使う。

```agda
          p′ : S
          p′ = a .fst
```

ただし、返された添字が順序数であることは分かる。周囲での充足 `amb` の第一の連言支は、中央の座標について読む三つの枠を持つ順序数の記述である。その連言支に読みの補題 `isOrd-at-p-out` を適用すると、`IsOrd p′` が得られる。この結論が述べるのは内部の原像の添字 `p′` である。`Goal` で使う順序数はその崩壊 `π p′` であり、こちらの順序数性は別に `ord-push` から得る。

```agda
          op′ : IsOrd p′
          op′ = isOrd-at-p-out (u .fst) p′ (z .fst) (amb .fst)
```

ここで健全性により、内部の答えの第一座標を特定する。`u`、`a`、`z` はいずれも Skolem 包の要素なので、`Hull⊆L` はそれらの基礎にある集合を `Lset lam` に入れ、`isLλ` がそれぞれの構成可能性を証明する。これら三つの前提を `amb` と合わせると、`u .fst ≡ Lset p′` が得られる。したがって、答えに記録された `y ∈ u .fst` を `y ∈ Lset p′` へ輸送できる。補助的な上界 `z .fst` は一意である必要がなく、`p′` と準備した `p` の間の等式も使わない。健全性は、返された順序数の添字だけから段階の値を定める。

```agda
          u≡ : u .fst ≡ Lset p′
          u≡ = level-sound (u .fst) p′ (z .fst)
                 (isLλ (u .fst) (Hull⊆L (u .fst) (u .snd)))
                 (isLλ p′ (Hull⊆L p′ (a .snd)))
                 (isLλ (z .fst) (Hull⊆L (z .fst) (z .snd))) amb
```

健全性から得た等式 `u≡` は、返された段階の値 `u .fst` を `Lset p′` と同一視する。この等式に沿って、すでに得られた所属 `y∈u` を移せば、`y ∈ Lset p′` が従う。ここで行うのは所属の右辺にある集合の置換だけであり、返された添字 `p′` と先に用意した添字 `p` の間には何の関係も課していない。

```agda
          y∈Lp′ : ⟨ y ∈ˢ Lset p′ ⟩
          y∈Lp′ = subst (λ v → ⟨ y ∈ˢ v ⟩) u≡ y∈u
```

返された中央の座標は、局所的な交換定理に必要なデータをちょうど与える。その基礎集合が `p′` であり、`op′` はそれが順序数であることを、`a .snd` はそれが包に属することを示す。したがって `commute p′ op′ (a .snd)` から、`Lset p′ ∈ M` と等式 `π (Lset p′) ≡ Lset (π p′)` の両方が得られる。この定理は包の中の順序数に対する局所的な主張であり、ここではその条件が満たされている。

```agda
          cm : ⟨ Lset p′ ∈ˢ M ⟩ × (π (Lset p′) ≡ Lset (π p′))
          cm = commute p′ op′ (a .snd)
```

`y∈Lp′` の両端は包の要素である。`y` については `y∈M` が、`Lset p′` については `cm .fst` がその所属を与える。そこで `member-push` によりこの所属を崩壊の後へ移し、`π y ∈ π (Lset p′)` を得る。さらに `cm .snd` に沿って右辺の集合を置換すると、`π y ∈ Lset (π p′)` となる。先に示した `π p′` の順序数性と像への所属と合わせれば、これは `finishP` が求める覆いの証人である。

```agda
          πy∈ : ⟨ π y ∈ˢ Lset (π p′) ⟩
          πy∈ = subst (λ w → ⟨ π y ∈ˢ w ⟩) (cm .snd)
                  (Cy.member-push (Lset p′) y (cm .fst) y∈M y∈Lp′)
```

`z` と `a` を固定すると、最後の存在量化子は適切な `u` が単に存在することだけを述べる。明示的な各答えから、上で構成した順序数 `π p′`、その崩壊像への所属、および `π y ∈ Lset (π p′)` の証明が定まる。この構成を命題的切り詰めの内部で写すことにより、問い合わせへの特定の答えを選ぶことなく、被覆する順序数の存在を保てる。

```agda
        takeA : (z : A.SM)
              → Σ[ a ∶ A.SM ]
                  ⟨ (a ∷ z ∷ []) Mse.⊨ ∃̇ (embed levelFo ∧̇ (con yM ∈̇ var zero)) ⟩
              → Goal
        takeA z (a , ha) = map₁ (finishP z a) ha
```

残る二つの存在の層も同じ制限に従う。`z` を固定した後、行き先 `Goal` が命題なので中央の証人 `a` を使える。外側の除去も同様に `z` を扱う。したがって内部の答えの三つの座標は、すべて局所的にだけ利用できる。結果は各 Skolem 包の要素に被覆する順序数が存在することを示すが、そのような順序数を選ぶ関数は作らない。

```agda
        takeZ : Σ[ z ∶ A.SM ]
                  ⟨ (z ∷ []) Mse.⊨ ∃̇ (∃̇ (embed levelFo ∧̇ (con yM ∈̇ var zero))) ⟩
              → Goal
        takeZ (z , hz) = rec₁ squash₁ (takeA z) hz
```

ここまでで示した二つの性質が、崩壊像を決定する。その順序数要素全体の集合を `β` とする。像の推移性と、順序数の要素も順序数であることから、`β` は順序数である。`x ∈ πX` なら、被覆によって、順序数 `γ ∈ πX` を添字とするある `Lset γ` に `x` が属する。したがって `γ ∈ β` であり、単調性から `x ∈ Lset β` が従う。逆に `x ∈ Lset β` をある `δ ∈ β` のところで分解する。像の要素 `δ` に被覆を適用すると、`δ ∈ γ` を満たす順序数 `γ ∈ β` が得られる。すると `x ∈ Lset γ` であり、`levelIn` は `Lset γ` を推移的な崩壊像に入れるので、`x ∈ πX` である。外延性から `πX ≡ Lset β` が得られる。

```agda
  module Cn = HS.Condense levelIn cover using (condenses)
```

こうして、`IsOrd β` と `HS.C.πX ≡ Lset β` を満たす明示的な集合 `β` が得られる。この証人は命題的切り詰めの中にはない。崩壊像の順序数要素全体からなる集合そのものだからである。この結論は `Condense` の構造的な仮定をすべて使い、その古典的なパラメータは `LEM (ℓ-suc ℓ)` だけである。`β` と外側の添字 `lam` の比較、基数評価、単射は与えない。それらには後の章で導入する追加の構成が必要である。

```agda
  condenses : Σ[ β ∶ S ] (IsOrd β × (HS.C.πX ≡ Lset β))
  condenses = Cn.condenses
```

</div>
</details>