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

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

M : S
M = Mʟ .fst

π 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 (Mʟ .snd)

持ち上げ 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∈ = 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 → (y .fst ∈ˢ M) ⊓ ((x .fst ∈ˢ M) ⊓ (y .fst ∈ˢ x .fst)))
          (λ y x z h → h) (λ y x z h → h)

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

R : CS.S
R = Membership.rel

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

R-in : (y x : CS.S) → ⟨ y .fst ∈ˢ M ⟩ → ⟨ x .fst ∈ˢ M ⟩ → ⟨ y .fst ∈ˢ x .fst ⟩
     → 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
      → ⟨ y .fst ∈ˢ M ⟩ × ⟨ x .fst ∈ˢ M ⟩ × ⟨ y .fst ∈ˢ x .fst ⟩
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 = 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 → v .fst ≡ 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 = v .fst} {b = C.π x} (λ w → ⇔toPath (fwd w) (bwd w))
    where
    xS : CS.S
    xS = x , xL

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

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

源の証人は関係の事実 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 (y .fst) y∈x y∈M)
        where
        y∈M : ⟨ y .fst ∈ˢ M ⟩

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

        y∈M = R-out y xS ry .fst
        y∈x : ⟨ y .fst ∈ˢ x ⟩
        y∈x = R-out y xS ry .snd .snd
        e : C.π (y .fst) ≡ w
        e = sym (IH (y .fst) y∈x (y .snd) 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 ∈ˢ v .fst ⟩
    bwd w w∈ = rec₁ ((w ∈ˢ v .fst) .snd) read (π-mem-out x w w∈)
      where
      read : Σ[ y ∶ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) → ⟨ w ∈ˢ v .fst ⟩
      read (y , (y∈x , y∈M , e)) = rec₁ ((w ∈ˢ v .fst) .snd) 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 ∈ˢ v .fst ⟩
        inner (u , fu) =
          subst (λ t → ⟨ t ∈ˢ v .fst ⟩) (eu ∙ e) (val u .snd ∣ yS , (ry , fu) ∣₁)
          where
          eu : u .fst ≡ C.π y

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

          eu = IH y y∈x (yS .snd) 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) → ⟨ x .fst ∈ˢ M ⟩ → (v : CS.S)
          → Complete F R x → ValueIs F R x v → v .fst ≡ C.π (x .fst)
value-val F hc x = value-val′ F hc (x .fst) (x .snd)
piFo-val : (q : CS.S) → ⟨ q .fst ∈ˢ M ⟩ → (v : CS.S) → ⟨ (v ∷ q ∷ []) ⊨ piFo ⟩
         → v .fst ≡ C.π (q .fst)

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

piFo-val q mq v h = rec₁ (setIsSet (v .fst) (C.π (q .fst)))
  (λ { (F , (hc , (hm , hv))) → value-val F hc q mq v hm hv })
  (piFo-out v q h)

module Cut (K : CS.S) where

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

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

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

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

  cut-out : (y : CS.S) → ⟨ y CS.∈ˢ cut ⟩ → ⟨ y .fst ∈ˢ M ⟩ × ⟨ y .fst ∈ˢ K .fst ⟩
  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Σ ((isL (C.π q)) .snd)
  λ qL → isPropΠ λ mq → (((C.π q , qL) ∷ up q mq ∷ []) ⊨ piFo) .snd

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

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

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.π (y .fst) , IH (y .fst) (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 (y .fst) my (Sl.cut-out y hy .snd) .snd my)

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

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

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

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

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 ⟩ × (v .fst ≡ C.π (x .fst))
Tab-pair = T.pair-out

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

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 = x .fst} {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.π (y .fst)) ∈ˢ Tab .fst ⟩) refl (Tab-in y' hy') ∣₁
  where
  ro = R-out y x ry
  y' : CS.S

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

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

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

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

  bwd : Src Tab R x w → ⟨ w .fst ∈ˢ v .fst ⟩
  bwd = rec₁ ((w .fst ∈ˢ v .fst) .snd) (λ { (y , (ry , ty)) →
    subst2 (λ s t → ⟨ s ∈ˢ t ⟩) (sym (Tab-pair y w ty .snd)) (sym ev)
      (C.π∈-fwd (x .fst) (y .fst) (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

  mx : ⟨ x .fst ∈ˢ 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 )

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

      ; 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)) ∥₁

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

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

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

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

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

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

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

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

        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-isL : ⟨ isL (C.π q) ⟩
  πq-isL = subst (λ t → ⟨ isL t ⟩) val≡π (Vq.table .snd)

  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δ = 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 = rec₁ ((isL (C.π y)) .snd)

証明 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 })
  (Mʟ .snd)
πX-isL : (x : S) → ⟨ x ∈ˢ C.πX ⟩ → ⟨ isL x ⟩
πX-isL x x∈πX = rec₁ ((isL x) .snd)

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

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

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

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; searchPredicate; Sat; Hull; val-wit
        ; satDecision )
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) → ⟨ (lookup i vs) .fst ∈ˢ Z .fst ⟩
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 ≡ (search k ψ vs w) .fst))
Reads : CS.S → S → Type (ℓ-suc ℓ)
Reads Z z = ⟨ z ∈ˢ Z .fst ⟩ ⊎ ((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 ∈ˢ Z .fst ⟩ → ⟨ z ∈ˢ (Φ Z) .fst ⟩
    junk    : (Z : CS.S) → ⟨ ∅ ∈ˢ (Φ Z) .fst ⟩
    least   : (Z : CS.S) (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec SL k)
            → From Z vs → (w : Sat k ψ vs) → ⟨ (search k ψ vs w) .fst ∈ˢ (Φ Z) .fst ⟩