---
title: "在 L 中定位 Skolem 壳及其塌缩"
module: L.GCH.ConstructibleHull
lang: zh
site: "Bedrock"
description: "在 L 中定位 Skolem 壳及其塌缩"
stage: "证明 GCH"
reading_order: 116
canonical: https://bedrock.institute/zh/L.GCH.ConstructibleHull.html
html: L.GCH.ConstructibleHull.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/ConstructibleHull.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Manipulation.Renaming, FOL.Absoluteness, FOL.Semantics, V.Hierarchy, V.Presentation, V.Coding, V.Collapse, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Full, L.Axioms.Infinity, L.Axioms.Numerals, L.Recursion, L.Recursion.Graph, L.Definability, L.Coding.Model, L.Coding.Expressions, L.Coding.Environment, L.Coding.EnvironmentSet, L.Coding.SatisfactionBridge, L.Coding.CodeSet, L.Coding.CodeConstructibility, L.Coding.UniformSatisfaction, L.Choice.CanonicalNames, L.Choice.NameComparison, L.Choice.InternalWellOrder, L.Choice.StageOrders, L.WellOrder.Base, L.GCH.CardinalSquareLaw, L.GCH.OrderType, L.GCH.OmegaRecursion, L.GCH.SkolemHull, L.InjectionComposition, L.GCH.AdequateStages, L.Coding.SatisfactionGraphSet, L.GCH.CondensationTransfer, V.Model]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.ConstructibleHull.md, https://bedrock.institute/ja/L.GCH.ConstructibleHull.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 在 L 中定位 Skolem 壳及其塌缩

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

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

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

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

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

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

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

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

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

```agda
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`。由于壳不传递，论证无法援引关于塌缩的全局事实，而必须逐层重新推得取值留在内部。

```agda
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` 的元素，这正是使整个构造留在它所描述的宇宙之内的原因。

```agda
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` 的元素，而只须每个实参处「仅仅存在」唯一取值。可定义性解释公式的常元；模型内侧的对与数码编码供给条目及其名字。

```agda
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` 的一个元素；可构造并则把构造沿途收集的各部分合并起来。

```agda
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 ω`，无常元公式仍可带有自由变元槽；某层的内部良序比较其成员，先按诞生层、再按名字。

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

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

```agda
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
```

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

```agda
  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 壳实现为各有限闭包层的并，从而证明载体本身可构造，并可对它应用第一部分。

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

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

```agda
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
```

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

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

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

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

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

```agda
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 ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ )
```

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

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

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

```agda
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 索引，长环境的每个槽位一个。

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

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

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

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

```agda
  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≡` 都作出这一认同。

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

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

```agda
  ρs : Fin 2 → Fin 2
  ρs zero = suc zero
  ρs (suc zero) = zero
```

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

```agda
  ρf : Fin 2 → Fin 3
  ρf zero = zero
  ρf (suc zero) = suc (suc zero)
```

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

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

固定任意可构造载体 `M`。

```agda
  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` 传递。

```agda
module PiIn (Mʟ : CS.S) where
```

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

```agda
  M : S
  M = fst Mʟ
```

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

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

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

```agda
  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` 内成员上的塌缩像」。

```agda
  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` 的成员。

```agda
    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`。

```agda
                 , ∈∈ₛ {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)))
```

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

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

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

```agda
  R : CS.S
  R = Membership.rel
```

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

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

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

```agda
  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`。它不声称任何全局的函数图；在每个实参处只断言这样的表存在，这正是该公式能在非传递载体上成立的原因。

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

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

```agda
    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
```

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

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

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

```agda
    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` 的塌缩。可构造性与隶属都随动机同行，因为表的条目是载体元素组成的对。

```agda
          , 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` 的每个成员处的动机。

```agda
  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 =
```

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

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

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

```agda
      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`。

```agda
        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` 的认同。

```agda
          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)`。

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

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

```agda
          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` 属于被记录的取值。这正是向后方向所主张的。

```agda
          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`，这正是向后方向所要安放的。

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

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

```agda
  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` 的某个给定元素之内的元素。

```agda
  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`。切片所容纳的，恰是满足它的那些元素。

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

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

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

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

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

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

```agda
      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` 处的塌缩公式。

```agda
      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` 成员呈现上成立。

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

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

```agda
  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` 都是「好」的。这些较早的塌缩值将被组装成下一实参处的取值。

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

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

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

层是传递的，因此层的成员的成员仍在层内；这条事实稍后会把表的条件限制到更小的实参。由归纳假设，切片成员的塌缩可作为 `𝒮ʟ` 的元素使用；其可构造性证明正是「好」的第一分量。

```agda
    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
```

塌缩公式在该塌缩与成员组成的对上成立，同样由归纳假设给出：「好」的第二分量恰是该公式在此对上的一个满足，沿「元素与其底层集合的认同」运输而来。

```agda
    πʟ-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)
```

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

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

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

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

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

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

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

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

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

```agda
    Tab : CS.S
    Tab = T.F
```

表的向内读式出示其条目：在每个切片成员处，成员与其塌缩组成的对都被记录。

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

向外读式把一条条目分解为切片成员与其底层集合的塌缩相等的取值。与向内读式合起来，这说明表记录的恰是诸塌缩，毫无走样。

```agda
    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` 传递。

```agda
    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` 的成员仍在该层内，因而属于切片。

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

对封闭的实参，表的完备性就是「表在相关成员处有自己的条目」的截断存在：封闭性把该成员放进切片，表在那里记录其塌缩。关系条目被分解以指名该成员。

```agda
    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
```

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

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

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

```agda
    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`。该分解是截断的存在，而消去的目标是一条命题。

```agda
      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` 见证。

```agda
          , ( 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` 放进第一分量的塌缩，而两条等式再把它运回被记录取值。

```agda
      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)) })
```

表在每条条目处的正确性，由该条目所指名的切片成员处的两个子句装配而成。对读法贡献切片隶属与载体隶属。

```agda
    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⊆` 得出。

```agda
      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
```

实参被载为载体元素，从而可以充当环境槽位以及有序对的第二分量。

```agda
      qS : CS.S
      qS = up q mq
```

载入后实参的封闭性由假设成立：其在载体内的每个成员都低于更早层，切片接纳它们。实参在载体内的成员随后被切出为它们自己的切片，塌缩取值将在这个定义域上计算。

```agda
      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` 中替换原理的假设。

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

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

```agda
          ; 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` 供给唯一性。

```agda
          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 δ'`，所以其中每个属于载体的元素都被层切片接纳。

```agda
            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` 的成员之可构造塌缩值。

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

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

```agda
      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` 的塌缩，运输把两者复合。

```agda
          (λ { (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` 的可构造性，从而把它呈现为 `𝒮ʟ` 的元素。

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

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

```agda
        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` 运到分量的塌缩，而表的向内读式在载入后的分量处产出条目，其记录的恰是该塌缩。

```agda
            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` 的成员低于更早层」的假设而属于层切片。

```agda
            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` 处「好」的第一个子句。

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

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

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

```agda
      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` 落在更早层 `δ'` 的可定义幂集内。该分解被消去到「好」之中，因为「好」是命题。

```agda
  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 δ'` 内，这正是步进所消费的封闭性假设。

```agda
      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` 的每个成员也放入其中。

```agda
        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` 的成员作相应论证，同样把截断呈现消去到可构造性。

```agda
    (λ { (α , (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` 的陈述是关于成员的：塌缩像的每个成员都是载体某个成员的塌缩，故可构造。

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

## 把 Skolem 壳写成 ω 迭代

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

```agda
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`、「壳包含于该层」以及「起点的每个成员都是壳的成员」。

```agda
  (∅∈λ : ⟨ ∅ ∈ˢ 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`，其中保存一条无常元公式及其参数的子码。先求出子码的值，再依是否存在见证，取最小见证或废弃值作为该码的值。

```agda
    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` 的底层集合；步进的搜索只在这样的向量上进行。

```agda
  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` 断言这样的见证存在。

```agda
  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` 的环境满足该公式。

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

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

```agda
      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) ⟩
```

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

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

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

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

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

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

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

```agda
    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` 次应用。

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

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

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

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

```agda
    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
```

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

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

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

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

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

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

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

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

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

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

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

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

```agda
    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
```

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

```agda
        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)) ⟩
```

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

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

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

```agda
      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
```

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

```agda
          (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) ∥₁
```

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

```agda
      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` 的值与搜索返回的最小见证等同。由于每个码的值都属于壳，该搜索值也属于壳。

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

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

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

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

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

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

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

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

```agda
    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
```

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

```agda
      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` 元素。

```agda
          (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` 元素的壳是诸迭代的并，其隶属描述说它的成员恰是壳的成员。向前：并的成员落在某个迭代处，故在壳内。

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

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

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

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

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

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

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

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

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

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

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

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

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

```agda
    A : CS.S
    A = LsetS lam ordλ
```

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

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

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

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

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

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

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

```agda
    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 ⟩
```

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

```agda
      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` 是满足图在该公式封存键处选出的满足集。这个固定集合在整个层中表示该公式的满足关系。

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

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

```agda
    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 χ
```

证明沿底层集合等式作路径归纳，而码集隶属的命题性吸收了隶属证明之间的差异。起作用的只有底层集合，因此运输对其余一切保持沉默。

```agda
    valOf-same x m k χ e =
      J (λ x' e' → (m' : ⟨ x' CS.∈ˢ AllCodes A ⟩) → SM.valOf x m ≡ SM.valOf x' m')
        (λ m' → cong (SM.valOf x) (snd (x CS.∈ˢ AllCodes A) m m'))
        (S≡ {x = x} {y = keyOf k χ} e) (keyOf∈ k χ)
    sat-at : (k : ℕ) (χ : Formula (⊥* {ℓ}) k) (δ : SL ^ k) (z : CS.S)
```

「属于一个满足集」此刻被算成层自身的满足。这座桥复合三个同认：封存的名字与其所自的键一致；键处的取值由一致满足定理向外部读取；而改名后公式的外部满足，经改名桥即层内部满足。

```agda
           → fst z ≡ graph A δ → (z CS.∈ˢ Tof k χ) ≡ (δ ⊨₀ χ)
    sat-at k χ δ z qz =
        cong (z CS.∈ˢ_) (SM.valOf≡ (keyOf k χ) (keyOf∈ k χ))
      ∙ val-sat A (mapFo ε′ χ) (keyOf k χ) (keyOf∈ k χ) (cong fst (keyOf≡ k χ)) δ z qz
      ∙ sym (sat-bridge k χ δ)
```

键识别式是一条公式。它断言槽位 `s` 的值属于该层的码集，并且对某个码，它是槽位 `a` 中数码的后继与该码组成的有序对。因此，当槽位 `a` 含有 `# k` 时，它识别一条元数为 `k+1` 的无参公式之键。这里「无参」表示常元域为空；公式仍可有自由变元。

```agda
    opaque
      keyIn : ∀ {n} → Fin n → Fin n → Formula CS.S n
      keyIn s a = (var s ∈̇ con C₀)
                ∧̇ ∃̇ ( sucAtL (suc a) zero
                     ∧̇ ∃̇ (prAtL (suc (suc s)) (suc zero) zero) )
```

两条读式在变元环境处陈述，针对固定的元数 `k`，其数码已被记在槽位 `a` 处。预先固定元数，正是使两条读式成为关于码的等式、而非在码中搜寻的原因。

```agda
    module KeyIn {n : ℕ} (s a : Fin n) (γ : CS.S ^ n) (k : ℕ)
                 (qa : fst (lookup a γ) ≡ # k) where
```

该公式在其自身槽位处被开启以供计算，因为两条读式必须穿过定义中的合取与存在量词。

```agda
      opaque
        unfolding keyIn
```

引入由三个数据建成满足：`s` 的码集隶属、层级的一个元素 `c`，以及把 `s` 同认于「后继数码与 `c` 之对」的等式。数码、后继子句与对子句依次填入。

```agda
        keyIn-in : ⟨ fst (lookup s γ) ∈ˢ fst C₀ ⟩ → (c : V ℓ)
                 → fst (lookup s γ) ≡ pr (# (suc k)) c → ⟨ γ ⊨ keyIn s a ⟩
        keyIn-in h c q = h , ∣ numAt , ( hsuc , ∣ cS , hpr ∣₁ ) ∣₁
          where
          numAt : CS.S
```

数码被呈现为载体元素，码 `c` 也被提升为载体元素。由把 `s` 同认于该有序对的等式以及 `s` 的可构造性，`pr-snd-isL` 推出有序对第二分量 `c` 的可构造性。

```agda
          numAt = nn (suc k)
          cS : CS.S
          cS = c , pr-snd-isL (# (suc k)) c
                     (subst (λ u → ⟨ isL u ⟩) q (isL-trans h (snd C₀)))
          hsuc : ⟨ (numAt ∷ γ) ⊨ sucAtL (suc a) zero ⟩
```

后继子句由槽位 `a` 处数码的等式运输而来，对子句由 `s` 的等式运输而来，各经其编码算子的充分性。这两次运输恰是把宿主等式转成满足的过程。

```agda
          hsuc = subst ⟨_⟩ (sym (sucAtL-adequate (suc a) zero (numAt ∷ γ)))
            (cong sucV (sym qa))
          hpr : ⟨ (cS ∷ numAt ∷ γ) ⊨ prAtL (suc (suc s)) (suc zero) zero ⟩
          hpr = subst ⟨_⟩
            (sym (prAtL-adequate (suc (suc s)) (suc zero) zero (cS ∷ numAt ∷ γ))) q
```

消去收回两条数据：`s` 的码集隶属，以及「`s` 是后继数码与某个码之对」的截断陈述。公式的存在链被逐步拆开。

```agda
        keyIn-out : ⟨ γ ⊨ keyIn s a ⟩
                  → ⟨ fst (lookup s γ) ∈ˢ fst C₀ ⟩
                  × ∥ Σ[ c ∈ V ℓ ] (fst (lookup s γ) ≡ pr (# (suc k)) c) ∥₁
        keyIn-out (h , hk) = h , PT.rec squash₁ atNum hk
          where
```

中间约束子名指后继槽位处的数码，而后继编码的充分性把其满足转换成底层集合的等式。

```agda
          atNum : Σ[ z ∈ CS.S ] ( ⟨ (z ∷ γ) ⊨ sucAtL (suc a) zero ⟩
                                × ⟨ (z ∷ γ) ⊨ ∃̇ (prAtL (suc (suc s)) (suc zero) zero) ⟩ )
                → ∥ Σ[ c ∈ V ℓ ] (fst (lookup s γ) ≡ pr (# (suc k)) c) ∥₁
          atNum (z , (hs , hc)) = PT.map
            (λ { (c , hp) → fst c
```

内层存在量词随之给出码 `c` 及对子句的一个满足；充分性把它运成有序对的等式，再与数码及其后继的认同复合。收回的等式正是所要的截断陈述。

```agda
               , ( subst ⟨_⟩ (prAtL-adequate (suc (suc s)) (suc zero) zero (c ∷ z ∷ γ)) hp
                 ∙ cong (λ u → pr u (fst c)) (qz ∙ cong sucV qa) ) })
            hc
            where
            qz : fst z ≡ sucV (fst (lookup a γ))
```

七槽环境在此装配：满足表、扩展环境、参数环境、键、数码、见证与当前集合，次序即体所要读取的次序。

```agda
            qz = subst ⟨_⟩ (sucAtL-adequate (suc a) zero (z ∷ γ)) hs
    Env : CS.S → CS.S → CS.S → CS.S → CS.S → CS.S → CS.S → CS.S ^ 7
    Env T e' e s k w Z = T ∷ e' ∷ e ∷ s ∷ k ∷ w ∷ Z ∷ []
```

极小性子公式对层的字母表量化。它说：若参数环境被某个层元素扩展后满足被编码公式，则该元素在层良序中不排在见证之前。它以常元 `A` 为界，故量词遍历的是该层而非整个宇宙。

```agda
    opaque
      minFo : Formula CS.S 7
      minFo = ∀̇∈ (con A)
        ( (∃̇ ( consAtL i0 i1 i4 ∧̇ (var i0 ∈̇ var i2) )) ⇒̇ ¬̇ (appC Rel i0 i6) )
```

体的各合取项依次说：数码落在内部 `ωʟ` 中；`s` 是元数加一的键；参数环境把当前集合上的一个向量编码；扩展环境由见证扩展该环境。

```agda
      bodyFo : Formula CS.S 7
      bodyFo = (var i4 ∈̇ con ωʟ)
            ∧̇ ( keyIn i3 i4
            ∧̇ ( envOverAt i2 i4 i6
            ∧̇ ( consAtL i1 i5 i2
```

其余合取项说：键与表组成的对落在满足图中；扩展环境属于表；见证属于该层；且极小性成立。合计八个合取项。层约束见证以及极小性所比较的候选，而各编码合取项提供把这份记录接到满足表所需的辅助对象。

```agda
            ∧̇ ( appC SM.pairs i3 i0
            ∧̇ ( (var i1 ∈̇ var i0)
            ∧̇ ( (var i5 ∈̇ con A)
            ∧̇ minFo ))))))
```

固定七个对象 `T,e',e,s,k,w,Z`。在它们组成的环境处，体成为一个具体命题，其八个合取项既可逐项投影，也可反向装配。

```agda
    module BodyRd (T e' e s k w Z : CS.S) where
```

七槽环境被记录；宿主侧极小性相对于呈现参数环境的族陈述：不存在用更小的层元素所作的扩展落入满足表、同时在层序中排在见证之前。

```agda
      γ₇ : CS.S ^ 7
      γ₇ = Env T e' e s k w Z
      Min : {m : ℕ} (g : Fin m → V ℓ) → Type (ℓ-suc ℓ)
      Min g = (w' : CS.S) → ⟨ fst w' ∈ˢ fst A ⟩ → (e'' : CS.S)
            → fst e'' ≡ env (cons (fst w') g) → ⟨ fst e'' ∈ˢ fst T ⟩
```

该子句终止于空类型：极小性表现为排除反例，也就是排除一个更小的扩展及其相应的对隶属。

```agda
            → ⟨ pr (fst w') (fst w) ∈ˢ fst Rel ⟩ → Empty.⊥
```

由于体是嵌套的合取，其八项条件都可由投影读出；反过来，八项条件的证明又可装配成对该体的满足。

```agda
      opaque
        unfolding bodyFo
```

第一条读法投影数码子句。属于内部 `ωʟ` 使我们能恢复自然数 `n`；再结合键子句，便知 `s` 是元数为 `n+1` 的键，其中一个槽位留给见证。

```agda
        b-num : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ fst k ∈ˢ fst ωʟ ⟩
        b-num h = h .fst
```

第二项投影是键子句：公式在 `s` 与 `k` 槽处断言，`s` 是一个被识别的键，其元数比数码 `k` 大一。

```agda
        b-key : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ γ₇ ⊨ keyIn i3 i4 ⟩
        b-key h = h .snd .fst
```

第三条读法投影环境子句：参数环境在所记录的槽位处把当前集合上的一个向量编码。

```agda
        b-env : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ γ₇ ⊨ envOverAt i2 i4 i6 ⟩
        b-env h = h .snd .snd .fst
```

第四条读法给出扩展等式，沿 cons 编码的充分性运输：扩展环境是参数环境由见证扩展而成。

```agda
        b-cons : {m : ℕ} (g : Fin m → V ℓ) → fst e ≡ env g
               → ⟨ γ₇ ⊨ bodyFo ⟩ → fst e' ≡ env (cons (fst w) g)
        b-cons g hE h =
          subst ⟨_⟩ (consAtL-adequate i1 i5 i2 γ₇ g hE) (h .snd .snd .snd .fst)
```

第五条读法给出「键与表之对」的图隶属，沿应用编码的充分性运输。

```agda
        b-tab : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ pr (fst s) (fst T) ∈ˢ fst SM.pairs ⟩
        b-tab h = subst ⟨_⟩ (appC-adequate SM.pairs i3 i0 γ₇) (h .snd .snd .snd .snd .fst)
```

第六条读法是扩展环境对满足表的隶属，即「见证在参数处满足被编码公式」这一事实。

```agda
        b-mem : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ fst e' ∈ˢ fst T ⟩
        b-mem h = h .snd .snd .snd .snd .snd .fst
```

第七项投影说明见证属于层 `A`，因而该见证与所有同它比较的候选都取自同一个层。

```agda
        b-stage : ⟨ γ₇ ⊨ bodyFo ⟩ → ⟨ fst w ∈ˢ fst A ⟩
        b-stage h = h .snd .snd .snd .snd .snd .snd .fst
```

第八条读法是以反驳形式读取的极小性子句：一个更小的候选若带有满足扩展，便与有界量词矛盾，其间关系条目要经应用的充分性运输。

```agda
        b-min : {m : ℕ} (g : Fin m → V ℓ) → fst e ≡ env g → ⟨ γ₇ ⊨ bodyFo ⟩ → Min g
        b-min g hE h w' hw' e'' qe hm hr =
          lower (h .snd .snd .snd .snd .snd .snd .snd w' hw' ∣ e'' , (hc , hm) ∣₁
            (subst ⟨_⟩ (sym (appC-adequate Rel i0 i6 (w' ∷ γ₇))) hr))
          where
```

候选扩展的 cons 子句由其宿主等式运输而来，恰与内层存在量词中扩展的编码互为镜像。

```agda
          hc : ⟨ (e'' ∷ w' ∷ γ₇) ⊨ consAtL i0 i1 i4 ⟩
          hc = subst ⟨_⟩ (sym (consAtL-adequate i0 i1 i4 (e'' ∷ w' ∷ γ₇) g hE)) qe
```

填充读法由八个分量装配出体的满足：数码子句、键子句、环境子句、扩展等式、图隶属、表隶属、层隶属，以及极小性。

```agda
        b-fill : {m : ℕ} (g : Fin m → V ℓ) → fst e ≡ env g
               → ⟨ fst k ∈ˢ fst ωʟ ⟩ → ⟨ γ₇ ⊨ keyIn i3 i4 ⟩ → ⟨ γ₇ ⊨ envOverAt i2 i4 i6 ⟩
               → fst e' ≡ env (cons (fst w) g) → ⟨ pr (fst s) (fst T) ∈ˢ fst SM.pairs ⟩
               → ⟨ fst e' ∈ˢ fst T ⟩ → ⟨ fst w ∈ˢ fst A ⟩ → Min g
               → ⟨ γ₇ ⊨ bodyFo ⟩
```

五个合取项被直接放入。扩展等式与图条目分别沿 `consAtL` 和 `appC` 的充分性等式反向转换为满足；极小性则由最后一项给出。

```agda
        b-fill g hE c1 c2 c3 c4 c5 c6 c7 mn =
          c1 , c2 , c3
          , subst ⟨_⟩ (sym (consAtL-adequate i1 i5 i2 γ₇ g hE)) c4
          , subst ⟨_⟩ (sym (appC-adequate SM.pairs i3 i0 γ₇)) c5
          , c6 , c7
```

极小性的填充靠把其截断的反例消去到空类型完成：反例先穿过两条充分性等式再交予反驳，因此填充者只需要矛盾本身，而不需要任何构造。

```agda
          , λ w' hw' hex hr → lift (PT.rec Empty.isProp⊥
              (λ { (e'' , (hc , hm)) → mn w' hw' e''
                     (subst ⟨_⟩ (consAtL-adequate i0 i1 i4 (e'' ∷ w' ∷ γ₇) g hE) hc) hm
                     (subst ⟨_⟩ (appC-adequate Rel i0 i6 (w' ∷ γ₇)) hr) })
              hex)
```

见证公式用五层嵌套存在量词包裹体，每个对象一个：满足表、扩展环境、参数环境、键、数码。该公式在 `w` 与 `Z` 处的满足，恰是说：`Z` 上 `w` 处的最小见证的完整记录存在。

```agda
    opaque
      witFo : Formula CS.S 2
      witFo = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ bodyFo))))
```

向内读法把五个对象与体的满足沿五层约束子逐一注入，每次注入把一个对象送入其槽位。

```agda
      witFo-in : (w Z T e' e s k : CS.S) → ⟨ Env T e' e s k w Z ⊨ bodyFo ⟩
               → ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩
      witFo-in w Z T e' e s k h = ∣ k , ∣ s , ∣ e , ∣ e' , ∣ T , h ∣₁ ∣₁ ∣₁ ∣₁ ∣₁
```

向外读法按约束次序消去五层截断存在。在最内层，`PT.map` 只把恢复出的对象重排为所展示的依赖元组，体的满足本身不作运输。

```agda
      witFo-out : (w Z : CS.S) → ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩
                → ∥ Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ e ∈ CS.S ] Σ[ s ∈ CS.S ] Σ[ k ∈ CS.S ]
                     ⟨ Env T e' e s k w Z ⊨ bodyFo ⟩ ∥₁
      witFo-out w Z = PT.rec squash₁ (λ { (k , hk) → PT.rec squash₁ (λ { (s , hs) →
        PT.rec squash₁ (λ { (e , he) → PT.rec squash₁ (λ { (e' , he') → PT.map
```

拆开 `witFo` 得到满足表、扩展环境、参数环境、键与数码；

```agda
          (λ { (T , hT) → T , e' , e , s , k , hT }) he' }) he }) hs }) hk })
```

## 固定键与环境处的最小见证关系

它们组成的环境满足体。固定 `e` 与 `s` 后，`LeastWitness Z e s z` 保留其余满足表、扩展环境与数码的截断存在。

```agda
    LeastWitness : CS.S → CS.S → CS.S → CS.S → Type (ℓ-suc ℓ)
    LeastWitness Z e s z =
      ∥ Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ k ∈ CS.S ]
          ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩ ∥₁
```

为了在保留六个周围变元的同时约束满足表、扩展环境与数码，体从七槽改名到九槽。槽位映射把七个有效条目放在 `T,e',e,s,k,z,Z` 处。

```agda
    private
      ρ₉ : Fin 7 → Fin 9
      ρ₉ zero = i0
      ρ₉ (suc zero) = i1
      ρ₉ (suc (suc zero)) = i4
```

余下四种情形依次安置键 `s`、数码 `k`、候选 `z` 与当前集合 `Z`。末尾的 `p,q` 不被读取，因此满足与它们的取值无关。

```agda
      ρ₉ (suc (suc (suc zero))) = i5
      ρ₉ (suc (suc (suc (suc zero)))) = i2
      ρ₉ (suc (suc (suc (suc (suc zero))))) = i6
      ρ₉ (suc (suc (suc (suc (suc (suc zero)))))) = i3
```

`Γ₉` 展示这一安置，而每条与原七槽环境的相合都由定义上的自反性成立。

```agda
      Γ₉ : (T e' k Z e s z p q : CS.S) → CS.S ^ 9
      Γ₉ T e' k Z e s z p q = T ∷ e' ∷ k ∷ Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []
```

相合说：在每个被改名的槽处，两个环境载有相同的载体元素。前三条由自反性证明，每个被改名的位置一条。

```agda
      ag₉ : (T e' k Z e s z p q : CS.S)
          → Ren.Agrees ρ₉ (Γ₉ T e' k Z e s z p q) (Env T e' e s k z Z)
      ag₉ T e' k Z e s z p q zero = refl
      ag₉ T e' k Z e s z p q (suc zero) = refl
      ag₉ T e' k Z e s z p q (suc (suc zero)) = refl
```

其余四条相合同样是自反性，每槽一条；每条相合都是一次计算，这正是改名能在满足内部使用的原因。

```agda
      ag₉ T e' k Z e s z p q (suc (suc (suc zero))) = refl
      ag₉ T e' k Z e s z p q (suc (suc (suc (suc zero)))) = refl
      ag₉ T e' k Z e s z p q (suc (suc (suc (suc (suc zero))))) = refl
      ag₉ T e' k Z e s z p q (suc (suc (suc (suc (suc (suc zero)))))) = refl
```

改名后的体是沿槽位表推送的体公式，居于九槽之上，所说却与从前相同。

```agda
      body₉ : Formula CS.S 9
      body₉ = renameFo ρ₉ bodyFo
```

读取等式说：在九槽环境上满足改名后的体，与在七槽环境上满足体，是同一命题。

```agda
      body₉-read : (T e' k Z e s z p q : CS.S)
                 → ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩
                 ≡ ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩
      body₉-read T e' k Z e s z p q =
        cong ⟨_⟩ (Ren.⊨-rename ρ₉ bodyFo (Γ₉ T e' k Z e s z p q)
```

证明是把改名定理施于槽位相合，再在满足的括号下运输。

```agda
                    (Env T e' e s k z Z) (ag₉ T e' k Z e s z p q))
```

最小见证公式在改名后的体上再包三层存在量词：数码、扩展环境、满足表。其在六槽环境处的满足说：对该候选，在当前集合、键与参数环境处，存在一份最小见证记录。

```agda
    opaque
      leastWitnessFo : Formula CS.S 6
      leastWitnessFo = ∃̇ (∃̇ (∃̇ body₉))
```

向内读法消去截断的最小见证数据并注入三个对象，且把体的满足沿改名体的读取等式运输。

```agda
      leastWitness-in : (Z e s z p q : CS.S) → LeastWitness Z e s z
                      → ⟨ (Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ leastWitnessFo ⟩
      leastWitness-in Z e s z p q = PT.rec (snd ((Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ leastWitnessFo))
        (λ { (T , e' , k , h) →
          ∣ k , ∣ e' , ∣ T , transport (sym (body₉-read T e' k Z e s z p q)) h ∣₁ ∣₁ ∣₁ })
```

向外读法依次消去三层嵌套存在量词，每次都消到截断的后续之中，于是公式满足重新变回一份最小见证记录。

```agda
      leastWitness-out : (Z e s z p q : CS.S)
                       → ⟨ (Z ∷ e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ leastWitnessFo ⟩
                       → LeastWitness Z e s z
      leastWitness-out Z e s z p q = PT.rec squash₁ at₁
        where
```

最内层消去由被名指的满足表、扩展环境与数码重建最小见证数据，并把体的满足沿读取等式运输。两个外层消去则提供该构造所需的约束对象。

```agda
        at₃ : (k e' : CS.S) → Σ[ T ∈ CS.S ] ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩
            → LeastWitness Z e s z
        at₃ k e' (T , h) = ∣ T , e' , k , transport (body₉-read T e' k Z e s z p q) h ∣₁
        at₂ : (k : CS.S) → Σ[ e' ∈ CS.S ] ∥ Σ[ T ∈ CS.S ] ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩ ∥₁
            → LeastWitness Z e s z
```

此处还剩两层截断：外层隐藏延拓环境 `e'`，内层隐藏表 `T`。两次消去依次取出它们，随后 `at₃` 把改名后的体证明搬回一份 `LeastWitness`。

```agda
        at₂ k (e' , h) = PT.rec squash₁ (at₃ k e') h
        at₁ : Σ[ k ∈ CS.S ] ∥ Σ[ e' ∈ CS.S ] ∥ Σ[ T ∈ CS.S ]
                ⟨ Γ₉ T e' k Z e s z p q ⊨ body₉ ⟩ ∥₁ ∥₁
            → LeastWitness Z e s z
        at₁ (k , h) = PT.rec squash₁ (at₂ k) h
```

数码槽位装着内部 `ω` 的一个成员，`decode-num` 将其解码：得到截断的自然数 `n`，以及把该条目与外围数码 `# n` 等同的等式。解码是内部编号与见证数据的自然数记账之间的桥梁。

```agda
    private
      decode-num : (q : CS.S) → ⟨ fst q ∈ˢ fst ωʟ ⟩ → ∥ Σ[ n ∈ ℕ ] (fst q ≡ # n) ∥₁
      decode-num q h = PT.map (λ { (n , e) → lower n , (e ∙ numeralL-fst (lower n)) })
        (subst ⟨_⟩ (ω-specL q) h)
```

`LeastWitnessData` 是最小见证背后的真实数据：自然数 `n`、把 `n` 个索引指派到 `Z` 呈现中的赋值 `g`、说明 `e` 正是命名这些取值的环境的等式，以及把 `s` 放入 `Lset ω` 的层隶属。

```agda
    LeastWitnessData : CS.S → CS.S → CS.S → Type (ℓ-suc ℓ)
    LeastWitnessData Z e s =
      Σ[ n ∈ ℕ ] Σ[ g ∈ (Fin n → ⟪ fst Z ⟫) ]
        ((fst e ≡ env (λ i → ⟪ fst Z ⟫↪ (g i))) × (⟨ fst s ∈ Lset ω ⟩))
```

定理 `leastWitness-data` 说明：公式层的最小见证在命题截断意义下决定一个自然数元数、`Z` 上的索引参数环境，以及键属于 `Lset ω` 的证明。

```agda
    opaque
      leastWitness-data : (Z e s z : CS.S) → LeastWitness Z e s z
                        → ∥ LeastWitnessData Z e s ∥₁
      leastWitness-data Z e s z = PT.rec squash₁ body
        where
```

转换的主体消耗体的满足：将其拆开为表 `T`、扩展 `e'`、键 `k` 与体证明，而键的数码条目最先被解码。

```agda
        body : Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ k ∈ CS.S ]
                 ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩
             → ∥ LeastWitnessData Z e s ∥₁
        body (T , e' , k , hb) = PT.map at (decode-num k (BodyRd.b-num T e' e s k z Z hb))
          where
```

有了数码 `n` 与点名键的等式，数据即可组装：长度 `n`、恢复出的赋值 `g`、环境的恢复等式，以及 `s` 的层隶属。七条目语境被一次性命名，使恢复过程能够寻址各个槽位。

```agda
          at : Σ[ n ∈ ℕ ] (fst k ≡ # n) → LeastWitnessData Z e s
          at (n , qk) = n , R.g , R.recovers , s∈Lω
            where
            γ : CS.S ^ 7
            γ = Env T e' e s k z Z
```

环境子句恢复出 `Z` 中索引的赋值 `g`，并证明 `e` 是这些索引之取值的图。另一方面，键子句说明 `s` 是一个码，而且是后继元数的数码与某个公式码组成的有序对。

```agda
            module R = Recover Z n γ i2 i4 i6 qk refl (BodyRd.b-env T e' e s k z Z hb)
              using ( g; recovers )
            kr : ⟨ fst s ∈ fst C₀ ⟩ × ∥ Σ[ c ∈ V ℓ ] (fst s ≡ pr (# (suc n)) c) ∥₁
            kr = KeyIn.keyIn-out i3 i4 γ n qk (BodyRd.b-key T e' e s k z Z hb)
            s∈Lω : ⟨ fst s ∈ Lset ω ⟩
```

键的取值的层隶属是数据的最后一块。它由对等式证明：键的第二分量 `c` 是一个码，而码在极限层处就可构造。

```agda
            s∈Lω = PT.rec (snd (fst s ∈ Lset ω)) read (kr .snd)
              where
              read : Σ[ c ∈ V ℓ ] (fst s ≡ pr (# (suc n)) c) → ⟨ fst s ∈ Lset ω ⟩
              read (c , qs) = PT.rec (snd (fst s ∈ Lset ω))
                (λ { (χ , qc) → subst (λ w → ⟨ w ∈ Lset ω ⟩) (sym qs)
```

于是键的两个分量都住在 `Lset ω` 中：后继数码凭数码的隶属属于极限层，而极限层成员的有序对仍留在极限层。沿对等式传输后，`s` 便落入 `Lset ω`，`LeastWitnessData` 随之完成。

```agda
                       (pr∈limit (# (suc n)) c (numeral∈limit (suc n))
                         (subst (λ w → ⟨ w ∈ˢ Lset ω ⟩) (sym qc) (snd (limitCode χ)))) })
                (freeCode-out (suc n) c (subst (λ u → ⟨ u ∈ fst C₀ ⟩) qs (kr .fst)))
```

见证公式的外向读法在此组装：`witFo` 在 `(z, Z)` 处的满足拆开为表、扩展、键与体证明，而体证明转换为截断的 `LeastWitness`。这正是消费 Skolem 子句之满足的形式。

```agda
      witFo-leastWitness : (z Z : CS.S) → ⟨ (z ∷ Z ∷ []) ⊨ witFo ⟩
                         → ∥ Σ[ e ∈ CS.S ] Σ[ s ∈ CS.S ] LeastWitness Z e s z ∥₁
      witFo-leastWitness z Z h = PT.map
        (λ { (T , e' , e , s , k , hb) → e , s , ∣ T , e' , k , hb ∣₁ })
        (witFo-out z Z h)
```

为比较两个见证，这里保留体的八条子句中的七条：数码、环境、延拓、表、隶属、层与最小性子句。这里不需要键子句，因为两份见证已经共享 `s`，而该键所对应之值的唯一性会把两张表同一视。

```agda
    private
      module WitnessBody (z T e' e s k Z : CS.S)
        (hb : ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩) where
        module Rd = BodyRd T e' e s k z Z
          using ( b-num; b-env; b-cons; b-tab; b-mem; b-stage; b-min )
```

其中两条子句立即给出延拓环境属于表，以及见证属于 `Lset lam`。一旦把键的数码认同为 `# n`，环境子句还会恢复出 `Z` 中索引组成的 `n` 元组。

```agda
        h6 = Rd.b-mem hb
        h7 = Rd.b-stage hb
        module AtNum (n : ℕ) (qk : fst k ≡ # n) where
          module R = Recover Z n (Env T e' e s k z Z) i2 i4 i6 qk refl (Rd.b-env hb)
            using ( g; recovers )
```

恢复出的索引借助 `Z` 的指名其外围取值，而恢复等式说：扩展环境所命名的恰是这些外围取值，顺序即索引排列的顺序。

```agda
          g′ : Fin n → V ℓ
          g′ i = ⟪ fst Z ⟫↪ (R.g i)
          hE : fst e ≡ env g′
          hE = R.recovers
```

为证明唯一性，取两份具有相同 `Z`、参数环境 `e` 与公式键 `s` 的体见证。解码第一份见证的元数数码，便固定恢复参数序列的共同长度 `n`。

```agda
      module WitnessUnique (Z e s z T e' k : CS.S)
        (hb : ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩)
        (z' T₂ e'₂ k₂ : CS.S)
        (hb₂ : ⟨ Env T₂ e'₂ e s k₂ z' Z ⊨ bodyFo ⟩)
        (n : ℕ) (qk : fst k ≡ # n) where
```

层子句把 `z` 与 `z'` 化为 `Lset lam` 的元素，因而可用该层的良序比较它们；第一份见证的解码则给出两个体共同使用的参数序列。

```agda
        module A₁ = WitnessBody z T e' e s k Z hb
        module A₂ = WitnessBody z' T₂ e'₂ e s k₂ Z hb₂
        module N = A₁.AtNum n qk
        zS : SL
        zS = fst z , A₁.h7
```

第二个元素同样打包。两条扩展等式说：每个体的环境都是参数环境添加自己的被见证元素后的扩展，`e'` 命名「把 `z` 添加到恢复值之前」，`e'₂` 以同样方式命名 `z'`。

```agda
        z'S : SL
        z'S = fst z' , A₂.h7
        e'≡ : fst e' ≡ env (cons (fst z) N.g′)
        e'≡ = A₁.Rd.b-cons N.g′ N.hE hb
        e'₂≡ : fst e'₂ ≡ env (cons (fst z') N.g′)
```

随后证明两个表槽位一致。两个体都断言「键 `s` 与自己的表组成的对」属于表族的诸对，而码命名的单射性迫使与同一键配对的两个表相等。

```agda
        e'₂≡ = A₂.Rd.b-cons N.g′ N.hE hb₂
        T≡ : fst T ≡ fst T₂
        T≡ =
          let p = SM.pairs-out s T (A₁.Rd.b-tab hb)
              q = SM.pairs-out s T₂ (A₂.Rd.b-tab hb₂)
```

表等式由两条表子句的外向读法组装：每个表都是键所指名的取值，而码命名的单射性认同两把键的码索引。随后准备陈述 `not-below`：严格更小的可构造元素若带有自己的体见证、且其扩展落在对方的表中，则不可能。

```agda
          in snd p ∙ cong (λ m → fst (SM.valOf s m))
            (snd (fst s ∈ fst (AllCodes A)) (fst p) (fst q)) ∙ sym (snd q)
        not-below : (a b : CS.S) (ha : ⟨ fst a ∈ fst A ⟩) (hb' : ⟨ fst b ∈ fst A ⟩)
                    (Ta e'a ka : CS.S) (hba : ⟨ Env Ta e'a e s ka a Z ⊨ bodyFo ⟩)
                    (e'b : CS.S) → fst e'b ≡ env (cons (fst b) N.g′) → ⟨ fst e'b ∈ fst Ta ⟩
```

若一个可构造候选严格低于某见证，且其延拓环境属于同一张表，最小性子句便给出矛盾。层上的良序提供该子句所需的内部比较关系。

```agda
                  → relOf wL (fst b , hb') (fst a , ha) → Empty.⊥
        not-below a b ha hb' Ta e'a ka hba e'b qe hm b<a =
          BodyRd.b-min Ta e'a e s ka a Z N.g′ N.hE hba b hb' e'b qe hm
            (relL-fill lam λ-isL ordλ (fst b , hb') (fst a , ha) b<a)
        result : fst z ≡ fst z'
```

结果由内部良序在两个打包见证上的三歧性得出。若 `z` 低于 `z'`，则更小的 `z` 将与 `z'` 的体所记录的最小性矛盾，此时共享的表经由表等式供给。

```agda
        result = go (SWO.tri∙ wL zS z'S)
          where
          go : Tri∙ (relOf wL zS z'S) (zS ≡ z'S) (relOf wL z'S zS) → fst z ≡ fst z'
          go (tri-lt h) = Empty.rec (not-below z' z A₂.h7 A₁.h7 T₂ e'₂ k₂ hb₂ e' e'≡
                        (subst (λ t → ⟨ fst e' ∈ t ⟩) T≡ A₁.h6) h)
```

若两个打包见证相等，则其底层集合相等。余下的严格次序情形与前者对称：若 `z'` 低于 `z`，便与 `z` 的最小性矛盾。

```agda
          go (tri-eq q) = cong fst q
          go (tri-gt h) = Empty.rec (not-below z z' A₁.h7 A₂.h7 T e' k hb e'₂ e'₂≡
                        (subst (λ t → ⟨ fst e'₂ ∈ t ⟩) (sym T≡) A₂.h6) h)
```

最小见证的唯一性由此组装：同一 `Z`、`e`、`s` 的两个见证具有相等的底层元素。两层截断被一起消耗，目标是 h-集合中的等式。

```agda
    opaque
      leastWitness-unique : (Z e s z z' : CS.S) → LeastWitness Z e s z
                          → LeastWitness Z e s z' → fst z ≡ fst z'
      leastWitness-unique Z e s z z' = PT.rec2 (setIsSet (fst z) (fst z')) inner
        where
```

内层引理接收两份拆开的体见证：候选元素 `z` 与 `z'` 各自的表、扩展、键与体满足。

```agda
        inner : (Σ[ T ∈ CS.S ] Σ[ e' ∈ CS.S ] Σ[ k ∈ CS.S ]
                   ⟨ Env T e' e s k z Z ⊨ bodyFo ⟩)
              → (Σ[ T₂ ∈ CS.S ] Σ[ e'₂ ∈ CS.S ] Σ[ k₂ ∈ CS.S ]
                   ⟨ Env T₂ e'₂ e s k₂ z' Z ⊨ bodyFo ⟩)
              → fst z ≡ fst z'
```

第一条键被解码为一个数码，使前述唯一性论证可在该元数处进行。同一解码原理写成 `ω-num`：内部 `ω` 的每个成员在命题截断意义下都是某个外围数码 `# n`。

```agda
        inner (T , e' , k , hb) (T₂ , e'₂ , k₂ , hb₂) =
          PT.rec (setIsSet (fst z) (fst z'))
            (λ { (n , qk) → WitnessUnique.result Z e s z T e' k hb z' T₂ e'₂ k₂ hb₂ n qk })
            (decode-num k (BodyRd.b-num T e' e s k z Z hb))
    ω-num : (q : CS.S) → ⟨ fst q ∈ˢ fst ωʟ ⟩ → ∥ Σ[ n ∈ ℕ ] (fst q ≡ # n) ∥₁
```

解码把内部 `ω` 的成员映射为自然数并附数码等式；`vecOf` 把 `Fin k` 上的函数变成长度 `k` 的可构造元素向量，即满足子句所消耗的形态。

```agda
    ω-num q h = PT.map (λ { (n , e) → lower n , (e ∙ numeralL-fst (lower n)) })
      (subst ⟨_⟩ (ω-specL q) h)
    vecOf : {k : ℕ} → (Fin k → SL) → Vec SL k
    vecOf {zero} f = []
    vecOf {suc k} f = f zero ∷ vecOf (λ i → f (suc i))
```

在 `vecOf f` 中逐项查找会恢复 `f`。现固定集合 `Z`、元数 `k`、含一个见证变量与 `k` 个参数变量的公式 `χ`、取自 `Z` 的参数向量 `vs`，以及 `χ` 在 `vs` 处有见证的证据。

```agda
    lookup-vecOf : {k : ℕ} (f : Fin k → SL) (i : Fin k) → lookup i (vecOf f) ≡ f i
    lookup-vecOf {suc k} f zero = refl
    lookup-vecOf {suc k} f (suc i) = lookup-vecOf (λ j → f (suc j)) i
    module Least (Z : CS.S) (k : ℕ) (χ : Formula (⊥* {ℓ}) (suc k)) (vs : Vec SL k)
                 (from : From Z vs) (w₀ : Sat k χ vs) where
```

被最小化的谓词说：元素 `a` 使扩展环境 `(a ∷ vs)` 满足 `χ`。它被打包为命题，故可充当良序的最小性谓词。

```agda
      P : SL → hProp (ℓ-suc ℓ)
      P a = (a ∷ vs) ⊨₀ χ
```

最小见证 `a` 由 `L` 的内部良序上的最小元搜索选取，施用于该谓词与非空记录。

```agda
      a : SL
      a = leastOf wL {ℓ'' = ℓ-suc ℓ} lem P w₀ .fst
```

其最小性数据被完整保留：`a` 满足该谓词，而良序中没有更小的元素满足它。

```agda
      a-least : IsLeast wL P a
      a-least = leastOf wL {ℓ'' = ℓ-suc ℓ} lem P w₀ .snd
```

所选见证 `a` 属于 `Lset lam`，因此可构造，可视为可构造载体中的元素 `aS`。对每个参数位置，`g` 在 `Z` 的呈现中选择一个指名该参数的索引。

```agda
      aS : CS.S
      aS = fst a , Lset→isL lam ordλ (fst a) (snd a)
      g : Ix Z k
      g i = fiber (fst Z) (from i) .fst
```

命名等式说：每个参数的索引所呈现的恰是该参数；被嵌入的索引作为 `L` 的元素等于该参数。

```agda
      g-val : (i : Fin k) → ⟪ fst Z ⟫↪ (g i) ≡ fst (lookup i vs)
      g-val i = fiber (fst Z) (from i) .snd
```

参数的外围取值收于 `g′`，每槽一个，使参数环境既能在内部、也能在外围被描述。

```agda
      g′ : Fin k → V ℓ
      g′ i = ⟪ fst Z ⟫↪ (g i)
```

参数环境 `e` 是这些取值在 `Z` 之上的内部图；`ext b` 是候选 `b` 的扩展环境：即把 `b` 添到参数之前的那个环境。

```agda
      e : CS.S
      e = envS Z g
      ext : SL → CS.S
      ext b = envFor A (b ∷ vs)
```

扩展的图等式说：其底层集合是「候选 `b` 添加到外围参数值之前」的图；扩展的两种读法逐条目被等同。

```agda
      ext-graph : (b : SL) → fst (ext b) ≡ env (cons (fst b) g′)
      ext-graph b = envFor-graph A (b ∷ vs)
        ∙ cong env (funExt (λ { zero → refl ; (suc i) → sym (g-val i) }))
```

扩展属于 `χ` 在元数 `suc k` 处的满足表，恰当扩展环境满足 `χ`。这里的表是仅属于这条公式的表，而这条等式使「属于表」可以换读为「满足」。

```agda
      ext-sat : (b : SL) → (ext b CS.∈ˢ Tof (suc k) χ) ≡ ((b ∷ vs) ⊨₀ χ)
      ext-sat b = sat-at (suc k) χ (b ∷ vs) (ext b) (envFor-graph A (b ∷ vs))
```

键 `sS` 点名公式及其元数：它正是表族用以索引 `χ` 之表的那个对。

```agda
      sS : CS.S
      sS = keyOf (suc k) χ
```

表 `T` 是 `χ` 在元数 `suc k` 处的满足表，即收集满足扩展的那个集合。

```agda
      T : CS.S
      T = Tof (suc k) χ
```

七条目环境 `γ₇` 把整个图景装配起来：表、由最小见证扩展的环境、参数环境、键、元数的数码、打包后的见证，以及基集合 `Z`。

```agda
      γ₇ : CS.S ^ 7
      γ₇ = Env T (ext a) e sS (nn k) aS Z
```

第一条子句记录：元数的数码属于内部 `ω`，因为环境的长度是自然数。

```agda
      c1 : ⟨ γ₇ ⊨ (var i4 ∈̇ con ωʟ) ⟩
      c1 = #∈ω k
```

键子句说：键属于码集，并且是「后继数码与 `χ` 的码」组成的对；该码是自由码，而自由码住在 `ω` 的极限层中。

```agda
      c2 : ⟨ γ₇ ⊨ keyIn i3 i4 ⟩
      c2 = KeyIn.keyIn-in i3 i4 γ₇ k refl
        (subst (λ u → ⟨ u ∈ˢ fst C₀ ⟩) (sym (keyOf-fst (suc k) χ)) (freeCode-in (suc k) χ))
        (fst (limitCode χ)) (keyOf-fst (suc k) χ)
```

环境子句说：参数环境是 `Z` 上长度 `nn k`、取值 `g′` 的环境；它从 `e` 的环境引理被传输到七条目语境。

```agda
      c3 : ⟨ γ₇ ⊨ envOverAt i2 i4 i6 ⟩
      c3 = envOverAt-transport (Z ∷ nn k ∷ e ∷ []) γ₇ i2 i1 i0 i2 i4 i6 refl refl refl
             (envOver Z g)
```

扩展等式重复：由最小见证扩展的环境，是把见证添加到参数值之前所得的图。

```agda
      c4 : fst (ext a) ≡ env (cons (fst a) g′)
      c4 = ext-graph a
```

键与表组成的对属于表族的诸对；表正是以这样的对被其键索引。

```agda
      c5 : ⟨ pr (fst sS) (fst T) ∈ˢ fst SM.pairs ⟩
      c5 = Tof-pair (suc k) χ
```

由最小见证得到的扩展属于表：表的隶属等式把它读作对 `χ` 的满足，而最小性数据恰供给了这份满足。

```agda
      c6 : ⟨ fst (ext a) ∈ˢ fst T ⟩
      c6 = transport (sym (cong ⟨_⟩ (ext-sat a))) (a-least .fst)
```

最小见证属于层 `Lset lam`；在内部表示 `A = LsetS lam ordλ` 中，这正是 `a` 所携带的隶属证明。

```agda
      c7 : ⟨ fst aS ∈ˢ fst A ⟩
      c7 = snd a
```

最小性子句排除 `Lset lam` 中每个满足如下条件的候选 `w'`：若其延拓环境属于该表，则其打包形式不可能严格低于所选见证。这正是 `a` 的最小性。

```agda
      c8 : BodyRd.Min T (ext a) e sS (nn k) aS Z g′
      c8 w' w'∈ e'' q hm hr = a-least .snd w'S sat lt'
        where
        w'S : SL
        w'S = fst w' , w'∈
```

较小候选与 `a` 之间的内部关系，由限制在可构造元素上的外围良序填充；而该候选满足 `χ`：其扩展属于表，经扩展等式读作满足。

```agda
        lt' : relOf-at w'S a
        lt' = relL-rep lam λ-isL ordλ w'S a hr
        sat : ⟨ (w'S ∷ vs) ⊨₀ χ ⟩
        sat = transport (cong ⟨_⟩ (ext-sat w'S))
                (subst (λ t → ⟨ t ∈ˢ fst T ⟩) (q ∙ sym (ext-graph w'S)) hm)
```

八条子句合起来证明 `witFo` 在 `(aS, Z)` 处成立：`a` 是 `χ` 在所选参数上的最小见证，而且这一事实完全在可构造结构内部表达。接下来假设 `Z` 的每个成员都属于 `Lset lam`，并把同一份体数据读到外围。

```agda
      least : ⟨ (aS ∷ Z ∷ []) ⊨ witFo ⟩
      least = witFo-in aS Z T (ext a) e sS (nn k)
        (BodyRd.b-fill T (ext a) e sS (nn k) aS Z g′ refl c1 c2 c3 c4 c5 c6 c7 c8)
    module Out (Z : CS.S) (Z⊆ : (z : S) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
               (w T e' e s k : CS.S) (h : ⟨ Env T e' e s k w Z ⊨ bodyFo ⟩) where
```

一份体见证提供八项事实：元数数码、键的形状、恢复出的参数环境、延拓等式、带索引的表、表隶属、层隶属与最小性。把这些事实读到外围，便可重建该码所表示的语义搜索。

```agda
      module Rd = BodyRd T e' e s k w Z
        using ( b-num; b-key; b-env; b-cons; b-tab; b-mem; b-stage; b-min )
```

层子句证明被见证集合 `w` 属于 `Lset lam`。把 `w` 与这份证明配对，得到层载体中的相应元素 `wS`。

```agda
      wS : SL
      wS = fst w , Rd.b-stage h
```

已解码键的元数分量属于内部 `ω`，因此在命题截断意义下等于某个数码 `# n`。固定这样的 `n` 后，便可在通常的自然数元数处分析该键。

```agda
      module AtNum (n : ℕ) (qk : fst k ≡ # n) where
```

在此情形中，第一条事实说：键的槽位分量 `s` 本身就是一个码，即 `C₀` 的成员。这由键的求逆得出：键是有序对「元数数码与码」，把对拆开便显现出码。

```agda
        s∈ : ⟨ fst s ∈ˢ fst C₀ ⟩
        s∈ = KeyIn.keyIn-out i3 i4 (Env T e' e s k w Z) n qk (Rd.b-key h) .fst
```

把元数认同为 `n` 后，环境子句恢复出函数 `g : Fin n → ⟪ fst Z ⟫`，并证明编码的参数环境正是这些索引所指名之值的图。

```agda
        module R = Recover Z n (Env T e' e s k w Z) i2 i4 i6 qk refl (Rd.b-env h) using ( g; recovers )
```

恢复出的环境列出起始集合的索引。每个索引经由其呈现的嵌入被实现为外围元素，得到底层集构成的向量 `g′`。

```agda
        g′ : Fin n → V ℓ
        g′ i = ⟪ fst Z ⟫↪ (R.g i)
```

向量 `vs` 把同样的元素收集为可构造载体的条目，并为每个条目配上其可构造性的证明。

```agda
        vs : Vec SL n
        vs = vecOf (λ i → g′ i , Z⊆ (g′ i) (member (fst Z) (R.g i)))
```

对每个位置 `i`，`lookup i vs` 的第一分量都是 `g′ i`。因此 `vs` 与 `g′` 描述同一参数序列，前者把它写成层载体的元素，后者把它写成外围集合。

```agda
        vs-val : (i : Fin n) → fst (lookup i vs) ≡ g′ i
        vs-val i = cong fst (lookup-vecOf (λ i → g′ i , Z⊆ (g′ i) (member (fst Z) (R.g i))) i)
```

恢复出的环境确实来自起始集合：`vs` 的每个条目作为集合都是 `Z` 的成员。这正是 `From Z vs` 记录。

```agda
        from : From Z vs
        from i = subst (λ u → ⟨ u ∈ˢ fst Z ⟩) (sym (vs-val i)) (member (fst Z) (R.g i))
```

恢复等式把原环境分量 `e` 与 `env g′` 同一视；后者是由恢复出的外围取值形成的图。

```agda
        hE : fst e ≡ env g′
        hE = R.recovers
```

见证槽位与其他候选的比较，通过把恢复的环境延长一个条目来进行：`ext b` 即把 `b` 前置到 `vs` 之前的环境。

```agda
        ext : SL → CS.S
        ext b = envFor A (b ∷ vs)
```

这一延拓的底层环境计算为 `b` 的底层集与 `g′` 的 cons：延拓环境的图描述逐条目吻合。

```agda
        ext-graph : (b : SL) → fst (ext b) ≡ env (cons (fst b) g′)
        ext-graph b = envFor-graph A (b ∷ vs)
          ∙ cong env (funExt (λ { zero → refl ; (suc i) → vs-val i }))
```

键自身的环境分量被认同为 `ext wS`：把恢复的环境以见证槽延拓，正是键所记录的内容。

```agda
        e'≡ : fst e' ≡ fst (ext wS)
        e'≡ = Rd.b-cons g′ hE h ∙ sym (ext-graph wS)
```

现取从码分量解出的公式 `χ`，并把 `s` 与其典范键 `keyOf (suc n) χ` 同一视。于是环境、公式与键都描述同一个满足查询。

```agda
        module AtCode (χ : Formula (⊥* {ℓ}) (suc n)) (qs : fst s ≡ fst (keyOf (suc n) χ)) where
```

谓词 `P b` 说：把 `b` 前置到恢复的环境后满足 `χ`。这正是最小见证搜索所最小化的性质。

```agda
          P : SL → hProp (ℓ-suc ℓ)
          P b = (b ∷ vs) ⊨₀ χ
```

在 `χ` 的满足表中的隶属与 `P b` 一致，因为 `ext b` 的环境计算为 `b ∷ vs` 的图。这在满足的编码读法与语义读法之间转换。

```agda
          ext-sat : (b : SL) → ⟨ ext b CS.∈ˢ Tof (suc n) χ ⟩ ≡ ⟨ P b ⟩
          ext-sat b = cong ⟨_⟩ (sat-at (suc n) χ (b ∷ vs) (ext b) (envFor-graph A (b ∷ vs)))
```

键的表分量随后被认同为 `χ` 在提升元数处的满足表；两个分量都解码后，键的成员便可按语义读取。

```agda
          module AtTable (qT : fst T ≡ fst (Tof (suc n) χ)) where
```

见证槽位满足恢复出的公式：键中记录的隶属沿环境与表的同一视搬运，成为 `χ` 在延拓环境处的满足。

```agda
            sat : ⟨ P wS ⟩
            sat = transport (ext-sat wS)
              (subst2 (λ u t → ⟨ u ∈ˢ t ⟩) e'≡ qT (Rd.b-mem h))
```

最小性断言：不存在满足 `χ` 且严格低于 `wS` 的层元素 `b`。`χ` 的满足被换读为 `ext b` 属于恢复出的表，而层上的良序则被换成体的最小性子句所需的内部关系。

```agda
            min : (b : SL) → ⟨ P b ⟩ → relOf-at b wS → Empty.⊥
            min b pb lt = Rd.b-min g′ hE h bS (snd b) (ext b) (ext-graph b) hm
              (relL-fill lam λ-isL ordλ b wS lt)
              where
              bS : CS.S
```

更小的候选被打包为可构造元素 `bS`，其延拓环境被证明落在表中，而这正是键的最小性所反驳的隶属。

```agda
              bS = fst b , Lset→isL lam ordλ (fst b) (snd b)
              hm : ⟨ fst (ext b) ∈ˢ fst T ⟩
              hm = subst (λ t → ⟨ fst (ext b) ∈ˢ t ⟩) (sym qT) (transport (sym (ext-sat b)) pb)
```

两条事实合成为「`χ` 在恢复环境处可满足」的见证：见证槽位连同其满足被截断为 `Sat`。

```agda
            w₀ : Sat n χ vs
            w₀ = ∣ wS , sat ∣₁
```

恢复出的元数 `n`、公式 `χ`、参数向量 `vs` 与见证 `w₀` 组成一次语义搜索。最小元的唯一性把搜索结果 `search n χ vs w₀` 与原被见证集合 `w` 同一视；另一方面，表子句开始证明恢复出的表正是 `χ` 的满足表。

```agda
            searched : Searched Z (fst w)
            searched = n , χ , vs , w₀ , (from , sym (cong (λ q → fst (fst q))
              (isPropLeastOf wL P (leastOf wL {ℓ'' = ℓ-suc ℓ} lem P w₀) (wS , (sat , min)))))
          table : ∥ Searched Z (fst w) ∥₁
          table = ∣ AtTable.searched
```

表子句把 `T` 的底层集合表示为键 `s` 所对应的值。由于 `s` 已与 `χ` 在元数 `suc n` 处的典范键同一视，该键之值的唯一性给出 `fst T ≡ fst (Tof (suc n) χ)`。

```agda
            (snd p ∙ cong fst (valOf-same s (fst p) (suc n) χ qs)) ∣₁
            where
            p : Σ[ m ∈ ⟨ s CS.∈ˢ AllCodes A ⟩ ] (fst T ≡ fst (SM.valOf s m))
            p = SM.pairs-out s T (Rd.b-tab h)
```

为解码码分量 `s`，`freeCode-out` 给出一条公式 `χ`，其自由码正是该分量。随后依次复合槽位等式、解码所得的码等式与 `keyOf` 的计算等式，便把 `s` 与 `χ` 的典范键同一视。

```agda
        code : ∥ Searched Z (fst w) ∥₁
        code = PT.rec squash₁
          (λ { (c , qc) → PT.rec squash₁
            (λ { (χ , ec) → AtCode.table χ
                   (qc ∙ cong (pr (# (suc n))) ec ∙ sym (keyOf-fst (suc n) χ)) })
```

键等式给出编码槽位与解码公式之间的最后联系。因此在这个数码情形中得到截断的 `Searched Z (fst w)`：被见证集合正是以从 `Z` 恢复的参数进行最小见证搜索所得的结果。

```agda
            (freeCode-out (suc n) c (subst (λ u → ⟨ u ∈ˢ fst C₀ ⟩) qc s∈)) })
          (KeyIn.keyIn-out i3 i4 (Env T e' e s k w Z) n qk (Rd.b-key h) .snd)
```

每份体见证所记录的元数都属于内部 `ω`，因此数码解码把前述分析推广为每份见证的一次截断语义搜索。作分离时取界 `Bnd Z = Z ∪ A`，其中 `A` 是 `Lset lam` 的内部表示。

```agda
      searched : ∥ Searched Z (fst w) ∥₁
      searched = PT.rec squash₁ (λ { (n , qk) → AtNum.code n qk }) (ω-num k (Rd.b-num h))
    Bnd : CS.S → CS.S
    Bnd Z = cupʟ Z A
```

`Z` 的成员由并的左包含落入界内。

```agda
    bnd-Z : (Z z : CS.S) → ⟨ fst z ∈ˢ fst Z ⟩ → ⟨ z CS.∈ˢ Bnd Z ⟩
    bnd-Z Z z = cupʟ-inl Z A (fst z)
```

`Lset lam` 的每个成员都由右包含进入 `Bnd Z`。一步闭包条件于是有三种情形：`Z` 的旧成员、无见证时使用的空集，或与基 `Z` 一起满足 `witFo` 的集合 `w`。

```agda
    bnd-L : (Z z : CS.S) → ⟨ fst z ∈ˢ Lset lam ⟩ → ⟨ z CS.∈ˢ Bnd Z ⟩
    bnd-L Z z = cupʟ-inr Z A (fst z)
    Body : CS.S → CS.S → Type (ℓ-suc ℓ)
    Body Z w = ⟨ fst w ∈ˢ fst Z ⟩ ⊎ ((fst w ≡ ∅) ⊎ ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩)
```

在第三种情形中，`witFo` 所编码的层子句直接证明 `w ∈ Lset lam`。因此每个新加入的最小见证都留在固定层内。

```agda
    wit-L : (Z w : CS.S) → ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩ → ⟨ fst w ∈ˢ Lset lam ⟩
    wit-L Z w hw = PT.rec (snd (fst w ∈ˢ Lset lam))
      (λ { (T , e' , e , s , k , h) → BodyRd.b-stage T e' e s k w Z h })
      (witFo-out w Z hw)
    opaque
```

分离公式在可构造结构内部表达这三种情形：属于 `Z`、等于空集，或满足改名后的 `witFo`。改名把它的两个自由变量放入存在包所形成的槽位。

```agda
      sepFo : CS.S → Formula CS.S 1
      sepFo Z = (var i0 ∈̇ con Z)
              ∨̇ ( (var i0 ≐ con ∅ʟ)
                ∨̇ ∃̇ ( (var i0 ≐ con Z) ∧̇ renameFo ρs witFo ) )
```

这次改名只交换环境中的两个条目。因此，改名后的 `witFo` 在 `(Z'', w)` 处的真值，等于原 `witFo` 在 `(w, Z'')` 处的真值。

```agda
      private
        rs : (Z'' w : CS.S)
           → ⟨ (Z'' ∷ w ∷ []) ⊨ renameFo ρs witFo ⟩ ≡ ⟨ (w ∷ Z'' ∷ []) ⊨ witFo ⟩
        rs Z'' w = cong ⟨_⟩ (Ren.⊨-rename ρs witFo (Z'' ∷ w ∷ []) (w ∷ Z'' ∷ []) (ags Z'' w))
```

分离公式的满足分解为体的三个截断情形：属于 `Z`、与空集相等，或一个其见证指认定义域的存在情形。

```agda
      sep-out : (Z w : CS.S) → ⟨ (w ∷ []) ⊨ sepFo Z ⟩ → ∥ Body Z w ∥₁
      sep-out Z w = PT.rec squash₁ (λ
        { (inl hz) → ∣ inl hz ∣₁
        ; (inr h') → PT.rec squash₁ (λ
          { (inl e) → ∣ inr (inl e) ∣₁
```

在存在情形中，其见证 `Z''` 等于固定参数 `Z`。先沿这条等式、再沿改名路径搬运，便得到 `witFo` 在 `(w, Z)` 处成立。

```agda
          ; (inr hw) → PT.map (λ { (Z'' , (eZ , hr)) → inr (inr
              (subst (λ u → ⟨ (w ∷ u ∷ []) ⊨ witFo ⟩) (S≡ {x = Z''} {y = Z} eZ)
                (transport (rs Z'' w) hr))) }) hw }) h' })
```

反过来，体的三种情形各自产生分离公式相应的满足，并在需要处重新包上改名。

```agda
      sep-in : (Z w : CS.S) → Body Z w → ⟨ (w ∷ []) ⊨ sepFo Z ⟩
      sep-in Z w (inl hz) = ∣ inl hz ∣₁
      sep-in Z w (inr (inl e)) = ∣ inr ∣ inl e ∣₁ ∣₁
      sep-in Z w (inr (inr hw)) = ∣ inr ∣ inr ∣ Z , (refl , transport (sym (rs Z w)) hw) ∣₁ ∣₁ ∣₁
```

在 `L` 内作分离，从 `Bnd Z` 中恰好选出满足 `sepFo Z` 的集合；所得可构造集记为 `Φ Z`。其隶属路径把「属于 `Φ Z`」同一视为「属于该界并满足公式」。

```agda
    opaque
      Φ : CS.S → CS.S
      Φ Z = hasSeparationL (Bnd Z) (sepFo Z) .fst .fst
```

隶属规格读作：`w` 属于 `Φ Z`，当且仅当 `w` 属于界 `Bnd Z` 且满足分离公式。

```agda
      Φ-mem : (Z w : CS.S) → (w CS.∈ˢ Φ Z) ≡ ((w CS.∈ˢ Bnd Z) ⊓ ((w ∷ []) ⊨ sepFo Z))
      Φ-mem Z = hasSeparationL (Bnd Z) (sepFo Z) .fst .snd
```

体的每种情形都落入 `Φ Z`。隶属情形经界进入；证明把每个析取支产生的界隶属与其分离满足打包。

```agda
    Φ-in : (Z w : CS.S) → Body Z w → ⟨ fst w ∈ˢ fst (Φ Z) ⟩
    Φ-in Z w b = subst ⟨_⟩ (sym (Φ-mem Z w)) (bnd b , sep-in Z w b)
      where
      bnd : Body Z w → ⟨ w CS.∈ˢ Bnd Z ⟩
      bnd (inl hz) = bnd-Z Z w hz
```

空集情形属于该界，因为 `∅ ∈ Lset lam`。见证情形也属于该界，因为 `witFo` 的层子句证明其取值属于 `Lset lam`。

```agda
      bnd (inr (inl e)) = bnd-L Z w (subst (λ u → ⟨ u ∈ˢ Lset lam ⟩) (sym e) HSH.∅∈Lsetα)
      bnd (inr (inr hw)) = bnd-L Z w (wit-L Z w hw)
```

反过来，`Φ Z` 中的隶属由隶属规格与分离读法给出截断的体情形。为写双条件公式，体随后改写为三空位排列。

```agda
    Φ-out : (Z w : CS.S) → ⟨ fst w ∈ˢ fst (Φ Z) ⟩ → ∥ Body Z w ∥₁
    Φ-out Z w h = sep-out Z w (subst ⟨_⟩ (Φ-mem Z w) h .snd)
    opaque
      bodyF : Formula CS.S 3
      bodyF = (var i0 ∈̇ var i2) ∨̇ ((var i0 ≐ con ∅ʟ) ∨̇ renameFo ρf witFo)
```

图公式 `ΦFo` 对新集合 `w` 作全称量化，并陈述 `w ∈ Z'` 与三种情形组成的条件 `Body Z w` 之间的两个蕴涵。因此 `(Z', Z)` 满足 `ΦFo`，恰当 `Z'` 与 `Φ Z` 具有相同成员。

```agda
      ΦFo : Formula CS.S 2
      ΦFo = ∀̇ ( ((var i0 ∈̇ var i1) ⇒̇ bodyF) ∧̇ (bodyF ⇒̇ (var i0 ∈̇ var i1)) )
```

图的改名等式与之前的同名引理一样证明：改名置换环境，满足沿置换搬运。

```agda
      private
        rf : (w Z' Z : CS.S)
           → ⟨ (w ∷ Z' ∷ Z ∷ []) ⊨ renameFo ρf witFo ⟩ ≡ ⟨ (w ∷ Z ∷ []) ⊨ witFo ⟩
        rf w Z' Z = cong ⟨_⟩ (Ren.⊨-rename ρf witFo (w ∷ Z' ∷ Z ∷ []) (w ∷ Z ∷ []) (agf w Z' Z))
```

体在三空位排列下双向转移：属于 `Z` 是直接的，其余析取支经截断映射。

```agda
        bodyF-out : (w Z' Z : CS.S) → ⟨ (w ∷ Z' ∷ Z ∷ []) ⊨ bodyF ⟩ → ∥ Body Z w ∥₁
        bodyF-out w Z' Z = PT.rec squash₁ (λ
          { (inl hz) → ∣ inl hz ∣₁
          ; (inr h') → PT.map (λ
            { (inl e) → inr (inl e)
```

在见证情形中，改名路径把三槽公式的满足换回 `witFo` 在 `(w, Z)` 处的满足，从而完成由图公式体到 `Body Z w` 的正向蕴涵。

```agda
            ; (inr hw) → inr (inr (transport (rf w Z' Z) hw)) }) h' })
```

逆向把三种情形组装成三空位读法，并逆着改名搬运见证析取支。

```agda
        bodyF-in : (w Z' Z : CS.S) → Body Z w → ⟨ (w ∷ Z' ∷ Z ∷ []) ⊨ bodyF ⟩
        bodyF-in w Z' Z (inl hz) = ∣ inl hz ∣₁
        bodyF-in w Z' Z (inr (inl e)) = ∣ inr ∣ inl e ∣₁ ∣₁
        bodyF-in w Z' Z (inr (inr hw)) = ∣ inr ∣ inr (transport (sym (rf w Z' Z)) hw) ∣₁ ∣₁
```

随后证明可定义性条款：对 `(Φ Z, Z)` 满足图公式。双条件的每个方向都是相应隶属方向与体转移的复合。

```agda
      Φ-defines : (Z : CS.S) → ⟨ (Φ Z ∷ Z ∷ []) ⊨ ΦFo ⟩
      Φ-defines Z w =
          (λ h → PT.rec (snd ((w ∷ Φ Z ∷ Z ∷ []) ⊨ bodyF)) (bodyF-in w (Φ Z) Z) (Φ-out Z w h))
        , (λ h → PT.rec (snd (fst w ∈ˢ fst (Φ Z))) (Φ-in Z w) (bodyF-out w (Φ Z) Z h))
```

图的唯一性由可构造结构的外延性证明：对任何「其与 `Z` 的对满足图公式」的 `Z'`，`Z'` 的每个成员都满足体，而 `Φ-in` 把它放入 `Φ Z`。

```agda
      Φ-only : (Z Z' : CS.S) → ⟨ (Z' ∷ Z ∷ []) ⊨ ΦFo ⟩ → Z' ≡ Φ Z
      Φ-only Z Z' h = extensionalL (λ v → ⇔toPath (fwd v) (bwd v))
        where
        fwd : (v : CS.S) → ⟨ fst v ∈ˢ fst Z' ⟩ → ⟨ fst v ∈ˢ fst (Φ Z) ⟩
        fwd v hv = PT.rec (snd (fst v ∈ˢ fst (Φ Z))) (Φ-in Z v) (bodyF-out v Z' Z (h v .fst hv))
```

外延性论证的反向把 `Φ Z` 的每个成员读作截断的体情形，并在该成员处应用图公式。

```agda
        bwd : (v : CS.S) → ⟨ fst v ∈ˢ fst (Φ Z) ⟩ → ⟨ fst v ∈ˢ fst Z' ⟩
        bwd v hv = h v .snd
          (PT.rec (snd ((v ∷ Z' ∷ Z ∷ []) ⊨ bodyF)) (bodyF-in v Z' Z) (Φ-out Z v hv))
```

由此得到可定义的一步运算 `Φ`：公式 `ΦFo` 刻画其图，而外延性证明任何满足该图条件的集合都等于 `Φ Z`。

```agda
    pack : StepPack
    pack = record
      { Φ       = Φ
      ; ΦFo     = ΦFo
      ; defines = Φ-defines
```

这一步包含 `Z` 的每个旧成员，始终包含空集，并对每条以 `Z` 中元素为参数且可满足的公式包含其最小见证。反过来，它的成员只来自这三种情形，因此 `Φ` 恰是所需的一步闭包。

```agda
      ; only    = Φ-only
      ; grows   = λ Z z hz → Φ-in Z (z , isL-trans {x = fst Z} {y = z} hz (snd Z)) (inl hz)
      ; junk    = λ Z → Φ-in Z ∅ʟ (inr (inl refl))
      ; least   = λ Z k χ vs from w₀ →
                    Φ-in Z (Least.aS Z k χ vs from w₀) (inr (inr (Least.least Z k χ vs from w₀)))
```

假设 `Z` 的每个成员都属于 `Lset lam`。若 `z ∈ Φ Z`，隶属刻画给出三种可能：`z` 原已属于 `Z`，`z = ∅`，或 `witFo` 在 `(z, Z)` 处成立。在第三种情形中，解码公式体会重建一次以 `Z` 中元素为参数、结果为 `z` 的语义搜索。

```agda
      ; out     = λ Z Z⊆ z hz → PT.rec squash₁ (λ
          { (inl h') → ∣ inl h' ∣₁
          ; (inr (inl e)) → ∣ inr (inl e) ∣₁
          ; (inr (inr hw)) → PT.rec squash₁
              (λ { (T , e' , e , s , k , hb) →
```

在见证情形中，`z ∈ Φ Z` 先给出 `z` 的可构造性，使它可被读作可构造载体的元素。解码后的公式体再证明 `Searched Z z`，把 `z` 与恢复出的公式和参数所决定的最小见证搜索同一视。

```agda
                 PT.map (λ sr → inr (inr sr)) (Out.searched Z Z⊆ (zS Z z hz) T e' e s k hb) })
              (witFo-out (zS Z z hz) Z hw) })
          (Φ-out Z (zS Z z hz) hz) }
      where
      zS : (Z : CS.S) (z : S) → ⟨ z ∈ˢ fst (Φ Z) ⟩ → CS.S
```

由于 `Φ Z` 可构造且可构造性具有传递性，`Φ Z` 的每个成员 `z` 都可构造。

```agda
      zS Z z hz = z , isL-trans {x = fst (Φ Z)} {y = z} hz (snd (Φ Z))
```

## 为凝聚提供可构造性前提

这给出前述解码所需的载体元素，并完成可定义一步闭包的构造。

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

假设壳 `M` 本身可构造。这样便可把 `M` 视为可构造载体，从而应用前面的塌缩论证，而无须假设该壳是传递的。

```agda
  (M-isL : ⟨ isL (HullStage.M lam ordλ succλ X X⊆L ∅∈λ) ⟩) where
```

把 `M` 视为可构造载体后，可得到其塌缩像 `πX`。该像的每个成员都是 `M` 某个成员的塌缩值，而可构造载体定理证明这些值都属于 `L`。

```agda
  module HS = HullStage lam ordλ succλ X X⊆L ∅∈λ using ( M )
  module HSC = HullStage.C lam ordλ succλ X X⊆L ∅∈λ using ( πX )
  module P = PiIn (HS.M , M-isL) using ( πX-isL )
```

因此，每个 `x ∈ πX` 都可构造。现在回到由 `X` 在 `Lset λ` 内生成的壳，并假设 `λ` 是对后继封闭的序数，且 `X` 的每个成员都属于这一层。

```agda
  pixL : (x : S) → ⟨ x ∈ˢ HSC.πX ⟩ → ⟨ isL x ⟩
  pixL = P.πX-isL
module Condense′ (lam : S) (ordλ : IsOrd lam)
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : S) (X⊆L : (x : S) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)
```

还假设 `∅ ∈ λ`，由 `X` 生成的壳框架是初等的，`λ` 是超充分的，并且 `X` 本身可构造。最后一条假设为内部有限迭代提供起点；初等性与超充分性则提供凝聚论证所需的假设。

```agda
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
  (elem : Frame.A.Elementary lam ordλ succλ X X⊆L ∅∈λ)
  (sup : Superadequate lam)
  (X-isL : ⟨ isL X ⟩)
  where
```

这一构造由三个相连的部分组成。码指称初始元素和后续搜索所选取的值；搜索没有见证时则以空集为值。一个可定义运算 `Φ` 完成一步闭包；对 `Φ` 作有限迭代再取并，便构造出一个随后将与 Skolem 壳认同的可构造集合。

```agda
  module T = Telescope lam ordλ succλ X X⊆L ∅∈λ using ( Code; val; Reads; module StepPack )
  module TB = Telescope.Build lam ordλ succλ X X⊆L ∅∈λ using ( pack; Φ )
  module HI = Telescope.HullIter lam ordλ succλ X X⊆L ∅∈λ X-isL TB.pack
    using ( hullL; hullL-spec; hullStep; hullStep-suc; hullStep-in; hullStep⊆Hull; depth; M-isL )
  module HS = HullStage lam ordλ succλ X X⊆L ∅∈λ using ( M )
```

有限闭包层之并已经构成可构造宇宙中的元素 `hullL`。接下来的等式将证明其底层集合恰是外围定义的壳 `M`；这便会给出上文处理塌缩像时所用的整体可构造性前提。

```agda
  module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ using ( Hull⊆L )
  module HSC = HullStage.C lam ordλ succλ X X⊆L ∅∈λ using ( πX )
  module D = Discharge lam ordλ succλ X X⊆L ∅∈λ HI.M-isL using ( pixL )
  hullL : CS.S
  hullL = HI.hullL
```

`hullL` 的底层集合恰是 `M`。因此，Skolem 壳的外围刻画与迭代所得的可构造集合描述了同样的成员，而 `hullL` 还携带其可构造性的证明。

```agda
  hullL-spec : fst hullL ≡ HS.M
  hullL-spec = HI.hullL-spec
```

壳的闭包层以自然数为索引：`hullStep n` 是闭包步骤施用 `n` 次后到达的层。

```agda
  hullStep : ℕ → CS.S
  hullStep = HI.hullStep
```

在后继索引处，下一层就是把 `Φ` 作用于当前层所得的结果。该运算保留当前成员，加入空集，并为每个参数已经出现的编码搜索加入其最小见证。

```agda
  hullStep-suc : (n : ℕ) → hullStep (suc n) ≡ TB.Φ (hullStep n)
  hullStep-suc = HI.hullStep-suc
```

每个码都有一个有限深度，而它所指称的值属于以该深度为索引的闭包层。由于每个壳成员都由某个码表示，这便为它给出一个包含它的有限层，但并不为该成员选定典范码。

```agda
  hullStep-in : (c : T.Code) → ⟨ fst (T.val c) ∈ˢ fst (hullStep (HI.depth c)) ⟩
  hullStep-in = HI.hullStep-in
```

反过来，每个有限闭包层的每个成员都属于 `M`。结合壳成员的编码刻画，这便证明诸层之并与 Skolem 壳恰有相同的元素。

```agda
  hullStep⊆Hull : (n : ℕ) (z : S) → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ HS.M ⟩
  hullStep⊆Hull = HI.hullStep⊆Hull
```

诸层之并可构造：壳层 `M` 是 `L` 的元素。这是本章要证明的两条隶属事实中的第一条。

```agda
  M-isL : ⟨ isL HS.M ⟩
  M-isL = HI.M-isL
```

第二条经兑现而来：壳层 `M` 的塌缩 `πX` 的每个值都可构造，因为载体 `M` 可构造。

```agda
  pixL : (x : S) → ⟨ x ∈ˢ HSC.πX ⟩ → ⟨ isL x ⟩
  pixL = D.pixL
```

凝聚现在给出一个序数 `β`，使塌缩像恰等于 `Lset β`。由此，先前逐个成员的可构造性陈述加强为把整个像认同为可构造层级中的一个层。结论只断言这一等式与 `β` 的序数性，并未进一步比较 `β` 与 `λ`。

```agda
  condenses′ : Σ[ β ∈ S ] (IsOrd β × (HSC.πX ≡ Lset β))
  condenses′ = Condense.condenses lam ordλ succλ X X⊆L ∅∈λ elem sup D.pixL
```