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

造集合运算怎样提升到可构造宇宙中？一个集合属于 `L`，当且仅当它能呈现为某个序数层 `Lset σ` 的可定义子集。本章反复使用同一思路：找出一个容纳所需输入的序数层，在该层上写出外延为目标集合的公式，再在周遭集合层级中证明相应的外延等式。

闭包引理 `defSet→isL` 完成这一过程。给定序数 `σ`，若仅仅存在一条外延为 `x` 的一元公式，`𝒟ₒ-intro` 便认出 `x` 是 `Lset σ` 的可定义子集，`𝒟ₒ→isL` 再把它放入 `L`。恒等式 `Lset (sucV σ) ≡ 𝒟ₒ (Lset σ)` 说明了层计算：下一层恰由当前层的可定义子集组成。打包后的集合 `LsetS` 与 `𝒟ₒS` 把这两个集合给成载体 `S` 的元素。

本章以此在 `L` 中构造空集、无序对与并。外延性利用传递性，把关于可构造成员的一致性推广到所有周遭成员；正则性则递归限制层级的可及性证明。若两个输入需要公共层，`bound2` 会给出共同的严格上界，而无须比较原来的两层。

设定固定一个宇宙层级 `ℓ`，并在该层级的累积层级 `V` 中工作。本章一切都是构造性的：不假设排中律、resize 或选择。公理将据以证明的载体，是 `V` 的集合连同可构造性证书 `isL` 组成的类型，而下文每条主张都仅凭周遭集合层级建立。

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

open import Base.Prelude

module L.Axioms.Basic {ℓ : Level} where

open import FOL.Syntax using ( Formula; var; con; _≐_; _∈̇_; _∨̇_; ⊤̇; ⊥̇; ∃̇∈ )
```

闭包模式的刻出步骤在一阶语言中进行。它的公式以某结构的小索引类型为载体，原子谓词是相等与隶属，并备有析取与有界存在量词；这正是可定义性算子所用的构造。关于从结构过渡到子结构，有两条周遭集合层级的事实将发挥作用：限制中两个元素之间的路径已经是其底层集合之间的路径，而继承来的公理要利用的正是这一方向。

```agda
open import FOL.ZFStructure using ( ↾-reflects; module hPropStructure )
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV )
open import V.Model {ℓ}
  using ( empty-spec; pair-spec; union-spec; self∈sucV; ∈sucV-elim
```

待提升的每个构造在周遭集合层级中已满足其成员律：空集没有成员，无序对的每个成员是两个条目之一，并集有精确的双向刻画。这些周遭定律在层级中证明一次，便充当下文公式以外延性接受检验的标准；它们被继承，而非重证。计算中还要用到两条周遭集合层级的事实：属于后继 `sucV σ` 可分成「属于 `σ`」与「就是 `σ`」两种情形，而单点集与对 `⁅ x , x ⁆` 被指认等同。有序对的 Kuratowski 码 `pr` 落在哪个层，将由无序对计算得出。

```agda
        ; pair-singleton )
open import V.Coding {ℓ} using ( pr )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-layer
```

可构造一侧提供层体系。`Lset` 以集合为索引给出各层，`IsOrd` 是序数性证书，`isL` 是可构造集的类，`isL-trans` 使其传递。层的可定义幂集是 `𝒟ₒ`；`𝒟ₒ-intro` 从一条公式加一条外延等式识别出可定义子集，而 `Lset-in`、`Lset-out`、`Lset⊆𝒟ₒ`、`Lset-mono` 与 `Lset→isL` 让层中的隶属得以转换、沿更大的层向上搬运、并被读成可构造性证书。层的传递性是 `layer-trans`。

```agda
        ; layer-trans; 𝒟ₒ; 𝒟ₒ-intro; Lset-in; Lset-out; Lset⊆𝒟ₒ
        ; Lset-mono; Lset→isL )
open import L.Ordinal {ℓ} using ( ∅-ord; suc-ord; bound2 )

open import Cubical.Data.FinData using ( zero; suc )
open import Cubical.Data.Sum using ( inl; inr )
```

三个序数事实控制层：空集是序数，序数的后继仍是序数，而 `bound2` 对两个给定序数返回一个严格包含二者的序数。配对用最后一条把两个可构造实参放进同一层，无须比较原层或选取最大者。有穷索引类型随后描述该层中的有穷像，二元和则表达定义这些像所用的析取。

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Foundations.Prelude using ( isPropIsContr )
open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
```

周遭集合层级中的隶属取值于命题，而呈现嵌入的纤维也是命题。因此，`∈-asFiber` 能把给定的隶属证明转换成小呈现中的实际索引，连同回到该成员的路径。具体地，从 `⟨ x ∈ Lset σ ⟩` 得到 `m : ⟪ Lset σ ⟫` 与 `⟪ Lset σ ⟫↪ m ≡ x`，公式因而能用常元指名该成员。这里直接得到数据，是因为相应纤维自身为命题；这一步没有另一个外层截断需要消去。

```agda
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; sett )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; ∈-asFiber; extensionality; _⊆_; ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
```

本章所需的周遭集合都带有精确的隶属刻画：空集配 `∅-empty`，无序对 `⁅_,_⁆` 及其单点变体配 `pairing-ax`，并配 `union-ax` 与 `⋃_`。这些是层级自己的分类结果，给出每条成员律的两个方向，故下文刻出的可定义子集可以对照它们以外延性检验。后继运算 `sucV` 给出下一层的索引。

```agda
  using ( ∅; ∅-empty; ⁅_,_⁆; ⁅_⁆s; pairing-ax; ⋃_; union-ax
        ; module InfinitySet )
open InfinitySet using ( sucV )

open hPropStructure 𝒮ʟ
```

语义一侧一次性确定。真值取层级 `ℓ-suc ℓ` 上的命题，故公式的解释落在普通的类型构造中；把限制结构经命题值语义读取，便得到结构成员关系 `∈ˢ`，以及取命题底层类型的括号记法 `⟨_⟩`。一个实现集合于是是载体 `S` 的元素，即带可构造性证书的集合，连同说明其成员关系实现哪条规格的等式；这就是类型 `SetOf Q`。原理 `setOf-unique` 把一个实现集合变成收缩性数据，正是它把本章余下每条公理字段化归为纯粹的存在问题。

```agda
module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf; setOf-unique )
```

## 可定义子集是可构造的

层 `Lset (sucV σ)` 是以 `δ ∈ sucV σ` 为指标的一族集合的并。由于 `σ ∈ sucV σ`，集合 `𝒟ₒ (Lset σ)` 是其中一个被并集合，所以它的每个元素都属于 `Lset (sucV σ)`。若 `σ` 是序数，其后继也是序数，这条层隶属便给出 `isL` 证书。

引理 `𝒟ₒ→isL` 接收一个序数 `σ` 及其序数性证书 `oσ`、一个集合 `x`、以及「`x` 属于 `σ` 处层的可定义幂集」的证明，结论是 `x` 可构造。证明把 `x` 抬高一级。由于 `σ` 属于自身的后继 `sucV σ`，包含关系 `Lset-in` 把「属于 `𝒟ₒ (Lset σ)`」变成「属于层 `Lset (sucV σ)`」，而该层的索引经 `suc-ord oσ` 是序数。再用一次 `Lset→isL`，就把这条层隶属转成证书 `isL x`。那条截断的假设按原样使用：它被直接送入 `Lset-in`，而后者的结论以同样方式截断，因此全程没有提取或选定任何可构造性见证。

```agda
𝒟ₒ→isL : (σ : V ℓ) → IsOrd σ → (x : V ℓ) → ⟨ x ∈ 𝒟ₒ (Lset σ) ⟩ → ⟨ isL x ⟩
𝒟ₒ→isL σ oσ x x∈𝒟ₒσ = Lset→isL (sucV σ) (suc-ord oσ) x
  (Lset-in (sucV σ) σ x (self∈sucV σ) x∈𝒟ₒσ)
```

把闭包引理与算子的识别原则复合，就得到本章每个构造所用的形式：要把一个集合放进 `L`，出示一个序数层、一条公式、以及一条说明该公式恰定义该集合的外延等式。这份出示只是存在层面的，即一条公式与一条等式组成的截断对，而这就已经足够。下文的空集、配对与并正是它的头三个实例。

`defSet→isL` 的假设是一个截断的存在式：仅仅是存在一条以该层成员为载体、元数为 1 的公式 `φ`，满足 `defSet (Lset σ) φ ≡ x`。识别原则 `𝒟ₒ-intro` 恰好把这样的数据转换成 `x` 属于 `𝒟ₒ (Lset σ)` 的成员关系。该隶属是命题，故向它消去截断是合法的，任何公式都从未被选定；与 `𝒟ₒ→isL` 的一行复合随即给出 `isL x`。这份证书的形状，序数层、定义公式、外延等式，正是本章余下部分反复实例化的模式。

```agda
defSet→isL : (σ : V ℓ) → IsOrd σ → (x : V ℓ)
           → ∥ Σ[ φ ∈ Formula ⟪ Lset σ ⟫ 1 ] (DefOf.defSet (Lset σ) φ ≡ x) ∥₁
           → ⟨ isL x ⟩
defSet→isL σ oσ x p = 𝒟ₒ→isL σ oσ x (𝒟ₒ-intro (Lset σ) x p)
```

这个模式的第零个实例是层自身。公式「真」定义出一个集合的全体，故每层都是它自身的可定义子集，从而在下一层可构造。正是这一点使层可以被一条公式**点名**，凡用层界住量词的构造都立足于此。再加上把层与其可构造性证书配对的打包 `LsetS`，层本身就成为 `L` 载体的一个元素。

`isL-Lset` 的证明是在 `x = Lset β` 处对 `𝒟ₒ→isL` 的直接实例化。见证公式是常真公式 `⊤̇`，而 `defSet⊤≡A` 把它的外延等同于载体集合的全体，在这里就是层 `Lset β` 自身。把公式与等式组成的对包进一次截断，便得到 `𝒟ₒ (Lset β)` 的一个成员；闭包引理再把它提升为 `⟨ isL (Lset β) ⟩`。证明没有检视层的任何内部结构；唯一进入论证的是 `β` 的序数性，经由 `suc-ord`。

```agda
opaque
  isL-Lset : (β : V ℓ) → IsOrd β → ⟨ isL (Lset β) ⟩
  isL-Lset β oβ = 𝒟ₒ→isL β oβ (Lset β)
    (𝒟ₒ-intro (Lset β) (Lset β) ∣ ⊤̇ , DefOf.defSet⊤≡A (Lset β) ∣₁)

LsetS : (β : V ℓ) → IsOrd β → S
```

限制结构的载体 `S` 由一个集合连同「它落在该类中」的证明组成；`LsetS` 恰好为序数层给出这个配对：底层集合 `Lset β` 加上刚构造的证书。经由这个元素，层作为一个普通的载体点进入可构造结构。

```agda
LsetS β oβ = Lset β , isL-Lset β oβ
```

## 后继层

塔的步进是可定义幂集；在后继索引处，步进就是全部：`Lset (sucV σ)` 恰是 `𝒟ₒ (Lset σ)`。这条恒等式作为两个包含来证明。其一，`σ` 属于自身的后继，所以 `𝒟ₒ (Lset σ)` 是被并集合之一，其每个元素都属于下一层。其二，`Lset (sucV σ)` 的成员属于某个 `δ ∈ sucV σ` 对应的 `𝒟ₒ (Lset δ)`；若 `δ` 是 `σ` 的成员，该集合已在 `Lset σ` 中，因而是它的可定义子集；若 `δ` 就是 `σ`，结论直接成立。两个方向都不使用相对化，也不需要算子的单调性；这里没有 `σ` 的序数性假设。

有了这条恒等式，可定义幂集的可构造性随之立得：层在下一层可构造，而层的可定义幂集正是那下一层。

两个集合用周遭集合层级的外延性比较，路径化归为一对包含关系。较难的方向需要一条桥引理：从下一层的成员 `x` 出发，仅仅是存在某个更早层的可定义幂集包含 `x`，其见证 `δ` 是 `sucV σ` 的成员。按 `sucV σ` 的构造，其成员要么是 `σ` 的成员，要么是 `σ` 自身，故这个见证正是论证可以分情况处理的信息。

```agda
Lset-suc : (σ : V ℓ) → Lset (sucV σ) ≡ 𝒟ₒ (Lset σ)
Lset-suc σ = extensionality (Lset (sucV σ)) (𝒟ₒ (Lset σ)) (sub₁ , sub₂)
  where
  fromEarlier : (x : V ℓ)
              → Σ[ δ ∈ V ℓ ] (⟨ δ ∈ sucV σ ⟩ × ⟨ x ∈ 𝒟ₒ (Lset δ) ⟩)
```

对见证的消去恰好使用这条二分法。`∈sucV-elim` 取「`δ` 落在 `sucV σ` 中」的证明与两个分支。第一个分支里 `δ` 是 `σ` 的成员，于是 `Lset-in` 把 `x` 放进 `Lset σ`，而引理 `Lset⊆𝒟ₒ` 说层的每个成员都是它的可定义子集之一，把 `x` 抬进 `𝒟ₒ (Lset σ)`。第二个分支里 `δ` 就是 `σ` 自身，`subst` 沿路径 `δ ≡ σ` 搬运已有的隶属，改换层的索引。整个目标 `x ∈ 𝒟ₒ (Lset σ)` 是命题，这正是截断的见证在此得以消去的前提。

```agda
              → ⟨ x ∈ 𝒟ₒ (Lset σ) ⟩
  fromEarlier x (δ , (δ∈suc , x∈𝒟ₒδ)) =
    ∈sucV-elim {A = σ} {x = δ} (snd (x ∈ 𝒟ₒ (Lset σ))) δ∈suc
      (λ δ∈σ → Lset⊆𝒟ₒ σ x (Lset-in σ δ x δ∈σ x∈𝒟ₒδ))
      (λ δ≡σ → subst (λ w → ⟨ x ∈ 𝒟ₒ (Lset w) ⟩) δ≡σ x∈𝒟ₒδ)
```

第一个包含正向使用这条桥。`Lset (sucV σ)` 的结构成员经 `∈∈ₛ` 转成周遭成员关系，层刻画 `Lset-out` 返回截断的更早层见证，`fromEarlier` 再把它映入 `𝒟ₒ (Lset σ)`；消去的目标是命题 `x ∈ 𝒟ₒ (Lset σ)`，这正是丢弃 `δ` 的选择得以合法的依据。反向包含只需 `σ` 属于自身的后继：经 `∈∈ₛ` 把结构成员关系转成周遭形式后，带见证 `self∈sucV σ` 的 `Lset-in` 把 `𝒟ₒ (Lset σ)` 的任何成员直接放进 `sucV σ` 处的层。两个包含合起来，便得到作为路径的恒等式。

```agda
  sub₁ : ⟨ Lset (sucV σ) ⊆ 𝒟ₒ (Lset σ) ⟩
  sub₁ x x∈ₛ = ∈∈ₛ {a = x} {b = 𝒟ₒ (Lset σ)} .fst
    (PT.rec (snd (x ∈ 𝒟ₒ (Lset σ))) (fromEarlier x)
      (Lset-out (sucV σ) x (∈∈ₛ {a = x} {b = Lset (sucV σ)} .snd x∈ₛ)))

  sub₂ : ⟨ 𝒟ₒ (Lset σ) ⊆ Lset (sucV σ) ⟩
```

另一个包含用 `self∈sucV σ` 指出：在 `Lset (sucV σ)` 的定义中，`𝒟ₒ (Lset σ)` 是被并集合之一。因此，`Lset-in` 把这个可定义幂集的每个元素送入后继层。结合第一个包含，周遭集合层级的外延性给出路径 `Lset (sucV σ) ≡ 𝒟ₒ (Lset σ)`；这条恒等式不含 `σ` 的序数性假设。

```agda
  sub₂ x x∈ₛ = ∈∈ₛ {a = x} {b = Lset (sucV σ)} .fst
    (Lset-in (sucV σ) σ x (self∈sucV σ)
      (∈∈ₛ {a = x} {b = 𝒟ₒ (Lset σ)} .snd x∈ₛ))
```

后继恒等式把「层在下一层可构造」转成关于可定义幂集自身的陈述：既然 `Lset (sucV σ)` 恰是 `𝒟ₒ (Lset σ)`，而前者由前文引理可构造，故任何序数层的可定义幂集都可构造。于是可以把它打包成载体的一个元素：一个 `L` 的集合，附上其可构造性证书。

证明是沿后继恒等式的一次传输。在后继处应用 `isL-Lset` (其序数性为 `suc-ord oσ`)，得到 `⟨ isL (Lset (sucV σ)) ⟩`；再沿路径 `Lset-suc σ` 改写目标，便得到 `⟨ isL (𝒟ₒ (Lset σ)) ⟩`。除这条恒等式外，没有使用算子的任何其他性质。

```agda
opaque
  isL-𝒟ₒ : (σ : V ℓ) → IsOrd σ → ⟨ isL (𝒟ₒ (Lset σ)) ⟩
  isL-𝒟ₒ σ oσ = subst (λ w → ⟨ isL w ⟩) (Lset-suc σ)
    (isL-Lset (sucV σ) (suc-ord oσ))

𝒟ₒS : (σ : V ℓ) → IsOrd σ → S
```

打包 `𝒟ₒS` 把该层的可定义幂集与其可构造性证书配成对，得到一个恰指称 `𝒟ₒ (Lset σ)` 的载体元素。上一节打包的是层自身，这一节打包的是「一层的可定义子集的全体」。

```agda
𝒟ₒS σ oσ = 𝒟ₒ (Lset σ) , isL-𝒟ₒ σ oσ
```

## 有穷族

闭包模式在有穷族上最容易看清。固定一层 `Lset σ` 与它的 `n` 个成员组成的族。它们的像是集合 `finSet n h`，而「等于这一个」的有穷析取恰好从该层中刻出这个像：长度为零时公式取假，此后每个长度多比较一个常元与自由变元。族中的成员可以重复，不同位置可以指名同一个集合。

全部内容是一次归纳，它把析取的满足与被该族命中等同起来，两个方向都对着被指名成员的嵌入代表陈述。两个方向就位后，一次周遭集合层级的外延性证出 `defSet≡`，即「可定义子集恰是该像」的等式；`finSet∈𝒟ₒ` 把该像记录为 `𝒟ₒ (Lset σ)` 的成员，而 `finSetL` 从「族中每个成员都落在该层」的假设出发，经闭包引理 `defSet→isL`，给出证书 `isL (finSet n h)`。

像集合被直接定义：`finSet n h` 是由提升到层级所在宇宙的索引类型 `Fin n` 与「先降层再作用 `h`」的索引映射所呈现的集合。成员关系按层级截断的形式刻画：`y` 属于 `finSet n h`，恰当仅仅是存在索引 `i` 满足 `h i ≡ y`。`finSet-in` 与 `finSet-out` 的每个方向都是截断内部的一次映射，因为呈现场合中的成员关系按构造就是索引的截断存在。

```agda
finSet : (n : ℕ) → (Fin n → V ℓ) → V ℓ
finSet n h = sett (Lift {ℓ-zero} {ℓ} (Fin n)) (λ i → h (lower i))

finSet-in : (n : ℕ) (h : Fin n → V ℓ) (y : V ℓ)
          → ∥ Σ[ i ∈ Fin n ] (h i ≡ y) ∥₁ → ⟨ y ∈ finSet n h ⟩
finSet-in n h y = PT.map (λ { (i , q) → lift i , q })
```

反向成员引理 `finSet-out` 是同一映射倒过来读，从提升后的索引降回 `Fin n`。随后可定义性的工作在序数层 `σ` 上进行：在 `DefOf (Lset σ)` 内部工作，把常元的字母表定为该层的小索引类型 `⟪ Lset σ ⟫`，于是层的成员可用常元命名，而所论的可定义子集就是从 `Lset σ` 中刻出的那些。

```agda
finSet-out : (n : ℕ) (h : Fin n → V ℓ) (y : V ℓ)
           → ⟨ y ∈ finSet n h ⟩ → ∥ Σ[ i ∈ Fin n ] (h i ≡ y) ∥₁
finSet-out n h y = PT.map (λ { (i , q) → lower i , q })

module FinOf (σ : V ℓ) (oσ : IsOrd σ) where
  module DefC = DefOf (Lset σ)
```

公式是等式的有穷析取。长度为零时无可等同之物，故公式取假；长度为后继时，自由变元与指名族首成员的常元比较，其余成员由族平移后的递归调用处理。元数始终为一：整个析取共用一个自由变元槽，而函数 `g` 无须单射，不同位置可以指名同一个成员。

```agda
  finDisj : (n : ℕ) → (Fin n → ⟪ Lset σ ⟫) → Formula ⟪ Lset σ ⟫ 1
  finDisj zero    g = ⊥̇
  finDisj (suc n) g =
    (var zero ≐ con (g zero)) ∨̇ finDisj n (λ i → g (suc i))

  private
```

桥陈述 `Hits` 说：赋值所指名的成员仅仅被该族命中，其中路径是对照被指名成员的嵌入代表 `⟪ Lset σ ⟫↪ (g i)` 书写的。两个方向连接的是：可定义子集所看见的「析取被满足」，与像集合所看见的「被族命中」。

```agda
    Hits : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫) (y : V ℓ) → Type (ℓ-suc ℓ)
    Hits n g y = ∥ Σ[ i ∈ Fin n ] (⟪ Lset σ ⟫↪ (g i) ≡ y) ∥₁

    sat→hits : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫) (m : ⟪ Lset σ ⟫)
             → ⟨ (DefC.ι m ∷ []) DefC.⊨ᵐ finDisj n g ⟩
             → Hits n g (⟪ Lset σ ⟫↪ m)
```

从满足到命中沿长度递归。长度为零时公式是假，其证明导致荒谬。长度为后继时，满足是截断的析取：左支中赋值等于第一个常元，给出索引 `zero`；右支中递归调用对平移后的族返回一个命中，其索引加一提升。每个分支都在截断内返回其见证，而外层消去合法，因为目标 `Hits` 取命题值。

```agda
    sat→hits zero    g m bot = Empty.rec* bot
    sat→hits (suc n) g m = PT.rec squash₁
      (λ { (inl e)  → ∣ zero , sym e ∣₁
         ; (inr sat) → PT.map (λ { (i , q) → suc i , q })
                         (sat→hits n (λ i → g (suc i)) m sat) })
```

反方向把命中转为满足，同样沿长度递归。长度为零时索引类型 `Fin 0` 没有任何元素，故通过对照空索引类型做匹配即可反驳那里的命中；这正与公式在零处取假相配。由于 `hits→sat` 是同时对所有长度陈述的，后继情形中的递归调用无须携带任何额外假设即可使用。

```agda
    hits→sat : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫) (m : ⟪ Lset σ ⟫)
             → Hits n g (⟪ Lset σ ⟫↪ m)
             → ⟨ (DefC.ι m ∷ []) DefC.⊨ᵐ finDisj n g ⟩
    hits→sat zero g m =
      PT.rec (snd ((DefC.ι m ∷ []) DefC.⊨ᵐ finDisj zero g)) (λ { (() , _) })
```

长度为后继时，命中是截断的对，其索引要么是 `zero`，要么是后继 `suc i`。第一种情形中，路径把成员与第一个常元等同，公式的左析取支得到满足。第二种情形中，对平移后族施用递归调用得到尾部析取的满足，它成为右析取支。两种情形都在截断内返回答案，故证明从不依赖于命中恰好携带的是哪个索引。

```agda
    hits→sat (suc n) g m =
      PT.rec (snd ((DefC.ι m ∷ []) DefC.⊨ᵐ finDisj (suc n) g))
        (λ { (zero  , q) → ∣ inl (sym q) ∣₁
           ; (suc i , q) →
             ∣ inr (hits→sat n (λ j → g (suc j)) m ∣ i , q ∣₁) ∣₁ })
```

桥的两个方向恰好是恒等式 `defSet≡` 所需的两条包含。证明用的是周遭集合层级的外延性：集合的路径化归为一对包含，而像集合以缩写 `F` 记之。剩下的工作只是在结构成员记号与周遭成员记号之间做簿记。

```agda
  defSet≡ : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫)
          → DefC.defSet (finDisj n g) ≡ finSet n (λ i → ⟪ Lset σ ⟫↪ (g i))
  defSet≡ n g = extensionality _ _ (sub₁ , sub₂)
    where
    F = finSet n (λ i → ⟪ Lset σ ⟫↪ (g i))
```

第一个包含从可定义子集的结构成员 `y` 出发。转换 `∈∈ₛ` 把它变成周遭成员关系，其读法引理给出截断的定义数据：赋值 `m` 连同满足证书，以及强迫 `y` 等于 `m` 所指名成员的路径 `q`。此处要证的目标是命题 `⟨ y ∈ F ⟩`，这正是消去截断得以合法的依据。

```agda
    sub₁ : ⟨ DefC.defSet (finDisj n g) ⊆ F ⟩
    sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = F} .fst (PT.rec (snd (y ∈ F))
      (λ { ((m , h) , q) →
        subst (λ v → ⟨ v ∈ F ⟩) q
          (finSet-in n (λ i → ⟪ Lset σ ⟫↪ (g i)) (⟪ Lset σ ⟫↪ m)
```

满足证书经可定义子集成员关系的计算规则 `defSet-mem` 转换，得到析取在赋值 `m` 处的一次满足。桥引理 `sat→hits` 随之产出一次命中，`finSet-in` 把命中读成嵌入元素在像中的成员关系。最后沿 `q` 的搬移把这条成员关系从被指名的成员移到 `y` 自身。

```agda
            (sat→hits n g m
              (subst ⟨_⟩ (DefC.defSet-mem (finDisj n g) m)
                ∣ (m , h) , refl ∣₁))) })
      (∈∈ₛ {a = y} {b = DefC.defSet (finDisj n g)} .snd y∈ₛ))
    sub₂ : ⟨ F ⊆ DefC.defSet (finDisj n g) ⟩
```

反向包含从 `y ∈ F` 出发。消去规则 `finSet-out` 仅仅给出索引 `i : Fin n` 与路径 `q : ⟪ Lset σ ⟫↪ (g i) ≡ y`。在代表元 `g i` 处，截断见证 `∣ i , refl ∣₁` 证明 `Hits n g (⟪ Lset σ ⟫↪ (g i))`；`hits→sat` 把它转换成有限析取在该代表元处的满足。随后沿 `q` 搬移，便得到 `y` 属于可定义子集。

```agda
    sub₂ y y∈ₛ = PT.rec (snd (y ∈ₛ DefC.defSet (finDisj n g)))
      (λ { (i , q) →
        subst (λ v → ⟨ v ∈ₛ DefC.defSet (finDisj n g) ⟩) q
          (∈∈ₛ {a = ⟪ Lset σ ⟫↪ (g i)} {b = DefC.defSet (finDisj n g)} .fst
            (subst ⟨_⟩ (sym (DefC.defSet-mem (finDisj n g) (g i)))
```

满足经反向使用 `defSet` 的隶属读法，被读成嵌入的 `g i` 在可定义子集中的结构成员关系，再沿命中路径的搬移把它落到 `y` 上。两条包含合起来，`defSet≡` 便作为集合的路径陈述这一相等：由有穷析取刻出的子集就是该族的像，族中的重复也在其内，因为相同的成员由多个常元名指，并不影响像。

```agda
              (hits→sat n g (g i) ∣ i , refl ∣₁))) })
      (finSet-out n (λ i → ⟪ Lset σ ⟫↪ (g i)) y
        (∈∈ₛ {a = y} {b = F} .snd y∈ₛ))

  finSet∈𝒟ₒ : (n : ℕ) (g : Fin n → ⟪ Lset σ ⟫)
            → ⟨ finSet n (λ i → ⟪ Lset σ ⟫↪ (g i)) ∈ 𝒟ₒ (Lset σ) ⟩
```

本节以两步收尾。第一步，`finSet∈𝒟ₒ` 把刚才证明的析取与等式交给 `𝒟ₒ-intro`，把像集合记录为该层可定义幂集的一个成员；这一可定义性证书是截断的，故被保留的数据中不含特定公式。第二步，`finSetL` 从一个由任意集合组成的族出发，并给定每个成员属于该层的证明。对每个成员，`∈-asFiber` 给出层呈现的索引以及回到该成员的路径；用 `cong (finSet n) (funExt qg)` 沿这些路径改写像集合，便把它与 `defSet≡` 所谈论的嵌入族等同起来。闭包引理 `defSet→isL` 随即给出 `finSet n h` 的可构造性。

```agda
  finSet∈𝒟ₒ n g = 𝒟ₒ-intro (Lset σ) _ ∣ finDisj n g , defSet≡ n g ∣₁

  finSetL : (n : ℕ) (h : Fin n → V ℓ) → ((i : Fin n) → ⟨ h i ∈ Lset σ ⟩)
          → ⟨ isL (finSet n h) ⟩
  finSetL n h hσ = defSet→isL σ oσ (finSet n h)
    ∣ finDisj n g , (defSet≡ n g ∙ cong (finSet n) (funExt qg)) ∣₁
```

假设 `hσ i` 只是陈述 `h i` 属于该层。对一个层级集合的隶属是嵌入映射 `⟪ Lset σ ⟫↪` 的纤维的截断，而该映射是嵌入，其纤维类型是命题，故向纤维类型消去截断是合法的，`∈-asFiber` 做的正是这一转换。于是 `g i` 是被选出的索引，其嵌入后的元素有路径 `qg i` 回到 `h i`。交给 `defSet→isL` 的证书把关于代表元 `g` 的有穷析取与 `defSet≡ n g` 配对，再接上改写 `funExt qg`，把这条等同从嵌入后的族 `finSet n (λ i → ⟪ Lset σ ⟫↪ (g i))` 搬到原先的族 `finSet n h` 上。

```agda
    where
    g : Fin n → ⟪ Lset σ ⟫
    g i = ∈-asFiber {a = h i} {b = Lset σ} (hσ i) .fst
    qg : (i : Fin n) → ⟪ Lset σ ⟫↪ (g i) ≡ h i
    qg i = ∈-asFiber {a = h i} {b = Lset σ} (hσ i) .snd
```

## 两个集合，一层

`isL-directed` 把任意两个可构造集合放进一个公共的序数层。

每个可构造集合都有自己的层，由其截断的可构造性证书「仅仅地」给出。结论把二者合并：仅仅是存在一个序数 `σ`，其层同时装下这两个集合。`bound2` 产出一个同时包含两个给定序数的序数，而层的单调性把每个集合从各自的层抬进上界处的层。结论以截断形式陈述，故从不向外界出示任何层；在局部，两份证书只被打开到足以读出它们各自名指的层为止。

这条陈述把两个可构造集合当作截断的证书接收：`⟨ isL x ⟩` 与 `⟨ isL y ⟩` 只是说各自落在 `L` 中，并不点名某一层。结论同样是截断的，因此那两份证书只被消去到一条截断的存在陈述中，从未向外部世界选出任何层。局部的目标内容被打包为 `Bound`：一个序数 `σ`、它的序数性，以及 `Lset σ` 中的两条隶属。

```agda
isL-directed : (x y : V ℓ) → ⟨ isL x ⟩ → ⟨ isL y ⟩
             → ∥ Σ[ σ ∈ V ℓ ] (IsOrd σ × (⟨ x ∈ Lset σ ⟩ × ⟨ y ∈ Lset σ ⟩)) ∥₁
isL-directed x y px py = PT.rec2 squash₁ go px py
  where
  Bound : Type (ℓ-suc ℓ)
```

两条截断由 `PT.rec2` 一次消去，其目标是截断 `∥ Bound ∥₁`。干活的分支 `go` 接收证书所隐藏的显式数据：序数层 `α` 且 `x` 属于 `Lset α`，以及序数层 `β` 且 `y` 属于 `Lset β`。合并它们并不是在比较大小；`bound2 α β oα oβ` 返回一个同时包含 `α` 与 `β` 的序数上界，连同它的序数性和两条隶属。

```agda
  Bound = Σ[ σ ∈ V ℓ ] (IsOrd σ × (⟨ x ∈ Lset σ ⟩ × ⟨ y ∈ Lset σ ⟩))
  go : Σ[ α ∈ V ℓ ] (IsOrd α × ⟨ x ∈ Lset α ⟩)
     → Σ[ β ∈ V ℓ ] (IsOrd β × ⟨ y ∈ Lset β ⟩) → ∥ Bound ∥₁
  go (α , (oα , x∈Lα)) (β , (oβ , y∈Lβ)) =
    ∣ bnd .fst , (bnd .snd .fst , ( Lset-mono (bnd .snd .snd .fst) x∈Lα
```

上界自带 `α ∈ σ₀` 与 `β ∈ σ₀` 两条隶属，于是单调性 `Lset-mono` 把 `x ∈ Lset α` 抬进上界处的层 `Lset σ₀`；对来自 `β` 的 `y` 同理。把拼好的三元组用 `∣_∣₁` 包起来便完成 `go`，也随之完成整条陈述：任意两个可构造集合「仅仅存在」一个公共的序数层。配对字段要消费的正是它，因为配对需要两个实参在同一层上可见。

```agda
                                  , Lset-mono (bnd .snd .snd .snd) y∈Lβ )) ∣₁
    where bnd = bound2 α β oα oβ
```

## 继承来的两条公理

外延性与正则性都从周遭集合层级限制而来，但论证不同。对外延性，`isL-trans` 把任一可构造集合的周遭成员变成载体元素，从而可以应用关于载体成员的一致性假设；周遭集合层级的外延性随后等同底层集合，限制反射再给出载体路径。正则性不使用 `isL-trans`：只需把周遭可及性递归地限制到已经自带可构造性证书的对子上。

`L` 内部的外延性形状是：若载体的两个元素在每个载体元素处的隶属一致，它们就作为路径相等。证明被化归到底层层级。载体由「集合加可构造性证书」的对组成，而 `↾-reflects` 是一条原理：这样的对由其第一投影决定，底层集合 `fst a` 与 `fst b` 之间的路径已经给出路径 `a ≡ b`。于是全部工作归结为制造那条底层路径，它在 `vwise` 的前提下由 `extensionalV` 提供。

```agda
extensionalL : {a b : S} → ((x : S) → (x ∈ˢ a) ≡ (x ∈ˢ b)) → a ≡ b
extensionalL {a} {b} h =
  ↾-reflects {𝒮 = 𝒮ᵥ} {M = isL} (extensionalV {a = fst a} {b = fst b} vwise)
  where
  vwise : (v : V ℓ) → (v ∈ fst a) ≡ (v ∈ fst b)
```

假设 `h` 只谈及载体元素，即可构造的对。要把它扩展到层级中任意的 `v`，出力的是传递性：由 `v ∈ fst a` 与 `a` 所携带的证书，`isL-trans` 得出 `v` 自身可构造；把该证书与 `v` 配成对，就把 `v` 呈现为载体元素，`h` 在该元素处给出限制成员关系的路径。沿这条路径搬移 `v∈a` 便落在 `⟨ v ∈ fst b ⟩`，故 `fwd` 是一个普通的蕴涵。用 `⇔toPath` 把两个方向的蕴涵合成路径，便得到 `extensionalV` 所要求的周遭隶属的逐点路径。

```agda
  vwise v = ⇔toPath fwd bwd
    where
    fwd : ⟨ v ∈ fst a ⟩ → ⟨ v ∈ fst b ⟩
    fwd v∈a = subst ⟨_⟩ (h (v , isL-trans v∈a (a .snd))) v∈a
    bwd : ⟨ v ∈ fst b ⟩ → ⟨ v ∈ fst a ⟩
```

反向是从 `b` 出发读同一个论证，因 `h` 的方向是从 `a` 指向 `b` 而加 `sym`。至此 `extensionalL` 完成。正则性要的是另一件事：把载体的成员关系的良基性作为显式的可及性数据。对对子 `(v , p)`，即集合 `v` 连同它的可构造性证书，周遭集合层级已经为 `v` 提供了 `Acc`；任务是把这份数据沿着证书抬上去。

```agda
    bwd v∈b = subst ⟨_⟩ (sym (h (v , isL-trans v∈b (b .snd)))) v∈b

regularityL : WellFounded _∈ᵗ_
regularityL (v , p) = accL v (regularityV v) p
  where
  module Vmem = hPropStructure 𝒮ᵥ
```

这次抬升是对周遭可及性数据的一次递归。若 `u` 可及，则依定义 `u` 的每个周遭成员 `y` 都可及，子句 `rec` 打包的正是这一点。限制元素 `(u , q)` 的成员 `(y , r)` 投影为 `u` 的周遭成员 `y`，故 `accL` 可以对 `rec y y∈` 递归，并把证书 `r` 附到结果上。限制的成员关系 `y ∈ᵗ (u , q)` 只沿用底层关系 `y ∈ u`；证书 `r` 属于前驱载体元素 `(y , r)`，并不是成员证明的一部分。因此，可及性沿底层集合逐成员转移。

```agda
  accL : (u : V ℓ) → Acc Vmem._∈ᵗ_ u → (q : u ∈ᶜ isL) → Acc _∈ᵗ_ (u , q)
  accL u (acc rec) q = acc (λ { (y , r) y∈ → accL y (rec y y∈) r })
```

## 由外延性得到唯一性

`uniqueL` 从外延性导出唯一性：实现固定成员规格的集合是唯一的，因此后文尚未完成的公理字段只须给出一个「仅仅存在」的见证。

论证是把载体的外延性用在实现者上。实现同一谓词 `Q` 的两个集合，在每个载体元素处取同一真值，即 `Q x`，故 `extensionalL` 把它们等同。此处所需的唯一性形式是收缩性，而收缩性是命题；这恰好使「仅仅存在的实现者」能够被转换为收缩性数据本身。

实现者的唯一性是收缩性数据：一个中心，即任一实现该规格的集合，以及从中心到任一实现集合的路径。给出路径的部分是 `extensionalL`，因为两个实现集合携带同一成员规格，因而重合；中心与路径的组装则是对 `extensionalL` 应用 `setOf-unique`。第二条陈述从仅仅存在出发：`PT.rec` 之所以能消去截断的假设，是因为其目标 `isContr (SetOf Q)` 是命题，并返回同样的收缩性数据。从这里起，余下每条公理字段都通过展示一个见证、且以截断形式给出，来完成证明。

```agda
uniqueL : (Q : S → hProp (ℓ-suc ℓ)) → SetOf Q → isContr (SetOf Q)
uniqueL = setOf-unique extensionalL

mere→uniqueL : (Q : S → hProp (ℓ-suc ℓ)) → ∥ SetOf Q ∥₁ → isContr (SetOf Q)
mere→uniqueL Q = PT.rec isPropIsContr (uniqueL Q)
```

## 空集

对象语言中的假公式把周遭空集定义为可定义子集，而 `hasEmptyL` 封装其可构造性与空成员规格。

对象语言的假在任何层中都定义不出元素：`defSet ⊥̇` 的成员会在其索引处包含一个假的证明。因此，`defSet ⊥̇` 经外延性等于空集，从而空集可构造。它的规格来自层级，因为 `L` 中的隶属就是层级中的隶属；而上一节的唯一性原理把这个见证变成模型所要求的收缩性数据。

空集是第一个被构造的集合，而且它完全不需要上界：实参 `σ` 跑遍任意层，没有序数性假设，因为定义空集的公式在任何层都可以解读。证书是对象语言的假 `⊥̇` 与等式 `defSet⊥≡∅` 组成的对，并按 `𝒟ₒ-intro` 的要求以截断形式给出。

```agda
∅∈𝒟ₒ : (σ : V ℓ) → ⟨ ∅ ∈ 𝒟ₒ (Lset σ) ⟩
∅∈𝒟ₒ σ = 𝒟ₒ-intro (Lset σ) ∅ ∣ ⊥̇ , defSet⊥≡∅ ∣₁
  where
  module DefC = DefOf (Lset σ)
  defSet⊥≡∅ : DefC.defSet ⊥̇ ≡ ∅
```

这条等式是对照周遭空集的一次外延，分两个包含方向。第一向是有实质内容的方向：可定义子集的成员 `y`，经 `defSet` 的读法引理，呈现为索引 `m` 与 `⊥̇` 的满足证明 `h` 组成的截断对。假在对象语言中的满足是空的宿主类型，故 `Empty.rec* h` 反驳任何这样的成员。由于包含关系以命题值陈述，向它消去截断是合法的。

```agda
  defSet⊥≡∅ = extensionality (DefC.defSet ⊥̇) ∅ (sub₁ , sub₂)
    where
    sub₁ : ⟨ DefC.defSet ⊥̇ ⊆ ∅ ⟩
    sub₁ y y∈ₛ = PT.rec (snd (y ∈ₛ ∅))
      (λ { ((m , h) , q) → Empty.rec* h })
```

第二向是空洞的：`∅-empty` 把周遭空集的任何候选成员直接变成反驳。两个方向齐备后，`defSet ⊥̇` 与 `∅` 作为集合相等，`∅∈𝒟ₒ` 于是记录下空集是任意层的可定义子集。闭包引理随后最后再施展一次，就在层 `∅` 自身处，其序数性由引理 `∅-ord` 提供：空集可构造，位于其自身之上一个后继。

```agda
      (∈∈ₛ {a = y} {b = DefC.defSet ⊥̇} .snd y∈ₛ)
    sub₂ : ⟨ ∅ ⊆ DefC.defSet ⊥̇ ⟩
    sub₂ y y∈ₛ = Empty.rec (∅-empty y y∈ₛ)

∅∈L : ⟨ isL ∅ ⟩
∅∈L = 𝒟ₒ→isL ∅ ∅-ord ∅ (∅∈𝒟ₒ ∅)
```

打包方式照应底层集合：`∅ʟ` 是 `∅` 连同其可构造性证书组成的对，是载体 `S` 的一个元素。模型的存在性要求「没有成员的集合唯一存在」。所给出的见证是 `∅ʟ`，连同从层级取来的规格，即对任何候选集合的底层集合读取 `empty-spec`；唯一性则由 `uniqueL` 得到。这是第一条字段，而下两条构造的模式在它身上已经可见：找界、刻出、收尾。

```agda
∅ʟ : S
∅ʟ = ∅ , ∅∈L

hasEmptyL : isContr (SetOf (λ _ → ⊥))
hasEmptyL = uniqueL _ (∅ʟ , (λ x → empty-spec (fst x)))
```

## 受层界住的配对

对同一层的两个成员，一条含两个常元的析取公式把其无序对定义为该可定义子集；派生的结果把单点集安置在高一层处，把 Kuratowski 有序对码安置在高两层处。

一层的两个成员，其无序对是该层的可定义子集：二者各是某个索引的 `⟪ Lset σ ⟫↪`，而点名那两个索引的公式恰好定义出这个对。验证它要对照层级自己的配对公理做一次双向外延：可定义子集的成员满足那个析取，故是二者之一；而二者各自满足它，故是成员。

论证里没有一处关乎模型，说的是塔本身的一条事实，故照这样陈述：Kuratowski 编码下的有序对嵌套了两层无序对，因此落在其条目之上两层处。

此处不涉及序数性，后继恒等式也不涉及，理由相同：这里做的是构造，而非比较。单点集是退化的对，而有序对是单点集与对所成的对。

这条陈述只假设 `x` 与 `y` 落在层 `Lset σ` 中；不要求 `σ` 的序数性，因为刻出一个子集不需要比较层。证书由 `𝒟ₒ-intro` 组装：一条公式 `φ`，连同说明 φ 在该层中的外延恰为 `⁅ x , y ⁆` 的等式 `defSet≡`，并按可定义性算子的接口要求以截断形式给出。

```agda
pair∈𝒟ₒ : (σ x y : V ℓ) → ⟨ x ∈ Lset σ ⟩ → ⟨ y ∈ Lset σ ⟩
        → ⟨ ⁅ x , y ⁆ ∈ 𝒟ₒ (Lset σ) ⟩
pair∈𝒟ₒ σ x y x∈ y∈ = 𝒟ₒ-intro (Lset σ) ⁅ x , y ⁆ ∣ φ , defSet≡ ∣₁
  where
  module DefC = DefOf (Lset σ)
```

公式必须以层的小呈现 `⟪ Lset σ ⟫` 中的元素为常元。对两条隶属证明应用 `∈-asFiber`，得到实际索引 `mₓ`、`mᵧ`，以及路径 `qₓ : ⟪ Lset σ ⟫↪ mₓ ≡ x` 与 `qᵧ : ⟪ Lset σ ⟫↪ mᵧ ≡ y`。呈现嵌入的纤维是命题，所以这里可以直接恢复这些数据；论证没有把隶属假设当作另一个外层截断。

```agda
  mₓ = ∈-asFiber {a = x} {b = Lset σ} x∈ .fst
  qₓ : ⟪ Lset σ ⟫↪ mₓ ≡ x
  qₓ = ∈-asFiber {a = x} {b = Lset σ} x∈ .snd
  mᵧ = ∈-asFiber {a = y} {b = Lset σ} y∈ .fst
  qᵧ : ⟪ Lset σ ⟫↪ mᵧ ≡ y
```

公式有一个自由变元槽，读作：变元等于常元 `mₓ`，或等于常元 `mᵧ`。它被断言的外延是 `x` 与 `y` 的无序对。证明并不直接把外延与这个对等同；它先把外延与嵌入代表元组成的对等同，常元实际上就在那里，再对构造子 `⁅_,_⁆` 应用 `cong₂`沿 `qₓ` 与 `qᵧ` 搬移整条等式。

```agda
  qᵧ = ∈-asFiber {a = y} {b = Lset σ} y∈ .snd

  φ : Formula ⟪ Lset σ ⟫ 1
  φ = (var zero ≐ con mₓ) ∨̇ (var zero ≐ con mᵧ)

  defSet≡ : DefC.defSet φ ≡ ⁅ x , y ⁆
  defSet≡ =
```

等同的前一半是一次外延性，从可定义子集到嵌入代表元的对，分为两个包含。此处展示的方向说的是：凡满足 φ 者，都是那两个被点名元素之一。

```agda
      extensionality (DefC.defSet φ) ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆
        (sub₁ , sub₂)
    ∙ cong₂ ⁅_,_⁆ qₓ qᵧ
    where
    sub₁ : ⟨ DefC.defSet φ ⊆ ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆ ⟩
```

可定义子集的成员 `w`，经读法引理，呈现为索引 `m` 与「在点名 `m` 的赋值下 φ 的满足证明」组成的截断对。等式析取的满足只是记录：`m` 所名指的元素等于两个常元之一。而这条截断析取恰好是层级的配对刻画在从右到左方向所需的假设，于是 `pairing-ax` 把嵌入元素 `⟪ Lset σ ⟫↪ m` 放进嵌入代表元组成的对中。再沿把 `w` 与嵌入索引等同的路径 `q` 做搬移，包含即告完成。

```agda
    sub₁ w w∈ₛ = PT.rec (snd (w ∈ₛ ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆))
      (λ { ((m , h) , q) →
        subst (λ v → ⟨ v ∈ₛ ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆ ⟩) q
          (pairing-ax (⟪ Lset σ ⟫↪ mₓ) (⟪ Lset σ ⟫↪ mᵧ) (⟪ Lset σ ⟫↪ m) .snd
            (subst ⟨_⟩ (DefC.defSet-mem φ m) ∣ (m , h) , refl ∣₁)) })
```

反向包含把层级的配对刻画按另一方向读取。嵌入代表元之对的成员 `w`，仅仅是等于两个条目之一。两个分支各自把相应的代表元交给同一个辅助引理：既然知道 `w` 等于哪个代表元，就能证明 `w` 在该代表元的常元处满足 φ，因而是可定义子集的成员。

```agda
      (∈∈ₛ {a = w} {b = DefC.defSet φ} .snd w∈ₛ)
    sub₂ : ⟨ ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆ ⊆ DefC.defSet φ ⟩
    sub₂ w w∈ₛ = PT.rec (snd (w ∈ₛ DefC.defSet φ))
      (λ { (inl p) → memOf mₓ ∣ inl refl ∣₁ p
         ; (inr p) → memOf mᵧ ∣ inr refl ∣₁ p })
```

辅助引理 `memOf` 接收一个代表元 `mᵢ`、φ 在名指 `mᵢ` 的常元处的满足证明，以及把 `w` 与 `mᵢ` 的嵌入元素等同的路径。`defSet` 的隶属读法把在常元处的满足转成嵌入元素在可定义子集中的隶属；沿路径 (方向为 `sym p`) 搬移，就把这条隶属搬到 `w` 上。两个包含证毕后，外延性给出与嵌入代表元之对的等式，再对构造子 `⁅_,_⁆` 应用 `cong₂`，沿路径 `qₓ` 与 `qᵧ` 把那个对改写成 `⁅ x , y ⁆`。

```agda
      (pairing-ax (⟪ Lset σ ⟫↪ mₓ) (⟪ Lset σ ⟫↪ mᵧ) w .fst w∈ₛ)
      where
      memOf : (mᵢ : ⟪ Lset σ ⟫) → ⟨ (DefC.ι mᵢ ∷ []) DefC.⊨ᵐ φ ⟩
            → w ≡ ⟪ Lset σ ⟫↪ mᵢ → ⟨ w ∈ₛ DefC.defSet φ ⟩
      memOf mᵢ sat p = subst (λ v → ⟨ v ∈ₛ DefC.defSet φ ⟩) (sym p)
```

第一条派生结果把可定义性陈述转成对某一层的隶属。本章前文证明的后继恒等式说 `Lset (sucV σ)` 恰是 `𝒟ₒ (Lset σ)`，故沿该恒等式 (方向取 `sym`) 搬移 `pair∈𝒟ₒ` 的结论，便得 `⟨ ⁅ x , y ⁆ ∈ Lset (sucV σ) ⟩`：一层两个成员的无序对由此得到的上界是下一层。

```agda
        (∈∈ₛ {a = ⟪ Lset σ ⟫↪ mᵢ} {b = DefC.defSet φ} .fst
          (subst ⟨_⟩ (sym (DefC.defSet-mem φ mᵢ)) sat))

pair∈Lset-suc : (σ x y : V ℓ) → ⟨ x ∈ Lset σ ⟩ → ⟨ y ∈ Lset σ ⟩
              → ⟨ ⁅ x , y ⁆ ∈ Lset (sucV σ) ⟩
pair∈Lset-suc σ x y x∈ y∈ =
```

单点集是退化情形。把配对安置对 `x` 施用两次，得到下一层中的 `⁅ x , x ⁆`；层级把 `⁅ x , x ⁆` 等同于 `⁅ x ⁆s` 的 `pair-singleton` 再把这条隶属搬到单点集 `⁅ x ⁆s` 上。

```agda
  subst (λ w → ⟨ ⁅ x , y ⁆ ∈ w ⟩) (sym (Lset-suc σ)) (pair∈𝒟ₒ σ x y x∈ y∈)

sgl∈Lset-suc : (σ x : V ℓ) → ⟨ x ∈ Lset σ ⟩ → ⟨ ⁅ x ⁆s ∈ Lset (sucV σ) ⟩
sgl∈Lset-suc σ x x∈ = subst (λ w → ⟨ w ∈ Lset (sucV σ) ⟩) (pair-singleton x)
  (pair∈Lset-suc σ x x x∈ x∈)

pr∈Lset-suc : (σ x y : V ℓ) → ⟨ x ∈ Lset σ ⟩ → ⟨ y ∈ Lset σ ⟩
```

有序对码 `pr x y` 是以单点集 `⁅ x ⁆s` 与无序对 `⁅ x , y ⁆` 为两个条目的对。两个条目都落在 `Lset (sucV σ)` 中，第一个由单点集结果、第二个由配对结果给出，于是外层无序对可以安置在再高一个的层处：`pr x y` 落在 `Lset (sucV (sucV σ))` 中。由于 Kuratowski 码把一个无序对嵌套在另一个之内，两次使用配对闭包给出有序对码的这个双后继上界，但并不声称它最早恰在此处出现。

```agda
            → ⟨ pr x y ∈ Lset (sucV (sucV σ)) ⟩
pr∈Lset-suc σ x y x∈ y∈ = pair∈Lset-suc (sucV σ) ⁅ x ⁆s ⁅ x , y ⁆
  (sgl∈Lset-suc σ x x∈) (pair∈Lset-suc σ x y x∈ y∈)
```

## 配对

`hasPairL` 先把任意两个可构造集合放进公共层，再施用有界配对构造与唯一性原理。

这条公理的见证是两个实参在公共序数层处的无序对，其可构造性由上一节的引理证明；规格是层级自己对无序对的分类，在底层集合处读取。唯一性则来自外延性。

配对字段以两个实参为参数。谓词 `Q x` 说元素 `x` 等于 `a` 或等于 `b`，其中析取在模型的真值中解释。一个集合实现该字段，是指它的元素恰为满足 `Q` 的元素。构造 `mkPair` 假设已有一个公共序数层包含两个实参的底层集合，而这正是上界步骤所供给的。

```agda
module PairOf (a b : S) where
  Q : S → hProp (ℓ-suc ℓ)
  Q x = (x ≈ˢ a) ⊔ (x ≈ˢ b)

  mkPair : (σ : V ℓ) → IsOrd σ → ⟨ fst a ∈ Lset σ ⟩ → ⟨ fst b ∈ Lset σ ⟩
         → SetOf Q
```

见证是底层集合的周遭无序对，连同其可构造性证书打包。该证书来自有界构造：`Lset σ` 两个成员的对是那里的可定义子集，而引理 `𝒟ₒ→isL` 把序数层的可定义子集抬进 `L`。规格是层级自己对无序对的分类 `pair-spec`，在底层集合处读取；限制载体上的隶属就是周遭隶属，故模型对该字段的解读与层级的分类一致。

```agda
  mkPair σ oσ fa∈ fb∈ = pairElt , (λ z → pair-spec (fst a) (fst b) (fst z))
    where
    pairElt : S
    pairElt = ⁅ fst a , fst b ⁆
            , 𝒟ₒ→isL σ oσ ⁅ fst a , fst b ⁆ (pair∈𝒟ₒ σ (fst a) (fst b) fa∈ fb∈)
```

这个构造还不是那条字段：它需要一层，而手头只有其「仅仅存在」。`build` 用 `PT.rec` 消去 `isL-directed` 的截断，其目标 `∥ SetOf Q ∥₁` 本身就是截断的，因此可以把 `a` 与 `b` 的两份可构造性证书打开到恰好读出公共层与两条隶属的程度，然后在该处运行 `mkPair`。全程没有向外部世界选定任何层。

```agda
  build : ∥ SetOf Q ∥₁
  build = PT.rec squash₁
    (λ { (σ , (oσ , (fa∈ , fb∈))) → ∣ mkPair σ oσ fa∈ fb∈ ∣₁ })
    (isL-directed (fst a) (fst b) (a .snd) (b .snd))

hasPairL : (a b : S) → isContr (SetOf (λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b)))
```

字段 `hasPairL` 要求实现者类型具有收缩性：给出一个典范实现者，以及从中心到任一实现者的路径。公共层的截断上界只被消去到截断存在 `∥ SetOf Q ∥₁` 中；在该消去内部，`mkPair` 由层及两条隶属证明构造实现者。随后 `mere→uniqueL` 借助 `uniqueL` 与外延性，把仅仅存在与唯一性合成为明确的收缩中心。因此，证明不任意选择公共层，而最终结果确实含有 `isContr` 所要求的明确典范实现者。

```agda
hasPairL a b = mere→uniqueL (PairOf.Q a b) (PairOf.build a b)
```

## 并

并不需要寻找上界：一个装着实参的层就足够了。由于层 `Lset σ` 是传递的，`fst a` 的成员的每个成员也仍在该层中，于是有界存在公式「实参的某个成员以我为成员」恰好刻出周遭并 `⋃ (fst a)`。

外延等式由两个包含方向证明。一个方向读出公式的满足：一个见证 `v` 使 `y` 属于 `v`，恰好是层级的并刻画所要求的输入。另一个方向从并刻画出发，必须先把中间成员 `v` 拉进层，而这正是层传递性所做的，施用两次。最后的规格比较两个量词：可构造条件只对载体见证量化，而层级的并律对全部 `V` 量化，`isL-trans` 在两个方向上把这两个范围等同起来。并就位之后，本章已证明五条公理：外延、正则、空集、配对与并。

成员条件 `Q` 是模型真值内部的一条带索引析取：若存在属于 `a` 的某个 `y` 使 `x` 属于 `y`，则 `x` 实现这个并。构造 `mkUnion` 只带一条假设：某个序数层 `σ` 装下 `a` 的底层集合。这里没有第二个实参需要安置，因此与配对不同，无须任何上界序数；`a` 本已有的那一层便够了。

```agda
module UnionOf (a : S) where
  Q : S → hProp (ℓ-suc ℓ)
  Q x = ∃[ y ∶ S ] (y ∈ˢ a) ⊓ (x ∈ˢ y)

  mkUnion : (σ : V ℓ) → IsOrd σ → ⟨ fst a ∈ Lset σ ⟩ → SetOf Q
  mkUnion σ oσ fa∈ = unionElt , spec
```

在层 `Lset σ` 上，公式跑遍该层的小呈现。由 `Lset-layer σ` 与 `layer-trans` 得到的传递性说明：层成员的成员仍属于该层。对给定的 `fst a` 层隶属应用 `∈-asFiber`，得到代表元 `mₐ` 与路径 `qₐ : ⟪ Lset σ ⟫↪ mₐ ≡ fst a`；与上文相同，这是直接取得的纤维数据，并非对外层截断作消去。

```agda
    where
    module DefA = DefOf (Lset σ)
    Atrans = layer-trans (Lset-layer σ)
    mₐ = ∈-asFiber {a = fst a} {b = Lset σ} fa∈ .fst
    qₐ : ⟪ Lset σ ⟫↪ mₐ ≡ fst a
```

公式有一个自由变元槽，是一个有界存在：变元跑遍常元 `mₐ` 的成员，也就是在层内呈现的 `a` 的成员；母式说，约束变元以外部变元为成员。由于约束变元在量词母式中占据第一个槽，外部变元落在后继槽上。被断言的外延是周遭并 `⋃ (fst a)`，等式 `defSet≡` 是一次外延性，分为两个包含。

```agda
    qₐ = ∈-asFiber {a = fst a} {b = Lset σ} fa∈ .snd

    φ : Formula ⟪ Lset σ ⟫ 1
    φ = ∃̇∈ (con mₐ) (var (suc zero) ∈̇ var zero)

    defSet≡ : DefA.defSet φ ≡ ⋃ (fst a)
    defSet≡ = extensionality (DefA.defSet φ) (⋃ (fst a)) (sub₁ , sub₂)
```

第一个包含说：凡满足公式者，都在周遭并中。可定义子集的成员 `y`，经 `defSet` 的读法引理，呈现为索引 `m` 与满足证明组成的截断对，连同把 `y` 与嵌入元素 `⟪ Lset σ ⟫↪ m` 等同的路径 `q`。满足假设是按索引来名指成员的，所以它只能用于嵌入元素；沿 `q` 的搬移把目标从 `y` 移到那个元素，而向命题 `y ∈ₛ ⋃ (fst a)` 的消去保证整步合法。

```agda
      where
      sub₁ : ⟨ DefA.defSet φ ⊆ ⋃ (fst a) ⟩
      sub₁ y y∈ₛ = PT.rec (snd (y ∈ₛ ⋃ (fst a)))
        (λ { ((m , h) , q) →
          subst (λ w → ⟨ w ∈ₛ ⋃ (fst a) ⟩) q
```

有界存在的满足证明仅仅给出一个来自范围的见证 `v`，连同母式的两条隶属：`fst v` 属于嵌入的 `mₐ`，而嵌入的 `m` 属于 `fst v`。这两条恰好是层级的并刻画在进入方向所需的输入：要把 `⟪ Lset σ ⟫↪ m` 放进 `⋃ (fst a)`，只须出示 `fst a` 的某个成员以它为成员。

```agda
            (PT.rec (snd (⟪ Lset σ ⟫↪ m ∈ₛ ⋃ (fst a)))
              (λ { (v , (fstv∈mₐ , m∈fstv)) →
                union-ax (fst a) (⟪ Lset σ ⟫↪ m) .snd
                  ∣ fst v
                  , ( ∈∈ₛ {a = fst v} {b = fst a} .fst
```

但母式的两条隶属说的是限制呈现的语言，必须变成周遭隶属。`∈∈ₛ` 执行转换，而已有的路径 `qₐ` 把范围从嵌入的 `mₐ` 改写为 `fst a`，于是见证 `fst v` 被呈现为 `fst a` 的成员；第二个合取肢按原样使用，因为它本来就是嵌入的 `m` 对 `fst v` 的隶属。两条隶属都成为周遭形式后，并刻画随即适用，第一个包含合拢。

```agda
                        (subst (λ w → ⟨ fst v ∈ w ⟩) qₐ fstv∈mₐ)
                    , ∈∈ₛ {a = ⟪ Lset σ ⟫↪ m} {b = fst v} .fst m∈fstv ) ∣₁ })
              (subst ⟨_⟩ (DefA.defSet-mem φ m) ∣ (m , h) , refl ∣₁)) })
        (∈∈ₛ {a = y} {b = DefA.defSet φ} .snd y∈ₛ)
      sub₂ : ⟨ ⋃ (fst a) ⊆ DefA.defSet φ ⟩
```

反向包含把同一条刻画按另一方向读取：`y` 在周遭并中的隶属，仅仅是 `fst a` 的某个成员 `v` 以 `y` 为成员。辅助引理 `member` 随后必须对这个特定的 `v` 把 `y` 展示在可定义子集中。这一半正是层假设出力的地方，因为到此为止，没有任何东西保证那个中间的 `v` 在层中可见。

```agda
      sub₂ y y∈ₛ = PT.rec (snd (y ∈ₛ DefA.defSet φ))
        (λ { (v , (v∈ₛfa , y∈ₛv)) → member v v∈ₛfa y∈ₛv })
        (union-ax (fst a) y .fst y∈ₛ)
        where
        member : (v : V ℓ) → ⟨ v ∈ₛ fst a ⟩ → ⟨ y ∈ₛ v ⟩
```

辅助引理先把 `y` 转成层的一个代表元 `m'`，连同其等同路径 `q'`，并把 `defSet` 的隶属读法反着用：在名指 `m'` 的常元处的 φ 满足变成嵌入 `m'` 的隶属，沿 `q'` 的搬移再把这条隶属搬到 `y` 上。剩下的只是满足证明 `sat`，它由两条隶属 `v ∈ₛ fst a` 与 `y ∈ₛ v` 组装：经由 `Atrans` 施用层传递性，先证 `v` 落在 `Lset σ` 中，再证 `y` 也如此，两个合取肢则沿路径 `sym qₐ` 与 `sym q'` 被搬到嵌入呈现上。

```agda
               → ⟨ y ∈ₛ DefA.defSet φ ⟩
        member v v∈ₛfa y∈ₛv =
          subst (λ w → ⟨ w ∈ₛ DefA.defSet φ ⟩) q'
            (∈∈ₛ {a = ⟪ Lset σ ⟫↪ m'} {b = DefA.defSet φ} .fst
              (subst ⟨_⟩ (sym (DefA.defSet-mem φ m')) sat))
```

这一块正是层假设出力之处，也是配对所不需要的一步。先用 `∈∈ₛ` 把两条周遭隶属从结构形式读出：`v` 是 `a` 底层集合的成员，`y` 是 `v` 的成员。然后对层的传递性施用两次：既然 `fst a` 落在 `Lset σ` 中而层传递，其成员 `v` 也落在 `Lset σ` 中；对 `y` 属于 `v` 这条隶属再施同一推理，便证得 `y` 自身是层的成员。于是 `a` 的成员的成员被拉进层，这恰好让公式的量词能够看到它。

```agda
          where
          v∈fa = ∈∈ₛ {a = v} {b = fst a} .snd v∈ₛfa
          y∈v = ∈∈ₛ {a = y} {b = v} .snd y∈ₛv
          v∈A = Atrans {x = fst a} {y = v} v∈fa fa∈
          y∈A = Atrans {x = v} {y = y} y∈v v∈A
```

`y` 落在层的证书到手后，纤维转换 `∈-asFiber` 给出代表元 `m'` 及其从嵌入元素回到 `y` 的等同路径 `q'`。随后在截断内组装 φ 在该代表元处的满足证明：见证是 `v` 连同它自身在层中的隶属 `v∈A` 组成的对，而两条母式合取肢被搬到嵌入呈现处，`v` 沿 `sym qₐ` 进入嵌入的 `mₐ`，嵌入的 `m'` 沿 `sym q'` 进入 `v`。这恰好就是有界存在所要求的数据。

```agda
          fib = ∈-asFiber {a = y} {b = Lset σ} y∈A
          m' = fib .fst
          q' = fib .snd
          sat : ⟨ (DefA.ι m' ∷ []) DefA.⊨ᵐ φ ⟩
          sat = ∣ (v , v∈A)
```

两个包含组装成等式 `defSet≡`，识别原则 `𝒟ₒ-intro` 把公式与等式转换为 `⋃ (fst a)` 在 `𝒟ₒ (Lset σ)` 中的隶属。再对闭包引理 `𝒟ₒ→isL` 施用一次便完成构造：既然 `σ` 是序数，`Lset σ` 的可定义子集就可构造，于是 `⋃ (fst a)` 连同其证书被打包成载体元素进入 `L`。下一块将对该打包给出刻画。

```agda
                , ( subst (λ w → ⟨ v ∈ w ⟩) (sym qₐ) v∈fa
                  , subst (λ w → ⟨ w ∈ v ⟩) (sym q') y∈v ) ∣₁

    union∈𝒟ₒ : ⟨ ⋃ (fst a) ∈ 𝒟ₒ (Lset σ) ⟩
    union∈𝒟ₒ = 𝒟ₒ-intro (Lset σ) (⋃ (fst a)) ∣ φ , defSet≡ ∣₁

    unionElt : S
```

规格是一条真值路径，由两块复合而成。层级自己的并律 `union-spec` 把 `fst z` 在周遭并中的隶属分类为跑遍整个层级的带索引析取：存在 `fst a` 中的 `y` 使 `fst z` 属于 `y`。剩下要做的是把这条周遭的带索引析取转成 `Q z`，后者对载体 `S` 量化，也就是只对可构造的见证量化。两个量化范围不同，下一块的桥将把这两条截断的析取等同起来。

```agda
    unionElt = ⋃ (fst a) , 𝒟ₒ→isL σ oσ (⋃ (fst a)) union∈𝒟ₒ

    spec : (z : S) → (z ∈ˢ unionElt) ≡ Q z
    spec z = union-spec (fst a) (fst z) ∙ bridge
      where
      bridge : (∃[ y ∶ (V ℓ) ] (y ∈ fst a) ⊓ (fst z ∈ y)) ≡ Q z
```

桥是这两条截断析取之间的一对映射，由 `⇔toPath` 接成路径。正向：带两条隶属的周遭见证 `y` 获得一份可构造性证书，依据恰恰是 `y` 属于 `fst a`，而 `a` 自身的证书 `a .snd` 就在手边；类的传递性在此处即 `isL-trans` 施于「`y` 的隶属」与「`a` 的证书」，证得 `y` 自身可构造，于是该见证可以被呈现为载体元素而不丢失隶属。反向：载体见证被投影回其底层集合，丢掉证书但保留隶属。两个方向都不检视真值是如何构造的，都作用于抽象的 Ω 值。桥就位后，`spec` 便是复合路径，模型的并字段由此得证。

```agda
      bridge = ⇔toPath
        (PT.map (λ { (y , py) →
          (y , isL-trans {x = fst a} {y = y} (py .fst) (a .snd)) , py }))
        (PT.map (λ { (y , py) → fst y , py }))

  build : ∥ SetOf Q ∥₁
```

组装方式照应配对字段。实参自身的证书 `a .snd` 是截断的，`build` 用 `PT.rec` 把它消去，得到实现集合的截断存在：在证书所名指的层处运行 `mkUnion`，产出见证。字段本身于是是一次唯一性原理的应用，`mere→uniqueL` 把仅仅存在的见证变成收缩性数据，这正是模型 record 每个存在字段所采取的形式。

```agda
  build = PT.rec squash₁ (λ { (σ , (oσ , fa∈)) → ∣ mkUnion σ oσ fa∈ ∣₁ }) (a .snd)

hasUnionL : (a : S) → isContr (SetOf (λ x → ∃[ y ∶ S ] (y ∈ˢ a) ⊓ (x ∈ˢ y)))
hasUnionL a = mere→uniqueL (UnionOf.Q a) (UnionOf.build a)
```

## 小结

本章为可构造宇宙供给五条公理。外延公理与正则公理是继承来的：外延性用传递性处理周遭成员，而正则性直接限制周遭可及性；而一旦载体内部有了外延性，余下每条公理都化归为出示一个见证，因为实现固定隶属条件的集合是唯一的。空集、配对与并是构造出来的：各由一条公式从单一层中刻出；两个实参须会合时，所需的层由上界序数提供。并的规格还第二次展示了传递性的作用：周遭并中的隶属见证，其可构造性证书恰由 `isL-trans` 给出，正是它把模型的限制见证与周遭并的全部见证等同起来。与公理并行，本章还记录了关于塔自身的相应安置事实：`pair∈Lset-suc` 把一层的两个成员的无序对放进下一层，`sgl∈Lset-suc` 放单点集，`pr∈Lset-suc` 把有序对放到高两层处；这正是以有序对写成的任何东西得以安置在某一层上的原因。