可构造层级与可构造宇宙

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

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

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

{-# 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，正是为这个算子而从语法章沿用的。

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 上取值为成员的集合。与之相伴，命题截断 ∥ _ ∥₁ 及其引入 ∣ _ ∣₁ 给出「仅仅存在」：截断陈述的一个证明断言存在某个见证，而不指名它。

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 展开，便得到记号 ⟨ _ ⟩ 取命题的底层类型、∈ˢ 表示结构成员关系。本章的每个陈述都在这个命题值设定中表述。

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，均已在彼处建立；这里只是赋予全书通用的短记号。

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 之间的路径。最后一行宣布第一条封闭性事实，关于空集。

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 的成员之成员的全体，也传递。

∅-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。

⋃-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 要供给的。

            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。

  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 等同的路径。

    (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 是命题。有了这些封闭性原则，空集、可定义幂集、以及一般、二元、索引三种形式的并，下文证明每个层都传递的归纳就成了一行分发：每个构造子对应这里证明的相应引理。

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

序数，仅取谓词

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

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

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；正是这种平行性使下一条证明变得直接。

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。

  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 的传递性时正要用到这一事实。

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 β) ∣ β ∈ α }，一条方程同时服务零、后继与极限：α 为空时并为空，后继时重复经典的下一步，极限时一次收齐所有更早层。

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

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

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

  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 α，而不必打开递归机制。

  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 α 都是层。其证明本身又是一次成员归纳的应用，即定义塔的那条同一原理。

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)))))，恰好是塔的步进函数所构造的那个族。

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 内部打开，故整个归纳都在塔的意读层面运行。结合上一节，每层都是传递的层。

      (λ 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 指认。由于环境层级中的成员关系是截断的，陈述冠以命题截断：所断言的只是这样的公式存在，而非选定了某条。下面两条引理把这条等价各按一个方向陈述；这里宣告的是进入方向，把截断的定义数据变成隶属。

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

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

  𝒟ₒ-intro A x p = p

  𝒟ₒ-inv : (A x : S) → ⟨ x ∈ˢ 𝒟ₒ A ⟩
         → ∥ Σ[ φ ∈ Formula ⟪ A ⟫  ] (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。

  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，即 ⟪ α ⟫ 中指名成员 δ 的元素。

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 确实从它构造出了纤维表示。

      (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。结果是截断的见证，正是因为并公理不指名任何典范前驱；分支内构造出的那一个只是局部数据，而非选定的函数。

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 α。注意其严格形式：单调性要求 β 是 α 的成员，而不仅是子集，这与塔沿成员取并的生长方式一致。

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 属于层 α 的证据；可构造集并不附带一个典范层。量词遍历整个载体，故见证只以「仅仅存在」的形式可得；把类当作命题值谓词，正是稍后能把它限制成结构的原因。

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 本身就是截断的存在式，而不是因为任何选择需要撤销。

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

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

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

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 公理；限制本身对此不作任何断言。

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

小结

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