---
title: "可构造层级与可构造宇宙"
module: L.Constructible
lang: zh
site: "Bedrock"
description: "可构造层级与可构造宇宙"
stage: "可构造层与公理"
reading_order: 25
canonical: https://bedrock.institute/zh/L.Constructible.html
html: L.Constructible.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Constructible.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Model, L.Definability]
routes: [constructible-axioms]
translations: [https://bedrock.institute/en/L.Constructible.md, https://bedrock.institute/ja/L.Constructible.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 可构造层级与可构造宇宙

可构造层级从空集开始，反复施加可定义幂集，并在极限点处取并。所得层都是传递集，而塔沿指标之间的隶属关系保持单调；出现在某一层中的集合构成类 `L`，连同把环境结构限制到其上所得的集合论结构。

一个设计选择承担了大部分工作。塔的索引不是另立的序数类型，而是**集合自身**，凭借正则性所授权的沿成员关系的递归：`Lset α = ⋃ { Def (Lset β) ∣ β ∈ α }`。这一条方程同时覆盖零、后继与极限，而在冯·诺伊曼序数上它恰是哥德尔的塔；定义本身接受任意集合作为索引，索引须为序数的要求留到定义类 `L` 时才施加。与之并行的是归纳谓词 `isLayer`，「是一个层」，其构造子就是塔的闭包原则；两个视角在全章配合使用。

本章在固定的宇宙层级 `ℓ` 上、累积层级 V 内工作。其载体 `S` 由带有外延且良基隶属关系的集合组成。相应结构把相等与隶属读作命题值关系，因此 `⟨ x ∈ˢ A ⟩` 这样的表达式表示通常的隶属证明类型。下文的构造都在这个环境中进行。

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

open import Base.Prelude

module L.Constructible {ℓ : Level} where

open import FOL.ZFStructure using ( ZFStructure; _↾_; module hPropStructure; Transitive )
```

推动构造的数学素材有三。其一是沿成员关系的良基递归：层级章的原理 `∈-induction` 允许沿 `∈ˢ` 递归地定义集合上的函数，塔本身正是这样定义的。其二是索引族的并，以及从两个方向读取这种并中隶属关系的两条模型引理。其三是可定义性章的算子 `Def A`，它收集在内层世界 `(A, ∈)` 中、由 `A` 中参数定义出的 `A` 的子集；逐层施加它，正是层级向上生长的动力。一阶公式的语法，尤其是类型 `Formula`，正是为这个算子而从语法章沿用的。

```agda
open import FOL.Syntax using ( Formula )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; ∈-induction-compute )
open import V.Model {ℓ} using ( union-family-in; union-family-out )
open import L.Definability {ℓ} using ( module DefOf )

open import Cubical.Foundations.HLevels using ( isProp× )
```

层级中的集合由一个小族来表现，本章正是通过这种表现读取成员：对集合 `α`，`⟪ α ⟫` 是其成员的小索引类型，`⟪ α ⟫↪` 把索引嵌回集合，`∈ₛ⟪ α ⟫↪ m` 证明 `m` 所指名的成员属于 `α`。桥梁 `∈∈ₛ` 在两个方向上连接层级自身的成员关系 `∈` 与结构成员关系 `∈ˢ`；`sett X f` 构造以 `f` 在 `X` 上取值为成员的集合。与之相伴，命题截断 `∥ _ ∥₁` 及其引入 `∣ _ ∣₁` 给出「仅仅存在」：截断陈述的一个证明断言存在某个见证，而不指名它。

```agda
import Cubical.Data.Empty as Empty
import Cubical.Data.Sum as Sum
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
```

基本构造连同隶属刻画一并可用：空集配 `∅-empty`，无序配对配 `pairing-ax`，二元并与索引族并配 `union-ax`。层级 `ℓ-suc ℓ` 上的命题直接充当真值，而把环境结构 `𝒮ᵥ` 经 `hPropStructure` 展开，便得到记号 `⟨ _ ⟩` 取命题的底层类型、`∈ˢ` 表示结构成员关系。本章的每个陈述都在这个命题值设定中表述。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; ⁅_,_⁆; pairing-ax; ⋃_; union-ax; _∪_ )
```

设定就位后，可定义幂集算子得到它的工作名：`𝒟 A` 恰是可定义性章中的 `Def A`，即在限制结构上、由 `A` 中有限多个参数定义的 `A` 的子集之集。该算子的数学内容，包括其成员都是 `A` 的子集、以及传递集满足 `A ⊆ 𝒟 A`，均已在彼处建立；这里只是赋予全书通用的短记号。

```agda
open hPropStructure 𝒮ᵥ

𝒟 : S → S
𝒟 A = DefOf.Def A
```

## 传递集

层级的每层都是传递的：空集传递，可定义幂集保持传递性，传递集之并仍然传递。这些封闭性事实与构造层所用的构造子逐一对应。

(`𝒟` 是上一章 `Def` 在本书中的短记号，沿用这个算子惯用的花体字母。)

集合 `A` 传递，指 `A` 的成员的成员仍是 `A` 的成员。定义 `isTransV` 把结构层面的闭合条件 `Transitive 𝒮ᵥ` 实例化到「等于 `A` 的集合」这个类上，故 `isTransV A` 的证明字面上就是一个函数：从 `y ∈ˢ x` 与 `x ∈ˢ A` 给出 `y ∈ˢ A`。注意宇宙层级：该陈述对载体做了量化，故位于 `ℓ-suc ℓ`。传递性是一个命题，`isPropIsTransV` 直接证明这一点：给定两个证明 `p` 与 `q`，其结论 `y ∈ˢ A` 按构造是命题，故逐点相等，而立方版的函数外延性把逐点一致组装成 `p` 与 `q` 之间的路径。最后一行宣布第一条封闭性事实，关于空集。

```agda
isTransV : S → Type (ℓ-suc ℓ)
isTransV A = Transitive 𝒮ᵥ (λ x → x ∈ˢ A)

isPropIsTransV : (A : S) → isProp (isTransV A)
isPropIsTransV A p q i {x} {y} y∈x x∈A = (y ∈ˢ A) .snd (p y∈x x∈A) (q y∈x x∈A) i

∅-trans : isTransV ∅
```

空集情形是空洞的：从 `x ∈ˢ ∅` 经 `∈∈ₛ` 提取 `∅` 的原生成员，`∅-empty` 由此导出荒谬，故任何到达 `y ∈ˢ A` 的蕴涵都成立。对可定义幂集，前一章的两条引理合用。`𝒟 A` 的成员 `x` 是可定义子集，故 `y ∈ x` 迫使 `y ∈ A` (`Def∋⊆A`)；把传递性假设 `Atr` 用于此，传递集满足 `A ⊆ 𝒟 A` (`A⊆Def`)，从而 `y` 进入 `𝒟 A`。最后 `⋃-trans` 陈述并原理：若 `x` 的每个成员都传递，则 `⋃ x`，即 `x` 的成员之成员的全体，也传递。

```agda
∅-trans {x} y∈x x∈∅ = Empty.rec (∅-empty x (∈∈ₛ {a = x} {b = ∅} .fst x∈∅))

𝒟-trans : ∀ {A} → isTransV A → isTransV (𝒟 A)
𝒟-trans {A} Atr {x} {y} y∈x x∈𝒟A =
  DefOf.Refine.A⊆Def A Atr y (DefOf.Def∋⊆A A x x∈𝒟A y y∈x)

⋃-trans : (x : S) → ((y : S) → ⟨ y ∈ˢ x ⟩ → isTransV y) → isTransV (⋃ x)
```

要看并的一个成员，必须先看它究竟是不是成员。假设 `u∈⋃x` 是环境层级中的成员关系；`∈∈ₛ` 的第二方向把它转换成截断的纤维形式，而 `union-ax` 刻画这种隶属：`u ∈ ⋃ x` 仅仅当某个 `w ∈ x` 满足 `u ∈ w`。截断不可省略：公理并不指名中间的 `w`，只断言其存在。故证明在截断内部做映射，而在给出对 `w , (w∈ₛx , u∈ₛw)` 的分支里，两次 `∈∈ₛ` 从纤维数据恢复出可用的假设 `w∈x` 与 `u∈w`。

```agda
⋃-trans x mem {u} {v} v∈u u∈⋃x =
  ∈∈ₛ {a = v} {b = ⋃ x} .snd (union-ax x v .snd
    (PT.map
      (λ { (w , (w∈ₛx , u∈ₛw)) →
        let w∈x = ∈∈ₛ {a = w} {b = x} .snd w∈ₛx
```

在该分支中，假设 `mem w w∈x` 说 `w` 传递，故 `v ∈ u` 与 `u ∈ w` 给出 `v ∈ w`；再用第一方向的 `∈∈ₛ` 转换，这些数据成为 `union-ax` 合法的纤维，而截断消去合法，因为目标，即 `v` 属于 `⋃ x`，是命题。二元并随之得到：`A ∪ B` 定义为 `⋃ ⁅ A , B ⁆`，故 `∪-trans` 就是把 `⋃-trans` 用于这个配对，剩余的义务是配对的每个成员都传递，而这正是局部陈述 `prem` 要供给的。

```agda
            u∈w = ∈∈ₛ {a = u} {b = w} .snd u∈ₛw
        in w , (w∈ₛx , ∈∈ₛ {a = v} {b = w} .fst (mem w w∈x v∈u u∈w)) })
      (union-ax x u .fst (∈∈ₛ {a = u} {b = ⋃ x} .fst u∈⋃x))))

∪-trans : ∀ {A B} → isTransV A → isTransV B → isTransV (A ∪ B)
∪-trans {A} {B} tA tB = ⋃-trans ⁅ A , B ⁆ prem
```

义务 `prem` 问的是：配对中的每个 `y` 是否传递？配对的隶属刻画是「仅仅」式的：`y ∈ ⁅ A , B ⁆` 仅仅当 `y` 是 `A` 或 `y` 是 `B`，由命题截断给出，而非选定的析取支。消去的目标是命题 `isTransV y`，每个分支携带一条等式 `p` 把 `y` 与 `A` 或 `B` 等同；由于传递性在集合相等下不变，`subst isTransV (sym p)` 沿这条等式把已知的 `tA` 或 `tB` 传送到类型 `isTransV y`。

```agda
  where
  prem : (y : S) → ⟨ y ∈ˢ ⁅ A , B ⁆ ⟩ → isTransV y
  prem y y∈ = PT.rec (isPropIsTransV y)
    (λ { (Sum.inl p) → subst isTransV (sym p) tA
       ; (Sum.inr p) → subst isTransV (sym p) tB })
```

`prem` 的末行把截断的隶属经 `pairing-ax` 送入上述情形分析，情形分析完成，二元情形随之完成。族形式 `setUnion-trans` 一次处理小的索引族：给定类型 `X : Type ℓ` 与函数 `f : X → S`，集合 `sett X f` 的成员是取值 `f x`，而每个 `f x` 由假设传递。这里对索引集合的成员同样是截断的：证明收到的是对 `x , fx≡y`，即一个索引连同把取值与 `y` 等同的路径。

```agda
    (pairing-ax A B y .fst (∈∈ₛ {a = y} {b = ⁅ A , B ⁆} .fst y∈))

setUnion-trans : (X : Type ℓ) (f : X → S) → ((x : X) → isTransV (f x))
               → isTransV (⋃ (sett X f))
setUnion-trans X f hf = ⋃-trans (sett X f)
  (λ y → PT.rec (isPropIsTransV y)
```

传输再次承担簿记：`subst isTransV fx≡y (hf x)` 沿等同把 `f x` 的传递性证明移到 `y` 上，而截断消去合法，因为 `isTransV y` 是命题。有了这些封闭性原则，空集、可定义幂集、以及一般、二元、索引三种形式的并，下文证明每个层都传递的归纳就成了一行分发：每个构造子对应这里证明的相应引理。

```agda
    (λ { (x , fx≡y) → subst isTransV fx≡y (hf x) }))
```

## 序数，仅取谓词

对可构造层级真正起作用的索引是冯·诺伊曼序数，而在良基、外延的宇宙里，经典定义所剩无几：**序数**就是由传递集组成的传递集。良基与外延无须写进定义，层级处处保证它们成立；线序则是留待后文的经典定理，不属于概念本身。本章记录这个谓词及其命题性；序数的理论待需要时另章展开。

因此，`IsOrd A` 是两个命题的合取：`A` 是传递集，而且 `A` 的每个成员都是传递集。证明 `isPropIsOrd A` 利用命题在积与依值函数下的封闭性，把两个分量的命题性合并起来。`isL` 的定义会显式使用这份证书，其中 `(IsOrd α , isPropIsOrd α)` 给出「层指标是序数」这一真值。

```agda
IsOrd : S → Type (ℓ-suc ℓ)
IsOrd A = isTransV A × ((x : S) → ⟨ x ∈ˢ A ⟩ → isTransV x)

isPropIsOrd : (A : S) → isProp (IsOrd A)
isPropIsOrd A = isProp× (isPropIsTransV A)
                  (isPropΠ λ x → isPropΠ λ _ → isPropIsTransV x)
```

## 层

`isLayer A` 用五个构造子记录塔的封闭性：空集是层；对一层应用 `𝒟` 仍得到层；并集则有三种形式，分别来自成员全是层的集合、两个层以及层的小指标族。要证明每个层都具有某性质时，可用的归纳情形正是这五种。特别地，每个情形都对应上一节的一条传递性引理。

这个谓词是以载体为索引的归纳族，其构造子被读作层的生成规则。基底说空集是层。对 `𝒟` 的闭包说：若 `A` 是层，则其可定义幂集也是层，对应后继步骤。一般并构造子对应极限步骤：若 `x` 的成员全部、以不加截断的方式是层，则 `⋃ x` 是层。二元并构造子直接从 `A` 与 `B` 的层见证覆盖 `A ∪ B`。每个构造子对应上一节的一条传递性引理，只是把 `isTransV` 换成 `isLayer`；正是这种平行性使下一条证明变得直接。

```agda
data isLayer : S → Type (ℓ-suc ℓ) where
  ∅-layer        : isLayer ∅
  𝒟-layer        : ∀ {A} → isLayer A → isLayer (𝒟 A)
  union-layer    : (x : S) → ((y : S) → ⟨ y ∈ˢ x ⟩ → isLayer y) → isLayer (⋃ x)
  union₂-layer   : ∀ {A B} → isLayer A → isLayer B → isLayer (A ∪ B)
```

小索引族构造子补全全图：对类型 `X : Type ℓ` 与族 `f : X → S`，若所有取值都是层，则并 `⋃ (sett X f)` 是层。极限层正是经由这个构造子从更早层的族组装出来。接下来是归纳：要证 `layer-trans`，即每层都传递，层以归纳参数的形式给出，情形由其构造子决定。空集情形逐字就是 `∅-trans`。`𝒟` 情形应用 `𝒟-trans`，其前提正是对子层的归纳假设 `layer-trans lA`。

```agda
  setUnion-layer : (X : Type ℓ) (f : X → S)
                 → ((x : X) → isLayer (f x)) → isLayer (⋃ (sett X f))

layer-trans : ∀ {A} → isLayer A → isTransV A
layer-trans ∅-layer = ∅-trans
layer-trans (𝒟-layer {A} lA) = 𝒟-trans {A} (layer-trans lA)
```

三种并的情形同样直接分发。一般并情形把逐成员的归纳假设交给 `⋃-trans`：该引理要求对 `x` 的每个成员 `y` 给出 `y` 的传递性证明，而构造子前提 `mem` 恰好不加截断地供给，故无需消去截断。二元情形是对两个归纳假设应用 `∪-trans`。族情形是带逐点归纳假设的 `setUnion-trans`。于是本节仅凭结构递归就确立了塔的每层都是传递集，本章稍后证明类 `L` 的传递性时正要用到这一事实。

```agda
layer-trans (union-layer x mem) = ⋃-trans x (λ y y∈x → layer-trans (mem y y∈x))
layer-trans (union₂-layer lA lB) = ∪-trans (layer-trans lA) (layer-trans lB)
layer-trans (setUnion-layer X f hf) = setUnion-trans X f (λ x → layer-trans (hf x))
```

## 塔

现在构造塔本身，沿成员关系递归。先做两项技术处理：`𝒟` 的展开是公式上较大的 `sett`，递归机制自身又会展开成可及性消去子，若不加遮蔽，二者都会进入后续的转换；`opaque` 让 `𝒟ₒ` 与塔成为黑箱，只在显式展开它们的块内打开，`Lset-compute` 则作为塔的被声明展开式。步进取索引 `α` 的成员 `β`，`𝒟ₒ` 作用于递归值再取并；计算规则作为命题路径成立。

算子先在 `opaque` 块内被重新包装为 `𝒟ₒ`，使 `Def` 精细的定义保持隐藏，除非某条引理显式要求展开。步进函数 `LsetStep` 接收索引集 `α`，以及对 `α` 的每个成员 `β` 的递归值 `rec β`；这里的成员关系经由 `∈ᵗ`，即结构成员命题的取类型读法出现。函数体构造一个族：把小索引 `m : ⟪ α ⟫` 映到 `𝒟ₒ` 作用于 `m` 所指名成员 `⟪ α ⟫↪ m` 处递归值的结果，再取其并。沿索引类型展开这个并，其意读恰好是 `⋃ { 𝒟ₒ (Lset β) ∣ β ∈ α }`，一条方程同时服务零、后继与极限：`α` 为空时并为空，后继时重复经典的下一步，极限时一次收齐所有更早层。

```agda
opaque
  𝒟ₒ : S → S
  𝒟ₒ A = 𝒟 A

LsetStep : (α : S) → (∀ β → β ∈ᵗ α → S) → S
LsetStep α rec = ⋃ (sett ⟪ α ⟫ (λ m → 𝒟ₒ (rec (⟪ α ⟫↪ m) (mem m))))
```

辅助引理 `mem` 提供函数体所需的转换：索引 `m` 指名的 `α` 的成员是 `⟪ α ⟫↪ m`，`∈ₛ⟪ α ⟫↪ m` 证明这个集合在小表示中属于 `α`；`∈∈ₛ` 再把它转换为 `rec` 所期望的取类型成员关系 `∈ᵗ`。塔本身随之只是一次调用：`Lset` 定义为 `∈-induction` 作用于步进函数。这是沿成员关系的良基递归，其正当性由层级章的正则性定理一次性给出；递归索引就是集合 `α` 自身，原始定义不要求索引是序数，序数性只在使用层级之处施加。

```agda
  where
  mem : (m : ⟪ α ⟫) → ⟪ α ⟫↪ m ∈ᵗ α
  mem m = ∈∈ₛ {a = ⟪ α ⟫↪ m} {b = α} .snd (∈ₛ⟪ α ⟫↪ m)

opaque
  Lset : S → S
```

`𝒟ₒ` 与 `Lset` 各自被包在 `opaque` 块中，二者的 Agda 项在类型检查期间保持抽象；递归机制内部，即某个可及性消去子，展开出的一切都不会泄漏到后续的转换中。取代盲目展开的是一条被声明的计算规则：`Lset-compute` 以命题路径陈述 `Lset α` 等于把步进函数作用于 `α` 与递归值 `λ β _ → Lset β` 的结果。这正是层级章的 `∈-induction-compute` 在该步进上的实例化；该等式未必定义性成立，而显式陈述它，使后续证明得以按这一条受控的等式改写 `Lset α`，而不必打开递归机制。

```agda
  Lset = ∈-induction LsetStep

opaque
  unfolding Lset
  Lset-compute : (α : S) → Lset α ≡ LsetStep α (λ β _ → Lset β)
  Lset-compute = ∈-induction-compute LsetStep
```

塔的每个值都是层：先用 `Lset-compute` 展开一次，对每个成员应用归纳假设，再经 `𝒟ₒ-layer` 升一层 (不透明定义只在此处展开)，最后用 `setUnion-layer` 证明族的并仍是层。

从算子到谓词的桥只花一行。在展开 `𝒟ₒ` 的块内，陈述 `𝒟ₒ-layer` 字面上就是构造子 `𝒟-layer`，因为 `𝒟ₒ A` 化归为 `𝒟 A`；这是全章唯一需要查看不透明包装内部之处，此后对算子的每个使用都可保持抽象。目标 `Lset-layer` 随之说塔完全落在归纳谓词之内：每层 `Lset α` 都是层。其证明本身又是一次成员归纳的应用，即定义塔的那条同一原理。

```agda
opaque
  unfolding 𝒟ₒ
  𝒟ₒ-layer : ∀ {A} → isLayer A → isLayer (𝒟ₒ A)
  𝒟ₒ-layer = 𝒟-layer

Lset-layer : (α : S) → isLayer (Lset α)
```

这次归纳的步进函数接收 `α` 与归纳假设 `IH`，后者对 `α` 的每个成员 `β` 给出 `Lset β` 是层的证明。由于 `Lset` 不透明，目标 `isLayer (Lset α)` 无法直接与构造子匹配；必须先做传输。等式 `Lset-compute α` 把 `Lset α` 与步进的并等同，`subst isLayer (sym (Lset-compute α))` 沿该路径把目标移到正确方向，于是目标变为 `isLayer (⋃ (sett ⟪ α ⟫ (λ m → 𝒟ₒ (Lset (⟪ α ⟫↪ m)))))`，恰好是塔的步进函数所构造的那个族。

```agda
Lset-layer = ∈-induction step
  where
  step : (α : S) → (∀ β → β ∈ᵗ α → isLayer (Lset β)) → isLayer (Lset α)
  step α IH = subst isLayer (sym (Lset-compute α))
    (setUnion-layer ⟪ α ⟫ (λ m → 𝒟ₒ (Lset (⟪ α ⟫↪ m)))
```

剩余义务与族构造子严丝合缝：`setUnion-layer` 要求族以及每个取值的层证明。对索引 `m`，取值是 `𝒟ₒ` 作用于 `Lset (⟪ α ⟫↪ m)` 的结果，而归纳假设 `IH` 在该成员处应用、经局部辅助 `mem` 转换为取类型成员关系后，给出 `isLayer (Lset (⟪ α ⟫↪ m))`；`𝒟ₒ-layer` 再把它提升一个可定义幂集步。`Lset` 的不透明包装只经由被声明的等式打开，`𝒟ₒ` 的不透明包装只在 `𝒟ₒ-layer` 内部打开，故整个归纳都在塔的意读层面运行。结合上一节，每层都是传递的层。

```agda
      (λ m → 𝒟ₒ-layer (IH (⟪ α ⟫↪ m) (mem m))))
    where
    mem : (m : ⟪ α ⟫) → ⟪ α ⟫↪ m ∈ᵗ α
    mem m = ∈∈ₛ {a = ⟪ α ⟫↪ m} {b = α} .snd (∈ₛ⟪ α ⟫↪ m)
```

## 层之间的比较

关于塔还有两个事实。第一条给算子的隶属命名：`𝒟ₒ A` 就是 `A` 的可定义子集之集，故属于它按构造即「仅仅是某个 `defSet φ`」；要把一个集合放进算子里，拿出一条公式连同一个外延等式恰好就够。第二条把塔展开一次，从两个方向读那个并：一层是其索引的成员对更早诸层的 `𝒟ₒ` 取的并，故属于一层恰是属于某个更早层的 `𝒟ₒ`；这条刻画按两个独立方向给出。单调性随之作为推论得到，而非另行构造。

在展开 `𝒟ₒ` 的块内，属于 `𝒟ₒ A` 化归为 `Def` 的定义性质：`𝒟ₒ A` 的成员是由一条元数为 1 的公式、在 `A` 的小成员上选出的 `A` 的子集，而实际的集合由路径 `DefOf.defSet A φ ≡ x` 指认。由于环境层级中的成员关系是截断的，陈述冠以命题截断：所断言的只是这样的公式存在，而非选定了某条。下面两条引理把这条等价各按一个方向陈述；这里宣告的是进入方向，把截断的定义数据变成隶属。

```agda
opaque
  unfolding 𝒟ₒ
  𝒟ₒ-intro : (A x : S)
           → ∥ Σ[ φ ∈ Formula ⟪ A ⟫ 1 ] (DefOf.defSet A φ ≡ x) ∥₁
           → ⟨ x ∈ˢ 𝒟ₒ A ⟩
```

证明在两个方向上都是恒等：`𝒟ₒ` 一旦展开，截断定义数据的一个元素本来就是成员，反之，反演引理 `𝒟ₒ-inv` 把一个隶属作为同样的截断数据返回。于是 `𝒟ₒ-intro` 与 `𝒟ₒ-inv` 这一对恰是上文描述的接口：把一层处的 `DefOf.defSet` 读作从公式出发的映射，用反演恢复成员的定义公式。二者都在「仅仅存在」的层面工作，因此从不选定任何典范公式；`𝒟ₒ A` 的成员仅仅是某个可定义子集，这两条方向所说的也仅止于此。

```agda
  𝒟ₒ-intro A x p = p

  𝒟ₒ-inv : (A x : S) → ⟨ x ∈ˢ 𝒟ₒ A ⟩
         → ∥ Σ[ φ ∈ Formula ⟪ A ⟫ 1 ] (DefOf.defSet A φ ≡ x) ∥₁
  𝒟ₒ-inv A x p = p
```

关于塔还有两个事实，承载着后续诸章的每一个闭包论证，而只要在对的地方开封，二者都很廉价。第一条给算子的隶属命名：`𝒟ₒ A` 就是 `A` 的可定义子集之集，故属于它按构造即「仅仅是某个 `defSet φ`」；要把一个集合放进算子里，拿出一条公式连同一个外延等式恰好就够。第二条把塔展开一次，从两个方向读那个并：一层是其索引的成员对更早诸层的 `𝒟ₒ` 取的并，故属于一层恰是属于某个更早层的 `𝒟ₒ`；这条刻画按两个独立方向给出，因为证明正是这样使用它。单调性随之作为推论得到，而非另行构造。

第一条引理是层包含于其自身的可定义幂集：由于 `Lset-layer β` 说层 `Lset β` 是层，而 `layer-trans` 使其传递，可定义性章的精化界 `A⊆Def` 逐字适用，给出 `x ∈ Lset β ⟹ x ∈ 𝒟ₒ (Lset β)`。其对偶 `𝒟ₒ∋⊆` 重申算子只精化不扩缩：`𝒟ₒ A` 的每个成员都是 `A` 的子集，故成员的成员仍在 `A` 中。最后 `stageFam` 为塔的步进下的族命名：对 `α` 的小表示中的索引 `m`，对应的层是 `𝒟ₒ` 作用于 `m` 所指名成员处的 `Lset`。

```agda
  Lset⊆𝒟ₒ : (β x : S) → ⟨ x ∈ˢ Lset β ⟩ → ⟨ x ∈ˢ 𝒟ₒ (Lset β) ⟩
  Lset⊆𝒟ₒ β x = DefOf.Refine.A⊆Def (Lset β) (layer-trans (Lset-layer β)) x

  𝒟ₒ∋⊆ : (A x : S) → ⟨ x ∈ˢ 𝒟ₒ A ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ A ⟩
  𝒟ₒ∋⊆ A = DefOf.Def∋⊆A A

stageFam : (α : S) → ⟪ α ⟫ → S
```

现在从上方刻画层隶属。`Lset-in` 说：若 `δ` 是 `α` 的成员且 `x` 落在 `𝒟ₒ (Lset δ)` 中，则 `x` 已经落在 `Lset α` 中。证明先用计算规则改写 `Lset α` 一次，使目标变为并 `⋃ (sett ⟪ α ⟫ (stageFam α))` 的隶属，然后调用 `union-family-in`，即模型章的引理：它接收索引 `i` 与 `f i` 的成员 `x`，返回索引并的成员。所供索引是 `fib .fst`，即 `⟪ α ⟫` 中指名成员 `δ` 的元素。

```agda
stageFam α m = 𝒟ₒ (Lset (⟪ α ⟫↪ m))

Lset-in : (α δ x : S) → ⟨ δ ∈ˢ α ⟩ → ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩ → ⟨ x ∈ˢ Lset α ⟩
Lset-in α δ x δ∈α x∈𝒟ₒδ =
  subst (λ w → ⟨ x ∈ˢ w ⟩) (sym (Lset-compute α))
    (union-family-in ⟪ α ⟫ (stageFam α) (fib .fst) x
```

名字 `fib` 缩写一次纤维计算：结构成员 `δ∈α` 是截断的，`∈-asFiber` 把它转换为嵌入 `⟪ α ⟫↪` 的纤维，即索引 `i` 与路径 `⟪ α ⟫↪ i ≡ δ` 组成的对。证明内部沿这条等同做传输：`x∈𝒟ₒδ` 谈的是 `Lset δ`，而 `union-family-in` 需要的是 `stageFam α (fib .fst)` 的成员，后者等于 `𝒟ₒ (Lset (⟪ α ⟫↪ (fib .fst)))`，故 `subst` 沿路径 `sym (fib .snd)` 把假设移过去。`δ∈α` 的截断来源在此无关紧要，因为 `∈-asFiber` 确实从它构造出了纤维表示。

```agda
      (subst (λ δ → ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩) (sym (fib .snd)) x∈𝒟ₒδ))
  where
  fib = ∈-asFiber {a = δ} {b = α} δ∈α

Lset-out : (α x : S) → ⟨ x ∈ˢ Lset α ⟩
         → ∥ Σ[ δ ∈ S ] (⟨ δ ∈ˢ α ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩) ∥₁
```

向下的方向 `Lset-out` 无法避开截断，并如实陈述：`Lset α` 的成员 `x` 仅仅来自某个前驱，即仅仅存在 `δ` 满足 `δ ∈ α` 与 `x ∈ 𝒟ₒ (Lset δ)`。证明同样先用计算规则改写 `Lset α`，对 `union-family-out` 的应用得到「仅仅」有 `⟪ α ⟫` 的索引 `m` 使 `x` 落在该索引处的族值中，再在截断内部做映射：对 `(m , hx)` 变为层 `⟪ α ⟫↪ m`、经 `∈∈ₛ` 的它在 `α` 中的结构隶属、以及 `hx`。结果是截断的见证，正是因为并公理不指名任何典范前驱；分支内构造出的那一个只是局部数据，而非选定的函数。

```agda
Lset-out α x x∈Lα = PT.map
  (λ { (m , hx) → ⟪ α ⟫↪ m
    , (∈∈ₛ {a = ⟪ α ⟫↪ m} {b = α} .snd (∈ₛ⟪ α ⟫↪ m) , hx) })
  (union-family-out ⟪ α ⟫ (stageFam α) x
    (subst (λ w → ⟨ x ∈ˢ w ⟩) (Lset-compute α) x∈Lα))
```

单调性由此成为刻画的不到三行的推论，而非另行构造。若 `β ∈ α` 且 `x ∈ Lset β`，先用 `Lset⊆𝒟ₒ` 把 `x` 提升到 `𝒟ₒ (Lset β)`，用到层传递；再以包含 `β ∈ α` 应用 `Lset-in`，把 `x` 送入 `Lset α`。注意其严格形式：单调性要求 `β` 是 `α` 的成员，而不仅是子集，这与塔沿成员取并的生长方式一致。

```agda
Lset-mono : {α β : S} → ⟨ β ∈ˢ α ⟩ → {x : S} → ⟨ x ∈ˢ Lset β ⟩ → ⟨ x ∈ˢ Lset α ⟩
Lset-mono {α} {β} β∈α {x} x∈Lβ = Lset-in α β x β∈α (Lset⊆𝒟ₒ β x x∈Lβ)
```

## 类 L，及其结构

一个集合是**可构造的**，指塔的某个序数层包含它。序数界故意写进定义：后文的理论要提取层序数，这个形状按构造直接给出。注意序数性正是在定义之处施加的；塔 `Lset` 本身接受任意集合作为索引。`L` 是传递类：层传递，见证序数不动。

这个类是一个真值，而非子类型：`isL x` 定义为对全体集合 `α` 的索引析取 `∃[ x ] P x`，其各项是 `IsOrd α` 与 `x ∈ˢ Lset α` 的合取。故按索引析取的含义，`isL x` 的一个元素仅仅是一个对：序数 `α` 与 `x` 属于层 `α` 的证据；可构造集并不附带一个典范层。量词遍历整个载体，故见证只以「仅仅存在」的形式可得；把类当作命题值谓词，正是稍后能把它限制成结构的原因。

```agda
isL : S → hProp (ℓ-suc ℓ)
isL x = ∃[ α ∶ S ] ((IsOrd α , isPropIsOrd α) ⊓ (x ∈ˢ Lset α))

isL-trans : Transitive 𝒮ᵥ isL
isL-trans {x} {y} y∈x x∈L = PT.rec (snd (isL y))
  (λ { (α , (ordα , x∈Lα)) →
```

类的传递性现在由层的闭包立即可得。给定 `y ∈ x` 与 `isL x` 的一个元素，向命题 `isL y` 消去截断：见证是对 `(α , ordα , x∈Lα)`，而层 `Lset α` 经 `layer-trans (Lset-layer α)` 是传递集，故两条假设 `y∈x` 与 `x∈Lα` 给出 `y ∈ Lset α`。同一个序数 `α` 重新为结论作证，故类对成员的成员封闭。结论再用 `∣ _ ∣₁` 重新截断，是因为目标 `isL y` 本身就是截断的存在式，而不是因为任何选择需要撤销。

```agda
    ∣ α , (ordα , layer-trans (Lset-layer α) y∈x x∈Lα) ∣₁ })
  x∈L
```

落在某个序数层中**就是**定义，故这个方向的桥就是构造子本身。给它一个名字，只是便于日后引用。

给定层 `α` 的序数见证 `oα` 与隶属 `x∈Lα`，证明把三个分量，序数、其序数性、隶属，打包成单个经命题截断的对。没有任何计算；该引理的内容在于：`isL x` 定义中的存在式恰好由手头的数据见证。注意信任的方向：引理把 `α` 的序数性作为假设接收，因为按定义 `Lset` 接受任意集合作为索引，所选索引确实是序数这一点必须由调用方知道。

```agda
Lset→isL : (α : S) → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ isL x ⟩
Lset→isL α oα x x∈Lα = ∣ α , (oα , x∈Lα) ∣₁
```

最后把可构造类看成一个结构。把 `𝒮ᵥ` 限制到命题值类 `isL` 上得到 `𝒮ʟ`：其元素是配有可构造性证明的集合，相等与隶属则从限制结构继承。这给出了后文解释关于 L 的公式所用的结构；要证明它是 ZFC 的模型，还需要随后各章分别给出的公理论证。

一行足矣。限制 `_↾_` 接收环境结构与类 `isL`，构成这样的结构：其元素是集合配上其满足 `isL` 的证明的对；等词与隶属沿第一投影读取，故与环境一致。由于 `isL` 是 `hProp` 中的真值、且该类已被证明传递，限制结构在同一框架中良定义。尚待解决、也是后续各章主题的，是这个结构是否满足 ZF 与 ZFC 公理；限制本身对此不作任何断言。

```agda
𝒮ʟ : ZFStructure (ℓ-suc ℓ)
𝒮ʟ = 𝒮ᵥ ↾ isL
```

## 小结

塔 `Lset` 由成员递归定义，`isLayer` 记录它对可定义性运算和三种并集构造的封闭性。对层见证作结构递归，并使用相应引理，便得到 `layer-trans`。一个集合属于 `isL`，是指它仅仅地属于某个序数 `α` 的层 `Lset α`；这个类是传递的，把环境结构限制到该类上便得到 `𝒮ʟ`。余下任务是逐条公理证明这个结构满足 ZFC。