BedrockL 内部的极限层序
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图Lset ω 的诸成员在外部已经带有严格良序。本章的问题是：怎样让 L内部的公式使用这个比较？答案要依次经过三种彼此有别的形态：元层面的比较、对象语言中对该比较的描述，以及在有穷层描述已经给出后实现该关系的可构造集合。
{-# OPTIONS --cubical --safe --guardedness #-}
本章的全部构造都相对于层级 ℓ-suc ℓ 上一个显式的排中律实例。前文已用这条假设取得极限层成员首次出现的最小有穷层，本章还把同一实例传给所用的分离结果与取界结果。它在这些构造需要时判定命题，却不为任意集合族提供选择函数。
open import Base.Prelude open import Base.Classical using ( LEM )
固定宇宙层级 ℓ 与刚才说明的排中律实例。此时后文的内部关系仍是条件式构造：只有给出描述有穷层序的公式及其两个语义方向后，它才在模块 Described 内部得到定义。下一章会提供这个实例，并把 codeOrder 公开给后续构造使用。
module L.Choice.LimitStageOrder {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
对象语言必须描述比较，同时不把语法与它在层级中的意义混为一谈。公式使用变元、常元、隶属、联结词与量词；由于常元域就是可构造载体，一个常元已经指称某个确定的可构造集合。后文所需的两个基本检验由编码引理提供。有序对的等式决定两个分量，数码编码也是单射的，而 #mono 把 k < m 变为 # k 属于 # m。因此，集合论隶属能够忠实承载有穷指标的严格比较。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_; _∨̇_; ¬̇_; _⇒̇_; ∃̇_; ∀̇_; ∀̇∈ ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′ )
这里采用的结构是可构造宇宙。其载体元素把一个集合与可构造性证据打包在一起，而传递性又为该集合的每个成员提供同类证据。这样，普通层级隶属中的见证便能进入对象语言的环境。特别地，finiteStage n 是 Lset (# n)，极限层则是 Lset ω；关于数码与序数的事实使这些指标始终区别于它们所指名的层。经过包装的层与常元 ωʟ 随后使公式能够从结构内部谈论这条层级。
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd ) open import L.Ordinal {ℓ} using ( numeral-ord; #∈ω; ∈#-elim; #∈#-elim; ω-ord ) open import L.Axioms.Basic {ℓ} using ( LsetS ) open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
三座桥把语义上的比较变成 L 的一个集合。首先，smallDom 把一个小族放进同一个可构造集合，却不声称这个界恰好等于该族的像。其次，分离从这样的界中精确取出满足一元公式的元素。最后，描述有序对、关系隶属与层级序列的编码公式都带有充分性定律，把满足关系翻译成相应的集合事实。这三件工具把寻找公共定义域与在该域上陈述精确关系这两个问题分开处理。
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL ) open import L.Recursion {ℓ} lem using ( smallDom ) open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; prAtL; prAtL-adequate; prʟ; prʟ-fst ) open import L.Coding.Expressions {ℓ} using ( numL ) open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt )
要表示的比较在外部已经定义。到了后继层，before (suc n) 用 before n 排列更早的点，并在最先分歧处比较 finiteStage n 的两个子集。precedes R A x y 的见证属于 A，属于 y 而不属于 x，并记录 x 与 y 在每个更早点处一致；该见证的存在带有命题截断。类型 Limit 打包 Lset ω 的成员，而它们的最小出现层号构成 limitOrder 的主键；只有层号相同才调用相应的 before 比较。所得关系集的两个表示方向，形状正好符合 Adequacy.Keys 的要求。
open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines ) open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; level; level-in; levelData; limitOrder ; before; precedes; Agrees; Witness; finiteStage ) open import L.Choice.NameComparison {ℓ} lem using ( module Adequacy )
limitOrder 以 SWO 束的形式给出：除比较本身外，还包含三歧性、非自反性、传递性与良基性。内部化论证不会重新证明这些定律。后文只为一个特定目的使用前三条：从对象语言析取读回时只能先得到带命题截断的严格比较，三歧性指出可能的分支，非自反性与传递性则排除不相容的分支。
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; Tri; lt; eq; gt )
极限比较具有后文所需的字典序形状。第一支说第一个成员的层号更小；第二支说双方层号相同，并在共同层号处用 before 比较底层集合。自然数的三歧分析第一把键，subst2 则在等式识别出编码层号或端点时运输二元关系。与之相伴的 Lift 与 lower 只处理宇宙层级，其中 lower 对应命题降级；它们都不消除命题截断。
import FOL.Absoluteness open import Cubical.Data.Sum using ( _⊎_; inl; inr ) open import Cubical.Foundations.Prelude using ( subst2 ) open import Cubical.Data.Nat.Order using ( _<_; _≟_ ) import Cubical.Data.Nat.Order as NatOrder
对象语言的存在量词与析取分别解释为带命题截断的存在与分支选择。因此，只有当目标是命题时才能使用其中的见证，例如不可能性、层级集合的等式或另一项命题截断。这不表示本章每个存在类型都带命题截断：当类型要求显式数据时，打包后的载体元素与公共界之类的数据仍然可见。从命题截断恢复严格比较也不是消除命题截断的一般原则；它专门依赖 limitOrder 的三歧性与序定律。
import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Properties
为了应用取界引理，Lset ω 的成员需要一个小索引类型。纤维 ⟪ Lset ω ⟫ 提供这种指标，而 ∈-asFiber 把给定的成员证明变成一个指标，其像就是原来的成员。因此，两个这种纤维的积索引了极限层成员的所有有序对。后文的 pairsBound 会包含这些对中的每一个；精确性要到分离以后才得到。
using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈∈ₛ; ∈ₛ⟪_⟫↪_ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_; ω )
现在有三种隶属记号，各自承担不同角色。对载体元素，x ∈ˢ y 是可构造结构中取命题值的隶属；对底层的层级集合，fst x ∈ fst y 使用外围隶属；在公式内部，_∈̇_ 只是句法上的隶属原子。下一步引入的满足关系把第三种形式解释成前两种。分清这些层次，就不会把描述一个序的公式误当成「其实现集合在内部已被证明为良序」。
open hPropStructure 𝒮ʟ
判断 _⊨_ 是把外围层级结构限制到可构造类后得到的内层满足关系。它的载体由集合及其可构造性证据组成，因此常元与量化取值都遍及可构造对象。原子隶属通过第一投影解释，而传递性保证可构造界的成员仍能包装成载体元素。于是，满足关系在对象语言公式与其底层集合的普通隶属事实之间给出精确的桥梁。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
把 limitOrder 携带的比较记作 _≺ˡ_。它先按最小出现层号比较两个极限层成员；层号相同，再按共同有穷层中的最先分歧比较。接下来的目标是条件式的：假设有一条对象语言公式在预定定义域上表示每个有穷层的 before 关系，便在 Described 内部构造集合 codeOrder，使 u 与 v 的有序对属于它当且仅当 u ≺ˡ v。下一章会给出所需的有穷层公式，从而得到可实际使用的实例。
open SWO limitOrder using () renaming ( _<∙_ to _≺ˡ_ )
约束变元用 de Bruijn 位置表示。打开两个嵌套的绑定后，外围环境中的每个位置都要越过两个新条目，sh2 正好记录这次移位。最先分歧公式先绑定候选分歧点、再绑定其下的点时会用到它；不同层号分支绑定两个层号数码时也会用到它。移位只改变既有自由变元的寻址方式，不改变该变元所指称的集合或关系。
private sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i)
环境包含的是可构造载体的元素，而不是未包装的层级集合。因此，对自然数 k，towerS k 把层 Lset (# k) 与其可构造性证据打包在一起。该定义保持不透明，使后续证明通过公开的投影等式使用它，而不展开层级构造。不透明性只控制归约，不会增加任何数学假设。
opaque towerS : ℕ → S towerS k = LsetS (# k) (numeral-ord k)
等式 towerS-fst k 把这个载体元素的底层集合认同为 Lset (# k)。它连接同一层的两种视角：公式接收包装后的元素 towerS k，外部层级引理则陈述底层层级集合中的隶属。后续证明在这两种视角之间运输成员事实时，都会经过这条等式。
towerS-fst : (k : ℕ) → fst (towerS k) ≡ Lset (# k) towerS-fst k = refl
指标自身还需要一个单独的载体元素。numS k 把数码 # k 与其可构造性证据打包。把 numS k 与 towerS k 分开可避免一种常见混淆：前者指称序数指标，后者指称由它索引的可构造层。LevelAt 将通过层级序列的描述把这两个对象联系起来。
numS : ℕ → S numS k = # k , numL k
投影等式 numS-fst k 从包装后的数码中恢复 # k。它与 towerS-fst k 配合，使同一个自然数能够协调地承担两种角色：一方面作为环境中的层号取值，另一方面作为见证所展示之层的指标。这两条等式为对象语言取值与外部的数码、层事实之间的运输提供依据。
numS-fst : (k : ℕ) → fst (numS k) ≡ # k numS-fst k = refl
设环境位置 i 的底层集合是 # j。引理 towerGraph 把 towerS j 放进新位置，并证明 LsetGraphAt 联系这两个位置。它的内容恰是层级序列的规格：与数码 # j 对应的取值是层 Lset (# j)。因此，同一条引理既为真实层号处的存在性提供塔见证，也为用该层检验最小性提供塔见证。
towerGraph : ∀ {n} (j : ℕ) (δ : S ^ n) (i : Fin n) → fst (lookup i δ) ≡ # j → ⟨ (towerS j ∷ δ) ⊨ LsetGraphAt zero (suc i) ⟩ towerGraph j δ i q = Lset-defines zero (suc i) (towerS j ∷ δ) (subst IsOrd (sym q) (numeral-ord j)) (towerS-fst j ∙ cong Lset (sym q))
层号，在内部说出
公式 LevelAt b x 开始刻画第一把键。它先要求位置 b 的取值属于 ω，因而可解码为数码；随后要求存在一个由 LsetGraphAt 在该数码处描述的取值，并要求位置 x 的取值属于所得的层。这些子句说明 b 是 x 的一个出现层；余下的子句将说明它还是最小的出现层。
LevelAt : ∀ {n} → Fin n → Fin n → Formula S n LevelAt b x = (var b ∈̇ con ωʟ) ∧̇ ( ∃̇ ( LsetGraphAt zero (suc b) ∧̇ (var (suc x) ∈̇ var zero) ) ∧̇ ∀̇∈ (var b) (∀̇ ( LsetGraphAt zero (suc zero)
最小性遍及候选数码 b 的每个成员 u，而不只检查它的直接前驱。对每个在这样的u 处被描述出来的层，位置 x 的取值都不得属于该层。由于 # k 的成员恰是更小的数码，候选 b = # k 因而排除了从 0 到 k-1 的所有层。两个嵌套绑定解释了 x 的移位。语义上，这些全称子句是函数类型；附近对数码成员的命题截断解码只在命题目标下使用，并不会选定一个更小指标。
⇒̇ ¬̇ (var (sh2 x) ∈̇ var zero) )) )
为证明 LevelAt 的两个读法，固定一个真实的极限层成员 a、一个自然数 k，以及把 k 认同为其最小出现层号的等式 qk : level a ≡ k。把 levelData a 的正面分量沿 qk 运输，便得到 aIn：a 的底层集合属于 Lset (# k)。负面分量则说，对任何 m < k，它不可能属于 Lset (# m)。这恰是证明公式识别真实层号所需的存在性与最小性事实；随后还会用它们证明公式识别出的任何层号都等于 # k。
module Level (a : Limit) (k : ℕ) (qk : level a ≡ k) where private aIn : ⟨ fst a ∈ Lset (# k) ⟩ aIn = subst (λ j → ⟨ fst a ∈ Lset (# j) ⟩) qk (level-in a)
levelData a 的第二个投影给出后续论证所需的最小性。若 a 的底层集合已经属于 Lset (# m)，且 m < k，等式 qk 就把后一条不等式化为 m < level a，与该最小性矛盾。levelData 所需的比较位于更高一层宇宙，因此这里用 lift 包装它。这只是宇宙层级的调整，不涉及命题截断。
aMin : (m : ℕ) → ⟨ fst a ∈ Lset (# m) ⟩ → m < k → Empty.⊥ aMin m h hm = levelData a .snd .snd m h (lift (subst (λ j → m < j) (sym qk) hm))
LevelAt 的两条读式都在任意环境的任意位置 b 与 x 上证明。为了向外读取公式，先为存在量词所隐藏的信息命名会很方便：一个载体元素c 在 b 的值处满足层级图，并且 x 的值属于 c 的底层集合。私有类型 Body 恰好就是施加命题截断之前的这份见证数据。
module _ {n : ℕ} (b x : Fin n) (γ : S ^ n) where private Body : S → Type (ℓ-suc ℓ) Body c = ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩ × ⟨ fst (lookup x γ) ∈ fst c ⟩
向内读取时，设 b 表示数码 # k，而 x 表示 a 的底层集合。结论包含 LevelAt 的三个部分：b 的值属于 ω；b 处有一个层级取值包含 x 的值；由 b 的成员所索引的每个层级取值都不包含它。证明把这三部分分别命名为 hω、hex 与 hmin，从而分开建立存在性与最小性。
LevelAt-in : fst (lookup b γ) ≡ # k → fst (lookup x γ) ≡ fst a
→ ⟨ γ ⊨ LevelAt b x ⟩
LevelAt-in qb qx = hω , (hex , hmin)
where
hω : ⟨ fst (lookup b γ) ∈ ω ⟩
第一部分来自每个数码都属于 ω 这一基本事实。等式 qb 把位置 b所存的值与 # k 认同；沿该等式的反向运输 #∈ω k，便得到所需的成员证明。这次运输把关于显式数码的事实接到关于环境位置的同一事实上。
hω = subst (λ u → ⟨ u ∈ ω ⟩) (sym qb) (#∈ω k)
对于存在部分，取包装后的有穷层 towerS k 为见证。引理 towerGraph 借助 qb 证明这个见证就是 b 处的层级取值。由 towerS-fst k，其底层集合是 Lset (# k)，所以只需再用 qx 对齐端点，即可应用已知的成员事实 aIn。
hex : ⟨ γ ⊨ ∃̇ ( LsetGraphAt zero (suc b) ∧̇ (var (suc x) ∈̇ var zero) ) ⟩ hex = ∣ towerS k , (towerGraph k γ b qb , hm) ∣₁ where hm : ⟨ fst (lookup x γ) ∈ fst (towerS k) ⟩ hm = subst (λ u → ⟨ fst (lookup x γ) ∈ u ⟩) (sym (towerS-fst k))
事实 aIn 已经说明 a 的底层集合属于 Lset (# k)。沿 qx 的反向运输，把其中的成员从 a 的底层集合改成 x 处的值。再与前面的投影运输合并，便证明了 hm，并在命题截断之下完成存在见证。
(subst (λ u → ⟨ u ∈ Lset (# k) ⟩) (sym qx) aIn)
这个有界全称表达全局最小性。给定 b 的值中的成员 u、一个在 u 处满足层级图的候选 c，以及一份声称 x 的值属于 c 的证明，目标是导出矛盾。用 qb 把 u 的成员身份改写到 # k 后，∈#-elim 在命题截断之下给出某个 m < k，使 u 等于 # m。由于目标是空类型，因而是命题，可以消去这个命题截断。所得矛盾只为匹配对象语言否定所在的宇宙层级而被抬升。
hmin : ⟨ γ ⊨ ∀̇∈ (var b) (∀̇ ( LsetGraphAt zero (suc zero) ⇒̇ ¬̇ (var (sh2 x) ∈̇ var zero) )) ⟩ hmin u u∈ c hg hmem = lift (PT.rec Empty.isProp⊥ step (∈#-elim k (fst u) (subst (λ w → ⟨ fst u ∈ w ⟩) qb u∈))) where
固定一次显式解码，得到 m < k 与 fst u ≡ # m。图证明 hg 不仅说明 c 是某个可能的见证；把数码 # m 的序数证明运输过去后，Lset-only 会把 c 的底层集合认同为 Lset (fst u)。因此，公式不能在存在见证后藏入任意集合，层级图会确定相应的有穷层。
step : Σ[ m ∈ ℕ ] ((m < k) × (fst u ≡ # m)) → Empty.⊥ step (m , (hm , qu)) = aMin m inStage hm where qc : fst c ≡ Lset (fst u) qc = Lset-only zero (suc zero) (c ∷ u ∷ γ) hg
现在沿三条认同运输那份假设的成员证明。先由 qc 把 x 的值放入 Lset (fst u)，再由 qx 把该值替换为 a 的底层集合，最后由 qu 把 fst u 替换为 # m。所得结论是 fst a ∈ Lset (# m)；当 m < k 时，这正是 aMin 所排除的陈述。因此，没有由小于 k 的数码索引的有穷层包含 a。
(subst IsOrd (sym qu) (numeral-ord m)) inStage : ⟨ fst a ∈ Lset (# m) ⟩ inStage = subst (λ w → ⟨ fst a ∈ Lset w ⟩) qu (subst (λ w → ⟨ w ∈ Lset (fst u) ⟩) qx (subst (λ w → ⟨ fst (lookup x γ) ∈ w ⟩) qc hmem))
向外读取时，假设 LevelAt b x 成立，并仍把 x 的值认同为固定成员a 的底层集合。目标是证明 b 处的候选正是真实数码 # k。候选属于 ω 只能在命题截断之下揭示其自然数索引。目标是累积层级中的一条等式，而 setIsSet 表明这个等式类型是命题，因此可以把截断的数码数据消去到其中。
LevelAt-out : ⟨ γ ⊨ LevelAt b x ⟩ → fst (lookup x γ) ≡ fst a
→ fst (lookup b γ) ≡ # k
LevelAt-out (hω , (hex , hmin)) qx =
PT.rec (setIsSet (fst (lookup b γ)) (# k)) named hω
where
先排除解码所得索引 m 高于真实层号的情形，即假设 k < m，且 b 的值是 # m。由 #mono，# k 属于 # m；于是包装 numS k 与 towerS k 让我们能在真正的有穷层 Lset (# k) 处使用 LevelAt 的最小性子句。该子句说 x 的值不在那里，与 aIn 矛盾。它返回抬升后的矛盾，lower 只移除这个宇宙抬升；这是命题降级，而不是命题截断。
notAbove : (m : ℕ) → fst (lookup b γ) ≡ # m → k < m → Empty.⊥ notAbove m qb hk = lower (hmin (numS k) (subst (λ w → ⟨ w ∈ fst (lookup b γ) ⟩) (sym (numS-fst k)) (subst (λ w → ⟨ # k ∈ w ⟩) (sym qb) (#mono k m hk))) (towerS k) (towerGraph k (numS k ∷ γ) zero (numS-fst k))
传给该最小性子句的最后一个实参，正是它即将反驳的正面成员证明。从 aIn 出发，沿 qx 的反向把 a 的底层集合替换成 x 的值，再沿 towerS-fst k 的反向把 Lset (# k) 替换成其载体包装的底层集合。这样，公式与外部的最小层号论证便在谈论同一个有穷层中的同一个成员。
(subst (λ w → ⟨ fst (lookup x γ) ∈ w ⟩) (sym (towerS-fst k)) (subst (λ w → ⟨ w ∈ Lset (# k) ⟩) (sym qx) aIn)))
再排除解码所得索引低于真实层号的情形。若 m < k，LevelAt 的存在部分就在命题截断之下给出一个载体 c：它在 b 处满足层级图，并包含 x 的值。这恰是 Body 所命名的数据。由于目标是导出矛盾，可以把命题截断消去到空类型；每个显式见证都将迫使 a 已在第 m 个有穷层出现。
notBelow : (m : ℕ) → fst (lookup b γ) ≡ # m → m < k → Empty.⊥ notBelow m qb hm = PT.rec Empty.isProp⊥ atTower hex where atTower : Σ[ c ∈ S ] Body c → Empty.⊥ atTower (c , (hg , hmem)) = aMin m inStage hm
对于这样的见证，Lset-only 先把 c 的底层集合认同为由 b 的值索引的层级阶段。它所需的序数前提来自 numeral-ord m，并沿「b 的值是 # m」这条等式运输。再把所得等式与 cong Lset qb 复合，便得到具体认同 fst c ≡ Lset (# m)。
where qc : fst c ≡ Lset (# m) qc = Lset-only zero (suc b) (c ∷ γ) hg (subst IsOrd (sym qb) (numeral-ord m)) ∙ cong Lset qb
现在可以在具体的有穷层读取见证中保存的成员事实。沿 qc 运输后，它变成 x 的值属于 Lset (# m)；再沿 qx 运输，该值变成 a的底层集合。因此 a 已在第 m 个有穷层出现；结合 m < k，这与 aMin 矛盾。故候选索引不可能低于真实层号。
inStage : ⟨ fst a ∈ Lset (# m) ⟩ inStage = subst (λ w → ⟨ w ∈ Lset (# m) ⟩) qx (subst (λ w → ⟨ fst (lookup x γ) ∈ w ⟩) qc hmem)
还需认同从 ω 的成员身份中解码出的数码。一份显式解码数据包含j : Lift ℕ，以及从 # (lower j) 到 b 处之值的等式。反转该等式便得到 qb。一旦自然数比较证明 lower j ≡ k，对这条等式应用数码映射并作复合，就得到所需结论 fst (lookup b γ) ≡ # k。
named : Σ[ j ∈ Lift ℕ ] (# (lower j) ≡ fst (lookup b γ)) → fst (lookup b γ) ≡ # k named (j , qj) = qb ∙ cong #_ (decide (lower j ≟ k)) where qb : fst (lookup b γ) ≡ # (lower j)
自然数的三歧性恰好给出所需等式。lower j < k 的情形与 notBelow 矛盾，k < lower j 的情形与 notAbove 矛盾；相等情形则原样返回其证明。因此，两条读式在真值层面互相对应：真实的最小有穷层满足 LevelAt，而该公式为固定成员 a 报告的任何候选都必是它的真实层号。
qb = sym qj decide : NatOrder.Trichotomy (lower j) k → lower j ≡ k decide (NatOrder.lt h) = Empty.rec (notBelow (lower j) qb h) decide (NatOrder.eq e) = e decide (NatOrder.gt h) = Empty.rec (notAbove (lower j) qb h)
最先的分歧，在内部说出
要用公式比较集合，必须先把可构造载体的外部成员表示成语义载体 S 的元素。若 A : S 且 z 属于它的底层集合，可构造性的传递性就会把 A 中保存的证书化为 z 可构造的证书。memS 把 z 与这份继承来的证明包装起来。它构造的是依值载体的一个元素，不是集合论的有序对。
opaque memS : (A : S) (z : V ℓ) → ⟨ z ∈ fst A ⟩ → S memS A z h = z , isL-trans {x = fst A} {y = z} h (snd A)
投影等式 memS-fst 说明这次包装保留了正在讨论的集合：memS A z h 的底层集合就是 z。该等式由自反性成立，但把它显式写成引理后，后续运输便能在量化所得的载体元素与它所表示的外部集合之间往返，而无须展开包装。
memS-fst : (A : S) (z : V ℓ) (h : ⟨ z ∈ fst A ⟩) → fst (memS A z h) ≡ z memS-fst A z h = refl
PrecedesAt 相对于已存于 r 的关系和已存于 A 的载体，表达一步最先分歧比较。对于 x 与 y 处的集合，它要求存在载体成员 z，使 z 属于y 而不属于 x。这个方向决定比较结果：在作出裁决的点上，右侧集合的成员值为一，左侧集合的成员值为零，所以 x 先于 y。
PrecedesAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n PrecedesAt r A x y = ∃̇ ( (var zero ∈̇ var (suc A)) ∧̇ ( (var zero ∈̇ var (suc y)) ∧̇ ( ¬̇ (var zero ∈̇ var (suc x))
这个见证还必须是关系 r 所判定的最先分歧点。对载体 A 中的每个 w，若该关系把 w 排在 z 之前，则 w 属于 x 与属于 y 必须双向一致。公式通过 appAt 查阅关系；在语义上，这询问由 w 与 z 组成的集合论有序对是否属于存放在 r 的关系集。约束 z 的存在量词与约束 w 的全称量词，正好说明旧变量为何要移过两个位置。
∧̇ ∀̇∈ (var (suc A)) ( appAt (sh2 r) zero (suc zero) ⇒̇ ( ((var zero ∈̇ var (sh2 x)) ⇒̇ (var zero ∈̇ var (sh2 y))) ∧̇ ((var zero ∈̇ var (sh2 y)) ⇒̇ (var zero ∈̇ var (sh2 x))) ) ) ) ) )
模块 Precedes 准确列出读取这条公式所需的数据。除四个位置及其环境外，它还固定一个元层关系 R。定律 Rrep 把集合论有序对属于 r处关系集的事实读成一个 R 事实，Rfill 则把这种事实写回成员关系。两条定律只需处理可构造端点，因为每个量化端点本来就在 S 中，而外部的载体成员可由 memS 包装。这里不假设 R 满足任何序公理；公式只表示一步比较的定义，不依赖后来对某个具体关系为良序的证明。
module Precedes {n : ℕ} (r A x y : Fin n) (γ : S ^ n) (R : V ℓ → V ℓ → hProp (ℓ-suc ℓ)) (Rrep : (u v : S) → ⟨ pr (fst u) (fst v) ∈ fst (lookup r γ) ⟩ → ⟨ R (fst u) (fst v) ⟩) (Rfill : (u v : S) → ⟨ R (fst u) (fst v) ⟩
先固定载体。关于早于分歧点之元素的每个断言，都由环境中 A 处取值所指的可构造集合限定，因此比较不会越出基底关系所作用的那一层。
→ ⟨ pr (fst u) (fst v) ∈ fst (lookup r γ) ⟩) where private Aʟ : S Aʟ = lookup A γ
用 xv 表示环境中 x 处取值所指的集合。这样便能直接陈述左侧集合中的隶属，而不必在每个子句中重复环境查找。
xv : V ℓ
xv = fst (lookup x γ)
同样，yv 表示环境中 y 处取值所给的集合。这两个名称的次序很重要，因为首个分歧点属于右侧集合而不属于左侧集合。
yv : V ℓ yv = fst (lookup y γ)
在首个分歧点之前，两个集合必须对隶属给出相同答案。Both w 精确记录这一等价：w 属于 xv 蕴含它属于 yv，反向亦然。
Both : V ℓ → Type (ℓ-suc ℓ) Both w = (⟨ w ∈ xv ⟩ → ⟨ w ∈ yv ⟩) × (⟨ w ∈ yv ⟩ → ⟨ w ∈ xv ⟩)
对候选分歧见证 z，Agreeing z 考察载体中被编码基底关系排在 z 之前的每个 w。原子 appAt r w z 表示关系集含有 w 与 z 的有序对；在此前提下，xv 与 yv 必须在 w 处一致。
Agreeing : S → Type (ℓ-suc ℓ) Agreeing z = (w : S) → ⟨ fst w ∈ fst Aʟ ⟩ → ⟨ (w ∷ z ∷ γ) ⊨ appAt (sh2 r) zero (suc zero) ⟩ → Both (fst w)
见证本身必须属于载体和 yv，但不属于 xv；载体中每个按基底关系更早的成员都必须满足一致条件。因此这个方向表示 xv 先于 yv。这里并未假设所给基底关系满足任何序律，所以只有当该关系确实是序时，才能称此见证为「最早」分歧。
Body : S → Type (ℓ-suc ℓ) Body z = ⟨ fst z ∈ fst Aʟ ⟩ × ( ⟨ fst z ∈ yv ⟩ × ( (⟨ fst z ∈ xv ⟩ → Lift {j = ℓ-suc ℓ} Empty.⊥) × Agreeing z ) )
要把公式向外读，就把它的命题截断存在消去到命题 precedes R A xv yv。只需把每个给出的模型见证变成宿主层定义的见证，因为目标也只保留其命题截断。
PrecedesAt-out : ⟨ γ ⊨ PrecedesAt r A x y ⟩ → ⟨ precedes R (fst Aʟ) xv yv ⟩ PrecedesAt-out = PT.rec squash₁ atZ where atZ : Σ[ z ∈ S ] Body z → ⟨ precedes R (fst Aʟ) xv yv ⟩
z 的底层集给出宿主层见证，前三个分量已经给出它的载体隶属与有向分歧。剩下的任务是在任意宿主层元素 w 被排在它之前时证明两边一致。
atZ (z , (z∈A , (z∈y , (z∉x , hag)))) = ∣ fst z , (z∈A , (z∈y , ((λ h → lower (z∉x h)) , ag))) ∣₁ where ag : Agrees R (fst Aʟ) xv yv (fst z) ag w w∈A hR = subst Both (memS-fst Aʟ w w∈A) (hag wS w∈A' happ)
由于 w 属于可构造载体，它继承可构造性，因而可打包为模型元素 wS。其投影等式把原来的载体隶属证明搬运成对象语言有界子句所需的形式。
where wS : S wS = memS Aʟ w w∈A w∈A' : ⟨ fst wS ∈ fst Aʟ ⟩ w∈A' = subst (λ u → ⟨ u ∈ fst Aʟ ⟩) (sym (memS-fst Aʟ w w∈A)) w∈A
当前前提在宿主层表示 R w z。把 w 与 wS 对齐后，Rfill 将这个事实写成有序对属于关系集，这恰是建立应用原子所需的信息。
hp : ⟨ pr (fst wS) (fst z) ∈ fst (lookup r γ) ⟩ hp = Rfill wS z (subst (λ u → ⟨ R u (fst z) ⟩) (sym (memS-fst Aʟ w w∈A)) hR) happ : ⟨ (wS ∷ z ∷ γ) ⊨ appAt (sh2 r) zero (suc zero) ⟩ happ = subst ⟨_⟩
appAt 的充分性把这个有序对隶属陈述变成在由 wS 与 z 延拓的环境中的满足。现在即可应用对象语言中的一致假设。
(sym (appAt-adequate (sh2 r) zero (suc zero) (wS ∷ z ∷ γ))) hp
反向从 precedes 中的命题截断见证开始。由于 PrecedesAt 的满足本身是命题，可以消去该截断，并把每个宿主层见证转成对象语言的存在见证。
PrecedesAt-in : ⟨ precedes R (fst Aʟ) xv yv ⟩ → ⟨ γ ⊨ PrecedesAt r A x y ⟩ PrecedesAt-in = PT.rec squash₁ atZ where atZ : Σ[ z ∈ V ℓ ] Witness R (fst Aʟ) xv yv z
展开宿主层见证 z，连同它的载体隶属、右侧隶属、左侧排除以及在更早点处的一致。它属于载体，因而具有可构造性，所以 zS 可以充当公式的量化见证。
→ ⟨ γ ⊨ PrecedesAt r A x y ⟩ atZ (z , (z∈A , (z∈y , (z∉x , ag)))) = ∣ zS , (z∈A' , (z∈y' , (z∉x' , hag))) ∣₁ where zS : S
投影 fst zS 等于原来的 z。沿此等式搬运可知，打包后的见证仍属于载体，所以打包只改变它的呈现，不改变其数学作用。
zS = memS Aʟ z z∈A qz : fst zS ≡ z qz = memS-fst Aʟ z z∈A z∈A' : ⟨ fst zS ∈ fst Aʟ ⟩ z∈A' = subst (λ u → ⟨ u ∈ fst Aʟ ⟩) (sym qz) z∈A
同一投影等式也搬运 yv 中的隶属和 xv 中的非隶属。还需把公式中的关系前提读回 R，才能使用宿主层的一致假设。
z∈y' : ⟨ fst zS ∈ yv ⟩ z∈y' = subst (λ u → ⟨ u ∈ yv ⟩) (sym qz) z∈y z∉x' : ⟨ fst zS ∈ xv ⟩ → Lift {j = ℓ-suc ℓ} Empty.⊥ z∉x' h = lift (z∉x (subst (λ u → ⟨ u ∈ xv ⟩) qz h)) hag : Agreeing zS
给定载体中的模型元素 w，appAt 的充分性先把满足读成 w 与 zS 的有序对属于编码关系。这正是向外证明中所用转换的反向。
hag w w∈A happ = ag (fst w) w∈A hR where hp : ⟨ pr (fst w) (fst zS) ∈ fst (lookup r γ) ⟩ hp = subst ⟨_⟩ (appAt-adequate (sh2 r) zero (suc zero) (w ∷ zS ∷ γ)) happ hR : ⟨ R (fst w) z ⟩
现在 Rrep 把关系集隶属读回 R (fst w) zS；再把第二个端点从 fst zS 搬运到 z，便得到原一致证明所需的前提，从而取得 Both 中的两条隶属蕴含。
hR = subst (λ u → ⟨ R (fst w) u ⟩) qz (Rrep w zS hp)
那个序，接合起来
元素 a : Limit 携带其底层集属于 Lset ω 的证明。属于这个可构造层便给出所需的 isL 证据，使同一个底层集可作为模型元素 limitEl a。
opaque limitEl : Limit → S limitEl a = fst a , Lset→isL ω ω-ord (fst a) (snd a)
打包并不改变集合：按定义投影 limitEl a 就得到 fst a。这个等式随后会把模型内构造的有序对与表示定理中使用的外围有序对对齐。
limitEl-fst : (a : Limit) → fst (limitEl a) ≡ fst a limitEl-fst a = refl
要把一条关系放入 L，相关的两个端点必须由一个本身也是模型元素的有序对表示。prS 为任意两个可构造端点给出这个内部有序对。
prS : S → S → S prS a b = prʟ a b
prS 的投影律把其底层集认同为两个底层端点的外围有序对。因此，内部配对构造与外部关系隶属谈论的是同一个集合。
prS-fst : (a b : S) → fst (prS a b) ≡ pr (fst a) (fst b) prS-fst a b = prʟ-fst a b
在分离选出满足比较的有序对之前，所有候选对需要一个集合大小的共同界。先用小纤维呈现 Lset ω 的成员，把每个呈现出的成员打包为可构造元素，再用两个小纤维的积为有序对编索引。
pairsBound : Σ[ D ∈ S ] ((u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst D ⟩) pairsBound = d .fst , onPair where ixL : ⟪ Lset ω ⟫ → S ixL m = ⟪ Lset ω ⟫↪ m , Lset→isL ω ω-ord (⟪ Lset ω ⟫↪ m)
每个呈现索引确实指向 Lset ω 的一个成员。隶属桥把呈现事实变成通常的隶属，而属于该层又给出 ixL 打包所需的可构造性证明。
(∈∈ₛ {a = ⟪ Lset ω ⟫↪ m} {b = Lset ω} .snd (∈ₛ⟪ Lset ω ⟫↪ m))
把 smallDom 用于这个小积，得到一个含有所有内部构造有序对的可构造集合。它只是共同界，可以含有额外对象；精确的比较关系要靠在其中施行分离获得。
d : Σ[ D ∈ S ] ((p : ⟪ Lset ω ⟫ × ⟪ Lset ω ⟫) → ⟨ prʟ (ixL (fst p)) (ixL (snd p)) ∈ˢ D ⟩) d = smallDom (⟪ Lset ω ⟫ × ⟪ Lset ω ⟫) (λ p → prʟ (ixL (fst p)) (ixL (snd p)))
对任意 u,v : Limit，它们的底层集在 Lset ω 的小纤维中都有呈现索引。由这些索引形成的有序对属于共同界，再沿投影等式搬运，就得到外围有序对 pr (fst u) (fst v) 的隶属。
onPair : (u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst (d .fst) ⟩ onPair u v = subst (λ t → ⟨ t ∈ fst (d .fst) ⟩) (prʟ-fst (ixL (fu .fst)) (ixL (fv .fst)) ∙ cong₂ pr (fu .snd) (fv .snd)) (d .snd (fu .fst , fv .fst)) where
两条纤维见证恰好恢复上面使用的呈现索引，并附带把所呈现成员分别认同为 fst u 与 fst v 的等式。正因这些等式，小呈现才足以覆盖每个实际的极限层端点。
fu = ∈-asFiber {a = fst u} {b = Lset ω} (snd u) fv = ∈-asFiber {a = fst v} {b = Lset ω} (snd v)
从公式读取时，有时只能得到极限严格比较的命题截断。strictLimit 先使用已经证明的严格良序 limitOrder 的三歧性来恢复比较；若三歧性给出 a ≺ˡ b，就无需再作任何选择。
strictLimit : (a b : Limit) → ∥ a ≺ˡ b ∥₁ → a ≺ˡ b strictLimit a b h = decide (SWO.tri∙ limitOrder a b) where decide : Tri (a ≺ˡ b) (a ≡ b) (b ≺ˡ a) → a ≺ˡ b decide (lt k) = k
在已有截断的正向比较时，三歧性的另外两种情形不可能成立。若 a = b，搬运会给出自比较；若 b ≺ˡ a，它与隐藏的正向比较经传递性也会给出自比较。非自反性反驳这两个命题，因此这里只把命题截断消去到矛盾中。
decide (eq q) = Empty.rec (PT.rec Empty.isProp⊥ (λ k → SWO.irr∙ limitOrder b (subst (λ t → t ≺ˡ b) q k)) h) decide (gt k) = Empty.rec (PT.rec Empty.isProp⊥ (λ j → SWO.irr∙ limitOrder a (SWO.trans∙ limitOrder a b a j k)) h)
level a 的定义性质把 fst a 放在 finiteStage (level a) 中。等式 level a ≡ k 把这一隶属搬运到 finiteStage k，恰好给出调用有限层比较时所需的层边界。
levelStage : (a : Limit) (k : ℕ) → level a ≡ k → ⟨ fst a ∈ finiteStage k ⟩ levelStage a k q = subst (λ j → ⟨ fst a ∈ Lset (# j) ⟩) q (level-in a)
Described 是一个条件式框架。它接收一条用来描述 before m 的公式 BeforeAt，以及一个向内方向；只有当 b 处的取值表示 # m，且第一个端点属于 finiteStage m 时，才能使用这个方向。
module Described (BeforeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n) (BeforeAt-in : ∀ {n} (b x y : Fin n) (γ : S ^ n) (m : ℕ) → fst (lookup b γ) ≡ # m → ⟨ fst (lookup x γ) ∈ finiteStage m ⟩
向内假设还要求第二个端点属于同一有限层，并要求实际比较 before m x y；由这些数据，它产出 BeforeAt 的满足。因此，这个框架既不构造有限层关系，也不推出它的序律。
→ ⟨ fst (lookup y γ) ∈ finiteStage m ⟩ → ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩ → ⟨ γ ⊨ BeforeAt b x y ⟩) (BeforeAt-out : ∀ {n} (b x y : Fin n) (γ : S ^ n) (m : ℕ) → fst (lookup b γ) ≡ # m
向外假设具有相同的数码与层边界，并把满足读回 before m x y。只有同时满足两个方向的公式才能实例化这个框架；实际的 BeforeAt 以及由此得到的 codeOrder 由 EarliestDisagreement 提供，此处并没有无条件得到它们。
→ ⟨ fst (lookup x γ) ∈ finiteStage m ⟩ → ⟨ fst (lookup y γ) ∈ finiteStage m ⟩ → ⟨ γ ⊨ BeforeAt b x y ⟩ → ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩) where
LimitOrdAt 的第一支处理层号不等的情形。它绑定两个候选数码，分别证明它们是 x 与 y 的最小层号，并要求 x 的数码属于 y 的数码，从而表达自然数层号的严格不等。
opaque LimitOrdAt : ∀ {n} → Fin n → Fin n → Formula S n LimitOrdAt x y = ∃̇ ( ∃̇ ( LevelAt (suc zero) (sh2 x) ∧̇ ( LevelAt zero (sh2 y) ∧̇ (var (suc zero) ∈̇ var zero) ) ) )
第二支用一个共同数码处理层号相等的情形。两个 LevelAt 子句都把同一数码认作最小层号，然后由假设的 BeforeAt 在该有限层内比较两个端点。共享一个见证便表达了相等，无须另加对象语言等式。
∨̇ ∃̇ ( LevelAt zero (suc x) ∧̇ ( LevelAt zero (suc y) ∧̇ BeforeAt zero (suc x) (suc y) ) )
为证明这条公式的充分性，先固定环境中的两个位置 x 与 y，并把其取值分别认同为实际的 u,v : Limit。显式指数 ku,kv 及其与真实层号的等式，使证明能在自然数比较、数码隶属与层隶属之间清楚转换。
module Order {n : ℕ} (x y : Fin n) (γ : S ^ n) (u v : Limit) (ku kv : ℕ) (qu : level u ≡ ku) (qv : level v ≡ kv) (qx : fst (lookup x γ) ≡ fst u) (qy : fst (lookup y γ) ≡ fst v)
两个 Level 实例不只是提供方便的名称：每个实例都为相应的实际端点及其最小层号给出 LevelAt 的已验证读法。向外读取时，正是这座桥排除了伪造的数码见证。
where private module Lu = Level u ku qu module Lv = Level v kv qv
Split c d 是层号不等分支的语义内容。它表示 c 是左端点的最小层数码，d 是右端点的最小层数码，并且 c ∈ d；最后一项把方向固定为左侧层号小于右侧层号。
Split : S → S → Type (ℓ-suc ℓ) Split c d = ⟨ (d ∷ c ∷ γ) ⊨ LevelAt (suc zero) (sh2 x) ⟩ × ( ⟨ (d ∷ c ∷ γ) ⊨ LevelAt zero (sh2 y) ⟩ × ⟨ fst c ∈ fst d ⟩ )
Same c 是层号相等分支的语义内容。同一个 c 必须描述两个端点的最小层号，只有随后才能由 BeforeAt c x y 给出它们在该共同有限层内的比较。
Same : S → Type (ℓ-suc ℓ) Same c = ⟨ (c ∷ γ) ⊨ LevelAt zero (suc x) ⟩ × ( ⟨ (c ∷ γ) ⊨ LevelAt zero (suc y) ⟩ × ⟨ (c ∷ γ) ⊨ BeforeAt zero (suc x) (suc y) ⟩ )
设 ku < kv。选择打包为模型元素的真实数码 # ku 与 # kv 作为两个存在见证。两次 LevelAt-in 验证这些数码确实描述了已对齐端点的实际最小层号。
split-in : ku < kv → Split (numS ku) (numS kv) split-in hlt = Lu.LevelAt-in (suc zero) (sh2 x) (numS kv ∷ numS ku ∷ γ) (numS-fst ku) qx , ( Lv.LevelAt-in zero (sh2 y) (numS kv ∷ numS ku ∷ γ)
自然数的严格不等经数码单调性给出 # ku ∈ # kv。沿两个打包数码的投影等式搬运，就得到 Split 所需的隶属 fst (numS ku) ∈ fst (numS kv)。
(numS-fst kv) qy , subst2 (λ s t → ⟨ s ∈ t ⟩) (sym (numS-fst ku)) (sym (numS-fst kv)) (#mono ku kv hlt) )
在同层分支中，等式 level v ≡ level u 使同一个数码 # ku 能描述两个端点。左侧的 LevelAt 读法直接使用 qu，右侧则利用该等式把 v 的层号也表示为同一指数 ku。
same-in : (e : level v ≡ level u) → ⟨ before (level u) (fst u) (fst v) ⟩ → Same (numS ku) same-in e h = Lu.LevelAt-in zero (suc x) (numS ku ∷ γ) (numS-fst ku) qx , ( Level.LevelAt-in v ku (e ∙ qu) zero (suc y) (numS ku ∷ γ)
只有先建立所需边界，才能使用条件式假设 BeforeAt-in。层号等式把查得的两个端点都放入 finiteStage ku，而 numS ku 的投影等式表明作为共同数码给出的取值确实表示 # ku。
(numS-fst ku) qy , BeforeAt-in zero (suc x) (suc y) (numS ku ∷ γ) ku (numS-fst ku) (subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qx) (levelStage u ku qu)) (subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qy)
最后，把给定比较从指数 level u 搬运到 ku，并把它的两个端点与环境中的值对齐。连同两条层隶属证明，这满足 BeforeAt-in 的全部前提，从而完成 Same (numS ku)。
(levelStage v ku (e ∙ qu))) (subst2 (λ s t → ⟨ before ku s t ⟩) (sym qx) (sym qy) (subst (λ j → ⟨ before j (fst u) (fst v) ⟩) qu h)) )
向外读取 Split c d 时，先由两条 LevelAt-out 引理把 c 认同为 # ku、把 d 认同为 # kv。沿这些认同搬运 c ∈ d 后，消去数码隶属便得到 ku < kv，再由保存的层号等式转成 level u < level v。
split-out : (c d : S) → Split c d → level u < level v split-out c d (hx , (hy , hlt)) = subst2 _<_ (sym qu) (sym qv) (#∈#-elim ku kv (subst2 (λ s t → ⟨ s ∈ t ⟩) qc qd hlt)) where qc : fst c ≡ # ku
每个数码认同都在正确的延拓环境中取得：第一条 LevelAt 越过两个新见证指向 x，第二条则指向 y。这种绑定者对齐保证最终比较的是原来两个端点的真实层号，而不是见证本身。
qc = Lu.LevelAt-out (suc zero) (sh2 x) (d ∷ c ∷ γ) hx qx qd : fst d ≡ # kv qd = Lv.LevelAt-out zero (sh2 y) (d ∷ c ∷ γ) hy qy
在同层支中，同一个模型元素 c 同时充当 u 与 v 的候选层号数码。读取它的两份 LevelAt 证书会得到两个结论：双方的真实层号必定相等，而给定的有穷层公式也可以读成公共层内 u 在 v 之前。
same-out : (c : S) → Same c → (level v ≡ level u) × ⟨ before (level u) (fst u) (fst v) ⟩ same-out c (hx , (hy , hb)) = e , below where qc : fst c ≡ # ku
第一份证书把 c 的底层集合认作数码 # ku，第二份则把它认作 # kv。数码编码的单射性于是给出 ku = kv；再与定义 ku、kv 的层号等式复合，便得到 level v = level u。因此，层号相等是从共同见证中恢复的，并未作为等式写进对象语言公式。
qc = Lu.LevelAt-out zero (suc x) (c ∷ γ) hx qx qc' : fst c ≡ # kv qc' = Lv.LevelAt-out zero (suc y) (c ∷ γ) hy qy e : level v ≡ level u e = qv ∙ sym (#-inj′ (sym qc ∙ qc')) ∙ sym qu
要使用假定的 BeforeAt 读取方向，必须先知道被比较的两个集合都属于同一个有穷层。u 的层号隶属给出它位于第 ku 层，新得到的层号等式则把 v 也放入这一层；环境等式再把这两个集合分别认作 x 与 y 处的取值。
xIn : ⟨ fst (lookup x γ) ∈ finiteStage ku ⟩ xIn = subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qx) (levelStage u ku qu) yIn : ⟨ fst (lookup y γ) ∈ finiteStage ku ⟩ yIn = subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qy) (levelStage v ku (e ∙ qu))
现在可以在 c 所表示的数码处应用抽象假设 BeforeAt-out。它先给出两个环境值之间的 before ku；把这两个值换成 fst u 与 fst v，再把 ku 换成 level u，便得到极限序同层支所需的有穷层比较。整个论证只在假设规定的层边界内使用 BeforeAt，不要求它在边界外具有任何语义。
below : ⟨ before (level u) (fst u) (fst v) ⟩ below = subst (λ j → ⟨ before j (fst u) (fst v) ⟩) (sym qu) (subst2 (λ s t → ⟨ before ku s t ⟩) qx qy (BeforeAt-out zero (suc x) (suc y) (c ∷ γ) ku qc xIn yIn hb))
LimitOrdAt 的两条充分性律保留了两个数学分支的意义：层号不同时比较其数码，同层时使用外部提供的有穷层公式。不透明边界使这一定义的每次使用都经过这两条定律。因此，Described 内的每项结果都以它的三个输入为条件。
opaque unfolding LimitOrdAt
先设 u 首次出现的有穷层严格早于 v。对象语言中的两个见证是模型数码 # ku 与 # kv；它们的 LevelAt 证书分别认出两个对象的层号，而第一个数码属于第二个数码正好表达 ku < kv。这些资料共同构成 LimitOrdAt 的异层支。
LimitOrdAt-in : u ≺ˡ v → ⟨ γ ⊨ LimitOrdAt x y ⟩ LimitOrdAt-in h = decide-in h where lower-in : ku < kv → ⟨ γ ⊨ LimitOrdAt x y ⟩ lower-in hlt = ∣ inl ∣ numS ku , ∣ numS kv , split-in hlt ∣₁ ∣₁ ∣₁
若双方层号相等，只需一个数码 # ku 同时证明两条 LevelAt 陈述。外部比较中的有穷层部分随后被写入这一公共层处的 BeforeAt 公式。共同使用一个见证本身就表达两个层号相等，因此对象语言里不需要另写两个层号数码之间的等式。
inner-in : (e : level v ≡ level u)
→ ⟨ before (level u) (fst u) (fst v) ⟩
→ ⟨ γ ⊨ LimitOrdAt x y ⟩
inner-in e k = ∣ inr ∣ numS ku , same-in e k ∣₁ ∣₁
外部极限比较恰好给出这两个选项。在第一支中，Lift 只把命题放入更高的宇宙；lower 所做的是命题降级，从中取回普通的自然数不等式。再用 ku 与 kv 的定义等式对齐索引，便可应用异层支的构造。
decide-in : Lift {ℓ-zero} {ℓ-suc ℓ} (level u < level v) ⊎ ((level v ≡ level u) × ⟨ before (level u) (fst u) (fst v) ⟩) → ⟨ γ ⊨ LimitOrdAt x y ⟩ decide-in (inl k) = lower-in (subst2 _<_ qu qv (lower k))
外部比较的第二个选项已经包含同层构造所需的两项资料：层号相等，以及该层中的 before 比较。把二者交给同层构造便完成填充方向。因此，LimitOrdAt-in 只是依照既有极限序的字典式定义行事，并未引入一条新序。
decide-in (inr (e , k)) = inner-in e k
读取 LimitOrdAt 时，两个分支的选择已经处在命题截断之中，所以最初只能得到命题截断的比较。在异层支中，两层存在见证由 split-out 读取；数码隶属由此还原为真实层号之间的严格不等式。所得不等式进入外部极限比较的第一支，并继续保留在命题截断内。
LimitOrdAt-out : ⟨ γ ⊨ LimitOrdAt x y ⟩ → ∥ u ≺ˡ v ∥₁ LimitOrdAt-out = PT.rec squash₁ decide where atSplit : (c : S) → Σ[ d ∈ S ] Split c d → ∥ u ≺ˡ v ∥₁ atSplit c (d , hs) = ∣ inl (lift (split-out c d hs)) ∣₁
在同层支中，same-out 返回真实层号相等以及该有穷层中的 before 比较。这两项正好构成外部极限比较的第二支。这里不会导出任何层号不等式；次序信息完全来自层内比较。
atSame : Σ[ c ∈ S ] Same c → ∥ u ≺ˡ v ∥₁
atSame (c , hs) = ∣ inr (same-out c hs) ∣₁
语义析取先把两个数学情形分开，再处理各自的见证。左侧含有两层嵌套的层号存在见证与数码隶属，右侧则含有一个共同层号及有穷层公式。这一结构正对应极限序先比较层号、同层时再作层内比较的字典式次序。
decide : ⟨ γ ⊨ ∃̇ ( ∃̇ ( LevelAt (suc zero) (sh2 x) ∧̇ ( LevelAt zero (sh2 y) ∧̇ (var (suc zero) ∈̇ var zero) ) ) ) ⟩ ⊎ ⟨ γ ⊨ ∃̇ ( LevelAt zero (suc x) ∧̇ ( LevelAt zero (suc y)
每个存在见证都只被消去到命题截断的目标中。异层情形局部取出两个候选层号并应用 atSplit，同层情形局部取出唯一的共同候选并应用 atSame。这些见证只用于证明当前比较，没有任何层号数码的选择逸出命题截断。
∧̇ BeforeAt zero (suc x) (suc y) ) ) ⟩ → ∥ u ≺ˡ v ∥₁ decide (inl h) = PT.rec squash₁ (λ { (c , hd) → PT.rec squash₁ (atSplit c) hd }) h decide (inr h) = PT.rec squash₁ atSame h
那个序，作为一个集合
要把比较化为关系集，分离条件必须先辨认候选元素是否为有序对。Cond₀ 绑定可能的分量 c 与 d，要求候选元素是二者的编码有序对，并要求 LimitOrdAt c d 成立。因此，这个条件同时规定元素的配对形状与其所表示比较的方向。
Cond₀ : Formula S 1 Cond₀ = ∃̇ ( ∃̇ ( prAtL (sh2 zero) (suc zero) zero ∧̇ LimitOrdAt (suc zero) zero ) )
在 Described 的一个实例内部，分离以 Cond₀ 筛选包含所有极限层元素对的公共界。所得模型元素 codeOrder 恰好包含这个界内满足比较条件的候选元素。它的存在以给定的 BeforeAt 公式及其两条充分性方向为条件；下一章才提供具体实例。
opaque codeOrder : S codeOrder = hasSeparationL (pairsBound .fst) Cond₀ .fst .fst
分离规格给出可直接使用的隶属刻画：一个候选元素属于 codeOrder，当且仅当它属于 pairsBound 并满足 Cond₀。公共界本身可能还含有额外元素，因此只负责给出集合大小的包容；精确性来自第二个合取项，它辨认有序对并验证相应的极限比较。
codeOrder-mem : (z : S) → (z ∈ˢ codeOrder) ≡ ((z ∈ˢ pairsBound .fst) ⊓ ((z ∷ []) ⊨ Cond₀)) codeOrder-mem = hasSeparationL (pairsBound .fst) Cond₀ .fst .snd
固定 z、c、d 后，Inner 集中记录分离公式所需的两个事实：z 是 c 与 d 的编码有序对，并且 LimitOrdAt 判定 c 在 d 之前。把二者放在一起，便能确保比较所用的端点正是候选对编码的两个分量。
private Inner : S → S → S → Type (ℓ-suc ℓ) Inner z c d = ⟨ (d ∷ c ∷ z ∷ []) ⊨ prAtL (sh2 zero) (suc zero) zero ⟩ × ⟨ (d ∷ c ∷ z ∷ []) ⊨ LimitOrdAt (suc zero) zero ⟩
Outer z 展示两层嵌套存在量词的见证结构：先给出第一个分量 c，再在命题截断中给出满足 Inner z c d 的第二个分量 d。这种嵌套与 Cond₀ 的语义一致，既保留见证之间的依赖，也不为 z 选择一个规范分解。
Outer : S → Type (ℓ-suc ℓ) Outer z = Σ[ c ∈ S ] ∥ (Σ[ d ∈ S ] Inner z c d) ∥₁
给定实际分量以及 Inner 中的两个事实，只要把这些分量依次放入嵌套存在量词，就能满足分离条件。两个存在见证都处在命题截断中，因为对象语言的存在只记录合适分量确实存在。分离所得集合的隶属本身是命题，所以这些资料已经足够。
cond-in : (z c d : S) → Inner z c d → ⟨ (z ∷ []) ⊨ Cond₀ ⟩ cond-in z c d hi = ∣ c , ∣ d , hi ∣₁ ∣₁
反过来，满足 Cond₀ 的证据已经具有 Outer 所记录的截断嵌套结构，所以读取时可以直接保留这份证据，不必选择任何一个分量。借助这一点，后面的隶属证明可以展开分离条件，同时始终留在命题截断的存在之内。
cond-out : (z : S) → ⟨ (z ∷ []) ⊨ Cond₀ ⟩ → ∥ Outer z ∥₁ cond-out z h = h
填充律从外部比较 u ≺ˡ v 出发，目标是证明二者底层集合的普通有序对属于 codeOrder。论证先使用真正位于模型中的 limitEl u、limitEl v 及其模型内编码对；最后再用一条等式把这一内部呈现与 pr (fst u) (fst v) 对齐。
codeOrder-fill : (u v : Limit) → u ≺ˡ v → ⟨ pr (fst u) (fst v) ∈ fst codeOrder ⟩ codeOrder-fill u v h = subst (λ t → ⟨ t ∈ fst codeOrder ⟩) qz (subst ⟨_⟩ (sym (codeOrder-mem (prS (limitEl u) (limitEl v))))
分离规格把隶属目标归约为两个数学义务。模型内编码对必须属于公共界，而 Cond₀ 必须以 limitEl u 与 limitEl v 为两个见证成立。完成这两项后，分离规格给出隶属，再沿两个配对呈现之间的等式得到原目标。
(inBound , cond-in (prS (limitEl u) (limitEl v)) (limitEl u) (limitEl v) (hpr , hord))) where qz : fst (prS (limitEl u) (limitEl v)) ≡ pr (fst u) (fst v) qz = prS-fst (limitEl u) (limitEl v)
对齐等式由两个直接步骤组成。模型内配对的投影等于两个投影的外部有序对，而每个 limitEl 又投影回原极限层元素的底层集合。复合这两个事实可知，改变呈现既不改变任何端点，也不改变端点的顺序。
∙ cong₂ pr (limitEl-fst u) (limitEl-fst v)
第一个分离义务使用 pairsBound 的定义性质：任取两个极限层元素，由它们形成的有序对都受这个界覆盖。应用覆盖证书前，先把模型内编码对与相应的外部有序对对齐。这里不需要公共界的反向刻画，因为精确的比较标准由 Cond₀ 提供。
inBound : ⟨ fst (prS (limitEl u) (limitEl v)) ∈ fst (pairsBound .fst) ⟩ inBound = subst (λ t → ⟨ t ∈ fst (pairsBound .fst) ⟩) (sym qz) (pairsBound .snd u v)
Cond₀ 的配对合取项由 prAtL 的充分性建立。模型内配对的投影已经是所需的有序对，因此这条充分性律把投影等式转成配对原子的满足证据。由此，公共界所用的集合论有序对与分离条件所用的对象语言描述连接起来。
hpr : ⟨ (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ []) ⊨ prAtL (sh2 zero) (suc zero) zero ⟩ hpr = subst ⟨_⟩ (sym (prAtL-adequate (sh2 zero) (suc zero) zero (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ []))) (prS-fst (limitEl u) (limitEl v))
比较合取项由 LimitOrdAt-in 在含有候选对及其两个分量的环境中给出。把分量取为 limitEl u 与 limitEl v 后，所需的对齐等式都是自反等式，而原假设 u ≺ˡ v 正好提供比较。至此完成条件式表示的正向证明。
hord : ⟨ (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ [])
⊨ LimitOrdAt (suc zero) zero ⟩
hord = Order.LimitOrdAt-in (suc zero) zero
(limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ [])
u v (level u) (level v) refl refl (limitEl-fst u) (limitEl-fst v) h
读取律从 pr (fst u) (fst v) 属于 codeOrder 出发。分离条件会给出一对处于命题截断中的分量，并证明它们满足配对与比较条件；读取这些条件最初只能得到 ∥ u ≺ˡ v ∥₁。最后由既已证明的严格良序 limitOrder 应用 strictLimit，利用三歧性排除相等与反向比较，才得到未截断的结论。
codeOrder-rep : (u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst codeOrder ⟩ → u ≺ˡ v codeOrder-rep u v h = strictLimit u v (PT.rec squash₁ atC (cond-out (prS (limitEl u) (limitEl v))
与填充方向相同，先把模型内编码对认作两个底层集合的外部有序对。把隶属转到这一呈现后，codeOrder-mem 展开分离的两个合取项，其中第二项正是满足 Cond₀。从此可以不再使用公共界合取项，因为端点及比较的全部信息都在分离条件中。
(subst ⟨_⟩ (codeOrder-mem (prS (limitEl u) (limitEl v))) inSet .snd))) where qz : fst (prS (limitEl u) (limitEl v)) ≡ pr (fst u) (fst v) qz = prS-fst (limitEl u) (limitEl v) ∙ cong₂ pr (limitEl-fst u) (limitEl-fst v)
已知隶属针对外部有序对，而分离规格要应用于 prS 产生的模型元素。配对对齐等式说明二者的底层集合相等，因此可以把隶属转到模型内呈现。只有完成这一步，才能在该模型元素所形成的环境中读取对象语言条件。
inSet : ⟨ fst (prS (limitEl u) (limitEl v)) ∈ fst codeOrder ⟩
inSet = subst (λ t → ⟨ t ∈ fst codeOrder ⟩) (sym qz) h
对给定见证 c、d，配对原子先证明它们正是原有序对所编码的两个端点。把所得端点等式调整到所需方向后，LimitOrdAt-out 才能把随附的比较公式读成命题截断的 u ≺ˡ v。因此，比较合取项不能脱离配对合取项单独读取，后者负责认定公式所比较的究竟是哪两个外部极限层元素。
atD : (c d : S) → Inner (prS (limitEl u) (limitEl v)) c d → ∥ u ≺ˡ v ∥₁ atD c d (hpr , hord) = Order.LimitOrdAt-out (suc zero) zero (d ∷ c ∷ prS (limitEl u) (limitEl v) ∷ []) u v (level u) (level v) refl refl (sym (split .fst)) (sym (split .snd)) hord where
配对原子的充分性把其满足证据转成候选元素底层集合与 pr (fst c) (fst d) 之间的等式。先前的对齐又把同一个候选元素认作 pr (fst u) (fst v)。复合这两个等式便得到两个有序对相等，并为读取 LimitOrdAt 准备好所需的端点等式。
qcd : pr (fst u) (fst v) ≡ pr (fst c) (fst d) qcd = sym qz ∙ subst ⟨_⟩ (prAtL-adequate (sh2 zero) (suc zero) zero (d ∷ c ∷ prS (limitEl u) (limitEl v) ∷ [])) hpr split : (fst u ≡ fst c) × (fst v ≡ fst d)
有序对编码的单射性把配对等式拆成 fst u = fst c 与 fst v = fst d。两个分量的位置与方向都被保留，左端不会与右端交换。把这两条等式反向，正好得到 LimitOrdAt 读取定理所需的对齐假设。
split = pr-inj qcd
外层读取按照 Cond₀ 的绑定次序处理嵌套见证：先处理 c，再在命题截断内处理 d 及其 Inner 证据。每次消去的目标都是 atD 已给出的命题截断比较，所以整个过程始终遵守截断限制。所有可能分解都被映到这个命题后，再由 strictLimit 给出最终未截断的比较。
atC : Outer (prS (limitEl u) (limitEl v)) → ∥ u ≺ˡ v ∥₁ atC (c , hd) = PT.rec squash₁ (λ { (d , hi) → atD c d hi }) hd
那个为诸码所设的位，已填上
CodeKeys 记录了在任意可构造载体 A 上进行名字比较时，使用这条条件式码关系的一种方式。除了 A 及其可构造性证明，它还固定 A 的小成员类型上的严格良序 w。名字比较的充分性结果于是可用 w 比较参数，并用当前 Described 实例比较码。这个嵌套模块是表示定理的一项可复用推论，主构造并不依赖它。
module CodeKeys (A : V ℓ) (pA : ⟨ isL A ⟩) (w : SWO ⟪ A ⟫) where private module Ad = Adequacy A pA w
w 的严格关系在局部获得一个专用记号，以便把参数比较与码所用的极限层比较 u ≺ˡ v 区分开来。两条关系位于不同载体上，也由不同的内部关系集表示。它们的充分性律形状相同，但数学输入彼此独立。
open SWO w using () renaming ( _<∙_ to _≺ₚ_ )
若模型关系 Ps 从两个方向表示参数序，AtParams 就把它连同 codeOrder 及码序的两条表示律一起交给 Adequacy.Keys；这两条被表示的关系在数学上仍彼此独立。真实的下游路线在 EarliestDisagreement 中实例化 Described，公开 codeOrder、codeOrder-fill 与 codeOrder-rep，再由 InternalWellOrder 把这三项连同另行表示的参数序直接交给 NameComparisonAdequacy.At.Least。
module AtParams (Ps : S) (Prep : (a b : ⟪ A ⟫) → ⟨ pr (Ad.ix a) (Ad.ix b) ∈ fst Ps ⟩ → a ≺ₚ b) (Pfill : (a b : ⟪ A ⟫) → a ≺ₚ b → ⟨ pr (Ad.ix a) (Ad.ix b) ∈ fst Ps ⟩) where open Ad.Keys codeOrder Ps codeOrder-rep codeOrder-fill Prep Pfill public
剩下什么，点准了名
Described 尚需一条公式 BeforeAt 及其两条读式。这两条读式只要求处理如下情形：第一个取值是数码 # m，两个端点都属于 finiteStage m；在这些假设下，公式成立当且仅当 before m 比较这两个端点。模块 EarliestDisagreement 恰好给出这些资料：relAt m 表示 before m，beforeFam 沿内部自然数收集这些已经表示的关系，而其中的 BeforeAt 先取出给定数码处的关系，再把它应用于两个端点。以这些结果实例化 Described，便得到公开的关系集 codeOrder 及其两条表示律 codeOrder-fill 与 codeOrder-rep。
小结
LevelAt 认出给定极限层成员首次出现的有穷层所对应的数码，PrecedesAt 则相对于任意已经表示的基底关系，表示一次最先分歧比较。给定 BeforeAt 在规定边界内的双向读法后，Described 用 LimitOrdAt 组合异层比较与同层比较，为所有候选有序对取界，再由分离得到条件式关系集 codeOrder。对每个 u,v : Limit，填充律与读取律给出 u ≺ˡ v 和 pr (fst u) (fst v) 属于该集合之间的两个方向；读取方向使用 strictLimit 与既有严格良序，从命题截断恢复比较。EarliestDisagreement 兑现有穷层假设，但本章既不在对象语言中断言 codeOrder 是良序，也不证明选择公理。