凝縮を通して構造を移す

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

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

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

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λ を通して、包から返された各証人を構成可能な集合にする。これは包が段階に各点で含まれるという主張であり、包そのものが段階の要素であるという主張ではない。

open HS.H using ( Hull⊆L )

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

M : S
M = HS.M

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

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

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

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 は集合の間の所属であり、一つの段階が別の段階に各点で含まれるという意味ではない。

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 と混同してはならない。

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 包の初等的な包含と崩壊同型に基づく。

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 のもとでの局所的な同値であり、任意の周囲の集合に対する π の振る舞いを述べるものではない。

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 と等しい必要がない。

findA : A.SM → Formula A.SM 
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 によって順に証明される。ここでは γ が最小であるとは主張しない。

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 と同一視する逆向きのパスだからである。各存在証人は命題的切り詰めのもとに置かれ、この三つ組を正準的に選ぶことなく、その存在だけを保つ。

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

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

  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 が必要とする埋め込まれた核をちょうど与える。完全な初等性を使うのは、非有界な問い合わせ全体を組み立てた後である。

  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 を含む正しく記述された構成可能段階であり、その添字は固定されない。被覆の議論に必要なのは、まさにこの条件である。

findP : A.SM → Formula A.SM 
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′ でもかまわない。

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 は指定された点の所属を保つ。したがって第二の場合、完全な初等性は別の内部添字を返してもかまわない。

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

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

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

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

  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 の間の等式はない。

  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 の両方が必要である。包みを切り詰めたままにしても、後で必要となる命題値の閉性と等式の結論には十分であり、十分な上界を選択済みのデータとして扱うこともない。

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₁ はこの命題的に切り詰められた供給を利用できる。

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 が従う。これは順序数の添字どうしの比較であり、任意の集合に対する一般的な階数原理ではない。

  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 γ の所属は、強化された十分さが γ を供給した後で別に導く。

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

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

  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 の完全性の証人をそこで述べられる。この γ の使用には、最小性も一意性も必要ない。

    Lγ∈Lλ = Lset∈Lλ γ γ∈λ

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

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

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

    hullSat : ⟨ [] Mse.⊨ findA dM ⟩
    hullSat = subst ⟨_⟩ (sym (elem  (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) での周囲の充足へ変換する。この変換が使うのは健全性であり、存在証人の一意性ではない。

    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) での周囲の充足と同一視する。この有界な一歩は、存在証人を展開した後に得られた核だけに作用する。非有界な問い合わせを除去するものでも、それだけで第一の座標を構成可能段階と同一視するものでもない。

                         × ⟨ (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) と同一視される。公式の充足だけでは、この同一視を正当化できない。

      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 である。したがって、返された第一の座標は、もともと指定した添字での段階である。この等式の連言支がなければ、同じ健全性の議論から分かるのは、返された何らかの添字での段階だということだけである。

           ∙ cong Lset ed

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

      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 と合わせると、切り詰められていない一つの分岐ができ、後で命題的切り詰めの中へ戻される。

      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 が外へ現れることはなく、残る座標も同じ命題的な制限のもとで扱われる。

    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 を処理する。したがって、強化された十分さと三つの存在量化子から得られる証人は、すべて命題である結論の内部にとどまる。十分な上界も包内の三つ組も、大域的なデータとして選ばれない。

    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-集合であるため命題である。したがって、その積は命題的切り詰めを除去できる正当な目標である。

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 から直接得られるが、その段階と崩壊との整合性は、段階の有界な記述からさらに証明する必要がある。

  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) の充足を与える。これは先に順序数性へ使ったのと同じ局所的な Δ₀ 移送を、今度は構成可能段階を記述する三変数の論理式へ適用したものである。

    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 はこの記述を検証するために必要であるが、得られる等式には現れない。

    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 の間の大域的な等式ではない。この局所性で十分なのは、以下の二つの適用では、まず関係する包内の順序数を取り戻し、その後で整合性の等式を使うからである。

           pushed

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

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 が包に属することを示すことである。

  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 包の要素だということである。その順序数性は、δ の順序数性と、有界な順序数論理式に対する反映から得られる。

    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 δ も含む。順序数でない集合や像の外の順序数について、閉性を主張しているわけではない。

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

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

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 に対する内部の答えから得られる。

  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 包が後で返す添字そのものではない。

  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 の中へ置く。添字に関するこの一つの閉性の仮定が、これらすべてを支えている。

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

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

    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 が必要とするのは構成可能段階への通常の所属である。

    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 の所属を固定する問い合わせを使う。

    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 が正しく記述されたある段階に属するという、包内部の存在主張が得られる。

      hullSat : ⟨ [] Mse.⊨ findP yM ⟩
      hullSat = subst ⟨_⟩ (sym (elem  (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 を含む順序数を得なければならない。局所的な各答えから明示的な依存和を作れるが、その和はただちに命題的切り詰めのもとへ戻されるので、被覆の添字が選択済みのデータとして外へ出ることはない。

      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′) である。これを得るには、まず論理式への答えを周囲の階層で読み、その後で所属を局所的な整合性の等式と結びつける。

                            × ⟨ π 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 を適用できる周囲での主張を取り戻すことである。

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

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

        p′ : S
        p′ = a .fst

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

        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 の間の等式も使わない。健全性は、返された順序数の添字だけから段階の値を定める。

        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 の間には何の関係も課していない。

        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′) の両方が得られる。この定理は包の中の順序数に対する局所的な主張であり、ここではその条件が満たされている。

        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 が求める覆いの証人である。

        π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′) の証明が定まる。この構成を命題的切り詰めの内部で写すことにより、問い合わせへの特定の答えを選ぶことなく、被覆する順序数の存在を保てる。

      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 包の要素に被覆する順序数が存在することを示すが、そのような順序数を選ぶ関数は作らない。

      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 β が得られる。

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

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

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