名前の比較の妥当性

module _ {n : ℕ} (e a B : Fin n) (γ : Vec S n) (k : ℕ)
         (qa : (lookup a γ) .fst ≡ # k) (qB : (lookup B γ) .fst ≡ A)
         (h : ⟨ γ ⊨ envOverAt e a B ⟩) where

private module R = Recover Aʟ k γ e a B qa qB h

復元された族は実際のデータなので、長さ k のベクトルに表としてまとめられる。ここで選択によって切り詰めを外しているわけではない。各添字について、定義域条件は成分の単なる存在しか与えないが、一価性により成分の型は命題になる。したがって、命題的切り詰めをその命題へ除去して、一意な成分を得られる。その値は A に属し、台の所属ファイバーが対応する ⟪ A ⟫ の要素を切り詰めなしで与える。これらの要素に FinVec→Vec を適用したものが paramSeq-out である。

paramSeq-out : Vec ⟪ A ⟫ k
paramSeq-out = FinVec→Vec R.g

表への変換は族の表示を変えるため、グラフの等しさによって往復を閉じる。R.recovers は、スロット e の集合を復元された有限族のグラフと同一視する。続いて FinVec→Vec の参照則が、表にしたベクトルの各成分を対応する族の値と同一視する。関数外延性と env の合同性により、これらの点ごとのパスはグラフの等しさへ持ち上がる。したがって、復元されたベクトルはもとの環境集合を正確に表示し、順序対条件が排除する余分な要素も含まない。

paramSeq-graph : (lookup e γ) .fst
               ≡ env (λ i → ix (lookup i paramSeq-out))
paramSeq-graph = R.recovers
               ∙ cong env (funExt (λ i → cong ix (sym (lookup-tab R.g i))))

module Named {n : ℕ} (B C C₀ s a e d : Fin n) (γ : Vec S n)
             (qB : lookup B γ ≡ Aʟ)
             (qC : (lookup C γ) .fst ≡ (AllCodes Aʟ) .fst)
             (q₀ : (lookup C₀ γ) .fst ≡ (AllCodes ∅ʟ) .fst) where

private

Fo は、論理式の台へのこの依存を切り出す。モデル要素 X とアリティ j に対して、Fo X j は、小さい要素型 ⟪ X .fst ⟫ から定数を取る論理式の型である。したがって、スロットに保存された台の上で読む論理式は、意味論的な比較を始める前から正しい型をもつ。後になって基礎集合の等しさだけで、この依存する台を置き換えることはできない。

  Fo : S → ℕ → Type ℓ
  Fo X j = Formula ⟪ X .fst ⟫ j

名前 t に対して、まず無パラメータ論理式 formula t を、固定した台 A の要素を定数として許す論理式へ埋め込む。もとの定数域は空なので、実際のパラメータは追加されない。次に、その型を sym qB に沿って Fo Aʟ から Fo (lookup B γ) へ輸送し、ψAt t を得る。この輸送が可能なのは、qB が台のモデル要素全体を同一視するからである。こうして得られたスロット相対的な論理式について、その鍵と充足関係の値を、上で作った固定台上の構成と比較できるようになる。

  ψAt : (t : Name) → Fo (lookup B γ) (suc (arity t))
  ψAt t = subst (λ X → Fo X (suc (arity t))) (sym qB) (embed (formula t))

記述で使う論理式は、まず固定された台 Aʟ からスロット B に格納された台へ輸送される。論理式の型そのものが台に依存するため、qB は基礎集合だけでなく、証明を伴う台全体を同一視しなければならない。qB に関するパス帰納法により、符号集合の鍵を作る操作がこの輸送と可換であることが分かる。したがって、スロットの台で ψAt t から得る鍵と、Aʟ で embed (formula t) から得る鍵は同じ集合である。

  keyψ : (t : Name)
       → (keyS (lookup B γ) (ψAt t)) .fst
       ≡ (keyS Aʟ (embed (formula t))) .fst
  keyψ t = sym (constSubstCommSlice (λ X → Fo X (suc (arity t))) (V ℓ)
    (λ X ψ → (keyS X ψ) .fst) (sym qB) (embed (formula t)))

統一充足関係の値にも同じ依存性がある。スロットの台では、輸送された論理式の定数をその台へ改名してから Sat を適用する。Aʟ では、対応する埋め込み済みの論理式を改名して Sat を適用する。qB に沿う代入はこの構成全体と可換なので、二つの充足関係集合の基礎集合は等しくなる。

  satψ : (t : Name)
       → (Sat (lookup B γ) (mapFo (asConst (lookup B γ)) (ψAt t))) .fst
       ≡ (Sat Aʟ (mapFo (asConst Aʟ) (embed (formula t)))) .fst
  satψ t = sym (constSubstCommSlice (λ X → Fo X (suc (arity t))) (V ℓ)
    (λ X ψ → (Sat X (mapFo (asConst X) ψ)) .fst)

パス帰納法の原理へ最後に渡す引数は、埋め込まれた論理式そのものである。これで satψ の証明が閉じる。ここに独立な意味論的選択はなく、等式は依存的な構成で台を代入することだけから従う。keyψ と satψ を合わせると、後の表示の議論は、論理式の鍵とその充足関係集合を揃えたまま、スロットの台と Aʟ の間を移動できる。

    (sym qB) (embed (formula t)))

固定したメタ言語の名前 t に対して、Data t はそれを表すために必要な四つのスロット等式を記録する。骨格のスロットは codeOf t の基礎集合を、アリティのスロットは # (arity t) を、パラメータのスロットは環境グラフ env (pfam t) を、表示のスロットは denote t を保持する。この四つの等式は NameAt の四つの概念的な連言項に対応する。ここで述べるのは現在のスロットがこの特定の名前と揃っていることであり、同じ指示対象をもつすべての名前の一意性ではない。

Data : Name → Type (ℓ-suc ℓ)
Data t = ((lookup s γ) .fst ≡ (codeOf t) .fst)
       × ( ((lookup a γ) .fst ≡ # (arity t))
         × ( ((lookup e γ) .fst ≡ env (pfam t))
           × ((lookup d γ) .fst ≡ denote t) ) )

表示の条件を denote t と比較するため、モジュール Body は t と Data t の最初の三成分を固定する。骨格の等式 qs が論理式の鍵をそろえ、パラメータの等式 qe がパラメータ・グラフをそろえる。アリティの等式 qa は同じ名前について残るスロットの対応を記録するが、t が固定された後の表示の議論では、拡張環境の長さを suc (arity t) として直接得る。非公開のベクトル δp は、充足関係の橋が要求する制限された意味論的な台の中でパラメータを表す。

module Body (t : Name) (qs : (lookup s γ) .fst ≡ (codeOf t) .fst)
            (qa : (lookup a γ) .fst ≡ # (arity t))
            (qe : (lookup e γ) .fst ≡ env (pfam t)) where
  private
    δp : Vec NM.DA.SM (arity t)

名前のパラメータは、すでに小さな要素型 ⟪ A ⟫ に属している。それぞれに NM.DA.ι を写す操作は、添字を保つだけではない。各添字が表す集合に、その集合が A に属する証明を組み合わせて、制限モデルの台 NM.DA.SM の要素にする。得られるベクトル δp の長さは arity t であり、名前の論理式を評価する内側の環境の尾部そのものである。

    δp = map NM.DA.ι (params t)

スロット等式 qe は外側のパラメータ族 pfam t によって同じパラメータを記述するが、充足関係の橋が必要とするのは、制限された台のベクトル δp のグラフである。等式 valuesOf t は二つの表現を成分ごとに同一視する。これを qe と合成して得る qd' は、パラメータのスロットがちょうど envGraph Aʟ δp を含むことを述べる。この形は、拡張環境を作るときにも、後で与えられた拡張環境を識別するときにも使われる。

    qd' : (lookup e γ) .fst ≡ envGraph Aʟ δp
    qd' = qe ∙ valuesOf t

表示の中身にある第四の条件は、その鍵を同一視する。封印された要素 keyAt t から始めると、keyAt-fst が埋め込まれた論理式の符号集合の鍵を取り出し、keyCode がその鍵を # (suc (arity t)) と論理式の極限段階コードとの順序対として計算する。骨格の等式 qs は第二成分をスロット s の集合で置き換える。残るのは、第一成分を封印された長さの数項によって表すことである。

    qkey : (keyAt t) .fst
         ≡ pr ((numAt (suc (arity t))) .fst) ((lookup s γ) .fst)
    qkey = keyAt-fst t ∙ keyCode (formula t)
         ∙ cong (pr (# (suc (arity t)))) (sym qs)
         ∙ cong (λ u → pr u ((lookup s γ) .fst))

最後の合同性では numAt-fst を逆向きに使い、順序対の中の集合論的な数項を numAt (suc (arity t)) の基礎集合で置き換える。完成した qkey は DenoteOf が要求する形そのものである。選んだ鍵は、選んだ定義域の数項と骨格のスロットとの対である。逆向きの証明では、中身に含まれる鍵の等式から同じ計算を組み立て直す。

             (sym (numAt-fst (suc (arity t))))

順方向では、実際の要素 m : ⟪ A ⟫、それと同じ基礎集合を表す外側の要素 z、そしてその集合が denote t に属するという証明から始める。DenoteOf の四つの証人を意味の順に与える。すなわち、パラメータの前に m を加えた環境、その長さの数項、論理式の鍵、その鍵での表の値である。これらを結ぶ条件は六つある。最初の五つは形と対応を記述し、最後の一つが、仮定した表示への所属を、環境が表の値に属するという所属へ変換する。

  denote-fill : (z : S) (m : ⟪ A ⟫) → ⟪ A ⟫↪ m ≡ z .fst
              → ⟨ ⟪ A ⟫↪ m ∈ denote t ⟩ → DenoteOf B C s e γ z
  denote-fill z m qm hz =
    envAt t m , (numAt (suc (arity t)) , (keyAt t , (valAt t
    , ( hcons , (hdom , (hkey , (qkey , (hgraph , hmem))))))))

第一の条件は、選んだ環境が候補の要素をパラメータ環境へ加えて得られることを述べる。consAtL の内向きの読みには、元のパラメータグラフを与える qd'、スロット z の候補集合を同一視する sym qm、新しく作った環境グラフを与える envAt-fst t m を渡す。すると対象言語の拡張論理式が証明される。これにより、論理式の余分な変数スロットには候補の要素が入り、その後に元のパラメータが続くことが保証される。

    where
    hcons : ⟨ (envAt t m ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩
    hcons = consAtL-in Aʟ δp (NM.DA.ι m) (envAt t m ∷ z ∷ γ)
              zero (suc zero) (sh2 e) qd' (sym qm) (envAt-fst t m)

第二の条件は、拡張環境の定義域を定める。その長さは suc (arity t) である。候補の要素のための一つの位置に、arity t 個のパラメータ位置が続く。domAt の内向きの妥当性補題には、environment t m の基礎となる値と、それぞれの値が構成可能であることの証明を渡す。後者は、それらの値が構成可能な台に属することと、L の推移性から従う。

    hdom : ⟨ (numAt (suc (arity t)) ∷ envAt t m ∷ z ∷ γ)
             ⊨ domAt (suc zero) zero ⟩
    hdom = domAt-fill (suc zero) zero
             (numAt (suc (arity t)) ∷ envAt t m ∷ z ∷ γ)
             (suc (arity t)) (values Aʟ (environment t m)) (valuesL t m)

同じ定義域の補題は、選んだ証人を、それが比較すべき基礎集合としても見る必要がある。等式 envAt-fst t m は envAt t m の下にある環境グラフを取り出し、numAt-fst (suc (arity t)) は長さの証人の下にある期待された von Neumann 数項を取り出す。この二つの射影等式により、定義域の論理式は、その数項が選んだ環境の長さを符号化することを正確に述べる。

             (envAt-fst t m) (numAt-fst (suc (arity t)))

第三の条件は、選んだ鍵を真正な符号領域に置く。構成 keyAt はすでに、その鍵が AllCodes Aʟ に属することを与える。スロット等式 qC に沿ってこの所属を輸送すれば、スロット C に格納された集合への所属が得られる。この仮定は省けない。充足関係グラフが論理式の意味論的な値を与えることを強制されるのは真正な符号の鍵においてであり、符号領域の外での振る舞いはそのような値を定める必要がないからである。

    hkey : ⟨ (keyAt t) .fst ∈ (lookup C γ) .fst ⟩
    hkey = subst (λ u → ⟨ (keyAt t) .fst ∈ u ⟩) (sym qC) (keyAt-∈ t)

第五の条件は、選んだ値が、選んだ鍵で充足関係グラフに許される値であることを述べる。グラフの論理式を評価するとき、外側の割り当ての前には、値、鍵、長さの数項、拡張環境、候補の要素という五項が順に置かれている。第一の対応条件は、keyAt t の基礎集合を、スロットの台における ψAt t の鍵と同一視する。先に示した keyψ は、まさにここで鍵の計算を qB に沿って台の境界の向こうへ運ぶ。

    hgraph : ⟨ (valAt t ∷ keyAt t ∷ numAt (suc (arity t)) ∷ envAt t m
                ∷ z ∷ γ) ⊨ satGraphAt (sh5 B) (suc zero) zero ⟩
    hgraph = graphAt-value (sh5 B) (suc zero) zero
               (valAt t ∷ keyAt t ∷ numAt (suc (arity t)) ∷ envAt t m
                ∷ z ∷ γ) (ψAt t)

第二の対応条件は、選んだ値を同一視する。まず valAt-val が、それを keyAt t における表の値として取り出す。法則 val-at は、その表の値を Aʟ 上の埋め込まれた論理式の Sat 集合と同一視する。最後に satψ を必要な向きに読んで、この集合をスロットの台へ輸送する。二つの対応等式が揃うと、graphAt-value は論理式の鍵とその意味論的な値を変えることなく、グラフの条件を証明できる。

               (keyAt-fst t ∙ sym (keyψ t))
               ( cong (λ p → p .fst) (valAt-val t)
               ∙ cong (λ p → p .fst) (val-at Aʟ Aʟ (embed (formula t))
                             (keyAt t) (keyAt-∈ t) (keyAt-fst t))
               ∙ sym (satψ t) )

第六の条件は決定的な所属である。符号化された拡張環境は、選んだグラフの値に属さなければならない。仮定は、m が表す要素が denote t に属することを述べる。特徴づけ NM.denote-mem t m は、これを environment t m が embed (formula t) を内側で充足することへ変える。したがって表示への所属は、統一充足関係表が記録すべき意味論的な事実をちょうど与える。

    hmem : ⟨ (envAt t m) .fst ∈ (valAt t) .fst ⟩
    hmem = subst (λ u → ⟨ envAt t m ∈ˢ u ⟩) (sym (valAt-val t)) inTable
      where
      inner : ⟨ environment t m NM.DA.⊨ᵐ embed (formula t) ⟩
      inner = subst ⟨_⟩ (NM.denote-mem t m) hz

法則 val-sat は、この内側の充足関係を、envAt t m が keyAt t における表の値に属することと同一視する。ここでは充足関係から始めるため、この法則を逆向きに読む。次に valAt-val に沿って輸送し、明示的な表の値を封印された証人 valAt t で置き換える。これで第六の条件が証明され、denote-fill が完成する。四つの証人とそれらを結ぶ六つの関係は、すべて名前 t のデータと、その指示対象への仮定された所属から得られた。

      inTable : ⟨ envAt t m ∈ˢ Table.val Aʟ Aʟ (keyAt t) (keyAt-∈ t) ⟩
      inTable = subst ⟨_⟩
        (sym (val-sat Aʟ (embed (formula t)) (keyAt t) (keyAt-∈ t)
                (keyAt-fst t) (environment t m) (envAt t m)
                (envAt-fst t m))) inner

逆向きでは、z に対する明示的な DenoteOf の中身、すなわち四つの束縛された要素と先の六条件が与えられているとする。目標は、z が表す要素 m が denote t に属することである。NM.denote-mem を逆向きに読めば、埋め込まれた論理式が environment t m で内側の充足関係を満たすことを復元すれば十分である。残る等式は、中身が任意に与えた環境、数項、鍵、値を順に識別する。

  denote-read : (z : S) (m : ⟪ A ⟫) → ⟪ A ⟫↪ m ≡ z .fst
              → DenoteOf B C s e γ z → ⟨ ⟪ A ⟫↪ m ∈ denote t ⟩
  denote-read z m qm (c , (k , (key , (v , (hc , (hk , (hi , (hp , (hg , hm)))))))))
    = subst ⟨_⟩ (sym (NM.denote-mem t m)) inner
    where

まず拡張の条件を読む。その外向きの妥当性定理は、元のグラフ qd'、候補の要素を同一視する sym qm、充足証明 hc を比較する。その結果、任意に与えられた証人 c の基礎集合は、ちょうど envGraph Aʟ (environment t m) だと分かる。したがって、最初の存在証人はパラメータグラフの単なる何らかの拡張ではなく、m を名前 t のパラメータの前に置いて得る正準な環境のグラフである。

    qcg : c .fst ≡ envGraph Aʟ (environment t m)
    qcg = consAtL-out Aʟ δp (NM.DA.ι m) (c ∷ z ∷ γ)
            zero (suc zero) (sh2 e) qd' (sym qm) hc

次に定義域の条件が数項の証人を決定する。qcg が c を environment t m のグラフと同一視しているので、domAt-numeral は hk を、k の基礎集合とその環境の長さを表す数項との等式として読める。この長さは suc (arity t) であり、valuesL が定義域の妥当性定理に必要な構成可能性を与える。したがって k .fst ≡ # (suc (arity t)) が得られる。

    qk : k .fst ≡ # (suc (arity t))
    qk = domAt-numeral (suc zero) zero (k ∷ c ∷ z ∷ γ) (suc (arity t))
           (values Aʟ (environment t m)) (valuesL t m) qcg hk

中身の第四の条件 hp は、その鍵が自身の定義域の証人 k と骨格のスロットとの対であることを述べる。第一成分を qk で、第二成分を qs で書き換えると、# (suc (arity t)) と論理式コードとの対が得られる。最後に keyCode (formula t) を逆向きに読み、この対を embed (formula t) の符号集合の鍵として認識する。こうして得た等式 qkey' は、中身が任意に与えた鍵を真正な論理式の鍵と同一視する。

    qkey' : key .fst ≡ (keyS Aʟ (embed (formula t))) .fst
    qkey' = hp ∙ cong (λ u → pr u ((lookup s γ) .fst)) qk
          ∙ cong (pr (# (suc (arity t)))) qs ∙ sym (keyCode (formula t))

所属条件 hi は、復元された鍵がスロット C に格納された集合に属することを述べる。qC に沿って輸送すると、AllCodes Aʟ への所属 key∈ が得られる。これは所属の証明であって、新しい鍵の選択ではない。鍵そのものはすでに DenoteOf の中身から与えられ、qkey' によって同一視されている。この証明の役割は、その鍵を、統一表と充足関係グラフの意味論的な仕様が成り立つ領域に置くことである。

    key∈ : ⟨ key ∈ˢ AllCodes Aʟ ⟩
    key∈ = subst (λ u → ⟨ key .fst ∈ u ⟩) qC hi

最後に、任意に与えられた値の証人 v を同一視する。qkey' と keyψ によって、その鍵をスロットの台における ψAt t の鍵と揃えると、グラフの証明 hg に一意性の読み graphAt-only を適用できる。これにより、まず v .fst が対応する Sat 集合と同一視される。輸送 satψ がその集合を Aʟ へ戻し、val-at を逆向きに読むことで Table.val Aʟ Aʟ key key∈ と同一視する。こうして qval が必要な表の値を復元し、次の段階で最後の所属 hm を内側の充足関係へ変換できるようになる。

    qval : v .fst ≡ (Table.val Aʟ Aʟ key key∈) .fst
    qval = graphAt-only (sh5 B) (suc zero) zero
             (v ∷ key ∷ k ∷ c ∷ z ∷ γ) (ψAt t) (qkey' ∙ sym (keyψ t)) hg
         ∙ satψ t
         ∙ sym (cong (λ p → p .fst) (val-at Aʟ Aʟ (embed (formula t)) key key∈ qkey'))

DenoteOf の最後の成分は、拡張された環境 c が復元された値 v に属することを述べる。パス qval は、この値を復元された論理式符号のキーにおける一様充足表の値と同定する。このパスに沿って所属を移送すると、次の意味論的な読みに必要な表への所属が得られる。

    inTable : ⟨ c ∈ˢ Table.val Aʟ Aʟ key key∈ ⟩
    inTable = subst (λ u → ⟨ c .fst ∈ u ⟩) qval hm

妥当性の等式 val-sat は、この表の値への所属を埋め込まれた論理式の充足として読む。その仮定では、qkey' が復元されたキーを同定し、qcg が c を拡張された環境のグラフと同定する。したがって inner は、environment t m が名前 t の論理式を満たすことを述べる。外側の結果では、さらに denote-mem を逆向きに用いて denote t への所属を得る。

    inner : ⟨ environment t m NM.DA.⊨ᵐ embed (formula t) ⟩
    inner = subst ⟨_⟩
      (val-sat Aʟ (embed (formula t)) key key∈ qkey'
         (environment t m) c qcg) inTable

ここまでの読みは、台の元 m に対して述べられていた。補題 member-fill は順方向の読みを任意の構成可能な要素 z に言い換える。その台集合が denote t に属するなら、台のスロットへの所属と、証人の組 DenoteOf の両方が得られる。第一の結論は、集合 A への実際の所属から得た後、スロットの等式 qB に沿って移送される。

  member-fill : (z : S) → ⟨ z .fst ∈ denote t ⟩
              → ⟨ z .fst ∈ (lookup B γ) .fst ⟩ × DenoteOf B C s e γ z
  member-fill z hz = subst (λ u → ⟨ z .fst ∈ u ⟩) (sym (cong (λ p → p .fst) qB)) hA
    , denote-fill z (fib .fst) (fib .snd)
        (subst (λ u → ⟨ u ∈ denote t ⟩) (sym (fib .snd)) hz)

元に対する補題を適用するには、z が表す台の元をまず復元する必要がある。包含補題 denoteMem は、表示への所属を A への所属に変える。次に、所属のファイバー表示から m : ⟪ A ⟫ と等式 ⟪ A ⟫↪ m ≡ z .fst が得られる。これは通常の依存データなので、選択原理も命題的切り詰めの除去も使わない。

    where
    hA : ⟨ z .fst ∈ A ⟩
    hA = denoteMem t (z .fst) hz
    fib : Σ[ mm ∶ ⟪ A ⟫ ] (⟪ A ⟫↪ mm ≡ z .fst)
    fib = ∈-asFiber {a = z .fst} {b = A} hA

逆向きの言い換えは、z の台のスロットへの所属と DenoteOf の証人の組から始まる。z が表す台の元を復元した後、先の補題 denote-read はその証人の組を、埋め込まれた元の denote t への所属として読む。最後にファイバーの等式に沿って移送し、z .fst の所属へ戻す。

  member-read : (z : S) → ⟨ z .fst ∈ (lookup B γ) .fst ⟩
              → DenoteOf B C s e γ z → ⟨ z .fst ∈ denote t ⟩
  member-read z hz hDen = subst (λ u → ⟨ u ∈ denote t ⟩) (fib .snd)
    (denote-read z (fib .fst) (fib .snd) hDen)
    where

ここで必要なファイバーは、台のスロットへの所属という仮定から得られる。等式 qB はそのスロットの台集合を A と同定するので、移送によってまず z .fst ∈ A が得られる。続いて ∈-asFiber が ⟪ A ⟫ の対応する元と、その埋め込みの等式を返す。したがって二つの補題は、小さな台の型の元としてあらかじめ与えられた場合だけでなく、必要な所属を満たすモデルの任意の要素に適用できる。

    fib : Σ[ mm ∶ ⟪ A ⟫ ] (⟪ A ⟫↪ mm ≡ z .fst)
    fib = ∈-asFiber {a = z .fst} {b = A}
      (subst (λ u → ⟨ z .fst ∈ u ⟩) (cong (λ p → p .fst) qB) hz)

名前を組み立てる

固定した名前 t に対して、Data t は四つの等式を記録する。骨格のスロットはその論理式の符号、アリティのスロットはその数項、環境のスロットはそのパラメータのグラフ、表示のスロットは denote t である。NameAt-fill はこれらの等式を用いて、NameAt の四つの概念的な連言、すなわち定数を含まないこと、アリティが ω に属すること、環境条件、表示の外延的な特徴付けを証明する。最後の連言は、所属の二方向 into と back によって与えられる。

NameAt-fill : (t : Name) → Data t → ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩
NameAt-fill t (qs , (qa , (qe , qd))) =
  NameAt-in B C C₀ s a e d γ hf ha he into back
  where
  module Bt = Body t qs qa qe

最初の連言は、名前 t がもつ具体的な無パラメータ論理式から得られる。この論理式には suc (arity t) 個の変数位置があり、qs はその極限段階での符号を骨格のスロットと同定する。さらに qa がアリティのスロットを、q₀ が空のアルファベットの符号集合を同定するので、codeFree-in はこの論理式と符号の等式をそのまま FreeAt の充足へ変換する。

  hf : ⟨ γ ⊨ FreeAt C₀ s a ⟩
  hf = codeFree-in C₀ s a γ (arity t) q₀ qa (formula t) qs

アリティの連言が要求するのは ω への所属だけである。標準的な事実 #∈ω (arity t) がその数項の ω への所属を与え、等式 qa がそれをアリティのスロットに格納された値へ移送する。この部分の記述では比較関係を使わない。

  ha : ⟨ (lookup a γ) .fst ∈ ω ⟩
  ha = subst (λ u → ⟨ u ∈ ω ⟩) (sym qa) (#∈ω (arity t))

環境の連言では、名前 t のパラメータベクトルを族 i ↦ lookup i (params t) とみなす。そのグラフの等式は qe、定義域の数項についての等式は qa であり、qB は終域の台を Aʟ と同定する。paramSeq-in はこの族の標準的な環境の性質を三つのスロットへ移送し、envOverAt の充足を与える。

  he : ⟨ γ ⊨ envOverAt e a B ⟩
  he = paramSeq-in e a B γ (arity t) (λ i → lookup i (params t)) qe qa
         (cong (λ p → p .fst) qB)

表示を外延的に特徴付ける連言の順方向は、表示のスロットの元から始まる。qd に沿って移送すると、その元は denote t の元になる。そこで Bt.member-fill が、表示の本体をなす二つの部分、すなわち台のスロットへの所属と証人の組 DenoteOf をちょうど与える。

  into : (z : S) → ⟨ z .fst ∈ (lookup d γ) .fst ⟩
       → ⟨ z .fst ∈ (lookup B γ) .fst ⟩ × DenoteOf B C s e γ z
  into z hz = Bt.member-fill z (subst (λ u → ⟨ z .fst ∈ u ⟩) qd hz)

逆に、Bt.member-read は台への所属と DenoteOf を合わせて、denote t への所属として読む。さらに qd の逆向きに沿って移送すると、その要素は表示のスロットへ戻る。この二つの関数が、NameAt にある一つの外延的な連言に必要な二方向である。

  back : (z : S) → ⟨ z .fst ∈ (lookup B γ) .fst ⟩ → DenoteOf B C s e γ z
       → ⟨ z .fst ∈ (lookup d γ) .fst ⟩
  back z hzB hDen = subst (λ u → ⟨ z .fst ∈ u ⟩) (sym qd)
    (Bt.member-read z hzB hDen)

NameAt の逆方向の読みが返すのは、名前とその四つのデータの等式の命題的切り詰めだけである。アリティの連言 ha は ω への所属であり、その意味論的な表示は、命題的切り詰めのもとで自然数 k と、アリティのスロットを # k と同定する等式を与える。最終結果も命題的に切り詰められた型なので、rec₁ はその結果を構成する範囲でこの証人を使える。

NameAt-read : ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩ → ∥ Σ[ t ∶ Name ] Data t ∥₁
NameAt-read (hf , (ha , (he , hd))) =
  rec₁ squash₁ atArity ha
  where
  atCode : (k : ℕ) (qa : (lookup a γ) .fst ≡ # k)

k とアリティの等式 qa を固定すると、codeFree-out が定数を含まないという連言を読む。そこからは、なお命題的切り詰めのもとで、論理式 χ : Formula ⊥* (suc k) と、骨格のスロットからその極限段階での符号への等式 qs が得られる。この分岐の中で atCode が名前とそのデータを組み立て、qs が第一の等式、qa が第二の等式になる。

         → Σ[ χ ∶ Formula (⊥* {ℓ}) (suc k) ]
             ((lookup s γ) .fst ≡ (limitCode χ) .fst)
         → Σ[ t ∶ Name ] Data t
  atCode k qa (χ , qs) = t , (qs , (qa , (qe , qd)))
    where

アリティが定まると、パラメータ成分は直接復元できる。paramSeq-out は qa と台の等式 qB を用いて he を読み、⟪ A ⟫ に値を取る長さ k のベクトルを得る。このベクトルを k と χ に組み合わせて名前 t を定義する。ベクトル自体の復元には命題的切り詰めがないが、構成全体はアリティと論理式の読みによる切り詰めの内側にある。

    t : Name
    t = k , (χ , paramSeq-out e a B γ k qa (cong (λ p → p .fst) qB) he)

復元されたベクトルは、Data t に記録される環境の等式も満たさなければならない。対応する補題 paramSeq-graph は、もとの環境のスロットがこのベクトルの符号化されたグラフ env (pfam t) に等しいことを述べる。このパスが第三のデータの等式 qe である。

    qe : (lookup e γ) .fst ≡ env (pfam t)
    qe = paramSeq-graph e a B γ k qa (cong (λ p → p .fst) qB) he

局所モジュール Bt は、復元された名前と、その最初の三つのデータの等式 qs、qa、qe において、表示の本体の読みを具体化する。したがって Data t に残る成分は、表示のスロットと denote t の間の集合の等式である。これは両者の元を二方向に比較して証明する。

    module Bt = Body t qs qa qe

まず順方向の包含を示す。y が表示のスロットに属するとする。そのスロットはモデルの要素なので、L の推移性から y は構成可能であり、z : S としてまとめられる。外延的な連言 hd を外向きに読むと、台への所属と、命題的に切り詰められた DenoteOf の証人が得られる。目標 y ∈ denote t は命題なので、rec₁ によってその証人の各代表へ Bt.member-read を適用できる。

    fwd : (y : V ℓ) → ⟨ y ∈ (lookup d γ) .fst ⟩ → ⟨ y ∈ denote t ⟩
    fwd y hy = rec₁ ((y ∈ denote t) .snd)
      (Bt.member-read z (body .fst)) (body .snd)
      where
      z : S

body は二段階の意味論的な読みから得られる。まず extAt-out が表示のスロットへの所属を DenoteBody の充足に変え、次に DenoteBody-out がその台についての連言と、DenoteOf にまとめられた四つの存在証人を取り出す。存在量化の意味論に従って、これらの証人は命題的に切り詰められたままであり、上の命題値をもつ所属の証明の中だけで使われる。

      z = y , isL-trans hy ((lookup d γ) .snd)
      body : ⟨ z .fst ∈ (lookup B γ) .fst ⟩ × ∥ DenoteOf B C s e γ z ∥₁
      body = DenoteBody-out B C s e γ z
               (extAt-out d (DenoteBody B C s e) γ hd z hy)

逆方向の包含では y ∈ denote t を仮定する。証明はまず y を要素 z : S とみなし、次に Bt.member-fill を用いて z における表示の本体を構成する。導入補題 DenoteBody-in と extAt-in が、本体の充足と表示のスロットへの所属を順に組み立て直す。

    bwd : (y : V ℓ) → ⟨ y ∈ denote t ⟩ → ⟨ y ∈ (lookup d γ) .fst ⟩
    bwd y hy = extAt-in d (DenoteBody B C s e) γ hd z
      (DenoteBody-in B C s e γ z (body .fst) (body .snd))
      where
      z : S

z の構成可能性は、すでに分かっている二つの包含関係から得られる。denoteMem は denote t の各要素を A に入れ、pA は A が構成可能であることを述べる。この z に対して、Bt.member-fill は台への所属と、切り詰められていない DenoteOf の証人の組を与える。したがって逆方向の包含では命題的切り詰めを除去する必要がない。

      z = y , isL-trans (denoteMem t y hy) pA
      body : ⟨ z .fst ∈ (lookup B γ) .fst ⟩ × DenoteOf B C s e γ z
      body = Bt.member-fill z hy

各集合 y に対して、関数 fwd y と bwd y は二つの所属命題の間の両方向の含意を与える。両辺は命題なので、⇔toPath はこの二つの含意を真理値の等式に変える。さらに V の外延性が、点ごとの所属の等式を (lookup d γ) .fst ≡ denote t、すなわち第四の等式 qd に変える。

    qd : (lookup d γ) .fst ≡ denote t
    qd = extensionalV (λ y → ⇔toPath (fwd y) (bwd y))

分岐 atArity は、大域的な証人を選ぶことなく二つの切り詰めを処理する。その入力はアリティを持ち上げられた自然数として表し、qk を逆向きにすると atCode が要求する等式になる。続いて codeFree-out が命題的切り詰めのもとで論理式と符号の等式を与え、map₁ がその切り詰めの内側で atCode を適用する。結果は、四つのデータの等式をすべて満たす名前が存在するという命題的に切り詰められた主張であり、ちょうど NameAt-read の終域である。

  atArity : Σ[ lk ∶ Lift {ℓ-zero} {ℓ} ℕ ] (# (lower lk) ≡ (lookup a γ) .fst)
          → ∥ Σ[ t ∶ Name ] Data t ∥₁
  atArity (lk , qk) = map₁ (atCode (lower lk) (sym qk))
    (codeFree-out C₀ s a γ (lower lk) q₀ (sym qk) hf)