在 L 中定位 Skolem 壳及其塌缩

凝聚论证需要的不只是外部的 Skolem 壳：壳本身与其塌缩的每个值都必须属于 L。本章通过编码塌缩、把壳写成 ω 迭代来证明这些成员关系。

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

本章在经典逻辑下运行：取模型自身层级后继处的排中律实例。这与选择构造所携带的假设相同，也是本章唯一的经典假设。

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

模块以该假设为参数，因此下文每条陈述都是相对于它而言的，而不诉诸任何笼统的排中律原理。

module L.GCH.ConstructibleHull {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

本章使用集合论的一阶语言：公式构筑于可构造结构的载体之上，其常元指名 L 的元素，且常元可沿任意映射改名，满足关系在改名下不变。这正是描述塌缩与壳所用的词汇。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ∃̇_; ∀̇_; ∀̇∈; ⊥̇ )
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp )
open import FOL.Manipulation.Relabelling using ( ⊨-map )

公式的读法经改名在环境间移动，而改名对满足无害。环境层级提供背景事实：沿隶属的归纳、集合的外延性，以及「元素=索引连同其隶属证明」的呈现方式。

open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV )
open import V.Presentation {ℓ} using ( member; fiber )

论证从 L 中每个集合的居所开始：以序数为索引的层之塔。一个集合的塌缩只由其成员算出，而可构造性沿隶属传递；有待证明的是这场局部计算从不离开 L。由于壳不传递，论证无法援引关于塌缩的全局事实，而必须逐层重新推得取值留在内部。

open import V.Coding {ℓ} using ( pr; module VCode )
open import V.Collapse {ℓ} using ( module Collapse )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-out; Lset→isL; 𝒟ₒ; 𝒟ₒ∋⊆
        ; Lset-layer; layer-trans )

可构造集合 ωʟ 表示周遭的 ω，其规格把它的成员认作内部数码。后文用分离刻出有界切片与单步闭包。这两种运算的结果都仍是 L 的元素，这正是使整个构造留在它所描述的宇宙之内的原因。

open import L.Ordinal {ℓ} using ( mem-ord; #∈ω )
open import L.Axioms.Basic {ℓ} using ( LsetS; ∅ʟ; extensionalL )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ; ω-specL )
open import L.Axioms.Numerals {ℓ} using ( numeralL-fst )

替换把取值装配成表：图可定义的递归成为 L 的元素，而只须每个实参处「仅仅存在」唯一取值。可定义性解释公式的常元；模型内侧的对与数码编码供给条目及其名字。

open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct )
open import L.Recursion.Graph {ℓ} lem using () renaming ( module Graph to RecursionGraph )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; envOverAt; envOverAt-transport )
open import L.Coding.Expressions {ℓ} using ( numL; sucAtL; sucAtL-adequate; consAtL; consAtL-adequate )

环境把参数向量编码为单个集合，向量又可从中恢复；满足桥把内部满足向外部读取；码集把所有码收集为 L 的一个元素；可构造并则把构造沿途收集的各部分合并起来。

open import L.Coding.Environment {ℓ} using ( env; cons )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envS; Ix; envOver; module Recover )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( graph; envFor; envFor-graph )
open import L.Coding.CodeSet {ℓ} lem using ( AllCodes; keyS; key∈AllCodes )
open import L.Coding.CodeConstructibility {ℓ} using ( cupʟ; cupʟ-inl; cupʟ-inr )

一致满足表为每条码指派其满足集，并向外部读取；典范名构造把数码以及无常元公式的码放入 Lset ω，无常元公式仍可带有自由变元槽；某层的内部良序比较其成员，先按诞生层、再按名字。

open import L.Coding.UniformSatisfaction {ℓ} lem using ( val-sat )
open import L.Choice.CanonicalNames {ℓ} lem using ( limitCode; numeral∈limit; pr∈limit )
open import L.Choice.NameComparison {ℓ} lem using ( freeCode-in; freeCode-out )
open import L.Choice.InternalWellOrder {ℓ} lem using ( relL; relL-fill; relL-rep )
open import L.Choice.StageOrders {ℓ} lem using ( orderAt; relOf )

严格良序上的最小元搜索，从有居留者的族返回最小元；关系自身成为带有两条读式的对之集，而序型章陈述描述塌缩表的三条谓词。

open import L.WellOrder.Base {ℓ-suc ℓ}
  using ( SWO; IsLeast; leastOf; isPropLeastOf )
  renaming ( Tri to Tri∙; lt to tri-lt; eq to tri-eq; gt to tri-gt )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( module Relation; isL-ord )
open import L.GCH.OrderType {ℓ} lem

正确性、在实参处的完备性、以及取值子句，各自都是带两条满足读式的公式；内部 ω 递归沿模型自身的 ω 迭代一个可定义的二元步进。壳的成员由任意嵌套深度的码名指，因此任何一次分离都造不出壳；只能沿 ω 迭代一个可定义的单步闭包抵达它，这正是闭包必须构建 ω 次的原因。

  using ( Holds; Complete; Src; ValueIs; Correct
        ; completeAt; complete-in; complete-out
        ; valueAt; value-in; value-out
        ; correctAt; correct-in; correct-out )
open import L.GCH.OmegaRecursion {ℓ} lem using ( module Iterate )

证明分为彼此衔接的两部分。首先，局部塌缩表证明可构造载体的每个塌缩值仍可构造。其次，把 Skolem 壳实现为各有限闭包层的并，从而证明载体本身可构造，并可对它应用第一部分。

open import L.GCH.SkolemHull {ℓ} lem using ( module HullStage; module Frame )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )
open import L.GCH.AdequateStages {ℓ} lem using ( Superadequate )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )
open import L.GCH.CondensationTransfer {ℓ} lem using ( module Condense )

嵌套壳码具有有限深度，其深度由各参数码深度的最大值计算。这个深度给出该码取值出现时所需闭包层的上界。

open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Data.Nat.Properties using ( max )
open import Cubical.Data.Nat.Order using ( _≤_; left-≤-max; right-≤-max )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Sum as Sum

有限参数向量使一个见证码能够依赖有限多个较早取值。空集、单点集与无序二元集提供集合编码，使这些参数及其有序对可在层级内部表示。

import Cubical.Data.Empty as Empty
open import Cubical.Foundations.Prelude using ( subst2; J )
open import Cubical.Data.Vec using ( Vec; _∷_; []; lookup )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ⁅_,_⁆; ⁅_⁆s; module InfinitySet )

冯·诺伊曼后继与数码把有限闭包层组织在 ω 内。无序对还提供构造有序对的原料，而图与环境正以这些有序对编码。

open import V.Model {ℓ} using ( pair-spec )
open InfinitySet {ℓ} using ( ω; sucV; #_ )
open import Cubical.Foundations.HLevels
  using ( isPropΣ; isPropΠ; isPropΠ2 )
open import Cubical.Functions.Logic using ( ⇔toPath )

存在陈述保持命题截断，直到其见证只用于证明另一命题时才予消去。累积层级中的等式是命题，因此塌缩论证在证明集合等式时可以消去这类截断数据。

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ )

这里须区分两层隶属。外围隶属属于累积层级；可构造载体的元素则把外围集合与其可构造性证明打包，而载体上的隶属通过底层集合读取。

open hPropStructure 𝒮ᵥ
module CS = hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )

对于常元为 L 元素的公式，⊨ 表示在 L 的类模型中的满足。沿恒等映射重标常元既不改变环境，也不改变满足关系。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename )

i0 至 i6 共七个名字，缩写前七个 de Bruijn 索引，长环境的每个槽位一个。

private
  i0 : ∀ {k} → Fin (suc k)
  i0 = zero
  i1 : ∀ {k} → Fin (suc (suc k))
  i1 = suc i0

每个后继索引把前一个索引移入更大的有限类型；这些名字逐槽延续。

  i2 : ∀ {k} → Fin (suc (suc (suc k)))
  i2 = suc i1
  i3 : ∀ {k} → Fin (suc (suc (suc (suc k))))
  i3 = suc i2
  i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))

它们表示自由变元位置，后续约束子扩张环境时，其读法随之移动。

  i4 = suc i3
  i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k))))))
  i5 = suc i4
  i6 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc k)))))))
  i6 = suc i5

载体的元素由其底层集合决定，因为可构造性是命题：底层集合相等的两个载体元素相等。凡从同一底层集合重建载体元素之处，辅助 S≡ 都作出这一认同。

  S≡ : {x y : CS.S} → fst x ≡ fst y → x ≡ y
  S≡ = Σ≡Prop (λ v → snd (isL v))

改名 ρs 交换两个槽位：以交换次序书写的关于某对的公式，可在原次序下读取。当步进公式按一种槽序证明、按另一种槽序使用时，就用到它。

  ρs : Fin  → Fin 
  ρs zero = suc zero
  ρs (suc zero) = zero

改名 ρf 保持 w 位于第零槽，并把 Z 从第一槽移到第二槽，越过由候选下一阶段 Z' 占据的中间槽。

  ρf : Fin  → Fin 
  ρf zero = zero
  ρf (suc zero) = suc (suc zero)

ρs 的相合说：交换后的环境在被移动的槽处载有与原环境相同的元素。两个情形都可由自反性证明，因为每个槽都被送到同一元素所在的位置。

  ags : (Z'' w : CS.S) → Ren.Agrees ρs (Z'' ∷ w ∷ []) (w ∷ Z'' ∷ [])
  ags Z'' w zero = refl
  ags Z'' w (suc zero) = refl

固定任意可构造载体 M。

  agf : (w Z' Z : CS.S) → Ren.Agrees ρf (w ∷ Z' ∷ Z ∷ []) (w ∷ Z ∷ [])
  agf w Z' Z zero = refl
  agf w Z' Z (suc zero) = refl

可构造载体的塌缩仍在 L 中

塌缩论证只使用 M 的可构造性以及仍位于其中的前驱，不要求 M 传递。

module PiIn (Mʟ : CS.S) where

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

  M : S
  M = fst Mʟ

π 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 (snd Mʟ)

提升 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∈ = PT.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 → (fst y ∈ˢ M) ⊓ ((fst x ∈ˢ M) ⊓ (fst y ∈ˢ fst x)))
      (λ y x z h → h) (λ y x z h → h)

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

  R : CS.S
  R = Membership.rel

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

  R-in : (y x : CS.S) → ⟨ fst y ∈ˢ M ⟩ → ⟨ fst x ∈ˢ M ⟩ → ⟨ fst y ∈ˢ fst x ⟩
       → 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
        → ⟨ fst y ∈ˢ M ⟩ × ⟨ fst x ∈ˢ M ⟩ × ⟨ fst y ∈ˢ fst x ⟩
  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 = PT.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 → fst v ≡ 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 = fst v} {b = C.π x} (λ w → ⇔toPath (fwd w) (bwd w))
      where
      xS : CS.S
      xS = x , xL

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

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

来源见证分成关系事实 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 (fst y) y∈x y∈M)
          where
          y∈M : ⟨ fst y ∈ˢ M ⟩

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

          y∈M = R-out y xS ry .fst
          y∈x : ⟨ fst y ∈ˢ x ⟩
          y∈x = R-out y xS ry .snd .snd
          e : C.π (fst y) ≡ w
          e = sym (IH (fst y) y∈x (snd y) 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 ∈ˢ fst v ⟩
      bwd w w∈ = PT.rec (snd (w ∈ˢ fst v)) read (π-mem-out x w w∈)
        where
        read : Σ[ y ∈ S ] (⟨ y ∈ˢ x ⟩ × ⟨ y ∈ˢ M ⟩ × (C.π y ≡ w)) → ⟨ w ∈ˢ fst v ⟩
        read (y , (y∈x , y∈M , e)) = PT.rec (snd (w ∈ˢ fst v)) 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 ∈ˢ fst v ⟩
          inner (u , fu) =
            subst (λ t → ⟨ t ∈ˢ fst v ⟩) (eu ∙ e) (val u .snd ∣ yS , (ry , fu) ∣₁)
            where
            eu : fst u ≡ C.π y

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

            eu = IH y y∈x (snd yS) 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) → ⟨ fst x ∈ˢ M ⟩ → (v : CS.S)
            → Complete F R x → ValueIs F R x v → fst v ≡ C.π (fst x)
  value-val F hc x = value-val′ F hc (fst x) (snd x)
  piFo-val : (q : CS.S) → ⟨ fst q ∈ˢ M ⟩ → (v : CS.S) → ⟨ (v ∷ q ∷ []) ⊨ piFo ⟩
           → fst v ≡ C.π (fst q)

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

  piFo-val q mq v h = PT.rec (setIsSet (fst v) (C.π (fst q)))
    (λ { (F , (hc , (hm , hv))) → value-val F hc q mq v hm hv })
    (piFo-out v q h)
  module Cut (K : CS.S) where

切割公式只有一条原子公式：自由槽位属于常元 K。切片所容纳的，恰是满足它的那些元素。

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

把分离施于 Mʟ，切片便作为 L 的元素而得，而不只是成员的类。因此切片可以作为内部递归的定义域使用。

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

隶属规格把「属于切片」等同于「属于载体且满足切割公式」，后者展开即落在 K 的底层集合之中。

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

向内方向把属于 M 与属于 K 的底层集合这两个事实合并，从而把载入后的元素放进切片。

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

向外方向把同一规格读回其两个分量。载体成员 q 在层 δ 处称为「好」，若它属于该层时，既能得到其塌缩的可构造呈现，也能得到 q 处的塌缩公式。

      cut-out : (y : CS.S) → ⟨ y CS.∈ˢ cut ⟩ → ⟨ fst y ∈ˢ M ⟩ × ⟨ fst y ∈ˢ fst K ⟩
      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Σ (snd (isL (C.π q)))
    λ qL → isPropΠ λ mq → snd (((C.π q , qL) ∷ up q mq ∷ []) ⊨ piFo)

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

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

切片在层 Lset δ' 处切出：该层已容纳的载体成员。由于该层是 L 的集合，切片由分离成为 L 的元素，而它恰是归纳假设所谈论的定义域。

    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.π (fst y) , IH (fst y) (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 (fst y) my (Sl.cut-out y hy .snd) .snd my)

该认同使用从切片规格读出的「成员属于载体」；底层集合未曾改变，而由于可构造性的证明是命题，该同一视足以确定所需的运输。

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

在切片上，这些塌缩取值组成以切片为定义域、以 piFo 为图公式的内部递归。可构造性把每个取值给成 𝒮ʟ 的元素，因此图条目是 𝒮ʟ 元素组成的有序对。

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

函数性成立，因为塌缩公式在载体的每个成员处都确定其取值：在同一对处满足公式的任何其他取值都等于它，确定性引理读出这一点。随后，由于其中的可构造性证明是命题值的，便得到相应 𝒮ʟ 元素的相等。

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

L 的图递归收集这张表：一个由载体元素之对组成的集合，其条目恰是切片上的塌缩记录。

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

收集所得的集合就是该层处的表：一个 L 的元素，把每个切片成员与其可构造的塌缩配成对。

    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 ⟩ × (fst v ≡ C.π (fst x))
    Tab-pair = T.pair-out

实参 x 称为封闭，若 x 的每个同时属于 M 的成员都落在层切片中。这个条件须逐实参给出，因为这里并未假定 M 传递。

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

切片成员因层的传递性而封闭：它的任何同时属于 M 的成员仍在该层内，因而属于切片。

    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 = fst x} {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.π (fst y)) ∈ˢ fst Tab ⟩) refl (Tab-in y' hy') ∣₁
      where
      ro = R-out y x ry
      y' : CS.S

该成员被载为载体元素，而封闭性把载入后的元素放进切片，这正是表记录其塌缩时所用的假设。

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

对封闭的实参，取值子句对塌缩自身成立。证明有两个方向：塌缩值的每个成员都来自某个相关成员，而与实参有关系的每个成员都被表载入塌缩值。

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

向前：候选取值 v 的成员 w 经塌缩读法分解为载体中实参的分量，其塌缩等于 w。该分解是截断的存在，而消去的目标是一条命题。

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

该分量先提升为载体元素。它属于实参这一事实给出关系条目，而表条目沿其塌缩与 w 的等式搬运。两条条目合在一起，构成所需的 Src Tab R x w 见证。

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

向后：w 的一条源条目名指一个表取值为 w 的相关成员。对读法把条目拆成隶属与等式；塌缩读法把 w 放进第一分量的塌缩，而两条等式再把它运回被记录取值。

      bwd : Src Tab R x w → ⟨ fst w ∈ˢ fst v ⟩
      bwd = PT.rec (snd (fst w ∈ˢ fst v)) (λ { (y , (ry , ty)) →
        subst2 (λ s t → ⟨ s ∈ˢ t ⟩) (sym (Tab-pair y w ty .snd)) (sym ev)
          (C.π∈-fwd (fst x) (fst y) (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

载体隶属与封闭性补全诸假设；步进模块由载体的实参 q 参数化，其所有成员都低于更早层。这是 Lset δ' 的可定义幂集中的元素所需的情形；此时封闭性由 q⊆ 得出。

      mx : ⟨ fst x ∈ˢ 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 )

q 的塌缩取值被构造为一个内部递归：定义域是 q 在载体内的成员切片，图是塌缩公式。因此，这个函数图满足 L 中替换原理的假设。

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

函数性经由 mereFunct 装配，所需输入是在每个实参处截断存在的唯一取值。见证 wit 在截断内部产出这样的取值连同其满足与唯一性，因为塌缩公式在载体成员处的唯一性是命题。

          ; 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)) ∥₁

见证是全局塌缩值 C.π (fst y)，由归纳假设给出其可构造呈现。层切片上的表供给它的 piFo 证明，piFo-val 供给唯一性。

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

y 在载体中的隶属来自 q 的切片。假设把 q 的每个成员放入 Lset δ'，所以其中每个属于载体的元素都被层切片接纳。

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

替换把该递归的取值收集成 L 的一个元素：其成员恰是 q 中同时属于 M 的成员之可构造塌缩值。

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

表的底层集合与 q 的塌缩一致，由逐成员等价经外延性证明。向前：表的成员是载体中某个成员 y 处的取值，而消去的目标是命题「w 属于 q 的塌缩」。

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

向外读法名指成员 y 及其取值；确定性引理把该取值同认于 y 的塌缩，而塌缩读法把 y 的塌缩放进 q 的塌缩，运输把两者复合。

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

由于 w 属于可构造的取值集合 Vq.table，L 的传递性给出 w 的可构造性，从而把它呈现为 𝒮ʟ 的元素。

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

向后：q 的塌缩的成员分解为载体中 q 的某分量，其塌缩等于该成员；这恰是表记录条目的形式。

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

等式把 w 运到分量的塌缩，而表的向内读式在载入后的分量处产出条目，其记录的恰是该塌缩。

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

载入后的分量因其在载体中的隶属而属于 q 的切片，又因「q 的成员低于更早层」的假设而属于层切片。

            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 的塌缩可构造：它等于表的底层集合，而表是 L 的元素，故可构造性沿该等式运输而来。这是 q 处「好」的第一个子句。

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

「好」的第二个子句是塌缩公式在该塌缩与成员组成的对上成立：表的正确性、封闭实参处的完备性、以及认同取值与塌缩的取值子句。有了两个子句，层归纳即可陈述：在每个序数处的「好」。

归纳沿层级的隶属运行，每步消耗「属于层」的分解。

      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δ = PT.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 = PT.rec (snd (isL (C.π y)))

由证明 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 })
    (snd Mʟ)
  πX-isL : (x : S) → ⟨ x ∈ˢ C.πX ⟩ → ⟨ isL x ⟩
  πX-isL x x∈πX = PT.rec (snd (isL x))

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

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

把 Skolem 壳写成 ω 迭代

这恰是说塌缩像包含于 L；它是关于成员的陈述，并不主张像本身是 L 的元素。前半完成后，后半在新参数下开启：一个对其成员的后继封闭的层 lam，以及成员全部落在该层内的起点 X。

module Telescope (lam : S) (ordλ : IsOrd lam)
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)

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

  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where
  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; Sat; Hull; val-wit )
  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) → ⟨ fst (lookup i vs) ∈ˢ fst Z ⟩
  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 ≡ fst (search k ψ vs w)))
  Reads : CS.S → S → Type (ℓ-suc ℓ)
  Reads Z z = ⟨ z ∈ˢ fst Z ⟩ ⊎ ((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 ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ fst (Φ Z) ⟩
      junk    : (Z : CS.S) → ⟨ ∅ ∈ˢ fst (Φ Z) ⟩
      least   : (Z : CS.S) (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec SL k)
              → From Z vs → (w : Sat k ψ vs) → ⟨ fst (search k ψ vs w) ∈ˢ fst (Φ Z) ⟩

向外的字段在「当前集合低于该层」的前提下，从宿主一侧读取步进的成员：步进的每个成员都是旧成员、废弃值、或某次搜索的取值。穷尽性证明所要消耗的正是这条读法。

      out     : (Z : CS.S) → ((z : S) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
              → (z : S) → ⟨ z ∈ˢ fst (Φ Z) ⟩ → ∥ Reads Z z ∥₁

迭代模块以「起点的可构造性」与打包好的步进为参数。两者缺一不可：内部递归从 L 的一个元素出发，而步进供给公式及其各子句。

  module HullIter (X-isL : ⟨ isL X ⟩) (P : StepPack) where
    open StepPack P

起点被呈现为载体元素，即集合连同其可构造性；这正是内部递归所消费的形式。

    Xʟ : CS.S
    Xʟ = X , X-isL

内部 ω 递归产出诸迭代，其闭包机制把增长字段随身携带：每个迭代包含前一个。诸迭代是模型的集合，而这正是使诸迭代之并成为 L 元素的原因。

    module It = Iterate Xʟ ΦFo Φ defines only
      using ( it; module Closure; iterUnion; iterUnion-in; iterUnion-out; iter; iter-in; iter-out; ω-num; Num )
    module Cl = It.Closure (λ Z z → grows Z (fst z)) using ( it-up )

迭代的各阶段被命名为 hullStep n，即步进对起点的第 n 次应用。

    hullStep : ℕ → CS.S
    hullStep = It.it

迭代由其定义等式支配：把步进应用 n+1 次，所得恰是把单步闭包 Φ 施于第 n 次迭代的结果。该等式由 refl 成立，因为内部 ω 递归在计算后继阶段时直接调用步进运算，无须任何搬运。这正是该构造最赤裸的算术：这一构造的每一层，就是前一层在单一可定义步进之下的闭包。

    hullStep-suc : (n : ℕ) → hullStep (suc n) ≡ Φ (hullStep n)
    hullStep-suc n = refl

迭代随其指标增长：若 n 不超过 n'，则第 n 个迭代所收集的一切仍被第 n' 个迭代收集。步进的增长字段沿差值逐次施加，每次都保留旧成员；数值等式搬运计数，而成员的可构造性随行，因为它属于某个可构造的迭代。这一单调性使「较早迭代中的收集」成为永久的性质。

    hullStep-≤ : (n n' : ℕ) → n ≤ n' → (z : S)
               → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ fst (hullStep n') ⟩
    hullStep-≤ n n' (k , e) z h =
      subst (λ m → ⟨ z ∈ˢ fst (hullStep m) ⟩) e (Cl.it-up n k (z , zL) h)
      where

迭代的单调性由增长字段而来：早前迭代的成员在之后每个迭代中仍是成员，且可构造性随行。壳码的深度由递归指定：基础码深度为零。

见证码比其码向量深一层，因为其取值在诸参数取值之后的下一步才计算。

      zL : ⟨ isL z ⟩
      zL = isL-trans {x = fst (hullStep n)} {y = z} h (snd (hullStep n))
    mutual
      depth : Code → ℕ
      depth (base m) = 

见证构造子在其子码向量的深度上加一。

      depth (wit k ψ cs) = suc (depths cs)

码向量的深度是其各项深度的最大值：向量在其所有各项可得时即可用。

      depths : {m : ℕ} → Vec Code m → ℕ
      depths [] = 
      depths (c ∷ cs) = max (depth c) (depths cs)

一个辅助事实记录了「可判定析取的一支不可能时」情形分裂的行为：若满足为空，则计算出的取值是废弃分支，无论另一支本会说什么。

    private
      stuck-r : {A : Type (ℓ-suc ℓ)} (na : A → Empty.⊥)
                (f : A → SL) (g : (A → Empty.⊥) → SL) (s : A ⊎ (A → Empty.⊥))
              → Sum.rec f g s ≡ g na
      stuck-r na f g (inl a) = Empty.rec (na a)

反驳分支由不可能函数的函数外延性证明：不存在任何成员可以区分二者。

      stuck-r na f g (inr h) = cong g (funExt (λ a → Empty.rec (na a)))

壳入并，前半：每个壳码的取值都安排在以其深度为索引的迭代处。基础码名指起点的成员，它在第零个迭代处已在。

    mutual
      hullStep-in : (c : Code) → ⟨ fst (val c) ∈ˢ fst (hullStep (depth c)) ⟩
      hullStep-in (base m) = member X m
      hullStep-in (wit k ψ cs) = go (lem (Sat k ψ (vals cs) , squash₁))
        where

见证码按其搜索是否可满足分情况。它的深度比参数码向量的深度大一，而相继等式把这一深度处的迭代认作再施行一次 Φ 所得的迭代。

        n : ℕ
        n = depths cs
        go : (s : Sat k ψ (vals cs) ⊎ (Sat k ψ (vals cs) → Empty.⊥))
           → ⟨ fst (Sum.rec (search k ψ (vals cs)) (λ _ → (∅ , HSH.∅∈Lsetα)) s)
                ∈ˢ fst (hullStep (suc n)) ⟩

若搜索被满足，步进的最小见证子句在下一个迭代处补入被搜索的值，其参数由向量深度可得。若搜索不可满足，则无见证可补，步进转而保留废弃值。

        go (inl w) = least (hullStep n) k ψ (vals cs) (vals-in cs) w
        go (inr h) = junk (hullStep n)

码向量的参数在各条目深度的最大值处可得：每项取值都在其自身深度处出现，单调性把它运到消耗该向量的更晚迭代。

      vals-in : {m : ℕ} (cs : Vec Code m) → From (hullStep (depths cs)) (vals cs)
      vals-in (c ∷ cs) zero =
        hullStep-≤ (depth c) (max (depth c) (depths cs)) left-≤-max (fst (val c)) (hullStep-in c)
      vals-in (c ∷ cs) (suc i) =
        hullStep-≤ (depths cs) (max (depth c) (depths cs)) right-≤-max

该选取沿参数向量递归进行。对空向量，空码向量的值向量正合要求；对非空向量，头项的壳成员资格给出它的码，递归则给出尾部各项的码。

          (fst (lookup i (vals cs))) (vals-in cs i)
    private
      choose : {k : ℕ} (vs : Vec SL k)
             → ((i : Fin k) → ⟨ fst (lookup i vs) ∈ˢ Hull ⟩)
             → ∥ Σ[ cs ∈ Vec Code k ] (vals cs ≡ vs) ∥₁

递归步进为头部按壳成员资格取码、为尾部递归取码；取值方程按分量装配，其中载体的相等化归为底层集合的相等。

      choose [] h = ∣ [] , refl ∣₁
      choose (v ∷ vs) h = PT.rec squash₁ (λ { (c , ec) → PT.map
        (λ { (cs , ecs) → (c ∷ cs)
           , cong₂ _∷_ (Σ≡Prop (λ z → snd (z ∈ˢ Lset lam)) ec) ecs })
        (choose vs (λ i → h (suc i))) })

对码向量 cs，val-wit 把 wit k ψ cs 的值与搜索返回的最小见证等同。由于每个码的值都属于壳，该搜索值也属于壳。

        (HSH.hull-member (fst v) (h zero))
      search-val : (k : ℕ) (ψ : Formula (⊥* {ℓ}) (suc k)) (cs : Vec Code k) (vs : Vec SL k)
                 → vals cs ≡ vs → (w : Sat k ψ vs) → ⟨ fst (search k ψ vs w) ∈ˢ Hull ⟩
      search-val k ψ cs vs e w =
        J (λ vs' e' → (w' : Sat k ψ vs') → ⟨ fst (search k ψ vs' w') ∈ˢ Hull ⟩)

路径归纳沿参数向量之间的同定搬运该陈述，而见证码在壳内受判。

          (λ w' → subst (λ z → ⟨ fst z ∈ˢ Hull ⟩) (val-wit k ψ cs w') (inHull (wit k ψ cs)))
          e w

码 wit 0 ⊥̇ [] 没有满足见证，因此其值走失败分支并等于 ∅。每个码的值都在壳中，所以废弃值也在壳中。

      junk∈Hull : ⟨ ∅ ∈ˢ Hull ⟩
      junk∈Hull = subst (λ z → ⟨ fst z ∈ˢ Hull ⟩)
        (stuck-r no (search  ⊥̇ []) (λ _ → (∅ , HSH.∅∈Lsetα)) (lem (Sat  ⊥̇ [] , squash₁)))
        (inHull (wit  ⊥̇ []))
        where

没有环境满足假式：展开这样的满足证明会得到空类型的元素。

        no : Sat  ⊥̇ [] → Empty.⊥
        no = PT.rec Empty.isProp⊥ (λ { (a , h) → Empty.rec* h })

并入壳，后半：每个迭代的每个成员都在壳内，对迭代指标归纳。基础情形是起点，其成员由壳章即是壳成员。

    hullStep⊆Hull : (n : ℕ) (z : S) → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ Hull ⟩
    hullStep⊆Hull zero z h = HSH.X⊆M z h
    hullStep⊆Hull (suc n) z h = PT.rec (snd (z ∈ˢ Hull)) read
      (out (hullStep n) (λ z' hz' → HSH.Hull⊆L z' (hullStep⊆Hull n z' hz')) z h)
      where

步进情形经向外子句读取后继迭代的成员：它是旧成员，由归纳假设已在壳内；是废弃值，已在壳内；或是被搜索的值，交由下一步处理。

      read : Reads (hullStep n) z → ⟨ z ∈ˢ Hull ⟩
      read (inl h') = hullStep⊆Hull n z h'
      read (inr (inl e)) = subst (λ t → ⟨ t ∈ˢ Hull ⟩) (sym e) junk∈Hull
      read (inr (inr (k , ψ , vs , w , from , e))) =
        subst (λ t → ⟨ t ∈ˢ Hull ⟩) (sym e)

被搜索的值与其参数的码向量相匹配，每个参数由归纳假设是壳成员；于是该搜索经 search-val 落在壳内，等式再把这一成员资格运给 z。诸迭代的并被命名为呈现壳的 L 元素。

          (PT.rec (snd (fst (search k ψ vs w) ∈ˢ Hull))
            (λ { (cs , ecs) → search-val k ψ cs vs ecs w })
            (choose vs (λ i → hullStep⊆Hull n (fst (lookup i vs)) (from i))))
    hullL : CS.S
    hullL = It.iterUnion

作为 L 元素的壳是诸迭代的并，其隶属描述说它的成员恰是壳的成员。向前：并的成员落在某个迭代处，故在壳内。

    hullL-spec : fst hullL ≡ Hull
    hullL-spec = extensionalV {a = fst hullL} {b = Hull} (λ z → ⇔toPath (fwd z) (bwd z))
      where
      fwd : (z : S) → ⟨ z ∈ˢ fst hullL ⟩ → ⟨ z ∈ˢ Hull ⟩
      fwd z h = PT.rec (snd (z ∈ˢ Hull))

迭代指标由并的向外读法消去，成员的可构造性则由这个并继承；该并依构造即为可构造集合。

        (λ { (n , hn) → hullStep⊆Hull n z hn })
        (It.iterUnion-out (z , isL-trans {x = fst hullL} {y = z} h (snd hullL)) h)

向后：壳成员由某个码名指，其取值出现在以该码深度为索引的迭代处；并的向内读式接纳它。

      bwd : (z : S) → ⟨ z ∈ˢ Hull ⟩ → ⟨ z ∈ˢ fst hullL ⟩
      bwd z h = PT.rec (snd (z ∈ˢ fst hullL))
        (λ { (c , ec) → It.iterUnion-in (depth c) zS
               (subst (λ t → ⟨ t ∈ˢ fst (hullStep (depth c)) ⟩) ec (hullStep-in c)) })
        (HSH.hull-member z h)

被名指的成员被载入载体：其可构造性由「壳包含于该层」而来，而该层的元素呈现供给了证书。

        where
        zS : CS.S
        zS = z , Lset→isL lam ordλ z (HSH.Hull⊆L z h)

底层集合的相等把并的可构造性传递给壳：壳是 L 的元素。本章前半至此全部清偿，第二个模块则建造刚才被迭代所消费的可定义步进。

步进在该层内部建造，其常元名指该层的对象：lam 的可构造性由「lam 是序数」而来。

    M-isL : ⟨ isL HS.M ⟩
    M-isL = subst (λ t → ⟨ isL t ⟩) hullL-spec (snd hullL)
  module Build where

层级的序数可构造，这把该层锚定在 L 之内。

    λ-isL : ⟨ isL lam ⟩
    λ-isL = isL-ord lam ordλ

A 把 Lset lam 连同其可构造性证明呈现为模型元素；满足图以及该层上的公式编码都以它为层参数。

    A : CS.S
    A = LsetS lam ordλ

该层上的满足图一次性供给所有码的满足集，连同两条读式；层上的可定义性把公式的常元解释为层的元素。

    module SM = SatGraph A using ( pairs; pairs-in; pairs-out; valOf; valOf≡ )
    module DA = DefOf (Lset lam) using ( ι; _⊨ᵐ_; 𝒮M )

空字母表处的码集收集无常元公式的码。这些公式可以带有自由变量；它们缺少的是常元，而自由变量将由搜索的参数环境赋值。

    C₀ : CS.S
    C₀ = AllCodes ∅ʟ

该层的内部良序被呈现为模型的元素，即比较最小见证所用的关系。

    Rel : CS.S
    Rel = relL lam λ-isL ordλ

小载体上的严格良序由该关系读取；其比较在载体元素上陈述。可构造有序对的第二分量也可构造，这正是一会儿名字的参数所需要的。

    wL : SWO SL
    wL = orderAt lam ordλ
    relOf-at : SL → SL → Type (ℓ-suc ℓ)
    relOf-at = relOf wL
    pr-snd-isL : (a b : V ℓ) → ⟨ isL (pr a b) ⟩ → ⟨ isL b ⟩

证明经由单点集把有序对剥开两次：属于一对把第二分量放进「单点集-对」的嵌套中，而每次剥开都由传递性保持可构造性。

    pr-snd-isL a b h =
      isL-trans {x = ⁅ a , b ⁆} {y = b} (subst ⟨_⟩ (sym (pair-spec a b b)) ∣ inr refl ∣₁)
        (isL-trans {x = pr a b} {y = ⁅ a , b ⁆}
          (subst ⟨_⟩ (sym (pair-spec ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a , b ⁆)) ∣ inr refl ∣₁) h)

数码被呈现为载体元素：有限序数连同其可构造性，见证公式的键子句将对它们量化。

    nn : ℕ → CS.S
    nn k = # k , numL k

由于常元字母表为空，存在唯一的解释 ε′ 映入该层载体。借此可把无常元公式改名到该层语言中，而无须作任何选择。

    ε′ : ⊥* {ℓ} → ⟪ Lset lam ⟫
    ε′ = Empty.rec*
    sat-bridge : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) (δ : SL ^ k)
               → (δ ⊨₀ χ) ≡ (δ DA.⊨ᵐ mapFo ε′ χ)
    sat-bridge k χ δ =

这座桥是一个复合：空字母表的环境平凡地相合，因为并无常元需要解释；而改名定理把「改名后公式的外部满足」与「层内部满足」等同。

        cong (λ κ → FOL.Semantics.At._⊨_ DA.𝒮M (⊥* {ℓ}) κ δ χ)
          (funExt (λ b → Empty.rec* b))
      ∙ sym (⊨-map DA.𝒮M ε′ DA.ι χ δ)
    opaque
      keyOf : (k : ℕ) → Formula (⊥* {ℓ}) k → CS.S

一条无常元公式在该层的键，是其改名后的形在该层码集中的键。它只命名一次，使后文各陈述可以提到它而不重新打开其构造。

      keyOf k χ = keyS A (mapFo ε′ χ)

该键属于该层处的码集：改名后公式的码是该层字母表上的码，而码集把它们尽数包含。

      keyOf∈ : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) → ⟨ keyOf k χ CS.∈ˢ AllCodes A ⟩
      keyOf∈ k χ = key∈AllCodes A (mapFo ε′ χ)

虽然 keyOf 是不透明定义，引理 keyOf≡ 明确给出它与 keyS A (mapFo ε′ χ) 的等式。后续证明可使用该等式，而不展开封存的定义。

      keyOf≡ : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) → keyOf k χ ≡ keyS A (mapFo ε′ χ)
      keyOf≡ k χ = refl

封存键的底层集合被算出：它是「元数的数码与改名后公式的码」组成的有序对。证明复合了公式的两次改名，先经空字母表、再经该层的嵌入，而改名定理把结果与极限层所记录的码等同。

      keyOf-fst : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
                → fst (keyOf k χ) ≡ pr (# k) (fst (limitCode χ))
      keyOf-fst k χ = cong (pr (# k)) (cong VCode.⌜_⌝
        ( mapFo-comp ε′ ⟪ Lset lam ⟫↪ χ
        ∙ cong (λ f → mapFo f χ) (funExt (λ b → Empty.rec* b)) ))

对每条无参公式，Tof 是满足图在该公式封存键处选出的满足集。这个固定集合在整个层中表示该公式的满足关系。

    Tof : (k : ℕ) → Formula (⊥* {ℓ}) k → CS.S
    Tof k χ = SM.valOf (keyOf k χ) (keyOf∈ k χ)

键与其满足集组成的有序对属于满足图。此外，任何与该键具有相同底层集合的载体元素都会选出同一满足集：其可构造性见证都是命题，所以底层集合的相等可提升为载体中的相等，继而得到所选取值的相等。

    Tof-pair : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
             → ⟨ pr (fst (keyOf k χ)) (fst (Tof k χ)) ∈ˢ fst SM.pairs ⟩
    Tof-pair k χ = SM.pairs-in (keyOf k χ) (keyOf∈ k χ)
    valOf-same : (x : CS.S) (m : ⟨ x CS.∈ˢ AllCodes A ⟩) (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
               → fst x ≡ fst (keyOf k χ) → SM.valOf x m ≡ Tof k χ