---
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: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 凝縮を通して構造を移す

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

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

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

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

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

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

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

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ∃̇_ )
open import FOL.Manipulation.ConstantMapping using ( mapFo; embed )
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

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

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

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

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

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

```agda
open import Cubical.Data.Vec using ( _∷_; [] )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Foundations.HLevels using ( isProp× )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

`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 hPropStructure 𝒮ᵥ
```

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

```agda
module SemVᵃ = FOL.Semantics 𝒮ᵥ
open SemVᵃ using ( _^_ )
```

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

論理式 `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 包の構成に必要な既定の要素を与えます。この最初の仮定群の最後は完全な初等性です。パラメータが包から取られるなら、非有界量化子を含む論理式も含め、すべての論理式は包と周囲の段階で同じ真理値をもちます。

```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 ∅∈λ)
```

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

```agda
  (sup : Superadequate lam)
  (pixL : (x : S) → ⟨ x ∈ˢ HullStage.C.πX lam ordλ succλ X X⊆L ∅∈λ ⟩
        → ⟨ isL x ⟩)
  where
```

ここからは三つの構造を同時に使います。`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) → fst dM ≡ 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
    δ : 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) → fst yM ≡ 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
    δ : 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` に属することを述べます。その基礎集合は `fst yM` であり、パス `ey : fst yM ≡ y` によって、与えられた所属 `y ∈ Lset p` を逆向きにその解釈へ移せます。この小さな書き換えが、添字を固定せずに指定された点を問い合わせへ入れます。後で初等性が三つ組 `(u,p′,z)` を返すとき、保持される結論は `y ∈ u` であり、`p′` と現在の `p` の間の等式はありません。

```agda
    mem : ⟨ fst (A.inL yM) ∈ˢ 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` 自体が命題なので、外側の `PT.rec` はこの命題的に切り詰められた供給を利用できます。

```agda
  witness : (d : S) → IsOrd d → ⟨ d ∈ˢ M ⟩ → Witness d
  witness d od d∈M = PT.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γ) =
      PT.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)` での埋め込まれた核の充足、および等式 `fst d′ ≡ 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 ⟩
                  × (fst d' ≡ d) )
              → Σ[ w ∈ S ] ( ⟨ w ∈ˢ M ⟩ × ⟨ Lset d ∈ˢ M ⟩
```

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

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

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

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

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

```agda
             ∙ cong Lset ed
```

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

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

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

```agda
        amb' : ⟨ (Lset d ∷ d ∷ fst z ∷ []) ⊨ₚ levelFo ⟩
        amb' = subst (λ v → ⟨ (v ∷ d ∷ fst z ∷ []) ⊨ₚ levelFo ⟩) ea
          (subst (λ p → ⟨ (fst a ∷ p ∷ fst z ∷ []) ⊨ₚ 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) = PT.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) = PT.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 =
    PT.rec (isProp× (snd (Lset d ∈ˢ M)) (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 =
    PT.rec (snd (Lset δ ∈ˢ HS.C.πX)) 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 = PT.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) = PT.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γ) = PT.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(fst u,fst a,fst z)` を満たし、同じ答えは `y ∈ fst u` も記録しています。ここから、崩壊像に属し、その段階が `π y` を含む順序数を得なければなりません。局所的な各答えから明示的な依存和を作れますが、その和はただちに命題的切り詰めのもとへ戻されるので、被覆の添字が選択済みのデータとして外へ出ることはありません。

```agda
        finishP : (z a : A.SM)
                → Σ[ u ∈ A.SM ]
                    ( ⟨ (u ∷ a ∷ z ∷ []) Mse.⊨ embed levelFo ⟩
                    × ⟨ y ∈ˢ fst u ⟩ )
                → Σ[ β ∈ 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′ (snd a) op′ , HS.C.πX-intro p′ (snd a) , πy∈
          where
          amb : ⟨ (fst u ∷ fst a ∷ fst z ∷ []) ⊨ₚ levelFo ⟩
```

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

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

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

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

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

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

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

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

健全性から得た等式 `u≡` は、返された段階の値 `fst u` を `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′` はそれが順序数であることを、`snd a` はそれが包に属することを示します。したがって `commute p′ op′ (snd a)` から、`Lset p′ ∈ M` と等式 `π (Lset p′) ≡ Lset (π p′)` の両方が得られます。この定理は包の中の順序数に対する局所的な主張であり、ここではその条件が満たされています。

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

`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) = PT.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) = PT.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
```