计数无穷可构造层的工具

在 L 内部计数无穷序数 δ 的层 Lset δ，依赖两件材料：基础单射 Lω ↪ ω，以及把单射逐项提升到有限环境的手段。本章给出这两者；本章所证的一切，都恰针对文中点名的构造。

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

本章在固定宇宙层级的排中律下工作。全章调用的构造都继承这一假设；它在本章中最清楚的两项作用，是在有穷层的点名册中搜索一个名称，以及用序数三歧比较塌缩值与 ω。

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

因此，所有构造共享唯一的假设 lem : LEM (ℓ-suc ℓ)。特别地，下文的有限搜索由排中律推出，并不调用选择公理。

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

下文使用的内部图必须由 L 自身能够解释的公式描述。相等、隶属、合取、蕴涵以及有界和无界量词，共同提供了表达「一个关系是全域单值单射」并定义它在有限环境上作用的语言。

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.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import V.Model {ℓ} using ( ∈sucV-inl; self∈sucV )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; #mono )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset→isL )

序数结构在两处进入论证。数码标识环境的有限定义域，而可构造层上的序稍后给出 Lset ω 的典范良序。随后，三分法判断序数塌缩的每个值相对于 ω 所处的位置。

open import L.Ordinal {ℓ} using ( ∈#-elim; mem-ord; ω-ord; numeral-ord; #∈ω )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )

编码单射由一个有序对集合表示。它的四项义务分别断言：图是单值的、定义域恰为指定集合、在输入上单射，并且取值落在指定目标中。本章第一部分从这样一个实际给定的编码图出发。

open import L.Coding.Model {ℓ} using ( prʟ; prʟ-fst; svAt; svAt-in; svAt-out; domAt; domAt-in; domAt-out; domAt-intro; appAt; appAt-adequate; envOverAt; envOverAt-transport )
open import L.Coding.Expressions {ℓ} using ( numL )
open import L.Coding.Injection {ℓ} lem
  using ( injAt; injAt-in; injAt-out; module Small )
open import L.Coding.Environment {ℓ} using ( env; lookup-spec )

对每个自然数 n，取值于 A 的长度 n 环境都有具体呈现。集合 seqL A 汇集所有有限长度。因此，一个逐项作用并保持长度的映射，正是把 A 上所有有限序列送入 B 上有限序列所需的操作。

open import L.Coding.EnvironmentSet {ℓ} lem
  using ( Ix; envS; envSet-in; envSet-out; envOver; module Recover )
open import L.Choice.NameComparison {ℓ} lem using ( domAt-numeral; domAt-fill )
open import L.Choice.StageOrders {ℓ} lem
  using ( carry; memOf; orderAt; orderAt-step; relOf

第二部分先按诞生层排列 Lset ω 的成员；诞生层相同时，再按该层上的步进序排列。这一区分不可忽略：一个前驱可以与其后继具有相同诞生层，但每个前驱仍落在该共同层的后继层中。

        ; birth-mem; module Family )
  renaming ( Mem to MemOf )
open import L.Choice.OrderTable {ℓ} lem using ( Related; IsRel; ixRel-rep; ixRel-fill )
open import L.Choice.InternalWellOrder {ℓ} lem using ( relL; relL-spec )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}

塌缩这一良序，会为 Lset ω 的每个成员赋予一个序数。接下来的任务是证明每个塌缩值都属于 ω。证明逐个处理前驱段，把它界定在某个有限可构造层内，并排除从 ω 到该层的单射。

  using ( SWO; lt; eq; gt ) renaming ( Tri to TriW )
open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )

有限序列编码与塌缩论证会在后续基数计算中汇合。前者把一个已给定的编码单射逐坐标搬运，后者给出基础结论 Lset ω ↪ ω。两条陈述都不主张双射，也不计数任意无穷序列。

open import L.GCH.CardinalSquareLaw {ℓ} lem using ( isL-ord )
open import L.GCH.FiniteSequenceCoding {ℓ} lem using ( seqL; seqL-in; seqL-out )
open import L.Ordinal.SquareLaw {ℓ} lem using ( module FiniteBase )
open FiniteBase using ( fromFin; fromFin-inj )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate; ω-limit; finite-excl-ω )

每个有限层都带有列出其全部成员的有限名册。名册中可以出现重复，因此它只是满射式的命名手段，并非双射。这已经足够：排中律允许通过有界搜索，为每个给定成员找到一个名字。

open import L.Choice.FiniteStageOrders {ℓ} lem
  using ( Tally; StageOrder; stageOrder; finiteStage )  -- lint-agda: keep (StageOrder used as the projection qualifier)
open import L.GCH.OrderType {ℓ} lem using ( Holds; module Code )

所找出的名册索引把有限层的每个成员送入一个有限序数呈现。若假设存在从 ω 出发的单射，把它与这一命名映射复合，再沿对角线复制所得值，就会与有限平方排除定理矛盾。

open import Cubical.Data.Nat.Order using ( _<_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.FinSet using ( DecΣ )
open import Cubical.Relation.Nullary using ( decRec; yes; no )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId'; inj-toℕ )

后文有若干等式涉及第二分量为证明的依赖对。由于这些分量都是命题，底层集合的相等便决定打包元素的相等。由此，论证可以在 L 的元素、它们的呈现与图编码之间顺畅往返。

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Sum as Sum
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ2; isPropΠ3 )

数码除标记环境长度外还有第二项作用。一个外围集合属于 ω，只表示它等于某个数码，并不保留一个全局选定的自然数表示。后文的消去始终遵守这一命题性。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; ω; sucV )

隶属关系与图的读法中的存在性，往往只保留在命题截断 ∥_∥₁ 之下。只有当目标是命题，或先由唯一性使目标类型成为命题时，才能消去这样的见证；这一操作不会任意选取代表。

open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

同一区分也适用于最终的计数结论。InjL A B 只保留「存在某个可构造图编码从 A 到 B 的单射」这一命题，并不公开一个全局选定的宿主层函数。

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

与此相对，序列构造从一个特定的图 E 及完整数据 InjCode E A B 出发。因此，可以从该图读出宿主层函数并逐坐标使用，最后再由 InjL 隐去所得图。

module SV = hPropStructure 𝒮ᵥ using ()

从可构造集合的成员中读出的每个条目，本身也因 L 的传递性而可构造。正是这一基本事实，使有限环境及其图中的有序对仍然是内部模型的对象。

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

满足记号把公式层的图描述与这些外围隶属事实连接起来。充分性引理将在两个方向上使用，因此证明既能由具体图数据填充内部公式，也能随后从该公式读回这些数据。

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

对自然数 k，nn k 把数码 # k 与其可构造性证明打包。满足关系的环境用这些打包数码表示有限定义域。

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

下文的图公式会引入多层嵌套约束。名字 i0、i1 等缩写相应的 De Bruijn 位置，其中 i0 总是表示最近约束的变元。

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

每增加一层约束，原有变元便向后移动一个位置。这些带类型的缩写统一记录这种移动，使公式能够显出数学结构，而无须反复写出冗长的后继表达式。

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

直到 i6 的位置，足以同时指向输入环境 s、其像 y、公共定义域 n、索引 i，以及由 E 联系的两个条目。

  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
  i8 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc (suc k)))))))))
  i8 = suc i7
  i9 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc k))))))))))

最后一个缩写补齐本模块所需的位置范围。这些名字不携带任何数学假设，只用于让变元位置的记录清晰可读。

  i9 = suc i8

环境的长度与外延性

第一条刚性事实比较两个编码环境的长度。若同一个底层集合同时等于 env h 与 env h'，且两列每项都可构造，则两个长度相等：编码环境的定义域就是其长度数码，而对同一集合的两次读取由数码投影认同。

env-len : (E : S) {n n' : ℕ} (h : Fin n → V ℓ) (h' : Fin n' → V ℓ)
        → ((i : Fin n) → ⟨ isL (h i) ⟩) → ((i : Fin n') → ⟨ isL (h' i) ⟩)
        → fst E ≡ env h → fst E ≡ env h' → n ≡ n'
env-len E {n} {n'} h h' cg cg' q q' =
  #-inj′ (domAt-numeral (suc zero) zero (nn n ∷ E ∷ []) n' h' cg' q'

证明先用 n 的数码填充第一种呈现的定义域，再把同一定义域读回为 n' 的数码，最后应用数码单射性。结论只是长度相等，而非两个呈现函数的相等。

            (domAt-fill (suc zero) zero (nn n ∷ E ∷ []) n h cg q refl))

第二条刚性事实假设两列已有相同长度，且其编码图相等。分别在两个图中查找某个索引的数码键，便得到对应条目的相等。反方向，即由逐点相等构造图的相等，将在后文实际需要之处证明。

env-pt : {n : ℕ} (h h' : Fin n → V ℓ) → env h ≡ env h' → (i : Fin n) → h i ≡ h' i
env-pt h h' q i = subst ⟨_⟩ (lookup-spec h' i (h i))
  (subst (λ w → ⟨ pr (# (toℕ i)) (h i) ∈ w ⟩) q
    (subst ⟨_⟩ (sym (lookup-spec h i (h i))) refl))

把编码单射提升到有限序列

提升模块以四条数据对可构造图 E 陈述：单值性、在 A 上的全域性、在 A 上的单射性、值落在 B。这恰是从 A 到 B 的编码单射的四条条款。

module SeqMap (A B E : S)
              (sv : ⟨ (E ∷ A ∷ []) ⊨ svAt zero ⟩)
              (dm : ⟨ (E ∷ A ∷ []) ⊨ domAt zero (suc zero) ⟩)
              (ij : ⟨ (E ∷ A ∷ []) ⊨ injAt zero ⟩)
              (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst E ⟩

最后的值域条款只要求 E 中出现的每个值都属于 B。它不要求 B 的每个成员都被命中，因此这些数据描述的是单射，而非满射或双射。

                   → ⟨ fst y ∈ fst B ⟩) where

提取机制把内部图读作 A 与 B 的呈现之间的实际函数：单值性使每个值的纤维成为命题，因此无需任何选择原理即可恢复该值。

  module Sm = Small E A B sv dm ij ran using ( at; fib; small; small-inj; module E )

提取出的函数保持不透明：后文只通过其图与单射性使用它。

  opaque
    f : ⟪ fst A ⟫ → ⟪ fst B ⟫
    f = Sm.small

图记录陈述：索引的呈现元素与被呈现像构成的有序对属于 E；它由项代数自身的图记录、沿被呈现值的同一视搬运而来。

    f-graph : (m : ⟪ fst A ⟫)
            → ⟨ pr (⟪ fst A ⟫↪ m) (⟪ fst B ⟫↪ (f m)) ∈ fst E ⟩
    f-graph m = subst (λ w → ⟨ pr (⟪ fst A ⟫↪ m) w ∈ fst E ⟩)
      (sym (Sm.fib m .snd)) (Sm.E.toFun-graph (Sm.at m))

提取出的函数在 A 的呈现上单射；这正是序列提升将要逐坐标继承的逐点单射性。

    f-inj : (m n : ⟪ fst A ⟫) → f m ≡ f n → m ≡ n
    f-inj = Sm.small-inj

A 的环境条目经呈现的嵌入被读作外围集合。

  vA : {n : ℕ} → Ix A n → Fin n → V ℓ
  vA g i = ⟪ fst A ⟫↪ (g i)

B 环境的条目亦然。

  vB : {n : ℕ} → Ix B n → Fin n → V ℓ
  vB h i = ⟪ fst B ⟫↪ (h i)

提升后的赋值逐条目施加提取出的函数：A 的长度 n 环境的像是 B 的长度 n 环境，长度不变。

  fg : {n : ℕ} → Ix A n → Ix B n
  fg g i = f (g i)

A 环境的每个条目都可构造：把对 A 的隶属沿可构造性的传递性搬运。

  isLA : {n : ℕ} (g : Ix A n) (i : Fin n) → ⟨ isL (vA g i) ⟩
  isLA g i = isL-trans (member (fst A) (g i)) (snd A)

B 环境的条目亦然。

  isLB : {n : ℕ} (h : Ix B n) (i : Fin n) → ⟨ isL (vB h i) ⟩
  isLB h i = isL-trans (member (fst B) (h i)) (snd B)

对索引对象 i，Ent y s i 仅仅断言存在模型元素 u 与 v，使得 s(i)=u、y(i)=v，且图 E 把 u 送到 v。这些见证以及三项图隶属事实都保留在命题截断之下。

  Ent : (y s i : S) → Type (ℓ-suc ℓ)
  Ent y s i = ∥ Σ[ u ∈ S ] Σ[ v ∈ S ]
      ( ⟨ pr (fst i) (fst u) ∈ fst s ⟩
      × ⟨ pr (fst i) (fst v) ∈ fst y ⟩
      × ⟨ pr (fst u) (fst v) ∈ fst E ⟩ ) ∥₁

宿主层读法 Wit y s 仅仅断言：存在对象 n，它是 s 的定义域；y 是固定目标 B 上以同一 n 为定义域的环境；并且每个 i∈n 都满足 Ent y s i。因此，y 与 s 具有相同的有限形状，且其条目逐点为 s 中条目在 E 下的像。

  Wit : (y s : S) → Type (ℓ-suc ℓ)
  Wit y s = ∥ Σ[ n ∈ S ]
      ( ⟨ (n ∷ y ∷ s ∷ []) ⊨ domAt i2 i0 ⟩
      × ⟨ (B ∷ n ∷ y ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩
      × ((i : S) → ⟨ fst i ∈ fst n ⟩ → Ent y s i) ) ∥₁

条目公式恰好表达 Ent 中隐藏的三项等式：存在量化的两个值 u 与 v 满足 s(i)=u、y(i)=v 以及 E(u)=v。变元位置同时计入外围参数与这两个新见证。

  opaque
    private
      entFo : Formula S 
      entFo = ∃̇ (∃̇ ( appAt i6 i2 i1 ∧̇ appAt i5 i2 i0 ∧̇ appC E i1 i0 ))

完整公式先绑定公共定义域 n，再绑定对象 b 并要求它等于固定常元 B。公式断言 y 是定义域为 n 的 b 环境，且条目公式对每个 i∈n 成立；等式 b=B 使它恰好成为预期目标上的环境。

    fo : Formula S 
    fo = ∃̇ ( domAt i2 i0
           ∧̇ ∃̇ ( (var i0 ≐ con B)
                ∧̇ envOverAt i2 i1 i0
                ∧̇ ∀̇∈ (var i1) entFo ) )

从公式读出条目时，证明依次消去两层存在见证 u 与 v。由于 Ent y s i 本身经命题截断成为命题，这一消去是合法的。

    private
      entOut : (y s n b i : S) → ⟨ (i ∷ b ∷ n ∷ y ∷ s ∷ []) ⊨ entFo ⟩ → Ent y s i
      entOut y s n b i = PT.rec squash₁ (λ { (u , hv) →
        PT.rec squash₁ (λ { (v , (h1 , (h2 , h3))) →
          let γ = v ∷ u ∷ i ∷ b ∷ n ∷ y ∷ s ∷ [] in

两个环境应用以及图 E 的应用各有充分性定律，它们把公式的满足转换为三项外围隶属。把读回的 u、v 与这些隶属打包，便得到所需的截断条目。

          ∣ u , v
          , ( subst ⟨_⟩ (appAt-adequate i6 i2 i1 γ) h1
            , subst ⟨_⟩ (appAt-adequate i5 i2 i0 γ) h2
            , subst ⟨_⟩ (appC-adequate E i1 i0 γ) h3 ) ∣₁ }) hv })

反方向把一个截断条目映为公式的满足。证明反向使用同三条充分性等式，把外围图隶属转换为两项环境应用条款与一项 E 的应用条款。

      entIn : (y s n i : S) → Ent y s i → ⟨ (i ∷ B ∷ n ∷ y ∷ s ∷ []) ⊨ entFo ⟩
      entIn y s n i = PT.map (λ { (u , v , (h1 , h2 , h3)) →
        let γ = v ∷ u ∷ i ∷ B ∷ n ∷ y ∷ s ∷ [] in
        u , ∣ v , ( subst ⟨_⟩ (sym (appAt-adequate i6 i2 i1 γ)) h1
                  , subst ⟨_⟩ (sym (appAt-adequate i5 i2 i0 γ)) h2

把两个见证重新装入嵌套存在量词后，E 的图隶属条款补全条目公式的满足。因此，entOut 与 entIn 给出了每个索引处所需的精确对应。

                  , subst ⟨_⟩ (sym (appC-adequate E i1 i0 γ)) h3 ) ∣₁ })

主体读取器接收外层公式展开后的三项数据：n 是 s 的定义域；辅助对象 b 的底层集合与 B 相等；y 是以 n 为定义域的 b 环境，且每个索引都满足条目公式。它需要把这些数据转换为 Wit y s。

      bodyOut : (y s n b : S)
              → ⟨ (n ∷ y ∷ s ∷ []) ⊨ domAt i2 i0 ⟩
              → fst b ≡ fst B
              → ⟨ (b ∷ n ∷ y ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩
              → ⟨ (b ∷ n ∷ y ∷ s ∷ []) ⊨ ∀̇∈ (var i1) entFo ⟩

b 与 B 的底层集合相等，据此可把「在 b 上的环境」这一断言搬运到固定目标 B。每个有界索引处的条目公式由 entOut 读回，最后把公共定义域与这两项数据一并装入命题截断。

              → Wit y s
      bodyOut y s n b hd eb he hS =
        ∣ n , ( hd
              , envOverAt-transport (b ∷ n ∷ y ∷ s ∷ []) (B ∷ n ∷ y ∷ s ∷ [])
                  i2 i1 i0 i2 i1 i0 refl refl eb he

有界全称子句按点使用：对每个 i∈n，entOut 把其满足证明转成 Ent y s i。这些条目与定义域等式及搬运后的环境条件一起，构成截断见证 Wit y s 的三个分量。

              , λ i i∈n → entOut y s n b i (hS i i∈n) ) ∣₁

向外读取整个图公式时，先消去截断见证 n，再消去截断见证 b。与它们相伴的子句分别给出定义域条件、等式 fst b ≡ fst B、环境条件和有界步骤条件；bodyOut 恰把这些数据变成 Wit y s。由于 Wit y s 本身经过命题截断，这两次消去是合法的。

    fo-out : (y s : S) → ⟨ (y ∷ s ∷ []) ⊨ fo ⟩ → Wit y s
    fo-out y s = PT.rec squash₁ (λ { (n , (hd , hb)) →
      PT.rec squash₁ (λ { (b , (eb , (he , hS))) → bodyOut y s n b hd eb he hS }) hb })

反过来，宿主层见证以 n 填入外层存在量词，以固定元素 B 填入内层存在量词。自反性证明该元素正表示所需目标，而 entIn 把每个逐点条目转回有界公式。于是，fo-out 与 fo-in 共同确立 fo 对 Wit 的充分性。

    fo-in : (y s : S) → Wit y s → ⟨ (y ∷ s ∷ []) ⊨ fo ⟩
    fo-in y s = PT.rec (snd ((y ∷ s ∷ []) ⊨ fo))
      (λ { (n , (hd , he , hS)) →
        ∣ n , ( hd , ∣ B , ( refl , he , λ i i∈n → entIn y s n i (hS i i∈n) ) ∣₁ ) ∣₁ })

固定 A 上长度为 N 的序列 g、载体元素 s，以及把 s 的底层集合认同于 g 的环境图的等式。借助这一具体表示，可以构造逐坐标像，并证明任何满足同一图公式的输出都具有相同的底层集合。

  module AtSeq (N : ℕ) (g : Ix A N) (s : S) (e : fst s ≡ fst (envS A g)) where

预期输出是逐坐标像 fg g 的环境图。在索引 j 处，它的值为 f (g j)；因此源序列与目标序列具有相同的有限长度，对应条目由输入图 E 联系。

    y₀ : S
    y₀ = envS B (fg g)

下一个引理给出构造该见证所需的基本隶属事实：每个坐标对都属于环境图。它保持为局部引理，因为本小节的公开结论是整个像环境的存在性与唯一性。

    private

条目引理说：函数的编码图包含每个自然索引与其值组成的有序对。证明由环境构造子的规格而来：该对由定义即在。

      at : {k : ℕ} (h : Fin k → V ℓ) (j : Fin k)
         → ⟨ pr (# (toℕ j)) (h j) ∈ env h ⟩
      at h j = subst ⟨_⟩ (sym (lookup-spec h j (h j))) refl

典范像满足宿主谓词 Wit：数码 nn N 记录公共定义域，he 记录 y₀ 是长度为 N、取值于 B 的环境，step 则在每个小于 N 的索引处验证关系。最后把这三条子句置于命题截断之下，只保留存在性，而不让后文依赖某个选定的分解。

    wit : Wit y₀ s
    wit = ∣ nn N , ( hd , he , step ) ∣₁
      where
      hd : ⟨ (nn N ∷ y₀ ∷ s ∷ []) ⊨ domAt i2 i0 ⟩
      hd = domAt-fill i2 i0 (nn N ∷ y₀ ∷ s ∷ []) N (vA g) (isLA g) e refl

事实 envOver B (fg g) 起初在只含 B、nn N 与 y₀ 的较短环境中陈述。运输引理把同一公式搬到还含有 s 的较长赋值；三条自反性证明表明，公式实际使用的槽位仍含有完全相同的元素。因此，加入未被该公式使用的源序列不会改变环境覆盖断言。

      he : ⟨ (B ∷ nn N ∷ y₀ ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩
      he = envOverAt-transport (B ∷ nn N ∷ y₀ ∷ []) (B ∷ nn N ∷ y₀ ∷ s ∷ [])
             i2 i1 i0 i2 i1 i0 refl refl refl (envOver B (fg g))

每个位置处的步进子句由消去数码隶属为有界自然数证明。消去的数据名指一个具体索引，其取值在两条序列中都可用。

      step : (i : S) → ⟨ fst i ∈ # N ⟩ → Ent y₀ s i
      step i i∈N = PT.map atIndex (∈#-elim N (fst i) i∈N)
        where
        atIndex : Σ[ k ∈ ℕ ] ((k < N) × (fst i ≡ # k))
                → Σ[ u ∈ S ] Σ[ v ∈ S ]

对恢复出的有限索引 j，所需条目由源值 vA g j、目标值 vB (fg g) j 与三条图隶属组成：源环境在 j 处存放前者，目标环境在该处存放后者，而 E 把前者联系到后者。可构造性证明把这两个值提升为载体 S 的元素。

                    ( ⟨ pr (fst i) (fst u) ∈ fst s ⟩
                    × ⟨ pr (fst i) (fst v) ∈ fst y₀ ⟩
                    × ⟨ pr (fst u) (fst v) ∈ fst E ⟩ )
        atIndex (k , p , ei) =
            (vA g j , isLA g j) , (vB (fg g) j , isLB (fg g) j)

环境条目引理给出前两条隶属，并沿「给定位置等于 j 的数码」这一等式运输；源环境的一项还要沿呈现等式 e 运输。图定理 f-graph 给出第三条隶属。有限索引 j 随即由上一步得到的有界自然数定义。

          , ( subst2 (λ a w → ⟨ pr a (vA g j) ∈ w ⟩) (sym qi) (sym e) (at (vA g) j)
            , subst (λ a → ⟨ pr a (vB (fg g) j) ∈ fst y₀ ⟩) (sym qi) (at (vB (fg g)) j)
            , f-graph (g j) )
          where
          j : Fin N

内部索引 j 由有界自然数的有限解码构造，数码等式由隶属运输与索引值恢复复合而成。

          j = fromℕ' N k p
          qi : fst i ≡ # (toℕ j)
          qi = ei ∙ cong #_ (sym (toFromId' N k p))

唯一性证明从任意满足 Wit y s 的候选 y 出发，目标是证明它与 y₀ 的底层集合相等。累积层级中的相等是命题，因此可以消去截断见证。展开其中三条子句后，局部模块 Only 从这些数据推出所需等式。

    only : (y : S) → Wit y s → fst y ≡ fst y₀
    only y = PT.rec (setIsSet (fst y) (fst y₀))
      (λ { (n , (hd , he , hS)) → Only.final n hd he hS })
      where
      module Only (n : S)

内部模块收集见证的三条子句：定义域条件、环境覆盖条件与每个位置处的步进子句。

                  (hd : ⟨ (n ∷ y ∷ s ∷ []) ⊨ domAt i2 i0 ⟩)
                  (he : ⟨ (B ∷ n ∷ y ∷ s ∷ []) ⊨ envOverAt i2 i1 i0 ⟩)
                  (hS : (i : S) → ⟨ fst i ∈ fst n ⟩ → Ent y s i) where

数码等式按域编码的充分性，把未知长度认同于已知长度 N。

        qn : fst n ≡ # N
        qn = domAt-numeral i2 i0 (n ∷ y ∷ s ∷ []) N (vA g) (isLA g) e hd

环境条件与恢复出的长度确定索引函数 gR : Ix B N，其环境图呈现候选 y。这个定义是不透明的，因为它的构造会消去截断数据；后续论证通过已陈述的等式使用恢复函数，而不展开这次消去。

        opaque
          gR : Ix B N
          gR = Recover.g B N (B ∷ n ∷ y ∷ s ∷ []) i2 i1 i0 qn refl he

恢复过程还证明，y 的底层集合正是 gR 生成的环境图。这个等式把见证中的任意呈现换成定长的逐坐标呈现，因此现在可以逐坐标证明唯一性。

          gR-eq : fst y ≡ fst (envS B gR)
          gR-eq = Recover.recovers B N (B ∷ n ∷ y ∷ s ∷ []) i2 i1 i0 qn refl he

在每个索引 j 处，步骤子句在命题截断下给出一个源值、一个候选目标值以及联系二者的三条图隶属。目标等式是命题，因此 PT.rec 可以把这些数据交给 read。该引理证明两个被呈现的值相等，再由 B 的呈现单射性得到 gR j ≡ fg g j。

        pt : (j : Fin N) → gR j ≡ fg g j
        pt j = ↪-inj {a = fst B} (PT.rec (setIsSet _ _) read (hS (nn (toℕ j)) j∈n))
          where
          j∈n : ⟨ # (toℕ j) ∈ fst n ⟩
          j∈n = subst (λ w → ⟨ # (toℕ j) ∈ w ⟩) (sym qn) (#mono (toℕ j) N (toℕ<n j))

读取引理陈述步进子句所供内容：两个元素与三条隶属，认同源序列中的实参、未知环境中的取值，以及经编码配对连接二者的关系事实。

          read : Σ[ u ∈ S ] Σ[ v ∈ S ]
                   ( ⟨ pr (# (toℕ j)) (fst u) ∈ fst s ⟩
                   × ⟨ pr (# (toℕ j)) (fst v) ∈ fst y ⟩
                   × ⟨ pr (fst u) (fst v) ∈ fst E ⟩ )
               → vB gR j ≡ vB (fg g) j

源实参的等式由源环境的查询规格恢复，沿认同等式运输。

          read (u , v , (hu , hv , hE)) = sym qv ∙ qv'
            where
            qu : fst u ≡ vA g j
            qu = subst ⟨_⟩ (lookup-spec (vA g) j (fst u))
                   (subst (λ w → ⟨ pr (# (toℕ j)) (fst u) ∈ w ⟩) e hu)

候选值 v 有两种刻画。由恢复环境中的查询可得 fst v ≡ vB gR j。另一方面，hE 说明 E 把恢复出的源实参联系到 v；把该实参认同为 vA g j 后，E 的单值性将这条边与 f-graph (g j) 比较，从而得到 fst v ≡ vB (fg g) j。

            qv : fst v ≡ vB gR j
            qv = subst ⟨_⟩ (lookup-spec (vB gR) j (fst v))
                   (subst (λ w → ⟨ pr (# (toℕ j)) (fst v) ∈ w ⟩) gR-eq hv)
            qv' : fst v ≡ vB (fg g) j
            qv' = svAt-out zero (E ∷ A ∷ []) sv u v (vB (fg g) j , isLB (fg g) j) hE

最后的等式复合函数图事实与反向的实参等式，完成两个像取值的认同。

                    (subst (λ w → ⟨ pr w (vB (fg g) j) ∈ fst E ⟩) (sym qu) (f-graph (g j)))

现在只需把逐坐标一致提升为两个环境图的相等。所需路径从 y 的恢复呈现出发，终止于典范图 y₀。

        final : fst y ≡ fst y₀

函数外延性把 pt 提升为两个索引函数的相等。让 envS B 沿这条路径变化即可认同两个环境图，再与 gR-eq 复合便得到 fst y ≡ fst y₀。这里的路径 lambda 直接表示环境图沿该等式的立方作用。

        final = gR-eq ∙ λ i → fst (envS B (funExt pt i))

序列集的隶属被陈述为类型，使论证能把它与每个元素并肩携带。

  Mem : S → Type (ℓ-suc ℓ)
  Mem s = ⟨ fst s ∈ˢ fst (seqL A) ⟩

表示是「长度、索引函数与认同两种呈现的等式」的截断记录。截断形式正是 seqL-out 所供给的。

  Rep : S → Type (ℓ-suc ℓ)
  Rep s = ∥ Σ[ n ∈ ℕ ] Σ[ g ∈ Ix A n ] (fst s ≡ fst (envS A g)) ∥₁

从 seqL A 中的隶属出发，seqL-out 在命题截断下给出长度 n 及相应定长环境集中的隶属。对这个 n，envSet-out 再给出截断的索引函数与呈现等式。映射这些数据，并且只向截断目标作消去，就能合并两个阶段而不选择全局表示。

  rep : (s : S) → Mem s → Rep s
  rep s m = PT.rec squash₁
    (λ { (n , hn) → PT.map (λ { (g , e) → n , g , e }) (envSet-out A n s hn) })
    (seqL-out A s m)

递归包以 seqL A 为定义域，以 fo 为图。对每个成员 s，它的一个截断表示确定典范像环境；AtSeq.wit 证明该像满足图，而 AtSeq.only 证明任何其他满足图的值都具有相同的底层集合。因此，这个图具有 mereFunct 所要求的全定义性与单值性。

  R : Recursion
  R = record
    { dom   = seqL A
    ; graph = fo
    ; funct = λ s m → mereFunct fo s (PT.map (λ { (n , g , e) →

对具体表示 (n , g , e)，函数性见证由典范像 AtSeq.y₀、它满足 fo 的证明，以及任何其他满足公式的载体元素都与它相等的证明组成。由于可构造性证明形成命题值纤维，Σ≡Prop 把底层集合的相等提升为 S 中的相等；PT.map 随后让整个构造继续处于截断之下。

        AtSeq.y₀ n g s e
        , ( fo-in (AtSeq.y₀ n g s e) s (AtSeq.wit n g s e)
          , λ y' h → Σ≡Prop (λ v → snd (isL v)) (AtSeq.only n g s e y' (fo-out y' s h)) ) })
        (rep s m)) }

递归表机制被打开，供给实际函数、其取值与取值的唯一性。

  module T = Of R using ( funct; val; val-uniq )

所得值 fn s m 是在 s 处满足 fo 的唯一载体元素。尽管它的构造从 s 的截断表示出发，唯一性保证其值不依赖于用哪个长度和索引函数表示该序列。

  fn : (s : S) → Mem s → S
  fn = T.val

只要 s 由长度 n 与索引函数 g 呈现，计算值 fn s m 就等于典范逐坐标像 AtSeq.y₀ n g s e。两者都在 s 处满足递归图，因此唯一性定理 T.val-uniq 给出该等式。后续证明由此可以从 s 的任一现有呈现出发推理。

  fn-code : (s : S) (m : Mem s) (n : ℕ) (g : Ix A n) (e : fst s ≡ fst (envS A g))
          → fn s m ≡ AtSeq.y₀ n g s e
  fn-code s m n g e =
    T.val-uniq s m (AtSeq.y₀ n g s e) (fo-in (AtSeq.y₀ n g s e) s (AtSeq.wit n g s e))

目标序列集的隶属由沿码等式运输并应用目标序列集的向内读式证明。

  into : (s : S) (m : Mem s) → ⟨ fst (fn s m) ∈ˢ fst (seqL B) ⟩
  into s m = PT.rec (snd (fst (fn s m) ∈ˢ fst (seqL B)))
    (λ { (n , g , e) → subst (λ w → ⟨ fst w ∈ˢ fst (seqL B) ⟩) (sym (fn-code s m n g e))
           (seqL-in B n (envS B (fg g)) (envSet-in B (fg g))) })
    (rep s m)

这些事实定义了从 seqL A 到 seqL B 的映射：fo 给出其图，fn 给出每个源元素处的唯一值，into 证明该值仍是 B 上的有限序列。余下任务是证明两个值相等必迫使其源序列相等。

  D : DefinableMap
  D = record
    { dom = seqL A ; cod = seqL B ; fn = fn ; into = into ; graph = fo
    ; defines = λ s m → T.funct s m .fst .snd
    ; only    = λ s m y h → sym (T.val-uniq s m y h) }

为证明单射性，先比较典范呈现即可。设两个逐坐标像环境相等，尽管它们所显示的长度可能不同。辅助引理 same 先恢复长度相等，把第二条源序列搬运到共同的有限索引类型，再逐坐标使用 f 的单射性，证明两个源环境图相等。

  private
    same : (n : ℕ) (g : Ix A n) (n' : ℕ) (g' : Ix A n')
         → fst (envS B (fg g)) ≡ fst (envS B (fg g'))
         → fst (envS A g) ≡ fst (envS A g')
    same n g n' g' q =

由 env-len，两个目标环境图的相等决定其有限长度相等，因为环境的编码定义域就是表示长度的数码。沿该等式作替换后，问题化为比较两条同以 Fin n 为索引的序列；局部类型族 P 记录对齐后尚待证明的命题。

      subst P (env-len (envS B (fg g)) (vB (fg g)) (vB (fg g')) (isLB (fg g)) (isLB (fg g')) refl q)
        base g' q
      where
      P : ℕ → Type (ℓ-suc ℓ)
      P k = (h : Ix A k) → fst (envS B (fg g)) ≡ fst (envS B (fg h))

长度相同后，env-pt 把目标图的相等读成每个索引处取值相等。B 的呈现单射性将其化为 f (g j) ≡ f (h j)，再由 f-inj 恢复 g j ≡ h j。函数外延性于是认同两个源索引函数，进而认同其环境图。

          → fst (envS A g) ≡ fst (envS A h)
      base : P n
      base h q' = λ i → fst (envS A (funExt (λ j →
        f-inj (g j) (h j) (↪-inj {a = fst B} (env-pt (vB (fg g)) (vB (fg h)) q' j))) i))

对任意成员 s 与 s'，它们的表示只在命题截断下可用。累积层级的值形成集合，因此目标等式 fst s ≡ fst s' 是命题；于是 PT.rec2 可以在局部展开两个输入各自的一个表示，并把它们交给典范呈现的比较。

  inj : (s : S) (m : Mem s) (s' : S) (m' : Mem s')
      → fst (fn s m) ≡ fst (fn s' m') → fst s ≡ fst s'
  inj s m s' m' q = PT.rec2 (setIsSet (fst s) (fst s'))
    (λ { (n , g , e) (n' , g' , e') →
        e

两个编码等式分别把实际输出 fn s m 与 fn s' m' 认同于各自的典范像环境。将这些认同与假设的输出相等复合，便得到 same 所需的前提；最后，呈现等式 e 与 e' 把所得源环境图相等转回 fst s ≡ fst s'。

      ∙ same n g n' g'
          (sym (cong fst (fn-code s m n g e)) ∙ q ∙ cong fst (fn-code s' m' n' g' e'))
      ∙ sym e' })
    (rep s m) (rep s' m')

刚证明的单射性把这条可定义映射提升为内部编码单射 seqL A ↪ seqL B。其图仍记录同一逐坐标作用；结论只保留适当编码的命题性存在。

  injL : InjL (seqL A) (seqL B)
  injL = Inj.injL D inj

导出的定理从一个实际的编码图 E 出发，它见证从 A 到 B 的单射：该图单值，定义域为 A，具有单射性，且值域包含于 B。把这四个分量交给 SeqMap，就得到从 seqL A 到 seqL B 的编码单射之命题截断存在性。该结论涵盖任意长度的有限序列，不涉及无穷序列。

seq-map : (A B E : S) → InjCode E A B → InjL (seqL A) (seqL B)
seq-map A B E (sv , dm , ij , ran) = SeqMap.injL A B E sv dm ij ran

把量化变量固定为常元

钉扎公式绑定一个存在量词以把自由槽固定到选定常元：它仅说某个值等于该常元且满足内层公式。

pinAt : ∀ {n} → S → Formula S (suc n) → Formula S n
pinAt c φ = ∃̇ ((var zero ≐ con c) ∧̇ φ)

向内读式出示该常元作为见证，以及体在扩展环境处的满足。

pin-in : ∀ {n} (c : S) (φ : Formula S (suc n)) (γ : S ^ n)
       → ⟨ (c ∷ γ) ⊨ φ ⟩ → ⟨ γ ⊨ pinAt c φ ⟩
pin-in c φ γ h = ∣ c , (refl , h) ∣₁

在向外方向，存在量词给出载体元素 z、它与 c 的底层集合相等，以及公式体在 z 处成立的证明。由于可构造性取命题值，Σ≡Prop 把底层集合相等提升为 S 中的等式 z ≡ c；沿该等式运输便得到公式体在钉扎环境中的满足。公式满足是命题，因此从命题截断作此消去是合法的。

pin-out : ∀ {n} (c : S) (φ : Formula S (suc n)) (γ : S ^ n)
        → ⟨ γ ⊨ pinAt c φ ⟩ → ⟨ (c ∷ γ) ⊨ φ ⟩
pin-out c φ γ = PT.rec (snd ((c ∷ γ) ⊨ φ))
  (λ { (z , (ez , h)) → subst (λ v → ⟨ (v ∷ γ) ⊨ φ ⟩) (Σ≡Prop (λ v → snd (isL v)) ez) h })

到固定目标的编码单射公式

InjCode F a b 由四个命题值条件组成：F 的单值性、其定义域为 a、图的单射性，以及其取值包含于 b。公式满足取命题值，最后一个条件则是取值于隶属命题的依值函数，因此它们的嵌套积仍是命题。

isPropInjCode : (F a b : S) → isProp (InjCode F a b)
isPropInjCode F a b =
  isProp× (snd ((F ∷ a ∷ []) ⊨ svAt zero))
    (isProp× (snd ((F ∷ a ∷ []) ⊨ domAt zero (suc zero)))
      (isProp× (snd ((F ∷ a ∷ []) ⊨ injAt zero))

余下的值域条件依次量化实参、取值以及图联系二者的证明，其结论是该取值属于 b。隶属是命题，故反复形成依值函数仍保持命题性，从而完成 InjCode 为命题的证明。

        (isPropΠ3 (λ _ y _ → snd (fst y ∈ fst b)))))

InjCode 对图参数与定义域参数只依赖它们所呈现的底层集合。由于可构造性证明是命题，等式 fst F ≡ fst F' 与 fst a ≡ fst a' 可唯一提升为 S 中的等式；随后二元替换把 (F , a) 上的单射码搬运到 (F' , a')，目标 b 保持不变。

injcode-resp : (F F' a a' b : S) → fst F ≡ fst F' → fst a ≡ fst a'
             → InjCode F a b → InjCode F' a' b
injcode-resp F F' a a' b qF qa = subst2 {x = F} {y = F'} {z = a} {w = a'}
  (λ E A → InjCode E A b)
  (Σ≡Prop (λ v → snd (isL v)) qF) (Σ≡Prop (λ v → snd (isL v)) qa)

公式 injFo b f B 用槽位 f 中的图与槽位 B 中的定义域表达单射码的四个条件：该图单值，定义域恰为所给集合，并且具有单射性；此外，只要它把某个实参联系到某个取值，该取值就属于固定目标 b。最后一条表达值域包含，而非到 b 的满射性。

injFo : ∀ {n} → S → Fin n → Fin n → Formula S n
injFo b f B = svAt f ∧̇ domAt f B ∧̇ injAt f
            ∧̇ ∀̇ (∀̇ (appAt (suc (suc f)) i1 i0 ⇒̇ (var i0 ∈̇ con b)))

为证明 injFo 的读法，固定目标 b、两个相关槽位 f 与 B，以及赋值 γ。局部名称 F 与 A 分别表示这两个槽位中的载体元素。后续论证于是可以把结论直接陈述为 InjCode F A b，不让变量查询的簿记遮蔽数学内容。

module InjFo {n : ℕ} (b : S) (f B : Fin n) (γ : S ^ n) where
  private
    F A : S
    F = lookup f γ
    A = lookup B γ

读取引理把单射公式的满足转换为单射码的四条性质。对定义域条款，输入的图见证从命题截断消去到「该输入属于 A」这一命题；反过来，A 中的隶属给出所需的定义域见证。

  read : ⟨ γ ⊨ injFo b f B ⟩ → InjCode F A b
  read (sv , dm , ij , ran) =
      svAt-in zero (F ∷ A ∷ []) (λ x y y' p q → svAt-out f γ sv x y y' p q)
    , domAt-intro zero (suc zero) (F ∷ A ∷ []) (λ x →
          (λ h → PT.rec (snd (fst x ∈ fst A))

单值性与单射性通过如下方式搬运：先在 γ 处读出各自的语义条款，再为二元环境 (F,A) 重建相应条款。值域条件利用应用的充分性，把 F 中的图隶属转换为公式所需的应用原子，随后公式的末条款给出该值属于固定目标 b。

                   (λ { (y , p) → domAt-out f B γ dm x y p }) h)
        , (λ hx → domAt-in f B γ dm x hx))
    , injAt-in zero (F ∷ A ∷ []) (λ y x x' p q → injAt-out f γ ij y x x' p q)
    , λ x y p → ran x y (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) i1 i0 (y ∷ x ∷ γ))) p)

填充引理是反向构造：由编码单射的四份数据构造单射公式的满足，这次是在公式陈述所在的那个结构上读取所有原子。

  fill : InjCode F A b → ⟨ γ ⊨ injFo b f B ⟩
  fill (sv , dm , ij , ran) =
      svAt-in f γ (λ x y y' p q → svAt-out zero (F ∷ A ∷ []) sv x y y' p q)
    , domAt-intro f B γ (λ x →
          (λ h → PT.rec (snd (fst x ∈ fst A))

对于全域性，截断的图见证只被消去到「输入属于 A」这一命题，而 A 中的隶属则在反方向提供见证。其余条款在 γ 处重建单值性与单射性，并由应用的充分性把值域假设转换为公式的末条款。因此，read 与 fill 给出公式满足和单射码四项条件之间的两个方向。

                   (λ { (y , p) → domAt-out zero (suc zero) (F ∷ A ∷ []) dm x y p }) h)
        , (λ hx → domAt-in zero (suc zero) (F ∷ A ∷ []) dm x hx))
    , injAt-in f γ (λ y x x' p q → injAt-out zero (F ∷ A ∷ []) ij y x x' p q)
    , λ x y p → ran x y (subst ⟨_⟩ (appAt-adequate (suc (suc f)) i1 i0 (y ∷ x ∷ γ)) p)

把无穷层计数归约到 L_ω

无穷序数 ω 处的层被呈现为可构造集合：序数层 Lset ω 连同其序数性由层呈现打包。

Lω : S
Lω = LsetS ω ω-ord

本节的目标随之陈述为一个类型：从 Lset ω 的可构造呈现到内部 ω 的内部编码单射。这是更大层级计数所依赖的基底情形。

LimitStageCounted : Type (ℓ-suc ℓ)
LimitStageCounted = InjL Lω ωʟ

搬运引理沿源与目标底层集合的等式搬运内部编码单射。源等式给出从新源 a' 到旧源 a 的包含；应用给定单射后，目标等式再给出从旧目标 b 到新目标 b' 的包含。复合这三条单射便得到 InjL a' b'。

move : (a a' b b' : S) → fst a ≡ fst a' → fst b ≡ fst b' → InjL a b → InjL a' b'
move a a' b b' qa qb h =
  injl-trans a' a b' (inclusion-coded a' a (λ z hz → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym qa) hz))
    (injl-trans a b b' h (inclusion-coded b b' (λ z hz → subst (λ w → ⟨ z ∈ˢ w ⟩) qb hz)))

基础计数：L_ω 单射到 ω

排除论证处理形如 Lset (# n) 的有限层，并从取该有限层的名册开始：即其成员的一个带索引枚举。

private
  module FinNo (n : ℕ) where
    t : Tally (finiteStage n)
    t = StageOrder.tally (stageOrder n)

名册供给其大小、每个索引处的成员，以及「每个成员都出现在某个索引处」的覆盖事实。

    open Tally t using ( size; item; onto )

搜索引理为成员命名：对有限层的每个成员 x，它在有限多个索引上运行可判定搜索，用排中律逐项比较条目与 x，返回条目等于 x 的某索引。搜索返回的是某个索引；并不主张该索引唯一，而且这是对有限族的有限判定，不是诉诸任何选择原理。

    named : (x : V ℓ) → ⟨ x ∈ˢ finiteStage n ⟩ → Σ[ i ∈ Fin size ] (item i ≡ x)
    named x hx = decRec (λ q → q) (λ nq → Empty.rec (PT.rec Empty.isProp⊥ nq (onto x hx)))
      (DecΣ size (λ i → item i ≡ x)
        (λ i → Sum.rec yes no (lem ((item i ≡ x) , setIsSet (item i) x))))

假设 f 把 ω 的呈现单射到某个有限层。每个值 f x 都可取得一个名册索引 q x；把该索引复制成 x ↦ (q x,q x)，便得到有限排除定理所需的映射。这些索引对相等会迫使相应的 f 值相等，再由 f 的单射性迫使原输入相等。

    noinj : (f : ⟪ ω ⟫ → ⟪ Lset (# n) ⟫)
          → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → Empty.⊥
    noinj f finj = finite-excl-ω (# size) (numeral-ord size) (#∈ω size)
      (λ x → q x , q x) (λ x y e → finj x y (qq x y (cong fst e)))
      where

辅助映射把 f 的每个值读作外围元素，证明它属于该有限层，并用上一步找到的有限索引为其命名。

      vl : ⟪ ω ⟫ → V ℓ
      vl x = ⟪ Lset (# n) ⟫↪ (f x)
      mm : (x : ⟪ ω ⟫) → ⟨ vl x ∈ˢ finiteStage n ⟩
      mm x = member (Lset (# n)) (f x)
      q : ⟪ ω ⟫ → ⟪ # size ⟫

映射 q 把选出的名册索引转换为有限序数呈现 ⟪# size⟫ 中的相应元素。若两个这样的名字相等，该呈现的单射性使其自然数索引相等，因而两项名册条目相等。随后，Lset (# n) 的呈现把这一外围等式转回 f 的两个值相等。

      q x = fromFin size (toℕ (named (vl x) (mm x) .fst) , toℕ<n (named (vl x) (mm x) .fst))
      qq : (x y : ⟪ ω ⟫) → q x ≡ q y → f x ≡ f y
      qq x y e = ↪-inj {a = Lset (# n)}
        (sym (named (vl x) (mm x) .snd)
          ∙ cong item (inj-toℕ (cong fst (fromFin-inj size _ _ e)))

同一视链以第二点的被命名条目闭合，完成「名字相等迫使值相等」的证明。

          ∙ named (vl y) (mm y) .snd)

对任意指标 w，NoInto w 是这样一个命题：不存在从 ω 的呈现到 Lset w 的呈现的宿主层单射。下一条引理将在附加假设 w∈ω 下证明这一命题。

  NoInto : V ℓ → Type ℓ
  NoInto w = (f : ⟪ ω ⟫ → ⟪ Lset w ⟫)
           → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → Empty.⊥

一般形式沿 g 在 ω 中的隶属搬运有限情形而得：ω 的成员仅仅是某个数码，该搬运把整条排除陈述移至该数码的层。由于目标是矛盾命题，消去合法。

  no-inj-fin : (g : V ℓ) → ⟨ g ∈ˢ ω ⟩ → NoInto g
  no-inj-fin g g∈ω = PT.rec (isPropΠ2 (λ _ _ → Empty.isProp⊥))
    (λ { (k , e) → subst NoInto e (FinNo.noinj (lower k)) }) g∈ω

无穷序数 ω 是可构造的：其序数性供给序数层构造。

hω : ⟨ isL ω ⟩
hω = isL-ord ω ω-ord

Lset ω 的层序被实现为 L 内部由编码对构成的可构造集合 Rω。

Rω : SL.S
Rω = relL ω hω ω-ord

关系规格说明：Rω 的编码对恰是由层序关联的 L 元素构成的有序对。

specω : IsRel ω Rω
specω = relL-spec ω hω ω-ord

端点条件从每个相关对中恢复两个端点的层隶属。展开编码对会得到 Lset ω 的两个成员，而分量等式把它们的底层集合分别认同于端点 y 与 x。

Rsub : (y x : SL.S) → Holds Rω y x
     → ⟨ fst y ∈ˢ Lset ω ⟩ × ⟨ fst x ∈ˢ Lset ω ⟩
Rsub y x h = PT.rec isP
  (λ { (_ , h₁) → PT.rec isP
    (λ { (a , h₂) → PT.rec isP

两个隶属沿有序对编码的单射性所供给的两条分量等式搬运。

      (λ { (b , (q , _)) →
             subst (λ w → ⟨ w ∈ˢ Lset ω ⟩) (sym (pr-inj q .fst)) (a .snd)
           , subst (λ w → ⟨ w ∈ˢ Lset ω ⟩) (sym (pr-inj q .snd)) (b .snd) })
      h₂ })
    h₁ })

两个隶属的合取是命题；编码对的关联性由可构造有序对处的关系规格产出。

  rel
  where
  isP : isProp (⟨ fst y ∈ˢ Lset ω ⟩ × ⟨ fst x ∈ˢ Lset ω ⟩)
  isP = isProp× (snd (fst y ∈ˢ Lset ω)) (snd (fst x ∈ˢ Lset ω))
  rel : ⟨ Related ω (pr (fst y) (fst x)) ⟩

关联性沿「编码对与两个底层集的朴素有序对」的同一视搬运。

  rel = subst (λ w → ⟨ Related ω w ⟩) (prʟ-fst y x)
    (specω (prʟ y x) .fst
      (subst (λ w → ⟨ w ∈ˢ fst Rω ⟩) (sym (prʟ-fst y x)) h))

序型机制在层 Lset ω 处、以内部关系及其端点条件实例化：由此固定小定义域、内部关系，以及上一章的塌缩构造。

module OT = Code Lω Rω Rsub using ( module Conjuncts; Dom; _≺_; isProp≺; ≺-in; ≺-out )

宿主良序是搬到 Lset ω 的呈现上的层序，于是抽象良序机制可用于该小索引类型。

Wω : SWO ⟪ Lset ω ⟫
Wω = carry (Lset ω) (orderAt ω ω-ord)

把该良序在 Lset ω 的呈现上给出的严格比较记作 a <ω b。下面两条引理证明，此关系与内部编码的前驱关系 a OT.≺ b 表达同一个比较。

open SWO Wω using () renaming ( _<∙_ to _<ω_ )

内部关系与宿主层序在共同呈现上相符。第一个方向利用编码关系的表示定理，把内部前驱证明 a OT.≺ b 读为宿主序比较 a <ω b。

≺→< : (a b : OT.Dom) → a OT.≺ b → a <ω b
≺→< a b k = ixRel-rep ω ω-ord Rω specω a b (OT.≺-out a b k)

反过来，编码关系的填充定理把宿主序比较 a <ω b 转换为内部前驱证明 a OT.≺ b。借助这两个方向，宿主关系的序论性质可以搬运到内部关系。

<→≺ : (a b : OT.Dom) → a <ω b → a OT.≺ b
<→≺ a b k = OT.≺-in a b (ixRel-fill ω ω-ord Rω specω a b k)

内部关系的良基性由宿主序的良基性得出。可达性逐点搬运：内部关系中的每个前驱先被转换为宿主前驱。

wfω : WellFounded OT._≺_
wfω m = go (SWO.wf∙ Wω m)
  where
  go : {n : OT.Dom} → Acc _<ω_ n → Acc OT._≺_ n
  go {n} (acc r) = acc (λ n' k → go (r n' (≺→< n' n k)))

内部关系的传递性同样经宿主序搬运：两个相邻的内部步先转换、再复合、最后转回。

transω : {a b c : OT.Dom} → a OT.≺ b → b OT.≺ c → a OT.≺ c
transω {a} {b} {c} k k' =
  <→≺ a c (SWO.trans∙ Wω a b c (≺→< a b k) (≺→< b c k'))

对任意 a 与 b，宿主良序的三分法给出三种形式之一：a <ω b、二者相等或 b <ω a。结论写成嵌套和，使每个比较都能转换为内部关系的对应情形。

triω : (a b : OT.Dom) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
triω a b = go (SWO.tri∙ Wω a b)
  where
  go : TriW (a <ω b) (a ≡ b) (b <ω a)
     → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))

宿主的每种情形都被转换回相应的内部情形：小于、相等或大于。

  go (lt h) = inl (<→≺ a b h)
  go (eq e) = inr (inl e)
  go (gt h) = inr (inr (<→≺ b a h))

良基性与传递性现在给出塌缩值及其序数像 otL。三分法证明不同点具有不同塌缩值，因此塌缩图 colTable 满足单射性条款，并给出下文所用的编码。

module C = OT.Conjuncts wfω transω using ( module Inj; col; col-ord; col-out; colTable; otL; otL-out )
module I = C.Inj triω using ( code; col-inj )

诞生层族在内部 ω 处实例化：Lset ω 的每个被呈现成员在 ω 中有一个诞生层，族关系对其排序。

private
  module F = Family ω (λ δ _ → orderAt δ) ω-ord using ( _≺_; bornAt )

证明族关系的展开读法：在 ω 处，抽象陈述的序等于具体的「先生于后步进」之序。

  unfoldω : (a b : MemOf (Lset ω))
          → relOf (orderAt ω ω-ord) a b ≡ F._≺_ a b
  unfoldω a b = cong (λ z → relOf (z ω-ord) a b) (orderAt-step ω)

成员的诞生层被读作外围集合。

  bAt : MemOf (Lset ω) → V ℓ
  bAt a = F.bornAt a .fst

每个诞生层都属于内部 ω，因为整个族都在 ω 之下。

  bAt∈ω : (a : MemOf (Lset ω)) → ⟨ bAt a ∈ˢ ω ⟩
  bAt∈ω a = F.bornAt a .snd

每个诞生层都是序数：它是序数 ω 的成员，而序数的成员是序数。

  bAt-ord : (a : MemOf (Lset ω)) → IsOrd (bAt a)
  bAt-ord a = mem-ord {A = ω} ω-ord (bAt a) (bAt∈ω a)

Lset ω 的每个被呈现成员都属于以其诞生层后继为指数的层：该成员的可构造性被搬运进该后继层。

  self-at : (a : MemOf (Lset ω)) → ⟨ a .fst ∈ˢ Lset (sucV (bAt a)) ⟩
  self-at a = birth-mem (a .fst) (Lset→isL ω ω-ord (a .fst) (a .snd))

步进界说：若 a 在族序中先于 b，则 a 的底层集属于以「b 的诞生层加一」为指数的层。在诞生层严格更早的情形，后继比较由序数线性性判定。

  step-bound : (a b : MemOf (Lset ω)) → F._≺_ a b
             → ⟨ a .fst ∈ˢ Lset (sucV (bAt b)) ⟩
  step-bound a b (inl h) =
    raise (suc∈or≡ (bAt a) (bAt b) (bAt-ord a) (bAt-ord b) h)
    where

在诞生层严格较早的分支中，序数的离散性直接比较 sucV (bAt a) 与 bAt b。无论该后继仍低于 bAt b，还是恰与之相等，层单调性都把已知的 a∈Lset (sucV (bAt a)) 搬入 Lset (sucV (bAt b))。

    raise : ⟨ sucV (bAt a) ∈ˢ bAt b ⟩ ⊎ (sucV (bAt a) ≡ bAt b)
          → ⟨ a .fst ∈ˢ Lset (sucV (bAt b)) ⟩
    raise (inl k) = Lset-mono {α = sucV (bAt b)} {β = sucV (bAt a)}
      (∈sucV-inl {A = bAt b} {x = sucV (bAt a)} k) (self-at a)
    raise (inr e) = Lset-mono {α = sucV (bAt b)} {β = sucV (bAt a)}

在等式子情形 sucV (bAt a) ≡ bAt b 中，证明先把该序数置于 bAt b 的后继中，再应用层单调性。另一个主分支中两个诞生层相等；此时步进序见证本身就包含 a 属于其公共诞生层的后继层，沿该等式搬运便得到所述界。

      (subst (λ w → ⟨ sucV (bAt a) ∈ˢ sucV w ⟩) e (self∈sucV (sucV (bAt a))))
      (self-at a)
  step-bound a b (inr (e , u)) =
    subst (λ w → ⟨ a .fst ∈ˢ Lset (sucV w) ⟩) (sym e) (u .fst)

内部塌缩定义域的每个点都被读作 Lset ω 的被呈现成员。

  atIx : OT.Dom → MemOf (Lset ω)
  atIx m = ⟪ Lset ω ⟫↪ m , memOf (Lset ω) m

对塌缩定义域中的点 p，护卫指标 gOf p 是 p 所表示成员的诞生层后继。有限层 Lset (gOf p) 将包含 p 的每个前驱。

  gOf : OT.Dom → V ℓ
  gOf p = sucV (bAt (atIx p))

每个护卫层都属于内部 ω，因为它是 ω 中某成员的后继。

  gOf∈ω : (p : OT.Dom) → ⟨ gOf p ∈ˢ ω ⟩
  gOf∈ω p = ω-limit (bAt (atIx p)) (bAt∈ω (atIx p))

前驱界说：点 p 的每个前驱 r 都呈现由 p 的护卫层所界定层的一个外围元素。证明把步进界穿过族序的展开读法搬运。

  seg-bound : (p r : OT.Dom) → r OT.≺ p
            → ⟨ ⟪ Lset ω ⟫↪ r ∈ˢ Lset (gOf p) ⟩
  seg-bound p r k =
    step-bound (atIx r) (atIx p) (transport (unfoldω (atIx r) (atIx p)) (≺→< r p k))

前驱段记录 p 的一个前驱 r，连同其塌缩值与给定集合的同一视。

private
  Seg : OT.Dom → V ℓ → Type (ℓ-suc ℓ)
  Seg p b = Σ[ r ∈ OT.Dom ] ((r OT.≺ p) × (C.col r ≡ b))

前驱段是命题：塌缩在小定义域上单射、关系取值于命题、底层集合构成 h-集合，三者合起来把塌缩值相同的两条记录等同。

  isPropSeg : (p : OT.Dom) (b : V ℓ) → isProp (Seg p b)
  isPropSeg p b (r , _ , e) (r' , _ , e') =
    Σ≡Prop (λ z → isProp× (OT.isProp≺ z p) (setIsSet _ _))
      (I.col-inj r r' (e ∙ sym e'))

塌缩值中的每个隶属都给出一个前驱段：塌缩的截断读取被消去到取值于命题的段中。

  seg : (p : OT.Dom) (b : V ℓ) → ⟨ b ∈ˢ C.col p ⟩ → Seg p b
  seg p b h = PT.rec (isPropSeg p b) (λ z → z) (C.col-out p b h)

现在只须证明每个序数 C.col p 都低于 ω。序数三歧留下两种阻碍情形：它等于 ω，或 ω 属于该塌缩。二者都会推出同一个包含 ω ⊆ C.col p，因此先证明这一包含会迫使一个不可能的单射进入有穷层 Lset (gOf p)。

col-fin : (p : OT.Dom) → ⟨ C.col p ∈ˢ ω ⟩
col-fin p = go (ord-tri (C.col p) (C.col-ord p) ω ω-ord)
  where
  refute : ((z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ C.col p ⟩) → Empty.⊥
  refute sub = no-inj-fin (gOf p) (gOf∈ω p) f f-inj