集合としての構文

この章を読むか、読書案内と依存マップで別のルートを選べます。

読書案内 · 依存マップ

モデルが量化できるのは台の元だけですが、項と論理式は初め、外側の型理論にあります。構文をモデルの内部で利用できるように、本章では各項と論理式に台の元を割り当てます。符号はタグ付きの対であり、数のタグが最外側の構成子を識別し、ペイロードが直下の部分の符号を保持します。集合定数はすでに台に属するので、そのままペイロードにできます。

構成では、単射な対の操作と自然数からの単射を仮定します。この二つの仮定により、タグ付き対の両成分を復元できます。まず項の符号化が単射であることを証明し、次に論理式の十個の構成子すべてに符号を定めます。また CodesT と Codes によって、関係としての符号化のうち定数と所属の場合を与えます。最後に、タグで添字付けた構成子形状の記述を用いて、同じアリティの論理式は符号が等しければ等しいことを証明します。

構文を集合として符号化するには、台の上の 2 つの操作があれば足りますが、復号を可能にするのは単射性です。もし 2 つの構文が同じ集合に対応してしまったら、符号化を逆にたどれません。そこで本章は、等号と所属が hProp ℓ に値を取る ZFStructure、すなわち構造 𝒮 のもとで作業し、符号化に必要なデータを明示的なモジュール引数として取ります。以下の定義はすべて、そのようなデータを持つ任意の構造に対して述べられ、累積階層が後の章で実例を供給します。

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import FOL.ZFStructure using ( ZFStructure )

module FOL.Coding {ℓ} (𝒮 : ZFStructure ℓ)

2 つのデータとは、単射な対の操作と単射な数の写像です。pr は台 S の 2 つの元をその対に写し、pr-inj はこの対がまた分解できることを述べます。つまり等式 pr a b ≡ pr c d から a ≡ c と b ≡ d という 2 つの道の組が得られます。encℕ は各自然数を S の元へ送り、encℕ-inj は異なる数が異なる元に写ることを述べます。タグ付き対の構成が消費するのはまさにこれらの仮定で、本章は 𝒮 のそれ以外の性質をまったく使いません。

  (pr       : ZFStructure.S 𝒮 → ZFStructure.S 𝒮 → ZFStructure.S 𝒮)
  (pr-inj   : ∀ {a b c d} → pr a b ≡ pr c d → (a ≡ c) × (b ≡ d))
  (encℕ     : ℕ → ZFStructure.S 𝒮)
  (encℕ-inj : ∀ {j k} → encℕ j ≡ encℕ k → j ≡ k)
  where

符号化される対象は構文層から来ます。すなわち帰納型 Term と Formula で、項の構成子は 2 つ (集合定数 con と変数 var)、論理式の構成子は 10 個あり、原子式 _∈̇_ と _≐_ から結合子、有界・無界量化子に至ります。構造そのものから使うのは台 S だけで、符号化が構文に集合論の演算を付加することはないからです。空型は、特定の符号が一致しえないことを証明するときの、ありえない等式の値域としてだけ現れます。

open ZFStructure 𝒮 using ( S )
open import FOL.Syntax
  using ( Term; con; var; Formula
        ; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )

import Cubical.Data.Empty as Empty

単射性の証明を支えるのは、2 つの小さな算術的事実です。第一に、構造的に異なる数は決して等しくありません。補題 znots と snotz がそれぞれ 0 ≡ suc k と suc j ≡ 0 を反駁し、異なるタグを持つ 2 つの論理式が同じ符号を共有すると仮定したときに生じる衝突は、まさにこの形をしています。第二に、Fin n の変数の添字は toℕ で自然数に変換され、inj-toℕ はこの変換が単射であることを記録します。したがって添字による変数の符号化で情報は失われません。

open import Cubical.Data.Nat using ( znots; snotz )
open import Cubical.Data.FinData using ( toℕ; inj-toℕ )

タグ付き対

唯一の構成です。構成子の番号とペイロードを対にします。単射性は 2 つのパラメータから直ちに得られ、衝突パターンは「異なる 2 つの構成子を比較する」という、のちに繰り返し現れる場合を一箇所にまとめます。

基本の部品は mkTag k x = pr (encℕ k) x です。タグは k の数であり、ペイロードは x です。pr が S の元を返すため、両者とも S にあります。小さな例で、タグが形をどう区別するかが分かります。定数の符号は mkTag 0 x になり、添字 i の変数の符号は mkTag 1 (encℕ (toℕ i)) になる予定です。2 つのタグ付き対が等しければタグは一致しなければならず、mkTag-inj がこれを正確に述べます。pr-inj と encℕ-inj を合成して (j ≡ k) × (x ≡ y) を返します。その双対である clash は否定の場合を扱います。タグ j と k が等しくなりえないことの証明が与えられると、タグ付き対の等式からタグの等式を取り出してその証明と矛盾させ、周囲のレベルの任意の型 A で結論します。

mkTag : ℕ → S → S
mkTag k x = pr (encℕ k) x

mkTag-inj : ∀ {j k x y} → mkTag j x ≡ mkTag k y → (j ≡ k) × (x ≡ y)
mkTag-inj p = encℕ-inj (pr-inj p .fst) , pr-inj p .snd

clash : ∀ {j k x y} {A : Type ℓ} → (j ≡ k → Empty.⊥) → mkTag j x ≡ mkTag k y → A

clash の本体はこの議論を 1 行にまとめます。mkTag-inj p .fst は仮定した符号の等式から取り出した等式 j ≡ k であり、それを仮定 ne に渡すと空型の元が得られ、Empty.rec がその元を消去して任意の型 A の値を返します。2 つの構成子の形が数 0 と suc _ を等しくさせるたびに、clash はこの算術的反駁を必要な結論へ変換します。

clash ne p = Empty.rec (ne (mkTag-inj p .fst))

項と論理式の符号

まず項からです。ここで前述の工夫が現れます。集合の定数はすでに集合であるため符号化を必要とせず、変数の添字だけを注入すればよいのです。項どうしはよく分離されているので、単射性は直ちに得られます。

文脈 n の項は、上の 2 つの節で S の元として符号化されます。定数 con x はタグ 0 とペイロード x、すなわち集合そのものを取ります。ここが前述の省力化で、ペイロードを別途符号化する必要がありません。変数 var i はタグ 1 と toℕ i の数を取り、タグと添字が対の異なる側に置かれるため混同されません。単射性の証明は両項の構成子で場合分けします。定数対定数の場合、違い得るのはペイロードだけなので、mkTag-inj p .snd が直接 x ≡ y を与え、cong con がこれを con x ≡ con y へ持ち上げます。

⌜_⌝ᵗ : ∀ {n} → Term S n → S
⌜ con x ⌝ᵗ = mkTag 0 x
⌜ var i ⌝ᵗ = mkTag 1 (encℕ (toℕ i))

⌜⌝ᵗ-inj : ∀ {n} (t u : Term S n) → ⌜ t ⌝ᵗ ≡ ⌜ u ⌝ᵗ → t ≡ u
⌜⌝ᵗ-inj (con x) (con y) p = cong con (mkTag-inj p .snd)

残りの分岐が議論を完成させます。混在する場合、符号の等しさは数 0 と 1 の等しさを強制します。1 は後続者なので znots か snotz がこれを反駁し、clash がその反駁を項の等式へ変えます。変数対変数の場合、ペイロードの等式は encℕ (toℕ i) ≡ encℕ (toℕ j) を意味し、encℕ-inj が toℕ i ≡ toℕ j を、inj-toℕ がさらに i ≡ j を与え、cong var によって var i ≡ var j が得られます。すべての分岐が項の等式で終わるため、固定した n ごとに符号関数は Term S n 上で単射です。ここでの n は利用できる変数スロットの個数であり、個々の項が実際に使う変数の個数ではない点に注意してください。

⌜⌝ᵗ-inj (con x) (var j) p = clash znots p
⌜⌝ᵗ-inj (var i) (con y) p = clash snotz p
⌜⌝ᵗ-inj (var i) (var j) p = cong var (inj-toℕ (encℕ-inj (mkTag-inj p .snd)))

次に論理式です。10 個の構成子に 10 個のタグを割り当てます。2 項の構成子は 2 つの部分符号を対にし、1 項のものは部分符号をそのまま受け取り、偽はタグだけで決まるため仮のペイロードを取ります。

論理式も同じタグ付き対の方式を使います。5 つの 2 項構成子にタグ 0 から 4 までを割り当てます。所属の原子式 t ∈̇ u はタグ 0 に 2 つの項の符号の対を組み合わせて符号化され、等号も同様にタグ 1 です。各結合子は 2 つの直接の部分論理式の符号を対にします。項と比べると、あちらのペイロードは生の集合か数でしたが、こちらではペイロード自身が組み上がった符号であり得るので、論理式の構造全体がペイロードの中にネスティングします。再帰はホストの帰納型 Term と Formula の上で起こり、集合の上では決して起こりません。

⌜_⌝ : ∀ {n} → Formula S n → S
⌜ t ∈̇ u ⌝   = mkTag 0  (pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ)
⌜ t ≐ u ⌝   = mkTag 1  (pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ)
⌜ φ ∧̇ ψ ⌝   = mkTag 2  (pr ⌜ φ ⌝ ⌜ ψ ⌝)
⌜ φ ∨̇ ψ ⌝   = mkTag 3  (pr ⌜ φ ⌝ ⌜ ψ ⌝)

含意は他の結合子と同様にタグ 4 を取ります。偽 ⊥̇ は部分を一切持たない唯一の構成子で、タグ 5 だけで決まるため、ペイロードは仮の数 encℕ 0 です。これは、すべての符号をタグ付き対という統一した形に保つために置かれています。無界量化子 ∃̇ と ∀̇ は単項で、その符号はタグ 6 または 7 に部分論理式の符号を直接対にしたものです。

⌜ φ ⇒̇ ψ ⌝   = mkTag 4  (pr ⌜ φ ⌝ ⌜ ψ ⌝)
⌜ ⊥̇ ⌝       = mkTag 5 (encℕ 0)
⌜ ∃̇ φ ⌝     = mkTag 6 ⌜ φ ⌝
⌜ ∀̇ φ ⌝     = mkTag 7 ⌜ φ ⌝
⌜ ∀̇∈ t φ ⌝  = mkTag 8 (pr ⌜ t ⌝ᵗ ⌜ φ ⌝)

有界量化子がタグ 8 と 9 で一覧を締めくくります。それぞれ、限定する項の符号と本体の符号を対にします。アリティが束縛を反映しています。限定する項は論理式全体と同じ文脈 n に住み、本体のアリティは suc n で、束縛される変数のために 1 つ余分なスロットを持ちます。これですべての論理式構成子が互いに異なるタグを持ち、タグとペイロードが論理式を定めることになります。それを次の節で証明します。

⌜ ∃̇∈ t φ ⌝  = mkTag 9 (pr ⌜ t ⌝ᵗ ⌜ φ ⌝)

符号化関係

次に、符号化を関係として表す最初のケースを記録します。CodesT s t は集合と項を、Codes s φ は集合と論理式を関係づけます。このファイルで前者が持つのは定数の場合、後者が持つのは所属の場合です。

CodesT の構成子 c-con は、符号 mkTag 0 x を定数 con x に関係づけます。Codes の構成子 c-∈ は二つの項の符号についての導出を受け取り、タグ 0 のもとで対にしたペイロードを所属論理式に関係づけます。これらの宣言が扱うのは、ここに示された場合だけです。後の論理式符号の単射性は ⌜_⌝ から直接証明されます。

data CodesT {n : ℕ} : S → Term S n → Type ℓ where
  c-con : (x : S)     → CodesT (mkTag 0 x) (con x)

data Codes : {n : ℕ} → S → Formula S n → Type ℓ where
  c-∈  : ∀ {n s s'} {t u : Term S n}
       → CodesT s t → CodesT s' u → Codes (mkTag 0 (pr s s')) (t ∈̇ u)

符号は論理式を一意に定める

同じアリティを持ち、同じ符号を持つ二つの論理式は等しくなります。十個の構成子のすべての組を直接比較する代わりに、証明は論理式の符号を数値タグとペイロードに分けます。タグで添字づけられた型族が対応する構成子の形を記述し、対の単射性がタグとペイロードの等しさを与えます。その後、証明はペイロードの成分に沿ってのみ再帰します。

この節はタグの分離による証明です。最初の材料 tagOf は、論理式の構成子の番号を自然数として読み取ります。番号付けは ⌜_⌝ が符号を作るときに使ったものと同じで、所属 0、等号 1、論理積 2、論理和 3 です。つまり ⌜_⌝ がタグを集合の中に組み込み、tagOf がそれを取り出します。この節が成り立つのは、2 つの番号付けが一致しているからです。

tagOf : ∀ {n} → Formula S n → ℕ
tagOf (t ∈̇ u)  = 0
tagOf (t ≐ u)  = 1
tagOf (a ∧̇ b)  = 2
tagOf (a ∨̇ b)  = 3

残りの節は、4 から 9 までを含意、偽、2 つの無界量化子、2 つの有界量化子に割り当てます。これによりすべての論理式は 0 から 9 のタグを持ち、2 つの構成子が同じタグを共有することはありません。タグが構成子の形を特定できるのはまさにこのためです。

tagOf (a ⇒̇ b)  = 4
tagOf ⊥̇        = 5
tagOf (∃̇ a)    = 6
tagOf (∀̇ a)    = 7
tagOf (∀̇∈ t a) = 8

2 つ目の材料 payOf は同じ方法でペイロードを取り出します。所属と等号では 2 つの項の符号の対、論理積では 2 つの部分論理式の符号の対です。各節は ⌜_⌝ の対応する節のペイロード成分そのものなので、tagOf と payOf で符号を読めば、⌜_⌝ が入れたデータがちょうど復元されます。

tagOf (∃̇∈ t a) = 9

payOf : ∀ {n} → Formula S n → S
payOf (t ∈̇ u)  = pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ
payOf (t ≐ u)  = pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ
payOf (a ∧̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝

論理和と含意は 2 つの部分符号を対にし、無界量化子は単一の部分符号を返します。偽は、抽出が規約によって構成と一致しなければならない場合です。⌜ ⊥̇ ⌝ が仮の数 encℕ 0 をペイロードとして選んだので、payOf ⊥̇ も節を省かずに同じ値を取ります。

payOf (a ∨̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝
payOf (a ⇒̇ b)  = pr ⌜ a ⌝ ⌜ b ⌝
payOf ⊥̇        = encℕ 0
payOf (∃̇ a)    = ⌜ a ⌝
payOf (∀̇ a)    = ⌜ a ⌝

有界量化子が payOf を完成させます。それぞれ、限定する項の符号と本体の符号を対にします。続く shape は 2 つの方向の間の橋を記録します。すべての論理式 φ に対し、符号 ⌜ φ ⌝ は mkTag (tagOf φ) (payOf φ) に等しい、というものです。tagOf と payOf は ⌜_⌝ の節から書き写したものなので、φ でマッチングすると両辺が同じタグ付き対に簡約され、各場合は refl で成立します。

payOf (∀̇∈ t a) = pr ⌜ t ⌝ᵗ ⌜ a ⌝
payOf (∃̇∈ t a) = pr ⌜ t ⌝ᵗ ⌜ a ⌝

shape : ∀ {n} (φ : Formula S n) → ⌜ φ ⌝ ≡ mkTag (tagOf φ) (payOf φ)
shape (t ∈̇ u)  = refl
shape (t ≐ u)  = refl

ここに示した節は、論理和、含意、偽、無界存在量化子に対して同じ根拠を与えます。いずれの場合も等式は定義的です。⌜_⌝、tagOf、payOf が論理式に対する同じ再帰から作られているからです。次のブロックが残りの構成子を完成させ、その後で逆方向に進みます。

shape (a ∧̇ b)  = refl
shape (a ∨̇ b)  = refl
shape (a ⇒̇ b)  = refl
shape ⊥̇        = refl
shape (∃̇ a)    = refl

最後の shape の節が有界の場合を閉じ、構成はここで逆向きに転じます。タグが与えられたとき、そのタグを持つ論理式がどのような形かを記述します。これを担うのが型族 Match です。タグ k に対し Match k φ は、φ が番号 k の構成子から生じる仕方の型です。部分論理式のスロットごとに従属対の 1 段があり、最後はそれらのスロットに構成子を適用した結果への道 φ ≡ で終わります。タグ 0 と 1 ではスロットは 2 つの項で、構成子 _∈̇_ と _≐_ で閉じます。

shape (∀̇ a)    = refl
shape (∀̇∈ t a) = refl
shape (∃̇∈ t a) = refl

Match : ∀ {n} → ℕ → Formula S n → Type ℓ
Match {n} 0  φ = Σ[ t ∈ Term S n ] (Σ[ u ∈ Term S n ] (φ ≡ (t ∈̇ u)))

タグ 2 から 4 は 3 つの 2 項結合子に対して同じパターンを繰り返し、それぞれアリティが同じ n の論理式を 2 つ要求します。タグ 5 は退化した場合です。偽にはスロットがないので、Match 5 φ は対をまったく持たず、単一の道 φ ≡ ⊥̇ そのものです。この族が構成子の形に応じて変化し、統一したアリティを強制しないことが分かります。

Match {n} 1  φ = Σ[ t ∈ Term S n ] (Σ[ u ∈ Term S n ] (φ ≡ (t ≐ u)))
Match {n} 2  φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ∧̇ b)))
Match {n} 3  φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ∨̇ b)))
Match {n} 4  φ = Σ[ a ∈ Formula S n ] (Σ[ b ∈ Formula S n ] (φ ≡ (a ⇒̇ b)))
Match     5 φ = φ ≡ ⊥̇

量化子のタグにはアリティの変化が現れます。タグ 6 と 7 の唯一のスロットはアリティ suc n の論理式であり、タグ 8 と 9 ではアリティ n の項とアリティ suc n の本体が 2 つのスロットを埋め、構成子 ∀̇∈ と ∃̇∈ に対応します。その他のタグに対応する論理式はないので、族は空型 Empty.⊥* で閉じられます。これにより Match はすべての自然数のタグに対して定義されます。

Match {n} 6 φ = Σ[ a ∈ Formula S (suc n) ] (φ ≡ (∃̇ a))
Match {n} 7 φ = Σ[ a ∈ Formula S (suc n) ] (φ ≡ (∀̇ a))
Match {n} 8 φ = Σ[ t ∈ Term S n ] (Σ[ a ∈ Formula S (suc n) ] (φ ≡ ∀̇∈ t a))
Match {n} 9 φ = Σ[ t ∈ Term S n ] (Σ[ a ∈ Formula S (suc n) ] (φ ≡ ∃̇∈ t a))
Match     _  _ = Empty.⊥*

証拠を計算する方向は容易です。matches φ は φ に対する再帰で Match (tagOf φ) φ の元を構成します。2 項の論理式 a ∧̇ b は 2 つのスロットに a と b を供給し、最後の道は refl です。a ∧̇ b がその部分から定義的に組み上がるからです。たとえば t ∈̇ u の証拠は三つ組 t , (u , refl) です。

matches : ∀ {n} (φ : Formula S n) → Match (tagOf φ) φ
matches (t ∈̇ u)  = t , (u , refl)
matches (t ≐ u)  = t , (u , refl)
matches (a ∧̇ b)  = a , (b , refl)
matches (a ∨̇ b)  = a , (b , refl)

残りの構成子は、それぞれの Match の行の形に従います。偽は refl だけを供給し、各無界量化子は本体と refl を対にし、各有界量化子は限定する項と本体を供給します。最後の構成子まで覆うと、matches はすべての論理式が自分のタグに適合することを示します。したがってタグだけで、どの論理式も 1 つの構成子の形にまで絞り込めます。

matches (a ⇒̇ b)  = a , (b , refl)
matches ⊥̇        = refl
matches (∃̇ a)    = a , refl
matches (∀̇ a)    = a , refl
matches (∀̇∈ t a) = t , (a , refl)

定理 ⌜⌝-inj はもう目の前です。同じアリティの論理式 φ と ψ に対し、等式 ⌜ φ ⌝ ≡ ⌜ ψ ⌝ は φ ≡ ψ を強制するはずです。証明は補助関数 go に帰着し、go は private ブロックの中で宣言されるため、書き出されるのは定理そのものだけです。go が仮定するのは、タグの分離がまさに与えるものです。すなわち φ のタグに対する適合として再提示された ψ と、ペイロードの等式 payOf φ ≡ payOf ψ です。これらから φ ≡ ψ を返さなければなりません。

matches (∃̇∈ t a) = t , (a , refl)

⌜⌝-inj : ∀ {n} (φ ψ : Formula S n) → ⌜ φ ⌝ ≡ ⌜ ψ ⌝ → φ ≡ ψ

private
  go : ∀ {n} (φ ψ : Formula S n) → Match (tagOf φ) ψ → payOf φ ≡ payOf ψ → φ ≡ ψ
  go (t ∈̇ u) ψ (t' , (u' , q)) p =

所属の節に仕組みの全体が表れているので、ゆっくり読む価値があります。適合は ψ を道 q : ψ ≡ (t' ∈̇ u') のもとで t' ∈̇ u' として提示しますが、仮定 p が等しいと言うのは φ と ψ のペイロードであって、t' ∈̇ u' のペイロードではありません。p に cong payOf q を合成すると、等式が q に沿って輸送され、pr ⌜ t ⌝ᵗ ⌜ u ⌝ᵗ ≡ pr ⌜ t' ⌝ᵗ ⌜ u' ⌝ᵗ が得られます。pr-inj がこれを項の符号の等式に分解し、それぞれはすでに証明済みの ⌜⌝ᵗ-inj を通ります。cong₂ _∈̇_ が両辺に構成子を組み立て直し、最後の sym q が右辺を t' ∈̇ u' から ψ へ向け直します。等号の節はこれを _≐_ に替えてそのまま繰り返します。

    cong₂ _∈̇_ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝ᵗ-inj u u' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (t ≐ u) ψ (t' , (u' , q)) p =
    cong₂ _≐_ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝ᵗ-inj u u' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q

すべての 2 項結合子はこの 1 つのパターンで処理されるので、論理積の節を汎用の処方として述べる価値があります。適合は三つ組 a' , (b' , q) で、q : ψ ≡ (a' ∧̇ b') が成り立ちます。輸送されたペイロードの等式は pr _ _ ≡ pr _ _ の形をしているので、pr-inj が 2 つの部分符号の等式を与え、⌜⌝-inj が再帰的にそれらを部分論理式の等式へ引き上げ、cong₂ _∧̇_ が a ∧̇ b ≡ a' ∧̇ b' を組み立て直し、sym q が右辺を ψ に向けます。この処方こそが、残りの結合子の節の内容のすべてです。

  go (a ∧̇ b) ψ (a' , (b' , q)) p =
    cong₂ _∧̇_ (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝-inj b b' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (a ∨̇ b) ψ (a' , (b' , q)) p =
    cong₂ _∨̇_ (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .fst))

論理和と含意の節は、それぞれの構成子でこの処方を具体化するだけで、他は何も変わりません。偽はペイロードの操作がまったく不要な唯一の場合です。適合は q : ψ ≡ ⊥̇ だけなので、sym q : ⊥̇ ≡ ψ がすでに求める等式であり、ペイロードの仮定 p は使われません。

              (⌜⌝-inj b b' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go (a ⇒̇ b) ψ (a' , (b' , q)) p =
    cong₂ _⇒̇_ (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .fst))
              (⌜⌝-inj b b' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q
  go ⊥̇ ψ q p = sym q

無界量化子では処方が単純になります。ペイロードは単一の部分符号なので、輸送された等式は直接 ⌜ a ⌝ ≡ ⌜ a' ⌝ であり、cong ∃̇_ か cong ∀̇_ で包んだ再帰呼び出し 1 回と、最後の sym q で足ります。有界量化子 ∀̇∈ は、2 つのレベルの符号化が 1 つの構成子の中で出会う場所です。pr-inj で分解した後、項の成分は ⌜⌝ᵗ-inj が、論理式の成分は再帰的な ⌜⌝-inj が解決し、cong₂ ∀̇∈ が両者を組み立て直し、最後はいつものように sym q で締めます。

  go (∃̇ a) ψ (a' , q) p = cong ∃̇_ (⌜⌝-inj a a' (p ∙ cong payOf q)) ∙ sym q
  go (∀̇ a) ψ (a' , q) p = cong ∀̇_ (⌜⌝-inj a a' (p ∙ cong payOf q)) ∙ sym q
  go (∀̇∈ t a) ψ (t' , (a' , q)) p =
    cong₂ ∀̇∈ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
             (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q

有界存在量化子は有界全称量化子と対応しており、これで 10 の場合がそろいます。そのうえで大域的な定理が組み立てられます。e : ⌜ φ ⌝ ≡ ⌜ ψ ⌝ が与えられると、go には φ のタグで添字づけられた ψ の適合が必要ですが、matches ψ は ψ のタグのところに住んでいます。数として両者は異なり得るので、適合を輸送します。tp .fst は道 tagOf φ ≡ tagOf ψ であり、その対称に沿って subst すると matches ψ は型 Match (tagOf φ) ψ に添字づけ直され、これは go が期待するものとちょうど一致します。

  go (∃̇∈ t a) ψ (t' , (a' , q)) p =
    cong₂ ∃̇∈ (⌜⌝ᵗ-inj t t' (pr-inj (p ∙ cong payOf q) .fst))
             (⌜⌝-inj a a' (pr-inj (p ∙ cong payOf q) .snd)) ∙ sym q

⌜⌝-inj φ ψ e = go φ ψ
  (subst (λ k → Match k ψ) (sym (tp .fst)) (matches ψ)) (tp .snd)

局所定義 tp が、この輸送に必要な一対の等式を作ります。sym (shape φ)、仮定 e、shape ψ をつなげると、仮定された符号の等式はタグ付き対の間の等式 mkTag (tagOf φ) (payOf φ) ≡ mkTag (tagOf ψ) (payOf ψ) に書き換わり、mkTag-inj がそれをタグの等式とペイロードの等式に分解します。タグの等式が subst を駆動し、ペイロードの等式が go の第 2 引数になります。定理はこれで完成です。構成子を十乗十で比較する必要はなく、必要なのはタグの計算とペイロードに沿う再帰だけです。

  where
  tp = mkTag-inj (sym (shape φ) ∙ e ∙ shape ψ)

まとめ

項と論理式には S の元としての符号が与えられます。⌜_⌝ は各部分の符号に構成子のタグを付け、定数はその台となる集合をペイロードにします。このファイルは関係による符号化のうち定数と所属の場合を記録し、続いて固定したアリティでは一つの符号が高々一つの論理式を定めることを証明します。この構成は単射な対の演算と自然数の単射をパラメータとします。