集合で符号化した有限環境

本章のすべてのことは、固定された一つの宇宙レベル ℓ の上で行われる。操作される集合は V ℓ の要素であり、言語の論理式はそれらの集合の上で量化する。レベルを明示的なパラメータとして保つことで、この構成全体は、そのレベルの階層が利用できるどこでもインスタンス化できる。

module L.Coding.Environment {ℓ : Level} where

一階言語の充足の各節は変数の値について語るが、量化できるのは集合の上だけである。したがって充足関係を集合論の内部で計算するには、変数割当てそのものが先に集合にならなければならない。本章はこの符号化を行う。すなわち、変数の添字から V ℓ の集合への関数という有限な割当てを、そのグラフ、つまり「添字の数項とそこでの値」の対の集合として表す。

この符号化の設計目標は、グラフの中での参照を正確にすることである。鍵の側が数項からなり、数項が単射であるため、鍵 i の位置に座る対の第二成分は i での値にちょうど等しく、それ以外の何ものでもない。この関数性の主張が本章の主補題である。

第二の関心事は拡張である。充足が量化子の内側へ降りるとき、新しい値は添字 0 に置かれ、すべての旧添字は一つ上へ動く。鍵の側では、これはまさに von Neumann 後者である。そこで本章は、所属だけを用いて、一方の添字が他方の後者であること、ある対が他の対の鍵をずらして得られること、そして最後に、ある集合が拡張後の割当てのグラフであることを述べる有界論理式を組み立てる。それぞれは妥当性の主張として証明される。論理式の充足は真理値のパスであり、集合についての対応する外側の事実へ通じており、そこで扱われるグラフは外延性によって一要素ずつ比較され、切り捨てられた所属データから証人を選び出すことは決してない。

open import Cubical.Data.Sum using () renaming ( map to sumMap )
open import Cubical.Data.FinData using ( inj-toℕ )

本章は一階言語の有界な断片の中で作業する。Δ₀ 論理式とは、すべての量化子が環境の変数によって有界化されている論理式であり、その充足は提示された界定集合への所属のみに依存する。符号化の数学的な仕事を担うのは、ホスト側の二つの事実である。Kuratowski 対 pr が単射であること、すなわち対がその成分を決めること。そして数項 # n が単射であること、すなわち数項がその添字を決めることである。この二つの単射性が合わさって、割当てのグラフに関数のグラフとしての振る舞いを与える。

有界な読み取り prAt は対の論理式の章で妥当であることが証明されており、指定された変数スロットの集合が、他の二つのスロットの集合の Kuratowski 対であることを述べる。ここでは、その妥当性補題と、成分を対の内側に置く二つの導入規則をそのまま再利用する。ずらされた項目もまた Kuratowski 対であり、鍵が動いただけだからである。ホスト側で二元の直和型が使われるのは、論理式が選言を生む場所に対応する。値がこれかあれかであることを、どちらの側かの選択として記録し、証人の一意性を主張しない。

階層の集合への所属は命題であるため、「グラフのある項目が与えられた対と関係する」という証明は常に「単に存在する」という形をとる。証人が存在することは記録されるが、通常のデータとして与えられるわけではない。この切り捨てを消除できるのは命題値の対象へのみであり、そこから全体として選ばれた証人を取り戻すことはできない。本章で二つの命題が同一視されるときは、常に ⇔toPath によって行われる。これは同値を真理値の間のパスに変えるもので、ここにある各妥当性補題はみなこの形をしている。

背景となる宇宙は cubical 累積階層である。集合は sett A f として導入される。これは索引型と要素の族の組であり、その所属関係はこの設定における他の所属と同様に切り捨てられる。外延性の原理は、同じ要素を持つ二つの集合がパスとして等しいと述べる。符号化されたグラフの比較はまさにこの道具によって行われる。ある候補グラフが別のグラフに等しいことを示すには、各要素について、一方への所属という命題が他方への所属という命題と真理値のパス一本分しか違わないことを証明すればよいのである。

open import Cubical.HITs.CumulativeHierarchy.Base
  using ( V; sett; setIsSet; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; _⊆_; extensionality )

階層の構成は、符号化が使う材料を供給する。空集合、単集合、非順序対 ⁅_,_⁆、そして数項である。ここで鍵となるのは数項の再帰的定義である。# 0 は ∅ であり、# (suc n) は sucV (# n)、つまり von Neumann 後者である。したがって「添字を一つ進めること」と「鍵の後者を取ること」は同じ操作であり、これこそ環境の拡張が有界論理式で記述できる理由である。意味論の側では、真理値は命題性の証明を伴う命題なので、論理式の充足それ自体が命題であり、一つのパスによって外側の集合論的な主張と同一視できる。

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_,_⁆; ⁅_⁆s; ∅; ∅-empty; module InfinitySet )
open InfinitySet using ( sucV; #_ )

module Sem = FOL.Semantics 𝒮ᵥ

最後に、充足関係 _⊨_ と項の解釈 ⟦_⟧ は、台となる集合として V ℓ 自身の上に、定数の恒等解釈とともに取られる。したがって項数 n の論理式に対する環境とは、型 Vec (V ℓ) n のベクトル、すなわち集合の有限な組である。本章が符号化するのは、証明書データが担う割当てであって、この意味論の台となる集合ではない。組の形は意味論が評価する対象であり、グラフの形こそが証明書が一つの集合として保管し操作できる対象である。

open Sem.At (V ℓ) id using ( _⊨_; ⟦_⟧ )

環境のグラフと参照

割当て g : Fin n → V ℓ は集合 env g になる。添字 i の鍵の位置にある項目は、数項 # (toℕ i) と値 g i の順序対である。この節は、この表現を使い物にする主張を証明する。lookup-spec は、「鍵 i の対が env g に属する」という命題を、「その対の第二成分が g i に等しい」という命題と同一視するのである。env g への所属は、他の階層の所属と同様に切り捨てられている。lookup-spec の要点は、この切り捨てられたファイバーデータであっても、値を正確に決定するという点にある。

この集め方は集合の構成子 sett のインスタンスであり、索引型と要素の族を受け取る。有限な索引型 Fin n はレベル ℓ より下に住むので、先に持ち上げる。Lift は宇宙を調整するだけであり、lower が索引を取り戻す。そして各索引 li は一つの項目、すなわちその添字の数項と g のそこでの値の対に寄与する。項目そのものは通常のデータであり、切り捨てられるのは結果の集合への所属だけである。索引をそのまま使わず鍵 # (toℕ i) に変えるのは、論理式言語が鍵について語えなければならず、論理式が語る対象は集合、ここでは数項だからである。

env : ∀ {n} → (Fin n → V ℓ) → V ℓ
env {n} g = sett (Lift {ℓ-zero} {ℓ} (Fin n))
                 (λ li → pr (# (toℕ (lower li))) (g (lower li)))

このグラフは関数的である。すなわち、ある対が鍵 i の位置で env g に属するのは、その第二成分が値 g i であるとき、そのときに限る。これは所属についての外延的な主張であり、この符号化が単に定義可能であるだけでなく参照に使える理由でもある。

議論は鍵の三つの層に沿って進む。証拠となる項目は Kuratowski 対であり、対は単射なので、その鍵は問われた鍵と等しくなる。鍵は数項であり、数項は単射なので、根底にある添字は自然数として一致する。最後に Fin n は自然数へ埋め込まれるので、二つの添字は同じ索引であり、値の成分はそこに g i があることを示す。逆方向は i の項目そのものを示すだけである。

主張は命題の等式である。鍵 i の対がグラフに属するという命題は、ちょうど v ≡ g i であり、その命題性の証明を伴う。これは V ℓ が h-集合であることから来る。命題の間の同値は真理値の間のパスに変換できるので、補題は各方向一つずつの二つの含意から組み立てられる。

lookup-spec : ∀ {n} (g : Fin n → V ℓ) (i : Fin n) (v : V ℓ)
  → (pr (# (toℕ i)) v ∈ env g) ≡ ((v ≡ g i) , setIsSet v (g i))
lookup-spec {n} g i v = ⇔toPath fwd bwd
  where
  step : (lj : Lift {ℓ-zero} {ℓ} (Fin n))

順方向は切り捨てられた証拠に作用するので、場合分けは明示的な項目上の通常の関数として切り出される。入力は、グラフのある項目が問われた対と等しいというパスであり、出力は目標の v ≡ g i である。目標が命題であるため、切り捨てをそこへ消去することは正当であり、項目が通常のデータとして取り出されることはない。

       → pr (# (toℕ (lower lj))) (g (lower lj)) ≡ pr (# (toℕ i)) v
       → v ≡ g i
  step lj e = sym (ps .snd) ∙ cong g (inj-toℕ (#-inj′ (ps .fst)))
    where
    ps : (# (toℕ (lower lj)) ≡ # (toℕ i)) × (g (lower lj) ≡ v)

対の単射性が仮定された等式を、鍵のパスと値のパスに分解する。値のパスを逆向きにしたものが目標の半分である。鍵のパスは二つの数項が一致することを言い、数項の単射性と自然数への埋め込みがそれを添字自身の等式に変え、g を適用して残りの半分を得る。逆方向は i の項目を直接示する。切り捨てられた証拠は持ち上げられた索引であり、パスは対の構成子を逆向きの仮定に適用して埋められる。正準な証拠は選ばれず、証拠の一意性も主張されない。

    ps = pr-inj e
  fwd : ⟨ pr (# (toℕ i)) v ∈ env g ⟩ → v ≡ g i
  fwd = rec₁ (setIsSet v (g i)) (λ { (lj , e) → step lj e })
  bwd : v ≡ g i → ⟨ pr (# (toℕ i)) v ∈ env g ⟩
  bwd e = ∣ lift i , cong (pr (# (toℕ i))) (sym e) ∣₁

後者となる添字を認識する

有界論理式 sucAt i j は、j での値が i での値の von Neumann 後者であることを表す。sucAt-adequate は、環境の下でのこの論理式の充足が、ちょうどこの二つの値の等しいことであることを証明する。

環境の拡張はすべての添字を一つずつずらし、数項の上ではこのずれが von Neumann 後者にあたる。したがって、束縛子の内側へ降りていく証明書の機構は、「この添字はあの添字の後者である」と言えなければならない。言語には後者の記号がないため、この関係は所属だけを用いて三つの節で述べられる。小さい方が大きい方に属すること、小さい方に属するすべてが大きい方に属すること、そして大きい方に属するすべてが、命題的に小さい方に属するかそれと等しいかのいずれかであることである。

三つの有界な条件でそれができる。小さい方が大きい方に属すること、小さい方への所属が大きい方へ移ること、そして大きい方への所属は切り捨てられた形で分類され、小さい方に属するか小さい方と等しいかのいずれかであることである。有界量化子は var zero を束縛し、量化子の本体では他の変数はずらしたスロットで読まれるため、本体の var (suc i) は降りる前の var i の値を指す。第二と第三の節は、大きい方が小さい方の要素と小さい方自身のほかに要素を持たないことを、まさに述べており、これがその後者であることの外延的な内容である。有界性は Δ₀-sucAt によって別途記録される。連言、有界な全称量化、そして葉にあたる所属と等式は、いずれも Δ₀ を保つ。

sucAt : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n
sucAt i j = (var i ∈̇ var j)
         ∧̇ ((∀̇∈ (var i) (var zero ∈̇ var (suc j)))
         ∧̇ (∀̇∈ (var j) ((var zero ∈̇ var (suc i)) ∨̇ (var zero ≐ var (suc i)))))

Δ₀-sucAt : ∀ {n} (i j : Fin n) → Δ₀ (sucAt i j)

妥当性の証明は、まず集合のレベルで述べたホスト側の特徴づけに依拠する。それは、三つの論理式の節を集合 I と J についての事実として読んだとき、それらが成り立つのは、J と sucV I が集合として等しいとき、ちょうどそのときだというものである。

Δ₀-sucAt i j = δ-∧ δ-∈ (δ-∧ (δ-∀∈ δ-∈) (δ-∀∈ (δ-∨ δ-∈ δ-≐)))

private
  suc-char : (I J : V ℓ)
    → ⟨ I ∈ J ⟩
    → ((z : V ℓ) → ⟨ z ∈ I ⟩ → ⟨ z ∈ J ⟩)

順方向の補題は、三つの節を仮定として、今度は集合のレベルで取る。I が J に属すること、I への所属が J へ移ること、そして J の各要素は切り捨てられた形で I に属するか I と等しいかのいずれかであることである。結論はパス J ≡ sucV I であり、所属同士の双条件ではなく集合の本当の等式である。

    → ((z : V ℓ) → ⟨ z ∈ J ⟩ → ∥ ⟨ z ∈ I ⟩ ⊎ (z ≡ I) ∥₁)
    → J ≡ sucV I
  suc-char I J hIJ mono cover = extensionality J (sucV I) (sub₁ , sub₂)
    where
    sub₁ : ⟨ J ⊆ sucV I ⟩

等式は外延性によって作られ、二つの包含に分けられる。第一の包含は J の各要素を送る。分類の仮定は切り捨てられた選言を与え、各選言肢は「sucV I に属する」という命題値の対象へと消去される。左の場合、要素は後者の合併の枝を通して移り、右の場合、要素は I 自身であり、それは自分自身を頂点要素として sucV I に属する。

    sub₁ z z∈ₛJ = rec₁ (⟨ z ∈ₛ sucV I ⟩isProp)
      (⊎-rec
        (λ h → ∈∈ₛ {a = z} {b = sucV I} .fst (∈sucV-inl {A = I} {x = z} h))
        (λ e → subst (λ w → ⟨ w ∈ₛ sucV I ⟩) (sym e)
                 (∈∈ₛ {a = I} {b = sucV I} .fst (self∈sucV I))))

第二の包含は sucV I の要素を J の方へ読み戻す。後者への所属は二つの場合を持つ消去子によって分類され、分類の仮定の切り捨てがここで消費される。消去子の対象が命題 z ∈ J であるため、切り捨てられた分類についての場合分けが正当化される。二つの場合は、すでに手元にある節をそれぞれ使い、要素を I から移すか、I へと書き換える。

      (cover z (∈∈ₛ {a = z} {b = J} .snd z∈ₛJ))
    sub₂ : ⟨ sucV I ⊆ J ⟩
    sub₂ z z∈ₛs = ∈∈ₛ {a = z} {b = J} .fst
      (∈sucV-elim {A = I} {x = z} {P = ⟨ z ∈ J ⟩} (⟨ z ∈ J ⟩isProp)
        (∈∈ₛ {a = z} {b = sucV I} .snd z∈ₛs)

逆の補題 suc-intro は特徴づけを逆向きに用いる。J ≡ sucV I が与えられると、最初の二条件は後者集合についての所属の事実を J へ輸送して得られる。第三条件では J の要素を sucV I へ輸送し、後者への所属の消去子を適用して、必要な切り捨てられた分類を直接得る。したがってこの方向は、仮定として与えられた切り捨てられた分類を消去するものではない。

        (λ h → mono z h)
        (λ e → subst (λ w → ⟨ w ∈ J ⟩) (sym e) hIJ))

  suc-intro : (I J : V ℓ) → J ≡ sucV I
    → ⟨ I ∈ J ⟩
    × (((z : V ℓ) → ⟨ z ∈ I ⟩ → ⟨ z ∈ J ⟩)

各条件は、sucV I に関する所属の事実を仮定されたパスに沿って輸送することで作られる。向きは、事実が J の側に着くように選ぶ。第一の条件は「I が自身の後者に属する」という事実を輸送し、第二の条件は移行規則 ∈sucV-inl を要素ごとに輸送する。

    × ((z : V ℓ) → ⟨ z ∈ J ⟩ → ∥ ⟨ z ∈ I ⟩ ⊎ (z ≡ I) ∥₁))
  suc-intro I J e =
      subst (λ w → ⟨ I ∈ w ⟩) (sym e) (self∈sucV I)
    , (λ z h → subst (λ w → ⟨ z ∈ w ⟩) (sym e) (∈sucV-inl {A = I} {x = z} h))
    , (λ z z∈J → ∈sucV-elim {A = I} {x = z} {P = ∥ ⟨ z ∈ I ⟩ ⊎ (z ≡ I) ∥₁} squash₁

第三の条件は J の要素の分類であり、その対象は切り捨てられた選言そのものである。後者の消去子はこの切り捨てを消除の対象として適用されるので、二つの分岐はいずれも、対応する枝を切り捨て直すだけで応えられる。三つの条件がそろえば、妥当性の主張は lookup-spec と同じ形を取る。γ が sucAt i j を充足するという命題とは、j での値が i での値の von Neumann 後者と等しいことである。

        (subst (λ w → ⟨ z ∈ w ⟩) e z∈J)
        (λ h → ∣ inl h ∣₁)
        (λ q → ∣ inr q ∣₁))

sucAt-adequate : ∀ {n} (i j : Fin n) (γ : Vec (V ℓ) n)
  → (γ ⊨ sucAt i j) ≡ ((⟦ var j ⟧ γ ≡ sucV (⟦ var i ⟧ γ)) , setIsSet _ _)

二つの補題は妥当性の主張にちょうどはまる。順方向では、連言の充足が三つの条件にほどけ、suc-char がそれを三つの仮定として受け取り意味論の等式へ変える。結論が命題であるため、量化子データの切り捨てられた構造は消去を正しく通過する。逆方向では、suc-intro が意味論の等式から三つの条件を作る。二方向が合成されて一つの真理値のパスになり、それが妥当性補題の姿である。

sucAt-adequate i j γ = ⇔toPath
  (λ { (h₁ , h₂ , h₃) → suc-char (⟦ var i ⟧ γ) (⟦ var j ⟧ γ) h₁ h₂ h₃ })
  (suc-intro (⟦ var i ⟧ γ) (⟦ var j ⟧ γ))

一つの項目をずらす

shiftPairAt p' p は、p にある対の数項の鍵をその von Neumann 後者に置き換え、値を変えずに得られる対が p' にあることを認識する。

環境を拡張すると、鍵 0 に新しい項目を挿入するだけでなく、既存の項目の番号も付け替わる。鍵 # i だったものが鍵 # (suc i) になるのである。この節ではその付け替えの一歩を切り出し、有界な記述を与える。一つの有界量化子が束縛できるのは集合の一つの要素だけで、Kuratowski 対の一つの要素からは添字と値が一度に一つずつしか得られないため、論理式は五つの有界量化子を順に重ね、二つの項目、それぞれの添字、そして共有される値を同時に手元に置く。本体は対読み取りの章の二つの Kuratowski 読み取りと前節の後者の読み取りであり、合わせて、二つの項目が同じ値を共有し鍵が一歩の後者だけ違うことを正確に述べる。

この論理式は、p の値に対する五重の有界量化である。各有界存在量化子は環境に一つのスロットを加えるので、束縛された証人はすでに入った量化子の数で決まる位置に現れる。最初の三つは p の項目、その添字、その値を捉える。

shiftPairAt : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n
shiftPairAt p' p =
  ∃̇∈ (var p)
    (∃̇∈ (var zero)
      (∃̇∈ (var (suc zero))

残りの二つの量化子は p' の項目とその添字を捉える。ここで本体は、元の項目、その添字、その値、ずらされた項目、そしてずらされた添字の五つを同時に使える。

        (∃̇∈ (var (suc (suc (suc p'))))
          (∃̇∈ (var zero)
            ( prAt (suc (suc (suc (suc (suc p)))))
                   (suc (suc (suc zero))) (suc (suc zero))
            ∧̇ ( prAt (suc (suc (suc (suc (suc p'))))) zero (suc (suc zero))

本体は、この五つの証人についての三つの有界な主張の連言である。二つの Kuratowski 読み取りは、元の項目がその添字と値の対であり、ずらされた項目がずらされた添字と同じ値の対であると言い、後者の読み取りは、ずらされた添字が元の添字の von Neumann 後者であると言う。合わせて読めば、ずらされた項目は一歩の後者だけ高い鍵で同じ値を担っている。

            ∧̇ sucAt (suc (suc (suc zero))) zero ))))))

shiftPairAt-adequate : ∀ {n} (p' p : Fin n) (γ : Vec (V ℓ) n)
  → (γ ⊨ shiftPairAt p' p)
  ≡ (∥ Σ[ i ∶ V ℓ ] Σ[ v ∶ V ℓ ]
       ((⟦ var p ⟧ γ ≡ pr i v) × (⟦ var p' ⟧ γ ≡ pr (sucV i) v)) ∥₁ , squash₁)

妥当性の主張は、このような入れ子の量化の充足が実際に何を与えるかを記録する。すなわち「単に存在する」という主張である。スロット p の集合はある添字と値の対として単に存在し、スロット p' の集合はその添字の後者と同じ値の対として単に存在する、と言う。切り捨ては論理式に忠実である。式のどこにも特定の分解が選ばれておらず、それを選ぶ必要もない。

shiftPairAt-adequate p' p γ = ⇔toPath fwd bwd
  where
  P = ⟦ var p ⟧ γ
  P' = ⟦ var p' ⟧ γ
  Tgt : Type (ℓ-suc ℓ)

順方向は、切り捨てられた証人の連なりを切り捨てられた対象の一つの要素へ変換する。やり方は、五つの証人がすべて明示になった時点でそれらを一度に使うことである。その時点で使える仮定は本体の三つの連言肢であり、いずれも五つの束縛された証人全員で拡張した環境の中で述べられている。結論は、切り捨てられた存在の主張の一つの要素である。

  Tgt = ∥ Σ[ i ∶ V ℓ ] Σ[ v ∶ V ℓ ] ((P ≡ pr i v) × (P' ≡ pr (sucV i) v)) ∥₁

  conclude : (c i v c' j : V ℓ)
    → ⟨ (j ∷ c' ∷ v ∷ i ∷ c ∷ γ)
        ⊨ prAt (suc (suc (suc (suc (suc p))))) (suc (suc (suc zero))) (suc (suc zero)) ⟩
    → ⟨ (j ∷ c' ∷ v ∷ i ∷ c ∷ γ)

五つの証人が明示されれば、添字 i、値 v、二つのパス等式を切り捨てられた対象へ入れられる。三つの充足仮定は既に証明した妥当性補題を通してそれらの等式を与え、得られたパスに沿う輸送が端点を対象に合わせる。外側の対象が命題であることは周囲の切り捨て消去に必要であるが、パスに沿う輸送そのものにはその仮定は要らない。

        ⊨ prAt (suc (suc (suc (suc (suc p'))))) zero (suc (suc zero)) ⟩
    → ⟨ (j ∷ c' ∷ v ∷ i ∷ c ∷ γ) ⊨ sucAt (suc (suc (suc zero))) zero ⟩
    → Tgt
  conclude c i v c' j sat₁ sat₂ sat₃ =
    ∣ i , v

対の読み取りに対する妥当性補題は、スロット p での充足仮定を再解釈する。それは、そこにある項目が束縛された添字と束縛された値の Kuratowski 対であることを、ちょうど述べている。これにより最初の充足の証明が、記録された二つの等式のうちの第一、すなわち P ≡ pr i v に変わる。

    , subst ⟨_⟩
        (prAt-adequate (suc (suc (suc (suc (suc p)))))
          (suc (suc (suc zero))) (suc (suc zero)) (j ∷ c' ∷ v ∷ i ∷ c ∷ γ))
        sat₁
    , (subst ⟨_⟩

二つ目の対の読み取りの仮定からは等式 P' ≡ pr j v が、後者の読み取りの仮定からは j ≡ sucV i が得られる。後者を前者に合成し、対の第一成分に後者の操作を作用させれば、記録された第二の等式 P' ≡ pr (sucV i) v が生まれる。これと第一の等式を合わせたものがまさに目標である。二つの項目は値を共有し、第二の鍵は第一の鍵の von Neumann 後者である。

        (prAt-adequate (suc (suc (suc (suc (suc p'))))) zero (suc (suc zero))
          (j ∷ c' ∷ v ∷ i ∷ c ∷ γ))
        sat₂
       ∙ cong (λ z → pr z v)
          (subst ⟨_⟩

組み上げられた添字、値、二つの等式は、切り詰められて目標の中へ入る。これで妥当性の順方向が完成する。この方向は五つの量化子を一度に一つずつほどいていく。各量化子は切り詰められた存在なので、各消除は命題へ着地しなければならない。目標が切り詰められているのは、まさにこの消除の入れ子を正当化するためである。

            (sucAt-adequate (suc (suc (suc zero))) zero (j ∷ c' ∷ v ∷ i ∷ c ∷ γ))
            sat₃))
    ∣₁

  fwd : ⟨ γ ⊨ shiftPairAt p' p ⟩ → Tgt
  fwd = rec₁ squash₁ (λ { (c , _ , h₁) → rec₁ squash₁

最も内側の消除が三つの充足の証明に到達し、順方向の証明はこれで完成する。五つの証人が消除の外で通常のデータになることは決してない。各消除は切り詰められた一層を命題の中へ消費するので、証人はその連鎖の中にのみ存在する。

    (λ { (i , _ , h₂) → rec₁ squash₁
      (λ { (v , _ , h₃) → rec₁ squash₁
        (λ { (c' , _ , h₄) → rec₁ squash₁
          (λ { (j , _ , sat₁ , sat₂ , sat₃) → conclude c i v c' j sat₁ sat₂ sat₃ })
          h₄ })

逆方向は分析ではなく導入で進む。添字、値、そして二つのスロットを対応する対と同一視する等式が与えられれば、充足の証明を作らねばならない。そこで必要なものはすべて通常の集合の構成である。項目の集合は対の操作で作られ、その所属は成分の導入規則から従う。

        h₃ })
      h₂ })
    h₁ })

  build : (i v : V ℓ) → P ≡ pr i v → P' ≡ pr (sucV i) v → ⟨ γ ⊨ shiftPairAt p' p ⟩
  build i v eP eP' =

最外層の存在に対する最初の証人は、対 ⁅ i , v ⁆ そのものである。仮定の等式がスロット p の集合を pr i v と同一視し、成分の導入規則により非順序対 ⁅ i , v ⁆ はそれ自身の Kuratowski 符号化の内側にあるので、これはその集合に属する。等式に沿って輸送すれば所属が正しい側に移る。次に対を開くのに仕事は要らない。添字の証人は i、値の証人は v であり、それぞれ一つの成分規則が与える。

    ∣ ⁅ i , v ⁆
    , subst (λ z → ⟨ ⁅ i , v ⁆ ∈ z ⟩) (sym eP)
        (∈pair-introR {u = ⁅ i ⁆s} {v = ⁅ i , v ⁆} {y = ⁅ i , v ⁆} refl)
    , ∣ i , ∈pair-introL {u = i} {v = v} {y = i} refl
      , ∣ v , ∈pair-introR {u = i} {v = v} {y = v} refl

ずらされた項目は sucV i と v から同じ構成で作られ、ずらされた添字の証人は後者の集合そのものである。残りの節は仮定された二つの等式で満たされ、妥当性補題がそれらを充足の証明として読み戻す。順方向が仮想的な証人を分析しなければならなかったのに対し、逆方向は論理式が求める五つの証人を組み立てるだけで、切り詰められた外側の層は一つの明示的な証人で満たされる。

        , ∣ ⁅ sucV i , v ⁆
          , subst (λ z → ⟨ ⁅ sucV i , v ⁆ ∈ z ⟩) (sym eP')
              (∈pair-introR {u = ⁅ sucV i ⁆s} {v = ⁅ sucV i , v ⁆}
                            {y = ⁅ sucV i , v ⁆} refl)
          , ∣ sucV i

最も内側の証人はずらされた項目 ⁅ sucV i , v ⁆ であり、その添字の証人は後者の集合 sucV i そのものである。これは Kuratowski 対の左成分規則で導入される。残るのは二つの項目に関する節である。第一の節は仮定された等式 eP : ⟦ var p ⟧ γ ≡ pr i v から埋められる。この節は五回拡張された環境で評価される。スロット 0 から 4 に sucV i、ずらされた対、v、i、元の対が並び、束縛された変数がこれらのスロットを占めるため、スロット p が読む値はそこでも ⟦ var p ⟧ γ であり、これは eP の左辺そのものである。対の読み取りの妥当性補題はこの節の充足をその等式と同一視するので、対称な妥当性のパスに沿って eP を輸送すれば第一の節が満たされる。

            , ∈pair-introL {u = sucV i} {v = v} {y = sucV i} refl
            , subst ⟨_⟩
                (sym (prAt-adequate (suc (suc (suc (suc (suc p)))))
                  (suc (suc (suc zero))) (suc (suc zero))
                  (sucV i ∷ ⁅ sucV i , v ⁆ ∷ v ∷ i ∷ ⁅ i , v ⁆ ∷ γ)))

項目に関する第二の節も同じやり方で eP' から埋められる。スロット p' の対の読み取りは添字をスロット 0 から読むが、そこには今 sucV i が入っており、値は v の入るスロット 2 から読む。したがって妥当性補題が期待する等式はちょうど ⟦ var p' ⟧ γ ≡ pr (sucV i) v、すなわち第二の仮定である。ここでずらされた項目そのものを分解する必要はない点に注意してほしい。二つの対の読み取りが二つの分解を与え、後者の読み取りはスロット 0 にスロット 3 の後者が入っているため refl で満たされ、新しい鍵が古い鍵の後者であり値が保たれていることを記録する。

                eP
            , subst ⟨_⟩
                (sym (prAt-adequate (suc (suc (suc (suc (suc p'))))) zero (suc (suc zero))
                  (sucV i ∷ ⁅ sucV i , v ⁆ ∷ v ∷ i ∷ ⁅ i , v ⁆ ∷ γ)))
                eP'

本体の最後の連言肢は、前節の後者の読み取りを二つの添字の証人に適用したものである。組み上げた環境では、スロット 3 の値が添字 i であり、スロット 0 の値がその von Neumann 後者 sucV i である。したがってこの読み取りの特徴づけは自反パス sucV i ≡ sucV i によって与えられ、その妥当性補題を通して充足の節へと輸送される。これで本体の三つの主張がすべて成立する。二つの項目が値を共有する本物の対であり、第二の鍵が第一の鍵の後者である、ということが。これこそ一項目分の番号付け替えの数学的内容である。

            , subst ⟨_⟩
                (sym (sucAt-adequate (suc (suc (suc zero))) zero
                  (sucV i ∷ ⁅ sucV i , v ⁆ ∷ v ∷ i ∷ ⁅ i , v ⁆ ∷ γ)))
                refl
            ∣₁

残るのは、五重に入れ子になった有界存在量化子をまたぐ整理である。各層は命題なので、一つずつ証人を示し、それを「単に存在する」として封入することは正当である。候補が競合していたわけではないので、候補の中から選択が行われることもない。各存在量化子に証人が揃えば、論理式全体の充足の証明が組み上がる。

          ∣₁
        ∣₁
      ∣₁
    ∣₁

逆方向で妥当性定理が閉じる。入力は「添字と値、そして二つの等式が存在する」という切り詰められた主張であり、出力は充足の証明、それ自体命題である。切り詰めを命題値の対象へ消除することはまさに規則が許すところなので、仮定された対の分解は消除の内部で使える。ただし、消除の外では通常のデータとして取り出されることはない。構成された証人は論理式の各節と一致し、次の同一視が完成する。ずらしの論理式の充足とは、真理値として、二つの項目が対として値を共有し鍵が後者関係にあるという切り詰められた主張なのである。

  bwd : Tgt → ⟨ γ ⊨ shiftPairAt p' p ⟩
  bwd = rec₁ (⟨ γ ⊨ shiftPairAt p' p ⟩isProp)
    (λ { (i , v , eP , eP') → build i v eP eP' })

空の項目を符号化する

拡張された環境の新しい第 0 項目は、タグ # 0 を付された Kuratowski 対であり、# 0 は定義により空集合である。本節で構成する読み取りは、このような対を、タグをその数学的性質を通してのみ言及することで認識する。すなわち、ある要素が空であるということを、偽の論理式への有界量化で表し、定数を一切必要としない。三つの論理式 sgl0At、pair0At、tag0At はそれぞれ、ある集合が空集合の一元集合であること、空集合と与えられた集合の非順序対であること、そして両者から組み立てられるタグ付きの対であることを述べる。

メタレベルの仕事は、これらの論理式の充足の読み、すなわち集合が要素を持たないことを述べる述語 Empty' による表現を、対読み取りの章の prChar-fwd と prChar-bwd がすでに受け入れる形、つまり空集合が名指しで現れる形へ変換することである。要素を持たない集合は外延性により ∅ と等しいので、二つの表現は同じ数学を述べている。そして妥当性補題 tag0At-adequate は、タグの読み取りの充足を、「タグ付きの集合が pr ∅ を第二のスロットの値に作用したものと等しい」という等式と同一視する。

最初の読み取りは、空集合を名指しすることなく一元集合 {∅} を記述する。sgl0At k は k の値について二つの有界な節を連言する。すなわち、本体 ∀̇∈ (var zero) ⊥̇ を満たす要素が命題的に一つあることと、すべての要素がそれを満たすことである。有界な量化子の下では、本体 ⊥̇ は量化された要素が自身の要素を持たないとき、そのときに限って成り立つので、各節はその主語が空であると言っている。存在の節があるおかげで値が非空であることが保証される。これがなければ、空集合自身も条件を満たしてしまう。二つの節を合わせると、k の値は要素を持ち、その要素がすべて空集合であり、これは外延的にちょうど {∅} である。

sgl0At : ∀ {n} → Fin n → Formula (V ℓ) n
sgl0At k = (∃̇∈ (var k) (∀̇∈ (var zero) ⊥̇))
        ∧̇ (∀̇∈ (var k) (∀̇∈ (var zero) ⊥̇))

pair0At : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n
pair0At k j = (∃̇∈ (var k) (∀̇∈ (var zero) ⊥̇))

第二の読み取り pair0At k j は非順序対 {∅, W} を記述する。ここで W は元の割り当てのスロット j の値であり、新しい束縛子の内側では suc j が同じ値を指す。三つの節は、k の値に空な要素が命題的に存在すること、j の値がそれに属すること、そしてそのすべての要素が命題的に空であるか W と等しいか、である。第一の節は単集合の読み取りが使ったのと同じ空要素の存在であり、第三の節は第一成分を ∅ に固定した対の分類である。第三の論理式 tag0At s x はこの二つの読み取りを組み合わせる。s の値は空単集合の節を満たす要素を命題的に持ち、空対の節を満たす要素を命題的に持ち、そのすべての要素は命題的にいずれかを満たす。

           ∧̇ ((var j ∈̇ var k)
           ∧̇ (∀̇∈ (var k) ((∀̇∈ (var zero) ⊥̇) ∨̇ (var zero ≐ var (suc j)))))

tag0At : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n
tag0At s x = (∃̇∈ (var s) (sgl0At zero))
          ∧̇ ((∃̇∈ (var s) (pair0At zero (suc x)))

メタレベルでは、空性は private な述語 Empty' z で表される。これは z への任意の所属から空の型 ⊥* の要素を導く関数であり、z が要素を持たないことを表す。空の型なのは ⊥* であり、Empty' z はその型へ至る関数型である。対象言語の偽の論理式 ⊥̇ は構文なので、これとは区別される。最初の補題 empty'→∅ が、名指しされた空集合への橋となる。Empty' が成り立つ集合はすべて ∅ と等しい、というものである。

          ∧̇ (∀̇∈ (var s) (sgl0At zero ∨̇ pair0At zero (suc x))))

private
  Empty' : V ℓ → Type (ℓ-suc ℓ)
  Empty' z = (y : V ℓ) → ⟨ y ∈ z ⟩ → ⊥* {ℓ-suc ℓ}

  empty'→∅ : (z : V ℓ) → Empty' z → z ≡ ∅

この橋の証明は外延性であり、どちらの向きも空虚に成り立つ。各 y が z に属することと ∅ に属することがちょうど一致することを示すには、y が z に属すると仮定する。その所属に Empty' z を適用すれば空の型の住人が得られ、そこから何でも、特に ∅ への所属が従う。逆の向きでは、∅-empty が ∅ へのあらゆる所属を反駁し、その反駁から同じく z への所属が従う。逆向きの橋 ∅→empty' は定義的なパスだけで足りる。z への所属を e : z ≡ ∅ に沿って輸送すれば ∅ の中に落ち、そこで再び ∅-empty が矛盾を与える。こうして Empty' z と z ≡ ∅ は取り替え可能である。

  empty'→∅ z hz = extensionalV (λ y → ⇔toPath
    (λ h → ⊥*-rec (hz y h))
    (λ h → ⊥*-rec (lift {j = ℓ} (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst h)))))

  ∅→empty' : (z : V ℓ) → z ≡ ∅ → Empty' z
  ∅→empty' z e y y∈z = lift (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst (subst (λ w → ⟨ y ∈ w ⟩) e y∈z)))

二つの読み取りの充足を展開すると、二つのメタレベルの包みの形になる。EmptySgl w は、「w の空な要素が存在する」という切り詰められた存在と、「すべての要素が空である」という切り詰められていない全称の節からなる。EmptyPair W w は切り詰められた空要素の存在を保ち、残りを W の w への所属と、切り詰められた分類、すなわちすべての要素が命題的に空であるか W と等しいか、に置き換える。切り詰めの位置は、論理式の有界存在量化子と切り詰められた選言が置いた場所とまさに一致する。特に、選ばれた対の分解が取り出されることは決してない。

  EmptySgl : V ℓ → Type (ℓ-suc ℓ)
  EmptySgl w = ∥ Σ[ z ∶ V ℓ ] (⟨ z ∈ w ⟩ × Empty' z) ∥₁
            × ((z : V ℓ) → ⟨ z ∈ w ⟩ → Empty' z)

  EmptyPair : V ℓ → V ℓ → Type (ℓ-suc ℓ)
  EmptyPair W w = ∥ Σ[ z ∶ V ℓ ] (⟨ z ∈ w ⟩ × Empty' z) ∥₁

対応する包みは空集合を直接名指しする。SglOf∅ w は、∅ が w に属し w のすべての要素が ∅ と等しいと主張する。証人が与えられているため、切り詰めは不要である。PairOf∅ W w は、∅ と W が w に属し、すべての要素が命題的に ∅ か W であると主張する。分類は切り詰められたままであり、階層の非順序対の所属と一致する。そこからどちらの側かを選び取ることはできない。これらはまさに、対読み取りの章の対の特徴づけが受け取る形であり、第一成分を ∅ に具体化したものである。したがって残る仕事のすべては、同じ所属の事実の二つの表現の間を行き来することである。

               × (⟨ W ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → ∥ Empty' z ⊎ (z ≡ W) ∥₁))

  SglOf∅ : V ℓ → Type (ℓ-suc ℓ)
  SglOf∅ w = ⟨ ∅ ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → z ≡ ∅)

  PairOf∅ : V ℓ → V ℓ → Type (ℓ-suc ℓ)
  PairOf∅ W w = ⟨ ∅ ∈ w ⟩ × (⟨ W ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → ∥ (z ≡ ∅) ⊎ (z ≡ W) ∥₁))

順方向の変換は、空な要素の存在という切り捨てられた主張を、∅ が w に属するという普通の事実へ変える。階層の集合への所属は命題なので、切り詰めを ⟨ ∅ ∈ w ⟩ へ消除するのは正当である。内部では、所属の証明と Empty' z の証明を伴って明示的に与えられた証人 z を、まず前の補題で ∅ と同一視し、その所属をこのパスに沿って輸送して ∅ の所属にする。EmptySgl w の残りの部分はそのまま変換される。切り詰められていない全称の節は w の各要素 z に対して Empty' z を与え、同じ補題がそれを z ≡ ∅ に書き換える。

  empty-member : (w : V ℓ) → ∥ Σ[ z ∶ V ℓ ] (⟨ z ∈ w ⟩ × Empty' z) ∥₁ → ⟨ ∅ ∈ w ⟩
  empty-member w = rec₁ (⟨ ∅ ∈ w ⟩isProp)
    (λ { (z , hz , ez) → subst (λ u → ⟨ u ∈ w ⟩) (empty'→∅ z ez) hz })

  EmptySgl→SglOf∅ : (w : V ℓ) → EmptySgl w → SglOf∅ w
  EmptySgl→SglOf∅ w (h₁ , hall) = empty-member w h₁ , (λ z hz → empty'→∅ z (hall z hz))

対の場合も同じ計画に従う。EmptyPair→PairOf∅ は第一成分に空要素の変換を再利用し、W の所属はそのまま保ち、分類を要素ごとに書き換える。すなわち、各要素が空であるか W と等しいかという切り捨てられた主張を、Empty' を ∅ との等しさに置き換えた対応する切り捨てられた主張へ写すのである。結果はまさに ∅ を基準とする分類であり、切り詰めは選ばれた側に解決されることなく全体を通じて保たれる。

  EmptyPair→PairOf∅ : (W w : V ℓ) → EmptyPair W w → PairOf∅ W w
  EmptyPair→PairOf∅ W w (h₁ , hW , hall) = empty-member w h₁ , hW
    , (λ z hz → map₁ (sumMap (empty'→∅ z) (λ e → e)) (hall z hz))

  SglOf∅→EmptySgl : (w : V ℓ) → SglOf∅ w → EmptySgl w
  SglOf∅→EmptySgl w (h∅ , hall) =

逆方向では証人を探す必要はまったくない。空集合が最初から名指しされているからである。SglOf∅→EmptySgl は切り詰められた証人を直接作る。∅ は仮定により w に属し、定義的なパス ∅ ≡ ∅ に逆向きの補題を適用すれば空であることが分かる。全称の節は同じ補題を逆の向きで変換する。PairOf∅→EmptyPair はこの証人を保ち、W の所属をそのまま引き継ぎ、分類の節を各点で書き換える。

      (∣ ∅ , (h∅ , ∅→empty' ∅ refl) ∣₁)
    , (λ z z∈w → ∅→empty' z (hall z z∈w))

  PairOf∅→EmptyPair : (W w : V ℓ) → PairOf∅ W w → EmptyPair W w
  PairOf∅→EmptyPair W w (h∅ , hW , hall) =
      (∣ ∅ , (h∅ , ∅→empty' ∅ refl) ∣₁)

この対の変換では、分類が逆向きに走る。∅ か W であると命題的に分かっている要素を、空であるか W と等しいかの要素へ変える。第一の分岐には ∅→empty' を使い、第二の分岐はそのままで構わない。続いてこの節は、両方向が共有するパターンを抽象化する。PairWitness P R Q は、Kuratowski 対の特徴づけが集合 Q から読み取る三つの節を束ねる。すなわち、P を持つ Q の要素の切り詰められた存在、R についても同様、そして Q のすべての要素に P か R のいずれかを割り当てる切り詰められた二分法である。

    , (hW , λ z z∈w → map₁ (⊎-rec (λ e → inl (∅→empty' z e)) (λ e → inr e))
        (hall z z∈w))

  PairWitness : (V ℓ → Type (ℓ-suc ℓ)) → (V ℓ → Type (ℓ-suc ℓ)) → V ℓ → Type (ℓ-suc ℓ)
  PairWitness P R Q = ∥ Σ[ w ∶ V ℓ ] (⟨ w ∈ Q ⟩ × P w) ∥₁
    × (∥ Σ[ w ∶ V ℓ ] (⟨ w ∈ Q ⟩ × R w) ∥₁

ここまでの内容は、一つの変換を三度適用したものにすぎない。map-witness は PairWitness P R Q と二つの各点の含意、すなわち各 P w を P' w に送るものと各 R w を R' w に送るものを受け取り、PairWitness P' R' Q を返す。これがまさにこの節全体の形である。空性に基づく述語と ∅ に基づく述語は、同じ集合についての同じ三節の構造を包んだ二つの形であり、四つの変換補題が必要な各点の含意を両方向に供給する。

    × ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ P y ⊎ R y ∥₁))

  map-witness : {P R P' R' : V ℓ → Type (ℓ-suc ℓ)} (Q : V ℓ)
    → ((w : V ℓ) → P w → P' w) → ((w : V ℓ) → R w → R' w)
    → PairWitness P R Q → PairWitness P' R' Q
  map-witness Q f g (h₁ , h₂ , h₃) =

そこで順方向の定理 prChar∅-fwd は、空性に基づく三つの仮定、すなわち tag0At の充足が現す切り詰められた形の仮定を受け取り、パス Q ≡ pr ∅ W を結論する。変換補題が一度適用され、仮定は ∅ に関する三つの節へ変わる。続いて一般の対の特徴づけが外延性により、Q を ∅ と W の Kuratowski 対と同一視する。切り詰められた証人が通常のデータとして取り出されることは決してなく、それらは変換の内部でのみ使われ、その出力は特徴づけが受け入れる命題の形をした節である。

      map₁ (λ { (w , hw , h) → w , hw , f w h }) h₁
    , map₁ (λ { (w , hw , h) → w , hw , g w h }) h₂
    , (λ y hy → map₁ (sumMap (f y) (g y)) (h₃ y hy))

prChar∅-fwd : (Q W : V ℓ)
  → ∥ Σ[ w ∶ V ℓ ] (⟨ w ∈ Q ⟩ × EmptySgl w) ∥₁

逆方向の定理 prChar∅-bwd はこれと鏡像である。パス Q ≡ pr ∅ W から出発し、一般の対の特徴づけを第一成分 ∅、第二成分 W で逆向きに走らせ、得られた各節を空性に基づく対応物へ変換して、三つの節を返す。両定理がそろえば、tag0At s x の充足は「スロット s の値がタグ付き対 pr ∅ (⟦ var x ⟧ γ) と等しい」という主張と互いに交換可能になり、これが次の節の拡張の条件が使う読みになる。

  → ∥ Σ[ w ∶ V ℓ ] (⟨ w ∈ Q ⟩ × EmptyPair W w) ∥₁
  → ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ EmptySgl y ⊎ EmptyPair W y ∥₁)
  → Q ≡ pr ∅ W
prChar∅-fwd Q W h₁ h₂ h₃ = prChar-fwd Q ∅ W (h .fst) ((h .snd) .fst) ((h .snd) .snd)
  where

中間述語 PairWitness によって、議論は Q の具体的な構成から独立になる。変わるのは二つの候補成分の各点での意味だけである。空であることを ∅ との等しさに置き換えるか、その逆に戻した後、切り捨てられた証人を開き直さずに一般の対の特徴づけを適用できる。

  h : PairWitness SglOf∅ (PairOf∅ W) Q
  h = map-witness Q EmptySgl→SglOf∅ (EmptyPair→PairOf∅ W) (h₁ , h₂ , h₃)

prChar∅-bwd : (Q W : V ℓ) → Q ≡ pr ∅ W
  → ∥ Σ[ w ∶ V ℓ ] (⟨ w ∈ Q ⟩ × EmptySgl w) ∥₁
  × (∥ Σ[ w ∶ V ℓ ] (⟨ w ∈ Q ⟩ × EmptyPair W w) ∥₁

妥当性補題は、これまでの読み取りと同じ形式で、真理値の間のパスとして述べられる。左辺は tag0At s x の充足であり、右辺は「スロット s の値が pr ∅ (⟦ var x ⟧ γ) と等しい」という命題である。これは空集合をタグとし第二成分にスロット x の値を持つ Kuratowski 対であり、V ℓ が h-集合であることから等号の型が命題である証明とともに包まれている。これはまさに、符号化された第 0 項目が空のタグと新しい値の対であることを言っている。

  × ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ EmptySgl y ⊎ EmptyPair W y ∥₁))
prChar∅-bwd Q W e = map-witness Q SglOf∅→EmptySgl (PairOf∅→EmptyPair W) (prChar-bwd Q ∅ W e)

tag0At-adequate : ∀ {n} (s x : Fin n) (γ : Vec (V ℓ) n)
                → (γ ⊨ tag0At s x) ≡ ((⟦ var s ⟧ γ ≡ pr ∅ (⟦ var x ⟧ γ)) , setIsSet _ _)
tag0At-adequate s x γ = ⇔toPath

証明は両方向でこの節の二つの補題を合成する。連言と三つの有界量子の充足を展開すると、左辺はちょうど、空単集合の要素の切り詰められた存在、空対の要素の切り詰められた存在、そして切り詰められた分類になる。これは prChar∅-fwd が受け取るものである。逆方向ではパス e が prChar∅-bwd に渡され、その出力は意味論が充足へと組み立て直す。どちらの向きも集合の構成方法を検査せず、空性はすべて Empty' と ∅ との等しいことの間の同値を通じて処理される。

  (λ { (h₁ , h₂ , h₃) → prChar∅-fwd _ _ h₁ h₂ h₃ })
  (λ e → prChar∅-bwd _ _ e)

環境を拡張する

割当てに値をひとつ前置きすると、二つのことが同時に起こる。新しい値が添字 0 に置かれ、すべての旧添字が一つずつ動くのである。本節は、有界論理式 consAt がこの変換を符号化されたグラフの上で正確に表すこと、そしてその妥当性が符号化された環境に対して成り立つことを証明する。

論理式は三つの節を持つ。新しい集合のある項目が空のタグと新しい値を持つこと、旧グラフのすべての項目がずらされて新しいグラフに現れること、そして新しいグラフのすべての項目が、その新しい項目であるか旧項目のずらしであること、である。妥当性の主張は、この論理式が二つの集合を cons に似た形で結びつけるだけだと言うのではない。関数 g と「旧スロットがグラフ env g と等しい」という仮定が与えられれば、新しいスロットからグラフ env (cons M g) へのパスが結論される。この等式の両辺はともに階層の集合なので、証明は外延的である。すなわち二つの包含を一要素ずつ示す。一つの方向では本章の読み取りで新しい集合の各要素を分類し、もう一つの方向では鍵ごとに cons M g のグラフを辿る。添字での一致は定義的である。suc k の数項は k の数項の後者だからである。

ホストレベルの操作 cons m g は Fin (suc n) 上の関数で、添字 0 では m を、添字 suc i では g i を返す。すなわち値を一つ前置きし、各旧値は添字が一つ動いてから同じ値を保つ。論理式 consAt e' m e は三つの環境変数を名指しする。e' の値が候補となる拡張グラフ、m の値が前置きされる要素、e の値が拡張されるグラフである。

cons : ∀ {ℓ'} {X : Type ℓ'} {n : ℕ} → X → (Fin n → X) → Fin (suc n) → X
cons m g zero    = m
cons m g (suc i) = g i

consAt : ∀ {n} → Fin n → Fin n → Fin n → Formula (V ℓ) n
consAt e' m e =

consAt の三つの節は cons の三つの定義等式と対応する。γ の下で読むと、e' の値はタグ付き対の読み取り tag0At zero (suc m) を満たす要素を命題的に一つ持ち、すなわちタグが空で第二成分が m の値である項目を保持する。e の値の各項目は、e' の値の中に自分のずらしが命題的に存在し、これは shiftPairAt で、旧項目を後ろのスロットに置いて述べられる。そして e' の値のすべての項目は、命題的に、そのタグ付き 0 項目であるか e の値の項目のずらしである。各部分式は有界量化子、等式、そして前の二つの読み取りから構成されるので、検査器は連言全体を Δ₀ として証明し、Δ₀-consAt が一度だけこれを記録する。

  (∃̇∈ (var e') (tag0At zero (suc m)))
  ∧̇ ((∀̇∈ (var e) (∃̇∈ (var (suc e')) (shiftPairAt zero (suc zero))))
  ∧̇ (∀̇∈ (var e') ((tag0At zero (suc m))
                   ∨̇ (∃̇∈ (var (suc e)) (shiftPairAt (suc zero) zero)))))

Δ₀-consAt : ∀ {n} (e' m e : Fin n) → Δ₀ (consAt e' m e)

妥当性補題は一つの追加仮定を持ち、これこそが結論を真にするものである。consAt の充足だけでは、新しい集合が古い集合と cons の関係にあることしか言えない。古い集合をグラフとして名指しするために、補題は長さ k の関数 g とパス ⟦ var e ⟧ γ ≡ env g を追加で受け取る。これが証明書の保持する符号化された形である。候補の環境は集合としてスロットに現れ、仮定がその集合を、それが符号化する割当てのグラフと同一視する。

Δ₀-consAt e' m e = checkΔ₀ (consAt e' m e) tt

consAt-adequate : ∀ {n} (e' m e : Fin n) (γ : Vec (V ℓ) n)
  {k : ℕ} (g : Fin k → V ℓ)
  → ⟦ var e ⟧ γ ≡ env g
  → (γ ⊨ consAt e' m e)

結論は新しいスロットに対する同種の同一視である。e' の値は cons M g のグラフと等しく、ここで M は m の値である。これまでの読み取りと同様に、主張は真理値の間のパスであり、等式の型の命題性は V ℓ の h-集合性から供給される。略称 M、E、E' が三つのスロットの値を名指しし、⇔toPath が主張を二つの包含へ帰着させる。

  ≡ ((⟦ var e' ⟧ γ ≡ env (cons (⟦ var m ⟧ γ) g)) , setIsSet _ _)
consAt-adequate e' m e γ {k} g hE = ⇔toPath fwd bwd
  where
  M = ⟦ var m ⟧ γ
  E = ⟦ var e ⟧ γ

補助的な shift-path は番号付け替えの算術を一度に記録する。符号化された二つの項目が対として等しければ、両側の鍵をそれぞれの von Neumann 後者に置き換え、値を保った項目もまた等しい、というものである。Kuratowski 対の単射性 pr-inj が仮定のパスを鍵のパスと値のパスに分解し、cong₂ がずらした対の構成子の下で再結合する。

  E' = ⟦ var e' ⟧ γ
  G' : Fin (suc k) → V ℓ
  G' = cons M g

  shift-path : {a b x y : V ℓ} → pr a x ≡ pr b y → pr (sucV a) x ≡ pr (sucV b) y
  shift-path {a} {b} {x} {y} e = cong₂ (λ a b → pr (sucV a) b) (p .fst) (p .snd)

順方向の包含は、論理式の第三の節を受け取り、それを本物の所属の主張に変える。その仮定は、E' の各要素 y が、命題的に、y を追加した環境でタグ付き 0 の読み取りを満たすか、あるいは E の要素で y へとずらされるものを証人とする有界存在を満たすかのいずれかである、と言う。目標は y が拡張後の割当てのグラフ env G' に属することである。仮定の形に注意してほしい。これは論理式の有界全称量化子が生むのとまさに同じ、切り詰められた選言である。

    where
    p : (a ≡ b) × (x ≡ y)
    p = pr-inj e

  classify : ((y : V ℓ) → ⟨ y ∈ E' ⟩
               → ∥ ⟨ (y ∷ γ) ⊨ tag0At zero (suc m) ⟩

切り詰められた選言は命題値の対象へしか消除できないが、env G' への所属はまさに命題である。二つの分岐はそれぞれ別に処理される。最初の分岐はタグ付き 0 の読み取りの充足を受け取り、グラフの鍵 0 を生み出す。

                 ⊎ ⟨ (y ∷ γ) ⊨ ∃̇∈ (var (suc e)) (shiftPairAt (suc zero) zero) ⟩ ∥₁)
           → (y : V ℓ) → ⟨ y ∈ E' ⟩ → ⟨ y ∈ env G' ⟩
  classify h₃ y y∈E' = rec₁ (⟨ y ∈ env G' ⟩isProp)
    (⊎-rec
      (λ tsat →

第一の分岐では、要素 y が y ∷ γ の中で tag0At zero (suc m) を満たし、この読み取りの妥当性補題が充足をパス y ≡ pr ∅ M に変換する。スロット 0 の値は y そのものであり、新しい束縛子の内側で suc m は元の割り当てのスロット m の値を指す。このパスを逆向きにすれば pr ∅ M ≡ y が得られ、これは鍵 0 における env G' の項目そのものである。G' zero は M に、0 の数項は空集合に計算されるからである。したがって証人はこのパスを伴う lift zero である。

        ∣ lift zero
        , sym (subst ⟨_⟩ (tag0At-adequate zero (suc m) (y ∷ γ)) tsat) ∣₁)
      (λ ssat → rec₁ (⟨ y ∈ env G' ⟩isProp)
        (λ { (p , p∈E , sh) → rec₁ (⟨ y ∈ env G' ⟩isProp)
          (λ { (li , peq) → rec₁ (⟨ y ∈ env G' ⟩isProp)

第二の分岐はずらしの場合で、入れ子になった三つの切り詰めを順に開く。有界存在の充足は、E の要素 p と、二項目の環境 p ∷ y ∷ γ に関するずらしの節を命題的に与え、shiftPairAt の妥当性補題がその節を、p ≡ pr i v かつ y ≡ pr (sucV i) v となる集合 i と v の単なる存在へ変換する。ここで二つのスロットの役割が重要である。shiftPairAt (suc zero) zero では旧項目が後ろのスロットに、ずらされたものがスロット 0 に置かれるため、y が後続の鍵を持つ対になるのである。

            (λ { (i , v , epv , eyv) →
                ∣ lift (suc (lower li))
                , sym (shift-path (sym epv ∙ sym peq))
                ∙ sym eyv ∣₁ })
            (subst ⟨_⟩ (shiftPairAt-adequate (suc zero) zero (p ∷ y ∷ γ)) sh) })

ずらしの場合では、古い項目の背後にある添字 i と値 v が明示できれば、env G' への所属は拡張後の割当てのグラフが持つ項目から直接組み立てられる。グラフは後続の鍵の位置で古い値を担うので、必要な証人は添字 suc (lower li) と、その項目から y へのパスである。このパスは三つの等式の合成である。古い項目が対 pr i v に等しいこと、両側の鍵を von Neumann 後者に置き換えると同じ値を持つずらされた鍵の対になること、そして env G' のその鍵での項目が y に等しいことである。この合成が記録しているのはまさにこの場合の数学的内容、すなわち新しい鍵が古い鍵の後者であり値が保たれるということである。

          (subst (λ z → ⟨ p ∈ z ⟩) hE p∈E) })
        ssat))
    (h₃ y y∈E')

  covered : ⟨ γ ⊨ ∃̇∈ (var e') (tag0At zero (suc m)) ⟩
          → ((p : V ℓ) → ⟨ p ∈ E ⟩

ずらしの場合にはもう一歩残っている。項目 p は E の要素として見つかったが、議論が必要とするグラフへの所属は env g の中にあり、仮定 E ≡ env g がこの所属をパスに沿って輸送する。グラフの内部では、最初の節で証明した参照の補題が、証人の指す添字の鍵に格納された値を特定する。これで第一の包含は完成である。新しい集合のすべての要素が命題的に拡張後の割当てのグラフに落ちる。

              → ⟨ (p ∷ γ) ⊨ ∃̇∈ (var (suc e')) (shiftPairAt zero (suc zero)) ⟩)
          → (y : V ℓ) → ⟨ y ∈ env G' ⟩ → ⟨ y ∈ E' ⟩
  covered h₁ h₂ y y∈G' = rec₁ (⟨ y ∈ E' ⟩isProp)
    (λ { (lj , eq) → byKey (lower lj) eq })
    y∈G'

逆向きの包含は、拡張後の割当てのグラフのすべての要素が新しい集合に属することを示さねばならない。グラフへの所属は切り詰められたファイバーのデータ、すなわちグラフの添字と、その添字の項目が与えられた要素に等しいというパスからなる。したがって要素 y はその添字と項目のパスとともに読み取られ、その後、証明は添字について場合分けして進む。cons の二つの定義等式が生むのはちょうど二種類の項目、添字 0 の新しい項目と、後続の添字にあるずらされた古い項目だからである。

    where
    byKey : (j : Fin (suc k)) → pr (# (toℕ j)) (G' j) ≡ y → ⟨ y ∈ E' ⟩
    byKey zero eq = rec₁ (⟨ y ∈ E' ⟩isProp)
      (λ { (q , q∈E' , tsat) →
        subst (λ z → ⟨ z ∈ E' ⟩)

0 の場合、項目の等式は定義計算により「空のタグと値 M を持つ項目が y に等しい」という主張に帰着する。論理式の第一の節は、新しい集合の要素 q で、そのタグ付き項目が空のタグと M の対であるものを命題的に与え、その妥当性補題が充足をちょうどその等式に変える。二つのパスを連結すれば q ≡ y となり、これに沿って q の所属を輸送すれば新しい集合への y の所属が得られる。この等式以外に q についての情報は使われないため、第一の節の内部の切り詰められた証人は、求められているとおり、命題の中へのみ消去される。後続の場合は議論を逆向きに走らせる。項目の等式が今や g の古い項目を名指しし、論理式の第二の節がそのずらしを新しい集合の中に生み出さねばならないのである。

          (subst ⟨_⟩ (tag0At-adequate zero (suc m) (q ∷ γ)) tsat ∙ eq)
          q∈E' })
      h₁
    byKey (suc i₀) eq = rec₁ (⟨ y ∈ E' ⟩isProp)
      (λ { (p' , p'∈E' , sh) → rec₁ (⟨ y ∈ E' ⟩isProp)

後続の場合、論理式のずらしの節は添字 i、値 v、そして二つの等式を与える。古い項目が対 pr i v に等しいことと、候補がずらされた対 pr (sucV i) v に等しいことである。目標は候補から要素 y へのパスであり、ファイバーの等式は後続の鍵にあるずらされたグラフの項目を提供し、それは y に等しくなる。後続の添字の数項は元の数項の後者なので、対 pr i v の両方の鍵をそれぞれの後者に置き換えると、ちょうどそのグラフの項目に着地する。三つの等式が合成されて必要なパスとなり、これに沿って候補の所属を輸送すればこの場合が閉じる。

        (λ { (i , v , epv , ep'v) →
          subst (λ z → ⟨ z ∈ E' ⟩)
            (ep'v
             ∙ shift-path (sym epv)
             ∙ eq)

まだ一つ入力が欠けていた。ずらしの節は充足の主張であり、その評価に使われる環境の第 2 スロットには、古い項目 pr (# (toℕ i₀)) (g i₀) そのものが入っていなければならない。この対応する所属を論理式の第二の節が供給する。参照の補題が使われるのはまさにここである。i₀ の鍵の位置で g のグラフはちょうど g i₀ を保持し、添字と refl からなる正準なファイバーがその所属を証する。これを「古い集合は g のグラフに等しい」という仮定に沿って輸送すれば、符号化された環境への所属になる。

            p'∈E' })
        (subst ⟨_⟩
          (shiftPairAt-adequate zero (suc zero) (p' ∷ pr (# (toℕ i₀)) (g i₀) ∷ γ)) sh) })
      (h₂ (pr (# (toℕ i₀)) (g i₀))
          (subst (λ z → ⟨ pr (# (toℕ i₀)) (g i₀) ∈ z ⟩) (sym hE) ∣ lift i₀ , refl ∣₁))

両方の包含が確立されれば、妥当性補題の順方向は累積階層の外延性への一度の訴えで済む。同じ元を持つ二つの集合は等しいからである。論理式の三つの節が、各要素 y に対して所属の比較の二方向を与える。新しい集合の要素から拡張後の割当てのグラフへ、そしてグラフから新しい集合へ、という方向である。この方向に読めば、論理式の充足は符号化されたグラフの間の等式へと変換される。補題の残りの方向は、そのような等式から充足を構成する。

  fwd : ⟨ γ ⊨ consAt e' m e ⟩ → E' ≡ env G'
  fwd (h₁ , h₂ , h₃) = extensionalV
    (λ y → ⇔toPath (classify h₃ y) (covered h₁ h₂ y))

  bwd : E' ≡ env G' → ⟨ γ ⊨ consAt e' m e ⟩
  bwd e'eq =