把小集合对可定义的最小见证封闭，应当保持原有的无穷基数界。本章在 L 内部证明：若起始集合单射入一个无穷基数，则其 Skolem 壳也单射入该基数。

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

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

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

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

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

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

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

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

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 中的集合。分离构造子图，配对与并构成其编码，充分性则把应用、单值性与定义域的内部公式同其集合论含义连接起来。

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 只保留这种图存在这一命题。

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 封闭提供这种映射，内部乘积则容纳带标签的对。

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 中的集合。

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

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 )

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

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

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

open import Cubical.Foundations.Prelude using ( subst2 )

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

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

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

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

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

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

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

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

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

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

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

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

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。

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

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

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

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

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

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

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

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

  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 的定义等式后，同样的后继模式定义第五与第六位置。这些名称使嵌套绑定造成的位移在编码公式的类型中清晰可见。

  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

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

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

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

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 α。

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

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

module Union2 (D₁ D₂ : S) where

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

  D : S
  D = cupʟ D₁ D₂

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

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

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

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

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

  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₂ 到 κ × κ 的单射。此构造不要求 κ 是序数。

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

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

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

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

  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 这一命题。输入连同这条证明，恰好提供分段函数求值所需的定义域证据。

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

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

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

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

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

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

  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)

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

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

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

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

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

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

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

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

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

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

    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 之对的等式。

          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)，沿充分性反向搬运便得到应用原子的满足。

      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

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

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

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

    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₁  y z v ha ht }) hv)
         ; (inr (h , hv)) → inr ((λ z∈ → lower (h z∈))
             , PT.map (λ { (v , (ha , ht)) → v , rd E₂  y z v ha ht }) hv) })

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

    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₁  y z v ha ht }) hv) ∣₁
    fo-in y z (inr (h , hv)) =
      ∣ inr ((λ z∈ → lift (h z∈))

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

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

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

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

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

    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 κ ⟩

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

    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₂ 提取的函数。两种情形中，提取过程都同时给出图条目，以及把带标签的对认同为所选取值的等式。

  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 ) (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 ) (X₂.toFun (z , off z m no))) ∣₁)

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

  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 (# )) (sv₁ z v (X₁.toFun (z , h)) hg (X₁.toFun-graph (z , h)))
          ∙ sym (prʟ-fst (nn ) (X₁.toFun (z , h))) }) hv

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

  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 (# )) (sv₂ z v (X₂.toFun (z , off z m no)) hg (X₂.toFun-graph (z , off z m no)))

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

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

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

  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 ) (X₁.toFun (z , h))))
    (prodL-in κ (nn ) (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 ) (X₂.toFun (z , off z m no))))
    (prodL-in κ (nn ) (X₂.toFun (z , off z m no)) 1∈κ

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

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

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

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

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

    ; 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)) }

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

  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 反演：标签一致，故取值的等式认同两个函数值，这正是单射性子句所要的论证。

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

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

      (pr-inj (sym (prʟ-fst (nn ) (X₁.toFun (z , h))) ∙ q ∙ prʟ-fst (nn ) (X₂.toFun (z' , off z' m' no')))))))
    go (inr no) (inl h') q = Empty.rec (snotz (#-inj   (fst
      (pr-inj (sym (prʟ-fst (nn ) (X₂.toFun (z , off z m no))) ∙ q ∙ prʟ-fst (nn ) (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')))

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

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

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

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

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

tag-union : (κ : S) → ⟨ #  ∈ fst κ ⟩ → ⟨ #  ∈ 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 前驱；任务在于典范地选取一个。

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

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

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

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

  private
    graphFo : Formula S 
    graphFo = appC G i0 i1

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

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

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

      (have z m)

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

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

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

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

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

  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 为陪域记录，取值的所属由既有假设的向内方向保证。

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

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

  T : S
  T = Ls.T

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

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

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

  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

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

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

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

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

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

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

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

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

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

  Y : S
  Y = sglʟ a

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

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

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

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

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

  fo : Formula S 
  fo = var i0 ≐ con ∅ʟ

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

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

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

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

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

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

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

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

计数每一步有限闭包

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

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 ∅∈λ)

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

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

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

  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 ω 的证明。唯一性是在公式键与环境固定之后成立的。

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

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

  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 )

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

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

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

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

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

  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) κ。

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

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

    ΦZ : S
    ΦZ = B.Φ Z

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

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

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

      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₂。

    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₂ 的隶属，并把对象层的反驳降回普通的蕴涵。

      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，并且满足那条否定原子。

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

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

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

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

      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∅。

    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₂，以及与空集的等式。

      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₂ 中不等于空集的元素。

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

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

      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₂，并要求对「与空集相等」的反驳。

    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₂ 的隶属与那条反驳，后者已从对象层降下。

      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。接下来的引理证明到这两个并集的所需包含关系。

        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 可构造。

    Φ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 证明它属于新增部分，再使用第二条包含。

      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)

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

    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 进入。

      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∅ ↪ κ。

    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∈κ ))

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

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

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

    PB : S
    PB = prodL U₂.D

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

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

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

      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)

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

      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 是由二者确定的最小见证。

    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，钉定公式承载见证条件。

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

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

      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 与截断的剩余部分。

      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 的命题截断之下。

        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 与其对象语言公式的满足之间的两个方向。

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

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

    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 的数据。

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

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

    G : S
    G = WitnessGraph.rel

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

    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。它不会在该截断之外选出键与环境。

    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 会给出它进入闭包步的三种可能原因。

    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 的旧成员，也不能是空集。剩下的就是见证情形，经见证公式的外向引理读取。

      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 ω。

        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 的有限序列进入。随后该关系接受这个对。

                (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' 的底层集合相等。同一个元素仍可拥有不同的码。

    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)

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

           → Σ[ 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 元素的等式。

        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'。

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

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

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

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

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

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

    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。它不声称见证码原本就唯一，而且这里得到的只是非空新增部分的计数，尚非完整的单步结论。

    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 仅仅具有某个相关码，而层序选出其中最小者。选取之前码无须唯一；单射性来自一个固定码至多表示一个见证。

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

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

    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 ↪ κ。两次折叠都使用平方律，因而都依赖内部基数性。

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

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

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

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

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

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

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