定義可能冪集合の Δ₀ 記述

module _ {j : ℕ} (e N0 z : Fin j) (δ : Vec S j) (q0 : (lookup N0 δ) .fst ≡ # ) where

private
  E = (lookup e δ) .fst
  Z = (lookup z δ) .fst

単項の節の読みから、符号化された集合が値の正準な単項環境と等しいことが得られる。順方向では、符号化された集合のすべての要素が、数項ゼロと値の順序対であり、対のアトムの妥当性に沿って運ばれる。

singleOf-out : ⟨ δ ⊨ singleOf e N0 z ⟩ → E ≡ envOne Z
singleOf-out (hall , hex) = extensionalV (λ y → ⇔toPath (fwd y) (bwd y))
  where
  fwd : (y : V ℓ) → ⟨ y ∈ E ⟩ → ⟨ y ∈ envOne Z ⟩
  fwd y hy = ∣ lift zero , sym (pr-out i0 (sh  N0) (sh  z) (down (lookup e δ) y hy ∷ δ) (hall (down (lookup e δ) y hy) hy)

逆向きの包含では、正準な一項環境の要素から始める。存在側の連言肢が符号化された集合のある要素を与え、その対の等式と既知のタグ 0 によって、その要素を最初に与えた要素と同一視できる。この等式に沿って所属を移送すれば、元の要素が符号化された集合に属することが得られる。

                               ∙ cong (λ a → pr a Z) q0) ∣₁
  bwd : (y : V ℓ) → ⟨ y ∈ envOne Z ⟩ → ⟨ y ∈ E ⟩
  bwd y = rec₁ ((y ∈ E) .snd)
    (λ { (lift zero , qy) → rec₁ ((y ∈ E) .snd)
      (λ { (y' , (y'∈ , hy')) →

envOne Z の要素は順序対 pr (# 0) Z である。したがってタグの枠を数項 0 に書き換えると、この要素は singleOf が要求する順序対と同一視される。要素そのものが Z と同一視されるわけではない。

        subst (λ u → ⟨ u ∈ E ⟩)
          (pr-out i0 (sh  N0) (sh  z) (y' ∷ δ) hy' ∙ cong (λ a → pr a Z) q0 ∙ qy) y'∈ })
      hex
       ; (lift (suc ()) , _) })

逆に、符号化された集合が正準な一項環境に等しいと仮定する。その環境の唯一の添字は 0 なので、各要素は必要な順序対の形をもち、残る後者添字の場合は不可能性で閉じる。正準な 0 番の項目が有界存在の証人を与え、仮定した等式に沿う移送がその所属を与える。

singleOf-in : E ≡ envOne Z → ⟨ δ ⊨ singleOf e N0 z ⟩
singleOf-in q =
    (λ y hy → pr-in i0 (sh  N0) (sh  z) (y ∷ δ)
       (rec₁ (setIsSet (y .fst) (pr ((lookup N0 δ) .fst) Z))
         (λ { (lift zero , qy) → sym qy ∙ cong (λ a → pr a Z) (sym q0) ; (lift (suc ()) , _) })

要素に名前が与えられ、その所属が運ばれる。そして存在の証人は、ゼロの数項と値の対を、タグの等式に逆らってまとめる。

         (subst (λ u → ⟨ y .fst ∈ u ⟩) q hy)))
  , ∣ yS , ( subst (λ u → ⟨ pr (# ) Z ∈ u ⟩) (sym q) ∣ lift zero , refl ∣₁
           , pr-in i0 (sh  N0) (sh  z) (yS ∷ δ) (cong (λ a → pr a Z) (sym q0)) ) ∣₁
  where
  yS : S

名前のついた要素は、数項ゼロと値の対の、符号化された集合の中での提示である。

  yS = down (lookup e δ) (pr (# ) Z) (subst (λ u → ⟨ pr (# ) Z ∈ u ⟩) (sym q) ∣ lift zero , refl ∣₁)

module _ {j : ℕ} (x w y N0 : Fin j) (δ : Vec S j) (q0 : (lookup N0 δ) .fst ≡ # ) where

private
  X = (lookup x δ) .fst
  Wv = (lookup w δ) .fst
  Y = (lookup y δ) .fst

Y は構成可能集合なので、一項環境が Y に属するという証明から、その環境を表す台の要素を得られる。この表示があるため、definesB の有界存在量化子は Y の実際の要素を証人にできる。

  YS = lookup y δ

単項の節の存在量化を読むと、それが、正準な単項環境の値の中での所属に変換される。証人は値の要素であり、単項の節が、符号化された項目をその索引の正準な環境と同一視する。

  one-out : (z : S) → ⟨ (z ∷ δ) ⊨ ∃̇∈ (var (sh  y)) (singleOf i0 (sh  N0) i1) ⟩ → ⟨ envOne (z .fst) ∈ Y ⟩
  one-out z = rec₁ ((envOne (z .fst) ∈ Y) .snd)
    (λ { (e , (e∈ , he)) → subst (λ u → ⟨ u ∈ Y ⟩) (singleOf-out i0 (sh  N0) i1 (e ∷ z ∷ δ) q0 he) e∈ })

存在量化の埋めは逆である。正準な単項環境は値の中で提示され、単項の節は延長された環境のもとで埋められる。

  one-in : (z : S) → ⟨ envOne (z .fst) ∈ Y ⟩ → ⟨ (z ∷ δ) ⊨ ∃̇∈ (var (sh  y)) (singleOf i0 (sh  N0) i1) ⟩
  one-in z h = ∣ down YS (envOne (z .fst)) h , (h , singleOf-in i0 (sh  N0) i1 (down YS (envOne (z .fst)) h ∷ z ∷ δ) q0 refl) ∣₁

定義可能部分集合の節を読むと、切り出し関係の二つの方向が得られる。第一の連言肢は、X の各要素が Wv に属し、その一項環境が Y に属することを与える。第二の連言肢は、この二つの事実から X への所属を戻す。

definesB-out : ⟨ δ ⊨ definesB x w y N0 ⟩ → Cuts X Wv Y
definesB-out (h1 , h2) = (λ z hz → h1 z hz .fst , one-out z (h1 z hz .snd)) , (λ z hw he → h2 z hw (one-in z he))

逆に、Cuts X Wv Y の二つの各点的な方向から、対象言語における定義可能部分集合の節の二つの連言肢を満たせる。上の内部変換は、有界な一項環境の証人と、正準な一項環境が Y に属することとの間を正確に行き来する。

definesB-in : Cuts X Wv Y → ⟨ δ ⊨ definesB x w y N0 ⟩
definesB-in (o , i) = (λ z hz → o z hz .fst , one-in z (o z hz .snd)) , (λ z hw he → i z hw (one-out z he))

module Read {m : ℕ} (v w T C : Fin m) (N : Fin  → Fin m) (γ : Vec S m) (tg : Tags γ N) where

private
  Vv = (lookup v γ) .fst
  Wv = (lookup w γ) .fst
  Tv = (lookup T γ) .fst

コードの定義域の底の集合と、タグ一の背後にある数項が名付けられる。所属の節が選ぶのは、タグ一と第二成分の対の形のコードだからである。

  Cv = (lookup C γ) .fst
  N1v = (lookup (N f1) γ) .fst

所属の節の読みは、提案された値の各要素に対して、切り詰められた記録を与える。定義域の中の、タグ一とある成分の対として分解される符号、その符号をある値と対にする表の項目、そしてその要素と値の間の切り出しの関係である。記録は切り詰めのもとで存在し、符号や値は選ばれない。

mem-out : ⟨ γ ⊨ memAt v w T C N ⟩ → (x : S) → ⟨ x .fst ∈ Vv ⟩
        → ∥ Σ[ c ∶ S ] Σ[ p ∶ S ] Σ[ y ∶ S ]
            (⟨ c .fst ∈ Cv ⟩ × ((c .fst ≡ pr (# ) (p .fst)) × (⟨ pr (c .fst) (y .fst) ∈ Tv ⟩ × Cuts (x .fst) Wv (y .fst)))) ∥₁
mem-out h x x∈ = rec₁ squash₁
  (λ { (c , (c∈ , hc)) → rec₁ squash₁

所属の節を読むには、まず候補の符号領域から鍵の形をした要素 c を取り出し、次に c と値 y を対にする表の項目を取り出す。対の仕様が符号化された第二成分を結果に現れる意味論的な等式へ変え、タグの等式が形式的なタグを実際の数項 1 へ書き換える。

    (λ { (p , s , (ec , he)) → rec₁ squash₁
      (λ { (e , (e∈ , hy)) → map₁
        (λ { (y , s' , (ee , hd)) →
          c , p , y , ( c∈ , ( ec ∙ cong (λ a → pr a (p .fst)) (tg f1)
                      , ( subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈

最も内側の存在は、definesB-out を通して読まれ、要素と表の項目の値 y の間の切り出しの関係を産み出す。

                        , definesB-out i6 (sh  w) i0 (sh  (N f0)) (y ∷ s' ∷ e ∷ p ∷ s ∷ c ∷ x ∷ γ) (tg f0) hd ) ) ) })
        (sndEx-out i0 i3 (definesB i6 (sh  w) i0 (sh  (N f0))) (e ∷ p ∷ s ∷ c ∷ x ∷ γ) hy) })
      he })
    (sndEx-out i0 (sh  (N f1)) (∃̇∈ (var (sh  T)) (sndEx i0 i3 (definesB i6 (sh  w) i0 (sh  (N f0))))) (c ∷ x ∷ γ) hc) })
  (h x x∈)

所属の節の埋めは逆の構成である。各要素に対して切り詰められた記録を産み出す関数を受け取り、節の充足を組み立てる。

mem-in : ((x : S) → ⟨ x .fst ∈ Vv ⟩
          → ∥ Σ[ c ∶ S ] Σ[ p ∶ S ] Σ[ y ∶ S ]
              (⟨ c .fst ∈ Cv ⟩ × ((c .fst ≡ pr (# ) (p .fst)) × (⟨ pr (c .fst) (y .fst) ∈ Tv ⟩ × Cuts (x .fst) Wv (y .fst)))) ∥₁)
       → ⟨ γ ⊨ memAt v w T C N ⟩
mem-in g x x∈ = map₁

逆に、候補出力の各要素に対して、このような切り詰められた意味論的記録が与えられているとする。等式 c = pr (# 1) p は有界論理式が要求するアリティ一の形を与え、pr(c,y) の表への所属は表の項目の有界な表示を与える。

  (λ { (c , p , y , (c∈ , (ec , (e∈ , cuts)))) →
    let ec' : c .fst ≡ pr N1v (p .fst)
        ec' = ec ∙ cong (λ a → pr a (p .fst)) (sym (tg f1))
        δ4 = p ∷ container c (lookup (N f1) γ) p ec' .fst ∷ c ∷ x ∷ γ
        eS = down (lookup T γ) (pr (c .fst) (y .fst)) e∈

続いて七つの枠からなる環境を組み立て、definesB-in によって切り出し関係を定義可能部分集合の節へ戻す。

        δ7 = y ∷ container eS c y refl .fst ∷ eS ∷ δ4
    in c , ( c∈ , fillSnd i0 (c ∷ x ∷ γ) (lookup (N f1) γ) p ec'
               (∃̇∈ (var (sh  T)) (sndEx i0 i3 (definesB i6 (sh  w) i0 (sh  (N f0)))))
               ∣ eS , ( e∈ , fillSnd i0 (eS ∷ δ4) c y refl (definesB i6 (sh  w) i0 (sh  (N f0)))
                            (definesB-in i6 (sh  w) i0 (sh  (N f0)) δ7 (tg f0) cuts) i3 refl ) ∣₁

鍵の形、表の項目、切り出し条件を符号化した後、外側の有界量化子が、この切り詰められたまとまりを候補出力の元の要素に適用する。したがって、この意味論的記録から所属の節全体の充足を再構成できる。

               (sh  (N f1)) refl ) })
  (g x x∈)

覆いの節の読みは、タグ一と p の対として分解される符号 c を取り、単に、c における表の値 y と、y によって切り出される集合 x を与える。

all-out : ⟨ γ ⊨ allAt v w T C N ⟩ → (c p : S) → ⟨ c .fst ∈ Cv ⟩ → c .fst ≡ pr (# ) (p .fst)
        → ∥ Σ[ y ∶ S ] Σ[ x ∶ S ] (⟨ pr (c .fst) (y .fst) ∈ Tv ⟩ × (⟨ x .fst ∈ Vv ⟩ × Cuts (x .fst) Wv (y .fst))) ∥₁
all-out h c p c∈ ec = rec₁ squash₁
  (λ { (e , (e∈ , hy)) → rec₁ squash₁
    (λ { (y , s' , (ee , hx)) → map₁

証明は、表の項目と三つの枠の存在量化を消去する。そして定義可能な部分集合の節の読みが、要素と表の値の間の切り出しの関係を産み出す。

      (λ { (x , (x∈ , hd)) →
        y , x , ( subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈
                , ( x∈ , definesB-out i0 (sh  w) i1 (sh  (N f0)) (x ∷ y ∷ s' ∷ e ∷ δ3) (tg f0) hd ) ) })
      hx })
    (sndEx-out i0 i3 (∃̇∈ (var (sh  v)) (definesB i0 (sh  w) i1 (sh  (N f0)))) (e ∷ δ3) hy) })

逆向きの構成では、符号領域の要素 c を固定し、それが pr (# 1) p として表される場合を調べる。意味論的な覆いの仮定は、命題的切り詰めの下で表の値と、その値が切り出す部分集合を与える。これらの証人が、その表示に対する有界な結論を満たす。

  (useSnd i0 (c ∷ γ) (lookup (N f1) γ) p ec'
    (∃̇∈ (var (sh  T)) (sndEx i0 i3 (∃̇∈ (var (sh  v)) (definesB i0 (sh  w) i1 (sh  (N f0))))))
    (sh  (N f1)) refl (h c c∈))
  where
  ec' : c .fst ≡ pr N1v (p .fst)

形式的なタグを使う等式は、Tags によって必要なアリティ一の等式へ変換される。補助的な容器は、成分と符号を有界量化子の範囲内に保つだけであり、意味論的な証人に選択や一意性を加えるものではない。

  ec' = ec ∙ cong (λ a → pr a (p .fst)) (sym (tg f1))
  δ3 : Vec S ( + m)
  δ3 = p ∷ container c (lookup (N f1) γ) p ec' .fst ∷ c ∷ γ

したがって覆いの節を満たす際には、候補の符号領域の要素のうち、アリティ一の鍵の形で表示されたものをすべて扱う。その各表示に対し、意味論的な仮定が命題的切り詰めの下で、表の値、それが切り出す候補出力の要素、および両者の所属を与える。後で satAt を加えるまでは、これらが実際の論理式の鍵であるとは主張しない。

all-in : ((c p : S) → ⟨ c .fst ∈ Cv ⟩ → c .fst ≡ pr (# ) (p .fst)
          → ∥ Σ[ y ∶ S ] Σ[ x ∶ S ] (⟨ pr (c .fst) (y .fst) ∈ Tv ⟩ × (⟨ x .fst ∈ Vv ⟩ × Cuts (x .fst) Wv (y .fst))) ∥₁)
       → ⟨ γ ⊨ allAt v w T C N ⟩
all-in g c c∈ = sndAll-in' (λ p s s∈ p∈ ec →
  map₁ (λ { (y , x , (e∈ , (x∈ , cuts))) →

最も内側の有界存在量化子には、切り出された集合 x と、x が値の集合に属する証明、さらに definesB で符号化したばかりの Cuts の証拠が渡される。これで逆向きの翻訳が完成する。表の項目とそれが切り出す部分集合についての意味論的な証人から所属の条項の充足が得られ、存在データはすべて命題的切り詰めの中に保たれる。

    let eS = down (lookup T γ) (pr (c .fst) (y .fst)) e∈
        δ6 = y ∷ container eS c y refl .fst ∷ eS ∷ p ∷ s ∷ c ∷ γ
    in eS , ( e∈ , fillSnd i0 (eS ∷ p ∷ s ∷ c ∷ γ) c y refl (∃̇∈ (var (sh  v)) (definesB i0 (sh  w) i1 (sh  (N f0))))
                     ∣ x , (x∈ , definesB-in i0 (sh  w) i1 (sh  (N f0)) (x ∷ δ6) (tg f0) cuts) ∣₁ i3 refl ) })
    (g c p c∈ (ec ∙ cong (λ a → pr a (p .fst)) (tg f1))))

覆いの条項にも同じ二段の存在選択がある。充足関係表の値と、その値が作業集合から切り出す部分集合である。両者を合わせた外向きの読み出しに名前を付けることで、次の議論では、この単に存在する一対の証人を一つの命題値のまとまりとして扱える。

  where
  sndAll-in' = sndAll-in i0 (sh  (N f1))
    (∃̇∈ (var (sh  T)) (sndEx i0 i3 (∃̇∈ (var (sh  v)) (definesB i0 (sh  w) i1 (sh  (N f0)))))) (c ∷ γ)

module DefRead {m : ℕ} (v w T C E : Fin m) (N : Fin  → Fin m) (γ : Vec S m) (W : S)
  (qw : (lookup w γ) .fst ≡ W .fst) (tg : Tags γ N) (hs : ⟨ γ ⊨ satAt T w C E N ⟩) where

open Alphabet W
open Match W

先に得た二つの読み出しが必要な橋を与える。SatRead は、記述された符号領域と表を、W 上の実際の符号と充足値に対応させる。Read は defAt を二つの意味論的な切り出し条件として読む。その上で DefOf (W .fst) が、復号されたアリティ一の各論理式を W の一つの部分集合として解釈する。

private module SR = SatRead T w C E N γ W qw tg hs
private module RD = Read v w T C N γ tg
private module DA = DefOf (W .fst)
private
  Vv = (lookup v γ) .fst
  Wv = (lookup w γ) .fst

表の枠と符号の枠が表す基礎の集合を、それぞれ Tv と Cv と書く。satAt の役割はまさに、これら記述された集合への所属と、実際の充足関係表および符号領域への所属とを相互に変換できるようにすることである。

  Tv = (lookup T γ) .fst
  Cv = (lookup C γ) .fst

対応 toS は、アルファベットの上の論理式のすべての定数を、S の対応する定数へ付け替え、周囲の充足で判定できる論理式を作る。

  toS : Formula Ab  → Formula S 
  toS = mapFo (asConst W)

表の値の補題は、論理式のキーで記録された値が、付け替えられた論理式の明示的な充足集合に等しいと言う。証明は、表の外向きの射影と、一様な充足の値の同定とを合成する。

  valOf : (ψ : Formula Ab ) (c y : S) → c .fst ≡ (keyS W ψ) .fst → ⟨ pr (c .fst) (y .fst) ∈ Tv ⟩
        → y .fst ≡ (Sat W (toS ψ)) .fst
  valOf ψ c y qc h = SR.T-out c y h .snd ∙ cong (λ p → p .fst) (val-at W W ψ c (SR.T-out c y h .fst) qc)

中心となる橋は論理式を一つずつ扱う。Cuts が、x は W の要素のうち、その一変数環境が ψ の充足集合に属するものからちょうど成ると述べるなら、x は特定の定義可能部分集合 DA.defSet ψ に等しくなる。この等式は、所属の両方向を示して外延性から得られる。

  cut≡ : (ψ : Formula Ab ) (x : S) → Cuts (x .fst) Wv ((Sat W (toS ψ)) .fst) → DA.defSet ψ ≡ x .fst
  cut≡ ψ x (o , i) = extensionalV (λ z → ⇔toPath (fwd z) (bwd z))
    where
    fwd : (z : V ℓ) → ⟨ z ∈ DA.defSet ψ ⟩ → ⟨ z ∈ x .fst ⟩
    fwd z = rec₁ ((z ∈ x .fst) .snd)

第一の方向では、DA.defSet ψ への所属から、命題的切り詰めの下で W の要素の表示が得られる。充足の橋によって、その表示の一変数環境は ψ の充足集合に入り、Cuts の内向きの半分が、表示された集合を x に入れる。

      (λ { ((q , hq) , e) →
        i (down W z (subst (λ u → ⟨ u ∈ W .fst ⟩) e (ι∈ q)))
          (subst (λ u → ⟨ z ∈ u ⟩) (sym qw) (subst (λ u → ⟨ u ∈ W .fst ⟩) e (ι∈ q)))
          (subst (λ u → ⟨ envOne u ∈ (Sat W (toS ψ)) .fst ⟩) e
            (subst ⟨_⟩ (defSet-Sat W ψ q) ∣ (q , hq) , refl ∣₁)) })

もう一方の方向では z ∈ x から始める。Cuts の外向きの半分は、z ∈ W と、その一変数環境が充足集合に属することの両方を与える。第一の事実は ∈-asFiber によって、W の表示の実際の添字と、そこから z へ戻るパスに変換される。

    bwd : (z : V ℓ) → ⟨ z ∈ x .fst ⟩ → ⟨ z ∈ DA.defSet ψ ⟩
    bwd z hz =
      let zS = down x z hz
          zW = subst (λ u → ⟨ z ∈ u ⟩) qw (o zS hz .fst)
          fib = ∈-asFiber {a = z} {b = W .fst} zW

その表示のパスに沿って環境の所属を移し、defSet-Sat を逆向きに適用する。これにより表示が DA.defSet ψ に属することが分かり、同じパスに沿って戻せば z ∈ DA.defSet ψ が得られて、外延的な等式が完成する。

      in subst (λ u → ⟨ u ∈ DA.defSet ψ ⟩) (fib .snd)
           (subst ⟨_⟩ (sym (defSet-Sat W ψ (fib .fst)))
             (subst (λ u → ⟨ envOne u ∈ (Sat W (toS ψ)) .fst ⟩) (sym (fib .snd)) (o zS hz .snd)))

逆に、DA.defSet ψ がすでに x に等しいとする。Cuts を再構成するには、x の要素を DA.defSet ψ の要素へ書き換え、定義可能部分集合への所属を展開する。すると、その集合を W の要素として表すデータと、対応する一変数環境が充足集合に属する証明が同時に得られる。

  cuts-of : (ψ : Formula Ab ) (x : S) → DA.defSet ψ ≡ x .fst → Cuts (x .fst) Wv ((Sat W (toS ψ)) .fst)
  cuts-of ψ x e = o , i
    where
    o : (z : S) → ⟨ z .fst ∈ x .fst ⟩ → ⟨ z .fst ∈ Wv ⟩ × ⟨ envOne (z .fst) ∈ (Sat W (toS ψ)) .fst ⟩
    o z hz = rec₁ (isProp× ((z .fst ∈ Wv) .snd) ((envOne (z .fst) ∈ (Sat W (toS ψ)) .fst) .snd))

この所属を展開すると、W の中の表示と、defSet-Sat を通じて、その一変数環境が必要な充足集合に属することが得られる。表示と元の要素との等式に沿って、二つの結論をどちらも x のその要素へ戻す。

      (λ { ((q , hq) , eq) →
          subst (λ u → ⟨ z .fst ∈ u ⟩) (sym qw) (subst (λ u → ⟨ u ∈ W .fst ⟩) eq (ι∈ q))
        , subst (λ u → ⟨ envOne u ∈ (Sat W (toS ψ)) .fst ⟩) eq (subst ⟨_⟩ (defSet-Sat W ψ q) ∣ (q , hq) , refl ∣₁) })
      (subst (λ u → ⟨ z .fst ∈ u ⟩) (sym e) hz)
    i : (z : S) → ⟨ z .fst ∈ Wv ⟩ → ⟨ envOne (z .fst) ∈ (Sat W (toS ψ)) .fst ⟩ → ⟨ z .fst ∈ x .fst ⟩

Cuts の内向きの半分では、W の表示された要素から始め、その一変数環境が ψ を満たすと仮定する。充足の橋がこれを DA.defSet ψ への所属に変え、仮定した等式 DA.defSet ψ = x .fst がその要素を x に入れる。

    i z hw he =
      let fib = ∈-asFiber {a = z .fst} {b = W .fst} (subst (λ u → ⟨ z .fst ∈ u ⟩) qw hw)
      in subst (λ u → ⟨ z .fst ∈ u ⟩) e
           (subst (λ u → ⟨ u ∈ DA.defSet ψ ⟩) (fib .snd)
             (subst ⟨_⟩ (sym (defSet-Sat W ψ (fib .fst)))

最後の輸送は、選んだ要素の表示とその基礎の集合を揃えるだけである。したがって cut≡ と cuts-of を合わせると、ψ に対する Cuts 述語は、一つの定義可能部分集合 DA.defSet ψ との等しさに対応する。どちらの向きも定義論理式の一意性を主張しない。

               (subst (λ u → ⟨ envOne u ∈ (Sat W (toS ψ)) .fst ⟩) (sym (fib .snd)) he)))

これで健全性を正確に述べられる。作業集合の枠が W と同一視され、数を表すタグが正しく、satAt が符号集合と充足関係表を正しく保証しているという前提の下で、defAt の充足は値の枠をちょうど 𝒟ₒ (W .fst) に定める。ここで 𝒟ₒ が集めるのは、W の要素をパラメータに使える一階論理式で定義される W の部分集合であり、完全な内部冪集合ではない。

def-sound : ⟨ γ ⊨ defAt v w T C N ⟩ → Vv ≡ 𝒟ₒ (W .fst)
def-sound hd = extensionalV (λ x → ⇔toPath (fwd x) (bwd x))
  where
  hm = defAt-out v w T C N γ hd .fst
  ha = defAt-out v w T C N γ hd .snd

順方向の包含では、所属の節が命題的切り詰めの下で、鍵の形をした符号、充足関係表の項目、その項目が切り出す部分集合を記述する条件を与える。satAt が候補の符号領域を実際のものと対応させた後、decodeAll は、符号が必要な第二成分をもつアリティ一の論理式が単に存在することだけを与える。続いて表の値の補題が、その項目の値をこの論理式の充足集合と同一視する。

  fwd : (x : V ℓ) → ⟨ x ∈ Vv ⟩ → ⟨ x ∈ 𝒟ₒ (W .fst) ⟩
  fwd x hx = rec₁ ((x ∈ 𝒟ₒ (W .fst)) .snd)
    (λ { (c , p , y , (c∈ , (ec , (e∈ , cuts)))) → rec₁ ((x ∈ 𝒟ₒ (W .fst)) .snd)
      (λ { (ψ , qp) →
        𝒟ₒ-intro (W .fst) x ∣ ψ , cut≡ ψ xS

Cuts の事実が、表の値の同定に沿って、復号された論理式の充足集合の中へ運ばれ、定義可能冪集合の導入が、切り出された集合を 𝒟ₒ の中に置く。切り詰められた論理式の復号は、命題値の導入の中で消費される。

          (subst (λ u → Cuts x Wv u) (valOf ψ c y (ec ∙ cong (pr (# )) qp) e∈) cuts) ∣₁ })
      (decodeAll c (SR.C-out c c∈)  (p .fst) ec) })
    (RD.mem-out hm xS hx)
    where
    xS : S

値の枠は、所属の条項の外向きの読み出しのために、台の要素として提示される。

    xS = down (lookup v γ) x hx

逆向きの包含では、𝒟ₒ (W .fst) への所属から得られるのは、命題的に切り詰められた論理式 ψ と等式 DA.defSet ψ = x だけである。所属命題への消去の内部で、defAt の覆いの側が、この一時的な証人 ψ から作った鍵に対し、表の値と、値の枠に属する集合 x' を与える。

  bwd : (x : V ℓ) → ⟨ x ∈ 𝒟ₒ (W .fst) ⟩ → ⟨ x ∈ Vv ⟩
  bwd x hx = rec₁ ((x ∈ Vv) .snd)
    (λ { (ψ , e) → rec₁ ((x ∈ Vv) .snd)
      (λ { (y , x' , (e∈ , (x'∈ , cuts))) →
        subst (λ u → ⟨ u ∈ Vv ⟩)

切り出しの等式が、表の値の同定に沿って運ばれて、切り出された集合の基礎の集合を復元し、輸送がそれを値の枠の中へ置く。

          (sym (cut≡ ψ x' (subst (λ u → Cuts (x' .fst) Wv u) (valOf ψ (keyS W ψ) y refl e∈) cuts)) ∙ e)
          x'∈ })
      (RD.all-out ha (keyS W ψ) (sndS (keyS W ψ) (# ) (cd ψ) refl) (SR.C-in (keyS W ψ) (key∈AllCodes W ψ)) refl) })
    (𝒟ₒ-inv (W .fst) x hx)

完全性は同じ同値関係を逆向きにたどる。作業集合の同一視、正しいタグ、satAt を引き続き仮定すると、値の枠と 𝒟ₒ (W .fst) との等式から defAt の充足を構成できる。二つの連言項はそれぞれ、列挙された各集合に定義論理式があることと、アリティ一の各論理式が定める部分集合が必ず現れることを示す。

def-complete : Vv ≡ 𝒟ₒ (W .fst) → ⟨ γ ⊨ defAt v w T C N ⟩
def-complete qv = defAt-in v w T C N γ mem all
  where

それぞれの論理式の表の項目は、すでに定義された再帰の表から選ばれる。その表は、表の中での所属と、明示的な充足集合との同定の両方を保証する。

  entry : (ψ : Formula Ab ) → Σ[ y ∶ S ] (⟨ pr ((keyS W ψ) .fst) (y .fst) ∈ Tv ⟩ × (y .fst ≡ (Sat W (toS ψ)) .fst))
  entry ψ = Table.val W W (keyS W ψ) (key∈AllCodes W ψ)
          , ( SR.T-in (keyS W ψ) (key∈AllCodes W ψ)
            , cong (λ p → p .fst) (val-at W W ψ (keyS W ψ) (key∈AllCodes W ψ) refl) )

所属の連言項では、値の枠の要素を 𝒟ₒ (W .fst) へ移し、𝒟ₒ-inv で展開する。定義論理式は命題的切り詰めの下でのみ存在する。その内部で論理式の鍵、対応する表の項目、必要な Cuts の証拠を組み立てるが、定義論理式を大域的に選んだり、標準的なデータとして保持したりはしない。

  mem : ⟨ γ ⊨ memAt v w T C N ⟩
  mem = RD.mem-in (λ x x∈ → map₁
    (λ { (ψ , e) →
      keyS W ψ , sndS (keyS W ψ) (# ) (cd ψ) refl , entry ψ .fst
      , ( SR.C-in (keyS W ψ) (key∈AllCodes W ψ)

ここで用いる表の値は、再帰的な充足関係表がこの論理式の鍵に対してすでに定めた値である。その値と明示的な充足集合との等式に沿って cuts-of を移せば、切り出しの証拠が得られる。この一時的な論理式の証人は終始 map₁ の内部にあり、得られる所属の証人も命題的に切り詰められたままである。

        , ( refl
          , ( entry ψ .snd .fst
            , subst (λ u → Cuts (x .fst) Wv u) (sym (entry ψ .snd .snd)) (cuts-of ψ x e) ) ) ) })
    (𝒟ₒ-inv (W .fst) (x .fst) (subst (λ u → ⟨ x .fst ∈ u ⟩) qv x∈)))

覆いの連言項は、符号の領域の中の、アリティ一のキーそれぞれに対して証明される。対の分解が明示的に名指される。

  all : ⟨ γ ⊨ allAt v w T C N ⟩
  all = RD.all-in (λ c p c∈ ec → map₁
    (λ { (ψ , qp) →
      let qc : c .fst ≡ (keyS W ψ) .fst
          qc = ec ∙ cong (pr (# )) qp

与えられたアリティ一の鍵に対し、復号は、その第二成分を符号にもつ論理式 ψ が単に存在することだけを与える。定義可能部分集合 DA.defSet ψ は導入によって 𝒟ₒ (W .fst) に属し、仮定した等式に沿う輸送で値の枠に入る。復号は一意な論理式や標準的な論理式を選ばない。

          xS : S
          xS = down (lookup v γ) (DA.defSet ψ)
                 (subst (λ u → ⟨ DA.defSet ψ ∈ u ⟩) (sym qv) (𝒟ₒ-intro (W .fst) (DA.defSet ψ) ∣ ψ , refl ∣₁))
      in entry ψ .fst , xS
       , ( subst (λ u → ⟨ pr u ((entry ψ .fst) .fst) ∈ Tv ⟩) (sym qc) (entry ψ .snd .fst)

充足関係表は、復号された論理式の鍵に対応する値を与え、cuts-of は、その値が作業集合からちょうど DA.defSet ψ を切り出すことを示す。先ほど得た所属と合わせれば、これらのデータは覆いの条項を満たす。decodeAll の結果は命題的に切り詰められ、この命題値の条項にだけ消去されるので、構成は存在だけを記録し、復号された論理式を保持しない。

         , ( subst (λ u → ⟨ DA.defSet ψ ∈ u ⟩) (sym qv) (𝒟ₒ-intro (W .fst) (DA.defSet ψ) ∣ ψ , refl ∣₁)
           , subst (λ u → Cuts (DA.defSet ψ) Wv u) (sym (entry ψ .snd .snd)) (cuts-of ψ xS refl) ) ) })
    (decodeAll c (SR.C-out c c∈)  (p .fst) ec))