構文についての内部的な議論は、L の中の論理式キーの集合から始まります。本章は、候補となる符号領域と外部の論理式文法を二方向に比較します。領域の各要素は、ある論理式のキーへ単に復号でき、すべての真正な論理式キーは領域に属します。これらは符号の所属についての主張であり、符号化された論理式の真理や充足についての主張ではありません。

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

以下の議論では、排中律と命題的切り詰めを併用します。命題的切り詰めは、復号の証人を選び出すことなく、その存在だけを記録します。この切り詰めを除去できるのは、行き先も命題である場合に限られます。

open import Base.Prelude
open import Base.Classical using ( LEM )

lem : LEM (ℓ-suc ℓ) を仮定します。本章のすべての構成はこの仮定のもとで行われますが、仮定によって復号の結論が強くなるわけではありません。復号された論理式の証人は、命題的に切り詰められたままです。

module L.Coding.CodeDomainAdequacy {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

本章は集合論の完全な一階言語を扱います。論理式には非有界の量化子に加えて二つの有界量化子があり、項は変数と定数から作られます。領域が集めて記述すべき対象は、これらです。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; Term; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∃̇∈; ∀̇∈ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

論理式キーは入れ子の順序対なので、対符号化の単射性により、キーの等しさからアリティ、タグ、ペイロードを復元できます。自然数のアリティはフォン・ノイマン数項で表され、構成可能な環境集合が有限パラメータベクトルの内部表現を与えます。

open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; #mono )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Environment {ℓ} using ( env )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )
open import L.Axioms.Numerals {ℓ} using ( numeralL-fst; sucʟ; sucʟ-fst )

対象言語では、構造に従って組み立てたキーが候補領域に属することを表現できます。順序対の式が入れ子のキーを構成し、その妥当性定理が、得られた論理式の充足と、対応するホスト側の対符号への所属とを同一視します。

open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate )
open import L.Coding.Expressions {ℓ} using ( sucAtL )
open import L.Coding.Model {ℓ} using ( container )
import L.Coding.Expressions {ℓ} as CodingExpressions
module E = CodingExpressions.PairExpression

量化子の符号ではアリティが変わります。どちらの量化子でも本体は後続アリティのキーであり、有界量化子はさらに現在のアリティで正当な項をもちます。対、後続、拡張環境についての意味論的補題が、束縛子の下で起こるこれらの変化を正確に表します。

open import L.Coding.Quantification {ℓ} using
  ( i0; i1; i2; i3; i4; i5; i6; i7; i8; sh
  ; pr-out; pr-in; down; fstS; sndS; suc-out; suc-in
  ; sndEx; sndAll; bothEx
  ; sndEx-out; sndAll-in; bothEx-out; bothAll-in

存在的なペイロードの記述は命題的に切り詰められ、ときには二重の証人を含みます。その内向きと外向きの読みは、この切り詰めを保ちます。十個の構成子タグは零から九までの数項で表され、別の環境塔が各符号を読むアリティを記録します。

  ; fillSnd; fillBoth; useSnd; useBoth
  ; f0; f1; f2; f3; f4; f5; f6; f7; f8; f9
  ; bigOr-in; bigOr-out )
open import L.Coding.EnvironmentTower {ℓ} lem using ( module Tower; nn )
open import L.Coding.CodeDomain {ℓ} using

記述 codesAt には、相補的な二つの部分があります。shapeAt は領域の既存要素を十種類の構成子形のいずれかとして読み、複合符号では直下の部分キーも領域に残ることを要求します。closeAt は生成する向きの主張であり、正当な項と既存の部分キーから対応する新しいキーが得られます。

  ( isTm; keyUp; keyExpr; atomKeyExpr; bndKeyExpr
  ; unKey; binKey; atomKey; bndKey
  ; Tags; shN; module Shape; shapeAt; module Close; closeAt; codesAt )
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet )

構成子タグは Fin 10 の要素です。その自然数値が十個のペイロード述語の一つを選び、その値は自動的に十未満です。環境は有限ベクトルであり、階層に格納される符号は入れ子の集合論的順序対です。

open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( toℕ<n )
open import Cubical.Data.Vec using ( _∷_; lookup )
open import Cubical.Data.Sigma using ( _×_ )

復号は互いに排他的な構成子の場合に分かれ、多くの場合、命題的に切り詰められた証人だけを返します。対の等しさは成分ごとに移され、不可能なタグは空型へ至ります。これらの操作から、単に存在する論理式を大域的に選ぶ復号写像は得られません。

open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.Prelude using ( subst2 )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

累積階層は、集合値の順序対符号、フォン・ノイマン数項、アリティの後続演算を与えます。所属には小さなファイバー表示があり、階層の集合の等しさは命題です。これらの事実により、切り詰められた分解と、所属や等しさへのその消去が正当化されます。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; sucV )

構成可能な構造の台が S として固定され、以下のすべての環境と論理式の読みがその上にあります。

open hPropStructure 𝒮ʟ using ( S )

符号の記述はすべて、L が担う一階構造で解釈されます。したがって、「組み立てたキーが C に属する」という主張には、対象言語の論理式としての形と、ホスト側の所属としての読みがあります。妥当性補題は、同じ主張のこの二つの形を同一視します。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )

記述の読み出し

まず、項の符号を記述します。集合 t がアリティ ar の項の符号であるのは、それが単に、タグ零と作業集合 Wv の要素の対、あるいはタグ一と集合 ar の要素の対であるときです。ここでの ar はまだ任意の集合です。それが数項だと分かってはじめて、第二の分岐から有界な変数の添字が復元されます。

IsTmV : V ℓ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
IsTmV Wv t ar = ∥ (Σ[ x ∈ V ℓ ] ((t ≡ pr (# ) x) × ⟨ x ∈ Wv ⟩))
                ⊎ (Σ[ i ∈ V ℓ ] ((t ≡ pr (# ) i) × ⟨ i ∈ ar ⟩)) ∥₁

最初の三種類のペイロード述語は、原子論理式、二項結合子、偽を扱います。原子のペイロードは二つの正当な項符号へ単に分解され、二項のペイロードは候補領域にすでに属する同じアリティの二つの部分キーへ単に分解されます。偽のペイロードは直接の等式 r = # 0 であり、存在証人をもちません。

module CodesSem (Wv Cv : V ℓ) where
  AtomP BinP ConP QuP BqP : V ℓ → V ℓ → Type (ℓ-suc ℓ)
  AtomP ar r = ∥ Σ[ t ∈ V ℓ ] Σ[ u ∈ V ℓ ] ((r ≡ pr t u) × (IsTmV Wv t ar × IsTmV Wv u ar)) ∥₁
  BinP ar r = ∥ Σ[ a ∈ V ℓ ] Σ[ b ∈ V ℓ ] ((r ≡ pr a b) × (⟨ pr ar a ∈ Cv ⟩ × ⟨ pr ar b ∈ Cv ⟩)) ∥₁
  ConP ar r = r ≡ # 

量化子のペイロードで一覧が完成します。非有界量化子のペイロードは、後続アリティにある下位キーです。有界量化子のペイロードは、現在のアリティで正当な項符号と、そのような下位キーとの対です。この非対称性は文法そのものに由来します。本体は後続アリティをもち、境界を表す項は量化された論理式と同じアリティをもちます。

  QuP ar r = ⟨ pr (sucV ar) r ∈ Cv ⟩
  BqP ar r = ∥ Σ[ t ∈ V ℓ ] Σ[ a ∈ V ℓ ] ((r ≡ pr t a) × (IsTmV Wv t ar × ⟨ pr (sucV ar) a ∈ Cv ⟩)) ∥₁

ペイロードの表はここからはじまります。タグ零と一が二つの原子の形を、タグ二と三が連言と選言の二項の形を担います。

  PayN : ℕ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
  PayN  = AtomP
  PayN  = AtomP
  PayN  = BinP
  PayN  = BinP

表は続き、タグ四が含意、タグ五が定数の偽、タグ六と七が二つの非有界量化子、タグ八が有界の全称を担います。

  PayN  = BinP
  PayN  = ConP
  PayN  = QuP
  PayN  = QuP
  PayN  = BqP

タグ九は有界存在量化子のペイロードを担います。補助族 PayN は十以上の自然数では空型ですが、正当な Key のタグは Fin 10 から選ばれます。したがって、キーに現れうるのは零から九までの十種類だけです。

  PayN  = BqP
  PayN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) _ _ = Empty.⊥*

アリティ ar でのキーとは、単に、十のタグの一つと、それに合った形のペイロードのことです。キーが何でないかに注意してください。キーは帰納的な構文木ではなく、その分解が一意なデータだとも主張していません。キーとは、集合として符号化された対が、既知の十の形のどれかに分解されるという、切り詰められた証拠なのです。

  Key : V ℓ → V ℓ → Type (ℓ-suc ℓ)
  Key ar p = ∥ Σ[ k ∈ Fin  ] Σ[ r ∈ V ℓ ] ((p ≡ pr (# (toℕ k)) r) × PayN (toℕ k) ar r) ∥₁

候補となる項符号 t、アリティ集合 ar、作業集合 Wv、そしてそれぞれ数項零と一であることが分かっている二つの要素を含む環境を固定します。これらのタグ等式のもとで、対象言語の述語 isTm と外部の述語 IsTmV Wv t ar を正確に比較できます。

module _ {k : ℕ} (t ar w N0 N1 : Fin k) (δ : S ^ k)
  (q0 : fst (lookup N0 δ) ≡ # ) (q1 : fst (lookup N1 δ) ≡ # ) where
  private
    Wv = fst (lookup w δ)

外向きの読み出しは、対象言語の論理式の切り詰められた選言を消去します。定数の分岐では、存在量化が対の第二成分を取り出し、数項の等式がタグを揃え、所属が IsTmV へ入ります。結果は、切り詰められた定義の左の分岐です。

  isTm-out : ⟨ δ ⊨ isTm t ar w N0 N1 ⟩ → IsTmV Wv (fst (lookup t δ)) (fst (lookup ar δ))
  isTm-out = PT.rec squash₁
    (λ { (inl h) → PT.map
           (λ { (v , s , (e , v∈)) → inl (fst v , (e ∙ cong (λ a → pr a (fst v)) q0 , v∈)) })
           (sndEx-out t N0 (var i0 ∈̇ var (sh  w)) δ h)

変数の分岐は、数項一とアリティの集合で同じ三歩を繰り返し、右の分岐を作ります。二つの分岐合わせて、対象言語の認識と、集合レベルの IsTmV がまさに同値であることが言えます。

       ; (inr h) → PT.map
           (λ { (v , s , (e , v∈)) → inr (fst v , (e ∙ cong (λ a → pr a (fst v)) q1 , v∈)) })
           (sndEx-out t N1 (var i0 ∈̇ var (sh  ar)) δ h) })

内向きの読み出しは、同じ変換を逆向きに行います。定数の分岐では、充填の補題が証人 x を枠零の存在量化子の下に置き、対の等式が逆向きの数項の等式に沿って運ばれて、充足が対象言語の論理式の形と一致するようにします。

  isTm-in : IsTmV Wv (fst (lookup t δ)) (fst (lookup ar δ)) → ⟨ δ ⊨ isTm t ar w N0 N1 ⟩
  isTm-in = PT.rec (snd (δ ⊨ isTm t ar w N0 N1))
    (λ { (inl (x , (e , x∈))) →
           ∣ inl (fillSnd t δ (lookup N0 δ) (down (lookup w δ) x x∈)
                    (e ∙ cong (λ a → pr a x) (sym q0)) (var i0 ∈̇ var (sh  w)) x∈ N0 refl) ∣₁

変数の分岐は、数項一の枠の存在量化子の下に証人 i を満たし、対応する逆向きの等式に沿って運びます。二つの分岐が、この同値を両方向で閉じます。

       ; (inr (i , (e , i∈))) →
           ∣ inr (fillSnd t δ (lookup N1 δ) (down (lookup ar δ) i i∈)
                    (e ∙ cong (λ a → pr a i) (sym q1)) (var i0 ∈̇ var (sh  ar)) i∈ N1 refl) ∣₁ })

述語 keyUp C ar r は、一つの正確な所属、すなわち対 (suc ar,r) が C に属することを表します。その有界存在による表現は、C の実際の要素を選び、その要素を順に明らかにして、対の形と後続の等式の両方を確かめます。

module _ {k : ℕ} (C ar r : Fin k) (δ : S ^ k) where
  keyUp-out : ⟨ δ ⊨ keyUp C ar r ⟩ → ⟨ pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ) ⟩
  keyUp-out = PT.rec (snd (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ)))
    (λ { (c' , (c'∈ , h)) → PT.rec (snd (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ)))
      (λ { (s , (s∈ , h')) → PT.rec (snd (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ)))

外向きには、対の論理式が選ばれた C の要素を (ar',r) と同一視し、後続の論理式が ar' を suc ar と同一視します。この二つの等式に沿って所属を移すと、(suc ar,r) ∈ C が得られます。切り詰められた証人はすべて、この所属命題へのみ消去されます。

        (λ { (ar' , (ar'∈ , (e , hs))) →
          subst (λ u → ⟨ u ∈ fst (lookup C δ) ⟩)
            (pr-out i2 i0 (sh  r) (ar' ∷ s ∷ c' ∷ δ) e
             ∙ cong (λ a → pr a (fst (lookup r δ))) (suc-out (sh  ar) i0 (ar' ∷ s ∷ c' ∷ δ) hs))
            c'∈ })

したがって、三層の有界な証人は、表示された対象が C の要素であることを確かめるためだけに使われます。その切り詰めを消去した結果、keyUp-out は外部の所属 (suc ar,r) ∈ C をちょうど与えます。

        h' })
      h })

内向きには、(suc ar,r) ∈ C から始めます。後続アリティを構成可能集合として提示し、それと r の順序対をまとめ、これらを三つの有界な証人として使います。すると、対と後続の論理式から keyUp C ar r の充足が再構成されます。

  keyUp-in : ⟨ pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ) ⟩ → ⟨ δ ⊨ keyUp C ar r ⟩
  keyUp-in h = ∣ c' , (h , ∣ c .fst , (c .snd .fst , ∣ ar' , (c .snd .snd .fst
    , ( pr-in i2 i0 (sh  r) (ar' ∷ c .fst ∷ c' ∷ δ) (sym (cong (λ a → pr a (fst (lookup r δ))) (sucʟ-fst (lookup ar δ))))
      , suc-in (sh  ar) i0 (ar' ∷ c .fst ∷ c' ∷ δ) (sucʟ-fst (lookup ar δ)) )) ∣₁) ∣₁) ∣₁
    where

具体的には、ar' が suc ar を表し、c' が C の要素 (suc ar,r) を表します。さらに c' とともに与えられる包含集合が、論理式で使う有界所属の鎖を証します。それぞれの基礎集合の等式により、内部の証人が意図した外部の対を表すことが保証されます。

    ar' : S
    ar' = sucʟ (lookup ar δ)
    c' : S
    c' = down (lookup C δ) (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ))) h
    c = container c' ar' (lookup r δ) (cong (λ a → pr a (fst (lookup r δ))) (sym (sucʟ-fst (lookup ar δ))))

候補領域 C、アリティ値 A、タグ値 N、ペイロード a を固定します。これらから組み立てる単項キーは、入れ子の対 (A,(N,a)) です。

module _ {k : ℕ} (C ar N a : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)

unKey の外向きの読みは、入れ子のキー (A,(N,a)) が C に属することを正確に述べます。順序対の式の妥当性により、対象言語の所属は、ホスト側のこの集合所属へ変換されます。

  unKey-out : ⟨ δ ⊨ unKey C ar N a ⟩ → ⟨ pr A (pr Nv (fst (lookup a δ))) ∈ Cv ⟩
  unKey-out = E.member-out (keyExpr ar N (E.slot a)) (var C) δ

妥当性は逆向きにも使えます。所属 (A,(N,a)) ∈ C から、対象言語の述語 unKey の充足が得られます。したがって、キーの条項とホスト側での読みは、双方向に一致します。

  unKey-in : ⟨ pr A (pr Nv (fst (lookup a δ))) ∈ Cv ⟩ → ⟨ δ ⊨ unKey C ar N a ⟩
  unKey-in = E.member-in (keyExpr ar N (E.slot a)) (var C) δ

二項構成子について、二つのペイロード成分 a と b を固定します。その順序対 P=(a,b) がキー (A,(N,P)) のペイロードとなり、アリティとタグは単項の場合と同じ外側の位置を占めます。

module _ {k : ℕ} (C ar N a b : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)

二つの引数の値から順序対 P = (a,b) を作ります。この対が、入れ子の二項キー (A,(N,P)) のペイロードです。

    P = pr (fst (lookup a δ)) (fst (lookup b δ))

binKey の外向きの読みは、所属 (A,(N,(a,b))) ∈ C にほかなりません。この形は、アリティ、構成子タグ、対にした引数という符号化の三つの論理的な層を保ちます。

  binKey-out : ⟨ δ ⊨ binKey C ar N a b ⟩ → ⟨ pr A (pr Nv P) ∈ Cv ⟩
  binKey-out = E.member-out (keyExpr ar N (E.pair (E.slot a) (E.slot b))) (var C) δ

内向きの読み出しはその逆向きであり、他のキーの条項と同じく、二者は論理式の主張と集合の所属を同一視します。

  binKey-in : ⟨ pr A (pr Nv P) ∈ Cv ⟩ → ⟨ δ ⊨ binKey C ar N a b ⟩
  binKey-in = E.member-in (keyExpr ar N (E.pair (E.slot a) (E.slot b))) (var C) δ

原子キーのペイロードは二つの項符号です。各項符号はそれぞれの項タグと引数をもち、その二つの項符号の対が、原子構成子のタグと共通のアリティの下に置かれます。

module _ {k : ℕ} (C ar N Nx x Ny y : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)

二つの項符号を T=(Nx,x)、U=(Ny,y) と書きます。この段階では Nx と Ny は環境から得た任意のタグ値であり、それらが零または一であるという条件は、原子の閉性の場合を具体化するときに課されます。

    T = pr (fst (lookup Nx δ)) (fst (lookup x δ))
    U = pr (fst (lookup Ny δ)) (fst (lookup y δ))

原子の条件を外向きに読むと、(A,(N,(T,U))) ∈ C となります。ここで T と U は二つの項符号です。最も外側の対がアリティを、その次が原子タグを、最も内側の対が二つの項を記録します。

  atomKey-out : ⟨ δ ⊨ atomKey C ar N Nx x Ny y ⟩ → ⟨ pr A (pr Nv (pr T U)) ∈ Cv ⟩
  atomKey-out = E.member-out (atomKeyExpr ar N Nx x Ny y) (var C) δ

内向きの読み出しはその逆向きで、これまでのどのキーの条項と同じく、原子の場合を両方向で閉じます。

  atomKey-in : ⟨ pr A (pr Nv (pr T U)) ∈ Cv ⟩ → ⟨ δ ⊨ atomKey C ar N Nx x Ny y ⟩
  atomKey-in = E.member-in (atomKeyExpr ar N Nx x Ny y) (var C) δ

有界量化子のキーのペイロードには、異なる二つの成分があります。境界を表す項符号と、本体を表す部分論理式の符号です。共通する外側のデータは、やはり現在のアリティ A と有界量化子タグ N です。

module _ {k : ℕ} (C ar N Nx x a : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)

境界項の符号を T=(Nx,x)、本体の符号を Av と書きます。項は現在のアリティで検査され、本体のキーは後続アリティで検査されます。両者を別々のペイロード成分として保つことで、この文法上の非対称が記録されます。

    T = pr (fst (lookup Nx δ)) (fst (lookup x δ))
    Av = fst (lookup a δ)

有界キーの条件を外向きに読むと、(A,(N,(T,Av))) ∈ C となります。最も内側の対には、境界項の符号と本体の符号がこの順で入ります。この所属だけでは、どちらの成分が正当であることもまだ主張しません。

  bndKey-out : ⟨ δ ⊨ bndKey C ar N Nx x a ⟩ → ⟨ pr A (pr Nv (pr T Av)) ∈ Cv ⟩
  bndKey-out = E.member-out (bndKeyExpr ar N Nx x a) (var C) δ

逆に、(A,(N,(T,Av))) が C に属することから bndKey の充足が得られます。二方向の読みが確立するのは構造的な所属の同値だけです。T の正当性と、後続アリティにおける Av の所属は、周囲のペイロード述語が別に与えます。

  bndKey-in : ⟨ pr A (pr Nv (pr T Av)) ∈ Cv ⟩ → ⟨ δ ⊨ bndKey C ar N Nx x a ⟩
  bndKey-in = E.member-in (bndKeyExpr ar N Nx x a) (var C) δ

ここで、候補となる符号領域 C、作業集合 W、そして零から九までの数項であることが証明された十個の環境要素を固定します。すると各タグについて、対象言語のペイロード記述を、対応する外部の述語 AtomP、BinP、ConP、QuP、BqP と比較できます。

module PayRead {m : ℕ} (C w : Fin m) (N : Fin  → Fin m) (δ : S ^ ( + m))
  (tg : Tags δ (shN  N)) where
  private
    Cv = fst (lookup (sh  C) δ)
    Wv = fst (lookup (sh  w) δ)

各ペイロードの読みでは、A が記録されたアリティを、R が生のペイロードを表します。タグ零と一の等式を取り出しておくのは、原子と有界量化子のペイロードがともに項符号を認識する必要があり、項の二つの正当な形がちょうどこの二タグを使うからです。

    A = fst (lookup i5 δ)
    R = fst (lookup i0 δ)
    q0 = tg f0
    q1 = tg f1
    rS = lookup i0 δ

比較の両側では、同じ基礎集合 Wv と Cv を使います。したがって、構文的なペイロード論理式が述べる Wv への項の所属と Cv への部分キーの所属は、五つの外部ペイロード述語のパラメータと正確に一致します。

    module Sh = Shape C w N
  open CodesSem Wv Cv

原子の本体は、ペイロードの二成分がともに、記録されたアリティで項符号の述語を満たすことを要求します。これに対して二項の本体は、両成分が同じアリティのキーとして候補領域に現れることを要求します。どちらのペイロードも対として符号化されますが、二つの条件は異なります。

  private
    tmBody : Formula S ( + m)
    tmBody = isTm i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) ∧̇ isTm i0 i8 (sh  w) (sh  (N f0)) (sh  (N f1))
    binBody : Formula S ( + m)
    binBody = appAt (sh  C) i8 i1 ∧̇ appAt (sh  C) i8 i0

最後のペイロード形は二つの有界量化子を扱います。その本体は、境界を表す項が現在のアリティで合法であることと、本体のキーが後続アリティで符号集合に属することを要求します。

    bqBody : Formula S ( + m)
    bqBody = isTm i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) ∧̇ keyUp (sh  C) i8 i0

原子ペイロードを外向きに読むと、二つの存在束縛が除かれ、項 t と u、等式 R ≡ pr t u、および両方の項がアリティ A で合法であることの証明が得られます。項の読みは 0 と 1 のタグ等式を用いて、二つの充足証明を対応する切り詰められた項の形へ変換します。

  atom-out : ⟨ δ ⊨ Sh.atomPay ⟩ → AtomP A R
  atom-out h = PT.map
    (λ { (t , u , s , (e , (ht , hu))) → fst t , fst u
       , ( e , ( isTm-out i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (u ∷ t ∷ s ∷ δ) q0 q1 ht
               , isTm-out i0 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (u ∷ t ∷ s ∷ δ) q0 q1 hu ) ) })

この消費は、二重の存在消去の一つの適用にすぎません。証人 t、u と容器を取り出し、残りの連言をペイロードのデータへ処理します。

    (bothEx-out i0 tmBody δ h)

内向きの読みは、データから充足を組み立て直します。切り詰められた合法性の証明は、目標もまた切り詰められた充足であるため消去でき、二つの項はそれぞれずらした文脈を通して合法性の原子に入ります。

  atom-in : AtomP A R → ⟨ δ ⊨ Sh.atomPay ⟩
  atom-in = PT.rec (snd (δ ⊨ Sh.atomPay))
    (λ { (t , u , (e , (ht , hu))) →
      fillBoth i0 δ (fstS rS t u e) (sndS rS t u e) e tmBody
        ( isTm-in i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (δ12 t u e) q0 q1 ht

二つ目の合法性の証明も同じ方法で入れます。補助環境 δ12 は、R ≡ pr t u によって選ばれた二つの成分、その対を証明するコンテナ、元の環境からなり、二つの項の原子式はまさにこの環境で解釈されます。

        , isTm-in i0 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (δ12 t u e) q0 q1 hu ) })
    where
    δ12 : (t u : V ℓ) (e : R ≡ pr t u) → S ^ ( + m)
    δ12 t u e = sndS rS t u e ∷ fstS rS t u e ∷ container rS (fstS rS t u e) (sndS rS t u e) e .fst ∷ δ

二項ペイロードを外向きに読むと、ペイロード a と b、等式 R ≡ pr a b、および pr A a と pr A b がともに符号集合に属することが得られます。二つの適用原子式の妥当性が、拡張環境におけるこれらの所属を同定します。

  bin-out : ⟨ δ ⊨ Sh.binPay ⟩ → BinP A R
  bin-out h = PT.map
    (λ { (a , b , s , (e , (ha , hb))) → fst a , fst b
       , ( e , ( subst ⟨_⟩ (appAt-adequate (sh  C) i8 i1 (b ∷ a ∷ s ∷ δ)) ha
               , subst ⟨_⟩ (appAt-adequate (sh  C) i8 i0 (b ∷ a ∷ s ∷ δ)) hb ) ) })

原子の場合と同じく、二項の条件の二重の存在量化は一度の消去で処理されます。

    (bothEx-out i0 binBody δ h)

内向きの読みは、名指された下位コードで二つの存在量化子を満たします。二つの適用の原子は、妥当性を逆向きに辿ってずらした文脈の中で充足されます。

  bin-in : BinP A R → ⟨ δ ⊨ Sh.binPay ⟩
  bin-in = PT.rec (snd (δ ⊨ Sh.binPay))
    (λ { (a , b , (e , (ha , hb))) →
      fillBoth i0 δ (fstS rS a b e) (sndS rS a b e) e binBody
        ( subst ⟨_⟩ (sym (appAt-adequate (sh  C) i8 i1 (δ12 a b e))) ha

二項の場合の補助定義も同じずらした文脈の形を記録します。今度は周囲の値 a と b から組み立てられます。

        , subst ⟨_⟩ (sym (appAt-adequate (sh  C) i8 i0 (δ12 a b e))) hb ) })
    where
    δ12 : (a b : V ℓ) (e : R ≡ pr a b) → S ^ ( + m)
    δ12 a b e = sndS rS a b e ∷ fstS rS a b e ∷ container rS (fstS rS a b e) (sndS rS a b e) e .fst ∷ δ

偽のペイロードには下位データがありません。その論理式は R が 0 タグのスロットに格納された値に等しいことを述べ、ConP A R は R ≡ # 0 を述べます。0 タグの等式と合成することで外向きの方向が得られます。

  con-out : ⟨ δ ⊨ Sh.conPay ⟩ → ConP A R
  con-out h = h ∙ q0

逆に、等式 R ≡ # 0 を 0 タグの等式の逆向きと合成すると、R が 0 タグのスロットの値に等しいことが示されます。これは偽のペイロードの充足そのものです。

  con-in : ConP A R → ⟨ δ ⊨ Sh.conPay ⟩
  con-in h = h ∙ sym q0

どちらの非有界量化子でも、ペイロードは後続アリティにおける本体のキーです。後続キーの読みは、このペイロード論理式の充足を pr (sucV A) R が符号集合に属することへ変換します。

  qu-out : ⟨ δ ⊨ Sh.quPay ⟩ → QuP A R
  qu-out = keyUp-out (sh  C) i5 i0 δ

逆向きには、pr (sucV A) R が符号集合に属することから後続キーの論理式に必要な証人が得られ、量化子ペイロードが証明されます。

  qu-in : QuP A R → ⟨ δ ⊨ Sh.quPay ⟩
  qu-in = keyUp-in (sh  C) i5 i0 δ

有界量化子のペイロードを外向きに読むと、項 t、本体のペイロード a、等式 R ≡ pr t a が得られます。さらに、t がアリティ A で合法であることと、本体のキー pr (sucV A) a が符号集合に属することも得られます。

  bq-out : ⟨ δ ⊨ Sh.bqPay ⟩ → BqP A R
  bq-out h = PT.map
    (λ { (t , a , s , (e , (ht , ha))) → fst t , fst a
       , ( e , ( isTm-out i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (a ∷ t ∷ s ∷ δ) q0 q1 ht
               , keyUp-out (sh  C) i8 i0 (a ∷ t ∷ s ∷ δ) ha ) ) })

有界の本体の二重の存在量化は、他の場所と同じく二重の消去で処理されます。

    (bothEx-out i0 bqBody δ h)

内向きの読みでは、境界の項がずらした文脈を通して合法性の原子に入ります。

  bq-in : BqP A R → ⟨ δ ⊨ Sh.bqPay ⟩
  bq-in = PT.rec (snd (δ ⊨ Sh.bqPay))
    (λ { (t , a , (e , (ht , ha))) →
      fillBoth i0 δ (fstS rS t a e) (sndS rS t a e) e bqBody
        ( isTm-in i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (δ12 t a e) q0 q1 ht

本体の鍵は後続の鍵の補題を通して入り、補助定義は境界の値とその容器から作られるずらした文脈の形を記録します。

        , keyUp-in (sh  C) i8 i0 (δ12 t a e) ha ) })
    where
    δ12 : (t a : V ℓ) (e : R ≡ pr t a) → S ^ ( + m)
    δ12 t a e = sndS rS t a e ∷ fstS rS t a e ∷ container rS (fstS rS t a e) (sndS rS t a e) e .fst ∷ δ

タグの読みはタグの上の再帰で選ばれます。タグ 0 と 1 が二つの原子式、タグ 2、3、4 が三つの二項結合子です。

  payN-out : (k : ℕ) → ⟨ δ ⊨ Sh.payN k ⟩ → PayN k A R
  payN-out  = atom-out
  payN-out  = atom-out
  payN-out  = bin-out
  payN-out  = bin-out

タグ 5、6、7 は偽と二つの非有界の量化子を、タグ 8 は有界の全称を担います。

  payN-out  = bin-out
  payN-out  = con-out
  payN-out  = qu-out
  payN-out  = qu-out
  payN-out  = bq-out

タグ 9 が有界の存在です。タグ 10 以上は構成子を名指さないためペイロードは空であり、読みはその空のデータの上の恒等写像です。

  payN-out  = bq-out
  payN-out (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) h = h

内向きの読みも同じ再帰で選ばれ、タグごとに一つの節をもちます。

  payN-in : (k : ℕ) → PayN k A R → ⟨ δ ⊨ Sh.payN k ⟩
  payN-in  = atom-in
  payN-in  = atom-in
  payN-in  = bin-in
  payN-in  = bin-in

タグ 4 から 7 までが一覧を続けます。最後の二項結合子、偽、そして二つの非有界の量化子です。

  payN-in  = bin-in
  payN-in  = con-in
  payN-in  = qu-in
  payN-in  = qu-in
  payN-in  = bq-in

タグ 9 が一覧を完成させます。10 以上を読むべきものはありません。そのようなタグをもつ合法な鍵はないからです。

  payN-in  = bq-in
  payN-in (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) h = h

十通りの読みは、周囲の環境を七項目だけ拡張した環境でタグ付きペイロードを解釈します。符号集合と定数アルファベットは周囲の項目から読み、N は周囲の環境にある十個の位置を選びます。タグの仮定は、それらの値をそれぞれ数項 0 から 9 までと同定します。

module TenRead {m : ℕ} (C w : Fin m) (N : Fin  → Fin m) (δ : S ^ ( + m))
  (tg : Tags δ (shN  N)) where
  private
    Cv = fst (lookup (sh  C) δ)
    Wv = fst (lookup (sh  w) δ)

新たに束縛された項目のうち、A はアリティであり、P はキーとして認識すべきタグ付きペイロードです。P の集合レベルの表示を保つことで、タグとそのペイロード r を選んだときに等式 P ≡ pr (# (toℕ j)) r を実現できます。

    A = fst (lookup i3 δ)
    P = fst (lookup i0 δ)
    pS = lookup i0 δ
    module Sh = Shape C w N
  open CodesSem Wv Cv

タグの読みは、j 番目のタグの原子の充足を鍵へ変換します。切り詰められた証人は添字 r と容器の対であり、符号化の等式は、j 番目のタグのスロットが j の数項を名指すというタグの等式に沿って輸送され、ペイロードはタグ j での読みによって読まれます。

  at-out : (j : Fin ) → ⟨ δ ⊨ Sh.at j ⟩ → Key A P
  at-out j h = PT.map
    (λ { (r , s , (e , hp)) → j , fst r
       , ( e ∙ cong (λ a → pr a (fst r)) (tg j)
         , PayRead.payN-out C w N (r ∷ s ∷ δ) tg (toℕ j) hp ) })

タグの原子の二重の存在量化はみずからの消去で処理されるため、読みが添字を選ぶことはありません。充足が与える一つを展開するだけです。

    (sndEx-out i0 (sh  (N j)) (Sh.pay j) δ h)

内向きの方向は、鍵から充足を組み立てます。証人の項目はずらした値で満たされ、ペイロードは拡張された文脈の上で内向きに読まれ、タグの等式が名指しのスロットを j の数項と同一視します。

  at-in : (j : Fin ) (r : V ℓ) (e : P ≡ pr (# (toℕ j)) r) → PayN (toℕ j) A r → ⟨ δ ⊨ Sh.at j ⟩
  at-in j r e pay =
    fillSnd i0 δ (lookup (sh  (N j)) δ) rS e' (Sh.pay j)
      (PayRead.payN-in C w N (rS ∷ container pS (lookup (sh  (N j)) δ) rS e' .fst ∷ δ) tg (toℕ j) pay)
      (sh  (N j)) refl

改名された値は j の数項と選ばれた項目を対にし、符号化の等式はタグの等式と逆向きに合成されて、拡張された名指しが正しいスロットに触れるようにします。

    where
    rS : S
    rS = sndS pS (# (toℕ j)) r e
    e' : P ≡ pr (fst (lookup (sh  (N j)) δ)) (fst rS)
    e' = e ∙ cong (λ a → pr a r) (sym (tg j))

十通りの外向きの読みは選言を消費し、証人が名指すタグのところでタグの読みを引用します。

  ten-out : ⟨ δ ⊨ Sh.ten ⟩ → Key A P
  ten-out h = PT.rec squash₁ (λ { (j , hj) → at-out j hj }) (bigOr-out δ  Sh.at h)

内向きの読みは、証人の現れたタグで選言に入り、ペイロードもそのタグで内向きに読まれます。二つの方向合わせて、十通りの選言の充足と、合法な鍵をもつことは同じことだと述べています。

  ten-in : Key A P → ⟨ δ ⊨ Sh.ten ⟩
  ten-in = PT.rec (snd (δ ⊨ Sh.ten))
    (λ { (j , r , (e , pay)) → bigOr-in δ  Sh.at j (at-in j r e pay) })

形の読みは三つの周囲の集合を固定します。候補となる符号集合 C、定数アルファベット w、そしてアリティと族の対からなる塔 E です。それぞれの基礎にある反復集合は、符号の所属、定数項の合法性、塔に属する証人 (ar,F) に用いられます。

module ShapeRead {m : ℕ} (C w E : Fin m) (N : Fin  → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Cv = fst (lookup C γ)
    Wv = fst (lookup w γ)
    Ev = fst (lookup E γ)

選ばれた要素 c と塔の証人 (ar,F) に対し、残りの論理式はペイロード p を選び、c ≡ pr ar p を要求し、十通りのタグ形に照らして p を検査します。このように、入れ子になった証人は外側のアリティと内側のタグ付きペイロードを別々に明らかにします。

    module Sh = Shape C w N
    inner : Formula S ( + m)
    inner = sndEx i4 i1 Sh.ten
  open CodesSem Wv Cv

Shaped c は形の節から取り出されるデータをそのまま記録します。pr ar F が E に属し、c ≡ pr ar p が成り立ち、p がアリティ ar における合法なタグ付きペイロードとなる ar、F、p が存在します。この存在データはすべて命題的に切り詰められており、分解の一意性は主張しません。

  Shaped : V ℓ → Type (ℓ-suc ℓ)
  Shaped c = ∥ Σ[ ar ∈ V ℓ ] Σ[ F ∈ V ℓ ] Σ[ p ∈ V ℓ ]
               (⟨ pr ar F ∈ Ev ⟩ × ((c ≡ pr ar p) × Key ar p)) ∥₁

符号集合の各 c について、外向きの読みはまず E の要素 q を得ます。q を分解すると ar と F および等式 q ≡ pr ar F が得られ、内側の存在量化からは p、等式 c ≡ pr ar p、十通りのペイロード論理式の充足が得られます。

  shape-out : ⟨ γ ⊨ shapeAt C w E N ⟩ → (c : S) → ⟨ fst c ∈ Cv ⟩ → Shaped (fst c)
  shape-out h c c∈ = PT.rec squash₁
    (λ { (q , (q∈ , hb)) → PT.rec squash₁
      (λ { (ar , F , s , (eq , hs)) → PT.map
        (λ { (p , s' , (ec , ht)) →

等式 q ≡ pr ar F は、既知の q の E への所属を pr ar F の所属へ輸送します。c に関する等式は保持され、十通りの読みが残りの充足証明を Key ar p へ変換します。

          fst ar , fst F , fst p
          , ( subst (λ u → ⟨ u ∈ Ev ⟩) eq q∈
            , ( ec , TenRead.ten-out C w N (p ∷ s' ∷ F ∷ ar ∷ s ∷ q ∷ c ∷ γ) tg ht ) ) })
        (sndEx-out i4 i1 Sh.ten (F ∷ ar ∷ s ∷ q ∷ c ∷ γ) hs) })
      (bothEx-out i0 inner (q ∷ c ∷ γ) hb) })

元の形の充足は符号集合の要素について全称量化されています。これを c とその所属証明に適用すると、上で除去した存在データが得られ、Shaped (fst c) の構成が完了します。

    (h c c∈)

内向きの方向では、符号集合の各要素 c が切り詰められた形のデータをもつと仮定します。その切り詰めを除去すると、ar、F、p とともに、pr ar F の E への所属、c に関する等式、Key ar p が得られます。目標自体が命題なので、この除去は正当です。

  shape-in : ((c : S) → ⟨ fst c ∈ Cv ⟩ → Shaped (fst c)) → ⟨ γ ⊨ shapeAt C w E N ⟩
  shape-in k c c∈ = PT.rec (snd ((c ∷ γ) ⊨ ∃̇∈ (var (sh  E)) (bothEx i0 inner)))
    (λ { (ar , F , p , (q∈ , (ec , key))) →
      let qS = down (lookup E γ) (pr ar F) q∈
          arS = fstS qS ar F refl

pr ar F が E に属することから集合レベルの表示 qS が得られ、その二成分がそれぞれ ar と F を表します。これとは別に、等式 c ≡ pr ar p は c の内部でペイロードの表示 pS を選びます。二つの対コンテナが、入れ子の存在論理式に必要な環境を与えます。

          FS = sndS qS ar F refl
          δ2 = qS ∷ c ∷ γ
          cq = container qS arS FS refl
          δ5 = FS ∷ arS ∷ cq .fst ∷ δ2
          pS = sndS c ar p ec

内側の論理式はアリティと表のデータで満たされ、十通りの選言は鍵で満たされます。こうして形の充足の全体が、実際のデータから組み上がります。

          cp = container c arS pS ec
          δ7 = pS ∷ cp .fst ∷ δ5
      in ∣ qS , ( q∈ , fillBoth i0 δ2 arS FS refl inner
            (fillSnd i4 δ5 arS pS ec Sh.ten
              (TenRead.ten-in C w N δ7 tg key) i1 refl) ) ∣₁ })

仮定した形の割り当てを c とその所属に適用すると、内向きの構成で用いる切り詰められた証人がちょうど得られます。外向きの方向と合わせると、符号集合の各要素について、形の論理式の充足が命題 Shaped と一致することが分かります。

    (k c c∈)

塔の要素を q ≡ pr ar F と分解した後で、各閉性の節を解釈します。得られる四項目の拡張では、A は固定されたアリティ ar です。符号集合と定数アルファベットは周囲の環境から引き続き参照でき、タグ等式もシフト後に保たれます。

module CloseRead {m : ℕ} (C w : Fin m) (N : Fin  → Fin m) (δ : S ^ ( + m)) (tg : Tags δ (shN  N)) where
  private
    Cv = fst (lookup (sh  C) δ)
    A = fst (lookup i1 δ)
    arS = lookup i1 δ

この固定アリティで、閉性条件は、必要な形の入力に十個の構成子のいずれかを適用すると結果が再び符号集合に属することを述べます。各節について、外向きと内向きの読みは、その有界論理式を対応する閉性と同定します。

    CS = lookup (sh  C) δ
    module Cl = Close C w N

原子の閉性の節を外向きに読むと、X が選ぶ境界から任意の x を取り、さらに x で拡張した環境で Y が選ぶ境界から任意の y を取れます。その結果、アリティ A、構成子タグ k、項の形を示すタグ Nx と Ny をもつ原子キーが符号集合に属することが得られます。

  atomClose-out : (k Nx Ny : Fin ) (X : Fin ( + m)) (Y : Fin ( + m))
                → ⟨ δ ⊨ Cl.atomClose k Nx Ny X Y ⟩
                → (x y : S) → ⟨ fst x ∈ fst (lookup X δ) ⟩ → ⟨ fst y ∈ fst (lookup Y (x ∷ δ)) ⟩
                → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (pr (# (toℕ Ny)) (fst y)))) ∈ Cv ⟩
  atomClose-out k Nx Ny X Y h x y x∈ y∈ =

この所属は、三つのタグの等式に沿って輸送されます。節はタグつきのスロットで述べられる一方、鍵は三つのタグの数項で書かれるからです。

    subst (λ u → ⟨ u ∈ Cv ⟩)
      (cong (pr A) (cong₂ pr (tg k) (cong₂ pr (cong (λ a → pr a (fst x)) (tg Nx)) (cong (λ a → pr a (fst y)) (tg Ny)))))
      (atomKey-out (sh  C) i3 (sh  (N k)) (sh  (N Nx)) i1 (sh  (N Ny)) i0 (y ∷ x ∷ δ) (h x x∈ y y∈))

内向きの方向は節を組み立て直します。すべての対に対する性質が与えられていれば、与えられた x と y で具体化し、名指しの等式を逆向きに走らせれば足ります。

  atomClose-in : (k Nx Ny : Fin ) (X : Fin ( + m)) (Y : Fin ( + m))
               → ((x y : S) → ⟨ fst x ∈ fst (lookup X δ) ⟩ → ⟨ fst y ∈ fst (lookup Y (x ∷ δ)) ⟩
                  → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (pr (# (toℕ Ny)) (fst y)))) ∈ Cv ⟩)
               → ⟨ δ ⊨ Cl.atomClose k Nx Ny X Y ⟩
  atomClose-in k Nx Ny X Y g x x∈ y y∈ =

所属は逆向きの改名に沿ってタグつきのスロットへ輸送され、閉包の節の導入規則がこの場合を閉じます。

    atomKey-in (sh  C) i3 (sh  (N k)) (sh  (N Nx)) i1 (sh  (N Ny)) i0 (y ∷ x ∷ δ)
      (subst (λ u → ⟨ u ∈ Cv ⟩)
        (sym (cong (pr A) (cong₂ pr (tg k) (cong₂ pr (cong (λ a → pr a (fst x)) (tg Nx)) (cong (λ a → pr a (fst y)) (tg Ny))))))
        (g x y x∈ y∈))

二項の閉性の節は、符号集合の二つの要素 c₁ と c₂ を量化します。等式 fst c₁ ≡ pr A (fst a) と fst c₂ ≡ pr A (fst b) は、固定アリティ A におけるそれぞれのペイロード a と b を取り出します。すると、この節はペイロード pr (fst a) (fst b) をもつ二項キーが再び符号集合に属することを述べます。

  binClose-out : (k : Fin ) → ⟨ δ ⊨ Cl.binClose k ⟩
               → (c₁ c₂ a b : S) → ⟨ fst c₁ ∈ Cv ⟩ → ⟨ fst c₂ ∈ Cv ⟩
               → fst c₁ ≡ pr A (fst a) → fst c₂ ≡ pr A (fst b)
               → ⟨ pr A (pr (# (toℕ k)) (pr (fst a) (fst b))) ∈ Cv ⟩
  binClose-out k h c₁ c₂ a b c₁∈ c₂∈ e₁ e₂ =

所属はタグの改名に沿って輸送され、二重に入れ子になった全称の層は有界量化子の消去の補題によって処理されます。各項目はみずからの対の容器を通して内側の節に入ります。

    subst (λ u → ⟨ u ∈ Cv ⟩) (cong (pr A) (cong (λ v → pr v (pr (fst a) (fst b))) (tg k)))
      (binKey-out (sh  C) i7 (sh  (N k)) i3 i0 δ10
        (useSnd i0 δ8 arS b e₂ (binKey (sh  C) i7 (sh  (N k)) i3 i0) i5 refl
          (useSnd i0 (c₁ ∷ δ) arS a e₁ inner i2 refl (h c₁ c₁∈) c₂ c₂∈)))
    where

c₁ を選んで pr A a と表した後、内側の論理式は符号集合の第二の符号 c₂ を量化し、それを pr A b として取り出します。次に、タグ k と対にしたペイロード pr a b からなる二項キーが符号集合に属することを要求します。補助環境は c₁ と c₂ の二つの分解を記録します。

    inner : Formula S ( + m)
    inner = ∀̇∈ (var (sh  C)) (sndAll i0 i5 (binKey (sh  C) i7 (sh  (N k)) i3 i0))
    δ7 : S ^ ( + m)
    δ7 = a ∷ container c₁ arS a e₁ .fst ∷ c₁ ∷ δ
    δ8 : S ^ ( + m)

量化子の条項では、下位キーと、そのアリティを定めるデータを同時に覚えておく必要があります。環境 δ8 は、候補となる引数 a、後続アリティの候補 ar'、両者の関係を証明する順序対、下位キー c₁ を含みます。有界量化子を扱う δ10 には、境界となる項も加わります。

    δ8 = c₂ ∷ δ7
    δ10 : S ^ ( + m)
    δ10 = b ∷ container c₂ arS b e₂ .fst ∷ δ8

二項閉包の条項を内向きに読むときは、対応する数学的な閉包則から出発します。同じアリティをもつ二つの下位キーが領域に属するなら、それらから作られる複合キーも領域に属します。二つの全称量化は、選んだ下位キーを明示するためのものです。

  binClose-in : (k : Fin )
              → ((c₁ c₂ a b : S) → ⟨ fst c₁ ∈ Cv ⟩ → ⟨ fst c₂ ∈ Cv ⟩
                 → fst c₁ ≡ pr A (fst a) → fst c₂ ≡ pr A (fst b)
                 → ⟨ pr A (pr (# (toℕ k)) (pr (fst a) (fst b))) ∈ Cv ⟩)
              → ⟨ δ ⊨ Cl.binClose k ⟩

二つの量化された成分を論理式が定める順に導入すると、対応する拡張環境が得られます。最も内側の含意では、仮定した閉包則から複合キーの所属が得られ、タグの等式 tg k が、表示されたタグを binKey の要求する数項に揃えます。

  binClose-in k g c₁ c₁∈ = sndAll-in i0 i2 (∀̇∈ (var (sh  C)) (sndAll i0 i5 (binKey (sh  C) i7 (sh  (N k)) i3 i0))) (c₁ ∷ δ) (λ a s s∈ a∈ e₁ c₂ c₂∈ →
    sndAll-in i0 i5 (binKey (sh  C) i7 (sh  (N k)) i3 i0) (c₂ ∷ a ∷ s ∷ c₁ ∷ δ) (λ b s' s'∈ b∈ e₂ →
      binKey-in (sh  C) i7 (sh  (N k)) i3 i0 (b ∷ s' ∷ c₂ ∷ a ∷ s ∷ c₁ ∷ δ)
        (subst (λ u → ⟨ u ∈ Cv ⟩) (sym (cong (pr A) (cong (λ v → pr v (pr (fst a) (fst b))) (tg k))))
          (g c₁ c₂ a b c₁∈ c₂∈ e₁ e₂))))

偽の符号には調べるべき下位符号がありません。したがって、その閉包条項を外向きに読むには、ペイロードが零の数項に等しいことを用い、タグの等式に沿って輸送すれば十分です。

  conClose-out : (k : Fin ) → ⟨ δ ⊨ Cl.conClose k ⟩ → ⟨ pr A (pr (# (toℕ k)) (# )) ∈ Cv ⟩
  conClose-out k h =
    subst (λ u → ⟨ u ∈ Cv ⟩) (cong (pr A) (cong₂ pr (tg k) (tg f0)))
      (unKey-out (sh  C) i1 (sh  (N k)) (sh  (N f0)) δ h)

逆に、偽のキーの所属を同じ等式に沿って反対向きに輸送すれば、閉包条項の充足が得られます。この場合には再帰的な前提がなく、零のペイロードだけでキーが完全に定まります。

  conClose-in : (k : Fin ) → ⟨ pr A (pr (# (toℕ k)) (# )) ∈ Cv ⟩ → ⟨ δ ⊨ Cl.conClose k ⟩
  conClose-in k h =
    unKey-in (sh  C) i1 (sh  (N k)) (sh  (N f0)) δ
      (subst (λ u → ⟨ u ∈ Cv ⟩) (sym (cong (pr A) (cong₂ pr (tg k) (tg f0)))) h)

非有界量化子の条項は、量化された成分を明示して外向きに読まれます。領域の下位キー c₁、その表示 c₁ = pr ar' a、そして等式 ar' = sucV A が与えられれば、現在のアリティでの量化子のキーが領域に属します。三つの仮定は、前者のスライスの要素のデータそのものです。

  quClose-out : (k : Fin ) → ⟨ δ ⊨ Cl.quClose k ⟩
              → (c₁ ar' a : S) → ⟨ fst c₁ ∈ Cv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
              → ⟨ pr A (pr (# (toℕ k)) (fst a)) ∈ Cv ⟩
  quClose-out k h c₁ ar' a c₁∈ e₁ es =
    subst (λ u → ⟨ u ∈ Cv ⟩) (cong (pr A) (cong (λ v → pr v (fst a)) (tg k)))

証明では、a、ar'、コンテナを環境に加え、後続の等式を用いて含意の結論へ進み、八つのスロットをもつ環境で unKey の所属を読み取ります。さらにタグの等式に沿って輸送し、タグ k が表す数項に対応する所属を得ます。

      (unKey-out (sh  C) i5 (sh  (N k)) i0 δ8
        (useBoth i0 (c₁ ∷ δ) ar' a e₁ (sucAtL i5 i1 ⇒̇ unKey (sh  C) i5 (sh  (N k)) i0) (h c₁ c₁∈)
          (suc-in i5 i1 δ8 es)))
    where
    δ8 : S ^ ( + m)

拡張された環境は、量化された三つの成分を、含意が読む順に、もとの成分とともにまとめます。

    δ8 = a ∷ ar' ∷ container c₁ ar' a e₁ .fst ∷ c₁ ∷ δ

内向きに読むときは、条項で量化された二つの成分を導入します。拡張環境には、後続アリティの候補 ar' とペイロード a が入り、後続の等式が含意の前提を与えます。

  quClose-in : (k : Fin )
             → ((c₁ ar' a : S) → ⟨ fst c₁ ∈ Cv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
                → ⟨ pr A (pr (# (toℕ k)) (fst a)) ∈ Cv ⟩)
             → ⟨ δ ⊨ Cl.quClose k ⟩
  quClose-in k g c₁ c₁∈ = bothAll-in i0 (sucAtL i5 i1 ⇒̇ unKey (sh  C) i5 (sh  (N k)) i0) (c₁ ∷ δ) (λ ar' a s s∈ ar'∈ a∈ e₁ hs →

これらのデータに仮定した閉包則を適用し、得られた所属をタグの等式に沿って輸送すると、unKey の結論が得られます。これで、非有界量化子の条項を内向きに読む証明が完成します。

    unKey-in (sh  C) i5 (sh  (N k)) i0 (a ∷ ar' ∷ s ∷ c₁ ∷ δ)
      (subst (λ u → ⟨ u ∈ Cv ⟩) (sym (cong (pr A) (cong (λ v → pr v (fst a)) (tg k))))
        (g c₁ ar' a c₁∈ e₁ (suc-out i5 i1 (a ∷ ar' ∷ s ∷ c₁ ∷ δ) hs))))

有界量化子の条項には前提が一つ加わります。後続アリティでの本体キーに加えて、現在のアリティで正しい境界項 x が必要です。得られるペイロードは、量化子のタグ、項のタグ Nx、その項、本体のペイロードを入れ子の順序対として記録します。

  bqClose-out : (k Nx : Fin ) (X : Fin ( + m)) → ⟨ δ ⊨ Cl.bqClose k Nx X ⟩
              → (c₁ ar' a : S) → ⟨ fst c₁ ∈ Cv ⟩ → (e₁ : fst c₁ ≡ pr (fst ar') (fst a)) → fst ar' ≡ sucV A
              → (x : S) → ⟨ fst x ∈ fst (lookup X (a ∷ ar' ∷ container c₁ ar' a e₁ .fst ∷ c₁ ∷ δ)) ⟩
              → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (fst a))) ∈ Cv ⟩
  bqClose-out k Nx X h c₁ ar' a c₁∈ e₁ es x x∈ =

証明では、境界を表す項を環境に加え、その環境で有界キーの消去を適用します。二つのタグ等式は、それぞれ量化子の構成子と項の構成子に対応し、入れ子の対を結論で指定された形へ輸送します。

    subst (λ u → ⟨ u ∈ Cv ⟩)
      (cong (pr A) (cong₂ pr (tg k) (cong (λ v → pr v (fst a)) (cong (λ v → pr v (fst x)) (tg Nx)))))
      (bndKey-out (sh  C) i6 (sh  (N k)) (sh  (N Nx)) i0 i1 (x ∷ δ8)
        (useBoth i0 (c₁ ∷ δ) ar' a e₁ (sucAtL i5 i1 ⇒̇ ∀̇∈ (var X) (bndKey (sh  C) i6 (sh  (N k)) (sh  (N Nx)) i0 i1))
          (h c₁ c₁∈) (suc-in i5 i1 δ8 es) x x∈))

八つの枠の環境は、非有界の場合と同じまとめ方を繰り返し、界の枠は消去に使われます。

    where
    δ8 : S ^ ( + m)
    δ8 = a ∷ ar' ∷ container c₁ ar' a e₁ .fst ∷ c₁ ∷ δ

内向きに読むため、型に示された数学的閉包則を仮定します。この規則が任意の拡張環境 s について量化されているのは、境界を表す項を選ぶ集合が、その環境で評価されるからです。

  bqClose-in : (k Nx : Fin ) (X : Fin ( + m))
             → ((c₁ ar' a s : S) → ⟨ fst c₁ ∈ Cv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
                → (x : S) → ⟨ fst x ∈ fst (lookup X (a ∷ ar' ∷ s ∷ c₁ ∷ δ)) ⟩
                → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (fst a))) ∈ Cv ⟩)
             → ⟨ δ ⊨ Cl.bqClose k Nx X ⟩

量化された下位キーのデータと境界を表す項を導入し、得られた環境で仮定した閉包則を適用します。その結論を二つのタグ等式に沿って輸送すると、bndKey が要求する所属が得られ、有界量化子の条項を内向きに読む証明が完成します。

  bqClose-in k Nx X g c₁ c₁∈ = bothAll-in i0 (sucAtL i5 i1 ⇒̇ ∀̇∈ (var X) (bndKey (sh  C) i6 (sh  (N k)) (sh  (N Nx)) i0 i1)) (c₁ ∷ δ) (λ ar' a s s∈ ar'∈ a∈ e₁ hs x x∈ →
    bndKey-in (sh  C) i6 (sh  (N k)) (sh  (N Nx)) i0 i1 (x ∷ a ∷ ar' ∷ s ∷ c₁ ∷ δ)
      (subst (λ u → ⟨ u ∈ Cv ⟩)
        (sym (cong (pr A) (cong₂ pr (tg k) (cong (λ v → pr v (fst a)) (cong (λ v → pr v (fst x)) (tg Nx))))))
        (g c₁ ar' a s c₁∈ e₁ (suc-out i5 i1 (a ∷ ar' ∷ s ∷ c₁ ∷ δ) hs) x x∈)))

健全性：各要素の復号

健全性を証明するため、ここまでに得た三つの記述を結びます。数値タグは十種類の構成子を識別し、形と閉包の論理式は集合内部の符号を記述し、AllCodes はそれらの符号を外部の論理式文法へ結び戻します。関係する性質は命題なので、代表を選ばずに切り詰められた証人を除去できます。

open import L.Coding.Expressions {ℓ} using ( tagAtL-adequate )
open import L.Coding.Closure {ℓ} using ( closedAt; binSameClosed-in; unSuccClosed-in; binSuccClosed-in )
open import L.Coding.CodeShape {ℓ} using
  ( shapedAt; shaped-in; ShapeWit; BinWit; bothTm; fstTm; noneB; isTmAt )
open import L.Coding.CodeSet {ℓ} lem using

標準的な符号集合は、この比較の両方向を与えます。その要素は論理式キーとして読め、どの論理式にも標準的なキーがあります。残りの導入からは、記録されたアリティの証人と、二つの命題の連言も命題であるという事実を得ます。

  ( AllCodes; AllCodes-out; key∈AllCodes; keyS; codeS; witnessAt-out )
open import Cubical.Foundations.HLevels using ( isProp× )

定数として現れうる要素をもつ作業集合 Wv と、候補となる符号領域 Cv を固定します。以下の議論はこの二つの集合をパラメータとし、この時点では Cv が標準的な領域 AllCodes であるとは仮定しません。

module _ (Wv Cv : V ℓ) where
  open CodesSem Wv Cv

どのペイロード条件 PayN n ar r も命題です。タグ 0 から 4 については命題的切り詰めから直ちに従います。対応する条件は、適切な成分が単に存在することだけを述べるからです。

  isPropPayN : (n : ℕ) (ar r : V ℓ) → isProp (PayN n ar r)
  isPropPayN  ar r = squash₁
  isPropPayN  ar r = squash₁
  isPropPayN  ar r = squash₁
  isPropPayN  ar r = squash₁

残りの構成子タグでも、各ペイロードに応じた形で同じ原理を用います。偽のペイロードは零に一意に等しく、非有界量化子は命題値をとる Cv への所属を要求し、有界量化子は再び切り詰められた存在を用います。

  isPropPayN  ar r = squash₁
  isPropPayN  ar r = setIsSet r (# )
  isPropPayN  ar r = snd (pr (sucV ar) r ∈ Cv)
  isPropPayN  ar r = snd (pr (sucV ar) r ∈ Cv)
  isPropPayN  ar r = squash₁

タグ 9 も切り詰められた存在によって扱われます。十種類の構成子タグを越える数項ではペイロード型が空であり、空型は命題です。したがって PayN は、どの自然数タグについても命題値をとります。

  isPropPayN  ar r = squash₁
  isPropPayN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) ar r = Empty.isProp⊥*

キーを揃える補題は、アリティ ar での Key を、同じ集合の別の分解 p = (# n, r) でのペイロードへ変えます。対の単射性と数項の単射性が、タグとペイロードを別々に揃えます。そして PayN n ar r は命題なので、切り詰められたキーをそこへ消去できます。

  keyAt : (ar p : V ℓ) → Key ar p → (n : ℕ) (r : V ℓ) → p ≡ pr (# n) r → PayN n ar r
  keyAt ar p key n r e = PT.rec (isPropPayN n ar r)
    (λ { (k , r' , (e' , pay)) →
      let q = pr-inj (sym e ∙ e')
      in subst2 (λ j x → PayN j ar x) (sym (#-inj′ (q .fst))) (sym (q .snd)) pay })

この除去を key に適用すると、位置合わせが完了します。Key から得たタグとペイロードは、指定された数項 n とペイロード r へすでに輸送されています。

    key

最初の復元の補題は、項の符号の主張を、形の章の項の述語の充足へ変換します。任意の枠に対して述べられ、切り詰められた IsTmV を、命題値の充足へ消去することで証明されます。

tmWit : ∀ {j} (ti Ni Ai : Fin j) (env : S ^ j)
      → IsTmV (fst (lookup Ai env)) (fst (lookup ti env)) (fst (lookup Ni env))
      → ⟨ env ⊨ isTmAt ti Ni Ai ⟩
tmWit ti Ni Ai env = PT.rec (snd (env ⊨ isTmAt ti Ni Ai))
  (λ { (inl (x , (e , x∈))) →

定数の分岐では、down が証人 x を作業集合 Wv の要素として表示します。タグの妥当性が順序対の等式を輸送し、もとの所属証明がもう一方の連言肢を与えます。得られた証拠は、形の述語の左の選言肢に入ります。

         ∣ inl ∣ down (lookup Ai env) x x∈
           , ( subst ⟨_⟩ (sym (tagAtL-adequate (suc ti)  zero (down (lookup Ai env) x x∈ ∷ env))) e
             , x∈ ) ∣₁ ∣₁
     ; (inr (i , (e , i∈))) →
         ∣ inr ∣ down (lookup Ni env) i i∈