---
title: "从已计数的起点计数 Skolem 壳"
module: L.GCH.HullCounting
lang: zh
site: "Bedrock"
description: "从已计数的起点计数 Skolem 壳"
stage: "证明 GCH"
reading_order: 117
canonical: https://bedrock.institute/zh/L.GCH.HullCounting.html
html: L.GCH.HullCounting.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/HullCounting.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Axioms.Full, L.Axioms.Infinity, L.Axioms.Numerals, L.Coding.Model, L.Coding.Expressions, L.Coding.CodeConstructibility, L.Coding.Injection, L.Cardinal, L.InjectionComposition, L.DefinableInjection, L.GCH.LeastWitnessMap, L.GCH.CardinalSquareLaw, L.Stage, L.Coding.EnvironmentSet, L.GCH.AdequateStages, L.Coding.SatisfactionGraphSet, L.GCH.SkolemHull, L.GCH.ConstructibleHull, L.GCH.StageCountingTools, L.GCH.FiniteSequenceCoding]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.HullCounting.md, https://bedrock.institute/ja/L.GCH.HullCounting.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
把小集合对可定义的最小见证封闭，应当保持原有的无穷基数界。本章在 `L` 内部证明：若起始集合单射入一个无穷基数，则其 Skolem 壳也单射入该基数。

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

排中律提供局部判定，例如并的一个成员是否属于左侧分支。经典推理只通过一条显式假设进入，因此所得的界准确记录这一假设。

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

固定宇宙层级 `ℓ`，并假设层级 `ℓ-suc ℓ` 上命题的排中律。内部集合、编码图与截断见证都相对于这个固定实例构造。

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

编码图用带相等与隶属的一阶语言表示。合取、析取、否定与存在量化描述各个情形，而满足关系则在外围累积层级中解释。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ¬̇_; ∃̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

论证在序数层与其中的可构造成员之间往返。传递性保证成员仍在 `L` 中，而序数隶属与层的累积性把每个对象放入足以进行可定义选择的层。

```agda
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-layer; layer-trans )
open import L.Ordinal {ℓ} using ( mem-ord; #∈ω )
open import L.Ordinal.Stages {ℓ} lem using ( Lset-cumul; ord∈Lset-suc )
```

计数映射本身必须是 `L` 中的集合。分离构造子图，配对与并构成其编码，充分性则把应用、单值性与定义域的内部公式同其集合论含义连接起来。

```agda
open import L.Axioms.Basic {ℓ} using ( LsetS; ∅ʟ )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Axioms.Numerals {ℓ} using ( pairʟ; unionʟ )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; appAt; appAt-adequate; svAt-out; domAt-in )
```

内部单射由一个可构造图见证，并满足定义域准确、单值、单射和值域有界。`InjCode` 保留具体的图，而 `InjL` 只保留这种图存在这一命题。

```agda
open import L.Coding.Expressions {ℓ} using ( numL; tagAtL; tagAtL-adequate )
open import L.Coding.CodeConstructibility {ℓ}
  using ( sglʟ; sglʟ-in; sglʟ-out; cupʟ; cupʟ-inl; cupʟ-inr; cupʟ-out )
open import L.Coding.Injection {ℓ} lem using ( injAt-out; module Extract )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
```

计数证明复合内部单射。可定义映射把具有唯一值的公式变成可构造图，最小见证选择为 Skolem 封闭提供这种映射，内部乘积则容纳带标签的对。

```agda
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
open import L.GCH.LeastWitnessMap {ℓ} lem using ( module Least )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( prodL; prodL-in; module Relation )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )
```

最小见证在同一个可构造层内选取。界定序数把参数收集于其中，超充分性使满足关系稳定，满足图则把这些选择记录为 `L` 中的集合。

```agda
open import L.Stage {ℓ} lem using ( LeastOrd; isPropLeastOrd; leastOrd; stage; stage-ord; stage-mem )
open import L.Ordinal using ( boundingOrd )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet; envSet-in )
open import L.GCH.AdequateStages {ℓ} lem using ( Superadequate )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )
```

Skolem 壳由起始集合反复施行最小见证封闭而得到。它的可构造呈现提供选择所需的层界，而凝聚把该壳认同为相应的可构造结构。

```agda
open import L.GCH.SkolemHull {ℓ} lem using ( module Frame; module HullStage )
open import L.GCH.ConstructibleHull {ℓ} lem using ( module Condense′; module Telescope )
open import L.GCH.StageCountingTools {ℓ} lem
  using ( isPropInjCode; injcode-resp; injFo; module InjFo; pinAt; pin-in; pin-out; seq-map; Lω
        ; limit-stage-counted )
```

每一步封闭都由公式码和有限参数序列索引。公式形状是可数的，无穷基数上的有限序列由平方律给出界，良基归纳则为计数中的内部基数提供这条平方律。

```agda
open import L.GCH.FiniteSequenceCoding {ℓ} lem using ( seqL; seqL-in; seq-count )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( prod-inj; ω⊆; Goal; module Step )
open import L.Cardinal {ℓ} lem using ( IsCardinalL )
open import V.Hierarchy {ℓ} using ( regularityV )
import Cubical.Induction.WellFounded as WF
```

当图的两个参数都由等式认同时，二元搬运可同时沿两条等式移动图的隶属证明。因此，等式替换与编码关系保持相容。

```agda
open import Cubical.Foundations.Prelude using ( subst2 )
```

标签 `0` 与 `1` 不同，因此带标签单射的两个分支互不相交。第二分量为命题的依值对之相等归结为第一分量相等，所以可构造性证明不影响计数。

```agda
open import Cubical.Data.Nat.Properties using ( znots; snotz )
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.HLevels using ( isProp×; isSetΣSndProp )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
```

von Neumann 数码提供标签，`ω` 收集这些数码，后继描述其有限递进。空集充当单点集单射的取值，而命题截断记录存在性却不选择代表。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; ω; sucV )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅ )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
```

编码单射的存在性经过命题截断，因为计数只依赖见证图是否存在。因此截断只消去到命题中，使结果不依赖所选的图。

```agda
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

对外围集合而言，`x ∈ˢ y` 是 `x` 属于 `y` 这一命题。编码函数的定义域和值域条件最终都归结为底层集合上的这一关系。

```agda
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
```

以 `S` 表示可构造模型的载体。其元素由外围集合及其属于 `L` 的证明组成；由于这些证明是命题，底层集合在相等意义下唯一确定可构造元素。

```agda
module SL = hPropStructure 𝒮ʟ using ( S )
open SL using ( S )
```

带可构造常元的公式可以在 `L` 内部求值，也可以投影到外围层级。传递性使两种读法一致，因此内部证明的图陈述可作为底层集合之间的普通隶属来使用。

```agda
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
```

`Holds F x y` 表示 `x` 与 `y` 的底层集合组成的有序对属于底层图 `F`。这就是论证中每个编码应用公式所表示的外围关系。

```agda
Holds : S → S → S → Type (ℓ-suc ℓ)
Holds F x y = ⟨ pr (fst x) (fst y) ∈ fst F ⟩
```

元素 `nn k : S` 由外围的 von Neumann 数码 `# k` 及其可构造性证明组成。特别地，`nn 0` 与 `nn 1` 充当内部标签而不离开 `L`。

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

若 `S` 的两个元素具有相等的底层集合，则这两个元素本身相等。第二分量只包含可构造性证明，故证明无关性把第一分量的等式提升为依值对的等式。

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

载体 `S` 是 h-集合。其第一分量位于本身为 h-集合的累积层级中，而每个可构造性证明纤维都是命题；因此 `S` 中的每个等式类型都是命题。

```agda
isSetS : isSet S
isSetS = isSetΣSndProp setIsSet (λ v → snd (isL v))
```

前两个变元槽的 De Bruijn 索引被命名，因为本章的编码公式一次至多涉及八个槽位。

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

名称 `i2`、`i3` 与 `i4` 分别表示第二、第三与第四变元位置。每个索引都是前一个索引的后继，多态的尾长 `k` 保证在还有更多可用变元时该位置仍然有效。

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

在补上 `i4` 的定义等式后，同样的后继模式定义第五与第六位置。这些名称使嵌套绑定造成的位移在编码公式的类型中清晰可见。

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

第七槽是最后一个；这八个索引覆盖本章用到的每个变元位置。

```agda
  i7 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc k))))))))
  i7 = suc i6
```

序数包含于其自身的层：序数的每个成员自身是序数，而累积构造把序数的每个成员放进该序数所索引的层。

```agda
ord⊆Lset : (α : V ℓ) → IsOrd α → (z : V ℓ) → ⟨ z ∈ α ⟩ → ⟨ z ∈ Lset α ⟩
ord⊆Lset α oα z z∈α =
  Lset-cumul z α oz oα z∈α (ord∈Lset-suc z oz)
  where
  oz : IsOrd z
```

由于 `z ∈ α` 且 `α` 是序数，`z` 本身也是序数。这使 `z` 属于其后继层；再沿 `z ∈ α` 使用累积性，便得到 `z ∈ Lset α`。

```agda
  oz = mem-ord {A = α} oα z z∈α
```

固定可构造集合 `D₁` 与 `D₂`。它们的内部二元并是合并两个单射时的共同定义域；其隶属原理给出两条包含和一个截断的情形拆分。

```agda
module Union2 (D₁ D₂ : S) where
```

该并即两个集合的内部并。

```agda
  D : S
  D = cupʟ D₁ D₂
```

左侧的成员由并的左规则包含进来。

```agda
  in₁ : (z : S) → ⟨ fst z ∈ fst D₁ ⟩ → ⟨ fst z ∈ fst D ⟩
  in₁ z = cupʟ-inl D₁ D₂ (fst z)
```

右侧的成员对称地包含进来。

```agda
  in₂ : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → ⟨ fst z ∈ fst D ⟩
  in₂ z = cupʟ-inr D₁ D₂ (fst z)
```

若 `z ∈ D₁ ∪ D₂`，则仅能断言它属于左侧或右侧。这个析取经过命题截断，因为隶属关系保留某个呈现索引指名 `z` 这一事实，却不保留具体索引。

```agda
  out : (z : S) → ⟨ fst z ∈ fst D ⟩ → ∥ ⟨ fst z ∈ fst D₁ ⟩ ⊎ ⟨ fst z ∈ fst D₂ ⟩ ∥₁
  out z = cupʟ-out D₁ D₂ (fst z)
```

令 `κ` 为包含标签 `0` 与 `1` 的可构造集合，并令 `E₁`、`E₂` 分别编码从 `D₁`、`D₂` 到 `κ` 的单射。给取值加标签，便把它们合成从 `D₁ ∪ D₂` 到 `κ × κ` 的单射。此构造不要求 `κ` 是序数。

```agda
module TagUnion (κ : S) (0∈κ : ⟨ # 0 ∈ fst κ ⟩) (1∈κ : ⟨ # 1 ∈ fst κ ⟩)
                (D₁ D₂ E₁ E₂ : S) (c₁ : InjCode E₁ D₁ κ) (c₂ : InjCode E₂ D₂ κ) where
```

记 `D = D₁ ∪ D₂`。任一分支的成员都属于 `D`，而 `D` 的每个成员都给出一条截断证明，说明它来自两个分支之一。

```agda
  open Union2 D₁ D₂ public using ( D; in₁; in₂; out )
```

每个编码单射都提取出其底层函数，连同「图恰好按编码所说成立」的证明。

```agda
  module X₁ = Extract E₁ D₁ (fst c₁) (fst (snd c₁)) using ( toFun; toFun-graph )
  module X₂ = Extract E₂ D₂ (fst c₂) (fst (snd c₂)) using ( toFun; toFun-graph )
```

`Mem z` 是 `z` 属于并定义域 `D` 这一命题。输入连同这条证明，恰好提供分段函数求值所需的定义域证据。

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem z = ⟨ fst z ∈ fst D ⟩
```

属于左定义域可由排中律判定，这一判定正是构造带标签单射所依赖的情形拆分。

```agda
  Case : S → Type (ℓ-suc ℓ)
  Case z = ⟨ fst z ∈ fst D₁ ⟩ ⊎ (⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥)
```

排中律对并的每个成员判定其是否来自左定义域。

```agda
  decide : (z : S) → Case z
  decide z = lem (fst z ∈ fst D₁)
```

不在左定义域的成员必在右定义域：并中的隶属拆成两侧，而左侧与所设的失败矛盾。

```agda
  off : (z : S) → Mem z → (⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥) → ⟨ fst z ∈ fst D₂ ⟩
  off z m no = PT.rec (snd (fst z ∈ fst D₂))
    (λ { (inl h) → Empty.rec (no h) ; (inr h) → h }) (out z m)
```

两侧的取值都是带标签的像：数码标签零或一与提取出的函数值配对，使两个单射落入不相交的带标签值域。

```agda
  val : (z : S) → Mem z → Case z → S
  val z m (inl h)  = prʟ (nn 0) (X₁.toFun (z , h))
  val z m (inr no) = prʟ (nn 1) (X₂.toFun (z , off z m no))
```

对 `z ∈ D`，函数 `fn` 判定 `z ∈ D₁` 是否成立。左侧情形返回 `(0,E₁(z))`，互补的右侧情形返回 `(1,E₂(z))`。

```agda
  fn : (z : S) → Mem z → S
  fn z m = val z m (decide z)
```

外围含义 `Wit y z` 分成两个分支。左分支要求 `z ∈ D₁`，并且仅仅存在满足 `(z,v) ∈ E₁` 的 `v`，使 `y` 的底层集合等于 `(0,v)`。

```agda
  Wit : (y z : S) → Type (ℓ-suc ℓ)
  Wit y z =
      (⟨ fst z ∈ fst D₁ ⟩
        × ∥ Σ[ v ∈ S ] (Holds E₁ z v × (fst y ≡ pr (# 0) (fst v))) ∥₁)
    ⊎ ((⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥)
```

右分支要求 `z ∉ D₁`，并且仅仅存在满足 `(z,v) ∈ E₂` 的 `v`，使底层集合意义下 `y = (1,v)`。两个不同标签排除了相异分支输出相等的可能。

```agda
        × ∥ Σ[ v ∈ S ] (Holds E₂ z v × (fst y ≡ pr (# 1) (fst v))) ∥₁)
```

图写作二空位公式：属于 `D₁` 与对第一个码的存在量化合取，或该隶属的否定与对第二个码的存在量化合取。存在量词之内，被单射的值与标签等式都是编码的原子。

```agda
  opaque
    fo : Formula S 2
    fo = ((var i1 ∈̇ con D₁) ∧̇ ∃̇ (appC E₁ i2 i0 ∧̇ tagAtL i1 0 i0))
       ∨̇ ((¬̇ (var i1 ∈̇ con D₁)) ∧̇ ∃̇ (appC E₂ i2 i0 ∧̇ tagAtL i1 1 i0))
```

读取两个编码原子使用其充分性引理：应用原子的满足变成隶属 `Holds E z v`，标记原子的满足变成 `y` 与带标签对的等式。

```agda
    private
      rd : (E : S) (k : ℕ) (y z v : S)
         → ⟨ (v ∷ y ∷ z ∷ []) ⊨ appC E i2 i0 ⟩ → ⟨ (v ∷ y ∷ z ∷ []) ⊨ tagAtL i1 k i0 ⟩
         → Holds E z v × (fst y ≡ pr (# k) (fst v))
      rd E k y z v ha ht =
```

沿两条充分性等价搬运后，满足见证恰好变成 `Wit` 所需的分量：图隶属 `Holds E z v`，以及把 `y` 认同为带标签 `k` 之对的等式。

```agda
          subst ⟨_⟩ (appC-adequate E i2 i0 (v ∷ y ∷ z ∷ [])) ha
        , subst ⟨_⟩ (tagAtL-adequate i1 k i0 (v ∷ y ∷ z ∷ [])) ht
```

反过来，由 `Holds E z v` 与底层等式 `y = (k,v)`，沿充分性反向搬运便得到应用原子的满足。

```agda
      wr : (E : S) (k : ℕ) (y z v : S)
         → Holds E z v → fst y ≡ pr (# k) (fst v)
         → ⟨ (v ∷ y ∷ z ∷ []) ⊨ appC E i2 i0 ⟩ × ⟨ (v ∷ y ∷ z ∷ []) ⊨ tagAtL i1 k i0 ⟩
      wr E k y z v ha ht =
          subst ⟨_⟩ (sym (appC-adequate E i2 i0 (v ∷ y ∷ z ∷ []))) ha
```

同样的反向搬运把带标签对的等式变成标签原子的满足。两条证明合在一起，便重建存在量词之下的合取。

```agda
        , subst ⟨_⟩ (sym (tagAtL-adequate i1 k i0 (v ∷ y ∷ z ∷ []))) ht
```

读取 `fo` 的满足证明时按两个析取支分类。左支给出 `z ∈ D₁` 和带零标签的截断 `E₁` 见证；右支给出 `z ∉ D₁` 和带一标签的相应 `E₂` 见证。在每个截断内部应用 `rd`，便得到 `Wit y z` 的截断元素。

```agda
    fo-out : (y z : S) → ⟨ (y ∷ z ∷ []) ⊨ fo ⟩ → ∥ Wit y z ∥₁
    fo-out y z = PT.map
      (λ { (inl (h , hv)) → inl (h , PT.map (λ { (v , (ha , ht)) → v , rd E₁ 0 y z v ha ht }) hv)
         ; (inr (h , hv)) → inr ((λ z∈ → lower (h z∈))
             , PT.map (λ { (v , (ha , ht)) → v , rd E₂ 1 y z v ha ht }) hv) })
```

图的向内读法逐情形把宿主侧见证转成满足。左支中，隶属与截断条目沿应用编码与标签编码的充分性等式运输；右支先把「不属于 `D₁`」的反驳提升为对象语言否定，再做同样处理。

```agda
    fo-in : (y z : S) → Wit y z → ⟨ (y ∷ z ∷ []) ⊨ fo ⟩
    fo-in y z (inl (h , hv)) =
      ∣ inl (h , PT.map (λ { (v , (ha , ht)) → v , wr E₁ 0 y z v ha ht }) hv) ∣₁
    fo-in y z (inr (h , hv)) =
      ∣ inr ((λ z∈ → lift (h z∈))
```

右支的末项完成第二个析取支：`E₂` 的条目按左支同样方式运输，只是标签由 `0` 换成 `1`。两个析取支随后被注入截断存在，引入完毕。

```agda
          , PT.map (λ { (v , (ha , ht)) → v , wr E₂ 1 y z v ha ht }) hv) ∣₁
```

每条被编码关系都是单值的：第一分量相同的两条目第二分量相同。这是注入码的第一个合取项，经应用编码的充分性读出。

```agda
  private
    sv₁ : (x y y' : S) → Holds E₁ x y → Holds E₁ x y' → fst y ≡ fst y'
    sv₁ = svAt-out zero (E₁ ∷ D₁ ∷ []) (fst c₁)
    sv₂ : (x y y' : S) → Holds E₂ x y → Holds E₂ x y' → fst y ≡ fst y'
    sv₂ = svAt-out zero (E₂ ∷ D₂ ∷ []) (fst c₂)
```

每条被编码关系还是单射的：第二分量相同的两条目，其第一分量的底层集合相等。范围子句开始列出：关系的每个取值都落在基数之中。

```agda
    ij₁ : (y x x' : S) → Holds E₁ x y → Holds E₁ x' y → fst x ≡ fst x'
    ij₁ = injAt-out zero (E₁ ∷ D₁ ∷ []) (fst (snd (snd c₁)))
    ij₂ : (y x x' : S) → Holds E₂ x y → Holds E₂ x' y → fst x ≡ fst x'
    ij₂ = injAt-out zero (E₂ ∷ D₂ ∷ []) (fst (snd (snd c₂)))
    ran₁ : (x y : S) → Holds E₁ x y → ⟨ fst y ∈ fst κ ⟩
```

第二条范围子句补全了从两份注入码读出的资料。对每条关系，我们现在都有单值性、单射性以及每个取值都属于 `κ`；构造带标签映射所用的正是这些性质。

```agda
    ran₁ = snd (snd (snd c₁))
    ran₂ : (x y : S) → Holds E₂ x y → ⟨ fst y ∈ fst κ ⟩
    ran₂ = snd (snd (snd c₂))
```

见证按成员的两种情形构造。若 `z ∈ D₁`，取值使用从 `E₁` 提取的函数；否则，先得到 `z ∈ D₂`，再使用从 `E₂` 提取的函数。两种情形中，提取过程都同时给出图条目，以及把带标签的对认同为所选取值的等式。

```agda
  wit : (z : S) (m : Mem z) (c : Case z) → Wit (val z m c) z
  wit z m (inl h)  = inl (h , ∣ X₁.toFun (z , h)
    , (X₁.toFun-graph (z , h) , prʟ-fst (nn 0) (X₁.toFun (z , h))) ∣₁)
  wit z m (inr no) = inr (no , ∣ X₂.toFun (z , off z m no)
    , (X₂.toFun-graph (z , off z m no) , prʟ-fst (nn 1) (X₂.toFun (z , off z m no))) ∣₁)
```

左支的唯一性复合三条等式：条目的第二分量等于截断见证所名指的取值；`E₁` 的单值性认同两个函数值；而对的第一投影等式说明该取值恰是带标签的条目。

```agda
  only : (z : S) (m : Mem z) (c : Case z) (y : S) → Wit y z → fst y ≡ fst (val z m c)
  only z m (inl h) y (inl (_ , hv)) = PT.rec (setIsSet _ _)
    (λ { (v , (hg , hy)) →
       hy ∙ cong (pr (# 0)) (sv₁ z v (X₁.toFun (z , h)) hg (X₁.toFun-graph (z , h)))
          ∙ sym (prʟ-fst (nn 0) (X₁.toFun (z , h))) }) hv
```

交叉情形被直接反驳：属于 `D₁` 的成员不可能带有在 `D₁` 之外记录的见证，反之亦然。随后右右情形完全按左支处理，只是换用 `E₂`、标签 `1` 与偏离集合的函数值。

```agda
  only z m (inl h) y (inr (no , _)) = Empty.rec (no h)
  only z m (inr no) y (inl (h , _)) = Empty.rec (no h)
  only z m (inr no) y (inr (_ , hv)) = PT.rec (setIsSet _ _)
    (λ { (v , (hg , hy)) →
       hy ∙ cong (pr (# 1)) (sv₂ z v (X₂.toFun (z , off z m no)) hg (X₂.toFun-graph (z , off z m no)))
```

最后一条等式复合标签认同与对的第一投影等式，唯一性就此完成。于是两种情形下见证都确定其取值。

```agda
          ∙ sym (prʟ-fst (nn 1) (X₂.toFun (z , off z m no))) }) hv
```

取值落入内部乘积：数码 `0` 或 `1` 与函数值组成的对经其第一投影等式呈现，而 `prodL-in` 予以接纳，因为两个数码都在 `κ` 中，且函数值由范围子句落在 `κ` 中。

```agda
  into : (z : S) (m : Mem z) (c : Case z) → ⟨ fst (val z m c) ∈ˢ fst (prodL κ) ⟩
  into z m (inl h) = subst (λ w → ⟨ w ∈ˢ fst (prodL κ) ⟩) (sym (prʟ-fst (nn 0) (X₁.toFun (z , h))))
    (prodL-in κ (nn 0) (X₁.toFun (z , h)) 0∈κ (ran₁ z (X₁.toFun (z , h)) (X₁.toFun-graph (z , h))))
  into z m (inr no) = subst (λ w → ⟨ w ∈ˢ fst (prodL κ) ⟩) (sym (prʟ-fst (nn 1) (X₂.toFun (z , off z m no))))
    (prodL-in κ (nn 1) (X₂.toFun (z , off z m no)) 1∈κ
```

右支由 `E₂` 与数码 `1` 供给范围事实，完成两个带标签取值在乘积中的成员资格。

```agda
      (ran₂ z (X₂.toFun (z , off z m no)) (X₂.toFun-graph (z , off z m no))))
```

这些材料定义出从普通并集 `D` 到内部乘积 `prodL κ` 的映射。取值由偏向左支的情形区分决定，`into` 则证明这个带标签的取值属于该乘积。

```agda
  Dmap : DefinableMap
  Dmap = record
    { dom = D ; cod = prodL κ ; fn = fn
    ; into = λ z m → into z m (decide z)
    ; graph = fo
```

定义子句把见证喂给图的引入，而唯一性把每条图条目转换为所选情形下的取值，并沿载体相等运输。可定义映射就此完成。

```agda
    ; defines = λ z m → fo-in (fn z m) z (wit z m (decide z))
    ; only = λ z m y h → S≡ (PT.rec (setIsSet _ _) (only z m (decide z) y) (fo-out y z h)) }
```

带标签映射的单射性通过比较两个输入所判定的情形来证明。情形分析有四种组合，而带标签的对结构把它们干净地分开。

```agda
  inj : (z : S) (m : Mem z) (z' : S) (m' : Mem z') → fst (fn z m) ≡ fst (fn z' m') → fst z ≡ fst z'
  inj z m z' m' = go (decide z) (decide z')
    where
    go : (c : Case z) (c' : Case z') → fst (val z m c) ≡ fst (val z' m' c') → fst z ≡ fst z'
    go (inl h) (inl h') q = ij₁ (X₁.toFun (z , h)) z z' (X₁.toFun-graph (z , h))
```

同标签情形中，对等式由 `pr-inj` 反演：标签一致，故取值的等式认同两个函数值，这正是单射性子句所要的论证。

```agda
      (subst (λ w → ⟨ pr (fst z') w ∈ fst E₁ ⟩) (sym (snd p)) (X₁.toFun-graph (z' , h')))
      where
      p : (# 0 ≡ # 0) × (fst (X₁.toFun (z , h)) ≡ fst (X₁.toFun (z' , h')))
      p = pr-inj (sym (prʟ-fst (nn 0) (X₁.toFun (z , h))) ∙ q ∙ prʟ-fst (nn 0) (X₁.toFun (z' , h')))
    go (inl h) (inr no') q = Empty.rec (znots (#-inj 0 1 (fst
```

标签不同的两种情形都不可能发生：两取值若相等，就会迫使数码 `0` 与数码 `1` 相等，两个方向分别由 `znots` 与 `snotz` 排除。两个输入都走右支时，则由 `E₂` 的单射性认同它们。

```agda
      (pr-inj (sym (prʟ-fst (nn 0) (X₁.toFun (z , h))) ∙ q ∙ prʟ-fst (nn 1) (X₂.toFun (z' , off z' m' no')))))))
    go (inr no) (inl h') q = Empty.rec (snotz (#-inj 1 0 (fst
      (pr-inj (sym (prʟ-fst (nn 1) (X₂.toFun (z , off z m no))) ∙ q ∙ prʟ-fst (nn 0) (X₁.toFun (z' , h')))))))
    go (inr no) (inr no') q = ij₂ (X₂.toFun (z , off z m no)) z z' (X₂.toFun-graph (z , off z m no))
      (subst (λ w → ⟨ pr (fst z') w ∈ fst E₂ ⟩) (sym (snd p)) (X₂.toFun-graph (z' , off z' m' no')))
```

右右情形的对等式拆分为标签一致与函数值一致，后者正是单射性所消耗者。

```agda
      where
      p : (# 1 ≡ # 1) × (fst (X₂.toFun (z , off z m no)) ≡ fst (X₂.toFun (z' , off z' m' no')))
      p = pr-inj (sym (prʟ-fst (nn 1) (X₂.toFun (z , off z m no))) ∙ q
                  ∙ prʟ-fst (nn 1) (X₂.toFun (z' , off z' m' no')))
```

所得的图是从普通并集 `D₁ ∪ D₂` 到 `prodL κ` 的编码单射。映射在取值中使用标签区分两支，并把同时属于两边的元素归入第一支。

```agda
  injL : InjL D (prodL κ)
  injL = Inj.injL Dmap inj
```

两个前提都只在命题截断下给出各自的注入图。把两层截断消去到命题 `InjL (D₁ ∪ D₂) (prodL κ)`，便可对任意一对见证图应用带标签构造，得到所需的仅仅存在的编码单射。

```agda
tag-union : (κ : S) → ⟨ # 0 ∈ fst κ ⟩ → ⟨ # 1 ∈ fst κ ⟩
          → (D₁ D₂ : S) → InjL D₁ κ → InjL D₂ κ
          → InjL (unionʟ (pairʟ D₁ D₂)) (prodL κ)
tag-union κ h0 h1 D₁ D₂ = PT.rec2 squash₁
  (λ { (E₁ , c₁) (E₂ , c₂) → TagUnion.injL κ h0 h1 D₁ D₂ E₁ E₂ c₁ c₂ })
```

最小前驱构造以一般形式陈述。它取序数 `γ`、关系 `G`、定义域 `D`，以及被层 `γ` 界住的前驱集 `P`，使得 `D` 的每个成员都「仅仅存在」某个 `P` 中的 `G` 前驱；任务在于典范地选取一个。

```agda
module LeastPre (γ : V ℓ) (oγ : IsOrd γ) (G D P : S)
  (inP : (p z : S) → Holds G p z → ⟨ fst p ∈ fst P ⟩)
  (P⊆L : (p : S) → ⟨ fst p ∈ fst P ⟩ → ⟨ fst p ∈ Lset γ ⟩)
  (have : (z : S) → ⟨ fst z ∈ fst D ⟩ → ∥ Σ[ p ∈ S ] Holds G p z ∥₁) where
```

定义域的隶属被记录为一个类型，使论证能把它与元素并肩携带。

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem z = ⟨ fst z ∈ fst D ⟩
```

图公式是常元 `G` 的应用子句：在一对上成立，恰是说该对属于这个关系。

```agda
  private
    graphFo : Formula S 2
    graphFo = appC G i0 i1
```

存在性假设被移到共同的层中，而没有全局选取前驱。每个截断地存在的前驱先属于 `P`，因而属于 `Lset γ`；充分性等式再把它的关系成员资格转成图公式的满足。

```agda
    have-γ : (z : S) → Mem z
           → ∥ Σ[ p ∈ S ] (⟨ fst p ∈ Lset γ ⟩ × ⟨ (p ∷ z ∷ []) ⊨ graphFo ⟩) ∥₁
    have-γ z m = PT.map
      (λ { (p , h) → p , P⊆L p (inP p z h)
                       , subst ⟨_⟩ (sym (appC-adequate G i0 i1 (p ∷ z ∷ []))) h })
```

原有的截断存在供给运输所要消耗的见证。

```agda
      (have z m)
```

层序构造现在为定义域的每个成员选取 `Lset γ` 中最小的 `G` 前驱。它还给出一个可定义图，以及把每个输入同其所选取值对应起来的成员读式。

```agda
    module Ls = Least γ oγ D graphFo have-γ using ( fn; fn-holds; Dmap; T; T-in; T-out )
```

选出的最小前驱就是该构造的取值函数。

```agda
  fn : (z : S) → Mem z → S
  fn = Ls.fn
```

取值在其输入处满足该关系：内部满足被运回「把取值与输入配成对的环境」处的应用子句。

```agda
  fn-holds : (z : S) (m : Mem z) → Holds G (fn z m) z
  fn-holds z m = subst ⟨_⟩ (appC-adequate G i0 i1 (fn z m ∷ z ∷ [])) (Ls.fn-holds z m)
```

可定义映射以 `P` 为陪域记录，取值的所属由既有假设的向内方向保证。

```agda
  Dmap : DefinableMap
  Dmap = record Ls.Dmap { cod = P ; into = λ z m → inP (fn z m) z (fn-holds z m) }
```

最小前驱函数的图是 `L` 的元素，层机制连同其隶属描述一并返回。

```agda
  T : S
  T = Ls.T
```

向内读式出示「输入与其选出的取值组成的对」是图的一条目。

```agda
  T-in : (z : S) (m : Mem z) → ⟨ pr (fst z) (fst (fn z m)) ∈ fst T ⟩
  T-in = Ls.T-in
```

向外读式从每条条目恢复输入，以及「第二分量等于选出的取值」的等式；后文比较候选者所用的正是它。

```agda
  T-out : (z e : S) → ⟨ pr (fst z) (fst e) ∈ fst T ⟩
        → Σ[ m ∈ Mem z ] (fst e ≡ fst (fn z m))
  T-out = Ls.T-out
```

在「该关系为函数性」这一附加假设下，最小前驱函数成为单射：该模块只携带这一条假设。

```agda
  module Functional
    (funct : (p z z' : S) → Holds G p z → Holds G p z' → fst z ≡ fst z') where
```

若两个输入共享取值，则该取值在两个输入处都满足关系；第二个满足沿取值的等式运输，函数性随即认同两个输入。

```agda
    inj : (z : S) (m : Mem z) (z' : S) (m' : Mem z')
        → fst (fn z m) ≡ fst (fn z' m') → fst z ≡ fst z'
    inj z m z' m' q = funct (fn z m) z z' (fn-holds z m)
      (subst (λ w → ⟨ pr w (fst z') ∈ fst G ⟩) (sym q) (fn-holds z' m'))
```

单射性被打包为从定义域到前驱集合的编码单射。

```agda
    injL : InjL D P
    injL = Inj.injL Dmap inj
```

点构造处理一个至多含一个元素的定义域。只需给定 `0 ∈ κ`，它便把由 `a` 生成的单点集的每个成员送到第零个数码，并得到一条到 `κ` 的编码单射。

```agda
module Point (κ : S) (0∈κ : ⟨ # 0 ∈ fst κ ⟩) (a : S) where
```

令 `Y` 为由 `a` 生成的可构造单点集。论证只使用它的成员引入律与消去律。

```agda
  Y : S
  Y = sglʟ a
```

成员 `a` 属于它自己的单点集，由单点构造的引入读式给出。

```agda
  Y-in : ⟨ fst a ∈ fst Y ⟩
  Y-in = sglʟ-in a (fst a) refl
```

消去读式说明单点集不含其他：任何成员的底层集合都是 `a`。

```agda
  Y-out : (z : S) → ⟨ fst z ∈ fst Y ⟩ → fst z ≡ fst a
  Y-out z = sglʟ-out a (fst z)
```

图由一条含两个自由槽位的原子公式描述；它把取值槽与内部空集相等，而内部空集的底层集合正是数码 `0`。

```agda
  fo : Formula S 2
  fo = var i0 ≐ con ∅ʟ
```

可定义映射把唯一的输入送到第零个数码；陪域隶属即既有事实 `0∈κ`。

```agda
  Dmap : DefinableMap
  Dmap = record
    { dom = Y ; cod = κ ; fn = λ _ _ → nn 0
    ; into = λ _ _ → 0∈κ
    ; graph = fo
```

图由定义成立，因为原子句把数码与其自身等同；唯一性成立，因为单点集的两个成员呈现同一底层集合。

```agda
    ; defines = λ z m → refl
    ; only = λ z m y h → S≡ h }
```

单射性复合两条向外读式：两个输入都呈现与 `a` 相同的底层集合，故作为载体元素二者相等。

```agda
  inj : (z : S) (m : ⟨ fst z ∈ fst Y ⟩) (z' : S) (m' : ⟨ fst z' ∈ fst Y ⟩)
      → fst (nn 0) ≡ fst (nn 0) → fst z ≡ fst z'
  inj z m z' m' _ = Y-out z m ∙ sym (Y-out z' m')
```

单点集到基数的单射与其他计数组件以同一形式打包。

```agda
  injL : InjL Y κ
  injL = Inj.injL Dmap inj
```

## 计数每一步有限闭包

计数定理固定一个对后继封闭的序数 `lam`、一个包含于 `Lset lam` 的起点集合 `X`，以及 `X` 可构造的证明。初等性与超充分性假设为从 `X` 生成的 Skolem 壳提供闭包和最小见证性质。

```agda
module Count (lam : V ℓ) (ordλ : IsOrd lam)
  (succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : V ℓ) (X⊆L : (x : V ℓ) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
  (elem : Frame.A.Elementary lam ordλ succλ X X⊆L ∅∈λ)
```

计数目标是一个不在 `ω` 中的内部基数 `κ`，连同起点到它的编码单射。任务是以同一基数计数整个壳。

```agda
  (sup : Superadequate lam)
  (X-isL : ⟨ isL X ⟩)
  (κ : S) (oκ : IsOrd (fst κ)) (cκ : IsCardinalL κ) (κ∉ω : ⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
  (base : InjL (X , X-isL) κ) where
```

该壳表示为各有限迭代 `hullStep n` 的并。一次闭包步由 `Φ` 控制；它的非平凡分支记录某个公式键与当前迭代上的有限参数环境所确定的最小见证。

```agda
  module Cn = Condense′ lam ordλ succλ X X⊆L ∅∈λ elem sup X-isL
    using ( hullStep; hullL; hullStep⊆Hull )
  module B = Telescope.Build lam ordλ succλ X X⊆L ∅∈λ
    using ( A; Body
          ; LeastWitness; leastWitnessFo; leastWitness-in; leastWitness-out
```

对一个最小见证，随附的数据恢复出一个自然数长度、一个到当前集合的有限赋值、相应的编码环境，以及公式键属于 `Lset ω` 的证明。唯一性是在公式键与环境固定之后成立的。

```agda
          ; LeastWitnessData; leastWitness-data; leastWitness-unique; witFo-leastWitness
          ; Φ; Φ-out; λ-isL; ω-num; pack )
  module SM = SatGraph B.A using ( pairs; pairs-out; valOf )
```

有限迭代带有成员引入律与消去律，并且每个迭代都包含于整个壳。整个壳又包含于 `Lset lam`；这些包含关系保证计数构造所用的集合始终位于固定的外围层中。

```agda
  module It = Telescope.HullIter.It lam ordλ succλ X X⊆L ∅∈λ X-isL B.pack
    using ( Num; iter; iter-in; iter-out; iterUnion-out; ω-num )
  module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ using ( Hull⊆L )
  open Cn using ( hullStep; hullL )
```

因为 `κ` 是序数且不属于 `ω`，所以它包含每个有限数码。这个结论不使用内部基数性；内部基数性另用于平方律。

```agda
  num∈κ : (k : ℕ) → ⟨ # k ∈ fst κ ⟩
  num∈κ k = ω⊆ (fst κ) oκ κ∉ω (# k) (#∈ω k)
```

无穷基数平方论证给出编码单射 `pairκ : InjL (prodL κ) κ`。它使用关于 `κ` 的三项相关假设：序数性、内部基数性以及不属于 `ω`；所得结论是单射，而非双射。

```agda
  pairκ : InjL (prodL κ) κ
  pairκ = WF.WFI.induction regularityV {P = Goal} Step.result (fst κ) (snd κ) oκ cκ κ∉ω
```

层 `Lω = Lset ω` 通过复合单射入 `κ`。极限层计数先给出 `Lω ↪ ωʟ`，再由 `κ` 的序数性与非有限性得到 `ω ⊆ κ`，从而有 `ωʟ ↪ κ`。

```agda
  Lω↪κ : InjL Lω κ
  Lω↪κ = injl-trans Lω ωʟ κ limit-stage-counted
    (inclusion-coded ωʟ κ (λ z hz → ω⊆ (fst κ) oκ κ∉ω z hz))
```

为计数一次闭包步，固定一个包含于 `Lset lam` 的可构造集合 `Z`，以及一个满足 `InjCode E Z κ` 的实际图 `E`。目标是从这条已选定的层注入构造出仅仅存在的编码单射 `InjL (Φ Z) κ`。

```agda
  module OneStep (Z : S) (Z⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
                 (E : S) (cE : InjCode E Z κ) where
```

`ΦZ = Φ Z` 是一次闭包步。其成员描述有三个分支：`Z` 的旧成员、空集后备项，或由公式键与 `Z` 上的有限参数环境确定的最小见证。

```agda
    ΦZ : S
    ΦZ = B.Φ Z
```

先分离出新的部分：`D₂` 收集 `ΦZ` 中不属于 `Z` 的成员。`L` 内部的分离保证新部分可构造。

```agda
    opaque
      D₂ : S
      D₂ = hasSeparationL ΦZ (¬̇ (var i0 ∈̇ con Z)) .fst .fst
```

其隶属规格恰说出分离所计算的内容：属于 `D₂`，就是属于 `ΦZ` 并且不属于 `Z`。

```agda
      D₂-spec : (z : S) → (fst z ∈ fst D₂)
              ≡ ((fst z ∈ fst ΦZ) ⊓ ((z ∷ []) ⊨ ¬̇ (var i0 ∈̇ con Z)))
      D₂-spec z = hasSeparationL ΦZ (¬̇ (var i0 ∈̇ con Z)) .fst .snd z
```

引入规则把隶属的反驳提升到对象层，于是 `ΦZ` 的元素连同「它不属于 `Z`」的证明即可进入 `D₂`。

```agda
    opaque
      D₂-in : (z : S) → ⟨ fst z ∈ fst ΦZ ⟩ → (⟨ fst z ∈ fst Z ⟩ → Empty.⊥) → ⟨ fst z ∈ fst D₂ ⟩
      D₂-in z h no = subst ⟨_⟩ (sym (D₂-spec z)) (h , λ z∈ → lift (no z∈))
```

消去规则经该规格拆开 `D₂` 的隶属，并把对象层的反驳降回普通的蕴涵。

```agda
      D₂-out : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → ⟨ fst z ∈ fst ΦZ ⟩ × (⟨ fst z ∈ fst Z ⟩ → Empty.⊥)
      D₂-out z h = r .fst , λ z∈ → lower (r .snd z∈)
        where
        r : ⟨ fst z ∈ fst ΦZ ⟩
          × ⟨ (z ∷ []) ⊨ ¬̇ (var i0 ∈̇ con Z) ⟩
```

展开后的陈述是一个对：属于 `ΦZ`，并且满足那条否定原子。

```agda
        r = subst ⟨_⟩ (D₂-spec z) h
```

在新的部分内部，等于空集的元素被分离为 `D∅`。

```agda
    opaque
      D∅ : S
      D∅ = hasSeparationL D₂ (var i0 ≐ con ∅ʟ) .fst .fst
```

其规格是同样的双重模式：属于 `D₂`，并且与空集相等。

```agda
      D∅-spec : (z : S) → (fst z ∈ fst D∅)
              ≡ ((fst z ∈ fst D₂) ⊓ ((z ∷ []) ⊨ var i0 ≐ con ∅ʟ))
      D∅-spec z = hasSeparationL D₂ (var i0 ≐ con ∅ʟ) .fst .snd z
```

`D₂` 中等于空集的元素，连同两条数据即可进入 `D∅`。

```agda
    opaque
      D∅-in : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → fst z ≡ ∅ → ⟨ fst z ∈ fst D∅ ⟩
      D∅-in z h e = subst ⟨_⟩ (sym (D∅-spec z)) (h , e)
```

其消去就是直接读出的规格：属于 `D₂`，以及与空集的等式。

```agda
      D∅-out : (z : S) → ⟨ fst z ∈ fst D∅ ⟩ → ⟨ fst z ∈ fst D₂ ⟩ × (fst z ≡ ∅)
      D∅-out z h = subst ⟨_⟩ (D∅-spec z) h
```

剩余部分 `Dw` 收集 `D₂` 中不等于空集的元素。

```agda
    opaque
      Dw : S
      Dw = hasSeparationL D₂ (¬̇ (var i0 ≐ con ∅ʟ)) .fst .fst
```

其规格与前一条镜像，只是把等式换成了否定等式。

```agda
      Dw-spec : (z : S) → (fst z ∈ fst Dw)
              ≡ ((fst z ∈ fst D₂) ⊓ ((z ∷ []) ⊨ ¬̇ (var i0 ≐ con ∅ʟ)))
      Dw-spec z = hasSeparationL D₂ (¬̇ (var i0 ≐ con ∅ʟ)) .fst .snd z
```

引入要求属于 `D₂`，并要求对「与空集相等」的反驳。

```agda
    opaque
      Dw-in : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → (fst z ≡ ∅ → Empty.⊥) → ⟨ fst z ∈ fst Dw ⟩
      Dw-in z h ne = subst ⟨_⟩ (sym (Dw-spec z)) (h , λ q → lift (ne q))
```

消去返回 `D₂` 的隶属与那条反驳，后者已从对象层降下。

```agda
      Dw-out : (z : S) → ⟨ fst z ∈ fst Dw ⟩ → ⟨ fst z ∈ fst D₂ ⟩ × (fst z ≡ ∅ → Empty.⊥)
      Dw-out z h = r .fst , λ q → lower (r .snd q)
        where
        r : ⟨ fst z ∈ fst D₂ ⟩
          × ⟨ (z ∷ []) ⊨ ¬̇ (var i0 ≐ con ∅ʟ) ⟩
```

两个并集给出后续所需的界。`U₁` 包含 `Z` 与真正新增的部分 `D₂`，`U₃` 包含空集部分 `D∅` 与非空见证部分 `Dw`。接下来的引理证明到这两个并集的所需包含关系。

```agda
        r = subst ⟨_⟩ (Dw-spec z) h
    module U₁ = Union2 Z D₂ using ( D; in₁; in₂ )
    module U₃ = Union2 D∅ Dw using ( D; in₁; in₂ )
```

闭包步骤被第一个并覆盖。`ΦZ` 的每个成员 `z` 要么属于 `Z` 要么不属于，由排中律判定；两种情形下 `z` 都可构造，因为 `ΦZ` 可构造。

```agda
    ΦZ⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst ΦZ ⟩ → ⟨ z ∈ˢ fst U₁.D ⟩
    ΦZ⊆ z h = go (lem (z ∈ fst Z))
      where
      zS : S
      zS = z , isL-trans {x = fst ΦZ} {y = z} h (snd ΦZ)
```

两种情形分别经并集的两条包含映入 `U₁`。已经属于 `Z` 的成员使用第一条包含；否则先由 `D₂-in` 证明它属于新增部分，再使用第二条包含。

```agda
      go : ⟨ z ∈ fst Z ⟩ ⊎ (⟨ z ∈ fst Z ⟩ → Empty.⊥) → ⟨ z ∈ fst U₁.D ⟩
      go (inl hz) = U₁.in₁ zS hz
      go (inr no) = U₁.in₂ zS (D₂-in zS h no)
```

新部分被第二个并覆盖，同样是对「与空集相等」这条等式使用排中律。

```agda
    D₂⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst D₂ ⟩ → ⟨ z ∈ˢ fst U₃.D ⟩
    D₂⊆ z h = go (lem ((z ≡ ∅) , setIsSet z ∅))
      where
      zS : S
      zS = z , isL-trans {x = fst D₂} {y = z} h (snd D₂)
```

等于空集的元素经 `D∅` 进入；与之不同的元素经 `Dw` 进入。

```agda
      go : (z ≡ ∅) ⊎ (z ≡ ∅ → Empty.⊥) → ⟨ z ∈ fst U₃.D ⟩
      go (inl e)  = U₃.in₁ zS (D∅-in zS h e)
      go (inr ne) = U₃.in₂ zS (Dw-in zS h ne)
```

`D∅` 的每个成员都等于 `∅`，但 `D∅` 本身可能为空。由于数码 `0` 属于 `κ`，包含编码因而在 `L` 内给出 `D∅ ↪ κ`。

```agda
    D∅↪κ : InjL D∅ κ
    D∅↪κ = inclusion-coded D∅ κ
      (λ z hz → subst (λ w → ⟨ w ∈ fst κ ⟩)
        (sym (D∅-out (z , isL-trans {x = fst D∅} {y = z} hz (snd D∅)) hz .snd)) (num∈κ 0))
```

第二个并为见证的编码做准备：`U₂` 连接「诞生于层 `ω` 的元素」与「`Z` 成员的有穷序列」。

```agda
    module U₂ = Union2 Lω (seqL Z) using ( D; in₁; in₂ )
```

令 `PB` 为 `U₂ = Lω ∪ seqL Z` 的平方。每个实际见证码 `(s,e)`，其中 `s ∈ Lω` 且 `e ∈ seqL Z`，都属于 `PB`；`PB` 是一个齐次上界，也包含并非有效见证码的对。

```agda
    PB : S
    PB = prodL U₂.D
```

最小见证公式在固定基 `Z` 处被钉定。所得的五变元公式 `pin₅` 在框架 `(e,s,z,p,q)` 上成立，恰当且仅当 `z` 是由环境 `e` 与键 `s` 确定的最小见证；最后两个槽位由外围框架携带。

```agda
    opaque
      pin₅ : Formula S 5
      pin₅ = pinAt Z B.leastWitnessFo
```

向内：以参数环境 `e` 与键 `s` 给出的 `z` 的最小见证，产生钉定公式在五槽位语境处的满足。

```agda
      pin₅-in : (e s z p q : S) → B.LeastWitness Z e s z
              → ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩
      pin₅-in e s z p q h =
        pin-in Z B.leastWitnessFo (e ∷ s ∷ z ∷ p ∷ q ∷ [])
          (B.leastWitness-in Z e s z p q h)
```

向外：钉定公式的满足可拆包为最小见证，钉定的逆操作由钉定引理完成。

```agda
      pin₅-out : (e s z p q : S) → ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩
               → B.LeastWitness Z e s z
      pin₅-out e s z p q h =
        B.leastWitness-out Z e s z p q
          (pin-out Z B.leastWitnessFo (e ∷ s ∷ z ∷ p ∷ q ∷ []) h)
```

待计数的关系经过命题截断。`GW p z` 仅仅断言存在一个键 `s` 与一个环境 `e`，使 `p = (s,e)`，且 `z` 是由二者确定的最小见证。

```agda
    GW : (p z : S) → Type (ℓ-suc ℓ)
    GW p z = ∥ Σ[ s ∈ S ] Σ[ e ∈ S ]
               ((fst p ≡ pr (fst s) (fst e)) × B.LeastWitness Z e s z) ∥₁
```

同一关系也写成公式：两个存在量词绑定键与环境，配对原子确定 `p`，钉定公式承载见证条件。

```agda
    opaque
      se₃ : Formula S 3
      se₃ = ∃̇ (∃̇ (prAtL i3 i1 i0 ∧̇ pin₅))
```

向内：给定对等式与最小见证，填入两个见证，并把配对原子沿其充分性传输进对象语言。

```agda
      se₃-in : (z p q s e : S) → fst p ≡ pr (fst s) (fst e)
             → B.LeastWitness Z e s z → ⟨ (z ∷ p ∷ q ∷ []) ⊨ se₃ ⟩
      se₃-in z p q s e qp h =
        ∣ s , ∣ e , ( subst ⟨_⟩ (sym (prAtL-adequate i3 i1 i0 (e ∷ s ∷ z ∷ p ∷ q ∷ []))) qp
                    , pin₅-in e s z p q h ) ∣₁ ∣₁
```

向外时逐个消耗两个存在量词；第一步剥去外层量词，保留条目 `s` 与截断的剩余部分。

```agda
      se₃-out : (z p q : S) → ⟨ (z ∷ p ∷ q ∷ []) ⊨ se₃ ⟩ → GW p z
      se₃-out z p q = PT.rec squash₁ at₁
        where
        at₂ : (s : S) → Σ[ e ∈ S ] ( ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ prAtL i3 i1 i0 ⟩
                                   × ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩ ) → GW p z
```

打开第二个存在量词后，配对原子的充分性恢复出 `p = (s,e)`，钉定公式的向外读式则恢复最小见证条件。随后把这些见证重新置于定义 `GW` 的命题截断之下。

```agda
        at₂ s (e , (qp , h)) = ∣ s , e
          , ( subst ⟨_⟩ (prAtL-adequate i3 i1 i0 (e ∷ s ∷ z ∷ p ∷ q ∷ [])) qp
            , pin₅-out e s z p q h ) ∣₁
        at₁ : Σ[ s ∈ S ] ∥ Σ[ e ∈ S ] ( ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ prAtL i3 i1 i0 ⟩
                                      × ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩ ) ∥₁ → GW p z
```

由于 `GW p z` 是命题，剩余的外层截断可以消去到其中。`se₃-in` 与 `se₃-out` 合起来给出宿主关系 `GW` 与其对象语言公式的满足之间的两个方向。

```agda
        at₁ (s , h) = PT.rec squash₁ (at₂ s) h
```

有界分离在 `L` 内构造关系 `G`；它的条目是有序对 `(p,z)`，其中 `p ∈ PB`、`z ∈ Dw` 且 `GW p z`。因此，`G` 把最小见证关系限制在选定的码池与非空新增部分之间。

```agda
    private
      module WitnessGraph = Relation PB Dw ((var i1 ∈̇ con PB) ∧̇ se₃)
        (λ p z → (fst p ∈ fst PB) ⊓ (GW p z , squash₁))
        (λ p z q h → h .fst , se₃-out z p q (h .snd))
        (λ p z q h → h .fst , PT.rec (snd ((z ∷ p ∷ q ∷ []) ⊨ se₃))
```

描述条件的外向读法就是公式自身的外向读法，它返回的恰是 `GW` 的数据。

```agda
          (λ { (s , e , qp , hw) → se₃-in z p q s e qp hw }) (h .snd))
```

`G` 是所得的可构造关系，表示为有序对 `(p,z)` 的集合。当 `PB` 中的候选码携带某个 `Dw` 元素的最小见证数据时，`G` 便把二者关联起来。

```agda
    G : S
    G = WitnessGraph.rel
```

向内：`PB` 中的码 `p` 若经由某个键与环境同 `z` 一起指名一个最小见证，则属于 `G`。

```agda
    G-in : (p z : S) → ⟨ fst p ∈ fst PB ⟩ → ⟨ fst z ∈ fst Dw ⟩
         → (s e : S) → fst p ≡ pr (fst s) (fst e)
         → B.LeastWitness Z e s z → Holds G p z
    G-in p z hp hz s e qp h =
      WitnessGraph.into p z hp hz (hp , ∣ s , e , qp , h ∣₁)
```

反过来，`Holds G p z` 同时给出 `p ∈ PB` 与经过命题截断的见证数据 `GW p z`。它不会在该截断之外选出键与环境。

```agda
    G-out : (p z : S) → Holds G p z → ⟨ fst p ∈ fst PB ⟩ × GW p z
    G-out = WitnessGraph.pair-out
```

该关系只在截断意义下对 `Dw` 整体：每个 `z ∈ Dw` 都仅仅存在某个满足 `Holds G p z` 的 `p`。向外读取 `z ∈ ΦZ` 会给出它进入闭包步的三种可能原因。

```agda
    have : (z : S) → ⟨ fst z ∈ fst Dw ⟩ → ∥ Σ[ p ∈ S ] Holds G p z ∥₁
    have z hz = PT.rec squash₁ body (B.Φ-out Z z (D₂-out z (Dw-out z hz .fst) .fst))
      where
      body : B.Body Z z → ∥ Σ[ p ∈ S ] Holds G p z ∥₁
      body (inl h) = Empty.rec (D₂-out z (Dw-out z hz .fst) .snd h)
```

其中两种已被分离器排除：`z` 不能是 `Z` 的旧成员，也不能是空集。剩下的就是见证情形，经见证公式的外向引理读取。

```agda
      body (inr (inl e)) = Empty.rec (Dw-out z hz .snd e)
      body (inr (inr hw)) = PT.rec squash₁ read (B.witFo-leastWitness z Z hw)
        where
        read : Σ[ e ∈ S ] Σ[ s ∈ S ] B.LeastWitness Z e s z
             → ∥ Σ[ p ∈ S ] Holds G p z ∥₁
```

见证分支给出环境 `e`、键 `s` 与一个最小见证。其数据引理随后给出自然数长度 `n`、元层赋值 `g : Fin n → ⟪Z⟫`、把 `e` 认同为 `g` 的编码环境的等式，以及成员资格 `s ∈ Lset ω`。

```agda
        read (e , s , hw') = PT.map at (B.leastWitness-data Z e s z hw')
          where
          at : B.LeastWitnessData Z e s → Σ[ p ∈ S ] Holds G p z
          at (n , g , qe , hs) = prʟ s e
            , G-in (prʟ s e) z
```

码 `p` 是键与环境组成的内部对。它属于 `PB` 的证明逐条目建立：键因落在 `Lset ω` 而经 `Lω` 进入，环境因为是「到 `Z` 的长度 `n` 赋值」的环境而经 `Z` 的有限序列进入。随后该关系接受这个对。

```agda
                (subst (λ w → ⟨ w ∈ fst PB ⟩) (sym (prʟ-fst s e))
                  (prodL-in U₂.D s e (U₂.in₁ s hs)
                    (U₂.in₂ e (seqL-in Z n e
                      (subst (λ w → ⟨ w ∈ˢ fst (envSet Z n) ⟩) (sym qe) (envSet-in Z g))))))
                hz s e (prʟ-fst s e) hw'
```

## 见证键的唯一性

所需的函数性具有计数论证所需的反向取向：若同一个固定码 `p` 同时关联 `z` 与 `z'`，则 `z` 与 `z'` 的底层集合相等。同一个元素仍可拥有不同的码。

```agda
    funct : (p z z' : S) → Holds G p z → Holds G p z' → fst z ≡ fst z'
    funct p z z' h h' = PT.rec2 (setIsSet (fst z) (fst z')) read (G-out p z h .snd) (G-out p z' h' .snd)
      where
      read : Σ[ s ∈ S ] Σ[ e ∈ S ]
               ((fst p ≡ pr (fst s) (fst e)) × B.LeastWitness Z e s z)
```

两条关系都向外读出，各自返回一个键、一个环境、一条对等式与一个最小见证。

```agda
           → Σ[ s₂ ∈ S ] Σ[ e₂ ∈ S ]
               ((fst p ≡ pr (fst s₂) (fst e₂)) × B.LeastWitness Z e₂ s₂ z')
           → fst z ≡ fst z'
      read (s , e , q , hw) (s₂ , e₂ , q₂ , hw₂) =
        B.leastWitness-unique Z e s z z' hw hw₂'
```

两次读取把同一个固定的 `p` 分别表示为 `(s,e)` 与 `(s₂,e₂)`。有序对编码的单射性在底层集合层面认同两个键与两个环境，证明无关性再把这些等式提升为相应 `S` 元素的等式。

```agda
        where
        ee : (fst s₂ ≡ fst s) × (fst e₂ ≡ fst e)
        ee = pr-inj (sym q₂ ∙ q)
        hw₂' : B.LeastWitness Z e s z'
        hw₂' = subst2 (λ e' s' → B.LeastWitness Z e' s' z')
```

沿这些等同运输第二份最小见证证明后，两份证明便针对同一个键与环境。最小见证唯一性于是给出 `fst z ≡ fst z'`。

```agda
          (S≡ {x = e₂} {y = e} (snd ee)) (S≡ {x = s₂} {y = s} (fst ee)) hw₂
```

码池有自己的诞生层：`γG` 是 `PB` 在层级中出现的那个层。

```agda
    γG : V ℓ
    γG = stage (fst PB) (snd PB)
```

该层由一个序数索引，这正是计数引理对它的要求。

```agda
    oγG : IsOrd γG
    oγG = stage-ord (fst PB) (snd PB)
```

池包含于其诞生层，由层的传递性得出：诞生于 `γG` 的集合的成员属于 `Lset γG`。

```agda
    PB⊆Lγ : (p : S) → ⟨ fst p ∈ fst PB ⟩ → ⟨ fst p ∈ Lset γG ⟩
    PB⊆Lγ p hp = layer-trans (Lset-layer γG) {x = fst PB} {y = fst p} hp (stage-mem (fst PB) (snd PB))
```

这些假设现在实例化 `LeastPre`：每个 `z ∈ Dw` 都仅仅存在某个与之关联的 `PB` 中的码，而固定一个码至多确定一个这样的 `z`。最小选择为每个元素选取一个码，并给出 `InjL Dw PB`。它不声称见证码原本就唯一，而且这里得到的只是非空新增部分的计数，尚非完整的单步结论。

```agda
    module LP = LeastPre γG oγG G Dw PB (λ p z h → G-out p z h .fst) PB⊆Lγ have
      using ( module Functional )
```

最小原像构造把真正新的见证单射入 `PB`。每个 `z ∈ Dw` 仅仅具有某个相关码，而层序选出其中最小者。选取之前码无须唯一；单射性来自一个固定码至多表示一个见证。

```agda
    Dw↪PB : InjL Dw PB
    Dw↪PB = LP.Functional.injL funct
```

单射 `Z ↪ κ` 逐坐标作用于有限序列，得到 `seqL Z ↪ seqL κ`。再与有限序列计数复合，便得到 `seqL Z ↪ κ`；后一个映射只要求 `κ` 是无穷序数，并不要求它是内部基数。

```agda
    seq↪κ : InjL (seqL Z) κ
    seq↪κ = injl-trans (seqL Z) (seqL κ) κ (seq-map Z κ E cE) (seq-count κ oκ κ∉ω)
```

先计数 `U₂.D = Lω ∪ seqL Z`：给两个分支加标签得到到 `κ × κ` 的单射，再由 `pairκ` 把该乘积折入 `κ`。由于 `PB = U₂.D × U₂.D`，`prod-inj` 把这个单射提升为 `PB ↪ κ × κ`；第二次使用 `pairκ` 才得到 `PB ↪ κ`。两次折叠都使用平方律，因而都依赖内部基数性。

```agda
    PB↪κ : InjL PB κ
    PB↪κ = injl-trans PB (prodL κ) κ
      (prod-inj U₂.D κ
        (injl-trans U₂.D (prodL κ) κ (tag-union κ (num∈κ 0) (num∈κ 1) Lω (seqL Z) Lω↪κ seq↪κ) pairκ))
      pairκ
```

复合这两个单射即得真正新见证的计数：每个这样的见证都被某个 `p ∈ PB` 编码，而 `PB` 单射入 `κ`，故 `Dw` 单射入 `κ`。

```agda
    Dw↪κ : InjL Dw κ
    Dw↪κ = injl-trans Dw PB κ Dw↪PB PB↪κ
```

新部分 `D₂` 包含于 `D∅ ∪ Dw`。其中 `D∅` 恰含等于空集的新成员，并且自身可能为空；`Dw` 则含非空的见证成员。两部分的计数加标签后进入 `κ × κ`，再由 `pairκ` 折叠，得到 `D₂ ↪ κ`。

```agda
    D₂↪κ : InjL D₂ κ
    D₂↪κ = injl-trans D₂ U₃.D κ (inclusion-coded D₂ U₃.D D₂⊆)
      (injl-trans U₃.D (prodL κ) κ (tag-union κ (num∈κ 0) (num∈κ 1) D∅ Dw D∅↪κ Dw↪κ) pairκ)
```

`ΦZ` 的每个成员都属于 `Z ∪ D₂`。给定图 `E` 计数 `Z`，前面的构造计数 `D₂`；给两条单射加标签可得到到 `κ × κ` 的映射，再由 `pairκ` 完成单射 `ΦZ ↪ κ`。

```agda
    result : InjL ΦZ κ
    result = injl-trans ΦZ U₁.D κ (inclusion-coded ΦZ U₁.D ΦZ⊆)
      (injl-trans U₁.D (prodL κ) κ (tag-union κ (num∈κ 0) (num∈κ 1) Z D₂ ∣ E , cE ∣₁ D₂↪κ) pairκ)
```

`step-count` 把 `Z ↪ κ` 的截断见证消去到命题 `ΦZ ↪ κ` 中。因此它证明的是由 `κ` 给出的基数界，并非可数性；它也不选择见证输出单射的图。

```agda
  step-count : (Z : S) → ((z : V ℓ) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
             → InjL Z κ → InjL (B.Φ Z) κ
  step-count Z Z⊆ = PT.rec squash₁ (λ { (E , cE) → OneStep.result Z Z⊆ E cE })
```

每个有限闭包迭代的成员都位于外围层 `Lset lam` 中：这由诸迭代包含于壳、而壳的成员都在该层中得出。

```agda
  iter⊆L : (n : ℕ) (z : V ℓ) → ⟨ z ∈ˢ fst (hullStep n) ⟩ → ⟨ z ∈ˢ Lset lam ⟩
  iter⊆L n z hz = HSH.Hull⊆L z (Cn.hullStep⊆Hull n z hz)
```

自然数归纳为每个有限迭代分别给出一条内部单射。基础情形使用起始集合的已知单射，后继情形应用 `step-count`。这些见证仍经过命题截断，因而不能直接同时选出并用来计数其并。

```agda
  counted : (n : ℕ) → InjL (hullStep n) κ
  counted zero    = base
  counted (suc n) = step-count (hullStep n) (iter⊆L n) (counted n)
```

`HoldsAt n σ` 是经过命题截断的断言：某个可构造图 `F ∈ Lset σ` 编码单射 `hullStep n ↪ κ`。它同时记录容纳该码的层以及该码所计数的准确迭代。

```agda
  HoldsAt : ℕ → V ℓ → hProp (ℓ-suc ℓ)
  HoldsAt n σ = ∥ Σ[ F ∈ S ] (⟨ fst F ∈ Lset σ ⟩ × InjCode F (hullStep n) κ) ∥₁ , squash₁
```

对每个 `n`，令 `ls n` 为满足 `HoldsAt n` 的最小序数层。`counted n` 给出的截断单射提供存在性，而所得最小性陈述是命题，所以可以进行最小序数选择。

```agda
  opaque
    ls : (n : ℕ) → LeastOrd (HoldsAt n)
    ls n = PT.rec (isPropLeastOrd (HoldsAt n)) from (counted n)
      where
      from : Σ[ F ∈ S ] InjCode F (hullStep n) κ → LeastOrd (HoldsAt n)
```

给定编码 `hullStep n ↪ κ` 的图 `F`，容纳 `F` 的典范层是序数，并见证该处的 `HoldsAt n`。因此候选层类有元素，`leastOrd` 返回其中最小者。

```agda
      from (F , code) = leastOrd (HoldsAt n)
        ∣ stage (fst F) (snd F) , stage-ord (fst F) (snd F)
        , ∣ F , stage-mem (fst F) (snd F) , code ∣₁ ∣₁
```

由元层自然数索引的最小层族 `n ↦ ls n` 具有一个共同的序数界 `γ`。界定定理把每个 `ls n` 严格放在这个公共序数之下。

```agda
  opaque
    γ : V ℓ
    γ = boundingOrd (Lift {ℓ-zero} {ℓ} ℕ) (λ n → ls (lower n) .fst) (λ n → ls (lower n) .snd .fst) .fst
```

公共界 `γ` 本身是序数。因此 `Lset γ` 是合法的可构造层，可以在其中收集各条独立的单射码。

```agda
    oγ : IsOrd γ
    oγ = boundingOrd (Lift {ℓ-zero} {ℓ} ℕ) (λ n → ls (lower n) .fst) (λ n → ls (lower n) .snd .fst) .snd .fst
```

对每个自然数 `n`，最小层 `ls n` 都属于公共上界 `γ`。这条严格界正是使用可构造层级单调性所需的条件。

```agda
    bnd-in : (n : ℕ) → ⟨ ls n .fst ∈ γ ⟩
    bnd-in n = boundingOrd (Lift {ℓ-zero} {ℓ} ℕ) (λ n → ls (lower n) .fst) (λ n → ls (lower n) .snd .fst)
                 .snd .snd (lift n)
```

更小层处的码成为公共层处的码：迭代的编码由层单调性搬运进 `Lset γ`。

```agda
  code-at-γ : (n : ℕ) → ⟨ HoldsAt n γ ⟩
  code-at-γ n = PT.map raise (ls n .snd .snd .fst)
    where
    raise : Σ[ F ∈ S ] (⟨ fst F ∈ Lset (ls n .fst) ⟩ × InjCode F (hullStep n) κ)
          → Σ[ F ∈ S ] (⟨ fst F ∈ Lset γ ⟩ × InjCode F (hullStep n) κ)
```

该搬运把码与其在更大层中的隶属配对，码本身不动；移动的只是层见证。

```agda
    raise (F , h , code) = F , Lset-mono {α = γ} {β = ls n .fst} (bnd-in n) h , code
```

令 `Lγ` 为底层集合等于公共层 `Lset γ` 的可构造集合。它是一个内部定义域，容纳每个有限迭代的单射码。

```agda
  opaque
    Lγ : S
    Lγ = LsetS γ oγ
```

其底层集按定义就是层 `Lset γ`。

```agda
    Lγ-fst : fst Lγ ≡ Lset γ
    Lγ-fst = refl
```

诸迭代自身也被收集为一个可构造集合：`Iter` 把每个内部数码与其所索引的闭包迭代配对。

```agda
    Iter : S
    Iter = It.iter
```

由迭代集合的引入规则，每对「数码与其迭代」都是成员。

```agda
    Iter-in : (n : ℕ) → ⟨ pr (# n) (fst (hullStep n)) ∈ fst Iter ⟩
    Iter-in = It.iter-in
```

反过来，每个成员都仅仅是这样的对，因此 `Iter` 中的隶属恰指认被计数的迭代，别无其他。

```agda
    Iter-out : (y : S) → ⟨ fst y ∈ fst Iter ⟩ → ∥ Σ[ n ∈ ℕ ] (fst y ≡ pr (# n) (fst (hullStep n))) ∥₁
    Iter-out = It.iter-out
```

内部数码 `n` 处可构造码 `F` 的表见证由两个事实组成：`F` 位于公共层；并且仅仅地存在记录在 `n` 处的迭代 `Zn`，使 `F` 编码 `Zn` 到 `κ` 的单射。

```agda
  TabWit : (F n : S) → Type (ℓ-suc ℓ)
  TabWit F n = ⟨ fst F ∈ Lset γ ⟩ × ∥ Σ[ Zn ∈ S ] (Holds Iter n Zn × InjCode F Zn κ) ∥₁
```

`tabBody` 有三个自由槽，分别放置码 `F`、内部数码 `n` 和一个未使用的关系参数。它断言 `F ∈ Lset γ`，并存在量化一个迭代 `Zn`，使 `Iter(n,Zn)` 成立且 `F` 编码单射 `Zn ↪ κ`。这个存在量词在 `S` 上无界。

```agda
  opaque
    tabBody : Formula S 3
    tabBody = (var i1 ∈̇ con Lγ) ∧̇ ∃̇ (appC Iter i1 i0 ∧̇ injFo κ i2 i0)
```

读回表主体使用应用原子的充分性与单射公式的读取，把满足转换为两分量的表见证。

```agda
    tab-read : (F n q : S) → ⟨ (n ∷ F ∷ q ∷ []) ⊨ tabBody ⟩ → TabWit F n
    tab-read F n q (hF , h) = subst (λ w → ⟨ fst F ∈ w ⟩) Lγ-fst hF
      , PT.map (λ { (Zn , hI , hc) → Zn
          , subst ⟨_⟩ (appC-adequate Iter i1 i0 (Zn ∷ n ∷ F ∷ q ∷ [])) hI
          , InjFo.read κ i2 i0 (Zn ∷ n ∷ F ∷ q ∷ []) hc }) h
```

反过来，`TabWit F n` 见证给出 `tabBody` 的满足。层隶属被搬运为属于 `Lγ`，而迭代关系与单射码则经应用公式和单射公式的充分性反向转换。

```agda
    tab-fill : (F n q : S) → TabWit F n → ⟨ (n ∷ F ∷ q ∷ []) ⊨ tabBody ⟩
    tab-fill F n q (hF , h) = subst (λ w → ⟨ fst F ∈ w ⟩) (sym Lγ-fst) hF
      , PT.map (λ { (Zn , hI , hc) → Zn
          , subst ⟨_⟩ (sym (appC-adequate Iter i1 i0 (Zn ∷ n ∷ F ∷ q ∷ []))) hI
          , InjFo.fill κ i2 i0 (Zn ∷ n ∷ F ∷ q ∷ []) hc }) h
```

`tabBody` 所定义的关系被收集为 `Lγ × ω` 的一个可构造子集。其成员是满足表见证条件的对 `(F,n)`；尽管 `tabBody` 中显示的存在量词无界，仍可用它进行分离，因为这里采用的是完整分离。

```agda
  private
    module TableGraph = Relation Lγ ωʟ tabBody
      (λ F n → TabWit F n , isProp× (snd (fst F ∈ Lset γ)) squash₁) tab-read tab-fill
```

以 `Gt` 表示这个可构造关系。对 `(F,n)` 属于它，当且仅当 `F ∈ Lset γ`，并且仅仅存在记录在 `n` 处的迭代 `Zn`，使 `F` 编码从 `Zn` 到 `κ` 的单射。

```agda
  Gt : S
  Gt = TableGraph.rel
```

若 `F ∈ Lset γ`、`n ∈ ω`、`Iter(n,Zn)`，且 `F` 编码 `Zn ↪ κ`，则对 `(F,n)` 属于 `Gt`。在该关系的刻画中，迭代 `Zn` 只保留在命题截断之下。

```agda
  Gt-in : (F n Zn : S) → ⟨ fst F ∈ Lset γ ⟩ → ⟨ fst n ∈ fst ωʟ ⟩
        → Holds Iter n Zn → InjCode F Zn κ → Holds Gt F n
  Gt-in F n Zn hF hn hI code = TableGraph.into F n
    (subst (λ w → ⟨ fst F ∈ w ⟩) (sym Lγ-fst) hF) hn (hF , ∣ Zn , hI , code ∣₁)
```

消去把表条目读回两分量见证。

```agda
  Gt-out : (F n : S) → Holds Gt F n → TabWit F n
  Gt-out = TableGraph.pair-out
```

`ω` 中的每个内部数码都有表条目：它记录的迭代是某个有限闭包层，其码已由上述搬运存在于公共层。

```agda
  have-code : (n : S) → ⟨ fst n ∈ fst ωʟ ⟩ → ∥ Σ[ F ∈ S ] Holds Gt F n ∥₁
  have-code n hn = PT.rec squash₁ at (It.ω-num n hn)
    where
    at : It.Num n → ∥ Σ[ F ∈ S ] Holds Gt F n ∥₁
    at (k , qk) = PT.map
```

随后把该码引入表中：迭代同一视沿数码等式搬运，使条目记录的是该数码与其自身迭代配对。

```agda
      (λ { (F , hF , code) → F
         , Gt-in F n (hullStep k) hF hn
             (subst (λ w → ⟨ pr w (fst (hullStep k)) ∈ fst Iter ⟩) (cong fst qk) (Iter-in k)) code })
      (code-at-γ k)
```

对 `Gt` 应用最小原像选择，以 `ω` 为定义域、`Lγ` 为码界。它为每个内部数码选取层序下最小的相关单射码，并把对 `(n,eS(n))` 收集成可构造表 `Te`。这种在同一公共层内的可定义选择避免了直接从截断族 `counted n` 中挑选代表。

```agda
  module Tb = LeastPre γ oγ Gt ωʟ Lγ
    (λ F n h → subst (λ w → ⟨ fst F ∈ w ⟩) (sym Lγ-fst) (Gt-out F n h .fst))
    (λ F hF → subst (λ w → ⟨ fst F ∈ w ⟩) Lγ-fst hF)
    have-code
    using ( T; fn; T-in; T-out; fn-holds )
```

`Te` 是所选条目的可构造图。其定义域是内部的 `ω`，在每个数码处的值是由 `Gt` 与该数码相关的最小码。

```agda
  Te : S
  Te = Tb.T
```

最小条目函数给 `ω` 中的每个内部数码指派：为该处记录的迭代编码的最小表条目。

```agda
  eS : (n : S) → ⟨ fst n ∈ fst ωʟ ⟩ → S
  eS = Tb.fn
```

对每个 `n ∈ ω`，有序对 `(n,eS(n))` 都属于 `Te`。因此，`Te` 把所选码记录为数码 `n` 处的值。

```agda
  Te-in : (n : S) (m : ⟨ fst n ∈ fst ωʟ ⟩) → ⟨ pr (fst n) (fst (eS n m)) ∈ fst Te ⟩
  Te-in = Tb.T-in
```

反过来，若 `(n,F) ∈ Te`，则 `n ∈ ω`，且 `F` 的底层集合等于所选条目 `eS(n)` 的底层集合。`n ∈ ω` 的隶属证明是命题值的，因此不会产生额外的表值。

```agda
  Te-out : (n F : S) → ⟨ pr (fst n) (fst F) ∈ fst Te ⟩
         → Σ[ m ∈ ⟨ fst n ∈ fst ωʟ ⟩ ] (fst F ≡ fst (eS n m))
  Te-out = Tb.T-out
```

所选条目 `eS(n)` 满足 `TabWit` 的第二分量：仅仅存在记录在 `n` 处的某个迭代 `Zn`，且 `eS(n)` 编码单射 `Zn ↪ κ`。这个存在仍被截断，因为表的刻画只包含其存在性。

```agda
  e-wit : (n : S) (m : ⟨ fst n ∈ fst ωʟ ⟩)
        → ∥ Σ[ Zn ∈ S ] (Holds Iter n Zn × InjCode (eS n m) Zn κ) ∥₁
  e-wit n m = Gt-out (eS n m) n (Tb.fn-holds n m) .snd
```

对自然数 `k` 的典范数码，截断被消去。该数码处的表条目编码了迭代 `hullStep k` 到 `κ` 的单射；由于 `InjCode` 是命题，消去合法。

```agda
  e-code : (k : ℕ) → InjCode (eS (nn k) (#∈ω k)) (hullStep k) κ
  e-code k = PT.rec (isPropInjCode (eS (nn k) (#∈ω k)) (hullStep k) κ) read (e-wit (nn k) (#∈ω k))
    where
    F : S
    F = eS (nn k) (#∈ω k)
```

先确定被记录的迭代：迭代集合的成员仅仅是这样的对，其数码分量与迭代分量都可读出，而配对等式识别出被记录的迭代。

```agda
    read : Σ[ Zn ∈ S ] (Holds Iter (nn k) Zn × InjCode F Zn κ) → InjCode F (hullStep k) κ
    read (Zn , hI , code) = PT.rec (isPropInjCode F (hullStep k) κ) at
      (Iter-out (prʟ (nn k) Zn) (subst (λ w → ⟨ w ∈ fst Iter ⟩) (sym (prʟ-fst (nn k) Zn)) hI))
      where
      at : Σ[ k' ∈ ℕ ] (fst (prʟ (nn k) Zn) ≡ pr (# k') (fst (hullStep k'))) → InjCode F (hullStep k) κ
```

数码等式迫使 `k'` 即 `k`，而码沿两个迭代的同一视被搬运，码本身不变。

```agda
      at (k' , q) = injcode-resp F F Zn (hullStep k) κ refl
        (snd ee ∙ cong (λ j → fst (hullStep j)) (sym (#-inj k k' (fst ee)))) code
        where
        ee : (# k ≡ # k') × (fst Zn ≡ fst (hullStep k'))
        ee = pr-inj (sym (prʟ-fst (nn k) Zn) ∙ q)
```

`FinWit p z` 仅仅记录内部数码 `n ∈ ω`、值 `v` 与表条目 `F`。其中的等式和图隶属表示 `p=(n,v)`、`Te(n)=F` 以及 `F(z)=v`。因此，用于计数 `z` 的对码是 `p`，而不是 `F`。

```agda
  FinWit : (p z : S) → Type (ℓ-suc ℓ)
  FinWit p z = ∥ Σ[ n ∈ S ] Σ[ v ∈ S ] Σ[ F ∈ S ]
      ((fst p ≡ pr (fst n) (fst v)) × ⟨ fst n ∈ fst ωʟ ⟩ × Holds Te n F × Holds F z v) ∥₁
```

`inner₆` 是两条应用陈述的合取：表 `Te` 把 `n` 映到条目 `F`，而该条目把 `z` 映到 `v`。在环境 `F,v,n,z,p,q` 中，它们恰是 `Holds Te n F` 与 `Holds F z v`。

```agda
  opaque
    inner₆ : Formula S 6
    inner₆ = appC Te i2 i0 ∧̇ appAt i0 i3 i1
```

填充两个原子使用其充分性引理，于是见证记录在单一环境中产出两个应用原子的满足。

```agda
    inner₆-in : (F v n z p q : S) → Holds Te n F → Holds F z v
              → ⟨ (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []) ⊨ inner₆ ⟩
    inner₆-in F v n z p q ht hv =
        subst ⟨_⟩ (sym (appC-adequate Te i2 i0 (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []))) ht
      , subst ⟨_⟩ (sym (appAt-adequate i0 i3 i1 (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []))) hv
```

读取两个原子沿正向使用同样的充分性引理，恢复表满足与图隶属。

```agda
    inner₆-out : (F v n z p q : S) → ⟨ (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []) ⊨ inner₆ ⟩
               → Holds Te n F × Holds F z v
    inner₆-out F v n z p q (ht , hv) =
        subst ⟨_⟩ (appC-adequate Te i2 i0 (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ [])) ht
      , subst ⟨_⟩ (appAt-adequate i0 i3 i1 (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ [])) hv
```

`nv₃` 的自由变元是 `z,p,q`，并依次存在量化 `n`、`v`、`F`。公式体陈述 `p=(n,v)`、`n ∈ ω`、`Te(n)=F` 与 `F(z)=v`；自由变元 `q` 未被使用。

```agda
  opaque
    nv₃ : Formula S 3
    nv₃ = ∃̇ (∃̇ (prAtL i3 i1 i0 ∧̇ ((var i1 ∈̇ con ωʟ) ∧̇ ∃̇ inner₆)))
```

给定 `p=(n,v)`、`n ∈ ω`、`Te(n)=F` 与 `F(z)=v`，三个见证 `n`、`v`、`F` 依次填入嵌套存在量词。配对的充分性给出配对原子，`inner₆-in` 给出两个应用原子。

```agda
    nv₃-in : (z p q n v F : S) → fst p ≡ pr (fst n) (fst v) → ⟨ fst n ∈ fst ωʟ ⟩
           → Holds Te n F → Holds F z v → ⟨ (z ∷ p ∷ q ∷ []) ⊨ nv₃ ⟩
    nv₃-in z p q n v F qp hn ht hv =
      ∣ n , ∣ v , ( subst ⟨_⟩ (sym (prAtL-adequate i3 i1 i0 (v ∷ n ∷ z ∷ p ∷ q ∷ []))) qp
                  , ( hn , ∣ F , inner₆-in F v n z p q ht hv ∣₁ ) ) ∣₁ ∣₁
```

读取 `nv₃` 时，先消去 `n` 的截断见证，再消去 `v` 的截断见证。固定 `n` 与 `v` 后，`Inner n v` 保留配对原子、隶属关系 `n ∈ ω`，以及满足 `inner₆` 的条目 `F` 的第三层截断存在。

```agda
    nv₃-out : (z p q : S) → ⟨ (z ∷ p ∷ q ∷ []) ⊨ nv₃ ⟩ → FinWit p z
    nv₃-out z p q = PT.rec squash₁ at₁
      where
      Inner : (n v : S) → Type (ℓ-suc ℓ)
      Inner n v = ⟨ (v ∷ n ∷ z ∷ p ∷ q ∷ []) ⊨ prAtL i3 i1 i0 ⟩
```

最内层的截断存在给出表条目 `F`，而不是已经固定的值 `v`。配对的充分性把配对原子转换为 `p=(n,v)`，`inner₆-out` 则恢复 `Te(n)=F` 与 `F(z)=v`；这些数据组成 `FinWit p z`。

```agda
                × ( ⟨ fst n ∈ fst ωʟ ⟩ × ∥ Σ[ F ∈ S ] ⟨ (F ∷ v ∷ n ∷ z ∷ p ∷ q ∷ []) ⊨ inner₆ ⟩ ∥₁ )
      at₃ : (n v : S) → Inner n v → FinWit p z
      at₃ n v (qp , (hn , h)) = PT.map
        (λ { (F , hi) → n , v , F
           , ( subst ⟨_⟩ (prAtL-adequate i3 i1 i0 (v ∷ n ∷ z ∷ p ∷ q ∷ [])) qp
```

固定 `n` 与 `v` 后，最内层转换产生 `FinWit p z`；外侧两次消去再依次处理 `v` 与 `n` 的截断选择。因此，`nv₃` 的满足恰好给出外围关系所需的截断元组。

```agda
             , hn , inner₆-out F v n z p q hi ) }) h
      at₂ : (n : S) → Σ[ v ∈ S ] Inner n v → FinWit p z
      at₂ n (v , h) = at₃ n v h
      at₁ : Σ[ n ∈ S ] ∥ Σ[ v ∈ S ] Inner n v ∥₁ → FinWit p z
      at₁ (n , h) = PT.rec squash₁ (at₂ n) h
```

最终关系由分离从 `prodL κ` 与 `hullL` 的笛卡尔积中取得。定义它的公式是 `nv₃`，其三个存在见证分别为内部自然数 `n`、值 `v` 与表项 `F`。当且仅当 `p = (n,v)`、`n ∈ ω`、表在 `n` 处记录 `F`，且 `F` 在 `z` 处记录 `v` 时，该关系才把 `p` 与 `z` 联系起来。

```agda
  private
    module FinalGraph = Relation (prodL κ) hullL nv₃ (λ p z → FinWit p z , squash₁)
      (λ p z q → nv₃-out z p q)
      (λ p z q → PT.rec (snd ((z ∷ p ∷ q ∷ []) ⊨ nv₃))
        (λ { (n , v , F , qp , hn , ht , hv) → nv₃-in z p q n v F qp hn ht hv }))
```

分离所得的集合命名为 `Gf`，即最终图的可构造载体。

```agda
  Gf : S
  Gf = FinalGraph.rel
```

要引入 `Gf` 中的隶属，取 `p ∈ prodL κ`、`z ∈ hullL`、内部自然数 `n ∈ ω`、值 `v` 与表项 `F`。等式 `p = (n,v)`，连同表示 `Te` 在 `n` 处记录 `F`、`F` 在 `z` 处记录 `v` 的两条图隶属，恰好给出定义关系所需的见证。

```agda
  Gf-in : (p z n v F : S) → ⟨ fst p ∈ fst (prodL κ) ⟩ → ⟨ fst z ∈ fst hullL ⟩
        → fst p ≡ pr (fst n) (fst v) → ⟨ fst n ∈ fst ωʟ ⟩ → Holds Te n F → Holds F z v
        → Holds Gf p z
  Gf-in p z n v F hp hz qp hn ht hv = FinalGraph.into p z hp hz ∣ n , v , F , qp , hn , ht , hv ∣₁
```

反过来，`Gf-out` 把一条图隶属化为命题截断的记录 `FinWit p z`。在证明集合隶属或集合相等等命题值结论时，可以消去这份记录的截断。

```agda
  Gf-out : (p z : S) → Holds Gf p z → FinWit p z
  Gf-out = FinalGraph.pair-out
```

每个表项所记录的值都属于 `κ`。由 `Te(n,F)`，表的读法把 `F` 与 `n` 处选出的表项同一视；`e-wit` 为该选定表项给出一个迭代 `Zn` 及从 `Zn` 到 `κ` 的单射码。把 `F(z)=v` 沿表项的同一视搬运后，该码的值域条款便证明 `v ∈ κ`。

```agda
  entry-ran : (n F z v : S) → Holds Te n F → Holds F z v → ⟨ fst v ∈ fst κ ⟩
  entry-ran n F z v ht hv = PT.rec (snd (fst v ∈ fst κ))
    (λ { (Zn , _ , code) → snd (snd (snd code)) z v
          (subst (λ w → ⟨ pr (fst z) (fst v) ∈ w ⟩) (Te-out n F ht .snd) hv) })
    (e-wit n (Te-out n F ht .fst))
```

凡被 `Gf` 关联的第一分量都属于 `prodL κ`。相应记录把它写成 `(n,v)`，其中 `n ∈ ω` 且 `v ∈ κ`。由于非有限序数 `κ` 包含 `ω`，还有 `n ∈ κ`；故两个坐标都属于 `κ`，从而 `(n,v) ∈ prodL κ`。

```agda
  inPκ : (p z : S) → Holds Gf p z → ⟨ fst p ∈ fst (prodL κ) ⟩
  inPκ p z h = PT.rec (snd (fst p ∈ fst (prodL κ)))
    (λ { (n , v , F , (qp , hn , ht , hv)) →
       subst (λ w → ⟨ w ∈ fst (prodL κ) ⟩) (sym qp)
         (prodL-in κ n v (ω⊆ (fst κ) oκ κ∉ω (fst n) hn) (entry-ran n F z v ht hv)) })
```

把上述论证施于 `Gf-out` 返回的截断记录，便得到 `inPκ`：只要 `Gf(p,z)` 成立，其第一分量 `p` 就属于 `prodL κ`。

```agda
    (Gf-out p z h)
```

每个壳成员都纯粹地存在一个与之相关的码。迭代并的刻画把 `z` 放入某个有限阶段 `hullStep n`。对选定的图 `F = eS (# n)`，精确陈述 `e-code n` 以 `hullStep n` 为定义域；因此其全域性条款纯粹地给出一个满足 `F(z)=v` 的值 `v`。

```agda
  have-fin : (z : S) → ⟨ fst z ∈ fst hullL ⟩ → ∥ Σ[ p ∈ S ] Holds Gf p z ∥₁
  have-fin z hz = PT.rec squash₁ at (It.iterUnion-out z hz)
    where
    at : Σ[ n ∈ ℕ ] ⟨ fst z ∈ fst (hullStep n) ⟩ → ∥ Σ[ p ∈ S ] Holds Gf p z ∥₁
    at (n , hn) = PT.map val (domAt-in zero (suc zero) (F ∷ hullStep n ∷ []) (fst (snd (e-code n))) z hn)
```

`e-code n` 的全域性条款给出值 `v`，以及图隶属 `F(z)=v`。把标准数码 `# n` 与该值配对，便得到候选码 `p = (# n,v)`。

```agda
      where
      F : S
      F = eS (nn n) (#∈ω n)
      val : Σ[ v ∈ S ] Holds F z v → Σ[ p ∈ S ] Holds Gf p z
      val (v , hv) = prʟ (nn n) v
```

引入规则组装整个记录：该对因数码隶属与码的值域条款而属于乘积，而图凭表自身的隶属把它与 `z` 关联。

```agda
        , Gf-in (prʟ (nn n) v) z (nn n) v F
            (subst (λ w → ⟨ w ∈ fst (prodL κ) ⟩) (sym (prʟ-fst (nn n) v))
              (prodL-in κ (nn n) v (num∈κ n) (snd (snd (snd (e-code n))) z v hv)))
            hz (prʟ-fst (nn n) v) (#∈ω n) (Te-in (nn n) (#∈ω n)) hv
```

最小原像选取所需的函数性从候选码指回壳：若同一个 `p` 同时关联 `z` 与 `z'`，则 `z = z'`。这一性质使从壳成员到其最小码的选取映射成为单射。两份关系见证都是截断记录，而此处的目标是集合相等这一命题，故可消去它们的截断。

```agda
  funct-fin : (p z z' : S) → Holds Gf p z → Holds Gf p z' → fst z ≡ fst z'
  funct-fin p z z' h h' = PT.rec2 (setIsSet (fst z) (fst z')) read (Gf-out p z h) (Gf-out p z' h')
    where
    read : Σ[ n ∈ S ] Σ[ v ∈ S ] Σ[ F ∈ S ]
             ((fst p ≡ pr (fst n) (fst v)) × ⟨ fst n ∈ fst ωʟ ⟩ × Holds Te n F × Holds F z v)
```

展开两份记录，分别得到 `n,v,F` 与 `n',v',F'`。每份记录都含一条配对等式，即 `p=(n,v)` 或 `p=(n',v')`，并含三项事实：索引属于 `ω`、表在该索引处记录相应表项，以及该表项在对应壳成员处记录所示的值。

```agda
         → Σ[ n' ∈ S ] Σ[ v' ∈ S ] Σ[ F' ∈ S ]
             ((fst p ≡ pr (fst n') (fst v')) × ⟨ fst n' ∈ fst ωʟ ⟩ × Holds Te n' F' × Holds F' z' v')
         → fst z ≡ fst z'
    read (n , v , F , (qp , hn , ht , hv)) (n' , v' , F' , (qp' , hn' , ht' , hv')) =
      PT.rec (setIsSet (fst z) (fst z'))
```

两条配对等式先给出 `n=n'` 与 `v=v'`。随后，表的读法把 `F`、`F'` 与同一个选定表项 `eS n m` 对齐。见证 `e-wit n m` 为该表项给出一个迭代 `Zn` 及相应的单射码。把两条图隶属都搬运到这一共同表项，并把第二个值沿 `v'=v` 搬运后，单射性条款便给出 `z=z'`。

```agda
        (λ { (Zn , _ , code) →
           injAt-out zero (eS n m ∷ Zn ∷ []) (fst (snd (snd code))) v z z'
             (subst (λ w → ⟨ pr (fst z) (fst v) ∈ w ⟩) (Te-out n F ht .snd) hv)
             (subst2 (λ u w → ⟨ pr (fst z') u ∈ w ⟩) (sym (snd ee)) qF hv') })
        (e-wit n m)
```

有序对的单射性把该同一视拆分为数码分量与值分量，而表读取证明数码属于 `ω`。

```agda
      where
      ee : (fst n ≡ fst n') × (fst v ≡ fst v')
      ee = pr-inj (sym qp ∙ qp')
      m : ⟨ fst n ∈ fst ωʟ ⟩
      m = Te-out n F ht .fst
```

两对「数码连同 `ω` 隶属」相等，因为 `ω` 隶属是命题，而数码等式是底层集合的等式。

```agda
      pth : _≡_ {A = Σ[ c ∈ S ] ⟨ fst c ∈ fst ωʟ ⟩} (n' , Te-out n' F' ht' .fst) (n , m)
      pth = Σ≡Prop (λ c → snd (fst c ∈ fst ωʟ)) (S≡ {x = n'} {y = n} (sym (fst ee)))
```

把 `F'` 的表读法沿两个内部自然数索引的相等搬运，便把 `F'` 与选定表项 `eS n m` 同一视。再结合 `F` 的相应读法，两条图隶属就落在同一个单射图中。

```agda
      qF : fst F' ≡ fst (eS n m)
      qF = Te-out n' F' ht' .snd ∙ (λ i → fst (eS (fst (pth i)) (snd (pth i))))
```

令 `γf` 为可构造集合 `prodL κ` 所对应的序数阶段。它给出包含所有候选码的共同层 `Lset γf`，从而可用典范阶段序比较这些原像。

```agda
  γf : V ℓ
  γf = stage (fst (prodL κ)) (snd (prodL κ))
```

该层是序数，正如所有层一样。

```agda
  oγf : IsOrd γf
  oγf = stage-ord (fst (prodL κ)) (snd (prodL κ))
```

由其阶段的定义性质，集合 `prodL κ` 属于 `Lset γf`。由于 `Lset γf` 是传递集，`prodL κ` 的每个成员也都属于 `Lset γf`；故 `prodL κ ⊆ Lset γf`。

```agda
  prodκ⊆Lγ : (p : S) → ⟨ fst p ∈ fst (prodL κ) ⟩ → ⟨ fst p ∈ Lset γf ⟩
  prodκ⊆Lγ p hp =
    layer-trans (Lset-layer γf) {x = fst (prodL κ)} {y = fst p} hp (stage-mem (fst (prodL κ)) (snd (prodL κ)))
```

对每个 `z ∈ hullL`，选取满足 `Gf(p,z)` 的阶段序最小元 `p ∈ prodL κ`。所需的三项事实恰为上文所得：每个相关的 `p` 都属于 `prodL κ`，该载体包含于 `Lset γf`，且每个壳成员都纯粹地存在一个相关的 `p`。由于 `funct-fin` 说明同一个 `p` 不会关联两个不同的壳成员，所得最小原像映射便是内部编码单射 `hullL ↪ prodL κ`。

```agda
  module LF = LeastPre γf oγf Gf hullL (prodL κ) inPκ prodκ⊆Lγ have-fin using ( module Functional )
```

最小原像构造给出从壳到 `prodL κ` 的编码单射，平方法则给出从 `prodL κ` 到 `κ` 的编码单射。二者复合便证明命题截断的陈述 `InjL hullL κ`。这是内部编码单射；它既不断言满射或基数相等，也不涉及任何塌缩像。因此，构造壳的所有成员在内部都有彼此不同的 `κ`-码。

```agda
  hull↪κ : InjL hullL κ
  hull↪κ = injl-trans hullL (prodL κ) κ (LF.Functional.injL funct-fin) pairκ
```