有界分离与替换

有界分离所求的不只是可构造集 a 的一个宿主层子类型，而是可构造模型中的一个元素，其成员恰为 a 中满足给定 Δ₀ 公式的 x。有界替换所求的则是函数性 Δ₀ 关系的取值所成之集。两项证明都会先把有关数据放入同一个序数层，在层内形成可定义子集，再把这项层内计算与整个可构造模型中的满足关系比较。

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

从一开始就须区分两层逻辑。公式及其量词属于由模型解释的对象语言；真值可判定这一陈述则属于宿主理论。我们假设后继宇宙层级上的排中律；这项假设经由「为可构造集指派包含它的最早层」这一运算进入证明。它既不是 L 内部断言的公理，也不是选择原则。

open import Base.Prelude
open import Base.Classical using ( LEM )

因此固定宇宙层级 ℓ，并取宿主层假设 lem : LEM (ℓ-suc ℓ)。由此得到的每条定理都在类型中显式保留这一参数。固定层上的论证只以构造方式使用可定义性、传递性与 Δ₀ 绝对性；当任意常元、源集合或选定的像值被指派典范的最早层索引时，经典依赖才实际出现。

module L.Axioms.Separation {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

对象语言使第一种有界性得到精确定义。公式 φ : Formula S n 可以含有来自模型载体 S 的常元，并有 n 个自由变元槽位。证书 Δ₀ φ 表示 φ 中出现的每个量词都由一个词项界定。隶属原子是 Δ₀ 的，合取保持这一性质，有界存在量化也保持这一性质。这三项封闭性保证分离公式与像公式仍是 Δ₀ 的。

open import FOL.ZFStructure using ( Transitive; module hPropStructure )
open import FOL.Syntax
  using ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇
        ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-∧; δ-∃∈ )

另一种有界性约束常元。BoundedTm P t 与 BoundedFo P φ 表示词项或公式中出现的每个常元都满足宿主层谓词 P。它们并不说明公式中的量词是否有界，所以 mkBoundedFo 也适用于非 Δ₀ 公式。给定这种证书，改名会把每个常元换成所选层中的一个索引；映射引理则比较这项语法变换前后的满足关系。

open import FOL.Manipulation.ConstantBounding
  using ( BoundedTm; BoundedFo; BoundedTm-mono; BoundedFo-mono; module Relabel )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
open import FOL.Manipulation.Relabelling using ( ⊨-map )
import FOL.Semantics

为何要把常元移入同一个层？层 Lset σ 有一个小呈现，所以定义其子集的公式以该呈现中的索引为常元；原公式却以 S 的任意元素为常元。完成改名之后，DefOf (Lset σ) 可以在外围累积层级中形成该公式选出的子集，再由可构造性结果把这个子集包装成模型元素。余下的问题是证明：这个在层内定义的子集，与原公式在 L 中指定的成员完全相同。

import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Constructible {ℓ}

层级工具提供两种规模的序数上界。bound2 把两个层索引置于一个共同序数之内，boundingOrd 则对由小类型索引的一族层索引作同样处理；层的单调性随后把成员关系提升到共同上界。运算 stage 为每个可构造集指派一个最早层索引，使相应的层包含该集合；在这项构造中，只有这个最早层运算使用 lem。另一端的 uniqueL 使用模型的集合外延性，从逐点成员规格证明唯一性。

  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-layer; layer-trans; Lset-mono
        ; 𝒟ₒ; 𝒟ₒ-intro; Lset→isL )
open import L.Ordinal {ℓ} using ( ∅-ord; boundingOrd; bound2 )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Axioms.Basic {ℓ} using ( LsetS; 𝒟ₒ→isL; uniqueL )

这里的几种相等各有不同作用。⇔toPath 使用命题外延性，把两个方向的蕴含化为命题值真值之间的路径。由于可构造性证书构成命题，Σ≡Prop 把底层集合的相等提升为模型元素的相等。集合外延性则另经 uniqueL 进入。最后，命题截断只记录见证存在而不保留一个选定见证；仅在目标仍是命题时使用其消去子。

open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Unit using ( tt* )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )

小呈现把模型成员关系与序数界定及层内可定义性所需的小索引类型连接起来。对累积层级中的集合 A，类型 ⟪ A ⟫ 为其呈现的成员编索引，⟪ A ⟫↪ 返回某索引所指名的集合。反过来，∈-asFiber 把成员证明 x ∈ A 化为一个索引，以及从其呈现值到 x 的路径。构造在局部直接使用这份未经截断的纤维数据；这里没有从命题截断中抽取代表。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )

L 上的命题值结构以 S 为模型载体。元素 x : S 是一个依值对，由外围集合 fst x 与证明该集合可构造的 snd x 组成。因此，S 是模型的载体类型，并不是一个名为 L 的集合；其相等与成员关系从底层集合读取，并取值于 hProp。

open hPropStructure 𝒮ʟ

这些公理最终要求该载体实现一个宿主层类 Q : S → hProp (ℓ-suc ℓ)。类型 SetOf Q 把模型元素 b 与如下规格配成一对：对每个 x : S，都有路径 (x ∈ˢ b) ≡ Q x。在分离中，Q x 会把属于源集合这一条件与一项对象语言满足判断合取起来。例如，若公式表示 x 属于常元 c，所求外延就是 a 与 c 的交。证明要用 L 中的一个集合实现这个类；它既不把类本身认作对象语言公式，也不假定宿主理论中的子类型已经属于 L。

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )

现在，同一条对象语言公式可以在两个结构中读取。记号 γ ⊨v φ 表示公式在外围累积层级中、以裸集合环境解释时的满足关系；γ ⊨ φ 则表示公式在以 S 为载体的结构中的满足关系。这两种判断必须保持区分：固定层构造先证明一个关于外围可定义子集的陈述，再用绝对性恢复可构造模型中所需的满足判断。

module SemV = FOL.Semantics 𝒮ᵥ
open SemV.At (V ℓ) id using () renaming ( _⊨_ to _⊨v_ )

可构造类是传递的：可构造集的成员仍可构造。这恰好足以处理有界量词。若一个外围见证属于某个可构造界定词项的解释，就能把它重新包装为 S 的元素；反向则可把内层见证投影回其底层集合。于是对 Δ₀ 公式作归纳便得到 abs₀，即外围真值与内层真值之间的路径。这是 Δ₀ 绝对性，并不声称 L 或任何层对任意公式都是初等的。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL using ( abs₀ ) renaming ( _⊨ᵐ_ to _⊨_ )

替换的像

对替换，先把像写成宿主层谓词。真值 ReplImage a φ z 表示仅仅存在某个 x : S，使 x ∈ˢ a，并且对象语言公式 φ 在环境 x ∷ z ∷ [] 下成立；此处源占零号槽，候选值占一号槽。这个宿主层索引存在采用命题截断，因此忘去究竟由哪个源产生 z；它不同于用一元公式定义同一像时采用的对象语言有界存在 ∃̇∈。该定义本身既不要求 φ 为 Δ₀，也不要求关系具有函数性。

ReplImage : (a : S) (φ : Formula S ) → S → hProp (ℓ-suc ℓ)
ReplImage a φ z = ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((x ∷ z ∷ []) ⊨ φ)

界住函数像

替换多出的困难，是找到一个容纳所有可能取值的层。FunctionalImage 处理任意宿主层关系 R，并假设对每个 x ∈ˢ a，纤维 Σ[ y ∈ S ] ⟨ R x y ⟩ 都可缩。因此，该纤维带有一个指定中心，任何其他相关对都与中心相等。这项假设在每个源处以数据形式给出存在性与唯一性；从这些中心作投影只是依值函数应用，不使用宿主层或对象理论的选择公理。

module FunctionalImage (a : S) (R : S → S → hProp (ℓ-suc ℓ))
                       (fc : (x : S) → ⟨ x ∈ˢ a ⟩
                           → isContr (Σ[ y ∈ S ] ⟨ R x y ⟩)) where

类型 Mem 把一个源元素与它属于 a 的证据包装在一起。可缩纤维假设要求这份证据作为输入，所以只有一个裸的 x : S 并不足够。由于 S 已经位于后继宇宙层级，Mem 太大，不能直接充当 boundingOrd 所需的小索引类型。底层集合 fst a 的典范小呈现提供一种小规模的枚举方式，列出构造上界所需的源成员。

  Mem : Type (ℓ-suc ℓ)
  Mem = Σ[ x ∈ S ] ⟨ x ∈ˢ a ⟩

对 p : Mem，可缩纤维 fc (p .fst) (p .snd) 已经包含其中心。函数 img 投影出该中心的值分量，从而为每个带证书的源成员给出一个确定的模型元素。这看似逐点选取取值，却没有消去任何经过截断的存在：这些中心本来就是所给依值函数 fc 的显式分量。

  img : Mem → S
  img p = fc (p .fst) (p .snd) .fst .fst

中心所含的不只是选定值。其第二分量证明 R (p .fst) (img p) 成立，img-sat 单独命名这项事实。二者的区别很重要：img 给出一个可以界定其所在层的元素，img-sat 则证明这个选定元素确实是该关系在给定源处的取值。

  img-sat : (p : Mem) → ⟨ R (p .fst) (img p) ⟩
  img-sat p = fc (p .fst) (p .snd) .fst .snd

可缩性还把选定中心与每个其他相关对 (y , h) 认同起来。对第一投影取合同，便得到 img p ≡ y，这是完整模型元素的相等，连同其可构造性证书也包括在内。把 img p 放入共同层，再沿这项相等运输成员证明，便可覆盖任意满足 R (p .fst) y 的 y。函数性逐个源使用；它并不表示不同源产生的值彼此不同。

  img-uniq : (p : Mem) (y : S) → ⟨ R (p .fst) y ⟩ → img p ≡ y
  img-uniq p y h = cong fst (fc (p .fst) (p .snd) .snd (y , h))

为得到小索引族，memS 从索引 m : ⟪ fst a ⟫ 出发。该索引所呈现的集合已知属于 fst a。由于 a 可构造且可构造类传递，这个呈现值也可构造，因而能与其证书配成 S 的元素；再加上原有的成员证明，就得到 Mem 的元素，可以对它应用 img 与纤维假设。

  private
    memS : ⟪ fst a ⟫ → Mem
    memS m = (⟪ fst a ⟫↪ m
             , isL-trans fm∈fa (a .snd)) , fm∈fa
      where

局部证明 fm∈fa 给出 memS 的成员分量。典范呈现先在其小成员关系中陈述成员事实，∈∈ₛ 再把该事实转换为累积层级中的命题值成员关系。把传递性施于 fm∈fa 与证书 a .snd，便得到 memS 的可构造性分量。因此，同一项成员事实既把呈现值定位在源集合内，也使它能够被包装成可构造模型元素。

      fm∈fa : ⟨ ⟪ fst a ⟫↪ m ∈ fst a ⟩
      fm∈fa = ∈∈ₛ {a = ⟪ fst a ⟫↪ m} {b = fst a} .snd (∈ₛ⟪ fst a ⟫↪ m)

现在可以沿小类型 ⟪ fst a ⟫ 遍历源集合。对每个索引 m，取包含选定值 img (memS m) 的最早层索引，并以 stage-ord 给出其序数性。构造性的运算 boundingOrd 返回一个严格高于所有这些索引的序数。共同上界论证使用 stage-ord 与 stage-mem 所给的事实，而不需要最小性，尽管典范的 stage 指派也提供了最小性。若 a 为空，索引族也为空，boundingOrd 仍返回一个序数上界，却不因此断言像非空。

    bImg = boundingOrd ⟪ fst a ⟫
      (λ m → stage (fst (img (memS m))) (img (memS m) .snd))
      (λ m → stage-ord (fst (img (memS m))) (img (memS m) .snd))

这一界定结果的第一投影被命名为 βimg。它是序数层索引，并非层本身；相应的层是累积层级中的集合 Lset βimg。range∈βimg 断言每个相关值的底层集合都属于这个层。把 Lset βimg 包装成模型元素是另一项独立运算，并且需要序数性证书。

  βimg : V ℓ
  βimg = bImg .fst

bImg 的第二投影证明上界的两个部分。其中第一部分在此命名为 βimg-ord，证明 βimg 是序数；这使 Lset βimg 能够被包装成模型元素。余下部分则对每个小源索引 m，给出所选值的层索引属于 βimg 的证明。把后一项比较与 stage-mem 合用，就能把每个选定像放入 Lset βimg；再从呈现的源运输到任意源成员，并应用 img-uniq，结论便扩展到与该成员相关的每个值。因此，序数性与值域包含是从同一界定构造中取得的两项不同结论。

  βimg-ord : IsOrd βimg
  βimg-ord = bImg .snd .fst

为界住关系的每个取值，固定 x ∈ˢ a、候选值 y 以及 R x y 的证明。源集成员关系把 x 认同为 a 的规范小表现中的一个成员；函数性继而把 y 认同为该被呈现成员处选定的值。这个选定值属于自己的典范层，而该层的索引严格位于 βimg 之下，所以 Lset-mono 把它抬入 Lset βimg。最后沿取值等式运输，即可得到 y 的层成员证明。因此，同一个层 Lset βimg 容纳关系作用于 a 的成员所得的一切值。前面选取典范层依赖 lem；这里的最终比较与向上运输没有引入更多经典原则。

  range∈βimg : (x : S) → ⟨ x ∈ˢ a ⟩ → (y : S) → ⟨ R x y ⟩
              → ⟨ fst y ∈ Lset βimg ⟩
  range∈βimg x x∈a y h = subst (λ w → ⟨ fst w ∈ Lset βimg ⟩) image≡y
    (Lset-mono {α = βimg} {β = stage (fst (img (memS m))) (img (memS m) .snd)}
      (bImg .snd .snd m) (stage-mem (fst (img (memS m))) (img (memS m) .snd)))

隶属纤维同时给出比较任意源元素与小表现所需的两项数据。第一投影是 fst a 的表现中的索引 m；它本来就包含在这份成员证明中，并非从一个仅知非空的集合中作选择。第二投影给出 m 所呈现的集合与 fst x 之间的等式。由于模型元素的第二分量 isL 是命题值的，不能区分底层集合相同的两个包裹，Σ≡Prop 把这条底层等式提升为 memS m .fst ≡ x。

    where
    m = ∈-asFiber {a = fst x} {b = fst a} x∈a .fst
    q : memS m .fst ≡ x
    q = Σ≡Prop (λ z → snd (isL z))
      (∈-asFiber {a = fst x} {b = fst a} x∈a .snd)

原来的关系证明以 x 为源。沿 q 的逆路径运输后，它成为R (memS m .fst) y 的证明，因而与 fc 在 memS m 处选定的中心落在同一个取值纤维中。该纤维可缩，所以 img-uniq 把中心 img (memS m) 与 y 等同。这正是函数性的用途：比较同一个固定源的两个取值；它并不断言不同源成员的取值彼此不同。

    image≡y : img (memS m) ≡ y
    image≡y = img-uniq (memS m) y (subst (λ z → ⟨ R z y ⟩) (sym q) h)

在固定的层上

固定层论证从序数索引 σ 及其证书 oσ 开始。构造 DefC = DefOf (Lset σ) 通过 Lset σ 的规范小表现处理其成员，并提供以表现索引为常元的公式，以及每条一元公式刻出的子集 defSet。余下任务是把这种层内定义与可构造模型中的满足关系作精确比较。

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

有界公式的绝对性要求所考虑的类具有传递性。这里 DefC.M 是 Lset σ 的成员类，而 layer-trans (Lset-layer σ) 恰好证明：其成员的成员仍在该层中。注意，这份证明不使用序数性证书 oσ；传递性直接来自 Lset-layer σ。正是这种封闭性保证有界量词的见证留在受限世界内。

  Atrans : Transitive 𝒮ᵥ DefC.M
  Atrans = layer-trans (Lset-layer σ)

把 Atrans 交给 DefC.Refine 后，就可使用有界公式的比较结果。改名后的记号_⊨σ_ 表示精炼模块给出的外围 V 值读法：层索引按其所呈现的成员解释，所得公式在周遭层级中求值。特别地，对 Δ₀ 公式，RefC.abs-defSet 将把属于可定义子集与这种外围读法等同；这构成下述语义桥的前半段。

  module RefC = DefC.Refine Atrans
  open RefC.Abs using () renaming ( _⊨ᵛ_ to _⊨σ_ )

谓词 Below c 只表示底层集合 fst c 属于 Lset σ。它用于证明词项或公式中出现的常元有界：BoundedFo Below φ 为 φ 的每个常元保存这样一份证书。它不约束自由变元的赋值，也不约束量词见证；稍后 carveAt 的另一个假设 cover才负责保证满足者落在该层中。

  Below : S → Type (ℓ-suc ℓ)
  Below c = ⟨ fst c ∈ Lset σ ⟩

重标 RL 把每个满足 Below 的模型常元变成小表现 ⟪ Lset σ ⟫ 的一个索引。它的两条语义映射分别是从模型元素取底层集合的 fst，以及从表现索引取其所指集合的 ⟪ Lset σ ⟫↪。给定 fst c ∈ Lset σ 的证明，∈-asFiber 同时返回所需索引和「该索引确实指名 fst c」的等式。这两个投影建立正确重标所需的交换三角形。

  module RL = Relabel {K = S} {K' = ⟪ Lset σ ⟫} {W = V ℓ}
                fst ⟪ Lset σ ⟫↪ Below
                (λ c p → ∈-asFiber {a = fst c} {b = Lset σ} p .fst)
                (λ c p → ∈-asFiber {a = fst c} {b = Lset σ} p .snd)

这座桥比较同一数学赋值的两条满足命题。左侧先由 RL.liftFo 把 φ 的每个常元重标为表现索引，再由 mapFo DefC.ι 把索引解释为其所呈现的成员，最后在周遭层级中于 ⟪ Lset σ ⟫↪ m 求值。右侧则在可构造模型内，于打包后的元素(⟪ Lset σ ⟫↪ m , xL) 处求原公式的值。常元界 h、Δ₀ 证明 dφ 与可构造性证明 xL 分别保证这几次视角转换合法。

  satBridge : (φ : Formula S ) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
              (m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
            → ((⟪ Lset σ ⟫↪ m ∷ []) ⊨σ (mapFo DefC.ι (RL.liftFo φ h)))
              ≡ (((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ)
  satBridge φ h dφ m xL =

前三条路径整理两次相继的常元解释。第一条 ⊨-map 展开层常元的解释DefC.ι；第二条取对称方向，把同一读法改写为经表现映射 ⟪ Lset σ ⟫↪ 的解释。随后把 RL.liftFo-correct 置于满足关系下作同余，以直接经 fst 解释取代「先重标为索引、再把索引指名回来」。最后这一步是由 RL 的交换三角形导出的语法公式等式。

      ⊨-map 𝒮ᵥ DefC.ι fst (RL.liftFo φ h)
        (⟪ Lset σ ⟫↪ m ∷ [])
    ∙ sym (⊨-map 𝒮ᵥ ⟪ Lset σ ⟫↪ id (RL.liftFo φ h)
             (⟪ Lset σ ⟫↪ m ∷ []))
    ∙ cong (λ ψ → (⟪ Lset σ ⟫↪ m ∷ []) ⊨v ψ) (RL.liftFo-correct φ h)

第四条路径再次使用 ⊨-map，把常元与环境都经 fst 读取的外围满足改写为模型元素上的相应公式。至此，原公式与打包后的单元素环境都已就位。最后一条路径取abs₀ 的对称方向：Δ₀ 绝对性把底层集合处的外围真值带回可构造模型内部的真值。所得结果是两个 hProp 之间的等式，故后续论证可沿任一方向运输证明。

    ∙ ⊨-map 𝒮ᵥ fst id φ (⟪ Lset σ ⟫↪ m ∷ [])
    ∙ sym (abs₀ dφ ((⟪ Lset σ ⟫↪ m , xL) ∷ []))

现在可以直接陈述所需的成员规格。对层表现中的索引 m，并给定其所呈现集合可构造的证明 xL，属于提升公式刻出的可定义子集，等同于原公式在 L 中得到满足。左侧使用 Lset σ 的小表现，右侧则把同一被呈现集合包装为模型元素。这条等式因而把层内构造与分离所要实现的谓词连接起来。

  carveSat : (φ : Formula S ) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
             (m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
           → (⟪ Lset σ ⟫↪ m ∈ DefC.defSet (RL.liftFo φ h))
             ≡ (((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ)
  carveSat φ h dφ m xL =

证明复合两条语义等式。首先，RefC.abs-defSet 使用传递性与提升后的 Δ₀ 证书，把属于 DefC.defSet (RL.liftFo φ h) 等同于公式mapFo DefC.ι (RL.liftFo φ h) 在被呈现成员处的外围满足。随后 satBridge 把这条外围命题等同于原公式在可构造模型内的满足。次序在这里不可颠倒：可定义性先抵达周遭层级，模型绝对性再给出最后一环。

    RefC.abs-defSet (RL.liftFo φ h) (RL.Δ₀-liftFo h dφ) m ∙ satBridge φ h dφ m xL

运算 carve 就是 DefC.defSet，这里只为后续构造给它一个稳定名称。将其声明为不透明既不改变所得集合，也不加入新的存在原则；它只阻止自动展开。在数学上，carve ψ 仍是由层表现上的一元公式 ψ 从 Lset σ 中选出的子集。以下引理给出使用这个子集所需的成员关系与可构造性事实。

  opaque
    carve : Formula ⟪ Lset σ ⟫  → V ℓ
    carve ψ = DefC.defSet ψ

公式 ψ 本身见证 carve ψ 是 Lset σ 的可定义子集。构造子 𝒟ₒ-intro 只要求「存在某条公式及其 defSet 与目标集合之间的外延等式」，所以显式数据(ψ , refl) 以 ∣ ψ , refl ∣₁ 放入命题截断。因此，成员命题carve ψ ∈ 𝒟ₒ (Lset σ) 不保留具体是哪条定义公式。这条引理给出前提，稍后𝒟ₒ→isL 将由此前提推出可构造性。此行只引入命题截断，并未从中消去或恢复一条公式。

  opaque
    unfolding carve
    carve∈𝒟ₒ : (ψ : Formula ⟪ Lset σ ⟫ ) → ⟨ carve ψ ∈ 𝒟ₒ (Lset σ) ⟩
    carve∈𝒟ₒ ψ = 𝒟ₒ-intro (Lset σ) (DefC.defSet ψ) ∣ ψ , refl ∣₁

DefC.defSet 产生的每个可定义子集都包含于其环境集合 Lset σ。引理 carve⊆为不透明名称记录这条包含：它用 DefC.defSet⊆A 从 y ∈ carve ψ 得到y ∈ Lset σ。这条包含不依赖 y 是否在可构造模型中满足某条公式；它来自defSet 只遍历该层所呈现成员的定义方式。

    carve⊆ : (ψ : Formula ⟪ Lset σ ⟫ ) (y : V ℓ) → ⟨ y ∈ carve ψ ⟩
           → ⟨ y ∈ Lset σ ⟩
    carve⊆ ψ y mem = DefC.defSet⊆A ψ y mem

carveSat 的正向读法把刻出集合的成员证明变成模型中的满足证明。给定一个被呈现成员属于 carve (RL.liftFo φ h)，沿 hProp 等式 carveSat 作替换，就得到相应模型元素满足 φ 的证明。这里没有另证一条逻辑蕴含；subst 只是把等式左端的元素运输到右端。

    imageOut : (φ : Formula S ) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
               (m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
             → ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo φ h) ⟩
             → ⟨ ((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ ⟩
    imageOut φ h dφ m xL mem = subst ⟨_⟩ (carveSat φ h dφ m xL) mem

反向读法沿同一条等式的相反方向进行。打包后的被呈现成员满足 φ，沿sym (carveSat ...) 运输后便成为刻出集合的成员证明。imageOut 与 imageIn合起来给出逐点对应的两个方向，但此时只适用于固定层中已被呈现的成员；稍后的cover 论证才保证任意满足的模型元素也能在该层中得到表现。

    imageIn : (φ : Formula S ) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
              (m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
            → ⟨ ((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ ⟩
            → ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo φ h) ⟩
    imageIn φ h dφ m xL sat = subst ⟨_⟩ (sym (carveSat φ h dφ m xL)) sat

满足关系不受模型元素所携证明分量的影响。由于每个 isL x 都是命题，底层集合的等式 fst u ≡ fst v 经 Σ≡Prop 提升为 u ≡ v，随后满足证明沿所得单元素环境等式运输。证明体并不查看 dφ，所以这条运输在数学上对任意公式都成立；Δ₀ 参数仍保留在陈述中，尽管证明并未使用它；证明也没有使用排中律。

  opaque
    ⊨-transport : (φ : Formula S ) (dφ : Δ₀ φ) (u v : S) → fst u ≡ fst v
                → ⟨ (u ∷ []) ⊨ φ ⟩ → ⟨ (v ∷ []) ⊨ φ ⟩
    ⊨-transport φ dφ u v p =
      subst (λ z → ⟨ (z ∷ []) ⊨ φ ⟩) (Σ≡Prop (λ x → snd (isL x)) p)

在一层上分离

每个索引 m : ⟪ Lset σ ⟫ 都呈现该层的一个实际成员。规范的小成员证明∈ₛ⟪ Lset σ ⟫↪ m 经 ∈∈ₛ 的第二个方向转换成外围命题⟪ Lset σ ⟫↪ m ∈ Lset σ。由于 σ 是序数，Lset→isL σ oσ 再把这份层成员证明转成可构造性证书，从而能把被呈现集合包装为 S 的元素。固定层构造正是在这里使用 oσ。

  private
    memberIsL : (m : ⟪ Lset σ ⟫) → ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩
    memberIsL m = Lset→isL σ oσ (⟪ Lset σ ⟫↪ m)
      (∈∈ₛ {a = ⟪ Lset σ ⟫↪ m} {b = Lset σ} .snd (∈ₛ⟪ Lset σ ⟫↪ m))

固定层的通用构造接收一元公式 χ、其全部常元满足 Below 的证明、Δ₀ 证书，以及一条覆盖条件：每个满足 χ 的模型元素，其底层集合都属于 Lset σ。目标是给出实现该满足谓词的可缩类型。uniqueL 把目标化为一个带逐点成员规格的显式模型元素：命题外延性先把每个 z 处的双向蕴含变成真值路径，集合外延性再给出实现集合的唯一性。

  carveAt : (χ : Formula S ) (hχ : BoundedFo Below χ) (dχ : Δ₀ χ)
            (cover : (z : S) → ⟨ (z ∷ []) ⊨ χ ⟩ → ⟨ fst z ∈ Lset σ ⟩)
          → isContr (SetOf (λ z → (z ∷ []) ⊨ χ))
  carveAt χ hχ dχ cover = uniqueL (λ z → (z ∷ []) ⊨ χ) (replElt , spec)
    where

选定实现者的底层集合是 carve (RL.liftFo χ hχ)。常元界 hχ 使每个常元重标入该层成为合法操作，而 carve∈𝒟ₒ 证明所得 defSet 属于 Lset σ 的可定义幂集。把 𝒟ₒ→isL σ oσ 施于这份成员证明，就得到模型元素的第二分量。因此，可定义性给出一个可构造实现者的存在；它的精确外延则由另行证明的 spec 确定。

    replElt : S
    replElt = carve (RL.liftFo χ hχ)
            , 𝒟ₒ→isL σ oσ (carve (RL.liftFo χ hχ)) (carve∈𝒟ₒ (RL.liftFo χ hχ))

规格对每个模型元素 z 给出「z 属于 replElt」与「z 满足 χ」之间的路径。正向蕴含从 z ∈ˢ replElt 开始。由于 replElt 的底层集合就是刻出集合，carve⊆把 fst z 放入 Lset σ，规范表现于是给出指名该集合的索引 m。将刻出集合的成员证明运输到被呈现代表后，imageOut 给出该处的满足证明，⊨-transport 再沿底层集合等式把它搬回 z。这个方向无需覆盖假设，因为刻出集合的成员关系已经给出所需的层界。

    spec : (z : S) → (z ∈ˢ replElt) ≡ ((z ∷ []) ⊨ χ)
    spec z = ⇔toPath fwd bwd
      where
      fwd : ⟨ z ∈ˢ replElt ⟩ → ⟨ ((z ∷ []) ⊨ χ) ⟩
      fwd z∈ = ⊨-transport χ dχ (⟪ Lset σ ⟫↪ m , xL) z q (imageOut χ hχ dχ m xL m∈)

这些局部数据把通往规范表现的步骤明确写出。首先，fz∈Lσ 来自刻出集合对该层的包含。把 ∈-asFiber 施于这份成员证明，得到索引 m : ⟪ Lset σ ⟫ 与路径q : ⟪ Lset σ ⟫↪ m ≡ fst z。二者是同一个隶属纤维的两个投影，所以这里不涉及任何选择原则。路径 q 将沿相反方向使用两次：先把刻出集合的成员证明移到被呈现集合，再把打包代表处的满足证明搬回 z。

        where
        fz∈Lσ = carve⊆ (RL.liftFo χ hχ) (fst z) z∈
        m = ∈-asFiber {a = fst z} {b = Lset σ} fz∈Lσ .fst
        q : ⟪ Lset σ ⟫↪ m ≡ fst z
        q = ∈-asFiber {a = fst z} {b = Lset σ} fz∈Lσ .snd

规格的正向方向以两步收尾。层中被表示的成员被打包成模型元素，其可构造性来自层本身；而对那个被表示成员证得的、对刻出集合的隶属，沿命名等式被搬到原元素身上。该方向完成：刻出集合的成员在模型中、于自身处满足公式。

        xL = memberIsL m
        m∈ : ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo χ hχ) ⟩
        m∈ = subst (λ w → ⟨ w ∈ carve (RL.liftFo χ hχ) ⟩) (sym q) z∈

反向方向从覆盖假设开始，此处使用覆盖假设：每个满足公式的元素都位于该层。把这个假设施于给定的满足证明。层隶属的纤维随即恢复出规范代表的索引。

      bwd : ⟨ ((z ∷ []) ⊨ χ) ⟩ → ⟨ z ∈ˢ replElt ⟩
      bwd qz = subst (λ w → ⟨ w ∈ carve (RL.liftFo χ hχ) ⟩) q m∈
        where
        fz∈Lσ = cover z qz
        m = ∈-asFiber {a = fst z} {b = Lset σ} fz∈Lσ .fst

代表由一条等式指名，而满足被搬到它身上。既然满足只依赖底层集合，底层集合之间的等式便已足够；代表被打包成带自身可构造性的模型元素，公式现在对代表成立，而非对原来的元素。

        q : ⟪ Lset σ ⟫↪ m ≡ fst z
        q = ∈-asFiber {a = fst z} {b = Lset σ} fz∈Lσ .snd
        xL = memberIsL m
        satz : ⟨ ((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ χ ⟩
        satz = ⊨-transport χ dχ z (⟪ Lset σ ⟫↪ m , xL) (sym q) qz

现在使用可定义性的正向蕴含：代表满足公式，于是代表属于刻出的集合；命名等式再把这份隶属搬回原元素。两个方向均已完备，而规格在每个元素处都是两条命题的相等：属于刻出的实现，与在模型中满足公式。

        m∈ : ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo χ hχ) ⟩
        m∈ = imageIn χ hχ dχ m xL satz

层上分离把前面的构造专用于子集。其假设为：源集合已在层内；其公式是「属于源」与给定公式的合取，因隶属原子有界、合取保持有界而成为有界公式；其常元有界，因为源被供在层下、公式的常元带着证书。于是固定层定理返回的恰是模型字段的分离所要的那份可缩实现。

  separateAt : (a : S) (fa∈σ : ⟨ fst a ∈ Lset σ ⟩)
               (φ : Formula S ) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
             → isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)))
  separateAt a fa∈σ φ h dφ =
    carveAt ((var zero ∈̇ con a) ∧̇ φ) ((tt* , fa∈σ) , h) (δ-∧ δ-∈ dφ)

固定层定理的覆盖假设只由第一个合取项即可解除。满足该合取的元素满足「属于源」，而源落在层中、层又传递，于是元素也落在层中。这正是分离谓词中隶属合取项并非装饰的数学缘由：是它把每个候选带进了正在刻出子集的那一层之内。

      (λ z q → layer-trans (Lset-layer σ) {x = fst a} {y = fst z} (q .fst) fa∈σ)

找到那一层

为了比较彼此独立选出的界，层条件改为以序数指标为参数。这个谓词的数学内容与前面相同：元素的底集属于该索引所指名的层。这样，原先选定的单个层便成为变量，随后的搜索可以在各层之间量化。

Below′ : V ℓ → S → Type (ℓ-suc ℓ)
Below′ σ c = ⟨ fst c ∈ Lset σ ⟩

第一条提升引理沿指标搬运词项的有界性。若一个层指标先于另一个，则凡落在第一层之下的常元也落在第二层之下，这由塔的严格增长保证；而词项的有界性证书通过在每个常元处逐点施加这条单调性，被搬到更大的指标上。词项本身保持不变；被搬运的只有其有界性证明。

liftTmTo : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → ∀ {n} (t : Term S n)
         → BoundedTm (Below′ σ) t → BoundedTm (Below′ β) t
liftTmTo {σ} {β} σ∈β t h =
  BoundedTm-mono {P = Below′ σ} {Q = Below′ β}
    (λ (c : S) h' → Lset-mono {α = β} {β = σ} σ∈β {x = fst c} h') t h

第二条提升引理对公式做同样的事：一条所有常元都落在某层指标之下的公式，在任何更晚的指标之下仍保持该性质。证明在公式的每个常元位置施加词项引理。有了这两条提升引理，在一个层上得到的有界性证明，可以搬运到为其余数据选定的任何更后层。

liftFoTo : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → ∀ {n} (φ : Formula S n)
         → BoundedFo (Below′ σ) φ → BoundedFo (Below′ β) φ
liftFoTo {σ} {β} σ∈β φ h =
  BoundedFo-mono {P = Below′ σ} {Q = Below′ β}
    (λ (c : S) h' → Lset-mono {α = β} {β = σ} σ∈β {x = fst c} h') φ h

常元之界的搜索从词项开始，而两种情形迥异。常元以自己的最早层为界，连同该指标的序数性以及该常元在其层中的隶属。变元不含常元，于是返回空层与平凡成立的证明；这里没有需要定界的常元，也不声称变元的取值属于空集。

mkBoundedTm : ∀ {n} (t : Term S n) → Σ[ σ ∈ V ℓ ] (IsOrd σ × BoundedTm (Below′ σ) t)
mkBoundedTm (con c) = stage (fst c) (c .snd)
                    , (stage-ord (fst c) (c .snd) , stage-mem (fst c) (c .snd))
mkBoundedTm (var i) = ∅ , (∅-ord , _)

两份搜索结果的合并被一次性、一般地陈述，适用于任何可沿指标提升的两种证书。其输入是一对结果，各自是一个序数指标带其序数性与一份证书；其输出是公共指标处的一个结果，两份证书都被搬运到位。两个提升操作作为参数传入，故同一构造可用于两个词项、两个公式，或一个词项与一个公式。

private
  mkBounded : ∀ {ℓc ℓd} {C : V ℓ → Type ℓc} {D : V ℓ → Type ℓd}
            → (liftC : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → C σ → C β)
            → (liftD : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → D σ → D β)
            → (r₁ : Σ[ σ ∈ V ℓ ] (IsOrd σ × C σ))

公共界的构造分为三步。取两个指标的界，即高于两者的一个序数；记录第一指标先于该界、第二指标亦然；沿这两条包含关系施加两个提升操作，使两份证书都描述公共指标。除「可提升的形状」之外，没有使用证书的任何性质。

            → (r₂ : Σ[ σ ∈ V ℓ ] (IsOrd σ × D σ))
            → Σ[ σ ∈ V ℓ ] (IsOrd σ × (C σ × D σ))
  mkBounded liftC liftD r₁ r₂ = b .fst , (b .snd .fst ,
      ( liftC (b .snd .snd .fst) (r₁ .snd .snd)
      , liftD (b .snd .snd .snd) (r₂ .snd .snd) ))

界本身是序数一章对两个序数的合并：一个被两者皆先于的序数。这是这项递归所需的唯一序数论事实，而且它是构造性的；经典参数不在此处进入，而是更早，在每个常元的最早层被指名之处。

    where
    b  = bound2 (r₁ .fst) (r₂ .fst) (r₁ .snd .fst) (r₂ .snd .fst)

公式之上的搜索沿语法递归。两种原子形式合并其两个词项的界。每个命题联结词合并其两个子公式的界。每种情形都由刚才描述的合并器完成工作，而有界性证明被搬运到公共指标。

mkBoundedFo : ∀ {n} (φ : Formula S n) → Σ[ σ ∈ V ℓ ] (IsOrd σ × BoundedFo (Below′ σ) φ)
mkBoundedFo (t ∈̇ u) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftTmTo σ∈β u) (mkBoundedTm t) (mkBoundedTm u)
mkBoundedFo (t ≐ u) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftTmTo σ∈β u) (mkBoundedTm t) (mkBoundedTm u)
mkBoundedFo (φ ∧̇ ψ) = mkBounded (λ σ∈β → liftFoTo σ∈β φ) (λ σ∈β → liftFoTo σ∈β ψ) (mkBoundedFo φ) (mkBoundedFo ψ)
mkBoundedFo (φ ∨̇ ψ) = mkBounded (λ σ∈β → liftFoTo σ∈β φ) (λ σ∈β → liftFoTo σ∈β ψ) (mkBoundedFo φ) (mkBoundedFo ψ)

余下的情形因其不对称而富有教益。假公式没有常元，所以空层就是一个界。无界量词与其公式体有相同的常元界：量词自身不引入常元，递归从其下方原样通过。有界量词还含有界定词项：其界定词项指名一个常元，故词项的界与公式体的界要合并。

mkBoundedFo (φ ⇒̇ ψ) = mkBounded (λ σ∈β → liftFoTo σ∈β φ) (λ σ∈β → liftFoTo σ∈β ψ) (mkBoundedFo φ) (mkBoundedFo ψ)
mkBoundedFo ⊥̇        = ∅ , (∅-ord , _)
mkBoundedFo (∃̇ φ)    = mkBoundedFo φ
mkBoundedFo (∀̇ φ)    = mkBoundedFo φ
mkBoundedFo (∀̇∈ t φ) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftFoTo σ∈β φ) (mkBoundedTm t) (mkBoundedFo φ)

有界存在与有界全称量词行为一致：界定词项的界与公式体的界合并。整个搜索的一条性质值得强调，因为它区分了两个彼此独立的概念：这场递归只检查常元，所以对含无界量词的公式同样成功。因此这里产出的证书对「公式是否有界」不置一词；「常元落在某层之下」与「量词皆有界」这两个概念全程各自独立。

mkBoundedFo (∃̇∈ t φ) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftFoTo σ∈β φ) (mkBoundedTm t) (mkBoundedFo φ)

Δ₀ 分离

有界分离至此完整陈述。对一个源集合与任何一元公式，只要其量词皆有界，「是源的成员且满足公式」这条谓词就有模型元素给出的可缩实现。证明只需应用一次固定层分离定理，在层算好之后。

separateΔ₀ : (a : S) (φ : Formula S ) → Δ₀ φ
           → isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)))
separateΔ₀ a φ dφ = AtStage.separateAt σ oσ a fa∈σ φ h dφ
  where
  rφ = mkBoundedFo φ

这个层由两个界共同确定。刚构造的搜索为公式中的常元给出一界，而既有的层指派给出容纳源集合的最早层。合并两个指标后，再把公式的证书提升到合并所得的层；于是公式的常元与源集合都落在同一个界之下。

  sa = stage (fst a) (a .snd)
  bb = bound2 (rφ .fst) sa (rφ .snd .fst) (stage-ord (fst a) (a .snd))
  σ  = bb .fst
  oσ = bb .snd .fst
  h  = liftFoTo {σ = rφ .fst} {β = σ} (bb .snd .snd .fst) φ (rφ .snd .snd)

源自身的位置单独处理：它属于自己的最早层，而合并所得的包含关系把这份隶属提升到公共层。这便给出固定层定理所需的覆盖假设，只用到塔的单调性与层指派所附的证书。

  fa∈σ : ⟨ fst a ∈ Lset σ ⟩
  fa∈σ = Lset-mono {α = σ} {β = sa} (bb .snd .snd .snd) (stage-mem (fst a) (a .snd))

Δ₀ 替换

有界替换连同其函数性假设一并陈述。给定源集合、一条量词皆有界的二元公式，并假设每个源成员所对应的值构成可缩纤维，像谓词便有模型元素给出的可缩实现。证明沿谓词的相等搬运可实现性：函数性用来为相关值取得共同的界，得到这个界后，再由普通的分离收集其像。

replaceΔ₀ : (a : S) (φ : Formula S ) → Δ₀ φ
          → ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (x ∷ y ∷ []) ⊨ φ ⟩))
          → isContr (SetOf (ReplImage a φ))
replaceΔ₀ a φ dφ fc =
  subst (λ Q → isContr (SetOf Q)) (sym Q≡)

函数像定界定理按关系的第一槽为源的次序应用，给出公共像层连同其序数性与覆盖事实。随后，在该层打包成模型元素之处，对一元像公式施用完整的有界分离；该公式的有界性证据是有界存在的情形，因为唯一添入的量词被源所界。

    (separateΔ₀ (LsetS βimg βimg-ord) imageFo (δ-∃∈ dφ))
  where
  module I = FunctionalImage a (λ x y → (x ∷ y ∷ []) ⊨ φ) fc
  open I using ( βimg; βimg-ord; range∈βimg )

一元像公式具有如下语义。它以对象语言说：源的某个成员与外侧候选相关，而有界存在把那个成员推进环境的第一个槽。此处的有界存在是对象语言自己的量词；像谓词的外层存在则是宿主层面的截断存在。两者经语义而意义相符，却不是同一个句法对象；区分二者，才能精确陈述下一条相等。

  imageFo : Formula S 
  imageFo = ∃̇∈ (con a) φ

带守卫的谓词收集构造所能核验的东西：候选者落在打包好的公共像层中，并且满足那条一元像公式。层成员这一合取项为分离提供一个界，另一个合取项描述真正的像；因此，随后可借覆盖定理去掉层条件。

  BoundedImage : S → hProp (ℓ-suc ℓ)
  BoundedImage y = (y ∈ˢ LsetS βimg βimg-ord) ⊓ ((y ∷ []) ⊨ imageFo)

两条谓词的相等逐点成立，而其两个方向用力不同。正向：从被截断的源见证走向带守卫的谓词。消去是合法的，因为带守卫的谓词是命题；覆盖事实供给层隶属；同一个源及其满足证明按公式要求的槽位次序重新放入截断。反向：什么都不需要，因为像公式在候选处的满足，按其语义恰是候选处的像谓词；层合取被丢弃，第二个合取项本身即为所求。由于源占据第一个槽位：全程无须任何变元换位。

  Q≡ : ReplImage a φ ≡ BoundedImage
  Q≡ = funExt (λ y → ⇔toPath (into y) (λ p → p .snd))
    where
    into : (y : S) → ⟨ ReplImage a φ y ⟩ → ⟨ BoundedImage y ⟩
    into y = PT.rec (snd (BoundedImage y)) λ { (x , (x∈a , h)) →

对 ReplImage a φ 中的候选者 y，源 x、成员证明 x∈a 与满足证明 h 只在命题截断下给出。由于 BoundedImage y 是命题，PT.rec 可以在构造它的两个合取项时使用这些数据。第一项来自 range∈βimg：函数性蕴涵，与 a 的成员相关的每个值都属于 Lset βimg。对于第二项，把同一个 x、x∈a 与 h 重新放入命题截断。按照 imageFo = ∃̇∈ (con a) φ 的语义，这恰是 y 满足 imageFo 的证明。因此，没有源作为未经截断的数据返回。

由此完成从 ReplImage a φ y 到 BoundedImage y 的蕴涵。再结合舍弃层成员关系分量所得的反向蕴涵，便得到 Q≡；沿 sym Q≡ 运输则证明 replaceΔ₀。准确地说，在假设 lem : LEM (ℓ-suc ℓ)、φ 的 Δ₀ 见证，以及每个 x ∈ˢ a 对应的值纤维均可缩这些条件下，结论是 isContr (SetOf (ReplImage a φ))。这是所陈述的 Δ₀ 替换定理。本分支没有引入额外的经典原理，但 range∈βimg 所使用的公共层之构造依赖 lem。

      range∈βimg x x∈a y h , ∣ x , (x∈a , h) ∣₁ }

小结

有界分离与有界替换遵循同一思路。先把源集合、公式中的常元，以及替换所涉及的全部取值置于同一个序数层之下；随后在该层内借助可定义性形成所需子集，再由重标与 Δ₀ 绝对性把其成员关系认同为可构造模型中的满足关系。由此，在唯一的宿主层假设 lem : LEM (ℓ-suc ℓ) 下得到 separateΔ₀ 与 replaceΔ₀。