基本公理

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

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

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

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

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

open import Cubical.HITs.PropositionalTruncation using ( rec2 )
open import Cubical.Foundations.Prelude using ( isPropIsContr )

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

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

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

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

open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )

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

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 hPropView 𝒮ʟ

语义一侧一次性确定。真值取层级 ℓ-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 σ ⟫  ] (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 = δ} ((x ∈ 𝒟ₒ (Lset σ)) .snd) δ∈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
    (rec₁ ((x ∈ 𝒟ₒ (Lset σ)) .snd) (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 = 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 = map₁ (λ { (i , q) → lower i , q })

module FinOf (σ : V ℓ) (oσ : IsOrd σ) where

module DefC = DefOf (Lset σ)

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

private

  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)

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

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

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

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))

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

          (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) ⟩

  sub₂ y y∈ₛ = rec₁ ((y ∈ₛ DefC.defSet (finDisj n g)) .snd)
    (λ { (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)))

            (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∈𝒟ₒ 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)) ∣₁

  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 = rec2 squash₁ go px py
  where
  Bound : Type (ℓ-suc ℓ)

两条截断由 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 是一条原理：这样的对由其第一投影决定，底层集合 a .fst 与 b .fst 之间的路径已经给出路径 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 = a .fst} {b = b .fst} vwise)
  where
  vwise : (v : V ℓ) → (v ∈ a .fst) ≡ (v ∈ b .fst)

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

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

反向是从 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 = hPropView 𝒮ᵥ

这次抬升是对周遭可及性数据的一次递归。若 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。第二条陈述从仅仅存在出发：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 = 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 组成的截断对。假在对象语言中的满足是空的宿主类型，故 ⊥*-rec h 反驳任何这样的元素。由于包含关系以命题值陈述，向它消去截断是合法的。

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

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

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

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

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

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

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

受层界住的配对

对同一层的两个元素，一条含两个常元的析取公式把其无序对定义为该可定义子集；派生的结果把单点集安置在高一层处，把 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 σ ⟫ 
  φ = (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∈ₛ = rec₁ ((w ∈ₛ ⁅ ⟪ Lset σ ⟫↪ mₓ , ⟪ Lset σ ⟫↪ mᵧ ⁆) .snd)
      (λ { ((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∈ₛ = rec₁ ((w ∈ₛ DefC.defSet φ) .snd)
      (λ { (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 σ → ⟨ a .fst ∈ Lset σ ⟩ → ⟨ b .fst ∈ Lset σ ⟩
       → SetOf Q

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

build : ∥ SetOf Q ∥₁
build = rec₁ squash₁
  (λ { (σ , (oσ , (fa∈ , fb∈))) → ∣ mkPair σ oσ fa∈ fb∈ ∣₁ })
  (isL-directed (a .fst) (b .fst) (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 σ 是传递的，a .fst 的元素的每个元素也仍在该层中，于是有界存在公式「实参的某个元素以我为元素」恰好刻出周遭并 ⋃ (a .fst)。

外延等式由两个包含方向证明。一个方向读出公式的满足：一个见证 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 σ → ⟨ a .fst ∈ Lset σ ⟩ → SetOf Q
mkUnion σ oσ fa∈ = unionElt , spec

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

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

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

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

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

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

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

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

             → ⟨ 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))

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

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

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

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

  unionElt : S

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

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

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

build : ∥ SetOf Q ∥₁

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