层序的内部表

related-in : relOf (orderAt α oα) a b → ⟨ Related α (pr (a .fst) (b .fst)) ⟩
related-in h = ∣ oα , ∣ a , ∣ b , (refl , ∣ h ∣₁) ∣₁ ∣₁ ∣₁

反向读式刻意采用更窄的形状。输入对象已经被呈现为固定端点 a,b 的编码对；只有在这种呈现下，证明才能把存在性表示中的对与这两个端点比较，并恢复它们的层序比较。它不会把任意被关联对象分解成一对选定端点。

related-out : ⟨ Related α (pr (a .fst) (b .fst)) ⟩ → relOf (orderAt α oα) a b
related-out h = strict α oα a b (rec₁ squash₁ atOrd h)
  where
  atPair : (o : IsOrd α) (a' b' : Mem (Lset α))
         → (pr (a .fst) (b .fst) ≡ pr (a' .fst) (b' .fst))

设截断记录给出端点 a',b' 与序数性证明 o。两条编码对的相等分别认同 a 与 a'、b 与 b'；序数性的命题性则认同 o 与固定证明 oα。沿这三项认同搬运被记录的比较，便得到固定端点处的截断比较。

         → ⟨ Ordering α o a' b' ⟩ → ⟨ Ordering α oα a b ⟩
  atPair o a' b' q = map₁
    (λ k → subst2 (relOf (orderAt α oα)) (sym ea) (sym eb)
      (subst (λ o' → relOf (orderAt α o') a' b') (isPropIsOrd α o oα) k))
    where

对编码的单射性先恢复底层端点集的相等。每个端点都是由集合及其属于 Lset α 的证明组成的依值对；由于该证明是命题，第一分量的相等可以提升为完整元素的相等。比较因而能在正确的依值类型中搬运。

    ea : a ≡ a'
    ea = Σ≡Prop (λ x → (x ∈ Lset α) .snd) (pr-inj q .fst)
    eb : b ≡ b'
    eb = Σ≡Prop (λ x → (x ∈ Lset α) .snd) (pr-inj q .snd)

外层序数证书是显式的，而两个端点都只在命题截断下存在。因此，消去逐层进入命题 Ordering α oα a b。这个目标允许证明临时使用代表，却不会让任一端点作为选定资料逸出。

  atOrd : Σ[ o ∶ IsOrd α ] ⟨ ∃[ a' ∶ Mem (Lset α) ] (∃[ b' ∶ Mem (Lset α) ] ((pr (a .fst) (b .fst) ≡ pr (a' .fst) (b' .fst))
               , setIsSet _ (pr (a' .fst) (b' .fst))) ⊓ Ordering α o a' b') ⟩
        → ⟨ Ordering α oα a b ⟩
  atOrd (o , h₁) = rec₁ squash₁
    (λ { (a' , h₂) → rec₁ squash₁

两个临时端点都被打开后，对齐有序对的论证给出 a,b 处的截断比较；随后 strict 把这一特定截断比较化为所需见证。复合后的证明完成反向读式，同时保留所有存在量词的截断边界，只有经三岐性论证的比较见证被恢复出来。

      (λ { (b' , (q , hr)) → atPair o a' b' q hr }) h₂ }) h₁

private
  memL : Mem (Lset α) → S
  memL c = c .fst , Lset→isL α oα (c .fst) (c .snd)

模型中由打包端点组成的内部有序对，与其底层集在宿主层组成的 Kuratowski 对在命题上相等，但二者不被当作定义性相同。把「属于 r」施于这条等式，便得到第一条搬运桥。

  atRel : (a b : Mem (Lset α))
        → ((prʟ (memL a) (memL b)) .fst ∈ r .fst)
        ≡ (pr (a .fst) (b .fst) ∈ r .fst)
  atRel a b = cong (λ x → x ∈ r .fst) (prʟ-fst (memL a) (memL b))

把 Related α 施于同一条有序对等式，得到语义一侧的配套桥。两条桥结合起来，便可先在内部有序对处使用实现证明，再把结论改述为底层集的朴素有序对，反向亦然。

  atRelated : (a b : Mem (Lset α))
            → ⟨ Related α ((prʟ (memL a) (memL b)) .fst) ⟩
            ≡ ⟨ Related α (pr (a .fst) (b .fst)) ⟩
  atRelated a b = cong (λ x → ⟨ Related α x ⟩) (prʟ-fst (memL a) (memL b))

填充方向从两个元素的一项宿主层比较出发。Related 的正向读式把它化为编码对的关联性，实现证明再把关联性化为属于 r，最后由有序对桥把陈述搬回宿主对。因此，orderAt 所比较的每一对都属于任意实现集合。

rel-fill : (a b : Mem (Lset α)) → relOf (orderAt α oα) a b
         → ⟨ pr (a .fst) (b .fst) ∈ r .fst ⟩
rel-fill a b h = subst ⟨_⟩ (atRel a b)
  (hr (prʟ (memL a) (memL b)) .snd
    (transport (sym (atRelated a b)) (related-in α oα a b h)))

读取方向反向走过同一条路径。宿主对的成员关系先搬到内部对处，经实现证明向外读成 Related 事实，再搬回固定的宿主对，最终由 related-out 化为未截断的层序比较。

rel-rep : (a b : Mem (Lset α))
        → ⟨ pr (a .fst) (b .fst) ∈ r .fst ⟩ → relOf (orderAt α oα) a b
rel-rep a b h = related-out α oα a b
  (transport (atRelated a b)
    (hr (prʟ (memL a) (memL b)) .fst (subst ⟨_⟩ (sym (atRel a b)) h)))

后续有些论证使用小呈现 ⟪ Lset α ⟫，而不直接使用依值元素对。呈现中的索引嵌入底层集合，并携带恰好足以组成 Mem (Lset α) 元素的成员关系证明。

private
  atIx : ⟪ Lset α ⟫ → Mem (Lset α)
  atIx m = ⟪ Lset α ⟫↪ m , memOf (Lset α) m

沿这个呈现搬运 orderAt，得到小索引类型上的严格序。这只是同一比较经嵌入后的读法，因此相应的表示定理无须新的序论论证。

open SWO (carry (Lset α) (orderAt α oα)) using () renaming ( _<∙_ to _≺ᶜ_ )

对呈现索引 u,v，搬运后的比较先被读成相应层元素之间的比较。先前的填充定理随后把嵌入端点所成的 Kuratowski 对放入 r。这就是从比较到成员关系的小索引形式。

ixRel-fill : (u v : ⟪ Lset α ⟫) → u ≺ᶜ v
           → ⟨ pr (⟪ Lset α ⟫↪ u) (⟪ Lset α ⟫↪ v) ∈ r .fst ⟩
ixRel-fill u v = rel-fill (atIx u) (atIx v)

反过来，嵌入端点所成的对属于 r，经先前定理读成相应层元素的比较。按照搬运序的定义，这恰是小呈现中 u 与 v 的严格比较。

ixRel-rep : (u v : ⟪ Lset α ⟫)
          → ⟨ pr (⟪ Lset α ⟫↪ u) (⟪ Lset α ⟫↪ v) ∈ r .fst ⟩ → u ≺ᶜ v
ixRel-rep u v = rel-rep (atIx u) (atIx v)

变元形式的假设是逐点且真正双向的：它既把满足公式的编码对象读成被关联的对，也从关联性构造公式的满足。这里仅要求序数以下条目的正确性与命题截断下的存在性，并不假设精确定义域，因此可能的界外条目不参与这项语义认同。

当序数与表已成为固定模型元素后，常元形式的等式给出同样的逐点等价。分离所用的定义公式只为可能的关系元素保留一个自由槽，因此需要这种第二种呈现。该等式认同两种语境的含义，而不声称 Cond 与 Cond₀ 在语法上相等。

给定变元条件后，StepAt v b f 外延地刻画候选取值：一个对象属于槽位 v 中的取值，当且仅当它满足 Cond b f。这是一项双向成员关系规格，而不是存在定理。实现该规格的实际集合将在后面的递归中由替换与分离产生。

StepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
StepAt v b f = extAt v (Cond b f)

固定候选取值、序数索引与较低层表的三个槽位，并给定一个满足序数性、取值可靠性与命题截断下表项存在性的环境。在这些假设下，充分性等式为条件给出统一的逐点含义。随后的两条读式将从相反方向使用它：外延步进规格产生候选取值的 IsRel 证明，而已有的 IsRel 证明填充该规格。在后续章节给出具体实例以前，整个构造始终以这条假设的步进描述为参数。

module _ {n : ℕ} (v b f : Fin n) (γ : Vec S n)
         (ob : IsOrd ((lookup b γ) .fst))
         (vals : Values (lookup f γ) ((lookup b γ) .fst))
         (ents : Entries (lookup f γ) ((lookup b γ) .fst)) where

private

  same : (z : S) → ((z ∷ γ) ⊨ Cond b f) ≡ Related ((lookup b γ) .fst) (z .fst)
  same = cond-spec b f γ ob vals ents

step-rel : ⟨ γ ⊨ StepAt v b f ⟩ → IsRel ((lookup b γ) .fst) (lookup v γ)
step-rel h z =
    (λ hz → subst ⟨_⟩ (same z) (extAt-out v (Cond b f) γ h z hz))
  , (λ hz → extAt-in v (Cond b f) γ h z (subst ⟨_⟩ (sym (same z)) hz))

step-table : IsRel ((lookup b γ) .fst) (lookup v γ) → ⟨ γ ⊨ StepAt v b f ⟩
step-table sp = extAt-in-both v (Cond b f) γ
  (λ z hz → subst ⟨_⟩ (sym (same z)) (sp z .fst hz))
  (λ z h → sp z .snd (subst ⟨_⟩ (same z) h))

诸逼近，与那个图

现在把通用递归形状专用于这条步进。逼近是集合编码的表，它具有指定定义域，并使每个已记录条目满足相应步进；图断言存在这样的逼近来支撑当前实参处的取值；成对图则把实参与该取值一起记录。相应的引入和消去原则使后文能按这些含义推理，而不必从命题截断的存在中选出见证。

module A = RecShape StepAt
open A using ( ApproxAt; GraphAt; ApproxAt-dom; ApproxAt-value; ApproxAt-step
             ; ApproxAt-in; GraphOf; Graph-in; Graph-out
             ; PairGraphAt; PairOf; PairGraph-in; PairGraph-out )

逼近所记录的每个取值

为了证明逼近只记录正确取值，先固定其表与定义域，再考察一个可能的实参 u。归纳性质说：若 u 可构造且为序数，则每个已记录对 (u,r) 的取值 r 都实现 u 处的关系。这里有意对所有已记录取值量化，因此没有预先假设单值性。

module _ {n : ℕ} (f a : Fin n) (γ : Vec S n) where

private
  Value : V ℓ → Type (ℓ-suc ℓ)
  Value u = ⟨ isL u ⟩ → IsOrd u → (r : S)
          → ⟨ pr u (r .fst) ∈ (lookup f γ) .fst ⟩ → IsRel u r

approx-val : ⟨ γ ⊨ ApproxAt f a ⟩ → IsOrd ((lookup a γ) .fst)
           → (c : S) → IsOrd (c .fst) → (r : S)
           → ⟨ pr (c .fst) (r .fst) ∈ (lookup f γ) .fst ⟩ → IsRel (c .fst) r
approx-val h oa c = ∈-induction {P = Value} go (c .fst) (c .snd)
  where

  go : (u : V ℓ) → ((t : V ℓ) → ⟨ t ∈ u ⟩ → Value t) → Value u
  go u IH hu ou r p = step-rel zero (suc zero) (sh2 f) (r ∷ d ∷ γ) ou vals ents
    (ApproxAt-step f a γ h d r p)
    where
    d : S

    d = u , hu
    u∈a : ⟨ u ∈ (lookup a γ) .fst ⟩
    u∈a = ApproxAt-dom f a γ h d r p
    vals : Values (lookup f γ) u
    vals e t e∈ q =

      IH (e .fst) e∈ (e .snd) (mem-ord {A = u} ou (e .fst) e∈) t q
    ents : Entries (lookup f γ) u
    ents e e∈ = ApproxAt-value f a γ h e (oa .fst {x = u} {y = e .fst} e∈ u∈a)

图对别的什么都不成立

图的断言只以命题截断形式包含支撑它的逼近见证。不过，所需结论「图中取值实现序数实参处的关系」本身是命题，因此可以把该命题截断消去到此结论中。这一步确立图取值的正确性；若要得到唯一性，仍须再用外延性比较两个实现集合。

module _ {n : ℕ} (w b : Fin n) (γ : Vec S n) where

graph-only : ⟨ γ ⊨ GraphAt w b ⟩ → IsOrd ((lookup b γ) .fst)
           → IsRel ((lookup b γ) .fst) (lookup w γ)
graph-only h ob = rec₁ ((Realizes ((lookup b γ) .fst) (lookup w γ)) .snd)
  read (Graph-out w b γ h)

  where
  read : GraphOf w b γ → IsRel ((lookup b γ) .fst) (lookup w γ)
  read (f , (ha , hs)) = step-rel (suc w) (suc b) zero (f ∷ γ) ob vals ents hs
    where
    vals : Values f ((lookup b γ) .fst)

    vals c r c∈ p = approx-val zero (suc b) (f ∷ γ) ha ob c
      (mem-ord {A = (lookup b γ) .fst} ob (c .fst) c∈) r p
    ents : Entries f ((lookup b γ) .fst)
    ents = ApproxAt-value zero (suc b) (f ∷ γ) ha

graph-table : (h : S) → IsOrd ((lookup b γ) .fst)
            → Values h ((lookup b γ) .fst) → Entries h ((lookup b γ) .fst)
            → Domain h ((lookup b γ) .fst)
            → IsRel ((lookup b γ) .fst) (lookup w γ) → ⟨ γ ⊨ GraphAt w b ⟩
graph-table h ob vals ents dom sp = Graph-in w b γ h approx

  (step-table (suc w) (suc b) zero (h ∷ γ) ob vals ents sp)
  where
  onDom : (c : S)
        → (⟨ ∃[ r ∶ S ] pr (c .fst) (r .fst) ∈ h .fst ⟩
           → ⟨ c .fst ∈ (lookup b γ) .fst ⟩)

        × (⟨ c .fst ∈ (lookup b γ) .fst ⟩
           → ⟨ ∃[ r ∶ S ] pr (c .fst) (r .fst) ∈ h .fst ⟩)
  onDom c = (λ hr → rec₁ ((c .fst ∈ (lookup b γ) .fst) .snd)
                      (λ { (r , p) → dom c r p }) hr)
          , ents c

  onStep : (c r : S) → ⟨ pr (c .fst) (r .fst) ∈ h .fst ⟩
         → ⟨ (r ∷ c ∷ h ∷ γ) ⊨ StepAt zero (suc zero) (suc (suc zero)) ⟩
  onStep c r p = step-table zero (suc zero) (suc (suc zero)) (r ∷ c ∷ h ∷ γ)
    oc vals' ents' (vals c r c∈ p)
    where

    c∈ : ⟨ c .fst ∈ (lookup b γ) .fst ⟩
    c∈ = dom c r p
    oc : IsOrd (c .fst)
    oc = mem-ord {A = (lookup b γ) .fst} ob (c .fst) c∈
    vals' : Values h (c .fst)

    vals' e t _ q = vals e t (dom e t q) q
    ents' : Entries h (c .fst)
    ents' e e∈ = ents e (ob .fst {x = c .fst} {y = e .fst} e∈ c∈)

  approx : ⟨ (h ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
  approx = ApproxAt-in zero (suc b) (h ∷ γ)
    (domAt-intro zero (suc b) (h ∷ γ) onDom) onStep

成对的那个图

替换作用于一张以完整表项为取值的图。因而，PairGraphAt 断言所显示的取值是当前索引与某个关系集组成的 Kuratowski 对，并且该关系集在此索引处满足 GraphAt。它的两条读式都把关系集见证保留在命题截断之内。这就把取值为关系集的递归连接到由带索引条目组成的替换图像。

那张表，与界上的那个关系

类 Recorded B 描述界 B 以下一张表应有的元素。一个对象属于该类，是指以命题截断形式存在模型元素 c 与 r，其中 c 属于 B，r 实现 c 处的关系，而且该对象等于二者底层集合组成的有序对。定义本身不要求 B 为序数；在序数界上使用这个类时，序数性才发挥作用。

Recorded : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Recorded B z = ∃[ c ∶ S ] (c .fst ∈ B) ⊓ (∃[ r ∶ S ]
  ((z ≡ pr (c .fst) (r .fst)) , setIsSet z (pr (c .fst) (r .fst)))
  ⊓ Realizes (c .fst) r)

模型中的集合若要成为 B 的表，它的成员关系必须逐点等价于属于 Recorded B。两个方向都不可缺少：一个排除不相关对象和定义域外对象，另一个纳入每个满足 c∈B 且 r 实现 c 处关系的对 (c,r)。因此，IsTable 表达的是精确表示，而不只是对正确条目的封闭性。

IsTable : V ℓ → S → Type (ℓ-suc (ℓ-suc ℓ))
IsTable B h = (z : S) → (z .fst ∈ h .fst) ≡ Recorded B (z .fst)

α 处的递归资料包含模型中的两个集合：一张精确表示 α 以下所有正确条目的表，以及一个实现 α 本身之关系的集合。处理更大实参时，第一个分量提供验证逼近所需的既有表，第二个分量提供要写入后续表的关系取值。这个包是沿成员关系递归返回的数据。这里没有证明其类型是命题，也不需要这样的证明，因为沿成员关系的归纳接受任意 Type 值类型族。

Bundle : V ℓ → Type (ℓ-suc (ℓ-suc ℓ))
Bundle α = Σ[ h ∶ S ] Σ[ r ∶ S ] (IsTable α h × IsRel α r)

固定界 B 的一张精确表 h。要在具体条目处使用其规格，必须对齐两种有序对：模型元素构成的内部对，以及其底层集合构成的宿主层 Kuratowski 对。内部配对的投影律把表的成员关系等价搬运到 (c,r) 的底层有序对处。

module _ (B : V ℓ) (oB : IsOrd B) (h : S) (sp : IsTable B h) where

private
  atPair : (c r : S)
         → (pr (c .fst) (r .fst) ∈ h .fst) ≡ Recorded B (pr (c .fst) (r .fst))
  atPair c r = subst (λ x → (x ∈ h .fst) ≡ Recorded B x) (prʟ-fst c r)

    (sp (prʟ c r))

table-out : Domain h B × Values h B
table-out = (λ c r p → read c r p .fst) , (λ c r _ p → read c r p .snd)
  where
  read : (c r : S) → ⟨ pr (c .fst) (r .fst) ∈ h .fst ⟩
       → ⟨ c .fst ∈ B ⟩ × IsRel (c .fst) r

  read c r p = rec₁ isPropBoth outer (subst ⟨_⟩ (atPair c r) p)
    where
    isPropBoth : isProp (⟨ c .fst ∈ B ⟩ × IsRel (c .fst) r)
    isPropBoth = isProp× ((c .fst ∈ B) .snd) ((Realizes (c .fst) r) .snd)

    inner : (d t : S) → ⟨ d .fst ∈ B ⟩
          → (pr (c .fst) (r .fst) ≡ pr (d .fst) (t .fst)) → IsRel (d .fst) t
          → ⟨ c .fst ∈ B ⟩ × IsRel (c .fst) r
    inner d t d∈ q hr =
        subst (λ x → ⟨ x ∈ B ⟩) (sym (pr-inj q .fst)) d∈

      , subst2 IsRel (sym (pr-inj q .fst)) (sym rt) hr
      where
      rt : r ≡ t
      rt = Σ≡Prop (λ x → (isL x) .snd) (pr-inj q .snd)

    outer : Σ[ d ∶ S ] ( ⟨ d .fst ∈ B ⟩
              × ⟨ ∃[ t ∶ S ] ((pr (c .fst) (r .fst) ≡ pr (d .fst) (t .fst))
                    , setIsSet _ (pr (d .fst) (t .fst))) ⊓ Realizes (d .fst) t ⟩ )
          → ⟨ c .fst ∈ B ⟩ × IsRel (c .fst) r
    outer (d , (d∈ , hs)) = rec₁ isPropBoth

      (λ { (t , (q , hr)) → inner d t d∈ q hr }) hs

table-in : (c r : S) → ⟨ c .fst ∈ B ⟩ → IsRel (c .fst) r
         → ⟨ pr (c .fst) (r .fst) ∈ h .fst ⟩
table-in c r c∈ hr = subst ⟨_⟩ (sym (atPair c r))
  ∣ c , (c∈ , ∣ r , (refl , hr) ∣₁) ∣₁

在通过分离得到序数 α 处的关系之前，需要先在 L 中找到一个集合，容纳所有可能的相关有序对。所需的界返回模型集合 D，使 Related α 中的每个对象都属于 D。它只是共同容器，可能含有无关元素；此时并不声称精确性。

bound : (α : V ℓ) (oα : IsOrd α)
      → Σ[ D ∶ S ] ((z : S) → ⟨ Related α (z .fst) ⟩ → ⟨ z .fst ∈ D .fst ⟩)
bound α oα = d .fst , confine
  where
  ixL : ⟪ Lset α ⟫ → S

Lset α 的小呈现为其所有元素提供索引。每个索引所呈现的底层集合与其可构造性证明打包，成为模型元素；该证明来自它对可构造层的成员关系。于是，每个被呈现端点都可用于内部有序配对。

  ixL m = ⟪ Lset α ⟫↪ m , Lset→isL α oα (⟪ Lset α ⟫↪ m) (memOf (Lset α) m)

呈现索引的有序对形成一个小索引类型。把共同定义域原则应用于这些索引所对应的内部有序对族，便得到模型集合 D，其中包含该族的每个元素。这条原则只给出包含关系，既不计算精确像，也不按照层序筛选有序对。

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

共同界不仅要适用于呈现索引，还要适用于 Lset α 的普通元素 a,b。先用各自的纤维索引表示这两个元素，再对相应内部有序对使用共同界，并沿「被呈现有序对等于宿主层有序对 pr(a,fst .fst b)」的等式搬运成员关系。因此，该层任意两个元素组成的有序对都属于 D。

  onPair : (a b : Mem (Lset α)) → ⟨ pr (a .fst) (b .fst) ∈ (d .fst) .fst ⟩
  onPair a b = subst (λ x → ⟨ x ∈ (d .fst) .fst ⟩)
    (prʟ-fst (ixL (fa .fst)) (ixL (fb .fst))
      ∙ cong₂ pr (fa .snd) (fb .snd))
    (d .snd (fa .fst , fb .fst))

a 与 b 的成员关系证明把它们分别认同为小呈现中的元素，所得纤维等式对齐两个端点；有序配对的合同性进而对齐两个宿主层有序对。再结合内部配对的投影律，就得到上一段搬运所需的等式。

    where
    fa = ∈-asFiber {a = a .fst} {b = Lset α} (a .snd)
    fb = ∈-asFiber {a = b .fst} {b = Lset α} (b .snd)

现取 Related α 中的任意对象。它的定义通过三层嵌套且经过命题截断的存在量词，给出序数性证明、Lset α 的两个元素 a,b，以及把该对象认同为二者有序对的等式；层序比较本身还保留在命题截断之内。目标「属于 D」是命题，因此可以逐层消去三层存在量词的命题截断。这个粗略界只依赖两个端点及有序对等式，连截断后的比较事实也无须使用。

  confine : (z : S) → ⟨ Related α (z .fst) ⟩ → ⟨ z .fst ∈ (d .fst) .fst ⟩
  confine z = rec₁ ((z .fst ∈ (d .fst) .fst) .snd)
    (λ { (_ , h₁) → rec₁ ((z .fst ∈ (d .fst) .fst) .snd)
      (λ { (a , h₂) → rec₁ ((z .fst ∈ (d .fst) .fst) .snd)
        (λ { (b , (q , _)) →

由前面的结论，恢复出的两个端点所成有序对已经属于 D。沿所恢复有序对等式的反向搬运这项成员关系，就得到原对象属于 D。这些见证只留在命题证明内部，所以该界并没有为每个相关对象选择端点。

          subst (λ x → ⟨ x ∈ (d .fst) .fst ⟩) (sym q) (onPair a b) }) h₂ }) h₁ })

表与当前关系通过沿成员关系的递归同时构造。它的实际输入范围是配有可构造性证明的序数：α 同时带有属于 L 的证明和序数性证明。递归取值是前述包，而定义被封装，使后文通过规格使用它。该递归允许 Type 值类型族，并不依赖 Bundle α 是命题。

opaque
  tableAt : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → Bundle α
  tableAt = ∈-induction {P = λ α → ⟨ isL α ⟩ → IsOrd α → Bundle α}
    (build (PairGraphAt zero (suc zero)) refl)
    where

在 α 处的归纳步中，递归假设说：对 α 的每个元素 δ，只要给出其可构造性与序数性，就有相应的包。当前任务是产生 α 以下的表以及 α 处的关系。成对图公式作为显式参数保留，并带有它等于预期公式的证明；这不增加数学假设，只保证替换论证使用的正是那张图。

    build : (φ : Formula S ) → φ ≡ PairGraphAt zero (suc zero)
          → (α : V ℓ)
          → ((δ : V ℓ) → ⟨ δ ∈ α ⟩ → ⟨ isL δ ⟩ → IsOrd δ → Bundle δ)
          → ⟨ isL α ⟩ → IsOrd α → Bundle α
    build φ qφ α IH hα oα = rep .fst .fst , (sep .fst .fst , (spec , rspec))

序数 α 与其可构造性证明组成模型元素 A。它将作为考察成对图的内部定义域；其中的元素正是那些更小集合，只要建立其序数性，沿成员关系的递归假设便可处理它们。

      where
      A : S
      A = α , hα

序数 α 的每个元素 c 本身仍是序数。这项继承的序数性不可缺少，因为递归构造只定义在可构造序数上，而不是任意可构造元素上。取得这份序数性证明不涉及命题截断。

      ordOf : (c : S) → ⟨ c .fst ∈ α ⟩ → IsOrd (c .fst)
      ordOf c c∈ = mem-ord {A = α} oα (c .fst) c∈

对于 c∈α，模型元素 c 已携带其可构造性证明，而序数元素法则给出其序数性。这些正是应用归纳假设所需的输入。所得结果是 c 处的完整包，其中同时含有 c 以下的精确表和 c 处的关系实现集合。

      bun : (c : S) → ⟨ c .fst ∈ α ⟩ → Bundle (c .fst)
      bun c c∈ = IH (c .fst) c∈ (c .snd) (ordOf c c∈)

从 c 处的递归包中取出当前关系分量，并把它作为 c 处的取值。它是一个具体的模型元素，并非从表的命题截断 Entries 字段中抽出的见证。递归之所以把定义域内每个可构造序数处的关系与其下的表一同携带，正是为了得到这样的具体取值。

      value : (c : S) → ⟨ c .fst ∈ α ⟩ → S
      value c c∈ = bun c c∈ .snd .fst

与该分量一同存储的规格断言：所选取值实现 Related c。这恰是归纳假设所提供的语义正确性。仅凭这项事实，既不能断言该取值满足成对图，也不能断言它与 c 组成的有序对已属于一张完成的表。

      relOK : (c : S) (c∈ : ⟨ c .fst ∈ α ⟩) → IsRel (c .fst) (value c c∈)
      relOK c c∈ = bun c c∈ .snd .snd .snd

对每个底层序数属于 α 的 c，归纳假设已经给出 c 处的关系集。替换必须保留产生该关系的索引，因此它的候选取值是 c 与这个关系集组成的内部有序对，而不是裸关系集。

      entry : (c : S) → ⟨ c .fst ∈ α ⟩ → S
      entry c c∈ = prʟ c (value c c∈)

还须证明这个候选取值落在替换所用的图上。在组成有序对之前，选定的关系集必须满足 c 处的递归图。c 处的包同时给出其下方的表与该处已实现的关系，而 c 属于序数 α 又保证 c 本身是序数，因而可以应用从表到图的一般论证。

      below : (c : S) (c∈ : ⟨ c .fst ∈ α ⟩) (k : S)
            → ⟨ (value c c∈ ∷ k ∷ c ∷ []) ⊨ GraphAt zero (suc (suc zero)) ⟩
      below c c∈ k = graph-table zero (suc (suc zero))
        (value c c∈ ∷ k ∷ c ∷ []) (bun c c∈ .fst) (ordOf c c∈)
        (reads .snd) ents (reads .fst) (relOK c c∈)

下方那张表的精确规格给出该论证所需三项事实中的两项：c 以下每个被记录的取值都实现相应关系，并且没有索引在 c 之外的有序对被记录。余下的是完备性，即 c 的每个元素处都有某个被记录的取值。

        where
        reads : Domain (bun c c∈ .fst) (c .fst) × Values (bun c c∈ .fst) (c .fst)
        reads = table-out (c .fst) (ordOf c c∈) (bun c c∈ .fst)
                  (bun c c∈ .snd .snd .fst)
        ents : Entries (bun c c∈ .fst) (c .fst)