充足関係の節の読み取りと検証

extB-out : ⟨ δ ⊨ extB y F φ ⟩ → ExtFact ((lookup y δ) .fst) ((lookup F δ) .fst) (λ z → ⟨ (z ∷ δ) ⊨ φ ⟩)
extB-out h = h

埋めも同じく定義的である。外延的な事実は、構成子の充足にほかならない。

extB-in : ExtFact ((lookup y δ) .fst) ((lookup F δ) .fst) (λ z → ⟨ (z ∷ δ) ⊨ φ ⟩) → ⟨ δ ⊨ extB y F φ ⟩
extB-in h = h

private
  Tv = (lookup T δ) .fst
  TS = lookup T δ
  A = (lookup ar δ) .fst

射影されたアリティを A、射影されたペイロードを Av と書く。部分キーの一致条件は一つの等式 c₁ .fst ≡ pr A Av となり、集合論的に符号化されたキーと、その二成分を与えたホストレベルのスロットとが区別される。

  Av = (lookup a δ) .fst

subAt が成り立つなら、底の対が (c₁,ya) であり、キーが c₁=(A,Av) を満たすすべての表要素から本体が従う。本体は ya ∷ c₁ ∷ s ∷ e' ∷ δ で評価される。ここで e' はその表要素を表し、s は対の二成分を取り出すためだけの容器である。どちらも追加の意味論的な値ではない。

subAt-out : ⟨ δ ⊨ subAt T ar a body ⟩ → (c₁ ya : S) (m : ⟨ pr (c₁ .fst) (ya .fst) ∈ Tv ⟩)
          → c₁ .fst ≡ pr A Av
          → ⟨ (ya ∷ c₁ ∷ container (down TS (pr (c₁ .fst) (ya .fst)) m) c₁ ya refl .fst
               ∷ down TS (pr (c₁ .fst) (ya .fst)) m ∷ δ) ⊨ body ⟩
subAt-out h c₁ ya m e =

証明はまず、表上の有界全称を (c₁,ya) の具体的な表示 e' に適用する。次に対の読み補題が二成分 c₁ と ya を与え、最後に pr-in が等式 c₁=(A,Av) を内部の含意が要求する前件へ変換する。残るのは四スロット拡張での本体そのものである。

  useBoth i0 (down TS (pr (c₁ .fst) (ya .fst)) m ∷ δ) c₁ ya refl (prAtL i1 (sh  ar) (sh  a) ⇒̇ body)
    (h (down TS (pr (c₁ .fst) (ya .fst)) m) m)
    (pr-in i1 (sh  ar) (sh  a)
      (ya ∷ c₁ ∷ container (down TS (pr (c₁ .fst) (ya .fst)) m) c₁ ya refl .fst
         ∷ down TS (pr (c₁ .fst) (ya .fst)) m ∷ δ) e)

埋めはその逆である。一致するすべての表の項目とその容器について本体が証明できれば、表の項目の上の有界全称が成立する。この読み手がしないことに注意してほしい。項目を一つ選ぶことも、値 ya が一意だと主張することもなく、一致するすべての項目の上で量化するだけである。

subAt-in : ((c₁ ya s e' : S) → ⟨ e' .fst ∈ Tv ⟩ → e' .fst ≡ pr (c₁ .fst) (ya .fst) → c₁ .fst ≡ pr A Av
            → ⟨ (ya ∷ c₁ ∷ s ∷ e' ∷ δ) ⊨ body ⟩)
         → ⟨ δ ⊨ subAt T ar a body ⟩
subAt-in g e' e'∈ = bothAll-in i0 (prAtL i1 (sh  ar) (sh  a) ⇒̇ body) (e' ∷ δ)
  (λ c₁ ya s s∈ c₁∈ ya∈ e hp → g c₁ ya s e' e'∈ e (pr-out i1 (sh  ar) (sh  a) (ya ∷ c₁ ∷ s ∷ e' ∷ δ) hp))

private
  Tv = (lookup T δ) .fst
  TS = lookup T δ
  A = (lookup ar δ) .fst

外側の論理式のアリティの値が名付けられ、上げられたアリティは証明の内部で別に復元される。

  Av = (lookup a δ) .fst

持ち上げられた読み補題は、キーが (ar',Av) である表要素と、等式 ar' .fst ≡ sucV A を使う。本体は ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ で評価される。二つの容器 s' と s は、有界論理式から持ち上げられたキーと表要素の成分を利用できるようにするだけである。

subSucAt-out : ⟨ δ ⊨ subSucAt T ar a body ⟩ → (c₁ ya ar' : S) (m : ⟨ pr (c₁ .fst) (ya .fst) ∈ Tv ⟩)
             → (e : c₁ .fst ≡ pr (ar' .fst) Av) → ar' .fst ≡ sucV A
             → ⟨ (ar' ∷ container c₁ ar' (lookup a δ) e .fst ∷ ya ∷ c₁
                  ∷ container (down TS (pr (c₁ .fst) (ya .fst)) m) c₁ ya refl .fst
                  ∷ down TS (pr (c₁ .fst) (ya .fst)) m ∷ δ) ⊨ body ⟩

証明は与えられた表要素から出発し、まず (c₁,ya) を分解して四スロットの主張 h4 を得る。次に fstAll へ第一成分の候補 ar' を与え、pr-in で c₁=(ar',Av) を、suc-in で ar'=suc A を証明する。本体を使う前に必要な条件は、まさにこの二つの等式である。

subSucAt-out h c₁ ya ar' m e es =
  (h4 (container c₁ ar' (lookup a δ) e .fst) (container c₁ ar' (lookup a δ) e .snd .fst)
      ar' (container c₁ ar' (lookup a δ) e .snd .snd .fst)
      (pr-in (sh  i1) i0 (sh  (sh  a)) δ6 e))
    (suc-in (sh  ar) i0 δ6 es)

局所名 e'S は、特定の表要素 (c₁,ya) の構成可能な表示であり、その対が T に属することから得られる。環境 δ4 は δ の前に ya、c₁、その対の成分を収める容器、e'S をこの順に置く。表全体の表示が入っているわけではない。

  where
  e'S = down TS (pr (c₁ .fst) (ya .fst)) m
  δ4 : Vec S ( + j)
  δ4 = ya ∷ c₁ ∷ container e'S c₁ ya refl .fst ∷ e'S ∷ δ
  δ6 : Vec S ( + j)

選んだ表要素に useBoth を適用すると、表上の外側の量化と対の分解が一度に除かれる。得られる h4 は δ4 における残りの fstAll の主張である。そこではなお c₁ の第一成分の候補を与え、その成分が後続アリティであることを示す必要がある。

  δ6 = ar' ∷ container c₁ ar' (lookup a δ) e .fst ∷ δ4
  h4 : ⟨ δ4 ⊨ fstAll i1 (sh  a) (sucAtL (sh  ar) i0 ⇒̇ body) ⟩
  h4 = useBoth i0 (e'S ∷ δ) c₁ ya refl (fstAll i1 (sh  a) (sucAtL (sh  ar) i0 ⇒̇ body)) (h e'S m)

逆方向では、表要素のあらゆる分解と、そのキーの第一成分のあらゆる分解について、一様に本体を証明すれば十分である。仮定中の二つの等式により、キーが (suc A,Av) である要素だけが関係する。特定の表要素や持ち上げられたアリティを大域的に選ぶことはない。

subSucAt-in : ((c₁ ya ar' s s' e' : S) → ⟨ e' .fst ∈ Tv ⟩ → e' .fst ≡ pr (c₁ .fst) (ya .fst)
               → c₁ .fst ≡ pr (ar' .fst) Av → ar' .fst ≡ sucV A
               → ⟨ (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) ⊨ body ⟩)
            → ⟨ δ ⊨ subSucAt T ar a body ⟩
subSucAt-in g e' e'∈ = bothAll-in i0 (fstAll i1 (sh  a) (sucAtL (sh  ar) i0 ⇒̇ body)) (e' ∷ δ)

導入の証明は、二段の全称的な対の読みから現れる成分を受け取る。pr-out で等式 c₁=(ar',Av) を、suc-out で ar'=suc A を復元し、それらの等式、表への所属、六スロットの環境を一様な仮定 g に渡す。

  (λ c₁ ya s s∈ c₁∈ ya∈ e s' s'∈ ar' ar'∈ hp hs →
    g c₁ ya ar' s s' e' e'∈ e
      (pr-out (sh  i1) i0 (sh  (sh  a)) (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) hp)
      (suc-out (sh  ar) i0 (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) hs))

private
  Tv = (lookup t δ) .fst
  Z = (lookup z δ) .fst

残る二つの射影は、候補値 Vv とタグ一のスロットに実際に入っている集合 N1v を名付ける。内部論理式は N1v を参照するが、TmIsV の変数の場合は正準な数項 #1 を使うため、証明は q1 に沿って等式を輸送しなければならない。

  Vv = (lookup v δ) .fst
  N1v = (lookup N1 δ) .fst

内側の有界存在が動くのはグラフ z の要素 q であり、添字そのものではない。その対のアトムは q=(i,v) を主張し、添字 i はすでに項コードの第二成分として復元されている。したがって内部論理式は、その固定した添字と候補値を組にした要素がグラフに含まれることを述べる。

  inner : Formula S ( + j)
  inner = ∃̇∈ (var (sh  z)) (prAtL i0 i1 (sh  v))

Inner i s は、この有界存在の意味を詰め直す。そこから得られるのは、グラフ要素 q、q∈Z の証明、そして q ∷ i ∷ s ∷ δ において対のアトム q=(i,Vv) が成り立つ証明だけである。スロット s は項コードの成分を取り出すための容器である。

  Inner : (i s : S) → Type (ℓ-suc ℓ)
  Inner i s = ∥ Σ[ q ∶ S ] (⟨ q .fst ∈ Z ⟩ × ⟨ (q ∷ i ∷ s ∷ δ) ⊨ prAtL i0 i1 (sh  v) ⟩) ∥₁

Outer は sndEx から読み出した変数の場合の全体をまとめる。ペイロードの表示 i と容器 s が単に存在し、Tv=pr N1v (i .fst) が成り立ち、内側の有界存在が i ∷ s ∷ δ で成り立つ。この等式が項コードと同一視するのはタグ一の対であり、i とタグそのものではない。

  Outer : Type (ℓ-suc ℓ)
  Outer = ∥ Σ[ i ∶ S ] Σ[ s ∶ S ] ((Tv ≡ pr N1v (i .fst)) × ⟨ (i ∷ s ∷ δ) ⊨ inner ⟩) ∥₁

内側の証人 q から pr-out により q=pr .fst (i .fst) Vv が得られ、既知の所属 q∈Z をこの等式に沿って輸送すると、必要なグラフ要素 (i,Vv) の所属が得られる。同時に q1 は、外側の等式に現れる実際のタグスロット N1v を #1 に書き換える。この二つが TmIsV の変数の場合の二つの成分そのものである。

  viaQ : (i s : S) → Tv ≡ pr N1v (i .fst) → Inner i s → TmIsV Tv Z Vv
  viaQ i s e = map₁
    (λ { (q , (q∈ , hp)) → inr (i .fst , ( e ∙ cong (λ a → pr a (i .fst)) q1
       , subst (λ u → ⟨ u ∈ Z ⟩) (pr-out i0 i1 (sh  v) (q ∷ i ∷ s ∷ δ) hp) q∈ )) })

viaI は、単に存在する外側の分解を TmIsV へ消去する。TmIsV 自身も命題的に切り詰められているため、この消去は各局所的な対の分解を変換するだけで、後で使う一つの分解を選び出すことはない。

  viaI : Outer → TmIsV Tv Z Vv
  viaI = rec₁ squash₁ (λ { (i , s , (e , hq)) → viaQ i s e hq })

対象論理式 tmIs は二つのコード形の選言である。定数の場合、pr-out が Tv=pr(q0,Vv) を読み出し、q0=#0 によってそれを TmIsV の第一の場合へ変換する。変数の場合、sndEx-out が Outer を生成し、viaI がそれをグラフ所属の場合へ変換する。

  cases : ⟨ δ ⊨ prAtL t N0 v ⟩ ⊎ ⟨ δ ⊨ sndEx t N1 inner ⟩ → TmIsV Tv Z Vv
  cases (inl h) = ∣ inl (pr-out t N0 v δ h ∙ cong (λ a → pr a Vv) q0) ∣₁
  cases (inr h) = viaI (sndEx-out t N1 inner δ h)

公開された消去補題 tmIs-out は、外側の選言の命題的切り詰めの下でこの場合分けを行う。結論は一つの候補値 Vv について述べるだけで、二つの候補値が等しいことは示さない。Z が任意の多値関係なら、同じ変数コードが複数の値で tmIs を満たしえる。

tmIs-out : ⟨ δ ⊨ tmIs t z v N0 N1 ⟩ → TmIsV Tv Z Vv
tmIs-out h = rec₁ squash₁ cases h

逆方向では、build が二つの具体的なコード形のどちらからでも tmIs の充足を再構成する。定数の等式は pr-in で変換する。変数の場合は、ペイロードの添字とグラフ要素を S の要素として表示し、その後 sndEx の入れ子になった有界存在を組み立て直す。

private
  build : (Tv ≡ pr (# ) Vv) ⊎ (Σ[ i ∶ V ℓ ] ((Tv ≡ pr (# ) i) × ⟨ pr i Vv ∈ Z ⟩))
        → ⟨ δ ⊨ tmIs t z v N0 N1 ⟩
  build (inl e) = ∣ inl (pr-in t N0 v δ (e ∙ cong (λ a → pr a Vv) (sym q0))) ∣₁
  build (inr (i , (e , hp))) = ∣ inr (fillSnd t δ (lookup N1 δ) iS e' inner hq N1 refl) ∣₁

iS はペイロード i の構成可能な表示であり、対の等式 Tv=(#1,i) の第二成分として復元される。qS はグラフ要素 (i,Vv) の構成可能な表示であり、その対が Z に属することから得られる。これらは S 内の証人であって、新しい意味論的な添字や値ではない。

    where
    iS : S
    iS = sndS (lookup t δ) (# ) i e
    qS : S
    qS = down (lookup z δ) (pr i Vv) hp

等式 e' は正準なタグの等式を、sndEx が要求する実際のタグ一スロットに書き換える。補助環境 δ3 は δ の前に、グラフ要素 qS、ペイロードの表示 iS、外側の項コードの対を収める容器をこの順に置く。残る目標 hq は、iS ∷ container ∷ δ における内側の有界存在そのものである。

    e' : Tv ≡ pr N1v (iS .fst)
    e' = e ∙ cong (λ a → pr a i) (sym q1)
    δ3 : Vec S ( + j)
    δ3 = qS ∷ iS ∷ container (lookup t δ) (lookup N1 δ) iS e' .fst ∷ δ
    hq : ⟨ (iS ∷ container (lookup t δ) (lookup N1 δ) iS e' .fst ∷ δ) ⊨ inner ⟩

hq を証明するには、グラフから qS を選ぶ。その所属は与えられた事実 hp であり、pr-in は反射性によって、その底集合が iS と Vv の対であることを示す。これで変数の場合に必要なグラフ要素がちょうど得られる。

    hq = ∣ qS , (hp , pr-in i0 i1 (sh  v) δ3 refl) ∣₁

最後に tmIs-in は、TmIsV の命題的切り詰めを tmIs の充足を表す命題へ消去し、どちらの場合にも build を適用する。tmIs-out と合わせて意味論の二方向が得られるが、大域的な選択や一意性の主張は導入されない。

tmIs-in : TmIsV Tv Z Vv → ⟨ δ ⊨ tmIs t z v N0 N1 ⟩
tmIs-in = rec₁ ((δ ⊨ tmIs t z v N0 N1) .snd) build

private
  Tv = (lookup T γ) .fst
  Cv = (lookup C γ) .fst
  Ev = (lookup E γ) .fst

枠組みは有界全称の列によって順にほどかれる。最も内側では inner9 k がすべての表要素を動き、その第一成分が c であるとき sndAll によって値 yc を取り出す。得られた十二スロットの環境で relN (toℕ k) が成り立たなければならない。これは一致するすべての要素についての全称条件であり、一つの値を探す存在条件ではない。

  module Cl = Clause T w C E N
  module R = Rel T w N
  inner9 : Fin  → Formula S ( + m)
  inner9 k = ∀̇∈ (var (sh  T)) (sndAll i0 i5 (R.relN (toℕ k)))
  inner7 : Fin  → Formula S ( + m)

その前の段階では入れ子になったキーを取り出す。inner4 k は、第一成分が現在のアリティ ar であるすべての c∈C を動き、そのペイロード p を得る。続いて inner7 k は p のタグが N k のスロットにある数項であることを要求し、残りのデータ r を取り出す。対を分解するたびに成分と容器が先頭へ加わるため、以前の枠組みのスロットへの参照はシフトによって保たれる。

  inner7 k = sndAll i0 (sh  (N k)) (inner9 k)
  inner4 : Fin  → Formula S ( + m)
  inner4 k = ∀̇∈ (var (sh  C)) (sndAll i0 i2 (inner7 k))

一つの節の実例について、At は塔の対 (ar,F)、論理式キー c=(ar,p)、タグ付きペイロード p=(N k,r)、表の対 (c,yc) を固定する。所属 q∈ と e∈ はそれぞれ E と T における射影された対について述べる。このモジュール自身は c∈C を証明せず、r を復号せず、表の値の一意性も示さない。

module At (ar F c p r yc : S) (q∈ : ⟨ pr (ar .fst) (F .fst) ∈ Ev ⟩)
          (ec : c .fst ≡ pr (ar .fst) (p .fst)) (k : Fin )
          (ep : p .fst ≡ pr ((lookup (N k) γ) .fst) (r .fst))
          (e∈ : ⟨ pr (c .fst) (yc .fst) ∈ Tv ⟩) where

qS eS : S

qS = down (lookup E γ) (pr (ar .fst) (F .fst)) q∈
eS = down (lookup T γ) (pr (c .fst) (yc .fst)) e∈

δ4 : Vec S ( + m)
δ4 = F ∷ ar ∷ container qS ar F refl .fst ∷ qS ∷ γ
δ7 : Vec S ( + m)
δ7 = p ∷ container c ar p ec .fst ∷ c ∷ δ4
δ9 : Vec S ( + m)

δ9 = r ∷ container p (lookup (N k) γ) r ep .fst ∷ δ7
δ12 : Vec S ( + m)
δ12 = yc ∷ container eS c yc refl .fst ∷ eS ∷ δ9

外向きの読み取りは第 k 節の充足から出発し、その枠の一つの実例に対応するデータをすべて固定する。塔の対から得られる ar と F、C に属するコード c=(ar,p)、タグ付きペイロード p=(#k,r)、そして (c,yc) が T に属する候補値 yc である。そのうえで、対応する十二の枠の環境における relN (toℕ k) の充足を返す。ここで表について仮定するのは対 (c,yc) の所属であり、実際の表要素とそのコンテナは局所的に構成される。

clause-out : (k : Fin ) → ⟨ γ ⊨ Cl.clause k ⟩
           → (ar F c p r yc : S) (q∈ : ⟨ pr (ar .fst) (F .fst) ∈ Ev ⟩) → ⟨ c .fst ∈ Cv ⟩
           → (ec : c .fst ≡ pr (ar .fst) (p .fst)) → (ep : p .fst ≡ pr (# (toℕ k)) (r .fst))
           → (e∈ : ⟨ pr (c .fst) (yc .fst) ∈ Tv ⟩)
           → ⟨ At.δ12 ar F c p r yc q∈ ec k (ep ∙ cong (λ a → pr a (r .fst)) (sym (tg k))) e∈ ⊨ R.relN (toℕ k) ⟩

対応するデータを固定すると、モジュール A は十二の枠すべてに対して整合した一つの実現を与える。最初の除去が塔の対を開き、最後の useSnd が実際の表の要素を (c,yc) として開く。その間には符号とタグの層を通る必要がある。そこで先に h4 を名づけることで、結論が構成子の関係を別に仮定したものではなく、一つの外側の節を順次特殊化して得られることが明示される。

clause-out k h ar F c p r yc q∈ c∈ ec ep e∈ =
  useSnd i0 (A.eS ∷ A.δ9) c yc refl (R.relN (toℕ k)) i5 refl (h9 A.eS e∈)
  where
  module A = At ar F c p r yc q∈ ec k (ep ∙ cong (λ a → pr a (r .fst)) (sym (tg k))) e∈
  h4 : ⟨ A.δ4 ⊨ inner4 k ⟩

三つの中間判断は、共通の枠の三つの意味論的な層を示す。δ4 では h4 が塔の項目 (ar,F) を開き、C の符号を調べられる状態にある。δ7 では h7 がさらに c=(ar,p) を分解している。δ9 では h9 が p をタグ k のペイロード r と同定し、T の項目を調べられる状態にある。最後の除去で、選んだ表の要素を (c,yc) と分解し、構成子の関係に到達する。

  h4 = useBoth i0 (A.qS ∷ γ) ar F refl (inner4 k) (h A.qS q∈)
  h7 : ⟨ A.δ7 ⊨ inner7 k ⟩
  h7 = useSnd i0 (c ∷ A.δ4) ar p ec (inner7 k) i2 refl (h4 c c∈)
  h9 : ⟨ A.δ9 ⊨ inner9 k ⟩
  h9 = useSnd i0 A.δ7 (lookup (N k) γ) r (ep ∙ cong (λ a → pr a (r .fst)) (sym (tg k))) (inner9 k) (sh  (N k)) refl h7

逆向きの構成では、完全に対応するすべての枠から構成子の関係を証明できると仮定する。そのような枠は、塔の要素 q=(ar,F)、C に属する符号 c=(ar,p)、タグの分解 p=(#k,r)、表の要素 e=(c,yc)、および四つの対の証人 s、s1、s2、s3 からなる。これらすべてのデータについて表示された環境で関係を証明できることが、第 k 節を再構成するために必要な前提そのものである。

clause-in : (k : Fin )
          → ((q ar F s c p s1 r s2 e yc s3 : S) → ⟨ q .fst ∈ Ev ⟩ → q .fst ≡ pr (ar .fst) (F .fst)
             → ⟨ c .fst ∈ Cv ⟩ → c .fst ≡ pr (ar .fst) (p .fst) → p .fst ≡ pr (# (toℕ k)) (r .fst)
             → ⟨ e .fst ∈ Tv ⟩ → e .fst ≡ pr (c .fst) (yc .fst)
             → ⟨ (yc ∷ s3 ∷ e ∷ r ∷ s2 ∷ p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) ⊨ R.relN (toℕ k) ⟩)

証明は全称量化された枠を論理的な順序で組み直す。まず E の任意の q と、そこから取り出される各分解 q=(ar,F) を扱い、次に C の任意の c と、それに一致する各分解 c=(ar,p) を扱う。続いて p のタグとペイロードを同定し、最後に T の任意の e と各分解 e=(c,yc) を扱う。有界な導入のたびに新しい値が環境の先頭に置かれ、対応する s 変数が論理式に必要な対分解の証人を保持する。

          → ⟨ γ ⊨ Cl.clause k ⟩
clause-in k g q q∈ = bothAll-in i0 (inner4 k) (q ∷ γ) (λ ar F s s∈ ar∈ F∈ eq c c∈ →
  sndAll-in i0 i2 (inner7 k) (c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ p s1 s1∈ p∈ ec →
    sndAll-in i0 (sh  (N k)) (inner9 k) (p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ r s2 s2∈ r∈ ep e e∈ →
      sndAll-in i0 i5 (R.relN (toℕ k)) (e ∷ r ∷ s2 ∷ p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ yc s3 s3∈ yc∈ ee →

ホスト側の規則 g を適用する前に、ペイロードの等式を tg k と合成し、タグの枠に格納された集合を正準な数項 #k に書き換える。したがって規則が受け取るのは、外向きの読み取りに現れる等式 p=(#k,r) そのものである。こうして clause-in と clause-out は、一致する各枠において、第 k 節とその関係の間の二方向を与える。

        g q ar F s c p s1 r s2 e yc s3 q∈ eq c∈ ec (ep ∙ cong (λ a → pr a (r .fst)) (tg k)) e∈ ee))))

全域性は、切り詰められた存在として外向きに読まれる。符号領域の各要素に対して、全域性の条項が、その第一成分をもつ表の項目の存在を保証し、表の項目の切り詰められた分解が値 yc を復元する。

total-out : ⟨ γ ⊨ Cl.total ⟩ → (c : S) → ⟨ c .fst ∈ Cv ⟩ → ∥ Σ[ yc ∶ S ] ⟨ pr (c .fst) (yc .fst) ∈ Tv ⟩ ∥₁
total-out h c c∈ = rec₁ squash₁
  (λ { (e , (e∈ , hs)) → map₁
    (λ { (yc , s , (ee , _)) → yc , subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈ })
    (sndEx-out i0 i1 ⊤̇ (e ∷ c ∷ γ) hs) })

c∈C を固定して仮定 h を c に適用すると、命題的切り詰めの下で、表要素 e、その T への所属、および分解を述べる証明が得られる。読み補題 sndEx-out がさらに e を (c,yc) に分解し、その等式に沿って e の所属を運ぶことで (c,yc)∈T を示す。二段の分解はいずれも切り詰めの内部にとどまるので、結論は存在を与えるだけで、正準な値を選ばない。

  (h c c∈)

逆に、C の各 c について、(c,yc) が T に属するような値 yc が命題的に切り詰められて存在すると仮定する。down はその所属の証明を、基礎の集合がその対である T の要素 e : S に実現し、fillSnd は e を c と yc に分解する有界な証人を与える。残る本体は真なので、このデータから全域性の節を構成できる。値の大域的な選択も一意性の主張も含まれない。

total-in : ((c : S) → ⟨ c .fst ∈ Cv ⟩ → ∥ Σ[ yc ∶ S ] ⟨ pr (c .fst) (yc .fst) ∈ Tv ⟩ ∥₁) → ⟨ γ ⊨ Cl.total ⟩
total-in g c c∈ = map₁
  (λ { (yc , m) → down (lookup T γ) (pr (c .fst) (yc .fst)) m
     , ( m , fillSnd i0 (down (lookup T γ) (pr (c .fst) (yc .fst)) m ∷ c ∷ γ) c yc refl ⊤̇ (λ b → b) i1 refl ) })
  (g c c∈)

領域条件は、あらかじめ選ばれた対ではなく、T の任意の要素 e から出発する。その外向きの読み取りは、e=(c,yc) かつ c が C に属するような c と yc を、命題的切り詰めの下で復元する。したがって表の各要素の第一成分は指定された領域の符号であるが、分解の正準な選択も、一つの符号が値を一つしか持たないことも述べていない。

onC-out : ⟨ γ ⊨ Cl.onC ⟩ → (e : S) → ⟨ e .fst ∈ Tv ⟩
        → ∥ Σ[ c ∶ S ] Σ[ yc ∶ S ] ((e .fst ≡ pr (c .fst) (yc .fst)) × ⟨ c .fst ∈ Cv ⟩) ∥₁
onC-out h e e∈ = map₁ (λ { (c , yc , s , (ee , c∈)) → c , yc , (ee , c∈) })
  (bothEx-out i0 (var i1 ∈̇ var (sh  C)) (e ∷ γ) (h e e∈))

逆向きの読み取りは、T の各要素についてまさにこの切り詰められた分解を要求し、それを onC の二つの有界存在量化へ入れる。二方向の読み取りを合わせると、onC は「表の各要素の第一射影が C に属する」という主張に正確に対応する。全域性と組み合わせれば表の領域射影は定まるが、表が一価の関係になるわけではない。

onC-in : ((e : S) → ⟨ e .fst ∈ Tv ⟩ → ∥ Σ[ c ∶ S ] Σ[ yc ∶ S ] ((e .fst ≡ pr (c .fst) (yc .fst)) × ⟨ c .fst ∈ Cv ⟩) ∥₁)
       → ⟨ γ ⊨ Cl.onC ⟩
onC-in g e e∈ = rec₁ (((e ∷ γ) ⊨ bothEx i0 (var i1 ∈̇ var (sh  C))) .snd)
  (λ { (c , yc , (ee , c∈)) → fillBoth i0 (e ∷ γ) c yc ee (var i1 ∈̇ var (sh  C)) c∈ })
  (g e e∈)

private module R = Rel T w N
private
  yc = lookup i0 δ
  r = lookup i3 δ

残る局所名は、環境集合の枠 F とアリティの枠 ar を示す。さらに表の底集合 Tv、アリティの値 A、構成子のペイロード Rv を一度だけ射影しておくことで、後の関係の読み補題が累積階層の中で仮定を直接述べられるようにする。

  F = lookup i8 δ
  ar = lookup i9 δ
  Tv = (lookup (sh  T) δ) .fst
  A = ar .fst
  Rv = r .fst

さらに拡張された任意の局所環境 env に対して、Ext env φ は外側の表の値 yc の正確な外延条件を述べる。要素 z が yc に属するのは、z がアリティに対応する環境集合 F に属し、かつ z を env の新しい先頭枠に置いたときに論理式 φ が成り立つ場合にちょうど限る。そのため、env の元の枠は φ の内部では一つ後ろの位置から読まれる。

Ext : ∀ {k} (env : Vec S k) (φ : Formula S ( + k)) → Type (ℓ-suc ℓ)
Ext env φ = ExtFact (yc .fst) (F .fst) (λ z → ⟨ (z ∷ env) ⊨ φ ⟩)

二項結合子では、ペイロード r が二つの子論理式の符号 a と b に分解されなければならない。また、鍵 c₁=(A,a) と c₂=(A,b) は、それぞれ表の値 ya と yb を持つ必要がある。これらの仮定から bin-out は、命題的切り詰めの下で五つの補助的な証人を返す。一つは r=(a,b) のコンテナで、各子論理式については T の実際の要素とその分解を示すコンテナである。数学的な結論は外側の値 yc に関する Ext であり、その本体は ya と yb への所属を結合子 op で組み合わせる。

bin-out : (op : ∀ {j} → Formula S j → Formula S j → Formula S j) → ⟨ δ ⊨ R.binRel op ⟩
        → (a b c₁ ya c₂ yb : S) → Rv ≡ pr (a .fst) (b .fst)
        → ⟨ pr (c₁ .fst) (ya .fst) ∈ Tv ⟩ → c₁ .fst ≡ pr A (a .fst)
        → ⟨ pr (c₂ .fst) (yb .fst) ∈ Tv ⟩ → c₂ .fst ≡ pr A (b .fst)
        → ∥ Σ[ s ∶ S ] Σ[ s₁ ∶ S ] Σ[ e₁ ∶ S ] Σ[ s₂ ∶ S ] Σ[ e₂ ∶ S ]

五つの証人をまとめるのは、対象言語の有界量化が各対分解を隠しているためである。ペイロードを開いた後、最初の subAt-out が左の子論理式の鍵における値を読み、二つ目が右の子論理式の鍵における値を読む。最も内側の extB がそこで yc の正確な外延を与えるが、表がどちらかの子の値を一意に選んだとは述べていない。

            Ext (yb ∷ c₂ ∷ s₂ ∷ e₂ ∷ ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b ∷ a ∷ s ∷ δ) (R.binBody op) ∥₁
bin-out op h a b c₁ ya c₂ yb er m₁ e₁ m₂ e₂ =
  ∣ container r a b er .fst , container e₁S c₁ ya refl .fst , e₁S , container e₂S c₂ yb refl .fst , e₂S ,
    subAt-out (sh  T) i16 i4 (extB i11 i19 (R.binBody op)) δ19
      (subAt-out (sh  T) i12 i1 (subAt (sh  T) i16 i4 (extB i11 i19 (R.binBody op))) δ15

最初の段階では、十二枠の環境内でペイロードの等式 r=(a,b) を開く。これにより対のコンテナが加わり、古い枠の前に b、a、そのコンテナを置いた δ15 が得られる。その後、入れ子になった二つの子の値の読み取りが左から右へ進むため、そこで隠される表の証人は外側の命題的切り詰めの内部に保たれる。

        (useBoth i3 δ a b er (subAt (sh  T) i12 i1 (subAt (sh  T) i16 i4 (extB i11 i19 (R.binBody op)))) h)
        c₁ ya m₁ e₁)
      c₂ yb m₂ e₂ ∣₁
  where
  δ15 : Vec S ( + m)

(c₁,ya) の所属証明そのものは、構造 S の要素を直接与えない。down はそれを、基礎の対が (c₁,ya) である T の実際の要素 e₁S : S として実現する。環境 δ19 はさらに ya、c₁、両者の対のコンテナ、e₁S を δ15 の前に置く。この四つの枠が、最初の subAt の読み取りが要求する枠に正確に一致する。

  δ15 = b ∷ a ∷ container r a b er .fst ∷ δ
  e₁S : S
  e₁S = down (lookup (sh  T) δ15) (pr (c₁ .fst) (ya .fst)) m₁
  δ19 : Vec S ( + m)
  δ19 = ya ∷ c₁ ∷ container e₁S c₁ ya refl .fst ∷ e₁S ∷ δ15

同じ構成により、二つ目の所属証明は、基礎の対が (c₂,yb) である実際の表の要素 e₂S : S として実現される。二つ目の subAt-out は δ19 を拡張するときに対応する対のコンテナも与える。こうして binBody は二つの子の値をともに読めるが、どちらの所属証明も表からの大域的な選択には変えられていない。

  e₂S : S
  e₂S = down (lookup (sh  T) δ19) (pr (c₂ .fst) (yb .fst)) m₂

逆向きの構成は、二項の枠のあらゆる分解に対する規則から始まる。規則は子論理式の符号と値に加えて、ペイロードのコンテナ、二つの実際の表の要素、それぞれの対のコンテナ、および鍵が (A,a) と (A,b) であることを示す等式を受け取る。その結論は、元の十二枠の前にこれら十一の対象を加えた環境における、外側の値 yc の Ext でなければならない。

bin-in : (op : ∀ {j} → Formula S j → Formula S j → Formula S j)
       → ((a b s c₁ ya s₁ e₁ c₂ yb s₂ e₂ : S) → Rv ≡ pr (a .fst) (b .fst)
          → ⟨ e₁ .fst ∈ Tv ⟩ → e₁ .fst ≡ pr (c₁ .fst) (ya .fst) → c₁ .fst ≡ pr A (a .fst)
          → ⟨ e₂ .fst ∈ Tv ⟩ → e₂ .fst ≡ pr (c₂ .fst) (yb .fst) → c₂ .fst ≡ pr A (b .fst)
          → Ext (yb ∷ c₂ ∷ s₂ ∷ e₂ ∷ ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b ∷ a ∷ s ∷ δ) (R.binBody op))