Bedrock可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。
交互式目录 · 依赖图从一开始就要区分两个话语层次。此前构造的 orderAt 是元语言中的严格良序。本章的目标是构造一些公式，使其满足关系表达该良序的底层比较；本章没有任何公式重新构造 SWO 结构，也不重证其良基性。
module L.Choice.StageOrderAdequacy {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
元理论已经在每个可构造层携带一个严格良序，但 L 的对象语言只能通过公式说话。本章把这一层序翻译成公式：描述每个集合的诞生层、随载体变化的码集，以及层序的比较规则，并证明这些描述忠实于其元语言含义。其中有一件被刻意留作参数：固定诞生层内部的比较。
经典推理只经由一个显式假设 lem 进入。比较序数层时会用到它，而本章构造的公式仍是对象语言的普通公式。因此，语义论证可以使用排中律，却不会把新公理写进被解释的语言。
这次翻译只使用对象语言的普通原子与联结词。成员关系原子陈述候选见证属于某层或码集，相等原子认同两个被表示的对象，而存在量词隐藏描述所需的辅助集合。后文的证明会在可构造结构中解释这些公式，再把所得命题与相应的元语言命题比较。
这里所需的层级几何很简单。序数线性排列各层，序数指标之间的成员关系使塔保持单调，而一个序数的后继把该层与下一可定义幂集层分开。借助这些事实，我们可以比较候选诞生序数的后继与集合首次出现的层，从而认定该候选序数。
对可构造集合 x，包含它的最早层是一个后继层，而 birth x 是紧邻其下的序数。因此，x 不属于 Lset (birth x)，却属于 Lset (sucV (birth x))，后者正是前一层的可定义幂集。公式 BirthAt 将表达这两条成员关系事实；最小性本身仍来自元语言定理。
既有的层序按诞生层对两个元素作字典式比较。较早的诞生层立即决定比较；诞生层相等时，比较交给该层新生元素上的局部序。后面的公式将精确对应这一次展开方程，因此其充分性只关乎 orderAt 已经携带的关系，并不关乎该序的构造。
同层比较需要使用定义在某个载体上的公式，而该载体随共同诞生序数变化。因此，相关语法不能预先固定在单一层上。下文的码谓词相对于一个由变元槽位持有的载体，涵盖每个有限元数，使载体及其公式码能够一同变化。
最终目标是在 L 中把关系表示为有序对之集。环境层以下的一张表提供局部关系取值，而公式必须对每个编码有序对都与元语言比较一致。证明这种一致既需要表项的正确性，也需要表项的存在性，并且始终以局部步进公式的两条充分性读式为条件。
被表示关系的一个元素读作编码 pr u v。因此，充分性有两个方向：从这种对码恢复某些被比较元素 u、v 并证明其层序比较成立；反过来，从一次已知比较把相应对码放入被表示集合。这里的存在经过命题截断，因而不会选出规范的分解。
证明中的若干认同会沿相等的层指标或对码搬运关系。由于序数性与可构造性证据都是命题，更换这些证据不会改变被表示的数学对象。正是这种证明无关性允许我们进行搬运，而不会把证书变成额外的选择。
存在量词的满足关系始终经过命题截断。证明只有在目标仍是命题时，才能使用某个层取值、可定义幂集取值、解码公式或表项。因此，下文任何一次消去都不会给出规范见证、选定的解码器，或为局部关系指定取值的选择函数。
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ )
这里有两种作用不同的后继构造。sucV 推进一个序数层，而数码在层级内部编码有限元数。区分二者，就不会把「集合在诞生层的后继处进入」与公式码的元数分量混为一谈。
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( sucV; #_ )
这些公式将在可构造结构 𝒮ʟ 中解释，所以其含义取值于命题：满足关系记录被描述的成员关系、相等或存在是否在 L 内成立，而比较这些含义的证明则生活在外围的 Cubical Agda 元理论中。
open hPropView 𝒮ʟ
我们以 γ ⊨ φ 表示公式在环境中的满足，以 ⟦ t ⟧ γ 表示项的取值。每条充分性陈述都通过这套记号架桥：左侧读取对象语言语法，右侧认定元理论中相应的集合、序数或关系。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ ; ⟦_⟧ᵐ to ⟦_⟧ )
第一个移位把变元命名到外移两槽的位置，为绑定四个对象的公式做准备。
sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
sh2 i = suc (suc i)
第二个移位把变元外移三槽。
sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n)))
sh3 i = suc (suc (suc i))
一个私有移位把变元外移四槽，预留给下一节绑定四个对象的公式。
private
sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n))))
sh4 i = suc (suc (suc (suc i)))
项的移位把一个项移过四个新绑定：常数保持其值，每个变元按同一移位改名。
tm4 : ∀ {n} → Term S n → Term S (suc (suc (suc (suc n))))
tm4 (con k) = con k
tm4 (var i) = var (sh4 i)
移位后的项的求值不受四个新绑定影响；这一定义性一致被记录一次，此后静默复用。
tm4-val : ∀ {n} (t : Term S n) (a b c d : S) (γ : Vec S n)
→ ⟦ tm4 t ⟧ (d ∷ c ∷ b ∷ a ∷ γ) ≡ ⟦ t ⟧ γ
tm4-val (con k) a b c d γ = refl
tm4-val (var i) a b c d γ = refl
为了把 Lset β 放入公式环境，我们将该层连同其可构造性证明打包为 S 的元素。序数性假设提供这份证明。数学上要紧的是下文的第一投影等式：这个封装仍恰好指称 Lset β，因而可以在向内读取 BirthAt 时充当层见证。
opaque
towerS : (β : V ℓ) → IsOrd β → S
towerS β ob = LsetS β ob
打包后的层的底层集按定义就是层本身。
towerS-fst : (β : V ℓ) (ob : IsOrd β) → (towerS β ob) .fst ≡ Lset β
towerS-fst β ob = refl
BirthAt 所需的第二个见证是该层的可定义幂集。我们以同样方式封装 𝒟ₒ (Lset β)；它的可构造性来自序数 β 处已有的层事实，而其第一投影正是公式所需的集合。
powS : (β : V ℓ) → IsOrd β → S
powS β ob = 𝒟ₒS β ob
其底层集按定义就是该序数处层的可定义幂集。
powS-fst : (β : V ℓ) (ob : IsOrd β) → (powS β ob) .fst ≡ 𝒟ₒ (Lset β)
powS-fst β ob = refl
诞生层的内部表述
BirthAt b x 绑定两个辅助集合。第一个必须是候选槽位 b 所描述的塔层 Lset β，且 x 不属于它；第二个必须是前者的可定义幂集，且 x 属于它。因此，该公式表达两个相继层之间的边界。它既不断言 β 是序数，也不包含对象语言内部的最小性子句。
BirthAt : ∀ {n} → Fin n → Fin n → Formula S n
BirthAt b x =
∃̇ ( LsetGraphAt zero (suc b)
∧̇ ( ¬̇ (var (suc x) ∈̇ var zero)
∧̇ ∃̇ ( DefAt zero (suc zero) ∧̇ (var (sh2 x) ∈̇ var zero) ) ) )
固定一个环境 γ。候选序数是槽位 b 中元素的底层集合，而待检验诞生层的集合是槽位 x 中的元素。后续推理都相对于这两个解释进行，所以定理适用于任意变元赋值，而非特选常元。
module _ {n : ℕ} (b x : Fin n) (γ : Vec S n) where
private
β : V ℓ
β = (lookup b γ) .fst
元素 z 同时携带其底层集合与它属于 L 的证据。元语言函数 birth 使用这份证据形成一个序数，但证明无关性保证所得序数不会编码对某份可构造性证明的选择。
z : S
z = lookup x γ
内层记录收集候选层 c 之上的可定义幂集值 d，连同幂集描述的满足，以及参数属于 d 的成员关系。
Inner : S → Type (ℓ-suc ℓ)
Inner c = Σ[ d ∶ S ]
( ⟨ (d ∷ c ∷ γ) ⊨ DefAt zero (suc zero) ⟩ × ⟨ z .fst ∈ d .fst ⟩ )
外层记录再加上「层图在抬升指数处的满足」「参数不属于候选层」的反驳，以及内层记录的截断。三者合起来恰是诞生公式所断言的内容。
Outer : S → Type (ℓ-suc ℓ)
Outer c = ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩
× ( (⟨ z .fst ∈ c .fst ⟩ → Lift {j = ℓ-suc ℓ} ⊥₀) × ∥ Inner c ∥₁ )
关键语义引理假设 β 是序数，并且 x 属于 𝒟ₒ (Lset β) 而不属于 Lset β。它恰从这些边界事实证明 β ≡ birth x。序数性是这条读式的输入，并非从 BirthAt 的满足关系中恢复。
decideBirth : IsOrd β → ⟨ z .fst ∈ 𝒟ₒ (Lset β) ⟩
→ (⟨ z .fst ∈ Lset β ⟩ → ⊥₀)
→ β ≡ birth (z .fst) (z .snd)
decideBirth ob hin hout = go (ord-tri (sucV β) (suc-ord ob)
(stage (z .fst) (z .snd))
借助 Lset-suc，𝒟ₒ (Lset β) 中的成员关系转化为 Lset (sucV β) 中的成员关系。这说明包含 x 的最早层不晚于 β 的后继；证明还必须排除所有更早的可能。
(stage-ord (z .fst) (z .snd)))
where
mem : ⟨ z .fst ∈ Lset (sucV β) ⟩
mem = subst (λ u → ⟨ z .fst ∈ u ⟩) (sym (Lset-suc β)) hin
假设 x 的最早层属于 sucV β。后继序数中的成员关系分成两种情形：该层属于 β，或该层等于 β。前一种由单调性、后一种由直接搬运，都会推出 x 属于 Lset β，与所假设的非成员关系矛盾。
early : ⟨ stage (z .fst) (z .snd) ∈ sucV β ⟩ → ⊥₀
early h = ⊥*-rec (∈sucV-elim {A = β} {x = stage (z .fst) (z .snd)}
isProp⊥* h below same)
where
below : ⟨ stage (z .fst) (z .snd) ∈ β ⟩ → ⊥*
若 stage x ∈ β，层的单调性会把已知的 x ∈ Lset (stage x) 推到 x ∈ Lset β。若 stage x ≡ β，沿该等式搬运即可直接得到同一结论。两种情形都与边界假设 x ∉ Lset β 矛盾。
below k = ⊥₀-rec (hout
(Lset-mono {α = β} {β = stage (z .fst) (z .snd)} k
{x = z .fst} (stage-mem (z .fst) (z .snd))))
same : stage (z .fst) (z .snd) ≡ β → ⊥*
same e = ⊥₀-rec (hout (subst (λ u → ⟨ z .fst ∈ Lset u ⟩) e
在相等情形中，stage x ≡ β 把已知的成员关系 x ∈ Lset (stage x) 搬运成 x ∈ Lset β。这是证明最早层不可能位于 β 或其下所需的第二个矛盾。
(stage-mem (z .fst) (z .snd))))
现在用序数三歧律比较 sucV β 与 stage x。若前者严格更早，则 x ∈ Lset (sucV β) 与 stage x 的定义性最小性矛盾；若 stage x 更早，则前述论证与 x ∉ Lset β 矛盾。因此，只可能剩下相等情形。
go : ⟨ sucV β ∈ stage (z .fst) (z .snd) ⟩
⊎ ((sucV β ≡ stage (z .fst) (z .snd)) ⊎ ⟨ stage (z .fst) (z .snd) ∈ sucV β ⟩)
→ β ≡ birth (z .fst) (z .snd)
go (inl h) = ⊥₀-rec
(stage-earliest (z .fst) (z .snd) (sucV β) (suc-ord ob) mem h)
由 sucV β ≡ stage x 与等式 stage x ≡ sucV (birth x)，序数后继的单射性给出 β ≡ birth x。结论来自对两个严格情形的排除；证明并未从公式中选取诞生见证。
go (inr (inl e)) = ord-suc-inj β (birth (z .fst) (z .snd)) ob
(e ∙ sym (birth-suc (z .fst) (z .snd)))
go (inr (inr h)) = ⊥₀-rec (early h)
读取引理携带槽位的序数性假设：公式自身并不证明该槽位是序数。证明拆开截断的存在量化，抵达外层记录。
BirthAt-out : ⟨ γ ⊨ BirthAt b x ⟩ → IsOrd β → β ≡ birth (z .fst) (z .snd)
BirthAt-out h ob =
rec₁ (setIsSet β (birth (z .fst) (z .snd))) atCarrier h
where
atInner : (c : S) → ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩
在每个候选层处，内层记录供给包含参数的可定义幂集值，以及参数不属于候选层的反驳；判定引理应用于这三份数据。
→ (⟨ z .fst ∈ c .fst ⟩ → ⊥₀)
→ Inner c → β ≡ birth (z .fst) (z .snd)
atInner c hg hn (d , (hd , hm)) = decideBirth ob
(subst (λ u → ⟨ z .fst ∈ u ⟩) qd hm)
(λ k → hn (subst (λ u → ⟨ z .fst ∈ u ⟩) (sym qc) k))
抬升指数处的层图由层级描述的唯一性认同为候选序数处的层；幂集值由描述的层等式认同为该层的可定义幂集。
where
qc : c .fst ≡ Lset β
qc = Lset-only zero (suc b) (c ∷ γ) hg ob
qd : d .fst ≡ 𝒟ₒ (Lset β)
qd = subst ⟨_⟩ (DefAt-stage β ob zero (suc zero) (d ∷ c ∷ γ) qc) hd
外层记录被消去到内层读取，内层读取喂给判定引理；整个证明把截断消去为序数的相等，而序数相等是命题。
atCarrier : Σ[ c ∶ S ] Outer c → β ≡ birth (z .fst) (z .snd)
atCarrier (c , (hg , (hn , hi))) =
rec₁ (setIsSet β (birth (z .fst) (z .snd)))
(atInner c hg (λ k → lower (hn k))) hi
反向证明假设槽位 b 中的序数等于 x 的元语言诞生层。两个存在见证分别是打包后的层 Lset β 及其打包后的可定义幂集。按照存在满足关系的要求，它们被置于命题截断之下，所以这项构造并不声称公式具有唯一确定的见证。
BirthAt-in : IsOrd β → β ≡ birth (z .fst) (z .snd) → ⟨ γ ⊨ BirthAt b x ⟩
BirthAt-in ob e = ∣ towerS β ob
, (hg , (hn , ∣ powS β ob , (hd , hm) ∣₁)) ∣₁
where
hg : ⟨ (towerS β ob ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩
抬升指数处的层图成立，因为打包后的层按呈现的定义等式就是该指数处的层。
hg = Lset-defines zero (suc b) (towerS β ob ∷ γ) ob (towerS-fst β ob)
若 x 属于 Lset β，把 β 换成 birth x 后，它就会出现在严格低于 stage x = sucV (birth x) 的层。这与 stage-earliest 矛盾，从而给出 BirthAt 所需的非成员关系。
hn : ⟨ z .fst ∈ (towerS β ob) .fst ⟩ → Lift {j = ℓ-suc ℓ} ⊥₀
hn k = lift (stage-earliest (z .fst) (z .snd) β ob
(subst (λ u → ⟨ z .fst ∈ u ⟩) (towerS-fst β ob) k)
(subst (λ u → ⟨ u ∈ stage (z .fst) (z .snd) ⟩) (sym e)
(birth-stage (z .fst) (z .snd))))
DefAt 的层等式把它的满足命题认同为与 𝒟ₒ (Lset β) 的相等。powS β ob 的投影等式恰好给出这项相等，因此封装后的可定义幂集满足所需子句。
hd : ⟨ (powS β ob ∷ towerS β ob ∷ γ) ⊨ DefAt zero (suc zero) ⟩
hd = subst ⟨_⟩
(sym (DefAt-stage β ob zero (suc zero)
(powS β ob ∷ towerS β ob ∷ γ) (towerS-fst β ob)))
(powS-fst β ob)
最后，birth-mem 把 x 放入 Lset (sucV (birth x))。先把候选序数换成诞生序数，再使用 Lset-suc，最后使用打包可定义幂集的投影等式，就把这条成员关系搬运到第二个见证中。结合向外读式，这证明了在候选槽位被假设为序数时，BirthAt 精确描述诞生序数；它既不在内部添加序数性，也不给出规范的存在见证。
hm : ⟨ z .fst ∈ (powS β ob) .fst ⟩
hm = subst (λ u → ⟨ z .fst ∈ u ⟩) (sym (powS-fst β ob))
(subst (λ u → ⟨ z .fst ∈ u ⟩) (Lset-suc β)
(subst (λ u → ⟨ z .fst ∈ Lset (sucV u) ⟩) (sym e)
(birth-mem (z .fst) (z .snd))))
任意元数处的诸码，位于槽位所持的载体上
逐码识别式合并两个子句：第一个从码读取元数数码，第二个检查该码见证工作字母表上的一条公式。二者合起来说该码是某个元数处的真公式码。
isCodeAnyAt : ∀ {n} → Fin n → Fin n → Formula S n
isCodeAnyAt c w = arityNumAtL c ∧̇ hasWitnessAt w c
向内读式以工作集 A、两个槽位、与 A 对齐的环境、元数 k 的公式、以及认同码槽与该公式键的等式为参数。它填充两个合取项。
module _ (A : S) where
codeAnyAt-in : ∀ {n k} (c w : Fin n) (γ : Vec S n)
→ (lookup w γ) .fst ≡ A .fst
→ (ψ : Formula ⟪ A .fst ⟫ k) → (lookup c γ) .fst ≡ (keyS A ψ) .fst
→ ⟨ γ ⊨ isCodeAnyAt c w ⟩
两个合取项由各自的向内读式填充：元数读法名指自然数与码，见证读式确认该公式在已对齐的字母表上。
codeAnyAt-in {k = k} c w γ qw ψ qc =
arityNumAtL-in c γ k (codeS A ψ) qc , witnessAt-in A w c γ ψ qw qc
向外读法恢复截断的码见证：某个元数与某条公式产生此键。截断数据保持在命题截断之内。
codeAnyAt-out : ∀ {n} (c w : Fin n) (γ : Vec S n)
→ (lookup w γ) .fst ≡ A .fst
→ ⟨ γ ⊨ isCodeAnyAt c w ⟩
→ ⟨ IsKeyOverAny A (lookup c γ) ⟩
codeAnyAt-out c w γ qw (hk , hw) =
证明消去元数读取为自然数与码的对，再把见证读法映入码层级的截断存在。
rec₁ squash₁ step (arityNumAtL-out c γ hk)
where
step : Σ[ m ∶ ℕ ] Σ[ z ∶ S ] ((lookup c γ) .fst ≡ pr (# m) (z .fst))
→ ⟨ IsKeyOverAny A (lookup c γ) ⟩
step (m , (z , qz)) = map₁ (λ { (ψ , q) → m , (ψ , q) })
见证读法的消去在正确元数处恢复公式与码等式，完成截断存在。
(witnessAt-out A w c γ qw hw m z qz)
那个集合，一次外延
CodesAt c w 并不构造码集。它借助 extAt 描述已经占据槽位 c 的集合：一个元素属于该集合，当且仅当它是槽位 w 所持载体上某个有限元数公式的键。这样便在外延意义上把槽位取值确定为 AllCodes A，而成员关系读式所用的每个公式见证仍处于命题截断之下。
CodesAt : ∀ {n} → Fin n → Fin n → Formula S n
CodesAt c w = extAt c (isCodeAnyAt zero (suc w))
码集的向外读法说：该槽位恰持有工作字母表的码集。证明沿两个方向作外延性。
module _ (A : S) {n : ℕ} (c w : Fin n) (γ : Vec S n)
(qw : (lookup w γ) .fst ≡ A .fst) where
CodesAt-out : ⟨ γ ⊨ CodesAt c w ⟩ → lookup c γ ≡ AllCodes A
CodesAt-out h = extensionalL step
where
对第一项包含，codeAnyAt-out 把描述槽位中的成员关系读成「该元素是某条公式之键」的命题截断。AllCodes-in 恰把这项断言化为对固定元语言集合 AllCodes A 的成员关系，并不选出某个特定解码。
step : (x : S) → (x ∈ˢ lookup c γ) ≡ (x ∈ˢ AllCodes A)
step x = ⇔toPath
(λ hx → AllCodes-in A x
(codeAnyAt-out A zero (suc w) (x ∷ γ) qw
(extAt-out c (isCodeAnyAt zero (suc w)) γ h x hx)))
为证明反向包含，AllCodes A 中的成员关系只给出一个元数与一条公式的命题截断，并说明给定元素是该公式的键。逐码公式的满足本身是命题，所以证明可以在此处消去该截断并应用 codeAnyAt-in，但不会提取出一份指定的解码。
(λ hx → extAt-in c (isCodeAnyAt zero (suc w)) γ h x
(rec₁ (((x ∷ γ) ⊨ isCodeAnyAt zero (suc w)) .snd)
(λ { (k , (ψ , q)) →
codeAnyAt-in A {k = k} zero (suc w) (x ∷ γ) qw ψ q })
(AllCodes-out A x hx)))
反过来，设槽位 c 的取值等于 AllCodes A。要证明 CodesAt，只需给出外延公式要求的两条成员关系蕴含：槽位中的元素满足逐码谓词，而满足该谓词的对象属于槽位。
CodesAt-in : lookup c γ ≡ AllCodes A → ⟨ γ ⊨ CodesAt c w ⟩
CodesAt-in q = extAt-in-both c (isCodeAnyAt zero (suc w)) γ into back
where
into : (x : S) → ⟨ x .fst ∈ (lookup c γ) .fst ⟩
→ ⟨ (x ∷ γ) ⊨ isCodeAnyAt zero (suc w) ⟩
对第一条蕴含，集合等式把槽位成员关系化为 AllCodes A 中的成员关系。后者只在命题截断下给出公式见证；由于目标是 isCodeAnyAt 的满足命题，可以把截断消去到这个目标中。
into x hx = rec₁ (((x ∷ γ) ⊨ isCodeAnyAt zero (suc w)) .snd)
(λ { (k , (ψ , qk)) →
codeAnyAt-in A {k = k} zero (suc w) (x ∷ γ) qw ψ qk })
(AllCodes-out A x (subst (λ u → ⟨ x .fst ∈ u .fst ⟩) q hx))
对反向蕴含，codeAnyAt-out 把满足关系读成「候选对象是某条公式之键」的命题截断。AllCodes-in 正用这条截断断言证明对象属于 AllCodes A，随后集合等式把结论搬回槽位 c。
back : (x : S) → ⟨ (x ∷ γ) ⊨ isCodeAnyAt zero (suc w) ⟩
→ ⟨ x .fst ∈ (lookup c γ) .fst ⟩
back x hx = subst (λ u → ⟨ x .fst ∈ u .fst ⟩) (sym q)
(AllCodes-in A x (codeAnyAt-out A zero (suc w) (x ∷ γ) qw hx))
层处的序，展开一次
在序数 δ 处，前章已经构造的 orderAt δ 比较 Lset δ 的元素。把该序搬到命名构造所需的小载体后，stepAt δ 据此在 New δ，即 Lset (sucV δ) 的元素上构造局部严格良序 stepOrder δ。
stepOrder : (δ : V ℓ) → IsOrd δ → SWO (New δ)
stepOrder δ oδ = stepAt δ (carry (Lset δ) (orderAt δ oδ))
若 δ ≡ δ'，则 δ 处的 Under 比较可搬运到 δ' 处。依赖对的路径同时认同两份序数性证明；这是因为 IsOrd 是命题。因此，搬运后的比较不依赖于所选的序数性证书。
stepMoved : (δ δ' : V ℓ) (e : δ ≡ δ') (o : IsOrd δ) (o' : IsOrd δ') (x y : V ℓ)
→ Under δ (stepOrder δ o) x y → Under δ' (stepOrder δ' o') x y
stepMoved δ δ' e o o' x y =
subst (λ p → Under (p .fst) (stepOrder (p .fst) (p .snd)) x y)
(Σ≡Prop isPropIsOrd {u = δ , o} {v = δ' , o'} e)
设可构造集合 x 的诞生序数属于序数 α。那么该诞生序数的后继要么属于 α，要么等于 α。由于 x 属于以该后继为指标的层，这两种情形都会把 x 放入 Lset α。
bornIn : (α : V ℓ) → IsOrd α → (x : V ℓ) (p : ⟨ isL x ⟩)
→ ⟨ birth x p ∈ α ⟩ → ⟨ x ∈ Lset α ⟩
bornIn α oα x p h = reach (suc∈or≡ (birth x p) α (birth-ord x p) oα h)
where
reach : ⟨ sucV (birth x p) ∈ α ⟩ ⊎ (sucV (birth x p) ≡ α) → ⟨ x ∈ Lset α ⟩
suc∈or≡ 给出的两种情形完成了论证。若诞生序数的后继属于 α，单调性把 birth-mem 推到 Lset α；若该后继等于 α，沿等式搬运即可直接得到同一成员关系。
reach (inl k) = Lset-mono {α = α} {β = sucV (birth x p)} k
{x = x} (birth-mem x p)
reach (inr e) = subst (λ w → ⟨ x ∈ Lset w ⟩) e (birth-mem x p)
现在固定环境序数 α。Lset α 的每个元素都有一个低于 α 的诞生序数，因此 orderAt α 的递归方程所需的较早层序恰在相应指标处可用。于是，我们可以把该方程直接表成两个元素的诞生层比较。
module _ (α : V ℓ) (oα : IsOrd α) where
private module Fam = Family α (λ δ _ → orderAt δ) oα
每个层元素可构造，由层的可构造性与沿成员关系的传递性而来。
memberL : (a : Mem (Lset α)) → ⟨ isL (a .fst) ⟩
memberL a = Lset→isL α oα (a .fst) (a .snd)
由于 Lset α 的每个元素 a 都可构造，它都有诞生序数。把这个序数记为 bornOf a；展开 α 处的序时，它将作为第一比较键。
bornOf : (a : Mem (Lset α)) → V ℓ
bornOf a = birth (a .fst) (memberL a)
事实 bornOf a ∈ α 有两项作用。它先确认该诞生序数可在展开 orderAt α 时充当较早指标；随后又使 bornIn 能从对象语言的诞生描述恢复 a 对环境层的成员关系。
bornMem : (a : Mem (Lset α)) → ⟨ bornOf a ∈ α ⟩
bornMem a = Fam.bornAt a .snd
展开等式是本章的连接点。它说：α 处的序在 a 与 b 之间成立，恰当 a 的诞生序数严格低于 b 的诞生序数，或二者共享同一诞生序数且该诞生序数处的局部步进序把 a 置于 b 之下。
order-unfold : (a b : Mem (Lset α))
→ relOf (orderAt α oα) a b
≡ ( ⟨ bornOf a ∈ bornOf b ⟩
⊎ ( (bornOf b ≡ bornOf a)
× Under (bornOf a) (stepOrder (bornOf a)
证明用 orderAt-step 展开一层成员关系递归，再对其底层关系应用同余。因此，这个两分等式来自前章已经构造的序；此处既不重新构造也不重新证明该严格良序。
(mem-ord {A = α} oα (bornOf a) (bornMem a)))
(a .fst) (b .fst) ) )
order-unfold a b = cong (λ z → relOf (z oα) a b) (orderAt-step α)
元素到载体的包装把每个层元素打包为载体元素，使公式环境能容纳它。
opaque
memS : (α : V ℓ) (oα : IsOrd α) → Mem (Lset α) → S
memS α oα a = a .fst , memberL α oα a
第一投影等式确认包装保持底层集合。
memS-fst : (α : V ℓ) (oα : IsOrd α) (a : Mem (Lset α))
→ (memS α oα a) .fst ≡ a .fst
memS-fst α oα a = refl
诞生呈现把诞生序数连同从外围序数 α 运来的可构造性打包。
bornS : (α : V ℓ) (oα : IsOrd α) → ⟨ isL α ⟩ → Mem (Lset α) → S
bornS α oα pα a = bornOf α oα a
, isL-trans {x = α} {y = bornOf α oα a} (bornMem α oα a) pα
第一投影等式确认包装保持诞生序数。
bornS-fst : (α : V ℓ) (oα : IsOrd α) (pα : ⟨ isL α ⟩) (a : Mem (Lset α))
→ (bornS α oα pα a) .fst ≡ bornOf α oα a
bornS-fst α oα pα a = refl
诞生等式确认打包的诞生与打包元素的计算诞生一致。
bornS-birth : (α : V ℓ) (oα : IsOrd α) (pα : ⟨ isL α ⟩) (a : Mem (Lset α))
→ (bornS α oα pα a) .fst
≡ birth ((memS α oα a) .fst) ((memS α oα a) .snd)
bornS-birth α oα pα a = refl
那个序，被描述出来，而那一步取作参数
步进公式类型是四槽公式族，以载体槽、表槽与两个比较槽为参数。
StpFo : Type (ℓ-suc ℓ)
StpFo = ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
步进公式的向外充分性读式相对于序数载体 d、表 f 与两个被比较对象陈述。它对表的假设是：在 d 处记录的每个取值 r 都实现层关系 IsRel d r。由 Stp 的满足只能推出相应 Under 比较的命题截断。
StpOut StpIn : StpFo → Type (ℓ-suc ℓ)
StpOut Stp = ∀ {n} (d f u v : Fin n) (γ : Vec S n) (od : IsOrd ((lookup d γ) .fst))
→ ((r : S) → ⟨ pr ((lookup d γ) .fst) (r .fst) ∈ (lookup f γ) .fst ⟩
→ IsRel ((lookup d γ) .fst) r)
→ ⟨ γ ⊨ Stp d f u v ⟩
向外方向有意返回 ∥ Under ... ∥₁，所以它只给出局部比较的存在，而不选择规范见证。向内方向的输入不同：调用方给出一个特定取值 r、表在 d 处记录它的证据，以及 r 实现当地关系的证明。
→ ∥ Under ((lookup d γ) .fst) (stepOrder ((lookup d γ) .fst) od)
((lookup u γ) .fst) ((lookup v γ) .fst) ∥₁
StpIn Stp = ∀ {n} (d f u v : Fin n) (γ : Vec S n) (od : IsOrd ((lookup d γ) .fst))
→ (r : S) → ⟨ pr ((lookup d γ) .fst) (r .fst) ∈ (lookup f γ) .fst ⟩
→ IsRel ((lookup d γ) .fst) r
→ Under ((lookup d γ) .fst) (stepOrder ((lookup d γ) .fst) od)
((lookup u γ) .fst) ((lookup v γ) .fst)
→ ⟨ γ ⊨ Stp d f u v ⟩
模块 Ordered 假设一条抽象步进公式及其两条读式。因此，下文给出的是诞生层优先规则的有条件翻译：它从同生比较的充分性推出整个层比较的充分性，却不在本章声称任何具体步进公式已经满足该接口。
module Ordered (Stp : StpFo) (stp-out : StpOut Stp) (stp-in : StpIn Stp) where
新绑定的四个对象是被比较集合 u,v 及其候选诞生序数 du,dv。前两项断言 BirthAt du u 与 BirthAt dv v；只有后续读式提供 du、dv 的序数性时，这两项才把候选者认同为相应诞生层。
OrdBody : ∀ {n} → Term S n → Fin n → Formula S (suc (suc (suc (suc n))))
OrdBody tb f =
BirthAt (suc zero) (sh3 zero)
∧̇ ( BirthAt zero (sh2 zero)
∧̇ ( (var (suc zero) ∈̇ tm4 tb)
接下来的两项要求两个候选诞生层都属于词项 tb 所指称的阶段。最后的析取复现诞生层优先规则：要么 du ∈ dv，要么 dv ≡ du 且外部给出的步进公式在这个共同载体处比较 u 与 v。这里没有断言 u 与 v 之间的集合成员关系。
∧̇ ( (var zero ∈̇ tm4 tb)
∧̇ ( (var (suc zero) ∈̇ var zero)
∨̇ ( (var zero ≐ var (suc zero))
∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ) ) )
CondCore 先以存在量词绑定两个被比较对象 u 与 v，对公式要求槽位 z 中的实参是二者的有序对。随后两个存在量词绑定它们的候选诞生层，再由 OrdBody 检查诞生层优先的比较。四个见证都位于存在公式的满足语义下，因此都经过命题截断。
opaque
CondCore : ∀ {n} → Fin n → Term S n → Fin n → Formula S n
CondCore z tb f =
∃̇ ( ∃̇ ( prAtL (sh2 z) (suc zero) zero ∧̇ ∃̇ (∃̇ (OrdBody tb f)) ) )
这条描述说了什么，两个方向
为读取 CondCore，固定由 tb 指称的序数阶段及其上的一张表。Values 保证每个已记录取值都实现相应的局部关系；Entries 则只说阶段以下每个载体处都记录着某个取值。这正是后面两个方向所用的假设。
module _ {n : ℕ} (z : Fin n) (tb : Term S n) (f : Fin n) (γ : Vec S n)
(oα : IsOrd ((⟦ tb ⟧ γ) .fst))
(vals : Values (lookup f γ) ((⟦ tb ⟧ γ) .fst))
(ents : Entries (lookup f γ) ((⟦ tb ⟧ γ) .fst)) where
private
阶段序数被命名以便直接引用。
α : V ℓ
α = (⟦ tb ⟧ γ) .fst
平移引理确认四槽改名保持阶段词项的指称。
shift : (u v du dv : S) → ⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ) ≡ ⟦ tb ⟧ γ
shift u v du dv = tm4-val tb u v du dv γ
对 α 以下的载体 d，Entries 只给出一项经过命题截断的表取值。这个辅助引理可以把该截断消去到任意命题 P 中：对恢复出的每个 r，Values 证明 IsRel d r，续至函数再用已记录的有序对及这份证明得到 P。
value : (d : S) → ⟨ d .fst ∈ α ⟩ → (P : hProp (ℓ-suc ℓ))
→ ((r : S) → ⟨ pr (d .fst) (r .fst) ∈ (lookup f γ) .fst ⟩
→ IsRel (d .fst) r → ⟨ P ⟩)
→ ⟨ P ⟩
value d hd P k = rec₁ ⟨ P ⟩isProp
具体地说，ents d hd 给出由取值 r 及其表条目组成的命题截断。这里只因 P 是 hProp 才能消去命题截断；随后 vals 提供续至函数所需的关系实现证明。该构造不会在这个命题之外选定一个表取值。
(λ { (r , hr) → k r hr (vals d r hd hr) }) (ents d hd)
深层满足类型读取有序体在由两个比较对象及其诞生序数组成的四槽环境处的满足。
Deep : (u v du : S) → S → Type (ℓ-suc ℓ)
Deep u v du dv = ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ OrdBody tb f ⟩
两条读式以相反方向使用 CondCore 的同一个定义方程。向外时，四个存在绑定被读成一对元素及两个候选诞生层；向内时，一项已有的 Related 比较提供这些绑定。只有同生分支会用到对 Stp 的两条假设读式。
opaque
unfolding CondCore
向外读式依次打开四层存在见证：先是被比较对象 u,v，再是候选诞生层 du,dv。每个见证都只能通过命题截断取得，而每次消去的目标都是命题 Related α ...。最内层数据随后交给数学比较论证。
CondCore-out : ⟨ γ ⊨ CondCore z tb f ⟩ → ⟨ Related α ((lookup z γ) .fst) ⟩
CondCore-out = rec₁ ((Related α ((lookup z γ) .fst)) .snd)
(λ { (u , hv) → rec₁ ((Related α ((lookup z γ) .fst)) .snd)
(λ { (v , (hp , hdu)) → rec₁ ((Related α ((lookup z γ) .fst)) .snd)
(λ { (du , hdv) → rec₁ ((Related α ((lookup z γ) .fst)) .snd)
局部名称 Goal 记录这样一个命题：槽位 z 中的实参满足元语言谓词 Related α。恢复出的四个见证给出有序对等式与 OrdBody 的满足，这两项被交给 atDeep；余下证明将把它们转化为该关联命题。
(λ { (dv , hd) → atDeep u v du dv hp hd }) hdv }) hdu }) hv })
where
Goal : Type (ℓ-suc ℓ)
Goal = ⟨ Related α ((lookup z γ) .fst) ⟩
四个存在见证被消去到命题 Related 之后，向外证明取得两部分信息：hp 说明实参是 u 与 v 的编码有序对；深层记录则说明 du,dv 是环境层以下的候选诞生层，并满足诞生层优先的比较。这些见证只在命题目标中使用；证明并未选出规范的有序对或规范的诞生数据。
atDeep : (u v du dv : S)
→ ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩
→ Deep u v du dv → Goal
atDeep u v du dv hp (hbu , (hbv , (hmu₀ , (hmv₀ , hcmp)))) =
subst (λ w → ⟨ Related α w ⟩) (sym qz)
配对公式的充分性把槽位 z 中的集合认同为 pr (u .fst) (v .fst)。正是这条等式，而非 u 与 v 之间的等式，使证明能把目标改写为该表示对的 Related α，再分析其中的诞生层比较。
(rec₁ ((Related α (pr (u .fst) (v .fst))) .snd) atCase hcmp)
where
qz : (lookup z γ) .fst ≡ pr (u .fst) (v .fst)
qz = subst ⟨_⟩ (prAtL-adequate (sh2 z) (suc zero) zero (v ∷ u ∷ γ)) hp
第一个诞生层在序数中的成员关系沿环境移位搬运：诞生层的移位读法与非移位读法在底层集合上一致。
hmu : ⟨ du .fst ∈ α ⟩
hmu = subst (λ w → ⟨ du .fst ∈ w .fst ⟩) (shift u v du dv) hmu₀
第二个诞生层由同一移位搬运，于是两个诞生层都属于该序数。
hmv : ⟨ dv .fst ∈ α ⟩
hmv = subst (λ w → ⟨ dv .fst ∈ w .fst ⟩) (shift u v du dv) hmv₀
第一个诞生层是序数：它属于该序数，而序数的元素是序数。
odu : IsOrd (du .fst)
odu = mem-ord {A = α} oα (du .fst) hmu
第二个诞生层由同样论证是序数。
odv : IsOrd (dv .fst)
odv = mem-ord {A = α} oα (dv .fst) hmv
诞生公式的读取引理现在适用于第一个诞生层：在其序数性下，诞生公式的满足把被记录的层认同为第一个对象的真正诞生序数。
qu : du .fst ≡ birth (u .fst) (u .snd)
qu = BirthAt-out (suc zero) (sh3 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) hbu odu
同样的读取适用于第二个诞生层与第二个对象。
qv : dv .fst ≡ birth (v .fst) (v .snd)
qv = BirthAt-out zero (sh2 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) hbv odv
现在可以把第一个对象视为 Lset α 的元素。其可构造性证据已由 u 携带；新增的事实是它属于环境层，而这由 bornIn 从「已经认出的诞生序数属于 α」推出。
a : Mem (Lset α)
a = u .fst , bornIn α oα (u .fst) (u .snd)
(subst (λ w → ⟨ w ∈ α ⟩) qu hmu)
第二个对象以同样方式打包。
c : Mem (Lset α)
c = v .fst , bornIn α oα (v .fst) (v .snd)
(subst (λ w → ⟨ w ∈ α ⟩) qv hmv)
打包元素 a 与 u 有相同的底层集合，但其可构造性证明来自层成员关系。birth-proof 表达这份证据的证明无关性，说明从 a 算出的诞生层与从 u 算出的诞生层相同；再与 qu 复合，便把它认同为记录的层 du。
qa : bornOf α oα a ≡ du .fst
qa = birth-proof (u .fst) (memberL α oα a) (u .snd) ∙ sym qu
打包后的第二个对象的诞生序数与被记录的第二个诞生层一致。
qc : bornOf α oα c ≡ dv .fst
qc = birth-proof (v .fst) (memberL α oα c) (v .snd) ∙ sym qv
此时只需证明元语言比较 relOf (orderAt α oα) a c。序表接口随后把这项比较送到命题：两个底层集合的编码有序对属于 Related α。这一步尚未选取任何对象语言关系集合。
fill : relOf (orderAt α oα) a c → ⟨ Related α (pr (u .fst) (v .fst)) ⟩
fill = related-in α oα a c
OrdBody 编码的比较恰有 orderAt 一次展开所得的两支。若 du ∈ dv，同一视 qa 与 qc 把它改写成 a 与 c 的「诞生更早」分支；沿 order-unfold 搬运后，即得二者的层序比较。
atCase : ⟨ du .fst ∈ dv .fst ⟩
⊎ ( (dv .fst ≡ du .fst)
× ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ⟩ )
→ ⟨ Related α (pr (u .fst) (v .fst)) ⟩
atCase (inl h) = fill (transport (sym (order-unfold α oα a c))
在同生分支中，OrdBody 给出抽象公式 Stp 的满足。把公共诞生层的序数性与 Values 假设交给 stp-out，只能得到一项经过命题截断的 Under 比较。由于 Related 是命题，可以把这项截断消去到其中；该论证既不考察 Stp 如何取得表值，也不从中提取表值。
(inl (subst2 (λ p q → ⟨ p ∈ q ⟩) (sym qa) (sym qc) h)))
atCase (inr (e , hs)) = rec₁
((Related α (pr (u .fst) (v .fst))) .snd) atUnder
(stp-out (suc zero) (sh4 f) (sh3 zero) (sh2 zero)
((dv ∷ du ∷ v ∷ u ∷ γ)) odu (λ r hr → vals du r hmu hr) hs)
给定记录的公共诞生层处的一项 Under 比较，证明还须把它与打包元素 a 所带的诞生层对齐。对齐之后，它给出 order-unfold 的同生分支；所得 orderAt 比较再由 Related 表示。
where
atUnder : Under (du .fst) (stepOrder (du .fst) odu) (u .fst) (v .fst)
→ ⟨ Related α (pr (u .fst) (v .fst)) ⟩
atUnder und = fill (transport (sym (order-unfold α oα a c))
(inr (qc ∙ e ∙ sym qa
这次对齐使用两条载体序数之间的等式 qa。stepMoved 沿该等式搬运局部比较，并借助证明无关性认同两份序数性证明；这里既不使用公共序数的传递性，也不构造新的局部序。
, stepMoved (du .fst) (bornOf α oα a) (sym qa) odu
(mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a))
(u .fst) (v .fst) und)))
在向内方向，Related α z 包含一份序数性证明，以及命题截断下的如下数据：Lset α 的两个元素 a,c、说明 z 是二者编码有序对的等式，以及二者的 Ordering 比较。Pairs 恰为这份载荷取名，使它只能被消去到正在构造的满足命题中。
private
Pairs : IsOrd α → Type (ℓ-suc ℓ)
Pairs o = Σ[ a ∶ Mem (Lset α) ] ∥ (Σ[ c ∶ Mem (Lset α) ]
( ((lookup z γ) .fst ≡ pr (a .fst) (c .fst)) × ⟨ Ordering α o a c ⟩ )) ∥₁
向内读式把 Related 的截断内容消去到 CondCore 的满足命题中。局部取得序数性证明与一对被表示的元素后，atRel 重建四个存在见证及诞生层优先比较；证明不会产出对表示元素的全局选择。
CondCore-in : ⟨ Related α ((lookup z γ) .fst) ⟩ → ⟨ γ ⊨ CondCore z tb f ⟩
CondCore-in = rec₁ ((γ ⊨ CondCore z tb f) .snd) atOrd
where
atRel : (o : IsOrd α) (a c : Mem (Lset α))
→ (lookup z γ) .fst ≡ pr (a .fst) (c .fst)
环境序数性 oα 已是整条读式的假设。此处的局部证明从层词项的取值中取出的是可构造性分量 pα，随后向表索取第一个元素诞生层处的一个取值。由于目标是满足命题，表值的仅仅存在可以消去到其中。
→ ⟨ Ordering α o a c ⟩ → ⟨ γ ⊨ CondCore z tb f ⟩
atRel o a c q hord =
value (bornS α oα pα a) hmu (γ ⊨ CondCore z tb f) atValue
where
pα : ⟨ isL α ⟩
每个词项都在结构 𝒮ʟ 中解释，而该结构的元素由底层集合及其可构造性证据组成。因此，⟦ tb ⟧ γ 的第二投影给出 isL α；这是词项语义值的一部分，并非另一项满足假设。
pα = (⟦ tb ⟧ γ) .snd
现在局部给出 CondCore 的见证：u,v 把两个层元素封装为 𝒮ʟ 的元素，du,dv 则封装它们真正的诞生序数。它们只是这次命题证明所用的见证，并非从 Related 导出的规范选择。
u v du dv : S
u = memS α oα a
v = memS α oα c
du = bornS α oα pα a
dv = bornS α oα pα c
Lset α 的每个元素，其真正诞生序数都低于 α。由于 bornS 的第一投影就是该序数，同一成员关系陈述也适用于放入槽位 du 的值；对象语言子句读取的正是这个形式。
hmu : ⟨ du .fst ∈ α ⟩
hmu = subst (λ w → ⟨ w ∈ α ⟩) (sym (bornS-fst α oα pα a))
(bornMem α oα a)
第二个元素的诞生层经同样搬运属于该序数。
hmv : ⟨ dv .fst ∈ α ⟩
hmv = subst (λ w → ⟨ w ∈ α ⟩) (sym (bornS-fst α oα pα c))
(bornMem α oα c)
第一个诞生层是序数，因为它落在该序数之内。
odu : IsOrd (du .fst)
odu = mem-ord {A = α} oα (du .fst) hmu
第二个诞生层由同样读取是序数。
odv : IsOrd (dv .fst)
odv = mem-ord {A = α} oα (dv .fst) hmv
展开已经构造好的层序，得到其两分的字典序规则：要么 a 的诞生严格早于 c，要么二者诞生层相同，且该公共诞生层处的局部 stepOrder 把 a 的底层集合排在 c 的底层集合之前。
cmp : ⟨ bornOf α oα a ∈ bornOf α oα c ⟩
⊎ ( (bornOf α oα c ≡ bornOf α oα a)
× Under (bornOf α oα a) (stepOrder (bornOf α oα a)
(mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a)))
(a .fst) (c .fst) )
该比较沿「两份序数性证明的同一视」搬运严格读法而得，因为序数性是命题，两份证明描述的是同一个序数。
cmp = transport (order-unfold α oα a c)
(strict α oα a c (subst (λ o' → ⟨ Ordering α o' a c ⟩)
(isPropIsOrd α o oα) hord))
Related 所含的等式把实参认同为 a 与 c 的底层集合所成的有序对。memS 的第一投影等式把这两个端点改写为放入槽位 u 与 v 的值，从而恰好得到 CondCore 所需的配对子句。
hp : ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩
hp = subst ⟨_⟩
(sym (prAtL-adequate (sh2 z) (suc zero) zero (v ∷ u ∷ γ)))
(q ∙ cong₂ pr (sym (memS-fst α oα a)) (sym (memS-fst α oα c)))
为填入第一条 BirthAt 子句，向内读式给出其充分性引理所需的两项事实：du 是序数，且其底层集合恰是 u 的诞生序数。公式本身仍不断言序数性，也不选择最小层。
hbu : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ BirthAt (suc zero) (sh3 zero) ⟩
hbu = BirthAt-in (suc zero) (sh3 zero) (dv ∷ du ∷ v ∷ u ∷ γ) odu
(bornS-birth α oα pα a)
第二个诞生层的诞生公式在同一深环境中填充。
hbv : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ BirthAt zero (sh2 zero) ⟩
hbv = BirthAt-in zero (sh2 zero) (dv ∷ du ∷ v ∷ u ∷ γ) odv
(bornS-birth α oα pα c)
在同生分支中，cmp 给出一项 Under 比较，其载体是 a 的真正诞生层，两个端点是 a,c 的底层集合。但步进公式读在封装值 du,u,v 上，因此必须把载体与两个端点都搬到这些表示中。
moved : Under (bornOf α oα a) (stepOrder (bornOf α oα a)
(mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a)))
(a .fst) (c .fst)
→ Under (du .fst) (stepOrder (du .fst) odu) (u .fst) (v .fst)
moved und = subst2 (λ p r → Under (du .fst) (stepOrder (du .fst) odu) p r)
两个端点的搬运使用 memS 的底层集合外显等式。载体的搬运使用 bornS-fst 与 stepMoved；后者的依赖路径还利用 IsOrd 是命题来认同两份序数性证明。这里不涉及传递性论证。
(sym (memS-fst α oα a)) (sym (memS-fst α oα c))
(stepMoved (bornOf α oα a) (du .fst) (sym (bornS-fst α oα pα a))
(mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a)) odu
(a .fst) (c .fst) und)
Entries 在第一个诞生层处给出一个仅仅存在的表值 r，而 Values 证明任一这样的记录值都实现 IsRel。对每份局部载荷，atValue 插入两个元素及其两个诞生层，构造 CondCore 的满足。同生分支把该表值专门传给 stp-in；它不会成为全局选定的取值。
atValue : (r : S) → ⟨ pr (du .fst) (r .fst) ∈ (lookup f γ) .fst ⟩
→ IsRel (du .fst) r → ⟨ γ ⊨ CondCore z tb f ⟩
atValue r hr hrel = ∣ u , ∣ v , (hp , ∣ du , ∣ dv
, (hbu , (hbv , (hmu₀ , (hmv₀ , side)))) ∣₁ ∣₁) ∣₁ ∣₁
where
在 OrdBody 内，原环境之前增加了四个绑定，故层词项写成 tm4 tb。移位等式证明这个提升后的词项仍指称 α，于是把第一诞生层的已知成员关系搬成对象语言子句所需的确切形式。
hmu₀ : ⟨ du .fst ∈ (⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ)) .fst ⟩
hmu₀ = subst (λ w → ⟨ du .fst ∈ w .fst ⟩) (sym (shift u v du dv)) hmu
第二个诞生层经同一移位等式搬运。
hmv₀ : ⟨ dv .fst ∈ (⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ)) .fst ⟩
hmv₀ = subst (λ w → ⟨ dv .fst ∈ w .fst ⟩) (sym (shift u v du dv)) hmv
余下的子句必须复现 order-unfold 给出的同一两支：诞生更早，或诞生相同后采用局部步进比较。辅助函数把这次分情形保持在满足命题内部，使见证与任何截断的表项都只在允许的命题目标中使用。
atCmp : ⟨ bornOf α oα a ∈ bornOf α oα c ⟩
⊎ ( (bornOf α oα c ≡ bornOf α oα a)
× Under (bornOf α oα a) (stepOrder (bornOf α oα a)
(mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a)))
(a .fst) (c .fst) )
在诞生更早分支中，bornS 的外显等式把真正诞生层之间的元语言成员关系改写为 du 与 dv 之间的成员关系。所得证明进入对象语言析取的左支，而该析取的满足经过命题截断。
→ ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ ( (var (suc zero) ∈̇ var zero)
∨̇ ( (var zero ≐ var (suc zero))
∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ⟩
atCmp (inl h) = ∣ inl (subst2 (λ p q → ⟨ p ∈ q ⟩)
(sym (bornS-fst α oα pα a)) (sym (bornS-fst α oα pα c)) h) ∣₁
在同生分支中，诞生层等式被改写为 dv 与 du 之间的等式。随后，向内充分性假设 stp-in 使用这个特定的记录值 r、它在表中的成员关系、它的 IsRel 证明，以及搬运后的 Under 比较，填入局部步进公式。正是在这一方向上，证明手中有一个具体的局部表值。
atCmp (inr (e , und)) = ∣ inr
( bornS-fst α oα pα c ∙ e ∙ sym (bornS-fst α oα pα a)
, stp-in (suc zero) (sh4 f) (sh3 zero) (sh2 zero)
(dv ∷ du ∷ v ∷ u ∷ γ) odu r hr hrel (moved und) ) ∣₁
把这项两分翻译施于 cmp，便完成 OrdBody 的比较子句。它与两条诞生描述及两条低于 α 的界条件共同给出 CondCore 所需的深层记录，并未增加新的选择或序论断言。
side : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ ( (var (suc zero) ∈̇ var zero)
∨̇ ( (var zero ≐ var (suc zero))
∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ⟩
side = atCmp cmp
对级组装消去第二个元素的截断存在：对与 a 关联的每个候选 c，局部组装产出核心子句的满足。
atPairs : (o : IsOrd α) → Pairs o → ⟨ γ ⊨ CondCore z tb f ⟩
atPairs o (a , h) = rec₁ ((γ ⊨ CondCore z tb f) .snd)
(λ { (c , (q , hord)) → atRel o a c q hord }) h
Related 的外层载荷给出一份序数性证明 o，以及 Pairs o 的命题截断。由于 CondCore 的满足是命题，atOrd 可以消去这项截断，并把每个表示对交给 atPairs。对特定序数性证明的无关性已在更早处使用：借助 isPropIsOrd，把 o 与环境证明 oα 认同。
atOrd : Σ[ o ∶ IsOrd α ] ∥ Pairs o ∥₁ → ⟨ γ ⊨ CondCore z tb f ⟩
atOrd (o , h) = rec₁ ((γ ⊨ CondCore z tb f) .snd) (atPairs o) h
该规格把核心子句的满足与编码对的关联等同为命题路径，双向成立。
CondCore-spec : (γ ⊨ CondCore z tb f) ≡ Related α ((lookup z γ) .fst)
CondCore-spec = ⇔toPath CondCore-out CondCore-in
那个框架的两条假设，已解除
当层与表已经占据环境中的变元槽位时，使用 Cond 这一形式。新增的第零槽留给待检验的编码有序对，原有的层与表索引则越过它而提升。因此，Cond 不为层引入见证，而是引用外围语境已经提供的层。
Cond : ∀ {n} → Fin n → Fin n → Formula S (suc n)
Cond b f = CondCore zero (var (suc b)) (suc f)
Cond₀ B F 是分离所需的常元层形式。它唯一的存在绑定给出一个表值，等式子句把该值固定为常元 F；层本身已经是常元词项 B。余下的自由槽保存待检验的编码有序对。后续规格证明这一形式与 Cond 描述同一个 Related 比较，而这仍相对于给定的 StpOut 与 StpIn；两种形式都不构造层序本身。
Cond₀ : S → S → Formula S 1
Cond₀ B F =
∃̇ ( (var zero ≐ con F) ∧̇ CondCore (suc zero) (con B) zero )
变元形式检验一个可能的有序对 z，而层与序表仍留在周围环境中。假设该层是序数，且序表具有给定的取值读式与表项读式，其充分性等式便把 Cond 的满足关系与宿主层的类 Related 对应起来。因此，这条公式描述的是已经构造好的层序比较，并不构造新的序。
cond-spec : ∀ {n} (b f : Fin n) (γ : Vec S n) → IsOrd ((lookup b γ) .fst)
→ Values (lookup f γ) ((lookup b γ) .fst)
→ Entries (lookup f γ) ((lookup b γ) .fst)
→ (z : S) → ((z ∷ γ) ⊨ Cond b f) ≡ Related ((lookup b γ) .fst) (z .fst)
cond-spec b f γ ob vals ents z =
把 z 加到环境首部后，原有的每个槽位都向后移动一位。因此，核心在零号槽位读取 z，经 var (suc b) 读取层，并经 suc f 读取序表。作出这些平移后，CondCore 的一般等式直接给出所需的变元形式等式。
CondCore-spec zero (var (suc b)) (suc f) (z ∷ γ) ob vals ents
作分离时，周围环境只含候选者 z，所以常元形式必须绑定它所查阅的序表。若一个被绑定的元素 c 的底层集合等于固定序表 F 的底层集合，并且以 c 占据序表槽位时核心比较成立，那么 c 就是合适的见证。辅助命题 Held c 恰好合并这两项事实；c 是序表的代表，并非公式码。
module _ (B F : S) (oB : IsOrd (B .fst))
(vals : Values F (B .fst)) (ents : Entries F (B .fst)) (z : S) where
private
Held : S → Type (ℓ-suc ℓ)
Held c = (c .fst ≡ F .fst)
在两槽环境 c ∷ z ∷ [] 中，零号槽位是被绑定的序表代表，一号槽位是可能的有序对，而层由常元词项 con B 给出。这样的安排使同一个核心也能表达常元情形；向外读取时，必须把 F 的序表读式转移给与它外延相等的代表 c。
× ⟨ (c ∷ z ∷ []) ⊨ CondCore (suc zero) (con B) zero ⟩
向外方向从被绑定序表的命题截断存在见证出发。由于 Related 本身是命题，可以把这层命题截断消去到该目标中。辅助定义 atHeld 只在局部使用一个临时代表 c 及其两项 Held 事实；没有任何代表逸出这段证明，所以该论证既不产生规范见证，也不产生选择函数。
cond₀-out : ⟨ (z ∷ []) ⊨ Cond₀ B F ⟩ → ⟨ Related (B .fst) (z .fst) ⟩
cond₀-out = rec₁ ((Related (B .fst) (z .fst)) .snd) atHeld
where
atHeld : Σ[ c ∶ S ] Held c → ⟨ Related (B .fst) (z .fst) ⟩
atHeld (c , (qc , hc)) =
等式 qc 使两条序表读式可以在被绑定的代表与 F 之间转换，但方向相反。先把假设属于 c 的表项运输到 F，再由 vals 判定其取值实现该层关系。反过来，ents 给出 F 中一个经过命题截断的表项，而在这层截断之下作映射，把该表项运回 c。
CondCore-out (suc zero) (con B) zero (c ∷ z ∷ []) oB
(λ x r hx hp → vals x r hx
(subst (λ w → ⟨ pr (x .fst) (r .fst) ∈ w ⟩) qc hp))
(λ x hx → map₁ (λ { (r , hr) → r
, subst (λ w → ⟨ pr (x .fst) (r .fst) ∈ w ⟩) (sym qc) hr })
这些经过运输的读式正是向外读取核心比较所需的假设。把它们用于 hc，便得到关于 z 的 Related 事实。在整个转换中，表项见证始终处于命题截断之下；这已经足够，因为核心满足关系与所得关系断言都是命题。
(ents x hx))
hc
向内方向已经给定序表 F，所以可直接用它作存在见证，而它与常元序表的等式就是自反性。核心的向内读式随后把给定的 Related 事实化为以 F 占据序表槽位时的满足证明。这里是在命题截断内部构造见证，并非从截断信息中提取见证，也没有断言序表代表是唯一选定的。
cond₀-in : ⟨ Related (B .fst) (z .fst) ⟩ → ⟨ (z ∷ []) ⊨ Cond₀ B F ⟩
cond₀-in h = ∣ F , (refl
, CondCore-in (suc zero) (con B) zero (F ∷ z ∷ []) oB vals ents h) ∣₁
这两个蕴含给出 Cond₀ B F 的满足命题与 Related (B .fst) (z .fst) 之间的路径。因此，在同样的序数性、取值与表项假设下，常元公式具有与变元形式完全相同的数学读法。该等式涉及命题值含义，并不在语法上等同两条公式，也不为序表选择一个特出的呈现。
cond₀-spec : (B F : S) → IsOrd (B .fst)
→ Values F (B .fst) → Entries F (B .fst)
→ (z : S) → ((z ∷ []) ⊨ Cond₀ B F) ≡ Related (B .fst) (z .fst)
cond₀-spec B F oB vals ents z =
⇔toPath (cond₀-out B F oB vals ents z) (cond₀-in B F oB vals ents z)
通用序表构造现在可以在层与序表占据变元槽位时使用 Cond，并在二者作为固定常元时使用 Cond₀。由此得到的关系对象表示先前已构造的严格良序 orderAt 的底层比较；这里没有重新构造良序。所有结果仍然相对于抽象步进公式的 StpOut 与 StpIn。随后，InternalWellOrder 为具体步进提供这两条读式，从而消去最后这个参数。
open Described Cond Cond₀ cond-spec cond₀-spec public
小结
本章在对象语言中描述了先前所构造层序的底层关系。BirthAt 只有在外部给出序数性假设时才认定诞生序数，CodesAt 只在外延意义上确定随载体变化的码集，而 CondCore 只有相对于 StpOut、StpIn、Values 与 Entries 才与诞生层优先的比较相符。存在、解码、表值与 Under 的见证始终留在命题截断之内。下一章将给出具体步进公式及其两条读式。