有界分离与替换

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 所需的小索引类型。底层集合 a .fst 的典范小呈现提供一种小规模的枚举方式，列出构造上界所需的源元素。

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 (λ p → p .fst) (fc (p .fst) (p .snd) .snd (y , h))

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

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

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

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

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

  bImg = boundingOrd ⟪ a .fst ⟫
    (λ m → stage ((img (memS m)) .fst) (img (memS m) .snd))
    (λ m → stage-ord ((img (memS m)) .fst) (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 ⟩
            → ⟨ y .fst ∈ Lset βimg ⟩
range∈βimg x x∈a y h = subst (λ w → ⟨ w .fst ∈ Lset βimg ⟩) image≡y
  (Lset-mono {α = βimg} {β = stage ((img (memS m)) .fst) (img (memS m) .snd)}
    (bImg .snd .snd m) (stage-mem ((img (memS m)) .fst) (img (memS m) .snd)))

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

  where
  m = ∈-asFiber {a = x .fst} {b = a .fst} x∈a .fst
  q : memS m .fst ≡ x
  q = Σ≡Prop (λ z → (isL z) .snd)
    (∈-asFiber {a = x .fst} {b = a .fst} 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)

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

module DefC = DefOf (Lset σ)

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

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

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

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

module RL = Relabel {K = S} {K' = ⟪ Lset σ ⟫} {W = V ℓ}
              (λ p → p .fst) ⟪ Lset σ ⟫↪ Below
              (λ c p → ∈-asFiber {a = c .fst} {b = Lset σ} p .fst)
              (λ c p → ∈-asFiber {a = c .fst} {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.ι (λ p → p .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 𝒮ᵥ (λ p → p .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 都是命题，底层集合的等式 u .fst ≡ v .fst 经 Σ≡Prop 提升为 u ≡ v，随后满足证明沿所得单元素环境等式运输。证明体并不查看 dφ，所以这条运输在数学上对任意公式都成立；Δ₀ 参数仍保留在陈述中，尽管证明并未使用它；证明也没有使用排中律。

opaque
  ⊨-transport : (φ : Formula S ) (dφ : Δ₀ φ) (u v : S) → u .fst ≡ v .fst
              → ⟨ (u ∷ []) ⊨ φ ⟩ → ⟨ (v ∷ []) ⊨ φ ⟩
  ⊨-transport φ dφ u v p =
    subst (λ z → ⟨ (z ∷ []) ⊨ φ ⟩) (Σ≡Prop (λ x → (isL x) .snd) 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 ∷ []) ⊨ χ ⟩ → ⟨ z .fst ∈ 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⊆把 z .fst 放入 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 ≡ z .fst。二者是同一个成员关系纤维的两个投影，所以这里不涉及任何选择原则。路径 q 将沿相反方向使用两次：先把刻出集合的成员关系证明移到被呈现集合，再把打包代表处的满足证明搬回 z。

      where
      fz∈Lσ = carve⊆ (RL.liftFo χ hχ) (z .fst) z∈
      m = ∈-asFiber {a = z .fst} {b = Lset σ} fz∈Lσ .fst
      q : ⟪ Lset σ ⟫↪ m ≡ z .fst
      q = ∈-asFiber {a = z .fst} {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 = z .fst} {b = Lset σ} fz∈Lσ .fst

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

      q : ⟪ Lset σ ⟫↪ m ≡ z .fst
      q = ∈-asFiber {a = z .fst} {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∈σ : ⟨ a .fst ∈ 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 = a .fst} {y = z .fst} (q .fst) fa∈σ)