最早分歧关系的内部族

在每个有穷层，before n 按两个集合的最早分歧来比较它们。本章在 L 内用集合 relAt n 表示这条关系，再把这些集合组成以数码为索引的族，并用对象语言公式 BeforeAt 表达对该族的查找。以此公式实例化 Described 后得到 codeOrder，它将在后续名字比较中供应码的比较关系。本章本身既不比较名字，也不证明名字比较的良基性。

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

本构造只通过稍后附在模块上的显式假设使用排中律。因此，这一经典假设在本章导出的每项结果中都保持可见。

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

固定宇宙层级 ℓ，并假设 LEM (ℓ-suc ℓ)。下文的集合、公式与命题值关系都处在这一选择所确定的层级上。

module L.Choice.EarliestDisagreement {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

我们将在累积层级上用一阶公式描述关系。有序对充当关系条目，稍后再借助其单射性从编码条目恢复两个被比较的集合。

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

第 n 个有穷层是 Lset (# n)，其中 # n 是层级内的冯·诺伊曼数码。关于它的序数性与可构造性的证明，使我们能把该层及其每个成员都视为 L 模型中的对象。

open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd; Lset-mono )
open import L.Ordinal {ℓ} using
  ( numeral-ord; #∈ω; ∈#-elim; #∈#-elim; mem-ord; boundingOrd )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )

两种集合构造承担不同任务。分离从一个界中切出单层关系；替换要到后面才用于沿内部 ω 收集这些关系。有穷逼近本身则由 finSet 与 finSetL 构造。

open import L.Axioms.Basic {ℓ}
  using ( extensionalL; LsetS; ∅ʟ; finSet; finSet-in; finSet-out; module FinOf )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL; hasReplacementL )
open import L.Recursion {ℓ} lem using ( smallDom; mereFunct )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )

数学递归已经确定：before zero 为空；before (suc n) 用 before n 排列较早的点，并在 finiteStage n 上按最早分歧比较下一有穷层的成员。PrecedesAt 在对象语言中表达这个后继步，RecShape 则组织它的有穷逼近。

open import L.Choice.FiniteStageOrders {ℓ} lem
  using ( before; precedes; Agrees; Witness; finiteStage )
open import L.Choice.LimitStageOrder {ℓ} lem
  using ( PrecedesAt; module Precedes; module Described )
open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt; module RecShape )

对象语言中的应用与外延性，使公式能够断言某个集合是关系值表的一项取值。我们先用它们描述一个递归步，之后再用它们读取完整族在某个数码处的值。

open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; appAt; appAt-adequate; appC; appC-adequate; domAt-intro )
open import L.Coding.Expressions {ℓ} using ( numL; extAt; extAt-out; extAt-in; extAt-in-both )

证明中会反复沿集合与有序对的等式作运输，还会对自然数严格序作归纳，以证明逼近所记录的每个取值都是唯一确定的。

import FOL.Absoluteness
import FOL.ZFModel
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Nat.Order using

这项归纳使用自然数 < 的良基性：先认定所有更小索引处的值，才能确定 k 处的值。这与 before 本身的任何良基性质是两回事。

  ( _<_; <-trans; <-asym; pred-≤-pred; <-wellfounded; _≟_ )
import Cubical.Data.Nat.Order as NatOrder
open import Cubical.Induction.WellFounded using ( module WFI )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Data.FinData.Properties using ( toℕ<n; enum; toℕ∘enum )

下文若干见证只能在命题截断下取得。这种见证只保证存在，并不选出规范资料；只有当目标是命题时才能消去，例如隶属、before，或 V 中集合的等式。

open import Cubical.Data.FinData.Base using ( toℕ )
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
  using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet using ( #_; ω )

从现在起，公式都在可构造集合所承载的命题值结构中解释。

open hPropStructure 𝒮ʟ

载体 S 由一个集合及其属于 L 的证明组成。因此，构造内部关系既要给出底层集合，也要给出它的可构造性证明。

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )

绝对性把这一结构中的满足关系与底层集合上的相应断言联系起来。记号 γ ⊨ φ 表示赋值 γ 满足对象语言公式 φ。

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

绑定两个新变元会使原有的每个 de Bruijn 位置后移两位。映射 sh2 记录这一变化，使每个自由变元在新增绑定之下仍指称原来的对象。

private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)

把二位移位应用两次得到 sh4，它用于穿过四个新增绑定。

  sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n))))
  sh4 i = sh2 (sh2 i)

同样，sh6 在新增六个绑定时保持原有引用。这些移位只改变 de Bruijn 位置，不改变公式的数学内容。

  sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n))))))
  sh6 i = sh2 (sh4 i)

对象 stageS n 把有穷层 Lset (# n) 封装为可构造载体的一个元素。保持这一封装不透明，可使后续论证不依赖其中可构造性证明的具体写法。

opaque
  stageS : ℕ → S
  stageS n = LsetS (# n) (numeral-ord n)

等式 stageS-fst 恰好揭示该封装所携带的数学集合：它的第一分量是 finiteStage n。

  stageS-fst : (n : ℕ) → fst (stageS n) ≡ finiteStage n
  stageS-fst n = refl

对象 numS k 类似地把冯·诺伊曼数码 # k 与其可构造性证明封装在一起。

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

等式 numS-fst 让后面的公式读取底层数码，而无须展开与它一同保存的证明。

  numS-fst : (k : ℕ) → fst (numS k) ≡ # k
  numS-fst k = refl

若 z 属于可构造集合 A，则 L 的传递性说明 z 也可构造。封装 memS A z h 记录这一结论，使 z 能作为模型元素使用。

  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 A z h 的第一分量仍是原集合 z；新增分量只提供它属于 L 的证明。

  memS-fst : (A : S) (z : V ℓ) (h : ⟨ z ∈ fst A ⟩) → fst (memS A z h) ≡ z
  memS-fst A z h = refl

对模型元素 a 与 b，prS a b 在 L 内构造它们的有序对。下文的关系集合正以这种对象为成员。

  prS : S → S → S
  prS a b = prʟ a b

忘掉可构造性证明后，就恢复普通有序对 pr (fst a) (fst b)。这条等式把内部隶属断言与底层集合上的关系 before 联系起来。

  prS-fst : (a b : S) → fst (prS a b) ≡ pr (fst a) (fst b)
  prS-fst a b = prʟ-fst a b

特别地，finiteStage n 的每个成员 x 都能提升到载体 S；该层本身提供这项提升所需的可构造性证明。

stageEl : (n : ℕ) (x : V ℓ) → ⟨ x ∈ finiteStage n ⟩ → S
stageEl n x h = x , Lset→isL (# n) (numeral-ord n) x h

每层的关系，作为 L 的一个元素

要用分离表示一条关系，首先需要一个包含所有可能条目的集合。因此，pairsAt n 给出可构造界 D：只要 u,v 都属于 finiteStage n，D 就包含 pr u v。

pairsAt : (n : ℕ)
        → Σ[ D ∈ S ] ((u v : V ℓ) → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
                     → ⟨ pr u v ∈ fst D ⟩)
pairsAt n = d .fst , onPair
  where

有穷层中被呈现的成员已经携带自己的隶属证明。映射 ixL 再附上由此得到的可构造性证明，把每个被呈现成员变成 S 的元素。

  ixL : ⟪ finiteStage n ⟫ → S
  ixL m = ⟪ finiteStage n ⟫↪ m
        , Lset→isL (# n) (numeral-ord n) (⟪ finiteStage n ⟫↪ m)
            (∈∈ₛ {a = ⟪ finiteStage n ⟫↪ m} {b = finiteStage n} .snd
              (∈ₛ⟪ finiteStage n ⟫↪ m))

两个呈现的乘积索引了该层成员的每一对。对这些内部有序对应用 smallDom，便把整个索引族放入同一个可构造集合 D 中。

  d : Σ[ D ∈ S ] ((p : ⟪ finiteStage n ⟫ × ⟪ finiteStage n ⟫)
                  → ⟨ prʟ (ixL (fst p)) (ixL (snd p)) ∈ˢ D ⟩)
  d = smallDom (⟪ finiteStage n ⟫ × ⟪ finiteStage n ⟫)
        (λ p → prʟ (ixL (fst p)) (ixL (snd p)))

给定任意 u,v ∈ finiteStage n，它们的隶属证明给出呈现索引 fu 与 fv。该界包含这两个索引处的有序对，再沿恢复出的分量等式运输，便得到 pr u v 本身属于该界。

  onPair : (u v : V ℓ) → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
         → ⟨ pr u v ∈ fst (d .fst) ⟩
  onPair u v hu hv = 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))

两个纤维 fu 与 fv 恰好记录呈现索引，以及把相应被呈现成员认同为 u、v 的等式。

    where
    fu = ∈-asFiber {a = u} {b = finiteStage n} hu
    fv = ∈-asFiber {a = v} {b = finiteStage n} hv

设在同一载体 A 上，每个 R' w z 都蕴含 R w z。那么，关于 R 的最早分歧见证也给出关于 R' 的见证。方向发生反转，是因为较早点上的关系出现在一致性子句的前件中。

precedes-map : (R R' : V ℓ → V ℓ → hProp (ℓ-suc ℓ)) (A x y : V ℓ)
             → ((w z : V ℓ) → ⟨ w ∈ A ⟩ → ⟨ z ∈ A ⟩ → ⟨ R' w z ⟩ → ⟨ R w z ⟩)
             → ⟨ precedes R A x y ⟩ → ⟨ precedes R' A x y ⟩
precedes-map R R' A x y f = PT.map step
  where

分歧点 z、它属于 A 与 y 的证明，以及它不属于 x 的证明都保持不变。需要转换的只有 x 与 y 在 z 之前一致的证明。

  step : Σ[ z ∈ V ℓ ] Witness R A x y z → Σ[ z ∈ V ℓ ] Witness R' A x y z
  step (z , (z∈A , (z∈y , (z∉x , ag)))) =
    z , (z∈A , (z∈y , (z∉x , ag')))
    where
    ag' : Agrees R' A x y z

在较早点 w，先把假设 R' w z 映到 R w z，再交给原有的一致性证明，由此得到相对于 R' 的一致性。

    ag' w w∈A hR' = ag w w∈A (f w z w∈A z∈A hR')

分离条件只把候选关系条目作为自由变元。它用存在量词绑定前一关系与前一层，以等式把它们固定为给定常元，并让两个端点在当前层中取值。

RelCond : (R A A' : S) → Formula S 
RelCond R A A' =
  ∃̇ ( (var zero ≐ con R)
    ∧̇ ∃̇ ( (var zero ≐ con A)
         ∧̇ ∃̇∈ (con A') ( ∃̇∈ (con A')

余下的合取把候选条目认同为两个端点的有序对，并断言它们相对于给定的前一层与前一关系满足 PrecedesAt。这正是递归步骤稍后采用的后继比较；区别在于，此处的 RelCond 用常元固定前一层与前一关系，而递归公式从逼近中取得关系，并通过层级图识别相应的层。

              ( prAtL (sh2 (sh2 zero)) (suc zero) zero
              ∧̇ PrecedesAt (sh2 (suc zero)) (sh2 zero) (suc zero) zero ) ) ) )

现在递归定义表示关系的集合。零处关系为空；在后继处，分离从包含较大有穷层全部成员对的界开始。

opaque
  relAt : ℕ → S
  relAt zero    = ∅ʟ
  relAt (suc n) =
    hasSeparationL (pairsAt (suc n) .fst)

在这个界中，RelCond (relAt n) (stageS n) (stageS (suc n)) 恰好选出那些按以前一关系为基础的后继子句进行比较的端点对。

      (RelCond (relAt n) (stageS n) (stageS (suc n))) .fst .fst

等式 relAt-zero 显式记录基例，使得以后能把所谓零层关系成员化为对空集的隶属，从而排除它。

  relAt-zero : relAt zero ≡ ∅ʟ
  relAt-zero = refl

在后继层，属于 relAt (suc n) 包含两部分：候选条目属于有序对之界，并且满足由 relAt n、前一层与当前层确定的分离公式。

  relAt-mem : (n : ℕ) (z : S)
            → (z ∈ˢ relAt (suc n))
            ≡ ( (z ∈ˢ pairsAt (suc n) .fst)
              ⊓ ((z ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n))) )
  relAt-mem n =

这条等价正是分离所给出的精确刻画。后续证明会双向使用它：或从隶属中取出公式，或由界证明与公式证明合成隶属。

    hasSeparationL (pairsAt (suc n) .fst)
      (RelCond (relAt n) (stageS n) (stageS (suc n))) .fst .snd

谓词 Rel n a b 是有序对 pr a b 属于表示集合 relAt n 的缩写。接下来的表示引理将证明，对该层成员而言，这一谓词等价于 before n a b。

Rel : ℕ → V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Rel n a b = pr a b ∈ fst (relAt n)

这些引理的证明会在含五个条目的环境中解释 PrecedesAt。在外围绑定造成移位后，s1 与 s2 标出端点槽与层槽的位置。

private
  s1 : Fin 
  s1 = suc zero
  s2 : Fin 
  s2 = sh2 zero

其余位置 s3 与 s4 分别指向前一关系和编码后的有序对。统一命名这些位置，使语义论证始终与 RelCond 中的四种角色对齐。

  s3 : Fin 
  s3 = sh2 (suc zero)
  s4 : Fin 
  s4 = sh2 (sh2 zero)

要辨认关系集的任意成员，必须恢复它的两个分量。因此，RelOf k zv 要求给出 finiteStage k 中的 x,y、把 zv 认同为其有序对的等式，以及 before k x y 成立的证明。这个见证类型包含选定的分量，故其本身不一定是命题。

RelOf : (k : ℕ) → V ℓ → Type (ℓ-suc ℓ)
RelOf k zv = Σ[ x ∈ S ] Σ[ y ∈ S ]
  ( ⟨ fst x ∈ finiteStage k ⟩
  × ( ⟨ fst y ∈ finiteStage k ⟩
    × ( (zv ≡ pr (fst x) (fst y)) × ⟨ before k (fst x) (fst y) ⟩ ) ) )

从 relAt k 的隶属关系只能在命题截断下得到这样的分量：关系只记录合适的呈现存在，并不规范地选定一份呈现。反过来，显式给出的分量及其比较足以把该有序对写入关系。

relAt-out : (k : ℕ) (zv : V ℓ) → ⟨ zv ∈ fst (relAt k) ⟩ → ∥ RelOf k zv ∥₁
relAt-in  : (k : ℕ) (zv : V ℓ) → RelOf k zv → ⟨ zv ∈ fst (relAt k) ⟩

基例反映 before zero：relAt zero 为空，所以假定的成员会导出矛盾。在后继情形，隶属首先给出分离条件，而其中的存在见证只能经命题截断使用。

relAt-out zero zv h = Empty.rec
  (∅-empty zv (∈∈ₛ {a = zv} {b = ∅} .fst
    (subst (λ t → ⟨ zv ∈ fst t ⟩) relAt-zero h)))
relAt-out (suc n) zv h = PT.rec squash₁
  (λ { (r , (qr , ha)) → PT.rec squash₁

逐层打开被截断的见证后，可以看到候选的前一关系、相应有穷层及有序对的两个分量。证明在把这些资料交给最后的重构时始终保留命题截断，因此不会把某份特定呈现作为选定资料带出。

    (λ { (a , (qa , hx)) → PT.rec squash₁
      (λ { (x , (x∈ , hy)) → PT.map (atY r a x qr qa x∈) hy }) hx }) ha }) cond
  where
  zS : S
  zS = memS (relAt (suc n)) zv h

由 zv ∈ relAt (suc n) 及 L 的传递性，可以把底层集合 zv 封装成 L 的元素。这样便能在当前分析的这个成员上解释对象语言的分离条件。

  qz : fst zS ≡ zv
  qz = memS-fst (relAt (suc n)) zv h

分离的定义性质把所假定的隶属转成 RelCond 的满足关系。因此，后续论证可以使用该条件的数学内容，而不只停留在属于有界对集这一事实上。

  cond : ⟨ (zS ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n)) ⟩
  cond = subst ⟨_⟩ (relAt-mem n zS)
    (subst (λ t → ⟨ t ∈ fst (relAt (suc n)) ⟩) (sym qz) h) .snd

对候选分量 x,y，剩余公式体陈述两件事：当前分析的成员是它们的有序对，并且 x 在前一层上按最早分歧先于 y。第二项仍使用 r 所表示的关系，因为外围见证还须把该关系认同为 relAt n。

  Body : (r a x y : S) → Type (ℓ-suc ℓ)
  Body r a x y =
      ⟨ (y ∷ x ∷ a ∷ r ∷ zS ∷ []) ⊨ prAtL s4 s1 zero ⟩
    × ⟨ (y ∷ x ∷ a ∷ r ∷ zS ∷ []) ⊨ PrecedesAt s3 s2 s1 zero ⟩

从后继层选定 x 后，AtY 记录从同一层选择 y，并附上配对与比较事实。把两个选择分开，正好对应 RelCond 中嵌套的存在结构。

  AtY : (r a x : S) → Type (ℓ-suc ℓ)
  AtY r a x = Σ[ y ∈ S ] (⟨ fst y ∈ fst (stageS (suc n)) ⟩ × Body r a x y)

所有见证齐备后，层等式把两个分量都放入 finiteStage (suc n)。余下工作是把当前成员认同为其有序对，并把依据所表示关系作出的比较转成 before (suc n)；随后两部分分别完成这两种转换。

  atY : (r a x : S) → fst r ≡ fst (relAt n) → fst a ≡ fst (stageS n)
      → ⟨ fst x ∈ fst (stageS (suc n)) ⟩ → AtY r a x → RelOf (suc n) zv
  atY r a x qr qa x∈ (y , (y∈ , (hpr , hprec))) =
    x , (y , ( subst (λ t → ⟨ fst x ∈ t ⟩) (stageS-fst (suc n)) x∈
             , ( subst (λ t → ⟨ fst y ∈ t ⟩) (stageS-fst (suc n)) y∈

供应关系与 relAt n 的等式，使其中记录的任意前驱对都能读成 Rel n。这是用本章构造的具体关系解释通用 PrecedesAt 陈述所需的一个方向。

               , (sym qz ∙ qpair , below) ) ) )
    where
    Rrep : (s t : S) → ⟨ pr (fst s) (fst t) ∈ fst (lookup s3 (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) ⟩
         → ⟨ Rel n (fst s) (fst t) ⟩
    Rrep s t p = subst (λ w → ⟨ pr (fst s) (fst t) ∈ w ⟩) qr p

反向搬运把 Rel n 的证明写回所供应的关系。有了这两个方向，PrecedesAt 的充分性定理便能把两种呈现当作同一个基底关系处理。

    Rfill : (s t : S) → ⟨ Rel n (fst s) (fst t) ⟩
          → ⟨ pr (fst s) (fst t) ∈ fst (lookup s3 (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) ⟩
    Rfill s t p = subst (λ w → ⟨ pr (fst s) (fst t) ∈ w ⟩) (sym qr) p

固定这两条表示映射后，Precedes 模块提供对象语言公式与宿主谓词 precedes 之间的语义桥梁。这座桥只处理一次比较步骤，并不在这里证明任何序性质。

    module P = Precedes s3 s2 s1 zero (y ∷ x ∷ a ∷ r ∷ zS ∷ [])
                        (Rel n) Rrep Rfill

读出 PrecedesAt 得到在公式所供应之层上的 precedes 比较。层等式再把该载体认同为 finiteStage n，也就是 before (suc n) 的递归定义所使用的载体。

    onStage : ⟨ precedes (Rel n) (finiteStage n) (fst x) (fst y) ⟩
    onStage = subst (λ w → ⟨ precedes (Rel n) w (fst x) (fst y) ⟩)
      (qa ∙ stageS-fst n) (P.PrecedesAt-out hprec)

在一致性子句内部，每次使用基底关系时，都必须把 before n 转为 relAt n 中的隶属。归纳得到的写入引理完成这一转换，随后 precedes-map 恰好给出后继关系 before (suc n)。

    below : ⟨ before (suc n) (fst x) (fst y) ⟩
    below = precedes-map (Rel n) (before n) (finiteStage n) (fst x) (fst y)
      (λ w t hw ht hb → relAt-in n (pr w t)
        (stageEl n w hw , (stageEl n t ht , (hw , (ht , (refl , hb))))))
      onStage

配对公式的充分性把封装后的成员认同为 pr (fst x) (fst y)。再与封装等式复合，便得到原始 zv 所需的等式。

    qpair : fst zS ≡ pr (fst x) (fst y)
    qpair = subst ⟨_⟩ (prAtL-adequate s4 s1 zero (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) hpr

当 k = 0 时，RelOf 见证已经包含不可能的 before zero 证明，所以写入方向由矛盾得出。在后继情形，目标有序对先被放入有界对集，再证明它满足分离条件。

relAt-in zero zv (x , (y , (x∈ , (y∈ , (qq , hb))))) = Empty.rec* hb
relAt-in (suc n) zv (x , (y , (x∈ , (y∈ , (qq , hb))))) =
  subst (λ t → ⟨ t ∈ fst (relAt (suc n)) ⟩) (prS-fst x y ∙ sym qq)
    (subst ⟨_⟩ (sym (relAt-mem n (prS x y))) (inBound , cond))
  where

两个层隶属假设把该有序对放入 pairsAt (suc n)。这是分离所需的界：只有有穷层成员组成的对才可能进入 relAt (suc n)。

  inBound : ⟨ prS x y ∈ˢ pairsAt (suc n) .fst ⟩
  inBound = subst (λ t → ⟨ t ∈ fst (pairsAt (suc n) .fst) ⟩) (sym (prS-fst x y))
    (pairsAt (suc n) .snd (fst x) (fst y) x∈ y∈)

在反向构造中，环境含有实际的前一关系 relAt n，故把它解释为 Rel n 只需恒等映射。于是可以使用同一座语义桥，从宿主层比较构造 PrecedesAt。

  module P = Precedes s3 s2 s1 zero
                      (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ [])
                      (Rel n) (λ _ _ p → p) (λ _ _ p → p)

假设 before (suc n) x y 展开为以 before n 为基底的最早分歧。为了用内部关系表达同一份一致性，每个已记录的前置有序对都经 relAt-out 读出；由于目标 before n w t 是命题，可以消去命题截断。

  held : ⟨ precedes (Rel n) (finiteStage n) (fst x) (fst y) ⟩
  held = precedes-map (before n) (Rel n) (finiteStage n) (fst x) (fst y)
    (λ w t hw ht hR → PT.rec (snd (before n w t)) (readBack w t)
      (relAt-out n (pr w t) hR))
    hb

读回的 RelOf 见证可能使用不同于 w,t 的分量，但其中的配对等式说明其有序对等于 pr w t。有序配对的单射性分别认同两个分量，随后所记录的 before n 证明便具有所需端点。

    where
    readBack : (w t : V ℓ) → RelOf n (pr w t) → ⟨ before n w t ⟩
    readBack w t (p , (q , (p∈ , (q∈ , (qq' , hbf))))) =
      subst2 (λ s u → ⟨ before n s u ⟩)
        (sym (pr-inj qq' .fst)) (sym (pr-inj qq' .snd)) hbf

转换后的宿主层比较已满足 PrecedesAt-in 的假设。它给出分离公式所需的比较子句，其中前一层与前一关系位于相应变元中。

  hprec : ⟨ (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ [])
          ⊨ PrecedesAt s3 s2 s1 zero ⟩
  hprec = P.PrecedesAt-in
    (subst (λ w → ⟨ precedes (Rel n) w (fst x) (fst y) ⟩) (sym (stageS-fst n))
      held)

候选成员本就是 prS x y，因此满足配对识别公式。其充分性等式把这一内部构造连接到公式所要求的底层有序对。

  hpr : ⟨ (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ []) ⊨ prAtL s4 s1 zero ⟩
  hpr = subst ⟨_⟩
    (sym (prAtL-adequate s4 s1 zero
      (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ []))) (prS-fst x y)

stageS (suc n) 的呈现等式把 finiteStage (suc n) 的每个已知成员搬运到公式使用的层对象中。这里不需要额外的闭包性质。

  onStage : (w : V ℓ) → ⟨ w ∈ finiteStage (suc n) ⟩
          → ⟨ w ∈ fst (stageS (suc n)) ⟩
  onStage w hw = subst (λ t → ⟨ w ∈ t ⟩) (sym (stageS-fst (suc n))) hw

刚构造的见证满足完整的分离条件：它们认同前一关系与前一层，把 x,y 放入后继层，并建立配对与最早分歧。嵌套存在量词在命题截断下引入，只断言存在，并不选取规范见证。

  cond : ⟨ (prS x y ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n)) ⟩
  cond = ∣ relAt n , (refl
       , ∣ stageS n , (refl
       , ∣ x , (onStage (fst x) x∈
       , ∣ y , (onStage (fst y) y∈ , (hpr , hprec)) ∣₁) ∣₁) ∣₁) ∣₁

实用的读出接口从已知有序对 pr u v 出发，并预先假设两个端点都属于 finiteStage n。它只把截断呈现消去到命题 before n u v，因此没有规范呈现并不会造成损失。

relAt-rep : (n : ℕ) (u v : V ℓ)
          → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
          → ⟨ pr u v ∈ fst (relAt n) ⟩ → ⟨ before n u v ⟩
relAt-rep n u v hu hv h = PT.rec (snd (before n u v)) read (relAt-out n (pr u v) h)
  where

若读回的呈现使用分量 p,q，其有序对与 pr u v 相等便迫使 p=u 且 q=v。沿这两条等式搬运，就把所存比较转成目标比较。

  read : RelOf n (pr u v) → ⟨ before n u v ⟩
  read (p , (q , (p∈ , (q∈ , (qq , hbf))))) =
    subst2 (λ s t → ⟨ before n s t ⟩)
      (sym (pr-inj qq .fst)) (sym (pr-inj qq .snd)) hbf

反过来，u,v 的层隶属与 before n u v 的证明组成 pr u v 的显式 RelOf 见证。写入引理随后把该对记录进 relAt n，完成逐对表示的另一个方向。

relAt-fill : (n : ℕ) (u v : V ℓ)
           → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
           → ⟨ before n u v ⟩ → ⟨ pr u v ∈ fst (relAt n) ⟩
relAt-fill n u v hu hv h = relAt-in n (pr u v)
  (stageEl n u hu , (stageEl n v hv , (hu , (hv , (refl , h)))))

那一步，对它所查阅的一切保持通用

递归描述必须把关系当作资料接收，而不能直接指称 relAt。Held r a b 给出所需解释：当且仅当 r 含有 a,b 的有序对时，r 才把 a 关联到 b。

Held : S → V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Held r a b = pr a b ∈ fst r

一次递归步骤先寻找当前索引的一个 ∈-极大成员 c。当该索引是后继数码 # (suc n) 时，这个成员就是其前驱 # n；在零处则不存在这样的成员。因此，该步骤所定义的关系在零处没有成员，而无须另写基例公式。

opaque
 RelBodyAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
 RelBodyAt z b f =
   ∃̇ ( (var zero ∈̇ var (suc b))
     ∧̇ ( ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero))

找到 c 后，公式从逼近中读取在 c 处记录的关系。层级图识别出 Lset (fst c) 以及当前索引所确定的 Lset 层，两个候选端点都在后一层中取值。只有当当前索引被认同为数码时，这些层才是有穷层。

       ∧̇ ∃̇ ( appAt (sh2 f) (suc zero) zero
            ∧̇ ∃̇ ( LsetGraphAt zero (suc (suc zero))
                 ∧̇ ∃̇ ( LsetGraphAt zero (sh4 b)
                      ∧̇ ∃̇∈ (var zero)
                           ( ∃̇∈ (var (suc zero))

最内层子句要求候选条目是两个端点的有序对，并使用从逼近读出的关系，在前一层上以 PrecedesAt 比较它们。因此，该公式无需指称任何特定的 relAt n，便描述了递归的后继步骤。

                               ( prAtL (sh6 z) (suc zero) zero
                               ∧̇ PrecedesAt (suc (suc (suc (suc zero))))
                                             (suc (suc (suc zero)))
                                             (suc zero) zero ) ) ) ) ) ) )

StepOf 是该公式在元层面的含义。它选择四个模型元素：当前索引的候选极大成员 c、在那里记录的关系值 r，以及端点 x,y；候选条目 zv 已经是谓词的参数。只有在当前索引被认同为数码后，c 才会被认同为它的前驱数码。

StepOf : ∀ {n} → Fin n → Fin n → S ^ n → V ℓ → Type (ℓ-suc ℓ)
StepOf b f γ zv =
  Σ[ c ∈ S ] Σ[ r ∈ S ] Σ[ x ∈ S ] Σ[ y ∈ S ]
    ( ⟨ fst c ∈ fst (lookup b γ) ⟩
    × ( ((d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩ → ⟨ fst c ∈ fst d ⟩ → Empty.⊥)

附带条件断言：c 属于当前索引并且在其中为 ∈-极大元；逼近在 c 处记录 r；两个端点都属于当前取值所索引的层级阶段；zv 是它们的有序对；并且 precedes (Held r) 在 Lset (fst c) 上比较它们。这些正是一次递归步骤所需的数学数据；有穷性要到后面才由数码等式给出。

      × ( ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
        × ( ⟨ fst x ∈ Lset (fst (lookup b γ)) ⟩
          × ( ⟨ fst y ∈ Lset (fst (lookup b γ)) ⟩
            × ( (zv ≡ pr (fst x) (fst y))
              × ⟨ precedes (Held r) (Lset (fst c)) (fst x) (fst y) ⟩ ) ) ) ) ) )

下面对任意变元 z,b,f 与任意环境证明语义对应。关于 lookup b γ 的底层集合为序数这一假设，用于把层级图描述的各阶段认同为相应的 Lset 值。

module _ {n : ℕ} (z b f : Fin n) (γ : S ^ n)
         (ob : IsOrd (fst (lookup b γ))) where
  private
    Body : (c r A A' x y : S) → Type (ℓ-suc ℓ)
    Body c r A A' x y =

六个存在见证扩展环境后，最内层公式体保留两项决定性事实：z 所指的值是 x,y 的有序对，并且这两个端点相对于已恢复的层与关系满足 PrecedesAt。

        ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) ⊨ prAtL (sh6 z) (suc zero) zero ⟩
      × ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
          ⊨ PrecedesAt (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                       (suc zero) zero ⟩

固定第一个端点 x 后，AtY 封装余下端点 y、它属于当前层的证明，以及最内层的两项事实。这个类型对应公式嵌套存在读法中的一层。

    AtY : (c r A A' x : S) → Type (ℓ-suc ℓ)
    AtY c r A A' x = Σ[ y ∈ S ] (⟨ fst y ∈ fst A' ⟩ × Body c r A A' x y)

MaxOf c 用隶属序表达极大性：若 d 也属于当前索引，则 c ∈ d 不可能成立。再结合 c 属于该索引，便知 c 是隶属序下的极大元。对后继数码而言，它就是前驱；在零处，c 的隶属前提本身已经没有见证。

    MaxOf : (c : S) → Type (ℓ-suc ℓ)
    MaxOf c = (d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩ → ⟨ fst c ∈ fst d ⟩
            → Empty.⊥

为了把公式见证转成 StepOf，该转换假设 c 的隶属与极大性、逼近条目 (c,r)、认同前一层与当前层的等式，以及 x 属于当前层。最后一份 AtY 见证供应 y 与两项内层事实。

    atY : (c r A A' x : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
        → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
        → fst A ≡ Lset (fst c) → fst A' ≡ Lset (fst (lookup b γ))
        → ⟨ fst x ∈ fst A' ⟩
        → AtY c r A A' x → StepOf b f γ (fst (lookup z γ))

层等式把公式中 x,y 的隶属转换成 Lset (lookup b γ) 中的隶属，正好符合 StepOf 的要求。配对等式与宿主层 precedes 比较随后由下面两项充分性论证给出。

    atY c r A A' x c∈ cmax hf qA qA' x∈ (y , (y∈ , (hpr , hprec))) =
      c , (r , (x , (y , (c∈ , (cmax , (hf
        , ( subst (λ t → ⟨ fst x ∈ t ⟩) qA' x∈
          , ( subst (λ t → ⟨ fst y ∈ t ⟩) qA' y∈
            , (qpair , hprec') ) ) ) ) ) ) ) )

这里直接把关系变元解释为 Held r，所以两条表示映射都是恒等映射。于是 Precedes 桥梁可以读出对象语言比较，而无需诉诸已经构造的 relAt 族。

      where
      module P = Precedes (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                          (suc zero) zero (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
                          (Held r) (λ _ _ p → p) (λ _ _ p → p)

读出 PrecedesAt 得到在公式所绑定层对象上的比较。该层的认同等式把载体搬运到 Lset (fst c)，从而得到 StepOf 所要求的比较。

      hprec' : ⟨ precedes (Held r) (Lset (fst c)) (fst x) (fst y) ⟩
      hprec' = subst (λ t → ⟨ precedes (Held r) t (fst x) (fst y) ⟩) qA
        (P.PrecedesAt-out hprec)

prAtL 的充分性把 z 所指的值认同为所恢复两端点的有序对。这便给出元层面步骤见证中的配对等式。

      qpair : fst (lookup z γ) ≡ pr (fst x) (fst y)
      qpair = subst ⟨_⟩
        (prAtL-adequate (sh6 z) (suc zero) zero
          (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)) hpr

第一个端点 x 已经显露后，余下端点仍只在命题意义下存在。AtX 正好记录这一中间状态：x 的层隶属，以及经过命题截断的 AtY 见证。

    AtX : (c r A A' : S) → Type (ℓ-suc ℓ)
    AtX c r A A' = Σ[ x ∈ S ] (⟨ fst x ∈ fst A' ⟩ × ∥ AtY c r A A' x ∥₁)

由于目标结论本身也经过命题截断，可以使用隐藏的 y 见证，而不把它作为选定资料带出命题。把逐点转换映射过该截断，恰好保留公式所供应的存在强度。

    atX : (c r A A' : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
        → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
        → fst A ≡ Lset (fst c) → fst A' ≡ Lset (fst (lookup b γ))
        → AtX c r A A' → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atX c r A A' c∈ cmax hf qA qA' (x , (x∈ , hy)) =

内层转换由恢复出的资料装配一份显式 StepOf 见证，PT.map 再把它放回命题截断之下。由此完成向外的语义读法，同时不产生规范的前驱或端点见证。

      PT.map (atY c r A A' x c∈ cmax hf qA qA' x∈) hy

找回 c 所索引的层之后，余下的内层量词要识别当前索引所索引的层。AtA' 打包一个可构造集合 A'、它在该处满足层图的证据，以及更内层见证 x 与 y 的命题截断存在。命题截断保留见证存在这一事实，却不选出一对规范见证。

    AtA' : (c r A : S) → Type (ℓ-suc ℓ)
    AtA' c r A = Σ[ A' ∈ S ]
      ( ⟨ (A' ∷ A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (sh4 b) ⟩
      × ∥ AtX c r A A' ∥₁ )

要从 A' 继续，论证保留已经得到的关于 c 的信息、表中的条目 (c,r)，以及 A 与 c 所索引之层的同一视。在把 AtX 中隐藏的见证解释为语义步进之前，还须把 A' 识别为当前序数索引所索引的层。

    atA' : (c r A : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
         → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
         → fst A ≡ Lset (fst c)
         → AtA' c r A → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atA' c r A c∈ cmax hf qA (A' , (hg , hx)) =

层图恰好给出这一同一视。把它的函数性定理 Lset-only 用于索引的序数性假设，便得到 fst A' ≡ Lset (fst (lookup b γ))；于是可以把命题截断的 AtX 消去到命题截断的步进结论中。

      PT.rec squash₁ (atX c r A A' c∈ cmax hf qA qA') hx
      where
      qA' : fst A' ≡ Lset (fst (lookup b γ))
      qA' = Lset-only zero (sh4 b) (A' ∷ A ∷ r ∷ c ∷ γ) hg ob

再向外一层量词，AtA 对 c 所索引的层完成同样的工作。它由一个满足相应层图的可构造集合 A，以及 AtA' 后续数据的命题截断存在组成。

    AtA : (c r : S) → Type (ℓ-suc ℓ)
    AtA c r = Σ[ A ∈ S ]
      ( ⟨ (A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩
      × ∥ AtA' c r A ∥₁ )

解释这一层时，首先需要一个等式来说明 A 究竟是哪一层。得到该等式后，便可像处理内层时一样，把命题截断的后续数据消去到命题截断的步进中。

    atA : (c r : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
        → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
        → AtA c r → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atA c r c∈ cmax hf (A , (hg , hA')) =
      PT.rec squash₁ (atA' c r A c∈ cmax hf qA) hA'

由于 c 属于 b 所指的序数，mem-ord 表明 c 本身也是序数。层图在这个序数处的函数性随即给出 fst A ≡ Lset (fst c)。这一识别不使用层的单调性。

      where
      qA : fst A ≡ Lset (fst c)
      qA = Lset-only zero (suc (suc zero)) (A ∷ r ∷ c ∷ γ) hg
        (mem-ord {A = fst (lookup b γ)} ob (fst c) c∈)

再外一层的见证是逼近表在 c 处记录的关系。AtR 记录一个可构造集合 r、应用公式的满足证据，此公式表示表中含有条目 (c,r)，以及用于重建所需两层的后续数据之命题截断。

    AtR : (c : S) → Type (ℓ-suc ℓ)
    AtR c = Σ[ r ∈ S ]
      ( ⟨ (r ∷ c ∷ γ) ⊨ appAt (sh2 f) (suc zero) zero ⟩ × ∥ AtA c r ∥₁ )

appAt 的充分性把它的满足判断转换成有序对 (c,r) 的周遭隶属陈述。有了这个表中条目，就可以把命题截断的 AtA 后续数据消去到命题截断的语义步进中。

    atR : (c : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
        → AtR c → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atR c c∈ cmax (r , (happ , hA)) = PT.rec squash₁ (atA c r c∈ cmax hf) hA
      where
      hf : ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩

具体而言，恢复出的事实是 pr (fst c) (fst r) ∈ fst (lookup f γ)。这正是 StepOf 所需的元层面形式：f 所指的逼近把关系 r 赋给索引 c。

      hf = subst ⟨_⟩ (appAt-adequate (sh2 f) (suc zero) zero (r ∷ c ∷ γ)) happ

在最外层，AtC 选取序数索引的一个成员 c，并断言该索引中不存在满足 c ∈ d 的成员 d。因此 c 是该索引在隶属关系下的极大元。当后文把索引识别为一个非零冯·诺伊曼数码时，这个条件将识别出它的前驱；余下的命题截断分量则提供关系与层的数据。

    AtC : Type (ℓ-suc ℓ)
    AtC = Σ[ c ∈ S ]
      ( ⟨ fst c ∈ fst (lookup b γ) ⟩
      × ( ⟨ (c ∷ γ) ⊨ ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ⟩
        × ∥ AtR c ∥₁ ) )

公式中的有界否定在提升后的宇宙中解释。把它降下便得到普通函数 MaxOf c：任何声称既属于该索引又满足 c ∈ d 的 d 都会导出矛盾。随后可经由前述各层消去命题截断的关系见证。

    atC : AtC → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atC (c , (c∈ , (hmax , hr))) = PT.rec squash₁ (atR c c∈ cmax) hr
      where
      cmax : MaxOf c
      cmax d hd hc = lower (hmax d hd hc)

这些逐层解释给出了步进主体的读出方向。为了建立反向结论，同一个主体公式在局部展开，使一个显式的 StepOf 见证能够重新填入其中的存在子句与有界子句。

  opaque
   unfolding RelBodyAt

从 RelBodyAt 的满足证据出发，最外层存在量词只给出 c 的命题截断存在。逐层读式在同一限制下恢复余下数据，最终得到 ∥ StepOf b f γ (fst (lookup z γ)) ∥₁。它们证明某个步进存在，却不为嵌套量词选择规范见证。

   RelBody-out : ⟨ γ ⊨ RelBodyAt z b f ⟩
               → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
   RelBody-out = PT.rec squash₁ atC

反过来，一个显式的 StepOf 见证已经包含 c、关系 r、被比较的对象 x,y、它们的层隶属、有序对等式与前驱层比较。RelBody-in 重建两个中间层，并把这些数据逐一填入嵌套公式。公式的存在子句经过命题截断，因此结论断言公式得到满足，而不保留一组规范的内部见证。

   RelBody-in : StepOf b f γ (fst (lookup z γ)) → ⟨ γ ⊨ RelBodyAt z b f ⟩
   RelBody-in (c , (r , (x , (y , (c∈ , (cmax , (hf , (x∈ , (y∈
              , (qpair , hprec))))))))))
     = ∣ c , (c∈ , (hmax , ∣ r , (happ , ∣ A , (hgA , ∣ A' , (hgA'
       , ∣ x , (x∈ , ∣ y , (y∈ , (hpr , hprec')) ∣₁) ∣₁) ∣₁) ∣₁) ∣₁)) ∣₁

首先要重建的事实是 c 为序数。序数的每个成员仍是序数，因此，这由 c ∈ fst (lookup b γ) 以及该集合的序数性假设得出；它也正是构造由 c 索引的可构造层所需的条件。

     where
     oc : IsOrd (fst c)
     oc = mem-ord {A = fst (lookup b γ)} ob (fst c) c∈

利用这一序数性，LsetS 把 Lset (fst c) 打包为模型元素 A。最早分歧比较正是在这个由前驱索引的层上求值。

     A : S
     A = LsetS (fst c) oc

当前索引的序数性假设同样把 Lset (fst (lookup b γ)) 打包为 A'。第二个层提供集合界，容纳有序对将要成为当前关系成员的两个对象。

     A' : S
     A' = LsetS (fst (lookup b γ)) ob

接下来须用对象语言中的有界全称否定表达语义上的极大性函数。对索引中的每个 d，任何 c ∈ d 的证明都会被 cmax 送到矛盾，再提升到公式满足关系所在的宇宙。

     hmax : ⟨ (c ∷ γ) ⊨ ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ⟩
     hmax d hd hc = lift (cmax d hd hc)

StepOf 中的表条目采用周遭形式 pr (fst c) (fst r) ∈ fst (lookup f γ)。沿 appAt 充分性路径的逆向搬运，便把这个事实转换为应用原子的满足证据，也就是主体公式所需的形式。

     happ : ⟨ (r ∷ c ∷ γ) ⊨ appAt (sh2 f) (suc zero) zero ⟩
     happ = subst ⟨_⟩
       (sym (appAt-adequate (sh2 f) (suc zero) zero (r ∷ c ∷ γ))) hf

所选的 A 按定义就是 c 所索引的层。因此，层级的呈现定理由 c 的序数性与被表示取值的自反等式证明相应的层图子句。

     hgA : ⟨ (A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩
     hgA = Lset-defines zero (suc (suc zero)) (A ∷ r ∷ c ∷ γ) oc refl

同一个呈现定理在当前索引处证明 A' 的图子句。这里所需的序数性就是既定假设 ob，故公式把 A' 精确识别为容纳 x 与 y 的那一层。

     hgA' : ⟨ (A' ∷ A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (sh4 b) ⟩
     hgA' = Lset-defines zero (sh4 b) (A' ∷ A ∷ r ∷ c ∷ γ) ob refl

StepOf 中的等式把 z 所指的候选取值认同为 x 与 y 的 Kuratowski 对。沿 prAtL 充分性路径的逆向搬运，把这个等式转换为对象语言配对子句的满足证据。

     hpr : ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) ⊨ prAtL (sh6 z) (suc zero) zero ⟩
     hpr = subst ⟨_⟩
       (sym (prAtL-adequate (sh6 z) (suc zero) zero
         (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ))) qpair

最后还须翻译前驱层上的比较。这里的 Precedes 实例把基底关系解释为 Held r，也就是有序对属于 r。由于这一解释已经与对象语言应用公式所要求的隶属命题完全相同，两个表示映射都取恒等函数。

     module P = Precedes (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                         (suc zero) zero (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
                         (Held r) (λ _ _ p → p) (λ _ _ p → p)

固定这一解释后，PrecedesAt-in 把 StepOf 携带的语义最早分歧比较转换为 PrecedesAt 的满足证据。至此 RelBodyAt 的每个子句都已完成，从语义步进返回对象语言公式的桥梁也随之建立。

     hprec' : ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
              ⊨ PrecedesAt (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                           (suc zero) zero ⟩
     hprec' = P.PrecedesAt-in hprec

上述主体只判定一个候选有序对。一个关系取值必须恰好收集所有这样的候选者，因此下一构造把这个单步条件外延地扩展到整个集合。

逼近与那个图

RelStepAt v b f 断言 v 所指集合的成员恰好是满足 RelBodyAt 的对象，其中候选者绑定为新引入的零号变元，索引 b,f 则在该绑定之下相应移位。因此它同时给出两个包含方向：候选关系的每个成员都实现一个语义步骤，而每个实现这种步骤的对象都属于该关系。

opaque
  RelStepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
  RelStepAt v b f = extAt v (RelBodyAt zero (suc b) (suc f))

只要 fst (lookup b γ) 是序数，这一外延描述的读式就成立。主体公式需要该假设来识别步骤见证中出现的两个可构造层。

module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n)
         (ob : IsOrd (fst (lookup b γ))) where
  opaque
   unfolding RelStepAt

正向包含从 v 所指集合的一个成员 w 出发，在 w 处读出主体公式，并得到 ∥ StepOf b f γ (fst w) ∥₁。结果经过命题截断，因为主体通过存在量词找出前驱、所记录的关系与被比较的分量。

   RelStep-out : ⟨ γ ⊨ RelStepAt v b f ⟩ → (w : S)
               → ⟨ fst w ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ (fst w) ∥₁
   RelStep-out h w hw = RelBody-out zero (suc b) (suc f) (w ∷ γ) ob
     (extAt-out v (RelBodyAt zero (suc b) (suc f)) γ h w hw)

反向包含从 w 的一个显式语义步骤出发。RelBody-in 把它转换为主体的满足证据，外延描述的反向蕴涵随即推出 w 属于 v 所指的集合。

   RelStep-back : ⟨ γ ⊨ RelStepAt v b f ⟩ → (w : S) → StepOf b f γ (fst w)
                → ⟨ fst w ∈ fst (lookup v γ) ⟩
   RelStep-back h w s = extAt-in v (RelBodyAt zero (suc b) (suc f)) γ h w
     (RelBody-in zero (suc b) (suc f) (w ∷ γ) ob s)

引入原理陈述了精确的逆命题。要证明 RelStepAt，只须对拟议关系的每个成员给出一个命题截断的步进，并对每个显式步进见证给出一个隶属证明。这两个函数正是外延性的两个包含方向。

   RelStep-in : ((w : S) → ⟨ fst w ∈ fst (lookup v γ) ⟩
                 → ∥ StepOf b f γ (fst w) ∥₁)
              → ((w : S) → StepOf b f γ (fst w)
                 → ⟨ fst w ∈ fst (lookup v γ) ⟩)
              → ⟨ γ ⊨ RelStepAt v b f ⟩

对第一个包含方向，每个命题截断的步进先经 RelBody-in 映射，再消去到作为命题的满足判断中。对第二个方向，RelBody-out 产生一个命题截断的步进；在应用给定的反向函数之前，它被消去到作为命题的隶属判断中。这里能够消去命题截断，仅仅因为两个目标都是命题。

   RelStep-in into back = extAt-in-both v (RelBodyAt zero (suc b) (suc f)) γ
     (λ w hw → PT.rec (snd ((w ∷ γ) ⊨ RelBodyAt zero (suc b) (suc f)))
       (RelBody-in zero (suc b) (suc f) (w ∷ γ) ob) (into w hw))
     (λ w h → PT.rec (snd (fst w ∈ fst (lookup v γ))) (back w)
       (RelBody-out zero (suc b) (suc f) (w ∷ γ) ob h))

这个外延步进现在实例化通用的递归形状构造。所得 ApproxAt 描述一张初始段表，其定义域与逐点步进子句符合 RelStepAt；RelGraphAt 则描述当前索引处由此前这种逼近支撑的一个取值。后文把该索引识别为数码时，这张表才成为有穷表。

module A = RecShape RelStepAt
open A using ( ApproxAt; ApproxAt-value; ApproxAt-step
             ; ApproxAt-in; GraphOf; PairOf )
     renaming ( GraphAt to RelGraphAt; Graph-in to RelGraph-in
              ; Graph-out to RelGraph-out; PairGraphAt to PairRelGraphAt

同一构造还为逼近图及其成对形式提供引入与消去原理。局部名称 RelGraphAt 与 PairRelGraphAt 表明，这套通用机制在此专用于递归定义的关系取值。

              ; PairGraph-in to PairRelGraph-in
              ; PairGraph-out to PairRelGraph-out )

到目前为止，这些公式只描述递归的形状，尚未识别其取值。下一步要证明，任何满足这一形状的表所记录的恰是先前构造的集合 relAt m；为此，证明把已记录取值的正确性与标准条目的存在性分开处理。

那一步，对着这场递归

Values g k 是正确性条件。对每个 m < k，若 g 含有把 # m 与任意模型元素 w 配成的条目，则 w 的底层集合等于 relAt m 的底层集合。这说明一个已记录索引处的集合值唯一，却不选择唯一的证明或见证包。

Values : S → ℕ → Type (ℓ-suc ℓ)
Values g k = (m : ℕ) → m < k → (w : S)
           → ⟨ pr (# m) (fst w) ∈ fst g ⟩ → fst w ≡ fst (relAt m)

Entries g k 是与之配合的完备性条件。它要求每个 m < k 的标准条目 (# m, relAt m) 都出现在 g 中。Values 与 Entries 合起来表明：表含有所有更小索引，并且每个索引处只记录预期的集合值。

Entries : S → ℕ → Type (ℓ-suc ℓ)
Entries g k = (m : ℕ) → m < k → ⟨ pr (# m) (fst (relAt m)) ∈ fst g ⟩

任何比较 before k x y 都迫使 k 为后继数。在零处该关系为空，因此比较会导出矛盾；在 suc m 处，前驱 m 与所需等式立即可得。这个小引理稍后把 relAt k 的成员转换回 StepOf 所需的前驱数据。

before-suc : (k : ℕ) (x y : V ℓ) → ⟨ before k x y ⟩ → Σ[ m ∈ ℕ ] (k ≡ suc m)
before-suc zero    x y h = Empty.rec* h
before-suc (suc m) x y h = m , refl

固定 v 所指的候选关系、b 所指的索引与 f 所指的表。等式 qb 把索引认同为数码 # k，而 vals 与 ents 断言该表在 k 以下正确且完备。在这些假设下，索引处的语义步骤可以与 relAt k 中的隶属精确比较。

module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) (k : ℕ)
         (qb : fst (lookup b γ) ≡ # k)
         (vals : Values (lookup f γ) k) (ents : Entries (lookup f γ) k) where
  private
    ob : IsOrd (fst (lookup b γ))

数码 # k 是序数。沿 qb : fst (lookup b γ) ≡ # k 的反向搬运这一事实，便证明 fst (lookup b γ) 为序数，从而可以使用先前关于步骤主体的读式与填入引理。

    ob = subst IsOrd (sym qb) (numeral-ord k)

考虑候选取值 x 的一个显式 StepOf 见证。其中的极大元 c 属于该索引，qb 把这一点转化为 fst c ∈ # k。数码隶属的消去在命题截断下恢复一个自然数 m < k 与等式 fst c ≡ # m；这里可以消去命题截断，因为目标隶属 x ∈ relAt k 是命题。

    into : (x : V ℓ) → StepOf b f γ x → ⟨ x ∈ fst (relAt k) ⟩
    into x (c , (r , (xx , (yy , (c∈ , (cmax , (hf , (xx∈ , (yy∈
           , (qx , hprec)))))))))) =
      PT.rec (snd (x ∈ fst (relAt k))) atC
        (∈#-elim k (fst c) (subst (λ t → ⟨ fst c ∈ t ⟩) qb c∈))

对这样一个 m，可用 relAt k 的引入引理证明所需隶属。相应的 RelOf k x 见证沿用分量 xx 与 yy，并需要它们属于 finiteStage k、x 与其有序对的等式，以及比较 before k xx yy。余下工作因而是证明极大元 c 确实对应 k 的直接前驱，并据此翻译表中记录的比较。

      where
      atC : Σ[ m ∈ ℕ ] ((m < k) × (fst c ≡ # m)) → ⟨ x ∈ fst (relAt k) ⟩
      atC (m , (hm , qc)) = relAt-in k x
        (xx , (yy , (xxk , (yyk , (qx , below)))))
        where

由于 c 由 # m 编码，而它又是 # k 的成员中的极大元，应有 k = suc m。三歧性比较 suc m 与 k：相等情形给出所需等式，两个严格不等情形则分别与已有的 m、k 关系或极大性矛盾。

        ksuc : k ≡ suc m
        ksuc = decide (suc m ≟ k)
          where
          decide : NatOrder.Trichotomy (suc m) k → k ≡ suc m
          decide (NatOrder.lt hlt) = Empty.rec

若 suc m < k，则数码 #(suc m) 本身属于 # k。又因 c = # m，还有 c ∈ #(suc m)。这两个隶属事实在索引中给出了一个严格位于 c 之上的成员，与极大性子句矛盾。

            (cmax (numS (suc m))
              (subst (λ t → ⟨ fst (numS (suc m)) ∈ t ⟩) (sym qb)
                (subst (λ t → ⟨ t ∈ # k ⟩) (sym (numS-fst (suc m)))
                  (#mono (suc m) k hlt)))
              (subst (λ t → ⟨ fst c ∈ t ⟩) (sym (numS-fst (suc m)))

反之，若 k < suc m，去掉后继便得到 k ≤ m，这与已知的 m < k 不相容。因此只余相等情形；把三歧性给出的等式反向，即得下文所需方向的 k ≡ suc m。

                (subst (λ t → ⟨ t ∈ # (suc m) ⟩) (sym qc)
                  (#mono m (suc m) NatOrder.≤-refl))))
          decide (NatOrder.eq e) = sym e
          decide (NatOrder.gt hgt) = Empty.rec (<-asym hm (pred-≤-pred hgt))

步进见证已经给出 xx 属于 Lset (fst (lookup b γ))。沿 qb 搬运，把这个集合识别为 Lset (# k)，也就是 finiteStage k，从而得到 RelOf k x 所需的第一个层隶属分量。

        xxk : ⟨ fst xx ∈ finiteStage k ⟩
        xxk = subst (λ t → ⟨ fst xx ∈ Lset t ⟩) qb xx∈

有序对的两个端点都必须属于由 k 索引的层。对于第二个端点，界等于 # k 的等式把 Lset (fst (lookup b γ)) 中的隶属关系化为 finiteStage k 中的隶属关系。

        yyk : ⟨ fst yy ∈ finiteStage k ⟩
        yyk = subst (λ t → ⟨ fst yy ∈ Lset t ⟩) qb yy∈

以前驱数码为索引的表项记录了关系 r。把第一分量从 fst c 化为 # m 后，正确性假设 vals 便把 r 的底层集合认同为 relAt m。

        rval : fst r ≡ fst (relAt m)
        rval = vals m hm r
          (subst (λ t → ⟨ pr t (fst r) ∈ fst (lookup f γ) ⟩) qc hf)

步进见证起初在 Lset (fst c) 上用 r 所持的关系比较两个端点。等式 fst c ≡ # m 与 fst r ≡ fst (relAt m) 把它改写为 precedes (Rel m) (finiteStage m)。

        atM : ⟨ precedes (Rel m) (finiteStage m) (fst xx) (fst yy) ⟩
        atM = subst (λ t → ⟨ precedes (λ s u → pr s u ∈ t) (finiteStage m)
                              (fst xx) (fst yy) ⟩) rval
          (subst (λ t → ⟨ precedes (Held r) (Lset t) (fst xx) (fst yy) ⟩) qc
            hprec)

为了得到递归比较，precedes-map 把基底关系 Rel m 换成 before m。由于基底关系出现在一致性条件的前件中，它所需的假设方向相反，即从 before m 走向 relAt m 中的隶属。因此先得到 before (suc m)，再由等式 k ≡ suc m 得到 before k。

        below : ⟨ before k (fst xx) (fst yy) ⟩
        below = subst (λ j → ⟨ before j (fst xx) (fst yy) ⟩) (sym ksuc)
          (precedes-map (Rel m) (before m) (finiteStage m) (fst xx) (fst yy)
            (λ w t hw ht hbf → relAt-fill m w t hw ht hbf) atM)

在反方向上，要把由 RelOf k 描述的成员化为语义步进见证。两个端点已经给出；余下的任务是恢复前驱索引及其关系表项，并证明此前驱是界中的极大成员。

    from : (x : V ℓ) → RelOf k x → StepOf b f γ x
    from x (xx , (yy , (xx∈ , (yy∈ , (qx , hbf))))) =
      numS m , (relAt m , (xx , (yy , (c∈ , (cmax , (hf , (xxb , (yyb
        , (qx , hprec)))))))))
      where

当 k 为零时，before k 不可能有证明。因此，引理 before-suc 从现有比较中取出自然数 m，使该比较发生在后继层。

      m : ℕ
      m = before-suc k (fst xx) (fst yy) hbf .fst

同一次后继分析还给出等式 k ≡ suc m。该等式把第 k 层的比较与以第 m 层数据为基底的递归步联系起来。

      qk : k ≡ suc m
      qk = before-suc k (fst xx) (fst yy) hbf .snd

由于 k 等于 suc m，前驱满足 m < k。这个界使证明能够在索引 m 处同时使用逼近表的正确性与完备性假设。

      hm : m < k
      hm = subst (λ j → m < j) (sym qk) NatOrder.≤-refl

表示前驱的数码必须属于 b 中保存的界。不等式 m < k 给出 # m ∈ # k；关于 numS m 与界的等式再把这项隶属关系化为所需形式。

      c∈ : ⟨ fst (numS m) ∈ fst (lookup b γ) ⟩
      c∈ = subst (λ t → ⟨ fst (numS m) ∈ t ⟩) (sym qb)
        (subst (λ t → ⟨ t ∈ # k ⟩) (sym (numS-fst m)) (#mono m k hm))

还需证明 # m 是 # k 的成员中的极大者。给定 d ∈ # k 与 # m ∈ d，数码消去只在命题截断中把 d 表成某个满足 j < k 的 # j；这两项隶属将同时迫使 m < j 与 j ≤ m。

      cmax : (d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩
           → ⟨ fst (numS m) ∈ fst d ⟩ → Empty.⊥
      cmax d hd hc = PT.rec Empty.isProp⊥ step
        (∈#-elim k (fst d) (subst (λ t → ⟨ fst d ∈ t ⟩) qb hd))
        where

在 d ≡ # j 的分支中，d 属于 # k = # (suc m) 给出 j ≤ m。另一方面，# m 属于 d 给出严格不等式 m < j，自然数序的非对称性遂排除该分支。

        step : Σ[ j ∈ ℕ ] ((j < k) × (fst d ≡ # j)) → Empty.⊥
        step (j , (hj , qd)) = <-asym mj (pred-≤-pred (subst (λ i → j < i) qk hj))
          where
          mj : m < j
          mj = #∈#-elim m j