---
title: "环境集的一致性"
module: L.Coding.EnvironmentAgreement
lang: zh
site: "Bedrock"
description: "环境集的一致性"
stage: "内部编码：表与统一满足关系"
reading_order: 52
canonical: https://bedrock.institute/zh/L.Coding.EnvironmentAgreement.html
html: L.Coding.EnvironmentAgreement.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/EnvironmentAgreement.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Absoluteness, V.Hierarchy, L.Constructible, L.Coding.Model, L.Coding.Expressions, L.Coding.EnvironmentSet]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.EnvironmentAgreement.md, https://bedrock.institute/ja/L.Coding.EnvironmentAgreement.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 环境集的一致性

满足关系的诸子句需要在 `L` 内部有一个集合，恰好收齐给定基集合上给定长度的全部环境。较早的章节分别给出了两项材料：按成员刻画这种集合的公式 `envSetAt`，以及上一章构造的集合 `envSet B m`。一个集合满足该描述，当且仅当其成员作为集合恰是基上长度 `m` 环境的图。本章证明这条描述与已构造的集合彼此一致，而一致有两个读法。凡被某个满足判断放到描述之集合槽位上的集合，其成员恰为已构造集合的成员；已构造的集合自身也满足该描述，于是绑定自己的基与长度的子句可以先把已构造的数据填入槽位，再引用这条描述。

两种读法都落在同一个对象上：从成员恢复出的环境。四条内部子句，单值性、以数码为定义域、取值落在基中、以及由数码与基中成员组成的对，说明一个集合正是这样的图；上一章由此恢复了那个赋值函数，并把该集合与其典范图等同起来。本章的每一步都归结为沿某个方向运行这一恢复，再加上一条搬运引理：当两个环境中被点名的槽位一致时，它把环境子句的满足关系从一个环境搬到另一个环境。

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

全书的常设选项继续生效。本章唯一的非构造性输入明确表现为下方的参数 `lem`。

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

基础词汇按《基础词汇》的安排整体引入。排中律不作为选项，而作为数据进入，本章以参数的形式接收它。

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

模块参数是层级 `ℓ-suc ℓ` 上的排中律实例，正是两个结构的满足陈述所在的层级。它被转交给本章所引用的、构造环境集的那一章。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
```

解释语言的有两个结构，本章在它们之间移动。周遭结构 `𝒮ᵥ` 就是层级自身；内层结构 `𝒮ʟ` 把它限制到可构造集，即 `isL` 所指的类。该类是传递的，由 `isL-trans` 记录；绝对性机制被引入，恰好在这一对结构上工作。

```agda
open import L.Coding.Model {ℓ} using ( envOverAt; envOverAt-transport )
open import L.Coding.Expressions {ℓ} using ( envSetAt; extAt-out; extAt-in; extAt-in-both; numL )
```

两条公式及其读式承担本章的工作。环境子句 `envOverAt` 说候选图是单值的，其定义域恰为指定定义域槽位中的集合，其取值属于指定基集合，且只含由这两个集合的成员组成的对；搬运引理则在被点名的槽位一致的环境之间移动这条子句的满足。外延描述 `envSetAt` 以两条全称蕴含的形式说：一个集合的成员恰好是那些环境；三条读式按任一方向拆开这两条蕴含。

```agda
open import L.Coding.EnvironmentSet {ℓ} lem
  using ( envSet; envSet-in; envSet-out; envS; envOver; module Recover )
```

来自上一章的有：已构造的集合 `envSet`、它的两条隶属引理、典范图元素 `envS`、在其自身典范环境处满足的环境子句 `envOver`，以及恢复模块，后者从四条子句读出一个环境，并把该集合与那个环境的图等同起来。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_ )
```

从环境集的隶属解码出表示它的环境时，只得到截断见证；目标中的满足与隶属陈述则都是命题。周遭数码 `# m` 填充长度槽位。

```agda
open hPropStructure 𝒮ʟ
```

打开内层结构即固定全章使用的满足记号：其载体的成员、其隶属关系，以及在 `L` 中读出的满足判断。

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

绝对性模块在可构造集这个传递类上实例化，其内层满足关系被改名为朴素的 `_⊨_`，因为本章读出的每条公式都在 `L` 之上，没有别的读法与它竞争。

## 从描述得到隶属关系

第一个模块固定基集合 `B`、某个长度 `k` 的环境 `γ`、它的三个槽位、一个长度 `m`，以及两条等式，后者说明长度槽位由 `m` 的数码填充、基槽位由 `B` 填充。其前提是 `γ` 满足以 `Ei` 为集合槽位的描述。结论是成员的一致：`Ei` 处所指名的集合与已构造的 `envSet B m` 恰好包含相同的集合。

两个方向都只依赖同样的两件材料。恢复模块从四条子句读出一个环境，并把来源集合与那个环境的典范图等同起来；搬运引理沿那几条命名等式，把环境子句的满足在被点名的槽位一致的环境之间搬运。两个方向都不重新证明描述，也不重新证明构造。

```agda
private
  nn : ℕ → S
  nn j = # j , numL j
```

长度槽位由一个数码填充，而数码本身必须是 `L` 的元素。辅助定义 `nn` 造出它：周遭的冯·诺伊曼数码 `# j` 连同其可构造性证明组成的对。

```agda
module Ambient (B : S) {k : ℕ} (γ : S ^ k) (Ei di bi : Fin k) (m : ℕ)
  (qd : fst (lookup di γ) ≡ # m) (qb : fst (lookup bi γ) ≡ fst B)
  (hE : ⟨ γ ⊨ envSetAt Ei di bi ⟩) where
```

模块汇集了该问题一个实例的全部数据。`B` 是基集合，`γ` 是长度 `k` 的环境，其中三个槽位被点名：`Ei` 装着候选集合，`di` 装着长度的数码，`bi` 装着基。等式 `qd` 与 `qb` 说明这两个槽位确实由 `m` 的数码与 `B` 填充，而 `hE` 说明 `γ` 满足以 `Ei` 为集合槽位的描述。在这些数据之下，`Ei` 处的集合与 `envSet B m` 被证明具有相同的成员。

```agda
  into : (z : S) → ⟨ fst z ∈ fst (lookup Ei γ) ⟩
       → ⟨ fst z ∈ fst (envSet B m) ⟩
```

第一个方向把槽位集合向内读：`Ei` 处所指名集合的任何成员，都是已构造的 `envSet B m` 的成员。

```agda
  into z hz = subst (λ w → ⟨ w ∈ fst (envSet B m) ⟩)
    (sym (Recover.recovers B m (z ∷ γ) zero (suc di) (suc bi) qd qb ov))
    (envSet-in B (Recover.g B m (z ∷ γ) zero (suc di) (suc bi) qd qb ov))
```

证明复用上一章的恢复过程，并把它对准这个成员本身。前提说 `z` 属于 `Ei` 处的集合，于是描述在 `z` 处适用：恢复过程从 `z` 读出一个环境 `g`，其典范图作为集合正是 `z` 自己。已构造的集合包含每个这样的环境的典范图，沿这条等同传输后，成员 `z` 便落入 `envSet B m`。

```agda
    where
    ov : ⟨ (z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi) ⟩
    ov = extAt-out Ei (envOverAt zero (suc di) (suc bi)) γ hE z hz
```

恢复需要那四条子句在 `z` 处成立，而描述给出的恰是这件事：把它施用于成员 `z`，便得到在扩展了 `z` 的环境上的环境子句，长度与基的槽位则越过新条目相应后移。

```agda
  outof : (z : S) → ⟨ fst z ∈ fst (envSet B m) ⟩
        → ⟨ fst z ∈ fst (lookup Ei γ) ⟩
```

第二个方向向外读：已构造的 `envSet B m` 的任何成员，都是 `Ei` 处所指名集合的成员。

```agda
  outof z hz = PT.rec (snd (fst z ∈ fst (lookup Ei γ)))
    (λ { (g , eg) →
```

已构造集合中的隶属交出一个截断的见证：一个环境 `g`，其典范图就是 `z`。目标是隶属陈述，因而是命题，截断因此可以消耗；而产出见证的，正是上一章的隶属刻画。

```agda
      extAt-in Ei (envOverAt zero (suc di) (suc bi)) γ hE z
        (envOverAt-transport (B ∷ nn m ∷ envS B g ∷ []) (z ∷ γ)
          (suc (suc zero)) (suc zero) zero zero (suc di) (suc bi)
          (sym eg) (sym qd) (sym qb)
          (envOver B g)) })
```

恢复出的环境在它自己的典范环境处满足环境子句，那里三个槽位装着 `B`、`m` 的数码与它的图。搬运引理沿三条等式把这个满足搬到扩展环境 `(z ∷ γ)`：把典范图读作 `z`，把数码读作 `di` 处的条目，把 `B` 读作 `bi` 处的条目。描述随即经其内向蕴含适用，结论是 `z` 属于 `Ei` 处的集合。

```agda
    (envSet-out B m z hz)
```

交给搬运的那个环境来自已构造集合的隶属刻画，施用于本方向出发时的那个成员 `z`。

## 已构造的集合满足描述

第二个模块把一致反过来，问的是产出方向：已构造的环境集自身满足这条描述吗？把它放在集合槽位、在另两个槽位放上 `m` 的数码与基之后，答案是肯定的；而这正是绑定自己的基与长度的子句在用已构造数据填充槽位时所需要的。证明沿与先前相同的两步运行，只是次序改由描述支配：已构造集合的每个成员都被证明满足逐成员子句，而每个满足该子句的集合也被证明是其成员。

模块不假设任何满足前提。它的三条等式说明：集合槽位装着已构造的集合自身，长度槽位装着 `m` 的数码，基槽位装着 `B`；仅凭这些，即可证明 `γ` 处的完整描述。

```agda
module AmbientHolds (B : S) {k : ℕ} (γ : S ^ k) (Ei di bi : Fin k) (m : ℕ)
  (qE : fst (lookup Ei γ) ≡ fst (envSet B m))
  (qd : fst (lookup di γ) ≡ # m) (qb : fst (lookup bi γ) ≡ fst B)
  where
```

三条等式就是全部前提。用已构造集合点名集合槽位、用数码点名长度槽位、用基点名基槽位，恰是子句以已构造数据填充三个槽位时所做的事，因此模块证明的描述，正是这类子句所消费的形式。

```agda
  holds : ⟨ γ ⊨ envSetAt Ei di bi ⟩
  holds = extAt-in-both Ei (envOverAt zero (suc di) (suc bi)) γ fwd bwd
```

这条描述是外延式的：它说 `Ei` 处的集合恰好包含那些环境；其两个全称蕴含分别证明后再合并。这正是模块开头预告的形状，此处将它填实。

```agda
    where
    fwd : (z : S) → ⟨ fst z ∈ fst (lookup Ei γ) ⟩
        → ⟨ (z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi) ⟩
```

向前蕴含是产出方向：已构造集合的每个成员都在扩展环境上满足逐成员子句。

```agda
    fwd z hz = PT.rec (snd ((z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi)))
      (λ { (g , eg) → envOverAt-transport (B ∷ nn m ∷ envS B g ∷ []) (z ∷ γ)
```

隶属 `hz` 先沿等式 `qE` 被重新指到已构造的集合上，上一章的隶属引理随即交出一个截断的环境。另一侧的目标是满足判断的一条子句，因而是命题，截断的见证因此可以拆开。

```agda
             (suc (suc zero)) (suc zero) zero zero (suc di) (suc bi)
             (sym eg) (sym qd) (sym qb) (envOver B g) })
```

恢复出的环境的环境子句被搬运，方式与读取方向完全相同：从其典范环境搬到判断的扩展环境上，图被读作成员 `z`，数码被读作 `di` 处的条目，基被读作 `bi` 处的条目。余下的就是那条子句本身，这正是向前蕴含所欠的东西。

```agda
      (envSet-out B m z (subst (λ w → ⟨ fst z ∈ w ⟩) qE hz))
```

交给搬运的那个环境来自已构造集合的隶属刻画，而 `qE` 供给了第一步：把该成员读作 `envSet B m` 的成员。

```agda
    bwd : (z : S) → ⟨ (z ∷ γ) ⊨ envOverAt zero (suc di) (suc bi) ⟩
        → ⟨ fst z ∈ fst (lookup Ei γ) ⟩
```

向后蕴含是读取方向：凡在扩展环境上满足逐成员子句者，都属于 `Ei` 处的集合。

```agda
    bwd z h = subst (λ w → ⟨ fst z ∈ w ⟩) (sym qE)
      (subst (λ w → ⟨ w ∈ fst (envSet B m) ⟩)
        (sym (Recover.recovers B m (z ∷ γ) zero (suc di) (suc bi) qd qb h))
        (envSet-in B (Recover.g B m (z ∷ γ) zero (suc di) (suc bi) qd qb h)))
```

`z` 处的子句正是恢复的输入：恢复出的环境的典范图作为集合与 `z` 一致，而已构造的集合包含那个图。第一次传输把恢复出的图读作 `z`，使隶属落入 `envSet B m`；第二次沿 `qE` 反向进行，把对 `envSet B m` 的隶属变为对 `Ei` 处集合的隶属。