---
title: "环境塔"
module: L.Coding.EnvironmentTower
lang: zh
site: "Bedrock"
description: "环境塔"
stage: "内部编码：表与统一满足关系"
reading_order: 60
canonical: https://bedrock.institute/zh/L.Coding.EnvironmentTower.html
html: L.Coding.EnvironmentTower.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/EnvironmentTower.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Absoluteness, V.Hierarchy, V.Coding, V.Model, L.Constructible, L.Coding.Environment, L.Coding.Model, L.Coding.Expressions, L.Coding.Quantification, L.Coding.EnvironmentSet, L.Coding.EnvironmentAgreement, L.Recursion, L.Axioms.Basic, L.Axioms.Full, L.Axioms.Numerals, L.Axioms.Infinity]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.EnvironmentTower.md, https://bedrock.institute/ja/L.Coding.EnvironmentTower.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
本章在 `L` 内构造环境塔。对每个自然数 `n`，该塔记录码化有序对 `(# n, envSet W n)`，其中 `envSet W n` 是全体取值于 `W` 的 `n` 元环境之集。我们先构造这个实际集合，再给出一份有界一阶描述，供后续章节读取其中的码化条目。

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

这一构造在立方类型论中进行，并使用所标宇宙层级上的排中律。该经典假设经由定长环境集、公共界、分离以及内部自然数集的构造进入本章。

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

固定宇宙层级 `ℓ` 与实例 `lem : LEM (ℓ-suc ℓ)`。下文所有构造都相对于这一项假设，不再加入更强的经典原理。

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

本章会同时使用环境塔的两种描述。第一种是在外围构造 `L` 中的一个集合，第二种是集合论对象语言中的公式。该公式由隶属、相等、合取、析取与有界量化组成，Lévy 层级检查器则会认证它属于 Δ₀。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ⊥̇; ∃̇_; ∃̇∈; ∀̇∈ )
open import FOL.LevyHierarchy using ( checkΔ₀; Δ₀ )
import FOL.Absoluteness
```

稍后的证明会把环境塔条目向下读到前驱。累积层级中的隶属归纳保证这种下降良基，而外延性在成员相同时识别两个环境集。码化有序对的单射性继而分别恢复数码分量与环境集分量。

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV )
open import V.Coding {ℓ} using ( pr; pr-inj )
open import V.Model {ℓ} using ( self∈sucV )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Environment {ℓ} using ( env; cons )
```

连接两种描述的桥梁，是识别码化有序对、冯·诺伊曼后继、环境集与 cons 扩展的公式。容器使分量量词保持有界，而充分性引理把这些公式的满足与累积层级中的相应构造联系起来。

```agda
open import L.Coding.Model {ℓ} using ( prAtL; prʟ; prʟ-fst; container )
open import L.Coding.Expressions {ℓ} using
  ( envSetAt; sucAtL; consAtL; consAtL-adequate; numL )
open import L.Coding.Quantification {ℓ} using
  ( i0; i1; i2; i3; sh; pr-out; pr-in; down; suc-out; suc-in
```

读取或构造码化有序对时，需要反复访问其两个分量。双分量量词在有界公式内部提供这种访问，其引入与消去引理保持满足关系的命题性。族 `envSet W n` 则提供与这些分量比较的语义集合。

```agda
  ; i4; i5
  ; sndEx; bothEx; bothAll
  ; sndEx-out; bothEx-out; bothAll-in
  ; fillSnd; fillBoth; useBoth )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet; envSet-in; envSet-out; envS; Ix )
```

环境集公式只能按外延确定一个集合，其一致定理把这份描述与已构造的 `envSet W n` 比较。随后，公共界与完整分离把所有元数收进一个可构造集合，而可构造数码提供各条目的第一分量。

```agda
open import L.Coding.EnvironmentAgreement {ℓ} lem using ( module Ambient; module AmbientHolds )
open import L.Recursion {ℓ} lem using ( smallDom )
open import L.Axioms.Basic {ℓ} using ( extensionalL )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
```

内部集合 `ωʟ` 把对象语言中的元数与外围自然数联系起来。读取其成员时，会在命题截断下得到一个自然数，以及该成员与相应可构造数码的同一视。因此，这一读法只确定某个元数存在，并不为每个成员全局选出一个元数。

```agda
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ; ω-specL )
```

有限向量表示解释公式所用的环境，依值对与余积则表达其语义返回的见证和情形分裂。自然数加法记录有界有序对读取器引入的额外槽位。

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Unit using ( tt )
open import Cubical.Data.Vec using ( _∷_; []; lookup )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
```

本章许多语义见证都位于命题截断之下。若目标本身是命题，例如隶属、满足关系或层级集合之间的相等，便可以使用这种见证；但不能从中投影出全局选定的元数或环境。命题外延性与空类型分别支持相应的相等和不可能性论证。

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
```

累积层级中的集合带有其成员的小呈现。在隶属与相应纤维之间转换，使证明能够把 `W` 的任意成员变成一个呈现索引。同一层级还提供冯·诺伊曼数码 `# n` 及其后继运算 `sucV`。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties using
  ( ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; sucV )
```

以 `S` 表示可构造集合的类型。`S` 的元素由一个底层层级集合及其属于 `L` 的证据组成；下文证明通过第一投影比较底层集合，并在构造见证时保留可构造性证据。

```agda
open hPropStructure 𝒮ʟ using ( S )
```

公式的满足关系在可构造集合向量上解释。`L` 的传递性把这种内部解释与外围累积层级联系起来，因此，同一批底层隶属事实既能支撑对象语言公式，也能支撑外围构造。

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

## 构造环境塔集合

固定这一解释后，首要任务便是把按元数索引的所有环境集收进一个集合。

塔模块固定载体 `W`，环境的取值即其成员。其第 `n` 个条目是「可构造数码 `n` 与长度为 `n` 的全体环境之集」的编码有序对：第一分量记录长度，第二分量收集恰该长度的所有环境。

```agda
module Tower (W : S) where
  entry : ℕ → S
  entry n = prʟ (numeralL n) (envSet W n)
```

诸条目先由小定义域原理收进一个公共容器。容器只是公共上界；精确的集合由下一步的分离刻出。

```agda
  private
    dom : Σ[ d ∈ S ] ((k : Lift {ℓ-zero} {ℓ} ℕ) → ⟨ fst (entry (lower k)) ∈ fst d ⟩)
    dom = smallDom (Lift {ℓ-zero} {ℓ} ℕ) (λ k → entry (lower k))
```

分离公式把候选分解为元数与环境集，并施加四个条件：基集见证等于 `W`；候选是该元数与环境集的码化有序对；元数属于内部 `ω`；该集合满足「它是 `W` 上这一元数的环境集」这一一阶外延描述 `envSetAt`。开头三个存在量词无界，因此这里使用完整分离，而非下文的 Δ₀ 论证。

```agda
    towerFo : Formula S 1
    towerFo = ∃̇ (∃̇ (∃̇ ( (var i2 ≐ con W)
                      ∧̇ ( prAtL i3 i1 i0
                      ∧̇ ( (var i1 ∈̇ con ωʟ)
                      ∧̇ envSetAt i0 i1 i2 )))))
```

塔由容器上的分离刻出并保持不透明，后文论证只通过其隶属规格使用它。

```agda
  opaque
    tower : S
    tower = hasSeparationL (dom .fst) towerFo .fst .fst
```

隶属规格被导出：塔中的隶属即容器中的隶属且满足分离公式。

```agda
    tower-mem : (x : S)
              → (fst x ∈ fst tower) ≡ ((fst x ∈ fst (dom .fst)) ⊓ ((x ∷ []) ⊨ towerFo))
    tower-mem = hasSeparationL (dom .fst) towerFo .fst .snd
```

关键材料是：每个环境集在其自身条目处满足其外延描述。环境集、其数码、载体与条目被置入四槽环境，而描述在该处按构造成立。

```agda
  private
    holdsAt : (n : ℕ) → ⟨ (envSet W n ∷ numeralL n ∷ W ∷ entry n ∷ []) ⊨ envSetAt i0 i1 i2 ⟩
    holdsAt n = AmbientHolds.holds W (envSet W n ∷ numeralL n ∷ W ∷ entry n ∷ [])
                  i0 i1 i2 n refl (numeralL-fst n) refl
```

于是每个标准条目都属于塔：容器隶属由界定记录供给，分离公式由载体、数码与环境集构成的截断见证满足。

```agda
    tower-in : (n : ℕ) → ⟨ fst (entry n) ∈ fst tower ⟩
    tower-in n = subst ⟨_⟩ (sym (tower-mem (entry n)))
      ( dom .snd (lift n)
      , ∣ W , ∣ numeralL n , ∣ envSet W n
        , ( refl
```

见证树嵌套载体、可构造数码与环境集，每一层各自搬运其分量：有序对经配对投影法则被识别，数码隶属经内部 `ω` 读法识别，而描述由上述材料满足。

```agda
          , ( pr-in i3 i1 i0 (envSet W n ∷ numeralL n ∷ W ∷ entry n ∷ [])
                (prʟ-fst (numeralL n) (envSet W n))
            , ( subst ⟨_⟩ (sym (ω-specL (numeralL n))) ∣ lift n , refl ∣₁
              , holdsAt n ))) ∣₁ ∣₁ ∣₁ )
```

标准条目随后以外围标准形重述：由两条投影法则，可构造数码与环境集的编码对的底层有序对，等于数码与底层层的朴素对。

```agda
  tower-in′ : (n : ℕ) → ⟨ pr (# n) (fst (envSet W n)) ∈ fst tower ⟩
  tower-in′ n = subst (λ u → ⟨ u ∈ fst tower ⟩)
    (prʟ-fst (numeralL n) (envSet W n) ∙ cong (λ u → pr u (fst (envSet W n))) (numeralL-fst n))
    (tower-in n)
```

反之，可以读出所构造环境塔的成员：每个成员仅仅是某个数码与相应长度环境集的码化有序对。自然数及其等式位于命题截断之下，因此该结论只记录存在性，并未为每个成员定义一个元数选择。证明先展开隶属规格，再取出其中满足分离公式的分量。

```agda
  tower-out : (x : S) → ⟨ fst x ∈ fst tower ⟩
            → ∥ Σ[ n ∈ ℕ ] (fst x ≡ pr (# n) (fst (envSet W n))) ∥₁
  tower-out x hx = PT.rec squash₁ byB (subst ⟨_⟩ (tower-mem x) hx .snd)
    where
    Goal : Type (ℓ-suc ℓ)
```

目标类型明确表达这一边界：它是命题截断，其中仅仅存在自然数 `n`，并有从该成员的底层集合到标准有序对 `pr (# n) (fst (envSet W n))` 的等式。

```agda
    Goal = ∥ Σ[ n ∈ ℕ ] (fst x ≡ pr (# n) (fst (envSet W n))) ∥₁
```

分离公式绑定三个见证。第一次消去命名基集见证 `b`；余下的公式随后把它与 `W` 认同，并继续暴露元数见证和环境集见证。

```agda
    byB : Σ[ b ∈ S ] ⟨ (b ∷ x ∷ []) ⊨ ∃̇ (∃̇ ( (var i2 ≐ con W)
                    ∧̇ ( prAtL i3 i1 i0
                    ∧̇ ( (var i1 ∈̇ con ωʟ)
                    ∧̇ envSetAt i0 i1 i2 )))) ⟩ → Goal
    byB (b , hb) = PT.rec squash₁ byN hb
```

第二次消去把元数命名为可构造集合。

```agda
      where
      byN : Σ[ n ∈ S ] ⟨ (n ∷ b ∷ x ∷ []) ⊨ ∃̇ ( (var i2 ≐ con W)
                    ∧̇ ( prAtL i3 i1 i0
                    ∧̇ ( (var i1 ∈̇ con ωʟ)
                    ∧̇ envSetAt i0 i1 i2 ))) ⟩ → Goal
```

第三次消去命名环境集并暴露四个合取支：基集是 `W`、有序对被识别、元数属于内部 `ω`，且环境集的外延描述成立。

```agda
      byN (n , hn) = PT.rec squash₁ byE hn
        where
        byE : Σ[ F ∈ S ] ⟨ (F ∷ n ∷ b ∷ x ∷ []) ⊨ ( (var i2 ≐ con W)
                    ∧̇ ( prAtL i3 i1 i0
                    ∧̇ ( (var i1 ∈̇ con ωʟ)
```

有序对读取器恢复从该成员到「元数与所描述集合的码化有序对」的等式。随后，元数属于内部 `ω` 这一事实在命题截断之下给出一个普通自然数，其可构造数码具有相同的底层集合。

```agda
                    ∧̇ envSetAt i0 i1 i2 ))) ⟩ → Goal
        byE (F , (qb , (hp , (hω , hE)))) = PT.rec squash₁ byK (subst ⟨_⟩ (ω-specL n) hω)
          where
          xq : fst x ≡ pr (fst n) (fst F)
          xq = pr-out i3 i1 i0 (F ∷ n ∷ b ∷ x ∷ []) hp
```

数码同一视把被记录的元数与该自然数的可构造数码对齐；环境一致模块在四槽环境处打开，准备比较被描述的集合与实际构造的集合。

```agda
          byK : Σ[ k ∈ Lift {ℓ-zero} {ℓ-suc ℓ} ℕ ] (fst n ≡ fst (numeralL (lower k))) → Goal
          byK (k , qn) = ∣ lower k , xq ∙ cong₂ pr (qn ∙ numeralL-fst (lower k)) Eq ∣₁
            where
            module Am = Ambient W (F ∷ n ∷ b ∷ x ∷ []) i0 i1 i2 (lower k)
                          (qn ∙ numeralL-fst (lower k)) qb hE using (into; outof)
```

一致模块供给被描述集与实际环境集之间隶属的两个方向；`L` 内的外延性把这两个方向转换为底层集合的等式。

```agda
            Eq : fst F ≡ fst (envSet W (lower k))
            Eq = cong fst (extensionalL {a = F} {b = envSet W (lower k)}
              (λ z → ⇔toPath (Am.into z) (Am.outof z)))
```

## 环境塔的有界规格

空性谓词说一个集合全无成员，由对其成员的有界全称表达。

```agda
emptyAll : ∀ {m} → Fin m → Formula S m
emptyAll x = ∀̇∈ (var x) ⊥̇
```

空集单点子句有两个合取支：该集合含有一个空成员，且其每个成员都是空的。两者都需要：第一个是存在子句，没有它该谓词也会对空集自身成立。

```agda
sglEmpty : ∀ {m} → Fin m → Formula S m
sglEmpty F = ∃̇∈ (var F) (emptyAll i0) ∧̇ ∀̇∈ (var F) (emptyAll i0)
```

cons 像子句给出集合相等所需的两个包含方向。所提议后继集的每个成员都必须仅仅是某个载体元素接到某个前驱集成员之前所得的 cons；反过来，对每个前驱环境与每个载体元素，相应的 cons 扩展都必须仅仅出现于后继集中。两项合起来说明后继集恰含这些 cons 扩展而无额外成员。

```agda
consImage : ∀ {m} → Fin m → Fin m → Fin m → Formula S m
consImage F' F w =
    ∀̇∈ (var F') (∃̇∈ (var (sh 1 w)) (∃̇∈ (var (sh 2 F)) (consAtL i2 i1 i0)))
  ∧̇ ∀̇∈ (var F) (∀̇∈ (var (sh 1 w)) (∃̇∈ (var (sh 2 F')) (consAtL i0 i1 i2)))
```

当前条目被分解为元数与环境集后，这两个主体描述相邻的一步。`upBody` 说新元数是当前元数的后继，且新环境集是当前环境集的 cons 像。`downBody` 反转这些角色：当前元数是前驱元数的后继，且当前环境集是前驱环境集的 cons 像。

```agda
private
  upBody downBody : ∀ {m} → Fin m → Formula S (8 + m)
  upBody w = sucAtL i5 i1 ∧̇ consImage i0 i4 (sh 8 w)
  downBody w = sucAtL i1 i5 ∧̇ consImage i4 i0 (sh 8 w)
```

向上子句在塔上作存在量化：塔中某条目满足向上主体。

```agda
  towerUp : ∀ {m} → Fin m → Fin m → Formula S (4 + m)
  towerUp E w = ∃̇∈ (var (sh 4 E)) (bothEx i0 (upBody w))
```

向下子句是一个析取：条目等于带空环境集的基条目，或塔中某条目是其 cons 像为当前条目的前驱。这正是下文隶属归纳读法所依赖的。

```agda
  towerDown : ∀ {m} → Fin m → Fin m → Fin m → Formula S (4 + m)
  towerDown E w N0 =
      ((var i1 ≐ var (sh 4 N0)) ∧̇ sglEmpty i0)
    ∨̇ ∃̇∈ (var (sh 4 E)) (bothEx i0 (downBody w))
```

完整公式合取了关于码化有序对条目的三个有界条件：`E` 中出现一个基准对；`E` 中每个经有序对接口读出的成员都有向上的后继；每个这样的对要么是基准对，要么具有前驱。因此，`towerAt` 控制的是后文读取器所使用的码化有序对条目。它本身不排除 `E` 中任意的非有序对成员，本章也没有由任意 `E` 满足该公式推出它等于所构造的 `Tower.tower W`。

```agda
towerAt : ∀ {m} → Fin m → Fin m → Fin m → Formula S m
towerAt E w N0 =
    ∃̇∈ (var E) (sndEx i0 (sh 1 N0) (sglEmpty i0))
  ∧̇ ( ∀̇∈ (var E) (bothAll i0 (towerUp E w))
    ∧̇ ∀̇∈ (var E) (bothAll i0 (towerDown E w N0)) )
```

Δ₀ 证书由检查器产出。它只证明每个量词都有界；公式的语义正确性由下文读取引理另行建立，而非由该证书证明。

```agda
Δ₀-towerAt : ∀ {m} (E w N0 : Fin m) → Δ₀ (towerAt E w N0)
Δ₀-towerAt E w N0 = checkΔ₀ (towerAt E w N0) tt
```

## 零元与后继元数的环境集

事实模块固定载体 `W`，并收集关于零长与后继长环境的实际递推事实。

```agda
module EnvFacts (W : S) where
  private
    ι : ⟪ fst W ⟫ → V ℓ
    ι = ⟪ fst W ⟫↪
```

每个被呈现索引指名 `W` 的一个成员：小隶属桥从呈现通入底层集合。

```agda
    ι∈ : (q : ⟪ fst W ⟫) → ⟨ ι q ∈ fst W ⟩
    ι∈ q = ∈∈ₛ {a = ι q} {b = fst W} .snd (∈ₛ⟪ fst W ⟫↪ q)
```

长度为零的索引恰有一个，其识别源于「从空类型出发的函数由不可能情形定义」。

```agda
    g0 : Ix W 0
    g0 ()
```

无成员的集合等于零长环境图，由外延性：两侧都没有成员，因为零长索引没有情形。

```agda
  noMembers→env0 : (z : V ℓ) → ((y : V ℓ) → ⟨ y ∈ z ⟩ → Empty.⊥) → z ≡ fst (envS W g0)
  noMembers→env0 z k = extensionalV (λ y → ⇔toPath
    (λ hy → Empty.rec (k y hy))
    (PT.rec (snd (y ∈ z)) (λ { (lift () , _) })))
```

反过来，长度为零的每个环境图都没有成员：索引没有情形，故编码成员所需的对无法形成。

```agda
  envAny0-noMembers : (g : Ix W 0) (y : V ℓ) → ⟨ y ∈ fst (envS W g) ⟩ → Empty.⊥
  envAny0-noMembers g y = PT.rec Empty.isProp⊥ (λ { (lift () , _) })
```

读出零长环境集：其每个成员都是无成员的集合。证明消去截断的呈现并应用前述事实。

```agda
  envSet0-out : (z : V ℓ) → ⟨ z ∈ fst (envSet W 0) ⟩
              → (y : V ℓ) → ⟨ y ∈ z ⟩ → Empty.⊥
  envSet0-out z hz y hy = PT.rec Empty.isProp⊥
    (λ { (g , e) → envAny0-noMembers g y (subst (λ u → ⟨ y ∈ u ⟩) e hy) })
    (envSet-out W 0 (down (envSet W 0) z hz) hz)
```

填充零长环境集使用空集：它被搬运进呈现，而空图由其无成员证明被识别。

```agda
  envSet0-in : (z : V ℓ) → ((y : V ℓ) → ⟨ y ∈ z ⟩ → Empty.⊥) → ⟨ z ∈ fst (envSet W 0) ⟩
  envSet0-in z k = subst (λ u → ⟨ u ∈ fst (envSet W 0) ⟩) (sym (noMembers→env0 z k)) (envSet-in W g0)
```

环境编码在函数层与 cons 一致：前置一个载体元素并移动索引，逐条目地恰好编码了编码函数的 cons。

```agda
  cons-env : (q : ⟪ fst W ⟫) {k : ℕ} (g : Ix W k)
           → env (cons (ι q) (λ i → ι (g i))) ≡ fst (envS W (cons q g))
  cons-env q g = cong env (funExt (λ { zero → refl ; (suc i) → refl }))
```

`W` 的每个成员把每个长度为 `k` 的环境延拓为长度 `suc k` 的环境：`W` 的新成员由一个索引呈现，延拓后的函数被插入后继环境集。

```agda
  envCons∈ : {k : ℕ} (x : V ℓ) → ⟨ x ∈ fst W ⟩ → (g : Ix W k)
           → ⟨ env (cons x (λ i → ι (g i))) ∈ fst (envSet W (suc k)) ⟩
  envCons∈ {k} x x∈ g =
    subst (λ u → ⟨ u ∈ fst (envSet W (suc k)) ⟩)
      (sym (cong (λ v → env (cons v (λ i → ι (g i)))) (sym (fib .snd)) ∙ cons-env (fib .fst) g))
```

呈现索引经呈现在该成员处的纤维恢复，因此编码使用的是 `x` 的实际呈现索引。

```agda
      (envSet-in W (cons (fib .fst) g))
    where
    fib : Σ[ q ∈ ⟪ fst W ⟫ ] (ι q ≡ x)
    fib = ∈-asFiber {a = x} {b = fst W} x∈
```

该插入对「带底层集同一视的可构造元素」重述：沿该同一视搬运，即得属于后继环境集。

```agda
  envSuc-in : {k : ℕ} (x e' : S) → ⟨ fst x ∈ fst W ⟩ → (g : Ix W k)
            → fst e' ≡ env (cons (fst x) (λ i → ι (g i)))
            → ⟨ fst e' ∈ fst (envSet W (suc k)) ⟩
  envSuc-in {k} x e' x∈ g qe' =
    subst (λ u → ⟨ u ∈ fst (envSet W (suc k)) ⟩) (sym qe') (envCons∈ (fst x) x∈ g)
```

后继环境在函数层拆为头部与尾部。若 `g'` 索引一个后继环境，则其底层集合等于以 `ι (g' zero)` 为零号条目、以 `ι (g' (suc i))` 为第 `i+1` 条目的编码图。证明依赖于环境构造子在函数外延性下的函数性，后者说两个索引函数在每个槽位处取值相同。

```agda
  env-split : {k : ℕ} (g' : Ix W (suc k))
            → fst (envS W g') ≡ env (cons (ι (g' zero)) (λ i → ι (g' (suc i))))
  env-split g' = cong env (funExt (λ { zero → refl ; (suc i) → refl }))
```

后继环境的向外读法只在命题截断下恢复其头部与尾部。对 `envSet W (suc k)` 的每个成员 `e'`，仅仅存在一个呈现索引 `q`、一个尾部索引 `g : Ix W k` 及一条等式，其中 `q` 指名 `W` 的成员 `ι q`，而该等式把 `e'` 的底层集合识别为二者 cons 函数的码化图。

```agda
  envSuc-out : {k : ℕ} (e' : S) → ⟨ fst e' ∈ fst (envSet W (suc k)) ⟩
             → ∥ Σ[ q ∈ ⟪ fst W ⟫ ] Σ[ g ∈ Ix W k ]
                  (fst e' ≡ env (cons (ι q) (λ i → ι (g i)))) ∥₁
  envSuc-out {k} e' h = PT.map
    (λ { (g' , e) → g' zero , (λ i → g' (suc i)) , (e ∙ env-split g') })
```

隶属证明被环境集的向外读法消耗，后者供给截断的索引；图的等式再与拆分引理复合，产出 cons 等式。

```agda
    (envSet-out W (suc k) e' h)
```

## 读取后继环境的构造

cons 像读取器以候选后继集 `F'`、候选基集 `F`、字母表槽 `w` 与环境为参数，连同把字母表槽与工作集对齐的等式。

```agda
module ConsImageRead {m : ℕ} (F' F w : Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) where
  open EnvFacts W
  private
    ι : ⟪ fst W ⟫ → V ℓ
```

载体到层级的嵌入只命名一次，使每个载体元素可在编码需要时呈现为层级元素。

```agda
    ι = ⟪ fst W ⟫↪
```

对 `W` 载体中的每个 `q`，呈现映射都把 `ι q` 放入 `W` 的底层集合。证明从该集合的典范呈现所给出的 fibre 中读出隶属。

```agda
    ι∈' : (q : ⟪ fst W ⟫) → ⟨ ι q ∈ fst W ⟩
    ι∈' q = ∈∈ₛ {a = ι q} {b = fst W} .snd (∈ₛ⟪ fst W ⟫↪ q)
```

cons 像子句的向外读法说：若基集等于 `k` 处的层环境集，则满足 cons 像子句的集合等于后继层环境集。证明以外延性比较成员于两个方向。

向前方向经 cons 像子句读取候选后继集的成员 `z`。

```agda
  consImage-out : (k : ℕ) → fst (lookup F γ) ≡ fst (envSet W k)
                → ⟨ γ ⊨ consImage F' F w ⟩ → fst (lookup F' γ) ≡ fst (envSet W (suc k))
  consImage-out k qF (h1 , h2) = extensionalV (λ z → ⇔toPath (fwd z) (bwd z))
    where
    fwd : (z : V ℓ) → ⟨ z ∈ fst (lookup F' γ) ⟩ → ⟨ z ∈ fst (envSet W (suc k)) ⟩
```

子句供给载体元素 `x`、编码环境条目 `e` 与 cons 等式；基集的环境集向外读法供给截断索引 `g`。每个截断见证都被消去到下一条命题。

```agda
    fwd z hz = PT.rec (snd (z ∈ fst (envSet W (suc k))))
      (λ { (x , (x∈ , hx)) → PT.rec (snd (z ∈ fst (envSet W (suc k))))
        (λ { (e , (e∈ , hc)) → PT.rec (snd (z ∈ fst (envSet W (suc k))))
          (λ { (g , qe) →
            envSuc-in x zS (subst (λ u → ⟨ fst x ∈ u ⟩) qw x∈) g
```

在向前包含中，cons 像子句的前半部给出头部 `x`、尾环境 `e`，以及码化 cons 关系的满足。把 `e` 作为真实基环境集的成员读取，会在命题截断下得到一个尾部索引。随后，`consAtL` 的充分性把 `z` 与语义上的 cons 图识别，`envSuc-in` 再把该图放入 `envSet W (suc k)`。每个截断都只消去到这个隶属命题中。

```agda
              (subst ⟨_⟩ (consAtL-adequate i2 i1 i0 (e ∷ x ∷ zS ∷ γ) (λ i → ι (g i)) qe) hc) })
          (envSet-out W k e (subst (λ u → ⟨ fst e ∈ u ⟩) qF e∈)) })
        hx })
      (h1 zS hz)
      where
```

`z` 属于候选后继集的证明给出一个可构造代表 `zS : S`，其底层集合就是 `z`。这个代表随后被传给有界 cons 像读取器。

```agda
      zS : S
      zS = down (lookup F' γ) z hz
```

为证明反向包含，取真实后继环境集的成员 `z`。其后继分解仅仅给出头部 `q`、尾部索引 `g`，以及把 `z` 认同为二者 cons 环境的等式。cons 像子句的后半部随后仅仅给出候选后继集中的相应成员 `e'`。

```agda
    bwd : (z : V ℓ) → ⟨ z ∈ fst (envSet W (suc k)) ⟩ → ⟨ z ∈ fst (lookup F' γ) ⟩
    bwd z hz = PT.rec (snd (z ∈ fst (lookup F' γ)))
      (λ { (q , g , qz) → PT.rec (snd (z ∈ fst (lookup F' γ)))
        (λ { (e' , (e'∈ , hc)) →
          subst (λ u → ⟨ u ∈ fst (lookup F' γ) ⟩)
```

`consAtL` 的充分性把子句所给出的对象语言 cons 关系认同为语义分解中使用的同一码化 cons 图。将该等式与分解等式复合，便认同 `e'` 与 `z`，从而可把 `e'` 的隶属运输为 `z` 的隶属。

```agda
            (subst ⟨_⟩ (consAtL-adequate i0 i1 i2 (e' ∷ xS q ∷ envS W g ∷ γ) (λ i → ι (g i)) refl) hc
             ∙ sym qz)
            e'∈ })
        (h2 (envS W g) (subst (λ u → ⟨ fst (envS W g) ∈ u ⟩) (sym qF) (envSet-in W g))
            (xS q) (subst (λ u → ⟨ ι q ∈ u ⟩) (sym qw) (ι∈' q))) })
```

两个命题截断都只被消去到正在证明的隶属命题中。`zS` 在可构造载体内呈现 `z`，而 `xS` 将以同样方式呈现恢复出的头部。

```agda
      (envSuc-out zS hz)
      where
      zS : S
      zS = down (envSet W (suc k)) z hz
      xS : ⟪ fst W ⟫ → S
```

对恢复出的头部 `q`，其像 `ι q` 属于 `W`；因此，可构造性的传递性为它配备构成载体元素 `xS q` 所需的证书。

```agda
      xS q = ι q , isL-trans {x = fst W} {y = ι q} (ι∈' q) (snd W)
```

cons 像子句的向内方向由与真实层环境集的两个认同证明。cons 像子句的两个方向至此可用。

```agda
  consImage-in : (k : ℕ) → fst (lookup F γ) ≡ fst (envSet W k)
               → fst (lookup F' γ) ≡ fst (envSet W (suc k))
               → ⟨ γ ⊨ consImage F' F w ⟩
  consImage-in k qF qF' = h1 , h2
    where
```

向内读法的第一方向说，候选后继集的每个成员都满足一个有界存在式：存在头部元素与来自基集的环境，其 cons 扩展即该成员。

成员的截断分解被消耗以名指头部与尾部。

```agda
    h1 : (e' : S) → ⟨ fst e' ∈ fst (lookup F' γ) ⟩
       → ⟨ (e' ∷ γ) ⊨ ∃̇∈ (var (sh 1 w)) (∃̇∈ (var (sh 2 F)) (consAtL i2 i1 i0)) ⟩
    h1 e' he' = PT.map
      (λ { (q , g , qe') →
        let xS : S
```

头部被载入载体，尾部经基集隶属认同呈现为基集元素，而 cons 充分性把 cons 等式运入对象语言。

```agda
            xS = ι q , isL-trans {x = fst W} {y = ι q} (ι∈' q) (snd W)
        in xS , ( subst (λ u → ⟨ ι q ∈ u ⟩) (sym qw) (ι∈' q)
              , ∣ envS W g , ( subst (λ u → ⟨ fst (envS W g) ∈ u ⟩) (sym qF) (envSet-in W g)
                             , subst ⟨_⟩ (sym (consAtL-adequate i2 i1 i0 (envS W g ∷ xS ∷ e' ∷ γ) (λ i → ι (g i)) refl)) qe' ) ∣₁ ) })
      (envSuc-out e' (subst (λ u → ⟨ fst e' ∈ u ⟩) qF' he'))
```

第二个子句从基集成员 `e` 与字母表集成员 `x` 出发。它只需给出候选后继集中的一个成员，使其码化图由把 `x` 接到 `e` 所表示的环境之前得到。

基环境集的向外读法仅仅给出尾部索引 `g`；语义上的 cons 引入随后把所得图放入真实后继环境集。

```agda
    h2 : (e : S) → ⟨ fst e ∈ fst (lookup F γ) ⟩ → (x : S) → ⟨ fst x ∈ fst (lookup w γ) ⟩
       → ⟨ (x ∷ e ∷ γ) ⊨ ∃̇∈ (var (sh 2 F')) (consAtL i0 i1 i2) ⟩
    h2 e he x hx = PT.map
      (λ { (g , qe) →
        let m : ⟨ env (cons (fst x) (λ i → ι (g i))) ∈ fst (envSet W (suc k)) ⟩
```

构造出的环境沿 cons 引理供给的隶属下降而呈现为后继层环境集的元素。cons 充分性把 cons 子句的满足运入对象语言。

```agda
            m = envCons∈ (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) qw hx) g
            e' : S
            e' = down (envSet W (suc k)) (env (cons (fst x) (λ i → ι (g i)))) m
        in e' , ( subst (λ u → ⟨ fst e' ∈ u ⟩) (sym qF') m
                , subst ⟨_⟩ (sym (consAtL-adequate i0 i1 i2 (e' ∷ x ∷ e ∷ γ) (λ i → ι (g i)) qe)) refl ) })
```

基集向外读法供给截断索引 `g`，其环境即条目 `e`。

```agda
      (envSet-out W k e (subst (λ u → ⟨ fst e ∈ u ⟩) qF he))
```

数码被呈现为可构造元素：有限序数连同其可构造性证书。

```agda
nn : ℕ → S
nn k = # k , numL k
```

## 读取环境塔规格

单点空集模块以候选集槽位与环境为参数。

```agda
module SglEmpty (W : S) {m : ℕ} (F : Fin m) (γ : S ^ m) where
  open EnvFacts W
```

单点空集子句的向外读法说：满足该子句的集合与零层环境集具有相同底层集合。证明以外延性在两个方向比较成员。

第一个被命名的对象是候选的底层集合，而 `none` 辅助式从有界子句提取反驳。

```agda
  sglEmpty-out : ⟨ γ ⊨ sglEmpty F ⟩ → fst (lookup F γ) ≡ fst (envSet W 0)
  sglEmpty-out (hex , hall) = extensionalV (λ z → ⇔toPath (fwd z) (bwd z))
    where
    Fv = fst (lookup F γ)
    none : (z : S) → ⟨ (z ∷ γ) ⊨ emptyAll i0 ⟩ → (y : V ℓ) → ⟨ y ∈ fst z ⟩ → Empty.⊥
```

`none` 辅助式把成员的载体呈现喂给有界子句，后者返回空类型，确认所呈现集合无成员。

```agda
    none z k y hy = Empty.rec* (k (down z y hy) hy)
```

向前：候选集的成员被呈现，有界子句反驳其每个成员，故它无成员；零层引入随后接纳它为零层环境集的成员。

```agda
    fwd : (z : V ℓ) → ⟨ z ∈ Fv ⟩ → ⟨ z ∈ fst (envSet W 0) ⟩
    fwd z hz = envSet0-in z (none (down (lookup F γ) z hz) (hall (down (lookup F γ) z hz) hz))
```

向后：零层环境集的成员被呈现，其截断索引被消耗。被索引的环境与该成员本身均被证明无成员，故由层级外延性二者相等。

```agda
    bwd : (z : V ℓ) → ⟨ z ∈ fst (envSet W 0) ⟩ → ⟨ z ∈ Fv ⟩
    bwd z hz = PT.rec (snd (z ∈ Fv))
      (λ { (e , (e∈ , he)) →
        subst (λ u → ⟨ u ∈ Fv ⟩)
          (noMembers→env0 (fst e) (none e he) ∙ sym (noMembers→env0 z (envSet0-out z hz)))
```

被运输的隶属闭合向后方向，而存在子句确认候选集非空，证明完成。

```agda
          e∈ })
      hex
```

为证明向内读式，选择空环境 `e0`。存在项成立，因为 `e0` 属于零层环境集且没有成员。全称项成立，因为该环境集的每个成员都没有成员。沿假设的等式运输，便在两项中都以候选集替代真实零层集。

```agda
  sglEmpty-in : fst (lookup F γ) ≡ fst (envSet W 0) → ⟨ γ ⊨ sglEmpty F ⟩
  sglEmpty-in q =
      ∣ e0 , ( subst (λ u → ⟨ fst e0 ∈ u ⟩) (sym q) (envSet-in W (λ ()))
             , (λ y hy → lift (envAny0-noMembers (λ ()) (fst y) hy)) ) ∣₁
    , (λ z hz y hy → lift (envSet0-out (fst z) (subst (λ u → ⟨ fst z ∈ u ⟩) q hz) (fst y) hy))
```

空环境是从空类型出发的函数的编码图，它没有条目。

```agda
    where
    e0 : S
    e0 = envS W (λ ())
```

环境塔读取器固定候选塔槽 `E`、参数集槽 `w`、零数码槽 `N0` 与解释环境。其假设把 `w` 与工作集 `W` 识别，把 `N0` 与 `# 0` 识别，并断言 `towerAt E w N0` 得到满足。下文两种读法恰好相对于这些同一视成立。

```agda
module TowerRead {m : ℕ} (E w N0 : Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (qN0 : fst (lookup N0 γ) ≡ # 0)
  (h : ⟨ γ ⊨ towerAt E w N0 ⟩) where
  private
    Ev = fst (lookup E γ)
```

塔公式的三个合取项被命名：基项子句、向上闭合子句与向下分解子句。

```agda
    hbase = h .fst
    hup = h .snd .fst
    hdown = h .snd .snd
```

条目是「自然数元数连同以该元数呈现的环境集」的截断记录。它是塔的向外方向的读取目标。

```agda
  Entry : V ℓ → V ℓ → Type (ℓ-suc ℓ)
  Entry n F = ∥ Σ[ k ∈ ℕ ] ((n ≡ # k) × (F ≡ fst (envSet W k))) ∥₁
```

塔条目的向外读法由编码对第一分量的集合隶属归纳证明。动机说：对层级中每个元素 `nv`，若某条目的第一分量等于 `nv` 且该条目属于候选塔，则该条目分解为自然数元数连同其环境集。这是对层级隶属关系的良基归纳，而非对自然数的普通归纳。

步进函数按塔公式的向下分解子句分裂。

```agda
  entry-out : (n F : S) → ⟨ pr (fst n) (fst F) ∈ Ev ⟩ → Entry (fst n) (fst F)
  entry-out n F = ∈-induction {P = P} step (fst n) n F refl
    where
    P : V ℓ → Type (ℓ-suc ℓ)
    P nv = (n F : S) → fst n ≡ nv → ⟨ pr (fst n) (fst F) ∈ Ev ⟩ → Entry (fst n) (fst F)
```

隶属归纳的步进按塔公式的向下分解子句分裂：该对或是基项，或有一前驱条目。

```agda
    step : (nv : V ℓ) → ((y : V ℓ) → ⟨ y ∈ nv ⟩ → P y) → P nv
    step nv IH n F qn p∈ = PT.rec squash₁ cases
      (useBoth i0 (pS ∷ γ) n F refl (towerDown E w N0) (hdown pS p∈))
      where
      pS : S
```

候选有序对的隶属证明给出一个可构造代表 `pS : S`。其容器通过有界量化暴露数码分量与环境集分量，四槽环境则把这些分量连同该有序对放在本章外围环境之前。

```agda
      pS = down (lookup E γ) (pr (fst n) (fst F)) p∈
      c = container pS n F refl
      δ : S ^ (4 + m)
      δ = F ∷ n ∷ c .fst ∷ pS ∷ γ
```

情形分裂消耗向下分解的满足。基例读取零数码等式连同单点空集向外读法，产出元数零与零层环境集。后继情形传入递归步。

```agda
      cases : ((fst n ≡ fst (lookup N0 γ)) × ⟨ δ ⊨ sglEmpty i0 ⟩)
            ⊎ ⟨ δ ⊨ ∃̇∈ (var (sh 4 E)) (bothEx i0 (downBody w)) ⟩
            → Entry (fst n) (fst F)
      cases (inl (qn0 , hF)) = ∣ 0 , (qn0 ∙ qN0 , SglEmpty.sglEmpty-out W i0 δ hF) ∣₁
      cases (inr hs) = PT.rec squash₁
```

后继情形拆开有界存在：前驱条目 `p'` 与后继等式，随后是前驱数码 `n'`、前驱环境集 `F'`、cons 容器与 cons 等式。四槽扩展为归纳做准备。

序数比较说：候选数码是前驱数码的冯·诺伊曼后继。

```agda
        (λ { (p' , (p'∈ , hb)) → PT.rec squash₁
          (λ { (n' , F' , s' , (qp' , (hsuc , hci))) →
            let δ' = F' ∷ n' ∷ s' ∷ p' ∷ δ
                qsuc : fst n ≡ sucV (fst n')
                qsuc = suc-out i1 i5 δ' hsuc
```

前驱数码属于候选数码，因为每个集合都属于其冯·诺伊曼后继；沿后继等式运输后，这正是隶属归纳所需的严格下降。应用归纳假设即可恢复元数 `k` 与层 `envSet W k`。

```agda
                n'∈ : ⟨ fst n' ∈ nv ⟩
                n'∈ = subst (λ u → ⟨ fst n' ∈ u ⟩) (sym qsuc ∙ qn) (self∈sucV (fst n'))
            in PT.map
              (λ { (k , (qk , qF')) →
                suc k , ( qsuc ∙ cong sucV qk
```

恢复的元数被映到其后继，cons 像向外读法把基层环境集运到后继层环境集。归纳假设施于前驱，其隶属沿塔等式运输。

```agda
                        , ConsImageRead.consImage-out i4 i0 (sh 8 w) δ' W qw k qF' hci ) })
              (IH (fst n') n'∈ n' F' refl
                (subst (λ u → ⟨ u ∈ Ev ⟩) qp' p'∈)) })
          (bothEx-out i0 (downBody w) (p' ∷ δ) hb) })
        hs
```

向内读式对外围自然数 `k` 作普通归纳。在零步，基项子句仅仅给出一个塔成员及其第二分量。读取 `sglEmpty` 将该分量认同为 `envSet W 0`，而对齐式 `N0 = # 0` 认同其第一分量；沿所得有序对等式运输，即得标准零条目。

```agda
  entry-in : (k : ℕ) → ⟨ pr (# k) (fst (envSet W k)) ∈ Ev ⟩
  entry-in zero = PT.rec (snd (pr (# 0) (fst (envSet W 0)) ∈ Ev))
    (λ { (p , (p∈ , hs)) → PT.rec (snd (pr (# 0) (fst (envSet W 0)) ∈ Ev))
      (λ { (F , s , (qp , hF)) →
        subst (λ u → ⟨ u ∈ Ev ⟩)
```

零步闭合后，后继步骤把向上闭合子句应用于已经构造出的第 `k` 个标准条目。该子句仅仅给出一个新的塔成员，以及满足后继公式的数码和满足 cons 像公式的环境集。

```agda
          (qp ∙ cong₂ pr qN0 (SglEmpty.sglEmpty-out W i0 (F ∷ s ∷ p ∷ γ) hF))
          p∈ })
      (sndEx-out i0 (sh 1 N0) (sglEmpty i0) (p ∷ γ) hs) })
    hbase
  entry-in (suc k) = PT.rec (snd (pr (# (suc k)) (fst (envSet W (suc k))) ∈ Ev))
```

后继公式由旧数码确定新的第一分量，cons 像公式的向外读法则由 `envSet W k` 确定新的第二分量。把码化有序对等式应用于这两条同一视，便得到标准后继条目 `(# (suc k), envSet W (suc k))`。

```agda
    (λ { (p' , (p'∈ , hb)) → PT.rec (snd (pr (# (suc k)) (fst (envSet W (suc k))) ∈ Ev))
      (λ { (n' , F' , s' , (qp' , (hsuc , hci))) →
        let δ' = F' ∷ n' ∷ s' ∷ p' ∷ δ
        in subst (λ u → ⟨ u ∈ Ev ⟩)
             (qp' ∙ cong₂ pr (suc-out i5 i1 δ' hsuc)
```

归纳假设先给出第 `k` 个标准条目的隶属证明。把向上闭合应用于该条目，仅仅得到一个后继条目及其两个分量公式。向外读取这两个公式，会把相应分量识别为 `# (suc k)` 与 `envSet W (suc k)`；沿所得码化有序对等式运输，便证明标准后继条目属于塔。

```agda
                             (ConsImageRead.consImage-out i0 i4 (sh 8 w) δ' W qw k refl hci))
             p'∈ })
      (bothEx-out i0 (upBody w) (p' ∷ δ) hb) })
    (useBoth i0 (pS ∷ γ) (nn k) (envSet W k) refl (towerUp E w) (hup pS (entry-in k)))
    where
```

为调用向上闭合，先把第 `k` 个标准条目呈现为载体元素 `pS`。其容器向有界量词暴露两个分量，四槽环境则依次记录当前环境集、数码、容器与塔条目。

```agda
    pS : S
    pS = down (lookup E γ) (pr (# k) (fst (envSet W k))) (entry-in k)
    c = container pS (nn k) (envSet W k) refl
    δ : S ^ (4 + m)
    δ = envSet W k ∷ nn k ∷ c .fst ∷ pS ∷ γ
```

塔持有模块假定候选塔已通过底层集合等式与真实塔等同，此外还有载体与数码等式。所有结论都相对于这些等同。

```agda
module TowerHolds {m : ℕ} (E w N0 : Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (qE : fst (lookup E γ) ≡ fst (Tower.tower W))
  (qN0 : fst (lookup N0 γ) ≡ # 0) where
  private
    Ev = fst (lookup E γ)
```

每条标准条目属于候选塔，方法是把真实塔的向内读式沿等同等式运输。

```agda
    entry∈ : (k : ℕ) → ⟨ pr (# k) (fst (envSet W k)) ∈ Ev ⟩
    entry∈ k = subst (λ u → ⟨ pr (# k) (fst (envSet W k)) ∈ u ⟩) (sym qE) (Tower.tower-in′ W k)
```

每条标准条目沿其在候选塔中的隶属下降而呈现为载体元素。

```agda
    entryS : (k : ℕ) → S
    entryS k = down (lookup E γ) (pr (# k) (fst (envSet W k))) (entry∈ k)
```

候选塔的每个成员都被读作标准条目，方法是把隶属运入真实塔并应用塔的向外读法。

```agda
    read : (p : S) → ⟨ fst p ∈ Ev ⟩ → ∥ Σ[ k ∈ ℕ ] (fst p ≡ pr (# k) (fst (envSet W k))) ∥₁
    read p p∈ = Tower.tower-out W p (subst (λ u → ⟨ fst p ∈ u ⟩) qE p∈)
```

塔持有结论是三个子句的三元组：基项子句、向上闭合子句与向下分解子句。基项子句的证明：呈现第零条标准条目及其隶属。

```agda
  holds : ⟨ γ ⊨ towerAt E w N0 ⟩
  holds = hbase , (hup , hdown)
    where
    hbase : ⟨ γ ⊨ ∃̇∈ (var E) (sndEx i0 (sh 1 N0) (sglEmpty i0)) ⟩
    hbase = ∣ entryS 0 , ( entry∈ 0
```

第零条目以其数码等式、其隶属以及施于所呈现环境的单点空集向内读式填充。数码等式从候选零数码槽运输而来。

```agda
      , fillSnd i0 (entryS 0 ∷ γ) (lookup N0 γ) (envSet W 0)
          (cong (λ a → pr a (fst (envSet W 0))) (sym qN0))
          (sglEmpty i0)
          (SglEmpty.sglEmpty-in W i0
            (envSet W 0 ∷ container (lookup i0 (entryS 0 ∷ γ)) (lookup N0 γ) (envSet W 0)
```

基条目子句至此完成。其见证是典范条目 `entryS 0`，该条目属于 `E` 是由 `E` 与已构造环境塔的对齐得到的。等式 `qN0` 把第一分量与指定的零数码槽位对齐，而 `SglEmpty.sglEmpty-in` 把第二分量识别为只含空环境的单点集。因此，所需的基条目在命题截断下存在。

```agda
               (cong (λ a → pr a (fst (envSet W 0))) (sym qN0)) .fst ∷ entryS 0 ∷ γ) refl)
          (sh 1 N0) refl ) ∣₁
```

为证明向上闭合，固定 `E` 的一个条目 `p`，并考虑传给 `bothAll-in` 的任意码化有序对表示 `p = (n,F)`。读式 `read p p∈` 在命题截断下断言：对某个 `k`，`p` 是典范条目 `(# k, envSet W k)`。码化有序对的单射性随即把 `n` 与 `# k`、`F` 与 `envSet W k` 分别识别。因而，该论证恰好使用 `towerAt` 所控制的码化有序对接口。

```agda
    hup : (p : S) → ⟨ fst p ∈ Ev ⟩ → ⟨ (p ∷ γ) ⊨ bothAll i0 (towerUp E w) ⟩
    hup p p∈ = bothAll-in i0 (towerUp E w) (p ∷ γ) (λ n F s s∈ n∈ F∈ e →
      PT.rec (snd ((F ∷ n ∷ s ∷ p ∷ γ) ⊨ towerUp E w))
        (λ { (k , qp) →
          let q = pr-inj (sym e ∙ qp)
```

下一个典范条目由 `entryS (suc k)` 属于 `E` 的证明取得。环境 `δ1` 同时记录该条目以及当前条目的分量 `F` 与 `n`；随后，`container` 提供有界容器，使新有序对的数码分量与环境集分量可由公式访问。再延拓一次得到 `δ2`，便把典范后继数码与 `envSet W (suc k)` 放入 `upBody` 所需的槽位。

```agda
              δ1 = entryS (suc k) ∷ F ∷ n ∷ s ∷ p ∷ γ
              c' = container (lookup i0 δ1) (nn (suc k)) (envSet W (suc k)) refl
              δ2 = envSet W (suc k) ∷ nn (suc k) ∷ c' .fst ∷ δ1
          in ∣ entryS (suc k) , ( entry∈ (suc k)
             , fillBoth i0 δ1 (nn (suc k)) (envSet W (suc k)) refl (upBody w)
```

此时，`upBody` 的两个合取支分别表达两种后继步骤。`sucAtL` 的引入引理把第一分量的等式经 `sucV` 搬运，从而将 `# (suc k)` 与新的数码槽位联系起来。另一方面，`ConsImageRead.consImage-in` 使用第二分量的等式、对齐 `w = W` 以及 `consAtL` 的充分性，证明 `envSet W (suc k)` 恰是 `envSet W k` 的 cons 像。这些证明产出一个截断的后继条目见证；再把 `read` 的截断结果消去到这个满足命题中，便对每个条目建立了向上闭合。

```agda
                 ( suc-in i5 i1 δ2 (cong sucV (sym (q .fst)))
                 , ConsImageRead.consImage-in i0 i4 (sh 8 w) δ2 W qw k (q .snd) refl ) ) ∣₁ })
        (read p p∈))
```

向下分解以同样的方式开始：固定条目 `p`，取其任意码化有序对表示 `p = (n,F)`，并且只在命题截断允许的范围内使用 `read`。所得见证给出某个自然数 `k`，使 `p = (# k, envSet W k)`。对该见证中的 `k` 作模式匹配，便分成 `k = 0` 与 `k = suc j` 两种情形，它们恰好对应 `towerDown` 的两个析取支。

```agda
    hdown : (p : S) → ⟨ fst p ∈ Ev ⟩ → ⟨ (p ∷ γ) ⊨ bothAll i0 (towerDown E w N0) ⟩
    hdown p p∈ = bothAll-in i0 (towerDown E w N0) (p ∷ γ) (λ n F s s∈ n∈ F∈ e →
      PT.rec (snd ((F ∷ n ∷ s ∷ p ∷ γ) ⊨ towerDown E w N0))
        (λ { (zero , qp) →
          let q = pr-inj (sym e ∙ qp)
```

若 `k` 为零，码化有序对的单射性便把 `n` 与 `# 0`、`F` 与 `envSet W 0` 分别识别。第一条等式与 `qN0` 合成，证明所记录的数码就是指定的零数码；`SglEmpty.sglEmpty-in` 则把第二条等式转成只含空环境的单点集条件。这就建立了左析取支。若 `k = suc j`，同一单射性转而恢复前驱索引及其环境集；接下来的环境为右析取支准备见证。

```agda
          in ∣ inl (q .fst ∙ sym qN0 , SglEmpty.sglEmpty-in W i0 (F ∷ n ∷ s ∷ p ∷ γ) (q .snd)) ∣₁
           ; (suc j , qp) →
          let q = pr-inj (sym e ∙ qp)
              δ1 = entryS j ∷ F ∷ n ∷ s ∷ p ∷ γ
              c' = container (lookup i0 δ1) (nn j) (envSet W j) refl
```

在后继情形中，`entryS j` 给出 `E` 内的典范前驱条目。`sucAtL` 的引入引理使用第一分量的等式，证明当前数码是前驱数码的后继。随后，`ConsImageRead.consImage-in` 使用 `w = W` 与第二分量的等式，证明当前环境集是前驱环境集的 cons 像。把该前驱条目与这两个事实打包，便得到右析取支所需的截断见证。

```agda
              δ2 = envSet W j ∷ nn j ∷ c' .fst ∷ δ1
          in ∣ inr ∣ entryS j , ( entry∈ j
             , fillBoth i0 δ1 (nn j) (envSet W j) refl (downBody w)
                 ( suc-in i1 i5 δ2 (q .fst)
                 , ConsImageRead.consImage-in i4 i0 (sh 8 w) δ2 W qw j refl (q .snd) ) ) ∣₁ ∣₁ })
```

把 `read` 的截断结果消去到满足命题中，便对真实环境塔的每个成员完成向下分解。结合基项与向上闭合子句可知：只要 `E`、`w`、`N0` 分别与 `Tower.tower W`、`W`、`# 0` 对齐，`towerAt E w N0` 就得到满足。该结论证明真实环境塔满足其有界描述，同时保留公式只控制码化有序对接口这一边界。

```agda
        (read p p∈))
```

## 回顾

环境塔现在具备后文所需的两种形式：一方面，它是一个实际的可构造集合，其成员恰为标准有序对 `(# n, envSet W n)`；另一方面，它有一条 Δ₀ 公式，可逐个相邻元数读取和生成这些码化有序对条目。两个方向使用不同的归纳：读取条目时以隶属归纳排除无穷下降，生成全部标准条目时则对自然数作普通归纳。恢复出的元数与分解始终留在命题截断之下，而该公式不对任意候选集合中可能存在的非有序对成员作出断言。