在 L 中定位 Skolem 壳及其塌缩

令 M 为所选可构造载体的底层集合。随附的证书保证，此后从 M 提升出的每个元素都是可构造的。

M : S
M = Mʟ .fst

π x 由 x 的元素中同时属于 M 者的塌缩值组成；πX 收集所有 x ∈ M 的取值 π x。这种受限的前驱关系使定义无须假设 M 传递。

module C = Collapse M using ( Fiber; π; π-compute; πX; πX-member; π∈-fwd )

可构造性向元素传递，所以每个 y ∈ M 都可构造。因此可把 y 与该证明配对，视为可构造载体的元素。

memL : (y : S) → ⟨ y ∈ˢ M ⟩ → ⟨ isL y ⟩
memL y y∈M = isL-trans {x = M} {y = y} y∈M (Mʟ .snd)

提升 up 把元素打包为载体元素。第一条引理向外读取塌缩值：π x 的每个元素都是 x 的某个属于 M 的元素的塌缩，其依据是塌缩的计算子句，即恒等式「π x 等于 x 在 M 内元素上的塌缩像」。

up : (y : S) → ⟨ y ∈ˢ M ⟩ → CS.S
up y y∈M = y , memL y y∈M
π-mem-out : (x w : S) → ⟨ w ∈ˢ C.π x ⟩
          → ∥ Σ[ y ∶ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) ∥₁
π-mem-out x w w∈ = map₁ mk (subst (λ u → ⟨ w ∈ˢ u ⟩) (C.π-compute x) w∈)

该转换把塌缩自身的纤维见证变成成员关系陈述：纤维把被呈现的索引与「被呈现元素的塌缩等于 w」的证明配对，而被呈现的元素正是被取塌缩的 x 的元素。

  where
  mk : Σ[ p ∶ C.Fiber x ] (C.π (⟪ x ⟫↪ (p .fst)) ≡ w)
     → Σ[ y ∶ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w))
  mk (p , q) = ⟪ x ⟫↪ (p .fst)
             , ( member x (p .fst)

M 的成员关系使用三个自由变元槽，并由 Relation 在环境 y ∷ x ∷ e ∷ [] 下读取；第三槽携带编码对，而公式断言 y ∈ M、x ∈ M 与 y ∈ x。

               , ∈∈ₛ {a = ⟪ x ⟫↪ (p .fst)} {b = M} .snd (p .snd)
               , q )
private module Membership = Relation Mʟ Mʟ
          ((var i1 ∈̇ con Mʟ) ∧̇ ((var i0 ∈̇ con Mʟ) ∧̇ (var i1 ∈̇ var i0)))

关系的宿主侧读法恰是三条成员关系的合取；正是这种充分性使对象语言公式与外部陈述可以互相代表。

          (λ y x → (y .fst ∈ˢ M) ⊓ ((x .fst ∈ˢ M) ⊓ (y .fst ∈ˢ x .fst)))
          (λ y x z h → h) (λ y x z h → h)

关系成为模型的元素：一个由载体元素之对组成的集合，由两条读式引入与消去。由于关系以载体为界，这个对集足够小，可用分离切出。

R : CS.S
R = Membership.rel

引入读式出示两端点的成员关系及二者之间的成员关系，这正是该关系在此对上的内容。

R-in : (y x : CS.S) → ⟨ y .fst ∈ˢ M ⟩ → ⟨ x .fst ∈ˢ M ⟩ → ⟨ y .fst ∈ˢ x .fst ⟩
     → Holds R y x
R-in y x my mx yx = Membership.into y x my mx (my , mx , yx)

消去读式返回同样的三个成员关系；两个方向合起来说明该关系是充分的，既不强于也不弱于宿主侧陈述。

R-out : (y x : CS.S) → Holds R y x
      → ⟨ y .fst ∈ˢ M ⟩ × ⟨ x .fst ∈ˢ M ⟩ × ⟨ y .fst ∈ˢ x .fst ⟩
R-out = Membership.pair-out

塌缩公式作用于一个取值与一个实参，它是局部的而非全局的。它说：仅存在一张对关系 R 正确、在该实参处完备、且在该实参处取给定值的表 F。它不声称任何全局的函数图；在每个实参处只断言这样的表存在，这正是该公式能在非传递载体上成立的原因。

opaque
  piFo : Formula CS.S 
  piFo = ∃̇ ( correctAt i0 R
           ∧̇ ( completeAt i0 R i2 ∧̇ valueAt i0 R i2 i1 ) )

公式的向外读法把满足拆成三个分量：正确的表、它在实参处的完备性、以及取值子句；每个合取项都由序型章自身的投影从约束子中运出。

  piFo-out : (v p : CS.S) → ⟨ (v ∷ p ∷ []) ⊨ piFo ⟩
           → ∥ Σ[ F ∶ CS.S ] (Correct F R × (Complete F R p × ValueIs F R p v)) ∥₁
  piFo-out v p = map₁ (λ { (F , (hc , (hm , hv))) → F
    , ( correct-out i0 R (F ∷ v ∷ p ∷ []) hc
      , ( complete-out i0 R i2 (F ∷ v ∷ p ∷ []) hm

最内层的投影完成拆包：取值子句作为关于「表在实参处的条目」的普通陈述抵达。

        , value-out i0 R i2 i1 (F ∷ v ∷ p ∷ []) hv ) ) })

向内读法为存在量词选取表 F，并给出其正确性、在实参处的完备性及取值子句的证明。结合向外读法，该公式便与其预期内容精确对应。

  piFo-in : (v p F : CS.S) → Correct F R → Complete F R p → ValueIs F R p v
          → ⟨ (v ∷ p ∷ []) ⊨ piFo ⟩
  piFo-in v p F hc hm hv = ∣ F
    , ( correct-in i0 R (F ∷ v ∷ p ∷ []) hc
      , ( complete-in i0 R i2 (F ∷ v ∷ p ∷ []) hm

唯一性由一次成员关系归纳证明。动机说：对载体的每个可构造元素 x，凡对该关系正确、且在 x 处完备的表，其取值必是 x 的塌缩。可构造性与成员关系都随动机同行，因为表的条目是载体元素组成的对。

        , value-in i0 R i2 i1 (F ∷ v ∷ p ∷ []) hv ) ) ∣₁
private
  Pv : CS.S → S → Type (ℓ-suc ℓ)
  Pv F x = (xL : ⟨ isL x ⟩) → ⟨ x ∈ˢ M ⟩ → (v : CS.S)
         → Complete F R (x , xL) → ValueIs F R (x , xL) v → v .fst ≡ C.π x

归纳沿环境层级的成员关系运行，与塌缩自身的定义方式一致：要证 x 处的动机，就证 x 的每个元素处的动机。

value-val′ : (F : CS.S) → Correct F R → (x : S) → Pv F x
value-val′ F hc = ∈-induction {P = Pv F} go
  where
  go : (x : S) → ((y : S) → ⟨ y ∈ˢ x ⟩ → Pv F y) → Pv F x
  go x IH xL x∈M v cmp val =

步进比较元素：被记录取值与塌缩有相同的元素，而环境层级的外延性把这一点变成相等。实参被呈现为载体元素，故其条目可以载体为类型。

    extensionalV {a = v .fst} {b = C.π x} (λ w → ⇔toPath (fwd w) (bwd w))
    where
    xS : CS.S
    xS = x , xL

向前：被记录取值的元素 w 被载入，取值子句产出一条关系条目及其处的表条目。载入时把从被记录取值承袭来的可构造性与 w 打包。

    fwd : (w : S) → ⟨ w ∈ˢ v .fst ⟩ → ⟨ w ∈ˢ C.π x ⟩
    fwd w w∈ = rec₁ ((w ∈ˢ C.π x) .snd) read (val wS .fst w∈)
      where
      wS : CS.S
      wS = w , isL-trans {x = v .fst} {y = w} w∈ (v .snd)

来源见证分成关系事实 ry 与表项 fy。读取 ry 得到 y ∈ M 与 y ∈ x；把归纳假设用于 fy，便把 w 认同为 π y，而 π∈-fwd 随后把 w 放入 π x。

      read : Σ[ y ∶ CS.S ] (Holds R y xS × Holds F y wS) → ⟨ w ∈ˢ C.π x ⟩
      read (y , (ry , fy)) =
        subst (λ t → ⟨ t ∈ˢ C.π x ⟩) e (C.π∈-fwd x (y .fst) y∈x y∈M)
        where
        y∈M : ⟨ y .fst ∈ˢ M ⟩

关系条目还说该分量低于实参，这就解锁了归纳假设：表在该分量处的取值等于该分量的塌缩。把这条等式与塌缩读法复合，即完成对 w 的认同。

        y∈M = R-out y xS ry .fst
        y∈x : ⟨ y .fst ∈ˢ x ⟩
        y∈x = R-out y xS ry .snd .snd
        e : C.π (y .fst) ≡ w
        e = sym (IH (y .fst) y∈x (y .snd) y∈M wS (hc y wS fy .fst) (hc y wS fy .snd))

向后：塌缩的元素 w 由已证的向外读法分解为载体中实参的某分量，其塌缩为 w。把表在原实参 x 处的完备性用于前驱 y，得到表项 (y,u)。

    bwd : (w : S) → ⟨ w ∈ˢ C.π x ⟩ → ⟨ w ∈ˢ v .fst ⟩
    bwd w w∈ = rec₁ ((w ∈ˢ v .fst) .snd) read (π-mem-out x w w∈)
      where
      read : Σ[ y ∶ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) → ⟨ w ∈ˢ v .fst ⟩
      read (y , (y∈x , y∈M , e)) = rec₁ ((w ∈ˢ v .fst) .snd) inner (cmp yS ry)

该分量被载为载体元素，而该对处的关系条目由两个成员关系与二者之间的成员关系重新引入。

        where
        yS : CS.S
        yS = up y y∈M
        ry : Holds R yS xS
        ry = R-in yS xS y∈M x∈M y∈x

归纳假设把 u 认同为 π y，再沿 π y = w 搬移，即得 w 属于被记录的取值。这正是向后方向所主张的。

        inner : Σ[ u ∶ CS.S ] Holds F yS u → ⟨ w ∈ˢ v .fst ⟩
        inner (u , fu) =
          subst (λ t → ⟨ t ∈ˢ v .fst ⟩) (eu ∙ e) (val u .snd ∣ yS , (ry , fu) ∣₁)
          where
          eu : u .fst ≡ C.π y

等式 eu 是归纳假设在分量 y 处的应用：表在 y 处的取值等于 y 的塌缩。把它与分解所携带的等式复合，条目的取值便被认同于 w，这正是向后方向所要安放的。

          eu = IH y y∈x (yS .snd) y∈M u (hc yS u fu .fst) (hc yS u fu .snd)

把归纳施于载体元素的底层集合，便在受限结构中得到同一唯一性陈述。所得确定性引理说明：塌缩公式若在 M 的元素处成立，其取值必等于该元素的塌缩。

value-val : (F : CS.S) → Correct F R → (x : CS.S) → ⟨ x .fst ∈ˢ M ⟩ → (v : CS.S)
          → Complete F R x → ValueIs F R x v → v .fst ≡ C.π (x .fst)
value-val F hc x = value-val′ F hc (x .fst) (x .snd)
piFo-val : (q : CS.S) → ⟨ q .fst ∈ˢ M ⟩ → (v : CS.S) → ⟨ (v ∷ q ∷ []) ⊨ piFo ⟩
         → v .fst ≡ C.π (q .fst)

证明把截断存在消去到两个 h-集合的相等之中，后者是命题，并对向外读法交出的正确表应用刚证的唯一性。下一个构造从载体中切出落在 L 的某个给定元素之内的元素。

piFo-val q mq v h = rec₁ (setIsSet (v .fst) (C.π (q .fst)))
  (λ { (F , (hc , (hm , hv))) → value-val F hc q mq v hm hv })
  (piFo-out v q h)

module Cut (K : CS.S) where

cutFo : Formula CS.S 
cutFo = var i0 ∈̇ con K

opaque
  cut : CS.S
  cut = hasSeparationL Mʟ cutFo .fst .fst

  cut-mem : (y : CS.S) → (y CS.∈ˢ cut) ≡ ((y CS.∈ˢ Mʟ) ⊓ ((y ∷ []) ⊨ cutFo))
  cut-mem = hasSeparationL Mʟ cutFo .fst .snd

  cut-in : (y : CS.S) → ⟨ y .fst ∈ˢ M ⟩ → ⟨ y .fst ∈ˢ K .fst ⟩ → ⟨ y CS.∈ˢ cut ⟩
  cut-in y my yK = subst ⟨_⟩ (sym (cut-mem y)) (my , yK)

  cut-out : (y : CS.S) → ⟨ y CS.∈ˢ cut ⟩ → ⟨ y .fst ∈ˢ M ⟩ × ⟨ y .fst ∈ˢ K .fst ⟩
  cut-out y h = subst ⟨_⟩ (cut-mem y) h

Good : S → S → Type (ℓ-suc ℓ)
Good δ q = ⟨ q ∈ˢ M ⟩ → ⟨ q ∈ˢ Lset δ ⟩
         → Σ[ qL ∶ ⟨ isL (C.π q) ⟩ ] ((mq : ⟨ q ∈ˢ M ⟩)

「好」的第二分量利用可构造性证明把塌缩包装成 𝒮ʟ 的元素，并断言塌缩公式在该取值与所选的 M 元素呈现上成立。

              → ⟨ ((C.π q , qL) ∷ up q mq ∷ []) ⊨ piFo ⟩)

「好」是命题：对载体的成员关系、对层的成员关系、可构造性与满足各自为命题。这一点至关重要，因为层的分解只返回仅仅存在的见证，而仅仅存在的「好」可以被消费，无须在见证之间挑选。

isPropGood : (δ q : S) → isProp (Good δ q)
isPropGood δ q = isPropΠ2 λ _ _ → isPropΣ ((isL (C.π q)) .snd)
  λ qL → isPropΠ λ mq → (((C.π q , qL) ∷ up q mq ∷ []) ⊨ piFo) .snd

固定序数层 δ'，并假设每个同时属于 M 与 Lset δ' 的 q 都是「好」的。这些较早的塌缩值将被组装成下一实参处的取值。

module Step (δ' : S) (oδ' : IsOrd δ')
            (IH : (q : S) → Good δ' q) where

module Sl = Cut (LsetS δ' oδ') using ( cut; cut-in; cut-out )

Lδ'-trans : {x y : S} → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ Lset δ' ⟩ → ⟨ y ∈ˢ Lset δ' ⟩
Lδ'-trans {x} {y} = layer-trans (Lset-layer δ') {x = x} {y = y}
πʟ : (y : CS.S) → ⟨ y CS.∈ˢ Sl.cut ⟩ → CS.S
πʟ y hy = C.π (y .fst) , IH (y .fst) (Sl.cut-out y hy .fst) (Sl.cut-out y hy .snd) .fst

πʟ-graph : (y : CS.S) (hy : ⟨ y CS.∈ˢ Sl.cut ⟩)
         → ⟨ (πʟ y hy ∷ y ∷ []) ⊨ piFo ⟩
πʟ-graph y hy =
  subst (λ y' → ⟨ (πʟ y hy ∷ y' ∷ []) ⊨ piFo ⟩) (S≡ refl)
    (IH (y .fst) my (Sl.cut-out y hy .snd) .snd my)

  where
  my : ⟨ y .fst ∈ˢ M ⟩
  my = Sl.cut-out y hy .fst

private
  Rπ : Recursion
  Rπ = record
    { dom = Sl.cut ; graph = piFo
    ; funct = λ y hy → (πʟ y hy , πʟ-graph y hy)

        , λ { (v , h) → Σ≡Prop (λ w → ((w ∷ y ∷ []) ⊨ piFo) .snd)
            (sym (S≡ (piFo-val y (Sl.cut-out y hy .fst) v h))) } }

  module T = RecursionGraph Rπ using ( F; F-in; pair-out )

Tab : CS.S
Tab = T.F

Tab-in : (y : CS.S) (hy : ⟨ y CS.∈ˢ Sl.cut ⟩) → Holds Tab y (πʟ y hy)
Tab-in = T.F-in

Tab-pair : (x v : CS.S) → Holds Tab x v
         → ⟨ x CS.∈ˢ Sl.cut ⟩ × (v .fst ≡ C.π (x .fst))
Tab-pair = T.pair-out

Closed : CS.S → Type (ℓ-suc ℓ)
Closed x = (y : S) (y∈x : ⟨ y ∈ˢ x .fst ⟩) (y∈M : ⟨ y ∈ˢ M ⟩)
         → ⟨ up y y∈M CS.∈ˢ Sl.cut ⟩

slice-closed : (x : CS.S) → ⟨ x CS.∈ˢ Sl.cut ⟩ → Closed x
slice-closed x hx y y∈x y∈M =
  Sl.cut-in (up y y∈M) y∈M (Lδ'-trans {x = x .fst} {y = y} y∈x (Sl.cut-out x hx .snd))

complete-of : (x : CS.S) → Closed x → Complete Tab R x
complete-of x cl y ry = ∣ πʟ y' hy' , subst (λ w → ⟨ pr w (C.π (y .fst)) ∈ˢ Tab .fst ⟩) refl (Tab-in y' hy') ∣₁
  where
  ro = R-out y x ry
  y' : CS.S

  y' = up (y .fst) (ro .fst)
  hy' : ⟨ y' CS.∈ˢ Sl.cut ⟩
  hy' = cl (y .fst) (ro .snd .snd) (ro .fst)

valueIs-of : (x : CS.S) → ⟨ x .fst ∈ˢ M ⟩ → Closed x → (v : CS.S) → v .fst ≡ C.π (x .fst)
           → ValueIs Tab R x v
valueIs-of x mx cl v ev w = fwd , bwd
  where
  fwd : ⟨ w .fst ∈ˢ v .fst ⟩ → Src Tab R x w

  fwd w∈ = map₁ read (π-mem-out (x .fst) (w .fst) (subst (λ t → ⟨ w .fst ∈ˢ t ⟩) ev w∈))
    where
    read : Σ[ y ∶ S ] (⟨ y ∈ˢ x .fst ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w .fst))
         → Σ[ y ∶ CS.S ] (Holds R y x × Holds Tab y w)
    read (y , (y∈x , y∈M , e)) = up y y∈M

      , ( R-in (up y y∈M) x y∈M mx y∈x
        , subst (λ t → ⟨ pr y t ∈ˢ Tab .fst ⟩) e (Tab-in (up y y∈M) (cl y y∈x y∈M)) )

  bwd : Src Tab R x w → ⟨ w .fst ∈ˢ v .fst ⟩
  bwd = rec₁ ((w .fst ∈ˢ v .fst) .snd) (λ { (y , (ry , ty)) →
    subst2 (λ s t → ⟨ s ∈ˢ t ⟩) (sym (Tab-pair y w ty .snd)) (sym ev)
      (C.π∈-fwd (x .fst) (y .fst) (R-out y x ry .snd .snd) (R-out y x ry .fst)) })

Tab-correct : Correct Tab R
Tab-correct x v hxv = complete-of x cl , valueIs-of x mx cl v (Tab-pair x v hxv .snd)
  where
  hx : ⟨ x CS.∈ˢ Sl.cut ⟩
  hx = Tab-pair x v hxv .fst

  mx : ⟨ x .fst ∈ˢ M ⟩
  mx = Sl.cut-out x hx .fst
  cl : Closed x
  cl = slice-closed x hx
module At (q : S) (mq : ⟨ q ∈ˢ M ⟩) (q⊆ : (y : S) → ⟨ y ∈ˢ q ⟩ → ⟨ y ∈ˢ Lset δ' ⟩) where

  qS : CS.S
  qS = up q mq

  cl : Closed qS
  cl y y∈q y∈M = Sl.cut-in (up y y∈M) y∈M (q⊆ y y∈q)
  module Mq = Cut qS using ( cut; cut-in; cut-out )

  private
    valR : Recursion
    valR = record
      { dom   = Mq.cut
      ; graph = piFo

      ; funct = λ y hy → mereFunct piFo y (wit y hy) }
      where
      wit : (y : CS.S) (hy : ⟨ y CS.∈ˢ Mq.cut ⟩)
          → ∥ Σ[ v ∶ CS.S ] (⟨ (v ∷ y ∷ []) ⊨ piFo ⟩
                            × ((v' : CS.S) → ⟨ (v' ∷ y ∷ []) ⊨ piFo ⟩ → v' ≡ v)) ∥₁

      wit y hy = ∣ πʟ y hy'
        , ( πʟ-graph y hy'
          , λ v' hv' → S≡ (piFo-val y my v' hv') ) ∣₁
        where
        my : ⟨ y .fst ∈ˢ M ⟩

        my = Mq.cut-out y hy .fst
        hy' : ⟨ y CS.∈ˢ Sl.cut ⟩
        hy' = Sl.cut-in y my (q⊆ (y .fst) (Mq.cut-out y hy .snd))

    module Vq = Of valR using ( table; table-in; table-out )

  val≡π : Vq.table .fst ≡ C.π q
  val≡π = extensionalV {a = Vq.table .fst} {b = C.π q} (λ w → ⇔toPath (fwd w) (bwd w))
    where
    fwd : (w : S) → ⟨ w ∈ˢ Vq.table .fst ⟩ → ⟨ w ∈ˢ C.π q ⟩
    fwd w hw = rec₁ ((w ∈ˢ C.π q) .snd)

      (λ { (y , (hy , h)) →
         subst (λ t → ⟨ t ∈ˢ C.π q ⟩)
           (sym (piFo-val y (Mq.cut-out y hy .fst) wS h))
           (C.π∈-fwd q (y .fst) (Mq.cut-out y hy .snd) (Mq.cut-out y hy .fst)) })
      (Vq.table-out wS hw)

      where
      wS : CS.S
      wS = w , isL-trans {x = Vq.table .fst} {y = w} hw (Vq.table .snd)

    bwd : (w : S) → ⟨ w ∈ˢ C.π q ⟩ → ⟨ w ∈ˢ Vq.table .fst ⟩
    bwd w hw = rec₁ ((w ∈ˢ Vq.table .fst) .snd) read (π-mem-out q w hw)
      where
      read : Σ[ y ∶ S ] (⟨ y ∈ˢ q ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) → ⟨ w ∈ˢ Vq.table .fst ⟩
      read (y , (y∈q , y∈M , e)) =

        subst (λ t → ⟨ t ∈ˢ Vq.table .fst ⟩) e
          (Vq.table-in yS (πʟ yS hy') hy (πʟ-graph yS hy'))
        where
        yS : CS.S
        yS = up y y∈M

        hy : ⟨ yS CS.∈ˢ Mq.cut ⟩
        hy = Mq.cut-in yS y∈M y∈q
        hy' : ⟨ yS CS.∈ˢ Sl.cut ⟩
        hy' = Sl.cut-in yS y∈M (q⊆ y y∈q)

  πq-isL : ⟨ isL (C.π q) ⟩
  πq-isL = subst (λ t → ⟨ isL t ⟩) val≡π (Vq.table .snd)

  good : (mq' : ⟨ q ∈ˢ M ⟩) → ⟨ ((C.π q , πq-isL) ∷ up q mq' ∷ []) ⊨ piFo ⟩
  good mq' = subst (λ q' → ⟨ ((C.π q , πq-isL) ∷ q' ∷ []) ⊨ piFo ⟩) (S≡ refl)
    (piFo-in (C.π q , πq-isL) qS Tab Tab-correct (complete-of qS cl)
      (valueIs-of qS mq cl (C.π q , πq-isL) refl))

good-at : (δ : S) → IsOrd δ → (q : S) → Good δ q

要证 δ 处的「好」，先把 q 对层 Lset δ 的成员关系分解：q 落在更早层 δ' 的可定义幂集内。该分解被消去到「好」之中，因为「好」是命题。

good-at = ∈-induction {P = λ δ → IsOrd δ → (q : S) → Good δ q} go
  where
  go : (δ : S) → ((δ' : S) → ⟨ δ' ∈ˢ δ ⟩ → IsOrd δ' → (q : S) → Good δ' q)
     → IsOrd δ → (q : S) → Good δ q
  go δ IH oδ q mq q∈Lδ = rec₁ (isPropGood δ q) read (Lset-out δ q q∈Lδ) mq q∈Lδ

分解给出低于 δ 的更早层 δ'，以及 q 属于其可定义幂集。利用 δ' 以下的「好」，步进构造得到 q 处的「好」。可定义幂集子句进而说 q 的每个元素都落在层 Lset δ' 内，这正是步进所消费的封闭性假设。

    where
    read : Σ[ δ' ∶ S ] (⟨ δ' ∈ˢ δ ⟩ × ⟨ q ∈ˢ 𝒟ₒ (Lset δ') ⟩) → Good δ q
    read (δ' , (δ'∈δ , q∈𝒟)) _ _ = A.πq-isL , A.good
      where
      oδ' : IsOrd δ'

由 δ' ∈ δ 得到 δ' 的序数性。把归纳假设用于 δ' 以下，并结合可定义幂集所给出的「q 的每个元素都属于 Lset δ'」，即可得到 q 处的「好」，从而闭合 good-at 的成员关系归纳。又因 M 本身属于 L，其可构造性证书给出一个包含 M 的层；该层的传递性于是把 M 的每个元素也放入其中。

      oδ' = mem-ord {A = δ} oδ δ' δ'∈δ
      module A = Step.At δ' oδ' (IH δ' δ'∈δ oδ') q mq (λ y y∈q → 𝒟ₒ∋⊆ (Lset δ') q q∈𝒟 y y∈q)
        using ( πq-isL; good )
π-isL : (y : S) → ⟨ y ∈ˢ M ⟩ → ⟨ isL (C.π y) ⟩
π-isL y y∈M = rec₁ ((isL (C.π y)) .snd)

由证明 Mʟ 取得一个包含可构造载体 M 的层，而该层处的「好」给出 M 每个元素之塌缩的可构造性。下一条结论开始对整个塌缩像 C.πX 的元素作相应论证，同样把截断呈现消去到可构造性。

  (λ { (α , (oα , M∈Lα)) →
     good-at α oα y y∈M (layer-trans (Lset-layer α) {x = M} {y = y} y∈M M∈Lα) .fst })
  (Mʟ .snd)
πX-isL : (x : S) → ⟨ x ∈ˢ C.πX ⟩ → ⟨ isL x ⟩
πX-isL x x∈πX = rec₁ ((isL x) .snd)

πX-isL 的陈述是关于元素的：塌缩像的每个元素都是载体某个元素的塌缩，故可构造。

  (λ { (y , (y∈M , e)) → subst (λ w → ⟨ isL w ⟩) e (π-isL y y∈M) })
  (C.πX-member x x∈πX)

空集也落在该层中；壳机制在这些数据上打开：壳载体 M、「壳包含于该层」以及「起点的每个元素都是壳的元素」。

module HS = HullStage lam ordλ succλ X X⊆L ∅∈λ using ( M )
module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ
  using ( ∅∈Lsetα; hull-member; X⊆M; Hull⊆L )
open HullStage.H.T lam ordλ succλ X X⊆L ∅∈λ public

壳码或是起点元素的基础名，或是 wit k ψ cs，其中保存一条无常元公式及其参数的子码。先求出子码的值，再依是否存在见证，取最小见证或废弃值作为该码的值。

  using ( Code; base; wit; val; vals; search; searchPredicate; Sat; Hull; val-wit
        ; satDecision )
open HullStage.H.T lam ordλ succλ X X⊆L ∅∈λ using ( inHull; _⊨₀_ )

小载体 SL 收集所有命名与搜索所涉的层内元素。参数向量取自集合 Z，指每个分量都属于 Z 的底层集合；步进的搜索只在这样的向量上进行。

SL : Type (ℓ-suc ℓ)
SL = HullStage.ASt.SL lam ordλ succλ X X⊆L ∅∈λ
From : {k : ℕ} → CS.S → Vec SL k → Type (ℓ-suc ℓ)
From {k} Z vs = (i : Fin k) → ⟨ (lookup i vs) .fst ∈ˢ Z .fst ⟩
Searched : CS.S → S → Type (ℓ-suc ℓ)

一次搜索使用元数为 k+1 的无常元公式。取自 Z 的向量给其中 k 个参数变元赋值，余下的变元由候选见证赋值；Sat 断言这样的见证存在。

Searched Z z = Σ[ k ∶ ℕ ] Σ[ ψ ∶ Formula (⊥* {ℓ}) (suc k) ] Σ[ vs ∶ Vec SL k ]
               Σ[ w ∶ Sat k ψ vs ] (From Z vs × (z ≡ (search k ψ vs w) .fst))
Reads : CS.S → S → Type (ℓ-suc ℓ)
Reads Z z = ⟨ z ∈ˢ Z .fst ⟩ ⊎ ((z ≡ ∅) ⊎ Searched Z z)

该包包含运算 Φ、二变元公式 ΦFo，以及证明：对每个 Z，把两个变元分别赋值为 Φ Z 与 Z 的环境满足该公式。

record StepPack : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    Φ       : CS.S → CS.S
    ΦFo     : Formula CS.S 
    defines : (Z : CS.S) → ⟨ (Φ Z ∷ Z ∷ []) ⊨ ΦFo ⟩

其余字段把步进钉死：任何满足该公式的集合都是步进之集；元素递增；废弃值总在；而对取自当前集合参数的每一次搜索，最小见证都被补入。

    only    : (Z Z' : CS.S) → ⟨ (Z' ∷ Z ∷ []) ⊨ ΦFo ⟩ → Z' ≡ Φ Z
    grows   : (Z : CS.S) (z : S) → ⟨ z ∈ˢ Z .fst ⟩ → ⟨ z ∈ˢ (Φ Z) .fst ⟩
    junk    : (Z : CS.S) → ⟨ ∅ ∈ˢ (Φ Z) .fst ⟩
    least   : (Z : CS.S) (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec SL k)
            → From Z vs → (w : Sat k ψ vs) → ⟨ (search k ψ vs w) .fst ∈ˢ (Φ Z) .fst ⟩