---
title: "可构造模型上的公式符号化"
module: L.Coding.Model
lang: zh
site: "Bedrock"
description: "可构造模型上的公式符号化"
stage: "内部编码：表达式与定义域"
reading_order: 42
canonical: https://bedrock.institute/zh/L.Coding.Model.html
html: L.Coding.Model.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Model.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Absoluteness, FOL.Coding, V.Hierarchy, V.Coding, V.Model, L.Constructible, L.Absoluteness, L.Coding.PairFormulas, L.Axioms.Numerals]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.Model.md, https://bedrock.institute/ja/L.Coding.Model.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 可构造模型上的公式符号化

可构造模型 `L` 的元素不是裸集合：它是一个层级 `V ℓ` 中的集合，连同「该集合可构造」的证明。于是在 `L` 中求值一条一阶公式时，量词遍历的是这样的对，而人们真正想要的集合编码事实，比如某个 Kuratowski 对属于某个图，却是关于底层集合的事实。本章就在这两种读法之间架桥。

桥有两个方向。把模型元素向外投影时，可直接舍去其可构造性证书；转移有界读式时，则使用由 `L` 的传递性保证的绝对性。向内读需要在模型中给出见证：由一个对属于可构造图的证明，传递性为该对提供可构造性证书，使它成为 `L` 的元素。

在对读式之上，本章逐步建立「函数即图」的数学描述，值得注意这些条款在逻辑上各自独立。图取值只断言某个给定的有序对属于该图。单值性说一个自变量至多决定一个取值，却不涉及哪些自变量有取值。恰当定义域与取值限制各自再约束一个侧面。而且以上三条条件都不禁止候选图携带并非有序对的额外成员，因为它们只谈及对形状的成员；第四条，即每个成员都是「指标与取值」的对，把这些冗余排除在外。合在一起便是 `envOverAt`：一个相对于定义域 `d` 与值域 `B`、施于单个候选图的谓词；它刻画一个给定的集合何时是 `d` 之上取值于 `B` 的环境，并不构造全体环境的集合。

后半章转向编码。有序对与数码都能在 `L` 内部造出，且各自投影到其周遭对应物。由于每个码都是「标签配载荷」，每个内部码都投影为「常元被投影后的公式」的周遭码；正是这一相容性，使层级一侧的读式能够分析造在模型内部的码。末尾还有两个观察：整个环境描述对赋值的依赖只通过三个投影后的集合，故可原样迁移到呈现同样图、定义域与值域的任何其他赋值；而当已知一个码是对时，`L` 的传递性把它的两个分量收进一个可构造集合。

两个世界处在同一宇宙层级 `ℓ`。内层语言的赋值是由载体 `S` 的元素组成的向量，每个元素是一个周遭集合连同其可构造性证书；而外部事实则是关于用 `fst` 把每项投影后所得的底层集合来陈述的。本章每条充分性陈述的形状，都是把「在该配对赋值处的满足判断」与「关于投影后赋值的事实」等同起来；投影必须先一次性、正确地处理完毕，集合论的论证才能开始。

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

open import Base.Prelude

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

open import FOL.ZFStructure using ( module hPropStructure )
```

充分性陈述比较的是真值，故周遭事实被打包成命题。特别地，层级中两个集合的相等是命题，因为层级是 h-集合。路径与同余负责把这些包装后的等式同投影查值对齐；绝对性、配对与数码等实质集合论事实则由各自的引理提供。

```agda
open import FOL.Syntax
  using ( Term; Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇
        ; ∀̇_; ∀̇∈; ∃̇_; ∃̇∈ )
open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo )
import FOL.Absoluteness
```

`L` 的传递性以两种相关方式进入论证：它是转移有界读式所需 Δ₀ 绝对性的基础，也把可构造集合的成员组成模型内见证。直接投影本身不需要新见证，但向外读取公式所依赖的转移定理仍以传递性为依据。

```agda
import FOL.Coding
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; module VCode )
open import V.Model {ℓ} using ( pair-singleton )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
```

有界公式的向外方向由绝对性承担：一条关于层级、且常元命名可构造集合的 Δ₀ 公式，在 `L` 中读出时意义不变，两种读法经一条路径一致。对读式正是这种公式，故它在模型中的满足被等同于投影后集合间的等式。向内方向没有一般捷径，只能逐词条显式构造见证；本章所需的正是对这一例。

```agda
open import L.Absoluteness {ℓ} using ( liftFo; transferFo )
open import L.Coding.PairFormulas {ℓ}
  using ( prAt; Δ₀-prAt; prAt-adequate; ∈pair-introL; ∈pair-introR )
open import L.Axioms.Numerals {ℓ}
  using ( numeralL; numeralL-fst; pairʟ; pairʟ-fst )
```

本章中的一些存在性陈述是刻意弱的。说「图中存在一个条目」时，主张仅仅是某个条目存在，而非选定一个：这类陈述居于命题截断之中，只能消去到取命题值的对象。把被截断的存在与显式见证区分开，在每条充分性证明的两个方向上都重要，因为存在公式的满足总是取截断的形状。

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Vec using ( map )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Functions.Logic using ( ⇔toPath; ∃[∶]-syntax )
import Cubical.HITs.PropositionalTruncation as PT
```

真值是层 `ℓ-suc ℓ` 上的命题：公式不取值为布尔值，而取值为一个 `hProp`，即底层类型连同「它是命题」的证明的包装。由此内层结构的载体 `S` 也随之固定：它的元素恰是环境集合与可构造性证书组成的对。此后，`γ ⊨ φ` 一律指在可构造模型中的满足，而 `⟦ t ⟧ γ` 是 `S` 的元素，即一个集合连同其证书。

```agda
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; setIsSet; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ⁅_,_⁆ )

open hPropStructure 𝒮ʟ using ( S )
```

还有一个结构性事实规定了所有陈述的形状：本章每条读式都只经查表的 `fst` 陈述，别无其他。也就是说，模型中的满足总是与关于底层集合的事实相比较，从不与证书内部的任何东西比较。同一条原则也使最后的迁移引理成为可能：若两个赋值在一条描述所查看之处呈现同样的三个底层集合，这条描述就无法区分这两个赋值。

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

## 在投影后的环境中查表

本章的每条充分性陈述，都是把「模型元素赋值处的满足判断」与「关于**投影后**赋值的外部事实」相比较：后者把每一项的证书用 `fst` 剥去。这两个赋值并非同一个对象，因此在做任何比较之前，必须知道：在投影后的赋值中查某变元所得，等于在原赋值中查它再投影。这正是下面这条引理的全部内容；其后凡需把外部等式改用 `γ` 自身的条目来陈述之处，都会用到它。

证明对位置 `i` 作递归。在位置 `zero`，两边都化归到表头：`lookup zero (x ∷ γ)` 就是 `x`，cons 的 `map fst` 是诸投影的 cons，而 `x` 的两次取首分量按定义相等，故得 `refl`。在后继位置，两次查表各前进一项，递归调用完成论证。这里没有用到可构造性；该引理对任何由对构成的环境都成立。

```agda
lookup-fst : ∀ {n} (i : Fin n) (γ : S ^ n)
           → lookup i (map fst γ) ≡ fst (lookup i γ)
lookup-fst zero    (x ∷ γ) = refl
lookup-fst (suc i) (x ∷ γ) = lookup-fst i γ
```

## 有序对

本章要搭的桥有两个方向。正向，模型中的一个满足判断 (在元素为模型元素的赋值处求值) 必须转化为关于层级集合的事实；各赋值项先用 `fst` 投影，故环境陈述始终针对投影后的取值。词典的第一个词条识别有序对：周遭读式 `prAt q u v` 说 `q` 处的取值正是 `u`、`v` 两处取值的 Kuratowski 对。这条读式是有界 (Δ₀) 的，其意义具有绝对性，因而改在 `L` 的语言中读出毫无代价；它又不含任何常元，抬升便对常元不施加任何条件。定理精确地陈述结果：抬升后的读式在模型中的满足，是一条通往「`q` 处投影值等于 `u`、`v` 处投影值之 `pr`」的路径。反方向，即把一条赤裸的周遭隶属转回生活在模型内部的见证，要到下一节才首次出现，那时由 `L` 的传递性承担工作。

该陈述比较的是真值，故右边本身也必须是一个真值。层级中两个集合的相等是命题，因为层级是 h-集合；`PairIs` 把这样的路径类型连同「它是命题」的证明包装起来。抬升后的读式 `prAtL q u v` 就是 `prAt q u v` 本身，只是把每个常元改名进载体 `S`；这里没有可改名的常元，但有界性证书 `Δ₀-prAt` 仍随公式携带，因为转换引理要求一份这样的见证。

```agda
private
  PairIs : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
  PairIs a p = (a ≡ p) , setIsSet a p

prAtL : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
prAtL q u v = liftFo (prAt q u v) _
```

充分性陈述用一条路径把读式在模型中的满足与右边的包装等式等同起来。注意投影所处的位置：赋值 `γ` 由 `S` 的元素组成，而等式是关于所查各项的 `fst` 陈述的。这部词典的每个词条都取这个形状，因为具体的隶属事实生活在层级中，而不在模型的载体内。

```agda
prAtL-adequate : ∀ {n} (q u v : Fin n) (γ : S ^ n)
  → (γ ⊨ prAtL q u v)
  ≡ PairIs (fst (lookup q γ)) (pr (fst (lookup u γ)) (fst (lookup v γ)))
prAtL-adequate q u v γ =
    transferFo (prAt q u v) _ (Δ₀-prAt q u v) γ
```

证明串联三条路径，未引入任何新内容。转换引理先借有界性证书，把 `L` 中的满足等同于 `prAt q u v` 在投影后赋值处的周遭满足。随后读式自身的充分性定理把那个周遭满足改写为被解释值之间的等式。最后，投影后赋值中的两次查表被换成 `γ` 中查表后的投影，再由同余把等式在 `PairIs` 之下重新组装。所得正是所允诺的等同。

```agda
  ∙ prAt-adequate q u v (map fst γ)
  ∙ cong₂ PairIs (lookup-fst q γ)
      (cong₂ pr (lookup-fst u γ) (lookup-fst v γ))
```

## 取值

对象语言中的图是有序对的集合，而使用图时，要问的都是某个给定的对是否属于它。下面的读式把这件事表达为一个有界存在：在某词项所指集合的成员范围内存在一员，其主体为对读式。它的含义是那个 Kuratowski 对属于图的底层集合这一周遭隶属。

正向把满足转化为隶属。反方向才是模型真正发挥作用之处：要满足那个存在量词，必须给出一个**模型的元素**，其底集正是那个对，而假设只提供了一个集合。这个对可构造，因为它属于某个可构造集合，而可构造类是传递的。这一步就是全部论证；此后凡要求见证造在模型之内、而非仅在层级之内，都会重复这一步。

定义读作：在该词项 `F` 的值为界的范围内，仅仅存在图的一个成员，满足对读式。存在量词的约束项扩展了环境；对读式的三个位置指称这个新项以及两个论元平移后的引用，而界 `F` 指定这个新条目所遍历的图。

```agda
private
  appTerm : ∀ {n} → Term S n → Fin n → Fin n → Formula S n
  appTerm F x y = ∃̇∈ F (prAtL zero (suc x) (suc y))

  appTerm-adequate : ∀ {n} (F : Term S n) (x y : Fin n) (γ : S ^ n)
    → (γ ⊨ appTerm F x y)
```

充分性陈述点名各成分。`a` 与 `b` 是两个论元槽位的投影值，`G` 是该词项的解释：它是 `S` 的元素，即一个携带可构造性证书的集合，其底层集合就是那个图。所断言的是一条真值路径，连接满足关系与一个周遭隶属：对 `pr a b` 属于图的底层集合。

```agda
    ≡ (pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst (⟦ F ⟧ γ))
  appTerm-adequate F x y γ = ⇔toPath fwd bwd
    where
    a = fst (lookup x γ)
    b = fst (lookup y γ)
```

辅助工具 `read` 拆开存在量词的一个纤维。给定模型的一个元素 `z`，以及「扩展赋值满足对读式」的证明，上一节的充分性定理把该证明传输到「`z` 的底层集合等于 `pr a b`」这一命题。展开有界存在的满足关系后，前进方向收到的是隶属 `z∈G` 与这样一份读式证明的截断对；由于目标是取命题值的隶属，消去截断是合法的，而在分支内部，隶属沿 `read` 给出的路径传输。

```agda
    G = ⟦ F ⟧ γ

    read : (z : S) → ⟨ (z ∷ γ) ⊨ prAtL zero (suc x) (suc y) ⟩ → fst z ≡ pr a b
    read z h = subst ⟨_⟩ (prAtL-adequate zero (suc x) (suc y) (z ∷ γ)) h

    fwd : ⟨ γ ⊨ appTerm F x y ⟩ → ⟨ pr a b ∈ fst G ⟩
    fwd = PT.rec (snd (pr a b ∈ fst G))
```

反方向才是可构造模型登场之处。从一条赤裸的隶属证明 `⟨ pr a b ∈ fst G ⟩` 出发，必须给出截断存在的一个证明，而其第一个分量不能是集合 `pr a b` 本身：那是层级中的集合，不是 `S` 的元素。见证将在随后几行构造；这里展示的分支把隶属与一份读式证明打包，后者是把 `refl` 沿充分性路径反方向传输得到的，之所以合法，是因为见证的底层集合按定义就是 `pr a b`。

```agda
      (λ { (z , (z∈G , h)) → subst (λ w → ⟨ w ∈ fst G ⟩) (read z h) z∈G })

    bwd : ⟨ pr a b ∈ fst G ⟩ → ⟨ γ ⊨ appTerm F x y ⟩
    bwd h = ∣ zS , (h , subst ⟨_⟩
        (sym (prAtL-adequate zero (suc x) (suc y) (zS ∷ γ))) refl) ∣₁
      where
```

见证是本节唯一真正属于模型的构造。要把 `pr a b` 呈现为 `S` 的元素，需要它的可构造性证书。假设说这个对属于 `G` 的底层集合，而 `G` 自带证书；可构造类的传递性把这两个事实变成 `isL (pr a b)`。可构造集合的成员是可构造的。见证就位后，公开形式 `appAt` 把图固定在变元槽位上，即取词项 `var f`；其充分性就是一般定理在该特定词项上的实例：投影对属于槽位 `f` 处取值的底层集合。

```agda
      zS : S
      zS = pr a b , isL-trans {x = fst G} {y = pr a b} h (G .snd)

appAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
appAt f = appTerm (var f)

appAt-adequate : ∀ {n} (f x y : Fin n) (γ : S ^ n)
```

这一特化使后面的图谓词都能通过赋值槽位引用其图。投影后，每次引用统一写成 `pr (fst x) (fst y) ∈ fst (lookup f γ)`，因此单值性与定义域论证可以始终使用同一种隶属陈述。

```agda
  → (γ ⊨ appAt f x y)
  ≡ (pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst (lookup f γ))
appAt-adequate f = appTerm-adequate (var f)
```

被读的图不必落在变元槽位中；它也可以是模型的一个固定元素，被直接命名。常元词项 `con F` 正是如此，而充分性陈述随之简化：由于常元被解释为元素 `F` 本身，右边就是属于 `fst F` 的隶属，完全不再涉及环境中关于图的项。

定义在 `con F` 处实例化共用读式。由于常元被解释为它自身，有界存在直接遍历 `fst F` 的成员，充分性陈述也如实记录这一点：满足关系是一条通往「两个论元值的投影对属于 `fst F`」的路径。右边的隶属是投影后的周遭隶属；左边的存在量词仍在模型的元素上取值。

```agda
appC : ∀ {n} → S → Fin n → Fin n → Formula S n
appC F = appTerm (con F)

appC-adequate : ∀ {n} (F : S) (x y : Fin n) (γ : S ^ n)
  → (γ ⊨ appC F x y)
  ≡ (pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst F)
```

证明就是在常元词项上使用共用充分性定理，自身无需任何论证。与 `appAt` 一道，词典如今同时识别由槽位给出的图与由固定元素给出的图中的对隶属，且各自的意义都精确地是一个周遭隶属。

```agda
appC-adequate F = appTerm-adequate (con F)
```

## 单值性

一个图是单值的，如果其中任意两个第一分量相同的对具有相同的第二分量。这条陈述只谈对之间的隶属；它既不说图有成员，也不说某个给定的论元在图中出现，因此与稍后的定义域条件在逻辑上相互独立。

该断言陈述为两个方向而非一条路径，取的正是它实际被使用的形式：向外读，即从对象语言的断言得到「记在同一论元下的两个取值的底层集合相等」这一等式。

由外向内读：对一切 `x`、`y`、`y'`，若 `x` 与 `y` 的对属于该图，且 `x` 与 `y'` 的对也属于，则取值 `y` 与 `y'` 相等。所要求的相等是两个取值的底层集合之间的相等，因为 `y` 与 `y'` 本身是模型的元素。这里没有说图非空，也没有说每个论元都有取值；那是独立的定义域条件。

```agda
svAt : ∀ {n} → Fin n → Formula S n
svAt f = ∀̇ (∀̇ (∀̇ (
      appAt (suc (suc (suc f))) (suc (suc zero)) (suc zero)
  ⇒̇ (appAt (suc (suc (suc f))) (suc (suc zero)) zero
  ⇒̇ (var (suc zero) ≐ var zero)))))
```

两个方向都相对于固定的图槽位 `f` 与固定环境 `γ` 陈述，故用一个局部谓词把外部含义记录一次。`Holds x y` 说 `x` 与 `y` 的投影对属于图的底层集合；这正是 `appAt-adequate` 一次应用所产出的形状。随后两个充分性实例分别固定所读的是哪一支：`at` 对应带取值 `y` 的对，`at'` 对应带 `y'` 的对。

```agda
module _ {n : ℕ} (f : Fin n) (γ : S ^ n) where
  private
    Holds : S → S → Type (ℓ-suc ℓ)
    Holds x y = ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩

    at : (x y y' : S)
```

两个辅助命题都是在以三个被量化元素扩展后的环境处应用充分性的实例，公式的下标随之平移。由于 `at` 与 `at'` 是命题之间的路径，证明可以沿任一方向传输；下面两个方向引理做的正是这件事，只是取向相反。

```agda
       → ((y' ∷ y ∷ x ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc (suc zero)) (suc zero))
       ≡ (pr (fst x) (fst y) ∈ fst (lookup f γ))
    at x y y' = appAt-adequate (suc (suc (suc f))) (suc (suc zero)) (suc zero)
                  (y' ∷ y ∷ x ∷ γ)

    at' : (x y y' : S)
```

把对象语言的断言向外读，得到可用的结论。给定 `svAt f` 的满足关系，量词为模型的任意元素 `x`、`y`、`y'` 提供那条蕴含；把两条隶属 `Holds x y` 与 `Holds x y'` 各自先从外部形式传输到量词所期望的满足形式再喂入，便得到两个底层值相等的 `fst y ≡ fst y'`。注意结论是投影后集合的相等，而 `y` 与 `y'` 作为模型元素之间的相等并未被断言。

```agda
        → ((y' ∷ y ∷ x ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc (suc zero)) zero)
        ≡ (pr (fst x) (fst y') ∈ fst (lookup f γ))
    at' x y y' = appAt-adequate (suc (suc (suc f))) (suc (suc zero)) zero
                   (y' ∷ y ∷ x ∷ γ)

  svAt-out : ⟨ γ ⊨ svAt f ⟩
```

逆向构造的是满足关系本身。一个从任意三个带两条隶属的元素到「其取值相等」的函数，恰是三个量词与两条蕴含所要求的东西；每个所需的隶属证明都由外部那条沿 `at` 或 `at'` 正向传输而造出。两条引理合起来说明：`svAt f` 的满足与外部的单值性条件相互蕴涵，只是陈述把二者保持为两个函数，而非打包成一条路径。

```agda
           → (x y y' : S) → Holds x y → Holds x y' → fst y ≡ fst y'
  svAt-out h x y y' p q = h x y y'
    (subst ⟨_⟩ (sym (at x y y')) p) (subst ⟨_⟩ (sym (at' x y y')) q)

  svAt-in : ((x y y' : S) → Holds x y → Holds x y' → fst y ≡ fst y')
          → ⟨ γ ⊨ svAt f ⟩
```

引入方向 `svAt-in` 是消去的镜像，只是传输方向相反：每条外部隶属沿充分性路径正向传输为各蕴含所期望的满足形式，然后三个全称量词施用函数 `h`。两个方向都把整个陈述保持在底层集合的层面：结论是投影值 `fst y` 与 `fst y'` 的相等，所供给的隶属也针对投影后的对。这里没有断言每个论元都有取值，也没有断言图非空；那是下一节定义域条件的事。

```agda
  svAt-in h x y y' p q = h x y y'
    (subst ⟨_⟩ (at x y y') p) (subst ⟨_⟩ (at' x y y') q)
```

## 定义域

上一节的取值读式回答一个问题：这两个值组成的对属于该图吗？一个图可以在某些论元处命中、在另一些处落空，故下一个结构性质问的是：哪些论元有条目。落在定义域中就是有取值，其读式只是对模型的一次无界存在。定义域条件随后把候选集合 `d` 与图相比较，说「属于 `d`」与「有取值」互相蕴含；由于对象语言没有自带的双条件，这条陈述写成两条蕴含。

至此发展出的三个逻辑成分，取值、单值性与恰当定义域，彼此独立，且在后文中各自单独被用到：一个图可以单值却漏掉某些论元，可以恰定义在 `d` 上却多值，等等。这个条件并不构造任何东西；它是一个谓词，某个候选集合要么满足它要么不满足。两条消去引理各只用一个方向：`domAt-out` 消费一条实际的条目而得到定义域中的隶属，`domAt-in` 则消费定义域中的隶属，只得到条目的截断存在，因为仅凭定义域中的隶属，人们只知道某个条目存在。当需要从外部证据证明某个集合**满足**这条描述时所需的引入方向，另取了第三个名字。

定义是对模型的一次无界存在：仅仅存在取值 `y`，使论元与 `y` 的对属于该图。量词遍历的是模型的载体 `S`，而非层级的某一层，故读式所说的恰是它应当说的。充分性陈述把存在的满足关系展开为相应的依赖和；由于 `∃[ y ∶ S ] _` 以命题方式包装 `y` 的存在，右边本身也是截断的，只断言这样的 `y` 存在。

```agda
inDomAt : ∀ {n} → Fin n → Fin n → Formula S n
inDomAt f x = ∃̇ (appAt (suc f) (suc x) zero)

inDomAt-adequate : ∀ {n} (f x : Fin n) (γ : S ^ n)
  → (γ ⊨ inDomAt f x)
  ≡ (∃[ y ∶ S ] (pr (fst (lookup x γ)) (fst y) ∈ fst (lookup f γ)))
```

证明无需新的论证：无界存在的满足是其各纤维的析取，故两边在每个 `y` 处逐点一致，而逐点一致恰是扩展环境处取值充分性的一次实例。有取值一事定案后，定义域条件 `domAt f d` 在两个方向上把候选集合 `d` 与图比较：对每个元素 `x`，投影后的 `x` 属于 `d` 蕴含有取值，有取值又蕴涵属于 `d`。两条蕴含以合取相连，因为语言中没有符号直接表示它们共同的断言。

```agda
inDomAt-adequate f x γ =
  cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ y → appAt-adequate (suc f) (suc x) zero (y ∷ γ)))

domAt : ∀ {n} → Fin n → Fin n → Formula S n
domAt f d = ∀̇ ( (inDomAt (suc f) zero ⇒̇ (var zero ∈̇ var (suc d)))
             ∧̇ ((var zero ∈̇ var (suc d)) ⇒̇ inDomAt (suc f) zero) )
```

方向引理相对于固定的图槽位 `f`、固定的候选 `d` 与固定环境 `γ` 陈述。辅助命题 `step` 一劳永逸地固定被量化主体的充分性路径：在模型的元素 `x` 处，「有取值」公式的满足是一条通往「投影后的 `x` 与 `y` 的对属于图」的截断存在的路径。下面每一次传输都经过这条唯一的路径。

```agda
module _ {n : ℕ} (f d : Fin n) (γ : S ^ n) where
  private
    step : (x : S)
         → ((x ∷ γ) ⊨ inDomAt (suc f) zero)
         ≡ (∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst (lookup f γ)))
```

消去 `domAt-out` 从条目得到定义域中的隶属。给定实际的见证对 `x`、`y` 及隶属 `p`，先把截断形式组装为 `∣ y , p ∣₁`，沿 `step` 反向传输到量词所期望的满足形式，再在 `x` 处喂给第一条蕴含。输出是一条素净的隶属证明：投影后的 `x` 属于投影后的 `d`，不留任何截断。

```agda
    step x = inDomAt-adequate (suc f) zero (x ∷ γ)

  domAt-out : ⟨ γ ⊨ domAt f d ⟩ → (x y : S)
            → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
            → ⟨ fst x ∈ fst (lookup d γ) ⟩
  domAt-out h x y p = h x .fst (subst ⟨_⟩ (sym (step x)) ∣ y , p ∣₁)
```

消去 `domAt-in` 反向执行，并保留截断。定义域中的隶属 `m` 被喂给第二条蕴含，其结论正是「有取值」公式的满足；沿 `step` 正向传输后，它变成截断的依赖和。这个截断形式正是应有的陈述：仅凭定义域中的隶属，人们只知道某个条目存在，并不知道是哪一个。

```agda
  domAt-in : ⟨ γ ⊨ domAt f d ⟩ → (x : S) → ⟨ fst x ∈ fst (lookup d γ) ⟩
           → ∥ (Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩) ∥₁
  domAt-in h x m = subst ⟨_⟩ (step x) (h x .snd m)

  domAt-intro : ((x : S)
                 → (⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst (lookup f γ)) ⟩
```

引入方向把两条蕴含逐点打包。假设要求：对每个 `x`，给出一对函数，一个从条目的截断存在到 `d` 中的隶属，一个反向。由于目标都是命题，此处消费截断和是合法的；每个分量中沿 `step` 的传输与两条消去引理互为镜像。

```agda
                    → ⟨ fst x ∈ fst (lookup d γ) ⟩)
                 × (⟨ fst x ∈ fst (lookup d γ) ⟩
                    → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst (lookup f γ)) ⟩))
              → ⟨ γ ⊨ domAt f d ⟩
  domAt-intro g x = (λ h → g x .fst (subst ⟨_⟩ (step x) h))
```

组装恰好是全称量词下蕴含合取的形状：对每个 `x` 给出一个对，第一分量回答第一条蕴含，第二分量回答第二条，各分量按其所在一侧所需的方向经传输调整。有了它，一个被声称是定义域的集合，就可以仅凭外部的证据被证明满足 `domAt f d`。

```agda
                  , (λ m → subst ⟨_⟩ (sym (step x)) (g x .snd m))
```

## 模型内的配对

前面的充分性陈述都在把模型的公式向外读成周遭的事实。剩下的任务是反方向：在模型内部构造一些东西，使它们的投影正是那些读式所谈的周遭集合。一切都建立在一个构造之上：模型中两个元素的有序对。它之所以存在，是因为模型有自己的配对运算；沿 Kuratowski 方案把它应用三次，就得到任意两个元素的内部对，且无需提供任何证书，因为配对按构造就落在载体之中。必须证明的是这个内部对投影为周遭的对：沿底层集合读出它，恰得层级中两个投影分量的对，其中出现两次的那个分量由单点集恒等式处理。

模型内的 Kuratowski 编码逐项镜像环境定义：`pr a b = ⁅ ⁅ a ⁆s , ⁅ a , b ⁆ ⁆` 变成 `pairʟ` 作用于 `pairʟ a a` 与 `pairʟ a b`。由于 `pairʟ` 按构造落在载体 `S` 中，结果是模型的一个元素，无需再提供证书：每处内层的 `pairʟ` 已自带可构造性，故复合它们不需要任何额外证明。

```agda
prʟ : S → S → S
prʟ a b = pairʟ (pairʟ a a) (pairʟ a b)

prʟ-fst : (a b : S) → fst (prʟ a b) ≡ pr (fst a) (fst b)
prʟ-fst a b =
    pairʟ-fst (pairʟ a a) (pairʟ a b)
```

投影等式在 `V` 中展开同一递归。外层投影给出两个投影的对；第一分量投影为 `fst a` 与自身的无序对，而层级的恒等式 `pair-singleton` 把它塌缩为 `fst a` 的单点集。结果正是所允诺的等同：沿底层集合读出模型的对，恰好得到 `pr (fst a) (fst b)`。这条等式是下一节的关键，因为每个「标签加对」的码都将经由它投影。

```agda
  ∙ cong₂ ⁅_,_⁆ (pairʟ-fst a a ∙ pair-singleton (fst a)) (pairʟ-fst a b)
```

## 模型处的符号化

对 `prʟ` 与诸数码是单射的，而这是一般编码方案对结构的全部要求，故词项与公式如今可编码进 `L` 自身。由此得到两件事实。其一，一个码**按构造**就是模型的元素，无需可构造性证书；其二，不同的表达式有不同的码，这正是「以码为索引的表」所需要的：两处不同的子公式的出现不可共用同一个键。

随后，桥把两套编码加以比较。内部的对与数码投影为周遭的对应物，而每个码都由「标签把数码与载荷配对」造出，故每个码都投影为那条常元已被 `fst` 投影的公式的周遭码。正是这一点使在层级一侧证明的充分性定理，能够施于造在模型内部的诸码。

`prʟ` 的单射性沿其投影的同一路线：若两个模型元素的对相等，沿 `prʟ-fst` 投影两侧便得到周遭对相等的路径，而周遭的单射性 `pr-inj` 取回两个投影分量的相等。每个分量的相等生活在一个依赖和中，其第二分量是命题，即证书 `isL`，故 `Σ≡Prop` 允许从第一分量的相等得出模型元素整体的相等。

```agda
prʟ-inj : {a b c d : S} → prʟ a b ≡ prʟ c d → (a ≡ c) × (b ≡ d)
prʟ-inj {a} {b} {c} {d} e =
    Σ≡Prop (λ v → snd (isL v)) (pr-inj q .fst)
  , Σ≡Prop (λ v → snd (isL v)) (pr-inj q .snd)
  where
```

周遭对相等的那条路径由三条已有等式组装而成：取左对的投影之逆，在 `fst` 之下施加所设的相等，再投影右对。同一模式给出数码的单射性，只是 `numeralL-fst` 扮演投影的角色，而 `#-inj′` 从投影后的有限序数的相等取回自然数下标的相等。

```agda
  q : pr (fst a) (fst b) ≡ pr (fst c) (fst d)
  q = sym (prʟ-fst a b) ∙ cong fst e ∙ prʟ-fst c d

numeralL-inj : {j k : ℕ} → numeralL j ≡ numeralL k → j ≡ k
numeralL-inj {j} {k} e =
  #-inj′ (sym (numeralL-fst j) ∙ cong fst e ∙ numeralL-fst k)
```

两条单射性到手后，一般编码方案在结构 `𝒮ʟ` 处实例化，以 `prʟ` 为配对、`numeralL` 为数码：所得模块 `LCode` 把词项与公式编码进载体 `S`。桥引理接着联系两套编码，而基本情形在 `tagBridge` 中已经可见：标签把一个数码与一个载荷配成对，故其投影由 `prʟ-fst` 与数码的投影等式给出「投影后载荷」的环境标签。

```agda
module LCode = FOL.Coding {ℓ-suc ℓ} 𝒮ʟ prʟ prʟ-inj numeralL numeralL-inj

tagBridge : (k : ℕ) (x : S) → fst (LCode.mkTag k x) ≡ VCode.mkTag k (fst x)
tagBridge k x = prʟ-fst (numeralL k) x ∙ cong₂ pr (numeralL-fst k) refl

codeBridgeTm : ∀ {n} (t : Term S n) → fst LCode.⌜ t ⌝ᵗ ≡ VCode.⌜ mapTm fst t ⌝ᵗ
codeBridgeTm (con c) = tagBridge 0 c
```

词项的递归只有两种情形。常元被编码为标签 0 作用于其自身，故桥就是在该常元处的 `tagBridge 0`。变元被编码为标签 1 作用于其下标的数码，而额外那步同余把该数码的投影等式移到标签之下，因为 `mapTm fst` 已把变元常元换成它的投影。公式的递归同样开头：隶属把两个词项配成对，这里的标签 0 标记环境编码中的隶属构造子，载荷路径是 `prʟ-fst` 再接对两条词项桥的同余。

```agda
codeBridgeTm (var i) =
  tagBridge 1 (numeralL (toℕ i)) ∙ cong (VCode.mkTag 1) (numeralL-fst (toℕ i))

codeBridge : ∀ {n} (φ : Formula S n) → fst LCode.⌜ φ ⌝ ≡ VCode.⌜ mapFo fst φ ⌝
codeBridge (t ∈̇ u) = tagBridge 0 _ ∙ cong (VCode.mkTag 0)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridgeTm u))
```

余下的二元构造子重复同一个模式。每个构造子由自己的标签标记，载荷是两条直接子公式之码的有序对，投影路径则是一条标签等式再复合对两条递归桥的同余。相等、合取、析取与蕴涵只在标签数字以及两条子桥各自用在哪里上不同。

```agda
codeBridge (t ≐ u) = tagBridge 1 _ ∙ cong (VCode.mkTag 1)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridgeTm u))
codeBridge (a ∧̇ b) = tagBridge 2 _ ∙ cong (VCode.mkTag 2)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge (a ∨̇ b) = tagBridge 3 _ ∙ cong (VCode.mkTag 3)
```

零元与一元构造子以退化的载荷嵌入同一个框架。永假式被编码为标签 5 作用于零的数码，故其桥是一条标签等式，内嵌数码的投影。无界量词只携带一条子公式，因而不发生配对，载荷路径就是主体的递归桥，在标签之下传输。

```agda
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge (a ⇒̇ b) = tagBridge 4 _ ∙ cong (VCode.mkTag 4)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridge a) (codeBridge b))
codeBridge ⊥̇       = tagBridge 5 _ ∙ cong (VCode.mkTag 5) (numeralL-fst 0)
codeBridge (∃̇ a)   = tagBridge 6 _ ∙ cong (VCode.mkTag 6) (codeBridge a)
```

有界量词是唯一同时涉及两个层面的构造子：有界量词把一个词项与一条公式配对，故载荷路径先投影外层对，再把词项桥与公式桥分别施于两个分量。至此，递归覆盖词项与公式的每个构造子，且每个内部码都已知投影为投影后公式的周遭码。

```agda
codeBridge (∀̇ a)   = tagBridge 7 _ ∙ cong (VCode.mkTag 7) (codeBridge a)
codeBridge (∀̇∈ t a) = tagBridge 8 _ ∙ cong (VCode.mkTag 8)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridge a))
codeBridge (∃̇∈ t a) = tagBridge 9 _ ∙ cong (VCode.mkTag 9)
  (prʟ-fst _ _ ∙ cong₂ pr (codeBridgeTm t) (codeBridge a))
```

## 环境

给定集合 B 之上的环境是一个取值都落在 B 中的函数，因此一个候选集合 e 恰在以下四条同时成立时才算一个：它是单值的；它的定义域是给定的 d；它的取值落在 B 中；而且它**由诸对构成**。这四条在逻辑上各自独立，各有其用。单值性只约束重复出现的论元；定义域一条说有对出现的论元恰是 d 的成员；取值限制说每个取值都落在 B 中。前三条只谈及 e 中那些是有序对的成员，所以一个另带非对元素的集合也能通过它们。第四条合取项弥补了这一点，它要求 e 的每个成员都是「d 的一个成员与 B 的一个成员」的对，从而使每个环境都是 d × B 的子集；排除非对成员这件事，正是前三条无法给出的。

本节给出的是关于单个候选的谓词，以及把每个合取项读回出来的消去引理。某个特定集合**是否就是**给定长度的全体环境的集合，是另一个更难的问题，这里不作解决。

第三个合取项限制取值。它对两个变元 x 与 y 作全称量化并断言：只要 x 与 y 构成的对属于图 e，取值 y 就必须属于 B。注意这里**没有**说什么：它不要求任何特定的 x 有取值，那是定义域一条的事。这一条只约束已有的条目，因此它既不使图成为函数，也不固定其定义域。

```agda
valuesInAt : ∀ {n} → Fin n → Fin n → Formula S n
valuesInAt f B = ∀̇ (∀̇ ( appAt (suc (suc f)) (suc zero) zero
                     ⇒̇ (var zero ∈̇ var (suc (suc B))) ))

valuesInAt-out : ∀ {n} (f B : Fin n) (γ : S ^ n)
               → ⟨ γ ⊨ valuesInAt f B ⟩ → (x y : S)
```

把这一条读出来只需一个方向，而且是直接的。设图中已有以 x 为第一分量、以 y 为取值的对；把全称量词施加于 x 与 y 即可，剩下的待证事项就是其中的蕴含。故先把隶属事实 p 换成前件的满足：`appAt-adequate` 把该满足等同于在投影后的环境 (y ∷ x ∷ γ) 处的隶属，沿其对称等式作替换，便恰好给出量化主体所需要的论据。结论是投影后的取值属于投影后的 B，全程不涉及截断。

```agda
               → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
               → ⟨ fst y ∈ fst (lookup B γ) ⟩
valuesInAt-out f B γ h x y p = h x y
  (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (y ∷ x ∷ γ))) p)

pairsInAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
```

第四个合取项，即诸对那条，全部用有界量词写出。它说：对 e 的每个成员 s，存在 d 的成员 u 与 B 的成员 v，使 s 等于 u 与 v 的对。由于量词遍历的是实际成员，这条只约束 e、d、B 中已有的东西，其含义也将在投影后从这些集合读出。主体是本章前文的对读式 `prAtL`，下标按三个约束子后移。

```agda
pairsInAt e d B =
  ∀̇∈ (var e) (∃̇∈ (var (suc d)) (∃̇∈ (var (suc (suc B)))
    (prAtL (suc (suc zero)) (suc zero) zero)))

pairsIn-out : ∀ {n} (e d B : Fin n) (γ : S ^ n) → ⟨ γ ⊨ pairsInAt e d B ⟩
            → (s : S) → ⟨ fst s ∈ fst (lookup e γ) ⟩
```

从诸对那条读出时保留了满足的形状：结论是一个命题截断，只是**仅仅存在**这样的 u 与 v。前提 h 是「公式成立」的普通证明，而 s∈ 是投影后的 s 属于投影后的 e 的普通隶属。该类型准确说明能恢复什么：u 在 d 中、v 在 B 中，且 s 的底集等于二者底集的对，一切都仅仅是存在。

```agda
            → ∥ (Σ[ u ∈ S ] (Σ[ v ∈ S ]
                  (⟨ fst u ∈ fst (lookup d γ) ⟩
                   × (⟨ fst v ∈ fst (lookup B γ) ⟩
                      × (fst s ≡ pr (fst u) (fst v)))))) ∥₁
pairsIn-out e d B γ h s s∈ = PT.rec squash₁
```

证明在截断之内剥去两层有界存在。这里消去命题截断是合法的，因为目标仍是命题，即一个 Σ 型的截断；所以并未全局地选取任何东西，每个分支只变换自己的见证。内层一步是本章反复出现的同一替换：`prAtL-adequate` 把主体的满足变成路径 `fst s ≡ pr (fst u) (fst v)`，环境按约束子的次序扩展为 v、u、s。

```agda
  (λ { (u , (u∈ , hv)) → PT.map
    (λ { (v , (v∈ , hp)) → u , (v , (u∈ , (v∈ , subst ⟨_⟩
      (prAtL-adequate (suc (suc zero)) (suc zero) zero (v ∷ u ∷ s ∷ γ)) hp))) })
    hv })
  (h s s∈)
```

反方向把逐成员的陈述取为前提。对每个投影后属于投影后 e 的 s，前提仅仅提供被截断的四元组：u、v、二者各自的隶属，以及对的等式；任务是把它们变成有界公式的满足。两个方向保持为两条引理而不合并成一条路径，因为有关论证每次恰好只用一个方向。

```agda
pairsIn-in : ∀ {n} (e d B : Fin n) (γ : S ^ n)
           → ((s : S) → ⟨ fst s ∈ fst (lookup e γ) ⟩
              → ∥ (Σ[ u ∈ S ] (Σ[ v ∈ S ]
                    (⟨ fst u ∈ fst (lookup d γ) ⟩
                     × (⟨ fst v ∈ fst (lookup B γ) ⟩
```

构造把前提中的被截断数据直接变成公式的满足。见证 u 与 v 连同各自的隶属原样通过，而对等式 eq 则沿充分性路径的对称等式传输，变成主体的满足，因为这里是从集合层面的对等式走回读式的满足。截断只经由 `PT.map` 进入，它在重新整理的数据周围重建被截断的和；公式自身的含义会供给其量词所需的任何截断。

```agda
                        × (fst s ≡ pr (fst u) (fst v)))))) ∥₁)
           → ⟨ γ ⊨ pairsInAt e d B ⟩
pairsIn-in e d B γ k s s∈ = PT.map
  (λ { (u , (v , (u∈ , (v∈ , eq)))) → u , (u∈ , ∣ v , (v∈ , subst ⟨_⟩
    (sym (prAtL-adequate (suc (suc zero)) (suc zero) zero (v ∷ u ∷ s ∷ γ))) eq) ∣₁) })
```

把四条合在一起，便得到「以 d 为定义域、取值在 B 中的环境」的定义：单值性、恰当的定义域、取值限制与诸对条目，用 `∧̇` 连接。接着一个匿名模块固定元数、三个指标、环境 γ，以及「γ 满足该合取」的证明，使四个投影可以只陈述一次，而不必每次重复这些参数。

```agda
  (k s s∈)

envOverAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
envOverAt e d B =
  svAt e ∧̇ (domAt e d ∧̇ (valuesInAt e B ∧̇ pairsInAt e d B))

module _ {n : ℕ} (e d B : Fin n) (γ : S ^ n) (h : ⟨ γ ⊨ envOverAt e d B ⟩) where
```

每个投影就是四重连言的满足所构成的嵌套对中的相应分量。第一个是 e 的单值性，第二个是联系 e 与 d 的定义域条，第三个是朝向 B 的取值限制，第四个是诸对条目本身。四者齐备之后，只需环境性质的某一面的论证便可直接取用而无需重组整个合取；而构造环境的论证也可以逐条合取项来检验。

```agda
  envOver-sv     : ⟨ γ ⊨ svAt e ⟩
  envOver-sv     = h .fst
  envOver-dom    : ⟨ γ ⊨ domAt e d ⟩
  envOver-dom    = h .snd .fst
  envOver-values : ⟨ γ ⊨ valuesInAt e B ⟩
```

这四个投影也说明了定义的模块性：唯一性、定义域、取值范围与对的形状可以分别迁移或使用，而它们的合取仍是「该候选者为 `d` 上取值于 `B` 的环境」这一完整断言。

```agda
  envOver-values = h .snd .snd .fst
  envOver-pairs  : ⟨ γ ⊨ pairsInAt e d B ⟩
  envOver-pairs  = h .snd .snd .snd
```

迄今构造的每条读式都只查看环境放在其指标处的底层集合：关于图、定义域或取值集合的满足断言，总是在用 `fst` 投影所查各项之后陈述的。由此可见，环境的描述在外延上只依赖三个集合，即投影后的图、投影后的定义域与投影后的取值集合，而不依赖环境的任何其他方面。于是，若两个元数可以不同的环境，把同样三个集合放在描述所查的指标处，则该描述在其中一个处成立，当且仅当它在另一个处成立。

这正是后文把「关于某个环境的陈述」变成「关于某个构造真正造出的集合的陈述」的关键：构造可以随意用它喜欢的索引来呈现其环境，只要三个底层集合吻合，描述便原样适用。

迁移定理需要取值限制的引入方向，即此前未曾提取的那个方向：从「图中每个对如何如何」的陈述回到满足本身。给定一个把图中任一对送到 B 中取值的函数，只需施加那两个全称量词，并用取值读式的充分性等式把隶属事实换成前件的满足。至此，`valuesInAt` 的两个方向各有一条引理可用。

```agda
valuesInAt-in : ∀ {n} (f B : Fin n) (γ : S ^ n)
              → ((x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
                 → ⟨ fst y ∈ fst (lookup B γ) ⟩)
              → ⟨ γ ⊨ valuesInAt f B ⟩
valuesInAt-in f B γ k x y hp = k x y
```

定理比较两个环境 γ 与 `γ'`，二者元数可以不同，并在每侧各取三个指标。前提是投影后集合之间的路径：图、定义域与取值集合作为层级中的集合逐元素相等。对两侧指标之间的关系不作任何假设，只假设投影后查表所得一致；这正是一个用别的索引呈现其环境的构造所处的情形。

```agda
  (subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (y ∷ x ∷ γ)) hp)

envOverAt-transport : ∀ {n n'} (γ : S ^ n) (γ' : S ^ n')
                      (e d B : Fin n) (e' d' B' : Fin n')
                    → fst (lookup e γ) ≡ fst (lookup e' γ')
                    → fst (lookup d γ) ≡ fst (lookup d' γ')
```

单值性的迁移是把 γ 处的消去引理与 `γ'` 处的引入引理复合。设在 `γ'` 处同一自变量 x 下记有两个取值 y 与 `y'`，先用「认同两侧投影图中对隶属」的路径把前提搬回 γ 一侧的满足；消去引理随后给出两个投影值相等，引入引理再把它包装成 `γ'` 处的满足。这个相等本身无需传输，因为两侧的取值都是 S 的元素。

```agda
                    → fst (lookup B γ) ≡ fst (lookup B' γ')
                    → ⟨ γ ⊨ envOverAt e d B ⟩ → ⟨ γ' ⊨ envOverAt e' d' B' ⟩
envOverAt-transport γ γ' e d B e' d' B' qe qd qb h =
    svAt-in e' γ' (λ x y y' p q →
      svAt-out e γ (envOver-sv e d B γ h) x y y'
```

定义域一条经由 `domAt` 的引入引理迁移，在 `γ'` 处同时给出两个蕴含。第一个蕴含说：有取值就必在定义域中。从取值的仅仅被截断的存在出发，γ 处的消去引理给出对投影后定义域 d 的隶属，消去到隶属命题无需选定任何见证，再由路径 qd 把这条隶属搬到 `d'` 一侧。

```agda
        (subst ⟨_⟩ (sym (at x y)) p) (subst ⟨_⟩ (sym (at x y')) q))
  , ( domAt-intro e' d' γ'
      (λ x → (λ m → subst (λ w → ⟨ fst x ∈ w ⟩) qd
                (PT.rec (snd (fst x ∈ fst (lookup d γ)))
                  (λ { (y , p) → domAt-out e d γ (envOver-dom e d B γ h) x y
```

第二个蕴含方向相反：在定义域中就必有取值。先把 `d'` 中的隶属沿对称路径搬回，γ 处的消去引理随即给出「有条目」的仅仅被截断的存在，再在截断内部把主体的满足换成 `γ'` 一侧的形式。取值 y 本身原样通过，这也正确：两个图只是投影后一致，而条目是 S 的元素。

```agda
                         (subst ⟨_⟩ (sym (at x y)) p) })
                  m))
            , (λ hx → PT.map (λ { (y , p) → y , subst ⟨_⟩ (at x y) p })
                (domAt-in e d γ (envOver-dom e d B γ h) x
                  (subst (λ w → ⟨ fst x ∈ w ⟩) (sym qd) hx))))
```

迁移取值限制时，先从新投影图中的一条对隶属出发。沿图隶属路径的反向把它搬回旧图，随后旧环境处的 `valuesInAt-out` 给出该取值属于旧集合 `B`；最后沿 `qb : B ≡ B′` 正向搬运一次，得到它属于 `B′`。因此 `qb` 只使用一次，方向从旧取值集合到新取值集合。

```agda
    , ( valuesInAt-in e' B' γ'
        (λ x y p → subst (λ w → ⟨ fst y ∈ w ⟩) qb
          (valuesInAt-out e B γ (envOver-values e d B γ h) x y
            (subst ⟨_⟩ (sym (at x y)) p)))
      , pairsIn-in e' d' B' γ'
```

诸对一条最后迁移，而各次传输都留在截断之内。在 γ 处读出该条，仅仅是得到见证 u 与 v、二者对投影后 d 与 B 的隶属，以及对的等式。两条隶属分别由 qd 与 qb 搬到 `d'` 与 `B'`，而等式 `fst s ≡ pr (fst u) (fst v)` 完全无需传输：它谈的是底层集合，前提恰好说这些集合一致，故这条等式在两侧是同一条。

```agda
        (λ s s∈ → PT.map
          (λ { (u , (v , (u∈ , (v∈ , eq)))) →
            u , (v , ( subst (λ w → ⟨ fst u ∈ w ⟩) qd u∈
                     , ( subst (λ w → ⟨ fst v ∈ w ⟩) qb v∈ , eq ) )) })
          (pairsIn-out e d B γ (envOver-pairs e d B γ h) s
```

剩下的原料就是路径 `at`：对每个 x 与 y，认同两侧「该对属于投影后的图」的路径。它是同余性，即把两条图之间的等式 qe 作用到固定对分量的隶属谓词上。定理内部凡涉及图的传输都经过这一条路径，因此整个论证只依赖所给的三条等式，别无隐藏之物。

```agda
            (subst (λ w → ⟨ fst s ∈ w ⟩) (sym qe) s∈))) ) )
  where
  at : (x y : S) → (pr (fst x) (fst y) ∈ fst (lookup e γ))
                 ≡ (pr (fst x) (fst y) ∈ fst (lookup e' γ'))
  at x y = cong (λ w → pr (fst x) (fst y) ∈ w) qe
```

## 容纳配对分量

读取配对形状的码会暴露它的两个分量，而把二者同时呈现为**同一个**可构造集合的成员会带来方便。候选对象由数学本身决定：若 `fst x` 是 `fst u` 与 `fst v` 的有序对，则无序对 `⁅ fst u , fst v ⁆` 属于 `fst x`，故由 `L` 的传递性它自身可构造，且两个分量都是它的成员。本节记录的正是这个见证连同三条隶属事实：一个类型 `Container x u v`，以及从路径 `fst x ≡ pr (fst u) (fst v)` 造出它的构造 `container`。

该类型把模型的一个元素 `s` 与三条周遭隶属事实打包，全部在投影后陈述：`s` 的底集属于 `fst x`，而 `u`、`v` 的底集都属于 `fst s`。除此之外不作任何断言；特别地，它并不声称 `s` 是具有此性质的极小集合。构造 `container` 以「`fst x` 等于 `pr (fst u) (fst v)`」为前提，把见证连同三份证书一并返回。

```agda
Container : (x u v : S) → Type (ℓ-suc ℓ)
Container x u v = Σ[ s ∈ S ] (⟨ fst s ∈ fst x ⟩ × (⟨ fst u ∈ fst s ⟩ × ⟨ fst v ∈ fst s ⟩))

opaque
  container : (x u v : S) → fst x ≡ pr (fst u) (fst v) → Container x u v
  container x u v e = s , (s∈ , (∈pair-introL refl , ∈pair-introR refl))
```

见证就是两个底集的无序对。作为 Kuratowski 编码之外层无序对的一个成员，它在自反路径上的引入规则下属于 `pr (fst u) (fst v)`，沿前提 `e` 传输后便成为对 `fst x` 的隶属。而这恰是 `L` 传递性所消费的输入：既然该无序对属于一个可构造集合，`isL-trans` 便把它连同证书一起作为 `S` 的元素给出。余下的两条隶属，即 `fst u` 与 `fst v` 属于它，则由自反路径上的两条引入规则给出。

```agda
    where
    s∈ : ⟨ ⁅ fst u , fst v ⁆ ∈ fst x ⟩
    s∈ = subst (λ w → ⟨ ⁅ fst u , fst v ⁆ ∈ w ⟩) (sym e) (∈pair-introR refl)
    s : S
    s = ⁅ fst u , fst v ⁆ , isL-trans s∈ (snd x)
```

## 小结

本章弥合了语义两侧之间的裂缝。公式在 `L` 中、在由可构造元素组成的环境处被满足，而它们需要表达的具体事实却是关于底集的周遭事实；词典各词条以精确的充分性路径把两侧连起来。有序对识别是绝对的；图的隶属经传递性获得可构造的见证；环境描述汇集了单值性、恰当定义域、取值限制与诸对条目，且只依赖三个投影后的集合。语法符号化随之在 `L` 内部实例化，桥定理表明内部码投影为投影后公式的周遭码，于是写在层级一侧的读式可以施于内部造出的码。容器则为配对形状的码给出一个同时容纳两个分量的可构造集合。