包とその崩壊を L の内部に置く

凝縮の議論には、外の包だけでは足りません。包そのものと、崩壊の各値が L に属する必要があります。本章は、崩壊を符号化し、包を ω 反復として表すことで、これらの所属の事実を証明します。

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

本章は古典論理のもとで進みます。モデル自身のレベルの後続での排中律の実例を使います。これは選択の構成が帯びるのと同じ仮定であり、ここで仮定される古典的な事実はこれだけです。

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

モジュールはこの仮定をパラメータとします。したがって以下の主張はすべてそれに相対的であり、漠然とした排中律の原理に訴えるものではありません。

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

本章は集合論の一階言語で語ります。論理式は構成可能な構造の台の上で組み立てられ、その定数は L の要素を名指します。定数は任意の対応に沿って改名でき、充足は改名で変わります。これが、崩壊と包を記述するための語彙です。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ∃̇_; ∀̇_; ∀̇∈; ⊥̇ )
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp )
open import FOL.Manipulation.Relabelling using ( ⊨-map )

論理式の読みは、改名によって環境の間を移動します。改名は充足にとって無害です。周囲の階層は、所属に沿う帰納、集合の外延性、そして「要素＝添字とその所属の証明」という提示の仕方という、背景の事実を供給します。

open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV )
open import V.Presentation {ℓ} using ( member; fiber )

議論は、L のすべての集合の住む場所からはじまります。順序数で添字づけられた段階の塔です。集合の崩壊はその要素だけから計算され、構成可能性は所属に沿って伝わります。示すべきは、この局所的な計算が L の外に出ないことです。包は推移的ではないので、議論は崩壊についての大域的な事実を使えず、段階ごとに、値が内側にとどまることを改めて導きます。

open import V.Coding {ℓ} using ( pr; module VCode )
open import V.Collapse {ℓ} using ( module Collapse )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-out; Lset→isL; 𝒟ₒ; 𝒟ₒ∋⊆
        ; Lset-layer; layer-trans )

構成可能集合 ωʟ は周囲の ω を表し、その仕様は要素を内部の数項と同定します。後では分出によって有界な切片と一段階の閉包を切り出します。どちらの演算も、結果が再び L の要素です。それが、構成全体を、その記述対象の宇宙の内側に保つのです。

open import L.Ordinal {ℓ} using ( mem-ord; #∈ω )
open import L.Axioms.Basic {ℓ} using ( LsetS; ∅ʟ; extensionalL )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ; ω-specL )
open import L.Axioms.Numerals {ℓ} using ( numeralL-fst )

置換が値を表へ集めます。グラフが定義可能な再帰は L の要素となり、各入力で一意な値が「単に存在する」だけで十分です。定義可能性が論理式の定数を解釈し、モデル側の対と数項の符号化が、項目とその名前を供給します。

open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct )
open import L.Recursion.Graph {ℓ} lem using () renaming ( module Graph to RecursionGraph )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; envOverAt; envOverAt-transport )
open import L.Coding.Expressions {ℓ} using ( numL; sucAtL; sucAtL-adequate; consAtL; consAtL-adequate )

環境はパラメータのベクトルを一つの集合として符号化し、ベクトルはそこから復元されます。充足の橋は内部の充足を外側で読み、符号の集合がすべての符号を L の一つの要素に集め、構成可能な合併が、構成が途中で集めた部分を結合します。

open import L.Coding.Environment {ℓ} using ( env; cons )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envS; Ix; envOver; module Recover )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( graph; envFor; envFor-graph )
open import L.Coding.CodeSet {ℓ} lem using ( AllCodes; keyS; key∈AllCodes )
open import L.Coding.CodeConstructibility {ℓ} using ( cupʟ; cupʟ-inl; cupʟ-inr )

一様な充足の表は、すべての符号にその充足集合を割り当て、外側で読めます。正準名の構成は、数項と、定数を持たない論理式のコードを Lset ω に置きます。そのような論理式にも自由変数の枠は残りえます。段階の内部の整列順序は要素を、まず誕生の段階、つぎに名前で比較します。

open import L.Coding.UniformSatisfaction {ℓ} lem using ( val-sat )
open import L.Choice.CanonicalNames {ℓ} lem using ( limitCode; numeral∈limit; pr∈limit )
open import L.Choice.NameComparison {ℓ} lem using ( freeCode-in; freeCode-out )
open import L.Choice.InternalWellOrder {ℓ} lem using ( relL; relL-fill; relL-rep )
open import L.Choice.StageOrders {ℓ} lem using ( orderAt; relOf )

狭義の整列順序の上の最小元の探索は、住民のある族から最小元を返します。関係そのものも、二つの読みをもつ対の集合になり、順序型の章が、崩壊の表を記述する三つの述語を述べます。

open import L.WellOrder.Base {ℓ-suc ℓ}
  using ( SWO; IsLeast; leastOf; isPropLeastOf )
  renaming ( Tri to Tri∙; lt to tri-lt; eq to tri-eq; gt to tri-gt )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( module Relation; isL-ord )
open import L.GCH.OrderType {ℓ} lem

正しさ、入力での完備さ、値の条項は、それぞれ二つの充足の読みをもつ論理式です。内部 ω 再帰は、モデル自身の ω に沿って、定義可能な二項のステップを反復します。包の要素は、任意の入れ子の深さの符号に名指されるので、一度の分離で包を作ることはできません。ω に沿って、定義可能な一段階の閉包を反復することではじめて届きます。閉包を ω 回作らねばならない理由はこれです。

  using ( Holds; Complete; Src; ValueIs; Correct
        ; completeAt; complete-in; complete-out
        ; valueAt; value-in; value-out
        ; correctAt; correct-in; correct-out )
open import L.GCH.OmegaRecursion {ℓ} lem using ( module Iterate )

証明は結びついた二つの部分からなります。まず局所的な崩壊表により、構成可能な台の各崩壊値が構成可能であることを示します。次に Skolem 包を有限閉包段階の合併として実現し、台自身の構成可能性を得て、第一の議論を適用します。

open import L.GCH.SkolemHull {ℓ} lem using ( module HullStage; module Frame )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )
open import L.GCH.AdequateStages {ℓ} lem using ( Superadequate )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )
open import L.GCH.CondensationTransfer {ℓ} lem using ( module Condense )

入れ子になった包の符号には有限の深さがあり、パラメータ符号の深さの最大値から計算されます。この深さが、その値の現れる閉包段階を上から評価します。

open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Data.Nat.Properties using ( max )
open import Cubical.Data.Nat.Order using ( _≤_; left-≤-max; right-≤-max )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Sum as Sum

有限パラメータベクトルにより、一つの証人符号は有限個の先行する値に依存できます。空集合、単集合、非順序対から、これらのパラメータとその順序対を階層内で表す集合符号を作れます。

import Cubical.Data.Empty as Empty
open import Cubical.Foundations.Prelude using ( subst2; J )
open import Cubical.Data.Vec using ( Vec; _∷_; []; lookup )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ⁅_,_⁆; ⁅_⁆s; module InfinitySet )

フォン・ノイマンの後者と数項により、有限閉包段階を ω の内部で整理します。非順序対は、グラフと環境に使う順序対を符号化する材料にもなります。

open import V.Model {ℓ} using ( pair-spec )
open InfinitySet {ℓ} using ( ω; sucV; #_ )
open import Cubical.Foundations.HLevels
  using ( isPropΣ; isPropΠ; isPropΠ2 )
open import Cubical.Functions.Logic using ( ⇔toPath )

存在の主張は、その証人を別の命題の証明にだけ使う段階まで命題的切断のまま保ちます。累積階層の等式は命題なので、崩壊の議論では集合の等式を示す際にこの切断されたデータを除去できます。

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ )

二つの所属を区別する必要があります。外側の所属は累積階層の関係です。一方、構成可能な台の要素は外側の集合とその構成可能性の証明を組にし、台上の所属はその基底集合を通して読まれます。

open hPropStructure 𝒮ᵥ
module CS = hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )

定数が L の要素である論理式について、⊨ は L のクラスモデルでの充足を表します。恒等写像による定数の付け替えは、環境も充足も変えません。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename )

i0 から i6 までの七つの名前が、最初の七つの de Bruijn 添字を略記します。長い環境の枠ごとに一つです。

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

各後続添字は直前の添字をより大きな有限型へ移します。名前は枠ごとに続きます。

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

これらは自由変数の位置であり、後の束縛子が環境を拡張すると読み方が移動します。

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

台の要素はその基礎の集合で決まります。構成可能性が命題だからです。基礎の集合が等しい台の要素は等しく、補助 S≡ が、同じ基礎の集合から台の要素を組み立て直す場所で、その同定を行います。

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

改名 ρs は二つの枠を入れ替えます。入れ替えた順で書かれた、ある対についての論理式を、元の順で読むためのものです。ステップの論理式を一方の枠の順で証明し、別の順で使うときに使われます。

  ρs : Fin  → Fin 
  ρs zero = suc zero
  ρs (suc zero) = zero

改名 ρf は w を第零スロットに保ち、Z を第一スロットから第二スロットへ送り、次段階の候補 Z' が占める中央のスロットを飛ばします。

  ρf : Fin  → Fin 
  ρf zero = zero
  ρf (suc zero) = suc (suc zero)

ρs の一致は、入れ替えた環境が、動いた枠で元の環境と同じ要素を載せていると言います。どちらの場合も反射性で証明できます。各枠が、同じ要素のある位置へ送られるからです。

  ags : (Z'' w : CS.S) → Ren.Agrees ρs (Z'' ∷ w ∷ []) (w ∷ Z'' ∷ [])
  ags Z'' w zero = refl
  ags Z'' w (suc zero) = refl

任意の構成可能な台 M を固定します。

  agf : (w Z' Z : CS.S) → Ren.Agrees ρf (w ∷ Z' ∷ Z ∷ []) (w ∷ Z ∷ [])
  agf w Z' Z zero = refl
  agf w Z' Z (suc zero) = refl

構成可能な台の崩壊は L にとどまる

崩壊の議論が使うのは M の構成可能性と、その内部に残る先行者だけであり、推移性は仮定しません。

module PiIn (Mʟ : CS.S) where

選んだ構成可能な台の基底集合を M とします。付随する証明により、後に M から持ち上げる各要素が構成可能であることが保証されます。

  M : S
  M = fst Mʟ

π x は、x の要素のうち M にも属するものの崩壊値から作られ、πX は x ∈ M に対する値 π x を集めます。この制限された先行者関係により、M の推移性を仮定せずに定義できます。

  module C = Collapse M using ( Fiber; π; π-compute; πX; πX-member; π∈-fwd )

構成可能性は要素へ受け継がれるので、各 y ∈ M は構成可能です。したがって y をその証明と組にし、構成可能な台の要素として扱えます。

  memL : (y : S) → ⟨ y ∈ˢ M ⟩ → ⟨ isL y ⟩
  memL y y∈M = isL-trans {x = M} {y = y} y∈M (snd Mʟ)

持ち上げ up は、要素を台の要素としてまとめます。最初の補題は、崩壊値を外向きに読みます。π x の要素はどれも、x の、M に属する要素の崩壊です。これは崩壊の計算の条項、すなわち「π x は x の M の中の要素の上の崩壊の像に等しい」という恒等式から従います。

  up : (y : S) → ⟨ y ∈ˢ M ⟩ → CS.S
  up y y∈M = y , memL y y∈M
  π-mem-out : (x w : S) → ⟨ w ∈ˢ C.π x ⟩
            → ∥ Σ[ y ∈ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) ∥₁
  π-mem-out x w w∈ = PT.map mk (subst (λ u → ⟨ w ∈ˢ u ⟩) (C.π-compute x) w∈)

この変換は、崩壊自身のファイバーの証人を、要素についての主張へ変えます。ファイバーは、提示された添字と、「提示された要素の崩壊が w に等しい」証明を組にします。提示された要素は、崩壊が取られる x の要素です。

    where
    mk : Σ[ p ∈ C.Fiber x ] (C.π (⟪ x ⟫↪ (p .fst)) ≡ w)
       → Σ[ y ∈ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w))
    mk (p , q) = ⟪ x ⟫↪ (p .fst)
               , ( member x (p .fst)

M の所属関係は三つの自由変数スロットで表され、Relation により環境 y ∷ x ∷ e ∷ [] で読まれます。第三スロットは符号化された対を載せ、論理式は y ∈ M、x ∈ M、y ∈ x を主張します。

                 , ∈∈ₛ {a = ⟪ x ⟫↪ (p .fst)} {b = M} .snd (p .snd)
                 , q )
  private
    module Membership = Relation Mʟ Mʟ
      ((var i1 ∈̇ con Mʟ) ∧̇ ((var i0 ∈̇ con Mʟ) ∧̇ (var i1 ∈̇ var i0)))

関係のホスト側の読みは、三つの所属の連言そのものです。この妥当性があるから、対象言語の論理式と外側の主張は互いに代わり合えます。

      (λ y x → (fst y ∈ˢ M) ⊓ ((fst x ∈ˢ M) ⊓ (fst y ∈ˢ fst x)))
      (λ y x z h → h) (λ y x z h → h)

関係はモデルの要素になります。台の要素の対からなる集合で、二つの読み出しによって導入と消去ができます。関係が台で界されているので、対の集合は分離で切り出せるほど小さいのです。

  R : CS.S
  R = Membership.rel

導入の読み出しは、両端の所属と、その間の所属を示します。それがこの対での関係の内容です。

  R-in : (y x : CS.S) → ⟨ fst y ∈ˢ M ⟩ → ⟨ fst x ∈ˢ M ⟩ → ⟨ fst y ∈ˢ fst x ⟩
       → Holds R y x
  R-in y x my mx yx = Membership.into y x my mx (my , mx , yx)

消去の読み出しは、同じ三つの所属を返します。二方向合わせて、この関係が妥当であること、ホスト側の主張よりも強くも弱くもないことが分かります。

  R-out : (y x : CS.S) → Holds R y x
        → ⟨ fst y ∈ˢ M ⟩ × ⟨ fst x ∈ˢ M ⟩ × ⟨ fst y ∈ˢ fst x ⟩
  R-out = Membership.pair-out

崩壊の論理式は、値と実引数の枠の上に立ち、大域的ではなく局所的です。こう言います。関係 R に対して正しく、実引数で完備であり、そこでの値が与えられた値であるような表 F が、単に存在する、と。一つの大域的な関数のグラフを主張するのではなく、各実引数でそのような表の存在だけを述べるのです。だからこの論理式は、推移的でない台の上でも成立します。

  opaque
    piFo : Formula CS.S 
    piFo = ∃̇ ( correctAt i0 R
             ∧̇ ( completeAt i0 R i2 ∧̇ valueAt i0 R i2 i1 ) )

論理式の外向きの読み出しは、充足を三つの成分にほどきます。正しい表、実引数での完備さ、値の条項です。それぞれの連言項が、順序型の章自身の射影によって束縛子の外へ運ばれます。

    piFo-out : (v p : CS.S) → ⟨ (v ∷ p ∷ []) ⊨ piFo ⟩
             → ∥ Σ[ F ∈ CS.S ] (Correct F R × (Complete F R p × ValueIs F R p v)) ∥₁
    piFo-out v p = PT.map (λ { (F , (hc , (hm , hv))) → F
      , ( correct-out i0 R (F ∷ v ∷ p ∷ []) hc
        , ( complete-out i0 R i2 (F ∷ v ∷ p ∷ []) hm

最も内側の射影がほどきを終えます。値の条項は、実引数での表の項目についての通常の主張として届きます。

          , value-out i0 R i2 i1 (F ∷ v ∷ p ∷ []) hv ) ) })

内向きの読みでは、存在量化の証人として表 F を選び、その正しさ、入力での完全性、値の条項の証明を与えます。外向きの読みと合わせると、この論理式は意図した内容と正確に対応します。

    piFo-in : (v p F : CS.S) → Correct F R → Complete F R p → ValueIs F R p v
            → ⟨ (v ∷ p ∷ []) ⊨ piFo ⟩
    piFo-in v p F hc hm hv = ∣ F
      , ( correct-in i0 R (F ∷ v ∷ p ∷ []) hc
        , ( complete-in i0 R i2 (F ∷ v ∷ p ∷ []) hm

一意性は、所属に沿う帰納が一回で証明します。動機はこう言います。台の構成可能な要素 x のそれぞれで、その関係に対して正しく x で完備な表は、x の崩壊を値として割り当てる、と。構成可能性も所属も、表の項目が台の要素の対であるために、動機とともに運ばれます。

          , value-in i0 R i2 i1 (F ∷ v ∷ p ∷ []) hv ) ) ∣₁
  private
    Pv : CS.S → S → Type (ℓ-suc ℓ)
    Pv F x = (xL : ⟨ isL x ⟩) → ⟨ x ∈ˢ M ⟩ → (v : CS.S)
           → Complete F R (x , xL) → ValueIs F R (x , xL) v → fst v ≡ C.π x

帰納は、周囲の階層の所属に沿って走ります。崩壊そのものがそうやって定義されているからです。x での動機を証明するには、x のすべての要素での動機を証明します。

  value-val′ : (F : CS.S) → Correct F R → (x : S) → Pv F x
  value-val′ F hc = ∈-induction {P = Pv F} go
    where
    go : (x : S) → ((y : S) → ⟨ y ∈ˢ x ⟩ → Pv F y) → Pv F x
    go x IH xL x∈M v cmp val =

ステップは要素を比較します。記録された値と崩壊は同じ要素をもち、周囲の階層の外延性がそれを等しさへ変えます。入力は台の要素として提示されるので、その項目は台の上で型づけられます。

      extensionalV {a = fst v} {b = C.π x} (λ w → ⇔toPath (fwd w) (bwd w))
      where
      xS : CS.S
      xS = x , xL

前向き：記録された値の要素 w を台に載せ、値の条項が、関係の項目と、そこの表の項目を作ります。載せるとき、記録された値から受け継いだ構成可能性を w とともに包みます。

      fwd : (w : S) → ⟨ w ∈ˢ fst v ⟩ → ⟨ w ∈ˢ C.π x ⟩
      fwd w w∈ = PT.rec (snd (w ∈ˢ C.π x)) read (val wS .fst w∈)
        where
        wS : CS.S
        wS = w , isL-trans {x = fst v} {y = w} w∈ (snd v)

源の証人は関係の事実 ry と表の項目 fy に分かれます。ry から y ∈ M と y ∈ x を読み、fy に帰納法の仮定を適用して w を π y と同定し、π∈-fwd によって w を π x に入れます。

        read : Σ[ y ∈ CS.S ] (Holds R y xS × Holds F y wS) → ⟨ w ∈ˢ C.π x ⟩
        read (y , (ry , fy)) =
          subst (λ t → ⟨ t ∈ˢ C.π x ⟩) e (C.π∈-fwd x (fst y) y∈x y∈M)
          where
          y∈M : ⟨ fst y ∈ˢ M ⟩

関係の項目はさらに、その成分が入力の下にあるとも言い、これが帰納の仮定を解き放ちます。その成分での表の値は成分の崩壊に等しい、と。この等式を崩壊の読み出しと合成すれば、w の同定が終わります。

          y∈M = R-out y xS ry .fst
          y∈x : ⟨ fst y ∈ˢ x ⟩
          y∈x = R-out y xS ry .snd .snd
          e : C.π (fst y) ≡ w
          e = sym (IH (fst y) y∈x (snd y) y∈M wS (hc y wS fy .fst) (hc y wS fy .snd))

後ろ向き：崩壊の要素 w は、すでに証明した外向きの読みによって、台の中の入力の成分へと分解され、その成分の崩壊が w になります。元の実引数 x における表の完備さを前者 y に適用すると、項目 (y,u) が得られます。

      bwd : (w : S) → ⟨ w ∈ˢ C.π x ⟩ → ⟨ w ∈ˢ fst v ⟩
      bwd w w∈ = PT.rec (snd (w ∈ˢ fst v)) read (π-mem-out x w w∈)
        where
        read : Σ[ y ∈ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) → ⟨ w ∈ˢ fst v ⟩
        read (y , (y∈x , y∈M , e)) = PT.rec (snd (w ∈ˢ fst v)) inner (cmp yS ry)

その成分は台の要素として載せられ、対での関係の項目が、二つの所属とその間の所属から改めて導入されます。

          where
          yS : CS.S
          yS = up y y∈M
          ry : Holds R yS xS
          ry = R-in yS xS y∈M x∈M y∈x

帰納法の仮定が u を π y と同定し、π y = w に沿って輸送すると、w が記録された値に属することが従います。後ろ向きの方向が主張するのはこれです。

          inner : Σ[ u ∈ CS.S ] Holds F yS u → ⟨ w ∈ˢ fst v ⟩
          inner (u , fu) =
            subst (λ t → ⟨ t ∈ˢ fst v ⟩) (eu ∙ e) (val u .snd ∣ yS , (ry , fu) ∣₁)
            where
            eu : fst u ≡ C.π y

等式 eu は、成分 y での帰納の仮定です。表の y での値は y の崩壊に等しい、というものです。分解が携える等式と合成すれば、項目の値は w と同一視され、後ろ向きの方向が置こうとしていたのはまさにこれです。

            eu = IH y y∈x (snd yS) y∈M u (hc yS u fu .fst) (hc yS u fu .snd)

台の要素の基礎集合に帰納を適用すると、制限された構造で同じ一意性の主張が得られます。得られる決定補題は、崩壊の論理式が M の要素で成立するなら、その値はその要素の崩壊に等しいことを述べます。

  value-val : (F : CS.S) → Correct F R → (x : CS.S) → ⟨ fst x ∈ˢ M ⟩ → (v : CS.S)
            → Complete F R x → ValueIs F R x v → fst v ≡ C.π (fst x)
  value-val F hc x = value-val′ F hc (fst x) (snd x)
  piFo-val : (q : CS.S) → ⟨ fst q ∈ˢ M ⟩ → (v : CS.S) → ⟨ (v ∷ q ∷ []) ⊨ piFo ⟩
           → fst v ≡ C.π (fst q)

証明は、切り詰められた存在を二つの h-集合の等しさという命題へ消去し、外向きの読み出しが手渡す正しい表に、今証明した一意性を適用します。次の構成では、L の与えられた要素の内側にある要素を台から切り出します。

  piFo-val q mq v h = PT.rec (setIsSet (fst v) (C.π (fst q)))
    (λ { (F , (hc , (hm , hv))) → value-val F hc q mq v hm hv })
    (piFo-out v q h)
  module Cut (K : CS.S) where

切り出しの論理式はただ一つの原子論理式です。自由な枠が定数 K の要素であることを表します。スライスが収めるのは、これを満たす要素だけです。

    cutFo : Formula CS.S 
    cutFo = var i0 ∈̇ con K

分離を Mʟ に適用することで、スライスも L の要素として得られ、単なる要素の類では終わりません。このため、スライスを内部再帰の定義域として使えます。

    opaque
      cut : CS.S
      cut = hasSeparationL Mʟ cutFo .fst .fst

所属の仕様は、スライスへの所属を、台への所属と切り出しの論理式の充足とを合わせたものとして同定します。後者はほどけば、K の基礎の集合の中にあることにほかなりません。

      cut-mem : (y : CS.S) → (y CS.∈ˢ cut) ≡ ((y CS.∈ˢ Mʟ) ⊓ ((y ∷ []) ⊨ cutFo))
      cut-mem = hasSeparationL Mʟ cutFo .fst .snd

内向きの方向は、M への所属と K の基礎集合への所属を組み合わせ、載せた要素をスライスに入れます。

      cut-in : (y : CS.S) → ⟨ fst y ∈ˢ M ⟩ → ⟨ fst y ∈ˢ fst K ⟩ → ⟨ y CS.∈ˢ cut ⟩
      cut-in y my yK = subst ⟨_⟩ (sym (cut-mem y)) (my , yK)

外向きの方向は、同じ仕様を二つの成分へ読み戻します。台の要素 q が段階 δ で「良い」とは、その段階に属するとき、崩壊の構成可能な表示と q における崩壊の論理式の両方が得られることです。

      cut-out : (y : CS.S) → ⟨ y CS.∈ˢ cut ⟩ → ⟨ fst y ∈ˢ M ⟩ × ⟨ fst y ∈ˢ fst K ⟩
      cut-out y h = subst ⟨_⟩ (cut-mem y) h
  Good : S → S → Type (ℓ-suc ℓ)
  Good δ q = ⟨ q ∈ˢ M ⟩ → ⟨ q ∈ˢ Lset δ ⟩
           → Σ[ qL ∈ ⟨ isL (C.π q) ⟩ ] ((mq : ⟨ q ∈ˢ M ⟩)

「良いこと」の第二成分は、構成可能性の証明によって崩壊を 𝒮ʟ の要素として包み、その値と選んだ M の要素の表示について崩壊の論理式が成立することを述べます。

                → ⟨ ((C.π q , qL) ∷ up q mq ∷ []) ⊨ piFo ⟩)

「良いこと」は命題です。台への所属も、段階への所属も、構成可能性も充足も、それぞれ命題だからです。ここが大切です。段階の分解が返すのは、単に存在するだけの証人ですが、命題である「良いこと」なら、証人を選ぶことなく消費できるのです。

  isPropGood : (δ q : S) → isProp (Good δ q)
  isPropGood δ q = isPropΠ2 λ _ _ → isPropΣ (snd (isL (C.π q)))
    λ qL → isPropΠ λ mq → snd (((C.π q , qL) ∷ up q mq ∷ []) ⊨ piFo)

順序数段階 δ' を固定し、M と Lset δ' の両方に属する各 q が「良い」と仮定します。これら先行する崩壊値を組み合わせて、次の入力での値を作ります。

  module Step (δ' : S) (oδ' : IsOrd δ')
              (IH : (q : S) → Good δ' q) where

スライスは、段階 Lset δ' で切り出されます。その段階がすでに収めている台の要素です。段階は L の集合なので、スライスは分離によって L の要素になり、これこそ帰納の仮定が語る定義域です。

    module Sl = Cut (LsetS δ' oδ') using ( cut; cut-in; cut-out )

段階は推移的です。したがって、段階の要素の要素も段階の内側にあり、この事実が後で表の条件をより小さい入力へ制限します。帰納の仮定により、スライスの要素の崩壊は 𝒮ʟ の要素として得られ、その構成可能性の証明が「良いこと」の第一成分です。

    Lδ'-trans : {x y : S} → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ Lset δ' ⟩ → ⟨ y ∈ˢ Lset δ' ⟩
    Lδ'-trans {x} {y} = layer-trans (Lset-layer δ') {x = x} {y = y}
    πʟ : (y : CS.S) → ⟨ y CS.∈ˢ Sl.cut ⟩ → CS.S
    πʟ y hy = C.π (fst y) , IH (fst y) (Sl.cut-out y hy .fst) (Sl.cut-out y hy .snd) .fst

崩壊の論理式が、その崩壊と要素の対の上で成立するのも、同じ帰納の仮定によります。「良いこと」の第二成分はちょうど、この対での論理式の充足であり、要素とその基礎の集合の同定に沿って運ばれます。

    πʟ-graph : (y : CS.S) (hy : ⟨ y CS.∈ˢ Sl.cut ⟩)
             → ⟨ (πʟ y hy ∷ y ∷ []) ⊨ piFo ⟩
    πʟ-graph y hy =
      subst (λ y' → ⟨ (πʟ y hy ∷ y' ∷ []) ⊨ piFo ⟩) (S≡ refl)
        (IH (fst y) my (Sl.cut-out y hy .snd) .snd my)

この同定には、スライスの仕様から読み出した要素の台への所属を使います。基礎集合は変わっておらず、構成可能性の証明は命題なので、この同一視に沿った輸送は一意に定まります。

      where
      my : ⟨ fst y ∈ˢ M ⟩
      my = Sl.cut-out y hy .fst

スライス上の崩壊値は、スライスを定義域、piFo をグラフの論理式とする内部再帰をなします。構成可能性によって各値は 𝒮ʟ の要素となるので、グラフの項目は 𝒮ʟ の要素の対です。

    private
      Rπ : Recursion
      Rπ = record
        { dom = Sl.cut ; graph = piFo
        ; funct = λ y hy → (πʟ y hy , πʟ-graph y hy)

関数性が成立するのは、崩壊の論理式が台のすべての要素でその値を決めるからです。同じ対で論理式を満たすほかの値はどれもそれと等しく、決定の補題がそれを読み出します。対応する 𝒮ʟ の要素の等しさは、構成可能性の証明が命題値であることから従います。

            , λ { (v , h) → Σ≡Prop (λ w → snd ((w ∷ y ∷ []) ⊨ piFo))
                (sym (S≡ (piFo-val y (Sl.cut-out y hy .fst) v h))) } }

L のグラフの再帰が表を集めます。台の要素の対からなる集合で、その項目はスライス上の崩壊の記録にほかなりません。

      module T = RecursionGraph Rπ using ( F; F-in; pair-out )

集められた集合が、この段階での表です。L の要素であり、スライスの各要素と、その構成可能な崩壊とを対にします。

    Tab : CS.S
    Tab = T.F

表の内向きの読み出しは、その項目を示します。スライスの各要素で、要素とその崩壊の対が記録されます。

    Tab-in : (y : CS.S) (hy : ⟨ y CS.∈ˢ Sl.cut ⟩) → Holds Tab y (πʟ y hy)
    Tab-in = T.F-in

外向きの読み出しは、項目をスライスの要素と、その基礎集合の崩壊に等しい値へ分解します。内向きの読み出しと合わせて、表が記録するのは崩壊そのものであり、歪みがないことが分かります。

    Tab-pair : (x v : CS.S) → Holds Tab x v
             → ⟨ x CS.∈ˢ Sl.cut ⟩ × (fst v ≡ C.π (fst x))
    Tab-pair = T.pair-out

引数 x が閉じているとは、x の要素であり、かつ M に属するものがすべて段階スライスに入ることです。この条件は引数ごとに課されます。ここでは M の推移性を仮定していません。

    Closed : CS.S → Type (ℓ-suc ℓ)
    Closed x = (y : S) (y∈x : ⟨ y ∈ˢ fst x ⟩) (y∈M : ⟨ y ∈ˢ M ⟩)
             → ⟨ up y y∈M CS.∈ˢ Sl.cut ⟩

スライスの要素は段階の推移性によって閉じています。その要素であり、かつ M に属するものは段階内にとどまるので、スライスに属します。

    slice-closed : (x : CS.S) → ⟨ x CS.∈ˢ Sl.cut ⟩ → Closed x
    slice-closed x hx y y∈x y∈M =
      Sl.cut-in (up y y∈M) y∈M (Lδ'-trans {x = fst x} {y = y} y∈x (Sl.cut-out x hx .snd))

閉じた入力に対する表の完備さとは、関係する各要素での表自身の項目の切り詰められた存在です。閉じていることがその要素をスライスの中へ置き、表がそこに崩壊を記録します。関係の項目は分解されて、その要素を名指します。

    complete-of : (x : CS.S) → Closed x → Complete Tab R x
    complete-of x cl y ry = ∣ πʟ y' hy' , subst (λ w → ⟨ pr w (C.π (fst y)) ∈ˢ fst Tab ⟩) refl (Tab-in y' hy') ∣₁
      where
      ro = R-out y x ry
      y' : CS.S

その要素は台の要素として載せられ、閉じていることが、載せられた要素をスライスの中へ置きます。これは、表が崩壊を記録したときの仮定そのものです。

      y' = up (fst y) (ro .fst)
      hy' : ⟨ y' CS.∈ˢ Sl.cut ⟩
      hy' = cl (fst y) (ro .snd .snd) (ro .fst)

閉じた入力に対して、値の条項は崩壊そのものについて成立します。証明には二方向あります。崩壊値の要素はどれも関係する要素から来ており、入力と関係する要素はどれも、表によって崩壊値の中へ運ばれます。

    valueIs-of : (x : CS.S) → ⟨ fst x ∈ˢ M ⟩ → Closed x → (v : CS.S) → fst v ≡ C.π (fst x)
               → ValueIs Tab R x v
    valueIs-of x mx cl v ev w = fwd , bwd
      where
      fwd : ⟨ fst w ∈ˢ fst v ⟩ → Src Tab R x w

前向きでは、候補の値 v の要素 w を、崩壊の読み出しによって台の中の入力の成分へ分解します。その成分の崩壊は w に等しくなります。分解は切り詰められた存在であり、消去の対象は命題です。

      fwd w∈ = PT.map read (π-mem-out (fst x) (fst w) (subst (λ t → ⟨ fst w ∈ˢ t ⟩) ev w∈))
        where
        read : Σ[ y ∈ S ] (⟨ y ∈ˢ fst x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ fst w))
             → Σ[ y ∈ CS.S ] (Holds R y x × Holds Tab y w)
        read (y , (y∈x , y∈M , e)) = up y y∈M

その成分を台の要素へ持ち上げます。入力への所属から関係の項目が得られ、表の項目はその崩壊と w の等式に沿って輸送されます。この二つを合わせると、必要な Src Tab R x w の証人になります。

          , ( R-in (up y y∈M) x y∈M mx y∈x
            , subst (λ t → ⟨ pr y t ∈ˢ fst Tab ⟩) e (Tab-in (up y y∈M) (cl y y∈x y∈M)) )

後ろ向き：w のソースの項目は、表の値が w であるような関係する要素を名指します。対の読み出しが項目を所属と等式に分け、崩壊の読み出しが w を第一成分の崩壊の中に置き、二つの等式がそれを記録された値へ運び戻します。

      bwd : Src Tab R x w → ⟨ fst w ∈ˢ fst v ⟩
      bwd = PT.rec (snd (fst w ∈ˢ fst v)) (λ { (y , (ry , ty)) →
        subst2 (λ s t → ⟨ s ∈ˢ t ⟩) (sym (Tab-pair y w ty .snd)) (sym ev)
          (C.π∈-fwd (fst x) (fst y) (R-out y x ry .snd .snd) (R-out y x ry .fst)) })

それぞれの項目での表の正しさは、その項目が名指すスライスの要素での二つの条項から組み立てられます。対の読み出しが、スライスへの所属と台への所属を与えます。

    Tab-correct : Correct Tab R
    Tab-correct x v hxv = complete-of x cl , valueIs-of x mx cl v (Tab-pair x v hxv .snd)
      where
      hx : ⟨ x CS.∈ˢ Sl.cut ⟩
      hx = Tab-pair x v hxv .fst

台への所属と閉じていることが仮定を完成させ、ステップのモジュールは、その要素がすべてより前の段階の下にあるような台の入力 q でパラメータづけられます。これは Lset δ' の定義可能冪集合の要素に必要な状況であり、ここでは閉じていることが q⊆ から従います。

      mx : ⟨ fst x ∈ˢ M ⟩
      mx = Sl.cut-out x hx .fst
      cl : Closed x
      cl = slice-closed x hx
    module At (q : S) (mq : ⟨ q ∈ˢ M ⟩) (q⊆ : (y : S) → ⟨ y ∈ˢ q ⟩ → ⟨ y ∈ˢ Lset δ' ⟩) where

入力は台の要素として載せられ、環境の枠としても、対の第二成分としても働けるようになります。

      qS : CS.S
      qS = up q mq

載せた入力の閉じていることは仮定から成立します。台の中のその要素はすべてより前の段階の下にあり、スライスが受け入れます。そして台の中の入力の要素が、それ自身のスライスとして切り出されます。崩壊の値はこの定義域の上で計算されます。

      cl : Closed qS
      cl y y∈q y∈M = Sl.cut-in (up y y∈M) y∈M (q⊆ y y∈q)
      module Mq = Cut qS using ( cut; cut-in; cut-out )

q の崩壊値は、内部の再帰として作られます。定義域は台の中の q の要素のスライス、グラフは崩壊の論理式です。したがって、この関数的グラフは L における置換の仮定を満たします。

      private
        valR : Recursion
        valR = record
          { dom   = Mq.cut
          ; graph = piFo

関数性は mereFunct を通して組み立てられます。各入力で、一意な値が「単に存在する」ことからです。証人 wit は、そのような値と、その充足と一意性とを、切り詰めの内側で産出します。台の要素での崩壊の論理式の一意性が命題だからです。

          ; funct = λ y hy → mereFunct piFo y (wit y hy) }
          where
          wit : (y : CS.S) (hy : ⟨ y CS.∈ˢ Mq.cut ⟩)
              → ∥ Σ[ v ∈ CS.S ] (⟨ (v ∷ y ∷ []) ⊨ piFo ⟩
                                × ((v' : CS.S) → ⟨ (v' ∷ y ∷ []) ⊨ piFo ⟩ → v' ≡ v)) ∥₁

証人は大域的な崩壊値 C.π (fst y) であり、帰納の仮定によって構成可能なものとして表示されます。段階スライス上の表が piFo の証明を与え、piFo-val が一意性を与えます。

          wit y hy = ∣ πʟ y hy'
            , ( πʟ-graph y hy'
              , λ v' hv' → S≡ (piFo-val y my v' hv') ) ∣₁
            where
            my : ⟨ fst y ∈ˢ M ⟩

y の台への所属は q のスライスから来ます。仮定により q の各要素は Lset δ' に入るので、そのうち台に属する要素はすべて段階スライスに入ります。

            my = Mq.cut-out y hy .fst
            hy' : ⟨ y CS.∈ˢ Sl.cut ⟩
            hy' = Sl.cut-in y my (q⊆ (fst y) (Mq.cut-out y hy .snd))

置換はこの再帰の値を L の要素として集めます。その要素はちょうど、q の要素であり、かつ M に属するものの構成可能な崩壊値です。

        module Vq = Of valR using ( table; table-in; table-out )

表の基礎の集合は、q の崩壊と一致します。要素ごとの同値を通して外延性で証明されます。前向き：表の要素は、台の中の q のある要素 y での値であり、消去の対象は「w が q の崩壊に属する」という命題です。

      val≡π : fst Vq.table ≡ C.π q
      val≡π = extensionalV {a = fst Vq.table} {b = C.π q} (λ w → ⇔toPath (fwd w) (bwd w))
        where
        fwd : (w : S) → ⟨ w ∈ˢ fst Vq.table ⟩ → ⟨ w ∈ˢ C.π q ⟩
        fwd w hw = PT.rec (snd (w ∈ˢ C.π q))

外向きの読み出しが要素 y とその値を名指し、決定の補題がその値を y の崩壊と同一視し、崩壊の読み出しが y の崩壊を q の崩壊の中へ置きます。輸送がこの二つを合成します。

          (λ { (y , (hy , h)) →
             subst (λ t → ⟨ t ∈ˢ C.π q ⟩)
               (sym (piFo-val y (Mq.cut-out y hy .fst) wS h))
               (C.π∈-fwd q (fst y) (Mq.cut-out y hy .snd) (Mq.cut-out y hy .fst)) })
          (Vq.table-out wS hw)

w は構成可能な値集合 Vq.table に属するので、L の推移性から w の構成可能性が得られ、𝒮ʟ の要素として表示できます。

          where
          wS : CS.S
          wS = w , isL-trans {x = fst Vq.table} {y = w} hw (snd Vq.table)

後ろ向き：q の崩壊の要素は、台の中の q の成分へと分解され、その成分の崩壊がそれと等しくなります。これは、表が項目を記録する形そのものです。

        bwd : (w : S) → ⟨ w ∈ˢ C.π q ⟩ → ⟨ w ∈ˢ fst Vq.table ⟩
        bwd w hw = PT.rec (snd (w ∈ˢ fst Vq.table)) read (π-mem-out q w hw)
          where
          read : Σ[ y ∈ S ] (⟨ y ∈ˢ q ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) → ⟨ w ∈ˢ fst Vq.table ⟩
          read (y , (y∈q , y∈M , e)) =

等式が w を成分の崩壊へ運び、表の内向きの読み出しが、載せた成分での項目を作ります。そこに記録されるのはまさにその崩壊です。

            subst (λ t → ⟨ t ∈ˢ fst Vq.table ⟩) e
              (Vq.table-in yS (πʟ yS hy') hy (πʟ-graph yS hy'))
            where
            yS : CS.S
            yS = up y y∈M

載せた成分は、台への所属によって q のスライスの中にあり、また「q の要素はより前の段階の下にある」という仮定によって、段階のスライスの中にもあります。

            hy : ⟨ yS CS.∈ˢ Mq.cut ⟩
            hy = Mq.cut-in yS y∈M y∈q
            hy' : ⟨ yS CS.∈ˢ Sl.cut ⟩
            hy' = Sl.cut-in yS y∈M (q⊆ y y∈q)

q の崩壊は構成可能です。それは表の基礎の集合に等しく、表は L の要素なので、構成可能性がこの等式に沿って運ばれます。これが q での「良いこと」の最初の条項です。

      πq-isL : ⟨ isL (C.π q) ⟩
      πq-isL = subst (λ t → ⟨ isL t ⟩) val≡π (snd Vq.table)

「良いこと」の第二の条項は、崩壊と要素の対の上で崩壊の論理式が成立することです。表の正しさ、閉じた入力での完備さ、そして値を崩壊と同定する値の条項です。二つの条項がそろえば、段階の帰納を述べられます。すべての順序数での「良いこと」です。

帰納は、階層の所属に沿って走り、各ステップで、段階への所属の分解を消費します。

      good : (mq' : ⟨ q ∈ˢ M ⟩) → ⟨ ((C.π q , πq-isL) ∷ up q mq' ∷ []) ⊨ piFo ⟩
      good mq' = subst (λ q' → ⟨ ((C.π q , πq-isL) ∷ q' ∷ []) ⊨ piFo ⟩) (S≡ refl)
        (piFo-in (C.π q , πq-isL) qS Tab Tab-correct (complete-of qS cl)
          (valueIs-of qS mq cl (C.π q , πq-isL) refl))
  good-at : (δ : S) → IsOrd δ → (q : S) → Good δ q

δ での「良いこと」を証明するには、段階 Lset δ への q の所属を分解します。q は、より前の段階 δ' の定義可能冪集合の中にある、と。分解は「良いこと」へ消去されます。「良いこと」が命題だからです。

  good-at = ∈-induction {P = λ δ → IsOrd δ → (q : S) → Good δ q} go
    where
    go : (δ : S) → ((δ' : S) → ⟨ δ' ∈ˢ δ ⟩ → IsOrd δ' → (q : S) → Good δ' q)
       → IsOrd δ → (q : S) → Good δ q
    go δ IH oδ q mq q∈Lδ = PT.rec (isPropGood δ q) read (Lset-out δ q q∈Lδ) mq q∈Lδ

分解は、δ の下のより前の段階 δ' と、その定義可能冪集合への q の所属を名指します。δ' より下での「良いこと」を使うと、ステップの構成から q での「良いこと」が得られます。定義可能冪集合の条項はさらに、q のすべての要素が段階 Lset δ' の中にあると言います。これが、ステップが消費する閉じていることの仮定です。

      where
      read : Σ[ δ' ∈ S ] (⟨ δ' ∈ˢ δ ⟩ × ⟨ q ∈ˢ 𝒟ₒ (Lset δ') ⟩) → Good δ q
      read (δ' , (δ'∈δ , q∈𝒟)) _ _ = A.πq-isL , A.good
        where
        oδ' : IsOrd δ'

δ' ∈ δ から δ' の順序数性が得られます。δ' より下で帰納の仮定を使い、q のすべての要素が Lset δ' に属するという定義可能冪集合の事実を合わせると、q での「良いこと」が得られ、good-at の所属帰納が閉じます。また M 自身が L に属するので、その構成可能性の証明から M を含む段階が得られ、その段階の推移性によって M の各要素も段階内に入ります。

        oδ' = mem-ord {A = δ} oδ δ' δ'∈δ
        module A = Step.At δ' oδ' (IH δ' δ'∈δ oδ') q mq (λ y y∈q → 𝒟ₒ∋⊆ (Lset δ') q q∈𝒟 y y∈q)
          using ( πq-isL; good )
  π-isL : (y : S) → ⟨ y ∈ˢ M ⟩ → ⟨ isL (C.π y) ⟩
  π-isL y y∈M = PT.rec (snd (isL (C.π y)))

証明 Mʟ から構成可能な台 M を含む段階を取り、その段階での「良いこと」から M の各要素の崩壊が構成可能であることを得ます。続く主張は、崩壊像全体 C.πX の要素について同じ議論を始め、やはり切り詰められた表示を構成可能性へ消去します。

    (λ { (α , (oα , M∈Lα)) →
       good-at α oα y y∈M (layer-trans (Lset-layer α) {x = M} {y = y} y∈M M∈Lα) .fst })
    (snd Mʟ)
  πX-isL : (x : S) → ⟨ x ∈ˢ C.πX ⟩ → ⟨ isL x ⟩
  πX-isL x x∈πX = PT.rec (snd (isL x))

πX-isL の主張は要素についてのものです。

    (λ { (y , (y∈M , e)) → subst (λ w → ⟨ isL w ⟩) e (π-isL y y∈M) })
    (C.πX-member x x∈πX)

Skolem 包を ω 反復として表す

崩壊像の各要素は台のどこかの要素の崩壊であり、だから構成可能です。これは、崩壊像が L に含まれると言っているだけです。像そのものが L の要素であるとは主張していません。前半が終わり、後半は新しいパラメータで始まります。要素の後者で閉じた段階 lam と、その要素がすべて段階の中にある始点 X です。

module Telescope (lam : S) (ordλ : IsOrd lam)
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)

空集合も段階の中にあり、包の機構がこれらのデータの上で開かれます。包の台 M、包が段階に含まれること、そして始点のすべての要素が包の要素であることです。

  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where
  module HS = HullStage lam ordλ succλ X X⊆L ∅∈λ using ( M )
  module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ
    using ( ∅∈Lsetα; hull-member; X⊆M; Hull⊆L )
  open HullStage.H.T lam ordλ succλ X X⊆L ∅∈λ public

包の符号は、X の要素に対する基底名か、無定数公式とそのパラメータの符号を保存する wit k ψ cs です。部分符号を評価した後、証人が存在するかどうかに応じて、最小の証人または廃棄値をその値とします。

    using ( Code; base; wit; val; vals; search; Sat; Hull; val-wit )
  open HullStage.H.T lam ordλ succλ X X⊆L ∅∈λ using ( inHull; _⊨₀_ )

小さな台 SL は、すべてが型づけられる、段階の要素を集めます。集合 Z から取ったパラメータのベクトルとは、各成分が Z の基礎の集合に属することです。ステップの探索はそのようなベクトルだけにわたります。

  SL : Type (ℓ-suc ℓ)
  SL = HullStage.ASt.SL lam ordλ succλ X X⊆L ∅∈λ
  From : {k : ℕ} → CS.S → Vec SL k → Type (ℓ-suc ℓ)
  From {k} Z vs = (i : Fin k) → ⟨ fst (lookup i vs) ∈ˢ fst Z ⟩
  Searched : CS.S → S → Type (ℓ-suc ℓ)

探索にはアリティ k+1 の無定数公式を使います。Z から取ったベクトルが k 個のパラメータ変数に値を与え、残る変数には候補となる証人を割り当てます。Sat はそのような証人の存在を表します。

  Searched Z z = Σ[ k ∈ ℕ ] Σ[ ψ ∈ Formula (⊥* {ℓ}) (suc k) ] Σ[ vs ∈ Vec SL k ]
                 Σ[ w ∈ Sat k ψ vs ] (From Z vs × (z ≡ fst (search k ψ vs w)))
  Reads : CS.S → S → Type (ℓ-suc ℓ)
  Reads Z z = ⟨ z ∈ˢ fst Z ⟩ ⊎ ((z ≡ ∅) ⊎ Searched Z z)

この構造は、演算 Φ、二変数公式 ΦFo、そして任意の Z について二つの変数に Φ Z と Z を割り当てた環境がその公式を満たすという証明を含みます。

  record StepPack : Type (ℓ-suc (ℓ-suc ℓ)) where
    field
      Φ       : CS.S → CS.S
      ΦFo     : Formula CS.S 
      defines : (Z : CS.S) → ⟨ (Φ Z ∷ Z ∷ []) ⊨ ΦFo ⟩

残りのフィールドがステップを確定させます。論理式を満たす集合はどれもステップの集合であり、要素は増え、廃棄値はつねにあり、現在の集合から取ったパラメータでのすべての探索に、最小の証人が加わります。

      only    : (Z Z' : CS.S) → ⟨ (Z' ∷ Z ∷ []) ⊨ ΦFo ⟩ → Z' ≡ Φ Z
      grows   : (Z : CS.S) (z : S) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ fst (Φ Z) ⟩
      junk    : (Z : CS.S) → ⟨ ∅ ∈ˢ fst (Φ Z) ⟩
      least   : (Z : CS.S) (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec SL k)
              → From Z vs → (w : Sat k ψ vs) → ⟨ fst (search k ψ vs w) ∈ˢ fst (Φ Z) ⟩

外向きのフィールドは、現在の集合が段階の下にあるとき、ステップの要素をホスト側で読みます。ステップの要素は、古い要素、廃棄値、探索の値のいずれかです。使い尽くしの証明が使うのはこの読み出しです。

      out     : (Z : CS.S) → ((z : S) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
              → (z : S) → ⟨ z ∈ˢ fst (Φ Z) ⟩ → ∥ Reads Z z ∥₁

反復のモジュールは、始点の構成可能性と、まとめられたステップを受け取ります。どちらも必要です。内部の再帰は L の要素からはじまり、ステップが論理式とその条項を供給するからです。

  module HullIter (X-isL : ⟨ isL X ⟩) (P : StepPack) where
    open StepPack P

始点は台の要素として提示されます。集合とその構成可能性の組であり、内部の再帰が消費するのはこの形です。

    Xʟ : CS.S
    Xʟ = X , X-isL

内部の ω 再帰が反復を作り、その閉包の機構が成長のフィールドを持ち運びます。それぞれの反復は前のものを含みます。反復はモデルの集合であり、反復の合併が L の要素になるのはこのためです。

    module It = Iterate Xʟ ΦFo Φ defines only
      using ( it; module Closure; iterUnion; iterUnion-in; iterUnion-out; iter; iter-in; iter-out; ω-num; Num )
    module Cl = It.Closure (λ Z z → grows Z (fst z)) using ( it-up )

反復の各段階は hullStep n と名づけられます。始点に対するステップの n 回目の適用です。

    hullStep : ℕ → CS.S
    hullStep = It.it

反復はその定義の等式に支配されます。ステップを n+1 回適用して得られるものは、n 番目の反復に一段階の閉包 Φ を適用したものちょうどです。この等式は refl で成立します。内部の ω 再帰は、後者の段階を計算するときにステップの演算を直接呼ぶので、輸送は何も要りません。これが、この構成のもっとも裸の算術です。この構成のそれぞれの層は、前の層の、ただ一つの定義可能なステップの下での閉包です。

    hullStep-suc : (n : ℕ) → hullStep (suc n) ≡ Φ (hullStep n)
    hullStep-suc n = refl

反復はその添字とともに増えます。n が n' を超えなければ、n 番目の反復が集めたものはすべて、n' 番目の反復も集めます。ステップの成長のフィールドを差のぶんだけ繰り返し適用し、そのたびに古い要素は保たれます。数の等式が計数を運び、要素の構成可能性もそれとともに運ばれます。その要素は構成可能な反復に属するからです。この単調性により、早い段階で集められたものは、その後も収められたままになります。

    hullStep-≤ : (n n' : ℕ) → n ≤ n' → (z : S)
               → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ fst (hullStep n') ⟩
    hullStep-≤ n n' (k , e) z h =
      subst (λ m → ⟨ z ∈ˢ fst (hullStep m) ⟩) e (Cl.it-up n k (z , zL) h)
      where

反復の単調性は成長のフィールドから従います。前の反復の要素は、それ以降のすべての反復の要素であり、構成可能性も運ばれます。包の符号の深さは再帰で割り当てられます。base の符号の深さは零です。

証人の符号は、その符号のベクトルより一つ深い。その値は、パラメータの値の一歩あとの段階で計算されるからです。

      zL : ⟨ isL z ⟩
      zL = isL-trans {x = fst (hullStep n)} {y = z} h (snd (hullStep n))
    mutual
      depth : Code → ℕ
      depth (base m) = 

証人の構成子は、その子の符号のベクトルの深さに一を加えます。

      depth (wit k ψ cs) = suc (depths cs)

符号のベクトルの深さは、項目の深さの最大値です。ベクトルは、すべての項目が手に入れば使えます。

      depths : {m : ℕ} → Vec Code m → ℕ
      depths [] = 
      depths (c ∷ cs) = max (depth c) (depths cs)

補助は、決定可能な選言の一方が不可能なときの、場合分けの振る舞いを記録します。充足が空なら、計算された値は廃棄の分岐であり、もう一方の分岐が何と言おうと変わりません。

    private
      stuck-r : {A : Type (ℓ-suc ℓ)} (na : A → Empty.⊥)
                (f : A → SL) (g : (A → Empty.⊥) → SL) (s : A ⊎ (A → Empty.⊥))
              → Sum.rec f g s ≡ g na
      stuck-r na f g (inl a) = Empty.rec (na a)

反駁の分岐は、不可能な関数の関数外延性で証明されます。区別するような要素は存在しないからです。

      stuck-r na f g (inr h) = cong g (funExt (λ a → Empty.rec (na a)))

包から合併へ、前半：すべての包の符号の値は、その深さで添字づけられた反復に用意されます。base の符号は始点の要素を名指し、それは零番目の反復にあります。

    mutual
      hullStep-in : (c : Code) → ⟨ fst (val c) ∈ˢ fst (hullStep (depth c)) ⟩
      hullStep-in (base m) = member X m
      hullStep-in (wit k ψ cs) = go (lem (Sat k ψ (vals cs) , squash₁))
        where

証人符号について、その探索が充足可能かどうかで場合分けします。その深さはパラメータ符号ベクトルの深さより一つ大きく、後続段階の等式により、その深さの反復は Φ をもう一度適用した反復と同一視されます。

        n : ℕ
        n = depths cs
        go : (s : Sat k ψ (vals cs) ⊎ (Sat k ψ (vals cs) → Empty.⊥))
           → ⟨ fst (Sum.rec (search k ψ (vals cs)) (λ _ → (∅ , HSH.∅∈Lsetα)) s)
                ∈ˢ fst (hullStep (suc n)) ⟩

探索が充足されていれば、ステップの最小の証人の条項が、次の反復で探索された値を加えます。そのパラメータはベクトルの深さによって手に入ります。探索が充足されなければ、加える証人はなく、ステップは代わりに廃棄値を保ちます。

        go (inl w) = least (hullStep n) k ψ (vals cs) (vals-in cs) w
        go (inr h) = junk (hullStep n)

符号のベクトルのパラメータは、項目の深さの最大値で手に入ります。各項目の値はそれぞれの深さで現れ、単調性がそれを、ベクトルを消費するより後の反復へ運びます。

      vals-in : {m : ℕ} (cs : Vec Code m) → From (hullStep (depths cs)) (vals cs)
      vals-in (c ∷ cs) zero =
        hullStep-≤ (depth c) (max (depth c) (depths cs)) left-≤-max (fst (val c)) (hullStep-in c)
      vals-in (c ∷ cs) (suc i) =
        hullStep-≤ (depths cs) (max (depth c) (depths cs)) right-≤-max

この選択はパラメータベクトルについて再帰します。空ベクトルでは空の符号ベクトルの値ベクトルが条件を満たします。空でない場合は、先頭の包への所属からその符号を得て、尾部の符号を再帰的に得ます。

          (fst (lookup i (vals cs))) (vals-in cs i)
    private
      choose : {k : ℕ} (vs : Vec SL k)
             → ((i : Fin k) → ⟨ fst (lookup i vs) ∈ˢ Hull ⟩)
             → ∥ Σ[ cs ∈ Vec Code k ] (vals cs ≡ vs) ∥₁

帰納のステップは、先頭を包の要素として符号化し、尾を帰納的に符号化します。値の等式は成分ごとに組み立てられ、台の等しさは基礎の集合の等しさへ帰着します。

      choose [] h = ∣ [] , refl ∣₁
      choose (v ∷ vs) h = PT.rec squash₁ (λ { (c , ec) → PT.map
        (λ { (cs , ecs) → (c ∷ cs)
           , cong₂ _∷_ (Σ≡Prop (λ z → snd (z ∈ˢ Lset lam)) ec) ecs })
        (choose vs (λ i → h (suc i))) })

符号ベクトル cs に対し、val-wit は wit k ψ cs の値を探索が返す最小の証人と同一視します。すべての符号の値は包に属するので、探索値も包に属します。

        (HSH.hull-member (fst v) (h zero))
      search-val : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (cs : Vec Code k) (vs : Vec SL k)
                 → vals cs ≡ vs → (w : Sat k ψ vs) → ⟨ fst (search k ψ vs w) ∈ˢ Hull ⟩
      search-val k ψ cs vs e w =
        J (λ vs' e' → (w' : Sat k ψ vs') → ⟨ fst (search k ψ vs' w') ∈ˢ Hull ⟩)

パスの帰納が、パラメータのベクトルの同定に沿って主張を運び、証人の符号は包の内側で判定されます。

          (λ w' → subst (λ z → ⟨ fst z ∈ˢ Hull ⟩) (val-wit k ψ cs w') (inHull (wit k ψ cs)))
          e w

符号 wit 0 ⊥̇ [] には充足する証人がないため、その値は失敗側の分岐を通って ∅ になります。すべての符号の値は包に属するので、廃棄値も包に属します。

      junk∈Hull : ⟨ ∅ ∈ˢ Hull ⟩
      junk∈Hull = subst (λ z → ⟨ fst z ∈ˢ Hull ⟩)
        (stuck-r no (search  ⊥̇ []) (λ _ → (∅ , HSH.∅∈Lsetα)) (lem (Sat  ⊥̇ [] , squash₁)))
        (inHull (wit  ⊥̇ []))
        where

偽を満たす環境はありません。そのような充足の証明を展開すると、空型の要素が得られてしまいます。

        no : Sat  ⊥̇ [] → Empty.⊥
        no = PT.rec Empty.isProp⊥ (λ { (a , h) → Empty.rec* h })

合併から包へ、後半：すべての反復のすべての要素が包の中にあります。反復の添字についての帰納です。基底の場合は始点であり、その要素は包の章によって包の要素です。

    hullStep⊆Hull : (n : ℕ) (z : S) → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ Hull ⟩
    hullStep⊆Hull zero z h = HSH.X⊆M z h
    hullStep⊆Hull (suc n) z h = PT.rec (snd (z ∈ˢ Hull)) read
      (out (hullStep n) (λ z' hz' → HSH.Hull⊆L z' (hullStep⊆Hull n z' hz')) z h)
      where

ステップの場合は、外向きの条項を通して、後者の反復の要素を読みます。それは古い要素であり、帰納の仮定によってすでに包の中にあります。廃棄値でもあり、すでに包の中にあります。あるいは探索された値で、つぎに扱われます。

      read : Reads (hullStep n) z → ⟨ z ∈ˢ Hull ⟩
      read (inl h') = hullStep⊆Hull n z h'
      read (inr (inl e)) = subst (λ t → ⟨ t ∈ˢ Hull ⟩) (sym e) junk∈Hull
      read (inr (inr (k , ψ , vs , w , from , e))) =
        subst (λ t → ⟨ t ∈ˢ Hull ⟩) (sym e)

探索された値は、そのパラメータの符号のベクトルと対応づけられ、各パラメータは帰納の仮定によって包の要素です。だから探索は search-val によって包の中にあり、等式がその所属を z へ運びます。反復の合併が、包を提示する L の要素として名づけられます。

          (PT.rec (snd (fst (search k ψ vs w) ∈ˢ Hull))
            (λ { (cs , ecs) → search-val k ψ cs vs ecs w })
            (choose vs (λ i → hullStep⊆Hull n (fst (lookup i vs)) (from i))))
    hullL : CS.S
    hullL = It.iterUnion

L の要素としての包は、反復の合併であり、その所属の記述は、要素がちょうど包の要素であると言います。前向き：合併の要素はある反復に属し、だから包の中にあります。

    hullL-spec : fst hullL ≡ Hull
    hullL-spec = extensionalV {a = fst hullL} {b = Hull} (λ z → ⇔toPath (fwd z) (bwd z))
      where
      fwd : (z : S) → ⟨ z ∈ˢ fst hullL ⟩ → ⟨ z ∈ˢ Hull ⟩
      fwd z h = PT.rec (snd (z ∈ˢ Hull))

反復の添字は、合併の外向きの読み出しに消費され、要素の構成可能性は合併から運ばれます。合併そのものが、構成によって構成可能なのです。

        (λ { (n , hn) → hullStep⊆Hull n z hn })
        (It.iterUnion-out (z , isL-trans {x = fst hullL} {y = z} h (snd hullL)) h)

後ろ向き：包の要素はある符号に名指され、その値は、符号の深さで添字づけられた反復に現れます。合併の内向きの読み出しがそれを受け入れます。

      bwd : (z : S) → ⟨ z ∈ˢ Hull ⟩ → ⟨ z ∈ˢ fst hullL ⟩
      bwd z h = PT.rec (snd (z ∈ˢ fst hullL))
        (λ { (c , ec) → It.iterUnion-in (depth c) zS
               (subst (λ t → ⟨ t ∈ˢ fst (hullStep (depth c)) ⟩) ec (hullStep-in c)) })
        (HSH.hull-member z h)

名指された要素は台の中へ載せられます。その構成可能性は、包が段階に含まれることから従い、段階の要素としての提示が証明書を供給します。

        where
        zS : CS.S
        zS = z , Lset→isL lam ordλ z (HSH.Hull⊆L z h)

基礎の集合の等しさが、合併の構成可能性を包の上へ運びます。包は L の要素です。本章の前半はこれで完全に清算され、第二のモジュールは、今消費された定義可能なステップを作ります。

ステップは段階の内側で作られ、その定数は段階の対象を名指します。lam の構成可能性は、lam が順序数であることから来ます。

    M-isL : ⟨ isL HS.M ⟩
    M-isL = subst (λ t → ⟨ isL t ⟩) hullL-spec (snd hullL)
  module Build where

階層の順序数は構成可能であり、これが段階を L の内側に固定します。

    λ-isL : ⟨ isL lam ⟩
    λ-isL = isL-ord lam ordλ

A は Lset lam をその構成可能性の証明とともにモデルの要素として表します。充足グラフと段階上の公式の符号化は、これを段階のパラメータとして用います。

    A : CS.S
    A = LsetS lam ordλ

段階の上の充足のグラフは、すべての符号の充足集合を、二つの読み出しとともに一度に供給します。そして段階の上の定義可能性が、論理式の定数を段階の要素として解釈します。

    module SM = SatGraph A using ( pairs; pairs-in; pairs-out; valOf; valOf≡ )
    module DA = DefOf (Lset lam) using ( ι; _⊨ᵐ_; 𝒮M )

空のアルファベットでの符号の集合は、無定数の論理式の符号を集めます。そのような論理式は自由変数をもつことがあります。欠けているのは定数であり、自由変数に値を与えるのは、探索のパラメータ環境です。

    C₀ : CS.S
    C₀ = AllCodes ∅ʟ

段階の内部の整列順序は、モデルの要素として提示されます。最小の証人を比較するための関係です。

    Rel : CS.S
    Rel = relL lam λ-isL ordλ

小さな台の上の狭義の整列順序は、その関係から読まれ、比較は台の要素の上で述べられます。構成可能な順序対の第二成分もまた構成可能であり、これが、のちの名前のパラメータに必要になります。

    wL : SWO SL
    wL = orderAt lam ordλ
    relOf-at : SL → SL → Type (ℓ-suc ℓ)
    relOf-at = relOf wL
    pr-snd-isL : (a b : V ℓ) → ⟨ isL (pr a b) ⟩ → ⟨ isL b ⟩

証明は、順序対を一元集合を通して二度剥がします。対への所属は第二成分を「一元集合と対」の入れ子の中に置き、それぞれの剥離が、推移性によって構成可能性を保ちます。

    pr-snd-isL a b h =
      isL-trans {x = ⁅ a , b ⁆} {y = b} (subst ⟨_⟩ (sym (pair-spec a b b)) ∣ inr refl ∣₁)
        (isL-trans {x = pr a b} {y = ⁅ a , b ⁆}
          (subst ⟨_⟩ (sym (pair-spec ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a , b ⁆)) ∣ inr refl ∣₁) h)

数項は台の要素として提示されます。有限の順序数とその構成可能性であり、証人の論理式のキーの条項がこれを量化します。

    nn : ℕ → CS.S
    nn k = # k , numL k

定数のアルファベットは空なので、段階の台への解釈 ε′ は一意です。これにより、何も選択せずに無定数公式を段階の言語へ付け替えられます。

    ε′ : ⊥* {ℓ} → ⟪ Lset lam ⟫
    ε′ = Empty.rec*
    sat-bridge : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) (δ : SL ^ k)
               → (δ ⊨₀ χ) ≡ (δ DA.⊨ᵐ mapFo ε′ χ)
    sat-bridge k χ δ =

この橋は合成です。空のアルファベットの環境は、解釈すべきものがないため、自明に一致します。そして改名の定理が、改名された論理式の外側の充足と、段階の内側の充足とを同一視します。

        cong (λ κ → FOL.Semantics.At._⊨_ DA.𝒮M (⊥* {ℓ}) κ δ χ)
          (funExt (λ b → Empty.rec* b))
      ∙ sym (⊨-map DA.𝒮M ε′ DA.ι χ δ)
    opaque
      keyOf : (k : ℕ) → Formula (⊥* {ℓ}) k → CS.S

無定数の論理式の、段階でのキーとは、改名された形の、段階の符号の集合でのキーです。一度だけ名づけられ、以後の主張はその構成を開かずに参照できます。

      keyOf k χ = keyS A (mapFo ε′ χ)

そのキーは、段階での符号の集合に属します。改名された論理式の符号は、段階のアルファベットの上の符号であり、符号の集合はそれらをすべて含みます。

      keyOf∈ : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) → ⟨ keyOf k χ CS.∈ˢ AllCodes A ⟩
      keyOf∈ k χ = key∈AllCodes A (mapFo ε′ χ)

keyOf は不透明ですが、補題 keyOf≡ が keyS A (mapFo ε′ χ) との正確な等式を公開します。以後の証明は、封印された定義を展開せずにこの等式を使えます。

      keyOf≡ : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) → keyOf k χ ≡ keyS A (mapFo ε′ χ)
      keyOf≡ k χ = refl

封印されたキーの基礎の集合が計算されます。それは、アリティの数項と、改名された論理式の符号との順序対です。証明は、論理式の二つの改名を合成します。空のアルファベットを経て、段階の埋め込みへ続くものです。改名の定理が、結果を極限段階が記録する符号と同一視します。

      keyOf-fst : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
                → fst (keyOf k χ) ≡ pr (# k) (fst (limitCode χ))
      keyOf-fst k χ = cong (pr (# k)) (cong VCode.⌜_⌝
        ( mapFo-comp ε′ ⟪ Lset lam ⟫↪ χ
        ∙ cong (λ f → mapFo f χ) (funExt (λ b → Empty.rec* b)) ))

各無パラメータ論理式に対し、Tof は充足のグラフがその論理式の封印されたキーで選ぶ充足集合です。この固定した集合が、段階全体でその論理式の充足関係を表します。

    Tof : (k : ℕ) → Formula (⊥* {ℓ}) k → CS.S
    Tof k χ = SM.valOf (keyOf k χ) (keyOf∈ k χ)

キーとその充足集合との順序対は、充足のグラフに属します。さらに、キーと同じ基礎集合をもつ台の要素は同じ充足集合を選びます。構成可能性の証明は命題なので、基礎集合の等しさが台での等しさへ持ち上がり、したがって選ばれた値も等しくなります。

    Tof-pair : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
             → ⟨ pr (fst (keyOf k χ)) (fst (Tof k χ)) ∈ˢ fst SM.pairs ⟩
    Tof-pair k χ = SM.pairs-in (keyOf k χ) (keyOf∈ k χ)
    valOf-same : (x : CS.S) (m : ⟨ x CS.∈ˢ AllCodes A ⟩) (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
               → fst x ≡ fst (keyOf k χ) → SM.valOf x m ≡ Tof k χ