この章を読むか、対話型目次と依存グラフで別のルートを選べます。

対話型目次 · 依存グラフ

宇宙レベル ℓ を固定する。このレベルをパラメータとして保つことで、異なる宇宙を同一視せずに、必要な大きさで構成を具体化できる。

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

この章の目標は、対象言語に、割り当てられたある集合が他の二つの集合の Kuratowski 順序対であると認識させること、そして道すがら、Kuratowski 対を構成する単集合と非順序対も認識させることである。一階の論理式が語れるのは所属と等号だけなので、認識は外延的でなければならない。pr U W を認識するとは、所属だけを通して、どの要素をちょうど持つのかを言うことである。本章では有界な論理式を三つ構成する。sglAt は「この集合はあれの単集合である」、pairAt は「これはあの二つの非順序対である」、prAt はこれらを組み合わせて「これはあの二つの Kuratowski 対である」と読み取る式である。

最後の妥当性定理は正確な同一視である。任意の割当てに対して、prAt q u v の充足は真理値のパスであり、その先にあるのは「q の位置の値が、u と v の位置の値に pr を施した結果と等しい」という命題である。一方向の含意のようなより弱い主張はここでは行わない。

各論理式の量化子は指定された集合で限られ、自由変数の位置は引数として与えられる de Bruijn 添字なので、同じ式を任意の入れ子の深さで使える。すべての節が原子か有界量化子であるため、各読解式は Lévy 階層の Δ₀ である。

外側の目標は明確な所属の形を持つ。pr U W = ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆ である。外側の集合は非順序対で、第 1 の要素は U の単集合、第 2 の要素は U と W の非順序対である。したがって順序対の認識は、指定された二要素がともに存在し、すべての要素がそのどちらかであるという三条件に帰着する。最後の条件は命題的に切り詰められており、非順序対の所属の分類と一致する。これは選択肢の存在を記録するが、どちら側かは選ばない。

open import Cubical.Data.Sum using () renaming ( map to sumMap )

これらの記述を表す道具は、一階言語の有界フラグメントである。原子 _∈̇_ と _≐_、結合子 _∧̇_ と _∨̇_ は、各位置に割り当てられた集合の間の所属と等号を述べる。量化子 ∀̇∈ と ∃̇∈ は常に割り当てられた集合で限られる。これらだけから作られる論理式は Lévy 階層の有界クラス Δ₀ をなし、checkΔ₀ が構文的に検査する。

認識の対象は Kuratowski 符号化 pr で、pr U W = ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆ と定義される。順序対は、U の単集合と U と W の対という二つの集合の非順序対として提示されるのである。したがって認識の問題は、有界論理式で、ある集合が U の単集合である要素をひとつ、U と W の非順序対である要素をひとつ持ち、それ以外の要素を持たない、と言うことに帰着する。単集合と非順序対への所属にはそれぞれ分類があり、外延性が完全な所属の条件を集合の間の等号に変換する。

単集合と非順序対の所属には、階層での所属 ⟨ y ∈ b ⟩ と、それぞれの構成が用いる小さな所属の分類という同値な二つの形がある。∈∈ₛ が両者を結ぶ。単集合の分類はパス y ≡ u を与え、非順序対の分類は切り詰められた選択肢 ∥ (y ≡ u) ⊎ (y ≡ v) ∥₁ を与える。各所属の記述を両方向に証明すれば、⇔toPath が所属命題の同値を外延性に必要なパスへ変える。

意味論は、レベル ℓ-suc ℓ の hProp を真理値として取る。論理式は裸のブール値に評価されるのではなく、その値は命題であり、環境のもとでの論理式の充足それ自体が判定ではなく命題である。複合した論理式を読むとき、連言と選言はこれらの hProp 真理値に直接作用する。この命題的な設定が目標にとって重要である。有界論理式の充足を、集合とその符号化された対の等号のような外側の条件と、パスとして同一視できるからである。

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

この意味論の中で、定数解釈は V ℓ 上の恒等写像に固定される。言語の定数はただの集合であり、自分自身を表示するのである。したがって ⟦ var k ⟧ γ は環境 γ が位置 k に割り当てる値であり、論理式は割り当てられた集合を直接語ることができる。

  using ( ⁅_,_⁆; pairing-ax; ⁅_⁆s; SingletonPackage; module InfinitySet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( SetPackage )  -- lint-agda: keep (used qualified: SetPackage.classification)
open InfinitySet using ( #_ )

これが次の妥当性の主張を意味あるものにする。読解式 prAt の位置 q、u、v での充足が、真理値として、⟦ var q ⟧ γ と pr (⟦ var u ⟧ γ) (⟦ var v ⟧ γ) の等号と比較されるのである。

module Sem = FOL.Semantics 𝒮ᵥ
open Sem.At (V ℓ) id using ( _⊨_; ⟦_⟧ )

単集合と非順序対を特徴付ける

唯一の要素が u である集合は u の単集合であり、要素がちょうど u と v である集合はそれらの非順序対である。これらは対象言語の読解式が表すことになる外側の意味なので、メタレベルでここに一度証明する。どちらの特徴付けも同じ手法に依る。二つの集合が同じ要素を許すなら、外延性 extensionalV が点ごとの所属の同値を集合間のパスに変えるのである。

二つの方向は強さが異なる。⁅ u ⁆s の要素が u と等しいことは外側の切り詰めを伴わないパスであるが、⁅ u , v ⁆ の要素が u か v のどちらかであることは命題的に切り詰められた形でしか、つまり命題として丸められた選言でしか言えない。証明はこの区別を正確に保つ。

単集合への所属は SingletonPackage の分類によって完全に記述される。y が ⁅ u ⁆s に属するのは、y が u と等しいとき、かつそのときに限る。橋 ∈∈ₛ が階層本来の所属とこの小さい所属の間を行き来するので、∈sgl-elim は橋の前半と分類をつなげ、単なる所属の証明から実際のパス y ≡ u を取り出す。∈sgl-intro は同じ二段階を逆向きに進める。ここに丸めは一切ない。等号のパスはそのまま使え、V ℓ が h-集合であるため命題のままである。

∈sgl-elim : {u y : V ℓ} → ⟨ y ∈ ⁅ u ⁆s ⟩ → y ≡ u
∈sgl-elim {u} {y} h =
    SetPackage.classification (SingletonPackage u) y .fst (∈∈ₛ {a = y} {b = ⁅ u ⁆s} .fst h)

∈sgl-intro : {u y : V ℓ} → y ≡ u → ⟨ y ∈ ⁅ u ⁆s ⟩
∈sgl-intro {u} {y} e = ∈∈ₛ {a = y} {b = ⁅ u ⁆s} .snd

非順序対については、分類 pairing-ax が所属を選言で記述する。要素は u と等しいか、v と等しいかである。ここに丸めが現れる。∈pair-elim は所属の証明を、命題的に切り詰められた形でしか成り立たない選言 ∥ (y ≡ u) ⊎ (y ≡ v) ∥₁ に変える。下の分類が側の選択を命題として丸めて返すためで、それを丸めなしの直和型へ消去することはできない。逆に ∈pair-introL と ∈pair-introR はそれぞれ片側の明示的なパスを受け取り、それを「どちらか一方が成り立つという切り詰められた形」として封入して所属を得る。

    (SetPackage.classification (SingletonPackage u) y .snd e)

∈pair-elim : {u v y : V ℓ} → ⟨ y ∈ ⁅ u , v ⁆ ⟩ → ∥ (y ≡ u) ⊎ (y ≡ v) ∥₁
∈pair-elim {u} {v} {y} h = pairing-ax u v y .fst (∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .fst h)

∈pair-introL : {u v y : V ℓ} → y ≡ u → ⟨ y ∈ ⁅ u , v ⁆ ⟩
∈pair-introL {u} {v} {y} e = ∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .snd

二つ目の導入は一つ目と対称である。両方の構成への出入りの所属が揃ったので、外側の特徴付けを述べられる。sgl-char はこう言う。u が x に属し、x のすべての要素が u と等しいなら、x は u の単集合である、と。pair-char は二つの成分について同様のことを言い、「すべての要素」の節が命題的に切り詰められた選言になるだけである。どちらの結論も集合間のパスであり、後でどちらも読解式 prAt が表す節をちょうど供給する。

    (pairing-ax u v y .snd ∣ inl e ∣₁)

∈pair-introR : {u v y : V ℓ} → y ≡ v → ⟨ y ∈ ⁅ u , v ⁆ ⟩
∈pair-introR {u} {v} {y} e = ∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .snd
    (pairing-ax u v y .snd ∣ inr e ∣₁)

sgl-char : (x u : V ℓ) → ⟨ u ∈ x ⟩ → ((y : V ℓ) → ⟨ y ∈ x ⟩ → y ≡ u) → x ≡ ⁅ u ⁆s

二つの所属の仮定から x ≡ ⁅ u ⁆s を証明するには、外延性を点ごとに適用する。各 y について、命題 ⟨ y ∈ x ⟩ を ⟨ y ∈ ⁅ u ⁆s ⟩ と結ぶパスが必要であり、⇔toPath は同値からまさにそのようなパスを作る。順方向は「x のすべての要素は u に等しい」という仮定を使い、その後で単集合への所属を再導入する。これが sub₁ である。

sgl-char x u hu hall = extensionalV (λ y → ⇔toPath (sub₁ y) (sub₂ y))
  where
  sub₁ : (y : V ℓ) → ⟨ y ∈ x ⟩ → ⟨ y ∈ ⁅ u ⁆s ⟩
  sub₁ y hy = ∈sgl-intro (hall y hy)
  sub₂ : (y : V ℓ) → ⟨ y ∈ ⁅ u ⁆s ⟩ → ⟨ y ∈ x ⟩

逆向きの sub₂ は単集合への所属から出発し、x への所属を作らねばならない。消去がパス y ≡ u を与え、その逆方向に所属が輸送される。u が x に属し、y が u とパス一本分しか違わないなら、y も x に属する、というわけである。この「パスに沿った輸送」の型は、構成を直接比較する代わりの標準的な手段であり、本章の残りのすべての証明で繰り返し現れる。両方向が揃えば、⇔toPath が点ごとの同値を組み立て、extensionalV がパス x ≡ ⁅ u ⁆s を返す。

  sub₂ y hy = subst (λ z → ⟨ z ∈ x ⟩) (sym (∈sgl-elim hy)) hu

pair-char : (x u v : V ℓ) → ⟨ u ∈ x ⟩ → ⟨ v ∈ x ⟩
          → ((y : V ℓ) → ⟨ y ∈ x ⟩ → ∥ (y ≡ u) ⊎ (y ≡ v) ∥₁)
          → x ≡ ⁅ u , v ⁆
pair-char x u v hu hv hall = extensionalV (λ y → ⇔toPath (sub₁ y) (sub₂ y))

pair-char の証明は同じ計画に従うが、新しい特徴が一つある。「すべての要素」の仮定は丸められているので、順方向の sub₁ は y がどちらの側かでパターンマッチできない。代わりに、rec₁ で丸めを、実際に命題値である所属の命題 ⟨ y ∈ ⁅ u , v ⁆ ⟩ へ消去し、直和の二つの側で場合分けする。u に等しい要素は対に左から、v に等しい要素は右から入る。これが命題的に切り詰められた選言の事実を用いる正しいやり方である。

  where
  sub₁ : (y : V ℓ) → ⟨ y ∈ x ⟩ → ⟨ y ∈ ⁅ u , v ⁆ ⟩
  sub₁ y hy = rec₁ (⟨ y ∈ ⁅ u , v ⁆ ⟩isProp)
    (⊎-rec (∈pair-introL {u = u} {v = v}) (∈pair-introR {u = u} {v = v})) (hall y hy)
  sub₂ : (y : V ℓ) → ⟨ y ∈ ⁅ u , v ⁆ ⟩ → ⟨ y ∈ x ⟩

逆向きの sub₂ はこれを鏡写しにする。⁅ u , v ⁆ への所属から ∈pair-elim で丸められた選言を得て、それを所属の命題 ⟨ y ∈ x ⟩ へ消去し、各分岐で取り戻したパスに沿って対応する仮定 hu か hv を逆方向へ輸送する。こうして sub₁ と sub₂ は、対の構成の分類だけを材料に x への所属を作り出し、extensionalV が点ごとの結果を x ≡ ⁅ u , v ⁆ へ引き上げる。

  sub₂ y hy = rec₁ (⟨ y ∈ x ⟩isProp)
    (⊎-rec (λ e → subst (λ z → ⟨ z ∈ x ⟩) (sym e) hu)
             (λ e → subst (λ z → ⟨ z ∈ x ⟩) (sym e) hv)) (∈pair-elim hy)

メタレベルの Kuratowski 対

読解式 prAt は、集合 Q について、U の単集合である要素をひとつ持ち、U と W の非順序対である要素をひとつ持ち、しかもすべての要素がこのどちらかである、と言う。この節は、まさにこの三つの条件が Q を Kuratowski 対 pr U W = ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆ と等しくすること、およびその逆を証明する。下の二つの補助述語は条件を節ごとに記録し、その形は有界論理式の充足が展開されていく形とちょうど同じである。そのため、妥当性の節の意味論的補題は、仮定をここで証明したメタレベルの補題にそのまま渡すことができ、同じことを二度証明する必要がない。

最初の述語 SglOf U w は、w が U の単集合であることを所属の言葉だけで述べる。U が w に属し、w に属する任意の z は打ち切りなしに U と等しい、ということである。二つ目の PairOf U W w は、w が非順序対であることを述べる。U と W がともに w に属し、すべての要素が命題的に切り詰められた形でこのどちらかである、つまり命題として丸められた選言である。両方がレベル ℓ-suc ℓ に住むのは、V ℓ のすべての集合を量化するのに一レベル必要で、それが意味論が真理値を取るレベルと同じだからである。

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

  PairOf : V ℓ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
  PairOf U W w =

パッケージは、前節の特徴付けを通して等号と結び付く。w が SglOf U を持てば、その二つの成分はちょうど sgl-char の仮定であり、sgl-char はパス w ≡ ⁅ U ⁆s を返す。同様に pair-char は PairOf のパッケージを w ≡ ⁅ U , W ⁆ に変える。つまりパッケージは対応する構成との等号の証明書であり、w がどう作られたかを検査することなしに得られる。

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

  sglOf→≡ : {U w : V ℓ} → SglOf U w → w ≡ ⁅ U ⁆s
  sglOf→≡ {U} {w} (hu , hall) = sgl-char w U hu hall

  pairOf→≡ : {U W w : V ℓ} → PairOf U W w → w ≡ ⁅ U , W ⁆
  pairOf→≡ {U} {W} {w} (hu , hv , hall) = pair-char w U W hu hv hall

逆向きのデータも存在する。構成そのものが自分のパッケージを持つのである。⁅ U ⁆s については、U の所属は反射パスでの ∈sgl-intro から、すべての要素が U と等しいことは ∈sgl-elim から従う。非順序対も、二つの導入と ∈pair-elim を使って同様にパッケージされる。最後に、パッケージは集合 w についての命題値の型なので、集合間のパスに沿って輸送できる。w ≡ ⁅ U ⁆s からは、⁅ U ⁆s のパッケージをパスに沿って逆方向へ輸送して SglOf U w が得られる。

  sglOf⁅⁆ : (U : V ℓ) → SglOf U ⁅ U ⁆s
  sglOf⁅⁆ U = ∈sgl-intro refl , (λ z z∈ → ∈sgl-elim z∈)

  pairOf⁅⁆ : (U W : V ℓ) → PairOf U W ⁅ U , W ⁆
  pairOf⁅⁆ U W = ∈pair-introL refl , ∈pair-introR refl , (λ z z∈ → ∈pair-elim z∈)

  sglOf-subst : {U w : V ℓ} → w ≡ ⁅ U ⁆s → SglOf U w

パッケージが揃ったので、メタレベルの特徴付けを述べられる。prChar-fwd は三つの仮定を受け取り、パス Q ≡ pr U W という結論を出す。最初の二つは丸められた存在の主張である。Q のある要素 w が SglOf U を持つこと、Q のある要素 w が PairOf U W を持つことが、いずれも命題的に切り詰められた形で主張される。三つ目は全称の節である。Q のすべての要素 y は、U の単集合か、U と W の対かのどちらかに命題的に切り詰められた形で等しい。pr U W の外側の集合は、順序づけられた成分を符号化する二つの要素を持つ非順序対であり、Q がその外側の対と等しいことを pair-char で示すことに注意してほしい。

  sglOf-subst {U} e = subst (SglOf U) (sym e) (sglOf⁅⁆ U)

  pairOf-subst : {U W w : V ℓ} → w ≡ ⁅ U , W ⁆ → PairOf U W w
  pairOf-subst {U} {W} e = subst (PairOf U W) (sym e) (pairOf⁅⁆ U W)

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

最初の二つの仮定は、それぞれ命題的に切り詰められた形で、Q の要素と、その要素が対応する構成と等しいことを証明するパッケージを与える。丸めは、命題値である所属の命題 ⟨ ⁅ U ⁆s ∈ Q ⟩ か ⟨ ⁅ U , W ⁆ ∈ Q ⟩ へ消去されるので、witness の選び方を揃える必要はない。各分岐の中で、パッケージはパス w ≡ ⁅ U ⁆s か w ≡ ⁅ U , W ⁆ に変えられ、w の所属がそれに沿って輸送され、その構成の Q への所属が得られる。これは、u と v の場所に ⁅ U ⁆s と ⁅ U , W ⁆ を置いた pair-char が要求する最初の二つの引数にちょうど相当する。

  → ∥ Σ[ w ∶ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁
  → ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁)
  → Q ≡ pr U W
prChar-fwd Q U W h₁ h₂ h₃ = pair-char Q ⁅ U ⁆s ⁅ U , W ⁆
  (rec₁ (⟨ ⁅ U ⁆s ∈ Q ⟩isProp)

全称の節には消去はまったく要らない。Q の各要素 y について、パッケージの丸められた選言を変換 sglOf→≡ と pairOf→≡ を通して写せば、y が命題的に切り詰められた形で ⁅ U ⁆s か ⁅ U , W ⁆ に等しいという丸められた主張が得られる。これが pair-char の三つ目の引数である。その結論は Q ≡ ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆ であり、これは定義により Q ≡ pr U W である。逆向きの prChar-bwd は、Kuratowski 対そのものについて三つの仮定を提示するだけの作業である。

    (λ { (w , hw , h) → subst (λ z → ⟨ z ∈ Q ⟩) (sglOf→≡ h) hw }) h₁)
  (rec₁ (⟨ ⁅ U , W ⁆ ∈ Q ⟩isProp)
    (λ { (w , hw , h) → subst (λ z → ⟨ z ∈ Q ⟩) (pairOf→≡ h) hw }) h₂)
  (λ y hy → map₁ (sumMap sglOf→≡ pairOf→≡) (h₃ y hy))

prChar-bwd : (Q U W : V ℓ) → Q ≡ pr U W

パス Q ≡ pr U W が与えられれば、三つの仮定が順に作られる。補助の inQ は、パスの逆方向に沿って輸送することで、pr U W への所属を Q への所属に移し、三つの成分すべてがこれを使う。

  → (∥ Σ[ w ∶ V ℓ ] (⟨ w ∈ Q ⟩ × SglOf U w) ∥₁)
  × ((∥ Σ[ w ∶ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁)
  × ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁))
prChar-bwd Q U W e = h₁ , h₂ , h₃
  where

一つ目の存在の主張は、⁅ U ⁆s そのものが証人になる。外側の対が第一成分を含むこと、つまり反射パスでの ∈pair-introL の実例によって、それは pr U W に属し、inQ を通した輸送の後、この所属は Q の中で成り立つ。SglOf U を持つことはパッケージ sglOf⁅⁆ による。二つ目は、⁅ U , W ⁆、∈pair-introR、pairOf⁅⁆ に置き換えた同じ議論である。どちらも型が求めるとおり丸めで封入される。対象が単なる存在の主張である以上、選んだ証人で十分である。

  inQ : {z : V ℓ} → ⟨ z ∈ pr U W ⟩ → ⟨ z ∈ Q ⟩
  inQ {z} h = subst (λ w → ⟨ z ∈ w ⟩) (sym e) h
  h₁ : ∥ Σ[ w ∶ V ℓ ] (⟨ w ∈ Q ⟩ × SglOf U w) ∥₁
  h₁ = ∣ ⁅ U ⁆s , (inQ (∈pair-introL refl) , sglOf⁅⁆ U) ∣₁
  h₂ : ∥ Σ[ w ∶ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁

全称の節は、対の構成の分類に帰着する。Q の要素 y について、パスに沿った輸送により y の pr U W への所属が得られ、∈pair-elim がそれを丸められた選言 y ≡ ⁅ U ⁆s か y ≡ ⁅ U , W ⁆ に変える。各側は輸送の補題 sglOf-subst と pairOf-subst によって対応するパッケージに引き上げられ、この対応はパスの選言をパッケージの選言へ写す。どちらの構成も展開されることは一度もない。

  h₂ = ∣ ⁅ U , W ⁆ , (inQ (∈pair-introR refl) , pairOf⁅⁆ U W) ∣₁
  h₃ : (y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁
  h₃ y y∈Q = map₁ (⊎-rec (λ q → inl (sglOf-subst q)) (λ q → inr (pairOf-subst q)))
    (∈pair-elim (subst (λ w → ⟨ y ∈ w ⟩) e y∈Q))

対象言語の読解式

外側の特徴付けを、対象言語の論理式にする。各読解式は、それが語る de Bruijn 位置を引数として取るので、同じ定義を任意の入れ子の深さで使える。有界量化の簿記は標準的なものである。有界量化子は位置ゼロに新しい変数を束縛し、既存の位置を一つ外へずらす。束縛の下で言及される位置はその後者として現れるわけである。すべての節が原子、連言か選言、あるいは環境の変数で限られた量化子であるため、各読解式は Δ₀ であり、その界定集合は形から直接読める。

単集合の読解式 sglAt k i は、位置 k と i に割り当てられた集合について、i のものが k のものの単集合であると言う。第一の連言支は原子 var i ∈̇ var k である。第二の支は var k の要素の上で有界に量化し、その内側で、位置ゼロに新しく束縛された変数を var (suc i) と比較する。後者は、束縛の下で一段ずらされた後の位置 i である。ある集合がこの読解を充足するのは、k の値と等しい要素をひとつ持ち、ほかに要素を持たないとき、かつそのときに限る。これが SglOf の内容である。

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

非順序対の読解式 pairAt k i j は第二の成分を加え、全称の節を選言に弱める。有界量化子の下では、位置ゼロの新しい変数が、ずらされた二つの引数位置 var (suc i) と var (suc j) のどちらとも比較される。外側から読めば、i と j の値がともに属し、すべての要素が命題的に切り詰められた形でそのどちらかと等しいときに充足される。これはパッケージ PairOf そのものである。_∧̇_ と _∨̇_ の結合の宣言はこれらの式の構文解析だけを制御するもので、結合子の結合律を主張するものではないことに注意してほしい。

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

組み立てられた対の読解式は、二つの小さな読解式を、メタレベルの特徴付けの三つの節とともにまとめる。ある要素が単集合であること、ある要素が対であること、そしてすべての要素がそのどちらかであることである。各有界量化子は q の値の要素の上で限られ、二つの引数位置は束縛の下で一つずつずれるので、内側の読解式はやはり新しい変数を位置ゼロとして参照する。

第一の節は、var q の要素の上に存在量化を限り、その本体を sglAt zero (suc u) とする。位置ゼロの新しい変数が候補の要素であり、suc u は一段ずれた後の u の位置である。第二の節は pairAt で同じことを行い、今度はずれた後の u と v 両方の位置に言及する。第三の節は全称量化子を限り、その本体が二つの読解式の選言である。q の値のすべての要素は、命題的に切り詰められた形で単集合か対のどちらかである。存在の証人も「どちらか一方」という分類も、SglOf と PairOf とまったく同じく命題として丸められたままである。対象言語は要素を選ばず、ひとつ命題的に切り詰められた形で存在することしか言わない。

prAt : ∀ {n} → Fin n → Fin n → Fin n → Formula (V ℓ) n
prAt q u v = (∃̇∈ (var q) (sglAt zero (suc u)))
          ∧̇ ((∃̇∈ (var q) (pairAt zero (suc u) (suc v)))
          ∧̇ (∀̇∈ (var q) (sglAt zero (suc u) ∨̇ pairAt zero (suc u) (suc v))))

Δ₀-prAt : ∀ {n} (q u v : Fin n) → Δ₀ (prAt q u v)

有界性は構文的に証明書を与えられる。検査器 checkΔ₀ が組み立てられた論理式をたどり、すべての節点が原子、結合子、あるいは変数で限られた量化子であるため、自明な証明書 _ とともに受理され、Δ₀-prAt が得られる。これでこの読解式は有界なクラスに属し、その充足は推移的モデルの間で絶対的である。後の絶対性に関する章が依拠するのはこの事実である。

Δ₀-prAt q u v = checkΔ₀ (prAt q u v) tt

妥当性

最後の定理が、対象言語の読解式とその外側の意味を結び付ける。充足は hProp に値を持つので、この主張そのものが真理値の間のパスである。命題 γ ⊨ prAt q u v は、「q の値が u と v の値の Kuratowski 対と等しい」という命題と同一視される。等号の型が命題であることの証明は、V ℓ が h-集合であることから付く。三つの結合子と有界量化子の充足を展開すると、左辺はちょうど prChar-fwd と prChar-bwd が受け取る三つの仮定になる。したがって妥当性の証明は、既にある二つの議論を組み合わせるだけで、新しいことを証明するのではない。

示されたパスの両辺はともに真理値である。右辺では、等号の型 ⟦ var q ⟧ γ ≡ pr (⟦ var u ⟧ γ) (⟦ var v ⟧ γ) に setIsSet _ _ が組にされる。後者は、h-集合の二つの要素の等号が命題であることの証明である。この組がまさに hProp の作り方である。証明はその後、根底にある同値の二方向を与え、⇔toPath がそれらを命題の間のパスへ引き上げる。

prAt-adequate : ∀ {n} (q u v : Fin n) (γ : Vec (V ℓ) n)
              → (γ ⊨ prAt q u v) ≡ ((⟦ var q ⟧ γ ≡ pr (⟦ var u ⟧ γ) (⟦ var v ⟧ γ))
                                   , setIsSet _ _)
prAt-adequate q u v γ = ⇔toPath
  (λ { (h₁ , h₂ , h₃) → prChar-fwd _ _ _ h₁ h₂ h₃ })

順方向は prAt q u v の充足を受け取る。_∧̇_ と有界な ∃̇∈、∀̇∈ の意味論により、それは三つ組である。単集合の読解を満たす要素の丸められた存在、対の読解を満たす要素の丸められた存在、そして全称の節である。これらはちょうど prChar-fwd の三つの引数であり、pr U W へのパスを返す。逆向きは等号のパスを受け取り、prChar-bwd に渡す。後者はそれを、意味論が充足へと組み立て直す三つの節にパッケージする。どちらの方向でも、集合がどう構成されたかを検査することは一切ない。

  (λ e → prChar-bwd _ _ _ e)

まとめ

prAt は対象言語の内部から Kuratowski 対を読み取る。それは Δ₀ であり、かつ妥当である。その充足は、割り当てられた値の pr との等号へのパスになっている。コードを分解するために証明書が必要とする情報は、いまやすべて有界な形で利用でき、再帰もコード値の比較も使わない。続く章は、これらの読解式の上に証明書を構築していく。