Bedrock基本公理
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图造集合运算怎样提升到可构造宇宙中？一个集合属于 L，当且仅当它能呈现为某个序数层 Lset σ 的可定义子集。本章反复使用同一思路：找出一个容纳所需输入的序数层，在该层上写出外延为目标集合的公式，再在周遭集合层级中证明相应的外延等式。
闭包引理 defSet→isL 完成这一过程。给定序数 σ，若仅仅存在一条外延为 x 的一元公式，𝒟ₒ-intro 便认出 x 是 Lset σ 的可定义子集，𝒟ₒ→isL 再把它放入 L。恒等式 Lset (sucV σ) ≡ 𝒟ₒ (Lset σ) 说明了层计算：下一层恰由当前层的可定义子集组成。打包后的集合 LsetS 与 𝒟ₒS 把这两个集合给成载体 S 的元素。
本章以此在 L 中构造空集、无序对与并。外延性利用传递性，把关于可构造成员的一致性推广到所有周遭成员；正则性则递归限制层级的可及性证明。若两个输入需要公共层，bound2 会给出共同的严格上界，而无须比较原来的两层。
设定固定一个宇宙层级 ℓ，并在该层级的累积层级 V 中工作。本章一切都是构造性的：不假设排中律、resize 或选择。公理将据以证明的载体，是 V 的集合连同可构造性证书 isL 组成的类型，而下文每条主张都仅凭周遭集合层级建立。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module L.Axioms.Basic {ℓ : Level} where open import FOL.Syntax using ( Formula; var; con; _≐_; _∈̇_; _∨̇_; ⊤̇; ⊥̇; ∃̇∈ )
闭包模式的刻出步骤在一阶语言中进行。它的公式以某结构的小索引类型为载体，原子谓词是相等与隶属，并备有析取与有界存在量词；这正是可定义性算子所用的构造。关于从结构过渡到子结构，有两条周遭集合层级的事实将发挥作用：限制中两个元素之间的路径已经是其底层集合之间的路径，而继承来的公理要利用的正是这一方向。
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 落在哪个层，将由无序对计算得出。
; 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。
; 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 对两个给定序数返回一个严格包含二者的序数。配对用最后一条把两个可构造实参放进同一层，无须比较原层或选取最大者。有穷索引类型随后描述该层中的有穷像，二元和则表达定义这些像所用的析取。
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，公式因而能用常元指名该成员。这里直接得到数据，是因为相应纤维自身为命题；这一步没有另一个外层截断需要消去。
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 给出下一层的索引。
using ( ∅; ∅-empty; ⁅_,_⁆; ⁅_⁆s; pairing-ax; ⋃_; union-ax ; module InfinitySet ) open InfinitySet using ( sucV ) open hPropStructure 𝒮ʟ
语义一侧一次性确定。真值取层级 ℓ-suc ℓ 上的命题，故公式的解释落在普通的类型构造中；把限制结构经命题值语义读取，便得到结构成员关系 ∈ˢ，以及取命题底层类型的括号记法 ⟨_⟩。一个实现集合于是是载体 S 的元素，即带可构造性证书的集合，连同说明其成员关系实现哪条规格的等式；这就是类型 SetOf Q。原理 setOf-unique 把一个实现集合变成收缩性数据，正是它把本章余下每条公理字段化归为纯粹的存在问题。
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，而后者的结论以同样方式截断，因此全程没有提取或选定任何可构造性见证。
𝒟ₒ→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。这份证书的形状，序数层、定义公式、外延等式，正是本章余下部分反复实例化的模式。
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。
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 β 加上刚构造的证书。经由这个元素，层作为一个普通的载体点进入可构造结构。
LsetS β oβ = Lset β , isL-Lset β oβ
后继层
塔的步进是可定义幂集；在后继索引处，步进就是全部：Lset (sucV σ) 恰是 𝒟ₒ (Lset σ)。这条恒等式作为两个包含来证明。其一，σ 属于自身的后继，所以 𝒟ₒ (Lset σ) 是被并集合之一，其每个元素都属于下一层。其二，Lset (sucV σ) 的成员属于某个 δ ∈ sucV σ 对应的 𝒟ₒ (Lset δ)；若 δ 是 σ 的成员，该集合已在 Lset σ 中，因而是它的可定义子集；若 δ 就是 σ，结论直接成立。两个方向都不使用相对化，也不需要算子的单调性；这里没有 σ 的序数性假设。
有了这条恒等式，可定义幂集的可构造性随之立得：层在下一层可构造，而层的可定义幂集正是那下一层。
两个集合用周遭集合层级的外延性比较，路径化归为一对包含关系。较难的方向需要一条桥引理：从下一层的成员 x 出发，仅仅是存在某个更早层的可定义幂集包含 x，其见证 δ 是 sucV σ 的成员。按 sucV σ 的构造，其成员要么是 σ 的成员，要么是 σ 自身，故这个见证正是论证可以分情况处理的信息。
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 σ) 是命题，这正是截断的见证在此得以消去的前提。
→ ⟨ 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 σ 处的层。两个包含合起来，便得到作为路径的恒等式。
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 σ)；这条恒等式不含 σ 的序数性假设。
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 σ)) ⟩。除这条恒等式外，没有使用算子的任何其他性质。
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 σ) 的载体元素。上一节打包的是层自身，这一节打包的是「一层的可定义子集的全体」。
𝒟ₒ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 的每个方向都是截断内部的一次映射，因为呈现场合中的成员关系按构造就是索引的截断存在。
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 σ 中刻出的那些。
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 无须单射，不同位置可以指名同一个成员。
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) 书写的。两个方向连接的是：可定义子集所看见的「析取被满足」，与像集合所看见的「被族命中」。
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 取命题值。
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 是同时对所有长度陈述的，后继情形中的递归调用无须携带任何额外假设即可使用。
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。第一种情形中，路径把成员与第一个常元等同，公式的左析取支得到满足。第二种情形中，对平移后族施用递归调用得到尾部析取的满足，它成为右析取支。两种情形都在截断内返回答案，故证明从不依赖于命中恰好携带的是哪个索引。
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 记之。剩下的工作只是在结构成员记号与周遭成员记号之间做簿记。
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 ⟩，这正是消去截断得以合法的依据。
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 自身。
(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 属于可定义子集。
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≡ 便作为集合的路径陈述这一相等：由有穷析取刻出的子集就是该族的像，族中的重复也在其内，因为相同的成员由多个常元名指，并不影响像。
(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 的可构造性。
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 上。
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 σ 中的两条隶属。
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β 返回一个同时包含 α 与 β 的序数上界，连同它的序数性和两条隶属。
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，也随之完成整条陈述：任意两个可构造集合「仅仅存在」一个公共的序数层。配对字段要消费的正是它，因为配对需要两个实参在同一层上可见。
, 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 提供。
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 所要求的周遭隶属的逐点路径。
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；任务是把这份数据沿着证书抬上去。
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)，并不是成员证明的一部分。因此，可及性沿底层集合逐成员转移。
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) 是命题，并返回同样的收缩性数据。从这里起，余下每条公理字段都通过展示一个见证、且以截断形式给出，来完成证明。
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 的要求以截断形式给出。
∅∈𝒟ₒ : (σ : V ℓ) → ⟨ ∅ ∈ 𝒟ₒ (Lset σ) ⟩ ∅∈𝒟ₒ σ = 𝒟ₒ-intro (Lset σ) ∅ ∣ ⊥̇ , defSet⊥≡∅ ∣₁ where module DefC = DefOf (Lset σ) defSet⊥≡∅ : DefC.defSet ⊥̇ ≡ ∅
这条等式是对照周遭空集的一次外延，分两个包含方向。第一向是有实质内容的方向：可定义子集的成员 y，经 defSet 的读法引理，呈现为索引 m 与 ⊥̇ 的满足证明 h 组成的截断对。假在对象语言中的满足是空的宿主类型，故 Empty.rec* h 反驳任何这样的成员。由于包含关系以命题值陈述，向它消去截断是合法的。
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 提供：空集可构造，位于其自身之上一个后继。
(∈∈ₛ {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 得到。这是第一条字段，而下两条构造的模式在它身上已经可见：找界、刻出、收尾。
∅ʟ : S ∅ʟ = ∅ , ∅∈L hasEmptyL : isContr (SetOf (λ _ → ⊥)) hasEmptyL = uniqueL _ (∅ʟ , (λ x → empty-spec (fst x)))
受层界住的配对
对同一层的两个成员，一条含两个常元的析取公式把其无序对定义为该可定义子集；派生的结果把单点集安置在高一层处，把 Kuratowski 有序对码安置在高两层处。
一层的两个成员，其无序对是该层的可定义子集：二者各是某个索引的 ⟪ Lset σ ⟫↪，而点名那两个索引的公式恰好定义出这个对。验证它要对照层级自己的配对公理做一次双向外延：可定义子集的成员满足那个析取，故是二者之一；而二者各自满足它，故是成员。
论证里没有一处关乎模型，说的是塔本身的一条事实，故照这样陈述：Kuratowski 编码下的有序对嵌套了两层无序对，因此落在其条目之上两层处。
此处不涉及序数性，后继恒等式也不涉及，理由相同：这里做的是构造，而非比较。单点集是退化的对，而有序对是单点集与对所成的对。
这条陈述只假设 x 与 y 落在层 Lset σ 中；不要求 σ 的序数性，因为刻出一个子集不需要比较层。证书由 𝒟ₒ-intro 组装：一条公式 φ，连同说明 φ 在该层中的外延恰为 ⁅ x , y ⁆ 的等式 defSet≡，并按可定义性算子的接口要求以截断形式给出。
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。呈现嵌入的纤维是命题，所以这里可以直接恢复这些数据；论证没有把隶属假设当作另一个外层截断。
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ᵧ 搬移整条等式。
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≡ =
等同的前一半是一次外延性，从可定义子集到嵌入代表元的对，分为两个包含。此处展示的方向说的是：凡满足 φ 者，都是那两个被点名元素之一。
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 做搬移，包含即告完成。
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 在该代表元的常元处满足 φ，因而是可定义子集的成员。
(∈∈ₛ {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 ⁆。
(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 σ) ⟩：一层两个成员的无序对由此得到的上界是下一层。
(∈∈ₛ {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 上。
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 码把一个无序对嵌套在另一个之内，两次使用配对闭包给出有序对码的这个双后继上界，但并不声称它最早恰在此处出现。
→ ⟨ 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 假设已有一个公共序数层包含两个实参的底层集合，而这正是上界步骤所供给的。
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，在底层集合处读取；限制载体上的隶属就是周遭隶属，故模型对该字段的解读与层级的分类一致。
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。全程没有向外部世界选定任何层。
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 所要求的明确典范实现者。
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 本已有的那一层便够了。
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；与上文相同，这是直接取得的纤维数据，并非对外层截断作消去。
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≡ 是一次外延性，分为两个包含。
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) 的消去保证整步合法。
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 的某个成员以它为成员。
(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 的隶属。两条隶属都成为周遭形式后，并刻画随即适用，第一个包含合拢。
(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 在层中可见。
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' 被搬到嵌入呈现上。
→ ⟨ 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 的成员的成员被拉进层，这恰好让公式的量词能够看到它。
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。这恰好就是有界存在所要求的数据。
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。下一块将对该打包给出刻画。
, ( 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 量化，也就是只对可构造的见证量化。两个量化范围不同，下一块的桥将把这两条截断的析取等同起来。
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 便是复合路径，模型的并字段由此得证。
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 每个存在字段所采取的形式。
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 把有序对放到高两层处；这正是以有序对写成的任何东西得以安置在某一层上的原因。