---
title: "集合で符号化した有限環境"
module: L.Coding.Environment
lang: ja
site: "Bedrock"
description: "集合で符号化した有限環境"
stage: "内部の符号化：式と定義域"
reading_order: 41
canonical: https://bedrock.institute/ja/L.Coding.Environment.html
html: L.Coding.Environment.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Environment.lagda.md
prerequisites: [Base.Prelude, FOL.Syntax, FOL.LevyHierarchy, FOL.Semantics, V.Hierarchy, V.Model, V.Coding, L.Coding.PairFormulas]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.Environment.md, https://bedrock.institute/zh/L.Coding.Environment.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 集合で符号化した有限環境

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

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

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

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

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

open import Base.Prelude

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

open import FOL.Syntax using ( var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; ∀̇∈; ∃̇∈; ⊥̇ )
```

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

```agda
open import FOL.LevyHierarchy using ( checkΔ₀; Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-∀∈ )
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
open import V.Model {ℓ} using ( self∈sucV; ∈sucV-inl; ∈sucV-elim )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′ )
```

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

```agda
open import L.Coding.PairFormulas {ℓ}
  using ( prAt; prAt-adequate; prChar-fwd; prChar-bwd
        ; ∈pair-introL; ∈pair-introR )

open import Cubical.Data.Unit using ( tt )
import Cubical.Data.Sum as Sum
```

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

```agda
open Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as E hiding ( elim )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.Functions.Logic using ( ⇔toPath )
```

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

```agda
open import Cubical.Data.FinData using ( toℕ; inj-toℕ )
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 後者です。したがって「添字を一つ進めること」と「鍵の後者を取ること」は同じ操作であり、これこそ環境の拡張が有界論理式で記述できる理由です。意味論の側では、真理値は命題性の証明を伴う命題なので、論理式の充足それ自体が命題であり、一つのパスによって外側の集合論的な主張と同一視できます。

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

module Sem = FOL.Semantics 𝒮ᵥ
```

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

```agda
open Sem using ( _^_ )
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)` に変えるのは、論理式言語が鍵について語えなければならず、論理式が語る対象は集合、ここでは数項だからです。

```agda
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-集合であることから来ます。命題の間の同値は真理値の間のパスに変換できるので、補題は各方向一つずつの二つの含意から組み立てられます。

```agda
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` です。目標が命題であるため、切り捨てをそこへ消去することは正当であり、項目が通常のデータとして取り出されることはありません。

```agda
       → 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` の項目を直接示します。切り捨てられた証拠は持ち上げられた索引であり、パスは対の構成子を逆向きの仮定に適用して埋められます。正準な証拠は選ばれず、証拠の一意性も主張されません。

```agda
    ps = pr-inj e
  fwd : ⟨ pr (# (toℕ i)) v ∈ env g ⟩ → v ≡ g i
  fwd = PT.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` によって別途記録されます。連言、有界な全称量化、そして葉にあたる所属と等式は、いずれも Δ₀ を保ちます。

```agda
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` が集合として等しいとき、ちょうどそのときだというものです。

```agda
Δ₀-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` であり、所属同士の双条件ではなく集合の本当の等式です。

```agda
    → ((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` に属します。

```agda
    sub₁ z z∈ₛJ = PT.rec ((z ∈ₛ sucV I) .snd)
      (Sum.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` へと書き換えます。

```agda
      (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) .snd)
        (∈∈ₛ {a = z} {b = sucV I} .snd z∈ₛs)
```

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

```agda
        (λ 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` を要素ごとに輸送します。

```agda
    × ((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 後者と等しいことです。

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

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

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

```agda
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` の項目、その添字、その値を捉えます。

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

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

```agda
        (∃̇∈ (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 後者であると言います。合わせて読めば、ずらされた項目は一歩の後者だけ高い鍵で同じ値を担っています。

```agda
            ∧̇ sucAt (suc (suc (suc zero))) zero ))))))

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

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

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

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

```agda
  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`、二つのパス等式を切り捨てられた対象へ入れられます。三つの充足仮定は既に証明した妥当性補題を通してそれらの等式を与え、得られたパスに沿う輸送が端点を対象に合わせます。外側の対象が命題であることは周囲の切り捨て消去に必要ですが、パスに沿う輸送そのものにはその仮定は要りません。

```agda
        ⊨ 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` に変わります。

```agda
    , 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 後者です。

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

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

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

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

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

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

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

```agda
        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` であり、それぞれ一つの成分規則が与えます。

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

```agda
        , ∣ ⁅ 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` を輸送すれば第一の節が満たされます。

```agda
            , ∈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` で満たされ、新しい鍵が古い鍵の後者であり値が保たれていることを記録します。

```agda
                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` によって与えられ、その妥当性補題を通して充足の節へと輸送されます。これで本体の三つの主張がすべて成立します。二つの項目が値を共有する本物の対であり、第二の鍵が第一の鍵の後者である、ということが。これこそ一項目分の番号付け替えの数学的内容です。

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

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

```agda
          ∣₁
        ∣₁
      ∣₁
    ∣₁
```

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

```agda
  bwd : Tgt → ⟨ γ ⊨ shiftPairAt p' p ⟩
  bwd = PT.rec ((γ ⊨ shiftPairAt p' p) .snd)
    (λ { (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` の値は要素を持ち、その要素がすべて空集合であり、これは外延的にちょうど `{∅}` です。

```agda
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` の値は空単集合の節を満たす要素を命題的に持ち、空対の節を満たす要素を命題的に持ち、そのすべての要素は命題的にいずれかを満たします。

```agda
           ∧̇ ((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'` が成り立つ集合はすべて `∅` と等しい、というものです。

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

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

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

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

```agda
  empty'→∅ z hz = extensionalV (λ y → ⇔toPath
    (λ h → E.rec (lower (hz y h)))
    (λ h → E.rec (∅-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` と等しいか、に置き換えます。切り詰めの位置は、論理式の有界存在量化子と切り詰められた選言が置いた場所とまさに一致します。特に、選ばれた対の分解が取り出されることは決してありません。

```agda
  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` であると主張します。分類は切り詰められたままであり、階層の非順序対の所属と一致します。そこからどちらの側かを選び取ることはできません。これらはまさに、対読み取りの章の対の特徴づけが受け取る形であり、第一成分を `∅` に具体化したものです。したがって残る仕事のすべては、同じ所属の事実の二つの表現の間を行き来することです。

```agda
               × (⟨ 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 ≡ ∅` に書き換えます。

```agda
  empty-member : (w : V ℓ) → ∥ Σ[ z ∈ V ℓ ] (⟨ z ∈ w ⟩ × Empty' z) ∥₁ → ⟨ ∅ ∈ w ⟩
  empty-member w = PT.rec ((∅ ∈ w) .snd)
    (λ { (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'` を `∅` との等しさに置き換えた対応する切り捨てられた主張へ写すのです。結果はまさに `∅` を基準とする分類であり、切り詰めは選ばれた側に解決されることなく全体を通じて保たれます。

```agda
  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 → PT.map (Sum.map (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` の所属をそのまま引き継ぎ、分類の節を各点で書き換えます。

```agda
      (∣ ∅ , (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` のいずれかを割り当てる切り詰められた二分法です。

```agda
    , (hW , λ z z∈w → PT.map (Sum.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` を返します。これがまさにこの節全体の形です。空性に基づく述語と `∅` に基づく述語は、同じ集合についての同じ三節の構造を包んだ二つの形であり、四つの変換補題が必要な各点の含意を両方向に供給します。

```agda
    × ((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 対と同一視します。切り詰められた証人が通常のデータとして取り出されることは決してなく、それらは変換の内部でのみ使われ、その出力は特徴づけが受け入れる命題の形をした節です。

```agda
      PT.map (λ { (w , hw , h) → w , hw , f w h }) h₁
    , PT.map (λ { (w , hw , h) → w , hw , g w h }) h₂
    , (λ y hy → PT.map (Sum.map (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 ⟧ γ)` と等しい」という主張と互いに交換可能になり、これが次の節の拡張の条件が使う読みになります。

```agda
  → ∥ Σ[ 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 (fst h) (fst (snd h)) (snd (snd h))
  where
```

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

```agda
  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 項目が空のタグと新しい値の対であることを言っています。

```agda
  × ((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) (γ : (V ℓ) ^ n)
                → (γ ⊨ tag0At s x) ≡ ((⟦ var s ⟧ γ ≡ pr ∅ (⟦ var x ⟧ γ)) , setIsSet _ _)
tag0At-adequate s x γ = ⇔toPath
```

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

```agda
  (λ { (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` の値が拡張されるグラフです。

```agda
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` が一度だけこれを記録します。

```agda
  (∃̇∈ (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` を追加で受け取ります。これが証明書の保持する符号化された形です。候補の環境は集合としてスロットに現れ、仮定がその集合を、それが符号化する割当てのグラフと同一視します。

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

consAt-adequate : ∀ {n} (e' m e : Fin n) (γ : (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` が主張を二つの包含へ帰着させます。

```agda
  ≡ ((⟦ 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₂` がずらした対の構成子の下で再結合します。

```agda
  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) (fst p) (snd p)
```

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

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

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

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

```agda
                 ⊎ ⟨ (y ∷ γ) ⊨ ∃̇∈ (var (suc e)) (shiftPairAt (suc zero) zero) ⟩ ∥₁)
           → (y : V ℓ) → ⟨ y ∈ E' ⟩ → ⟨ y ∈ env G' ⟩
  classify h₃ y y∈E' = PT.rec ((y ∈ env G') .snd)
    (Sum.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` です。

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

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

```agda
            (λ { (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` に等しいことです。この合成が記録しているのはまさにこの場合の数学的内容、すなわち新しい鍵が古い鍵の後者であり値が保たれるということです。

```agda
          (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` がこの所属をパスに沿って輸送します。グラフの内部では、最初の節で証明した参照の補題が、証人の指す添字の鍵に格納された値を特定します。これで第一の包含は完成です。新しい集合のすべての要素が命題的に拡張後の割当てのグラフに落ちます。

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

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

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

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

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

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

```agda
        (λ { (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` のグラフに等しい」という仮定に沿って輸送すれば、符号化された環境への所属になります。

```agda
            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` に対して所属の比較の二方向を与えます。新しい集合の要素から拡張後の割当てのグラフへ、そしてグラフから新しい集合へ、という方向です。この方向に読めば、論理式の充足は符号化されたグラフの間の等式へと変換されます。補題の残りの方向は、そのような等式から充足を構成します。

```agda
  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 =
```

逆方向は、新しい集合を拡張後の割当てのグラフと同一視するパスから出発し、三つの充足の節を直接構成します。第一の節は鍵 0 の項目を示します。`cons` の定義等式によりグラフの添字 0 での所属は成り立ち、仮定のパスがそれを新しい集合への所属へ移します。タグ付き項目の節はそのまま成り立ちます。空のタグと値 `M` を持つ項目は構成上対 `pr ∅ M` であり、0 の数項は空集合だからです。

```agda
      ∣ pr (# 0) M
      , subst (λ z → ⟨ pr (# 0) M ∈ z ⟩) (sym e'eq) ∣ lift zero , refl ∣₁
      , subst ⟨_⟩ (sym (tag0At-adequate zero (suc m) (pr (# 0) M ∷ γ))) refl ∣₁
    , (λ p p∈E → PT.rec
        (((p ∷ γ) ⊨ ∃̇∈ (var (suc e')) (shiftPairAt zero (suc zero))) .snd)
```

第二の節は、古い環境の各要素に対して、新しい集合の内側へそのずらされた対応物を生産しなければなりません。その要素の所属は仮定に沿って `g` のグラフへ輸送され、そこで参照の補題が添字と、項目をその要素と同一視する等式を読み取ります。ずらされた項目は、後続の数項を鍵とし値を保つ対です。新しい集合へのその所属も同様に、拡張後の割当てのグラフの後続の添字で成り立ち、仮定のパスを通して移されます。残るのはずらしの論理式そのものの充足の証明です。

```agda
        (λ { (li , peq) →
          ∣ pr (# (suc (toℕ (lower li)))) (g (lower li))
          , subst (λ z → ⟨ pr (# (suc (toℕ (lower li)))) (g (lower li)) ∈ z ⟩)
              (sym e'eq) ∣ lift (suc (lower li)) , refl ∣₁
          , subst ⟨_⟩
```

この証明は、ずらしの妥当性補題を逆向きに走らせることで得られます。補題による論理式の読みは、添字、値、そして二つの等式を要求します。一方は古い項目を、参照が見つけた添字の位置の対と同一視し、もう一方はずらされた対がずらされた項目そのものであると言います。これは計算によって成り立ちます。妥当性の主張は命題の間の等式なので、それに沿って `refl` を輸送すれば必要な充足が得られ、この要素に対して論理式の第二の節が完成します。

```agda
              (sym (shiftPairAt-adequate zero (suc zero)
                (pr (# (suc (toℕ (lower li)))) (g (lower li)) ∷ p ∷ γ)))
              ∣ # (toℕ (lower li)) , g (lower li) , sym peq , refl ∣₁ ∣₁ })
        (subst (λ z → ⟨ p ∈ z ⟩) hE p∈E))
    , (λ p' p'∈E' → PT.rec squash₁
```

第三の節は分類の節です。新しい環境のすべての要素が、タグ付きの二つの節のいずれかを命題的に満たさねばなりません。これを使うには、まず `E'` の要素 `p'` をパス `e'eq` に沿って符号化グラフ `env G'` への所属へ輸送します。これは切り捨てられたファイバーデータ、すなわちインデックス `j` と、その鍵の項目が `p'` に等しいという等式 `pr (# (toℕ j)) (G' j) ≡ p'` です。続いてインデックスで場合分けします。cons 後のグラフの項目は、`cons` を定義する二つの等式に対応して、ちょうど二種類あるからです。目標は二つの命題からなる切り捨てられた選言なので、各場合は対応する選言肢の下で自らの節を返すことができ、切り捨てが場合分けを包み込みます。

```agda
        (λ { (lj , eq) → byKey' p' (lower lj) eq })
        (subst (λ z → ⟨ p' ∈ z ⟩) e'eq p'∈E'))
    where
    byKey' : (p' : V ℓ) (j : Fin (suc k))
           → pr (# (toℕ j)) (G' j) ≡ p'
```

インデックス 0 における `G'` の項目は新しい項目で、等式は `pr (# 0) M ≡ p'` です。パスの向きを整えれば、これは `p'` が値 `M` を伴う空のタグを持つという主張そのものです。タグ付き読み取りの妥当性補題はその充足命題を等式 `⟦ var zero ⟧ (p' ∷ γ) ≡ pr ∅ M` と同一視し、`# 0` は `∅` に計算されます。そこで逆向きの等式を妥当性のパスに沿って輸送すれば、左の選言肢が得られます。

```agda
           → ∥ ⟨ (p' ∷ γ) ⊨ tag0At zero (suc m) ⟩
             ⊎ ⟨ (p' ∷ γ) ⊨ ∃̇∈ (var (suc e)) (shiftPairAt (suc zero) zero) ⟩ ∥₁
    byKey' p' zero eq =
      ∣ inl (subst ⟨_⟩ (sym (tag0At-adequate zero (suc m) (p' ∷ γ))) (sym eq)) ∣₁
    byKey' p' (suc i₀) eq =
```

後続インデックスでは、`G'` の項目はずらされた旧項目であり、右の選言肢は shift 式による証明を与えねばなりません。shift 式が要求するファイバーは五つの成分を持ち、そのうち集合としてのインデックスと値のスロットは直接です。旧項目のスロットは `pr (# (toℕ i₀)) (g i₀)` が旧環境に属することを必要としますが、これは `lookup-spec` から従います。`env g` のインデックス `i₀` では、その鍵の項目が値 `g i₀` を持つ対であり、これを `hE` に沿って輸送すれば `E` への所属になります。ずらした項目のスロットは、数項を鍵とする項目 `pr (# (toℕ i₀)) (g i₀)` そのもので埋められ、`eq` により (向きを除けば)`p'` と等しくなります。

```agda
      ∣ inr ∣ pr (# (toℕ i₀)) (g i₀)
            , subst (λ z → ⟨ pr (# (toℕ i₀)) (g i₀) ∈ z ⟩) (sym hE)
                ∣ lift i₀ , refl ∣₁
            , subst ⟨_⟩
                (sym (shiftPairAt-adequate (suc zero) zero
```

残る二つのパスがファイバーを完成させます。旧項目のパスは定義的です。選ばれたインデックスと値は、ちょうど `i₀` の数項と `g i₀` だからです。ずらしのパスは逆向きの `eq` を取ります。ずらされた項目は後続の鍵を持つ対と等しくなければならず、仮定によりその対は `p'` だからです。`shiftPairAt (suc zero) zero` の妥当性補題を逆向きに走らせると、組み立てたファイバーはその充足に変換され、右の選言肢の下に置かれます。こうして場合分けの両分岐は、第三の節の切り捨てられた選言が求めるとおり、それぞれの節を命題的に与えるだけにとどまります。

```agda
                  (pr (# (toℕ i₀)) (g i₀) ∷ p' ∷ γ)))
                ∣ # (toℕ i₀) , g i₀ , refl , sym eq ∣₁ ∣₁ ∣₁
```

## まとめ

本章は、充足関係の各節が必要とする二つの環境操作、すなわち値の参照と、量化子の下での割当ての拡張を、集合についての主張に変えました。

符号化そのものは `env` であり、割当てを数項を鍵とする対のグラフとして格納します。`lookup-spec` はこのグラフが関数的であることを示します。ある対が鍵 `i` の位置でグラフに属するのは、その値が `g i` であるとき、そのときに限ります。操作の側では、`sucAt` が言語で表現できる三つの所属の節によって集合の von Neumann 後者を特徴づけ、`shiftPairAt` が番号付け替えされた一つの項目を認識します。`consAt` はこれらを変換全体へ組み立てます。旧スロットが `g` のグラフに等しいという仮定のもとで、論理式の充足は、新しいスロットと `cons M g` のグラフとの等式であり、その証明は二つの包含を集合の外延性で比較するもので、切り捨てられた証人は命題の中へのみ消除されます。