---
title: "作为集合编码图的有穷环境"
module: L.Coding.Environment
lang: zh
site: "Bedrock"
description: "作为集合编码图的有穷环境"
stage: "内部编码：表达式与定义域"
reading_order: 41
canonical: https://bedrock.institute/zh/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/ja/L.Coding.Environment.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 作为集合编码图的有穷环境

一阶语言的满足子句谈论变元的取值，却只能对集合作量化。因此，要使满足关系能在集合论内部被计算，变元赋值本身必须先成为一个集合。本章完成这一编码：一个有穷赋值，即从变元序号到 `V ℓ` 中集合的函数，由它的图表示，也就是「序号的数码与该处取值」之对的集合。

这一编码的设计目标是图中的查值精确。由于键的一侧由数码构成，而数码是单射的，坐在键 `i` 处的那个对的第二分量恰为 `i` 处的值，别无他物。这条函数性命题是本章的主引理。

第二个关注点是扩张。当满足关系下降到量词之下时，新值被放在索引零处，每个旧索引上移一位；在键的一侧，这恰是 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)))
```

这个图是**函数性的**：一个对属于 `env g` 在键 `i` 处，恰当其第二分量为值 `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'` 处的有序对。

扩张环境不只是在零键处插入一个新条目，它还给旧条目重新编号：原来键为 `# 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` 填入。该子句在扩张五次的环境中求值，槽位零至四依次放着 `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'` 处的配对读式从槽位零取索引，而槽位零现在放着 `sucV i`；从槽位二取值，槽位二放着 `v`。于是充分性引理所期待的等式恰为 `⟦ var p' ⟧ γ ≡ pr (sucV i) v`，即第二条假定。注意此处无需拆开移位后的条目本身：两条配对读式给出两个分解，而后继读式由于槽位零放着槽位三的后继而由 `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'
```

主体的最后一个合取支是上一节的后继读式，作用于两个索引见证。在拼装好的环境中，槽位三处的值是索引 `i`，槽位零处的值是它的 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` 的 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)))
```

在元层一侧，空性由私有谓词 `Empty' z` 表达：它是一个函数，取 `z` 的任意成员 `y`，返回空类型 `⊥*` 的一个元素。这个函数表达 `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 ⟩` 是合法的。在内部，显式给出的见证 `z` 带有隶属证明与 `Empty' 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` 打包了从集合 `Q` 读出 Kuratowski 对刻画所需的三条子句：`Q` 的某个携带 `P` 的成员的截断存在，对 `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-集合。这恰好说明：编码后的第零个条目就是空标签与新值组成的对。

```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)
```

## 扩张环境

向赋值前置一个值同时做两件事：新值落在索引零处，而每个旧序号上移一位。本节证明一条有界公式 `consAt` 恰好在编码图上表达这一变换，并且其充分性针对**编码后的**环境成立。

公式有三条子句：新集合的一个条目带有空标签与新值；旧图的每个条目都出现在新图中并已移位；新图的每个条目要么是那条新条目，要么是某个旧条目的移位。充分性陈述并不是说该公式仅以某种类似 cons 的方式把两个集合联系起来。在给定函数 `g` 与「旧槽位等于图 `env g`」这一假设后，它得出从新槽位到图 `env (cons M g)` 的路径。等式两侧都是层级中的集合，故证明是外延的：逐成员证明两个包含。一个方向用本章各读式对新集合的每个成员分类；另一方向按键逐个走遍 `cons M g` 的图。在索引处相符是定义性的，因为 `suc k` 的数码就是 `k` 的数码的后继。

宿主层运算 `cons m g` 是 `Fin (suc n)` 上的函数：索引零处返回 `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'` 处之值的每个条目仅仅是那条带标签的零条目，或 `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` 的环境中满足带标签零读式，或者满足一个有界存在式，其见证是 `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'`」正是命题。随后两个分支分别处理：第一分支接收带标签零读式的满足，产出图的零键。

```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`：槽位零处的值就是 `y` 本身，而新绑定之下的 `suc m` 仍指向原赋值槽位 `m` 的取值。反转这条路径得 `pr ∅ M ≡ y`，恰是 `env G'` 在键零处的条目，因为 `G' zero` 化归为 `M`，零的数码化归为空集。于是见证就是 `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` 的充分性引理把该子句转换为集合 `i` 与 `v` 的仅仅存在，使 `p ≡ pr i v` 且 `y ≡ pr (sucV i) v`。这里两个槽位的角色很关键：在 `shiftPairAt (suc zero) zero` 中，旧条目坐在靠后的槽位，被移位者坐在槽位零，故 `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` 的两条定义等式恰好产出两类条目：索引零处的新条目，以及各后继索引处的移位旧条目。

```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' ⟩)
```

零键情形中，条目等式按定义化归为「带空标签、值为 `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)
```

还差一个输入。移位子句是一条满足陈述，它所在环境的第二槽必须真的存放旧条目 `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 =
```

反向从把新集合与扩张后赋值的图等同起来的那条路径出发，直接构造三条满足子句。第一条给出键零处的条目：按 `cons` 的定义等式，图在索引零处的隶属成立，而假定的路径把它转移到新集合中的隶属。带标签条目的子句随后直接成立，因为带空标签、值为 `M` 的条目按构造就是对 `pr ∅ M`，而零的数码就是空集。

```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'
```

索引零处 `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'` 的条目是一个移位后的旧条目，右边的析取支必须用移位公式给出证书。移位公式要求的纤维有五个分量，其中「作为集合的索引」与值槽是直接的。旧条目槽需要 `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` 的图的相等，其证明由两个包含经集合外延性比较而成，截断的见证只被消除进命题。