BedrockThe earliest-disagreement family, internalized
上一章留下一条敞着的假设，并把它点得很准：一条公式，说「在某个槽位所持有的数码处、按最先分歧处的那个序」把第二个槽位排在第三个之前，连同它对着有穷那一章的 before 的两条读式。极限之序的其余部分早已是无条件的。本章兑现那条假设，并连带兑现它前面那一章。
要造的是沿诸数码的一场递归，其取值是关系：零处是空关系，而 n 之后那个数码处，是在 n 处的阶段之上按最先分歧处的比较，以 n 处的关系为基底。取值为集合的递归没法被一个词项点名，故被描述的是逼近，与塔、与序之表被描述的方式一模一样：一个逼近谓词、一个对诸逼近作量化的图、一条把逼近所记录的每个取值钉住的值引理，以及那个对象自身在造出之处封印。
有两件事使它比塔更便宜。索引是 ωʟ 的成员，而后者是个集合，故外层归纳是对一个自然数作的，层级那一章那半场真类收集根本不会出现；而那一步已经写好，因为上一章的 PrecedesAt 把基底关系与基底阶段握在槽位里，正是为了让它能站在「关系是某场递归之取值」的地方。也有两件事使它更贵。某个数码处的取值是关系而非阶段，故每一步都要在一个有穷阶段的诸对之上付一次分离；而上一个关系要抵达一致性子句内部的一个槽位，那正是会撞墙的形状，故它以变元身份携带自己的定义等式到场，绝不以应用的身份到场。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Choice.Before {ℓ : 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 ( 𝒮ᵥ; extensionalV ) open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′ ) 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 ) open import L.Axioms.Basic {ℓ} using ( 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 ( ωʟ ) open import L.Choice.Finite {ℓ} lem using ( before; precedes; Agrees; Witness; finiteStage ) open import L.Choice.Limit {ℓ} lem using ( PrecedesAt; module Precedes; module Described ) open import L.Coding.Sequence {ℓ} lem using ( LsetGraphAt ) open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines ) open import L.Coding.Model {ℓ} using ( numL; prAtL; prAtL-adequate; prʟ; prʟ-fst ; appAt; appAt-adequate; domAt; domAt-in; domAt-out; domAt-intro ; 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 ( _<_; <-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 ) 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 TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module ModelL = FOL.ZFModel 𝒮ʟ open ModelL using ( SetOf ) module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ) private sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i) sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n)))) sh4 i = sh2 (sh2 i) sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n)))))) sh6 i = sh2 (sh4 i) -- perf: the finite stage and the numerals are sealed where they are built opaque stageS : ℕ → S stageS n = LsetS (# n) (numeral-ord n) stageS-fst : (n : ℕ) → fst (stageS n) ≡ finiteStage n stageS-fst n = refl numS : ℕ → S numS k = # k , numL k numS-fst : (k : ℕ) → fst (numS k) ≡ # k numS-fst k = refl 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 : (A : S) (z : V ℓ) (h : ⟨ z ∈ fst A ⟩) → fst (memS A z h) ≡ z memS-fst A z h = refl prS : S → S → S prS a b = prʟ a b prS-fst : (a b : S) → fst (prS a b) ≡ pr (fst a) (fst b) prS-fst a b = prʟ-fst a b stageEl : (n : ℕ) (x : V ℓ) → ⟨ x ∈ finiteStage n ⟩ → S stageEl n x h = x , Lset→isL (# n) (numeral-ord n) x h
每个阶段的关系，作为 L 的一个元素
某个阶段处的关系所能关联的诸对逃不出单一的一个集合：有穷阶段的诸成员是 L 元素的一个小族，它们的诸对也是，而递归那一章的界层引理一举把它们全部禁闭。把那个关系从那个界上雕出来的分离，正是超出塔的那笔额外开销之所在，而它每个数码付一次。
它据以雕刻的条件，就是上一章那条步进描述，别无其他。那条描述把基底关系与基底阶段握在槽位里，而分离是用单自由变量的公式去雕的，故这两样由存在量词绑定、并用对象等词钉在诸常元上。正是这一点，让那条步进描述能在此处按交付时的原样使用，无须再对着常元写第二份：一条公式，两个消费方。
relAt-out 与 relAt-in 是这场递归的两条读式，二者一并证出，用的是对数码的普通归纳。每个方向都在前趋处花掉另一个，因为上一个关系只在一致性子句内部被查阅，而 precedes-map 就是把它搬过去的那一行：一致性对基底关系是反变的，故从被记录的关系走到 before，需要的是反方向的那条读式。relAt-rep 与 relAt-fill 是消费方想要的推论，落在一个对上、而非落在一个成员上。
-- every pair of members of a finite stage lies in one set of the model 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 : ⟪ 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)) 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))) 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)) where fu = ∈-asFiber {a = u} {b = finiteStage n} hu fv = ∈-asFiber {a = v} {b = finiteStage n} hv -- the base relation transferred across the agreement clause precedes-map : (R R' : V ℓ → V ℓ → Ω) (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 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 ag' w w∈A hR' = ag w w∈A (f w z w∈A z∈A hR') -- the condition the separation carves with: the base relation and the base -- stage arrive as bound variables pinned to constants, so the step description -- stands at slots exactly as it was delivered RelCond : (R A A' : S) → Formula S 1 RelCond R A A' = ∃̇ ( (var zero ≐ con R) ∧̇ ∃̇ ( (var zero ≐ con A) ∧̇ ∃̇∈ (con A') ( ∃̇∈ (con A') ( 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))) .fst .fst relAt-zero : relAt zero ≡ ∅ʟ relAt-zero = refl 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 : ℕ → V ℓ → V ℓ → Ω Rel n a b = pr a b ∈ fst (relAt n) private s1 : Fin 5 s1 = suc zero s2 : Fin 5 s2 = sh2 zero s3 : Fin 5 s3 = sh2 (suc zero) s4 : Fin 5 s4 = sh2 (sh2 zero) 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-out : (k : ℕ) (zv : V ℓ) → ⟨ zv ∈ fst (relAt k) ⟩ → ∥ RelOf k zv ∥₁ relAt-in : (k : ℕ) (zv : V ℓ) → RelOf k zv → ⟨ zv ∈ fst (relAt k) ⟩ 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₁ atR cond where zS : S zS = memS (relAt (suc n)) zv h qz : fst zS ≡ zv qz = memS-fst (relAt (suc n)) zv h 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 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 ⟩ AtY : (r a x : S) → Type (ℓ-suc ℓ) AtY r a x = Σ[ y ∈ S ] (⟨ fst y ∈ fst (stageS (suc n)) ⟩ × Body r a x y) AtX : (r a : S) → Type (ℓ-suc ℓ) AtX r a = Σ[ x ∈ S ] (⟨ fst x ∈ fst (stageS (suc n)) ⟩ × ∥ AtY r a x ∥₁) AtA : (r : S) → Type (ℓ-suc ℓ) AtA r = Σ[ a ∈ S ] ((fst a ≡ fst (stageS n)) × ∥ AtX r a ∥₁) AtR : Type (ℓ-suc ℓ) AtR = Σ[ r ∈ S ] ((fst r ≡ fst (relAt n)) × ∥ AtA r ∥₁) 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∈ , (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 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 module P = Precedes s3 s2 s1 zero (y ∷ x ∷ a ∷ r ∷ zS ∷ []) (Rel n) Rrep Rfill 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) 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 qpair : fst zS ≡ pr (fst x) (fst y) qpair = subst ⟨_⟩ (prAtL-adequate s4 s1 zero (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) hpr atX : (r a : S) → fst r ≡ fst (relAt n) → fst a ≡ fst (stageS n) → AtX r a → ∥ RelOf (suc n) zv ∥₁ atX r a qr qa (x , (x∈ , hy)) = PT.map (atY r a x qr qa x∈) hy atA : (r : S) → fst r ≡ fst (relAt n) → AtA r → ∥ RelOf (suc n) zv ∥₁ atA r qr (a , (qa , hx)) = PT.rec squash₁ (atX r a qr qa) hx atR : AtR → ∥ RelOf (suc n) zv ∥₁ atR (r , (qr , ha)) = PT.rec squash₁ (atA r qr) ha 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 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∈) Rrep : (s t : S) → ⟨ pr (fst s) (fst t) ∈ fst (lookup s3 (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ [])) ⟩ → ⟨ Rel n (fst s) (fst t) ⟩ Rrep s t p = p Rfill : (s t : S) → ⟨ Rel n (fst s) (fst t) ⟩ → ⟨ pr (fst s) (fst t) ∈ fst (lookup s3 (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ [])) ⟩ Rfill s t p = p module P = Precedes s3 s2 s1 zero (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ []) (Rel n) Rrep Rfill 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 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 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) 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) 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 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)) ∣₁) ∣₁) ∣₁) ∣₁ 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 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 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)))))
那一步，对它所查阅的一切保持通用
递归那一步的体只写一次，其中成员、索引与逼近三者都在槽位里，其下有六层绑定：索引的前趋、逼近在那里所记录的关系、前趋处的阶段、索引处的阶段，以及被比较的那两个集合。
前趋不是对象语言的词项，也不必是。数码在隶属之下是一个有穷线序，故它的前趋就是它的 ∈-极大成员，而那是两个原子：c 属于索引，且索引的任何成员都不以 c 为成员。这样写，任何地方都不需要对象等词；而在数码零处根本没有这样的 c，故那一步在那里是空的，而这正是这场递归想要的。
两个阶段经序列那一章的图抵达，而那是抵达一个阶段的唯一办法；索引处的那个阶段则是禁闭取值的东西：没有它，那个外延就是一个真类，因为最先分歧处的比较从不提及被比较的两个集合住在哪里。StepOf 把载荷写了出来、不交给推断，而两条读式都站在变元环境的变元位上，唯一的假设是索引处的序数性。
Held : S → V ℓ → V ℓ → Ω Held r a b = pr a b ∈ fst r 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)) ∧̇ ∃̇ ( appAt (sh2 f) (suc zero) zero ∧̇ ∃̇ ( LsetGraphAt zero (suc (suc zero)) ∧̇ ∃̇ ( LsetGraphAt zero (sh4 b) ∧̇ ∃̇∈ (var zero) ( ∃̇∈ (var (suc zero)) ( prAtL (sh6 z) (suc zero) zero ∧̇ PrecedesAt (suc (suc (suc (suc zero)))) (suc (suc (suc zero))) (suc zero) zero ) ) ) ) ) ) ) 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.⊥) × ( ⟨ 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) ⟩ ) ) ) ) ) ) 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 = ⟨ (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 ⟩ 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) 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 ∥₁) 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' ∥₁ ) AtA : (c r : S) → Type (ℓ-suc ℓ) AtA c r = Σ[ A ∈ S ] ( ⟨ (A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩ × ∥ AtA' c r A ∥₁ ) AtR : (c : S) → Type (ℓ-suc ℓ) AtR c = Σ[ r ∈ S ] ( ⟨ (r ∷ c ∷ γ) ⊨ appAt (sh2 f) (suc zero) zero ⟩ × ∥ AtA c r ∥₁ ) MaxOf : (c : S) → Type (ℓ-suc ℓ) MaxOf c = (d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩ → ⟨ fst c ∈ fst d ⟩ → Empty.⊥ AtC : Type (ℓ-suc ℓ) AtC = Σ[ c ∈ S ] ( ⟨ fst c ∈ fst (lookup b γ) ⟩ × ( ⟨ (c ∷ γ) ⊨ ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ⟩ × ∥ AtR c ∥₁ ) ) 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 γ)) 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') ) ) ) ) ) ) ) ) where Rrep : (s t : S) → ⟨ pr (fst s) (fst t) ∈ fst (lookup (suc (suc (suc (suc zero)))) (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)) ⟩ → ⟨ Held r (fst s) (fst t) ⟩ Rrep s t p = p Rfill : (s t : S) → ⟨ Held r (fst s) (fst t) ⟩ → ⟨ pr (fst s) (fst t) ∈ fst (lookup (suc (suc (suc (suc zero)))) (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)) ⟩ Rfill s t p = p module P = Precedes (suc (suc (suc (suc zero)))) (suc (suc (suc zero))) (suc zero) zero (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) (Held r) Rrep Rfill 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) 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 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)) = PT.map (atY c r A A' x c∈ cmax hf qA qA' x∈) hy 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)) = 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 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' 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∈) 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 γ) ⟩ hf = subst ⟨_⟩ (appAt-adequate (sh2 f) (suc zero) zero (r ∷ c ∷ γ)) happ 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 = hmax d hd hc opaque unfolding RelBodyAt RelBody-out : ⟨ γ ⊨ RelBodyAt z b f ⟩ → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁ RelBody-out h = PT.rec squash₁ atC h 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')) ∣₁) ∣₁) ∣₁) ∣₁) ∣₁)) ∣₁ where oc : IsOrd (fst c) oc = mem-ord {A = fst (lookup b γ)} ob (fst c) c∈ A : S A = LsetS (fst c) oc A' : S A' = LsetS (fst (lookup b γ)) ob hmax : ⟨ (c ∷ γ) ⊨ ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ⟩ hmax d hd hc = cmax d hd hc happ : ⟨ (r ∷ c ∷ γ) ⊨ appAt (sh2 f) (suc zero) zero ⟩ happ = subst ⟨_⟩ (sym (appAt-adequate (sh2 f) (suc zero) zero (r ∷ c ∷ γ))) hf hgA : ⟨ (A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩ hgA = Lset-defines zero (suc (suc zero)) (A ∷ r ∷ c ∷ γ) oc refl hgA' : ⟨ (A' ∷ A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (sh4 b) ⟩ hgA' = Lset-defines zero (sh4 b) (A' ∷ A ∷ r ∷ c ∷ γ) ob refl 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 Rrep : (s t : S) → ⟨ pr (fst s) (fst t) ∈ fst (lookup (suc (suc (suc (suc zero)))) (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)) ⟩ → ⟨ Held r (fst s) (fst t) ⟩ Rrep s t p = p Rfill : (s t : S) → ⟨ Held r (fst s) (fst t) ⟩ → ⟨ pr (fst s) (fst t) ∈ fst (lookup (suc (suc (suc (suc zero)))) (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)) ⟩ Rfill s t p = p module P = Precedes (suc (suc (suc (suc zero)))) (suc (suc (suc zero))) (suc zero) zero (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) (Held r) Rrep Rfill 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 是罩在体上的一次 extAt。ApproxAt 是两个合取项，即定义域与那条步进条件，且刻意没有单值性合取项：步进条件已经把某个实参处记录的每个取值钉住了，故单值性是一条推论。RelGraphAt 是在逼近上的一个存在量词，其下罩着那两个合取项。
四条描述全都在造出之处封印，而这是本章自己的实测、不是继承来的习惯。不封印时，图在具体环境上的每一次满足关系，都要把一条内部装着两份完整层级描述的公式正规化，本章要跑 376 秒；封印之后，每条读式只展开它自己那条描述、别无其他，本章跑 3.8 秒。这是九十九倍，而数学分毫未改。
opaque RelStepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n RelStepAt v b f = extAt v (RelBodyAt zero (suc b) (suc f)) module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) (ob : IsOrd (fst (lookup b γ))) where opaque unfolding RelStepAt 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) 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) 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 ⟩ 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)) opaque ApproxAt : ∀ {n} → Fin n → Fin n → Formula S n ApproxAt f a = domAt f a ∧̇ ∀̇ (∀̇ ( appAt (sh2 f) (suc zero) zero ⇒̇ RelStepAt zero (suc zero) (sh2 f) )) module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) where opaque unfolding ApproxAt ApproxAt-dom : ⟨ γ ⊨ ApproxAt f a ⟩ → (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ fst x ∈ fst (lookup a γ) ⟩ ApproxAt-dom h = domAt-out f a γ (h .fst) ApproxAt-value : ⟨ γ ⊨ ApproxAt f a ⟩ → (x : S) → ⟨ fst x ∈ fst (lookup a γ) ⟩ → ∥ (Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩) ∥₁ ApproxAt-value h = domAt-in f a γ (h .fst) ApproxAt-step : ⟨ γ ⊨ ApproxAt f a ⟩ → (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ (y ∷ x ∷ γ) ⊨ RelStepAt zero (suc zero) (sh2 f) ⟩ ApproxAt-step h x y p = h .snd x y (subst ⟨_⟩ (sym (appAt-adequate (sh2 f) (suc zero) zero (y ∷ x ∷ γ))) p) ApproxAt-in : ⟨ γ ⊨ domAt f a ⟩ → ((x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ (y ∷ x ∷ γ) ⊨ RelStepAt zero (suc zero) (sh2 f) ⟩) → ⟨ γ ⊨ ApproxAt f a ⟩ ApproxAt-in hd hs = hd , λ x y p → hs x y (subst ⟨_⟩ (appAt-adequate (sh2 f) (suc zero) zero (y ∷ x ∷ γ)) p) opaque RelGraphAt : ∀ {n} → Fin n → Fin n → Formula S n RelGraphAt v b = ∃̇ (ApproxAt zero (suc b) ∧̇ RelStepAt (suc v) (suc b) zero) module _ {n : ℕ} (v b : Fin n) (γ : S ^ n) where GraphOf : Type (ℓ-suc ℓ) GraphOf = Σ[ g ∈ S ] ( ⟨ (g ∷ γ) ⊨ ApproxAt zero (suc b) ⟩ × ⟨ (g ∷ γ) ⊨ RelStepAt (suc v) (suc b) zero ⟩ ) opaque unfolding RelGraphAt RelGraph-in : (g : S) → ⟨ (g ∷ γ) ⊨ ApproxAt zero (suc b) ⟩ → ⟨ (g ∷ γ) ⊨ RelStepAt (suc v) (suc b) zero ⟩ → ⟨ γ ⊨ RelGraphAt v b ⟩ RelGraph-in g ha hs = ∣ g , (ha , hs) ∣₁ RelGraph-out : ⟨ γ ⊨ RelGraphAt v b ⟩ → ∥ GraphOf ∥₁ RelGraph-out h = h
那一步，对着这场递归
这是那座桥，而它的两半出自同样两行私有代码。给定索引以下一张正确且完备的表，索引处的那一步恰是元语言在那里算出的那个关系：step-rel 读一个被满足的步进、把关系取回来，rel-step 则由关系写出那一步。
两者都要花掉前趋分析，而那是本章唯一用到自然数三歧的地方：索引中在其内 ∈-极大的成员就是它的前趋，因为严格介于二者之间的数码，一边与极大性相抵触，另一边与隶属相抵触。一旦知道索引是后继，其余便是记账：那里被记录的关系因正确性而是这场递归的取值，那里的阶段因序列那一章的图而是塔的取值，而 precedes-map 在基底关系的两种写法之间搬运那次比较。
Values : S → ℕ → Type (ℓ-suc ℓ) Values g k = (m : ℕ) → m < k → (w : S) → ⟨ pr (# m) (fst w) ∈ fst g ⟩ → fst w ≡ fst (relAt m) Entries : S → ℕ → Type (ℓ-suc ℓ) Entries g k = (m : ℕ) → m < k → ⟨ pr (# m) (fst (relAt m)) ∈ fst g ⟩ 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 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 γ)) ob = subst IsOrd (sym qb) (numeral-ord 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∈)) 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 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 (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))) (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)) xxk : ⟨ fst xx ∈ finiteStage k ⟩ xxk = subst (λ t → ⟨ fst xx ∈ Lset t ⟩) qb xx∈ yyk : ⟨ fst yy ∈ finiteStage k ⟩ yyk = subst (λ t → ⟨ fst yy ∈ Lset t ⟩) qb yy∈ rval : fst r ≡ fst (relAt m) rval = vals m hm r (subst (λ t → ⟨ pr t (fst r) ∈ fst (lookup f γ) ⟩) qc hf) 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) 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) 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 m : ℕ m = before-suc k (fst xx) (fst yy) hbf .fst qk : k ≡ suc m qk = before-suc k (fst xx) (fst yy) hbf .snd hm : m < k hm = subst (λ j → m < j) (sym qk) NatOrder.≤-refl 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)) 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 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 (subst (λ t → ⟨ t ∈ # j ⟩) (numS-fst m) (subst (λ t → ⟨ fst (numS m) ∈ t ⟩) qd hc)) hf : ⟨ pr (fst (numS m)) (fst (relAt m)) ∈ fst (lookup f γ) ⟩ hf = subst (λ t → ⟨ pr t (fst (relAt m)) ∈ fst (lookup f γ) ⟩) (sym (numS-fst m)) (ents m hm) xxb : ⟨ fst xx ∈ Lset (fst (lookup b γ)) ⟩ xxb = subst (λ t → ⟨ fst xx ∈ Lset t ⟩) (sym qb) xx∈ yyb : ⟨ fst yy ∈ Lset (fst (lookup b γ)) ⟩ yyb = subst (λ t → ⟨ fst yy ∈ Lset t ⟩) (sym qb) yy∈ hprec : ⟨ precedes (Held (relAt m)) (Lset (fst (numS m))) (fst xx) (fst yy) ⟩ hprec = subst (λ t → ⟨ precedes (Held (relAt m)) (Lset t) (fst xx) (fst yy) ⟩) (sym (numS-fst m)) (precedes-map (before m) (Rel m) (finiteStage m) (fst xx) (fst yy) (λ w t hw ht hR → relAt-rep m w t hw ht hR) (subst (λ j → ⟨ before j (fst xx) (fst yy) ⟩) qk hbf)) step-rel : ⟨ γ ⊨ RelStepAt v b f ⟩ → fst (lookup v γ) ≡ fst (relAt k) step-rel h = extensionalV {a = fst (lookup v γ)} {b = fst (relAt k)} pt where fwd : (x : V ℓ) → ⟨ x ∈ fst (lookup v γ) ⟩ → ⟨ x ∈ fst (relAt k) ⟩ fwd x hx = PT.rec (snd (x ∈ fst (relAt k))) (λ st → into x (subst (StepOf b f γ) (memS-fst (lookup v γ) x hx) st)) (RelStep-out v b f γ ob h (memS (lookup v γ) x hx) (subst (λ t → ⟨ t ∈ fst (lookup v γ) ⟩) (sym (memS-fst (lookup v γ) x hx)) hx)) bwd : (x : V ℓ) → ⟨ x ∈ fst (relAt k) ⟩ → ⟨ x ∈ fst (lookup v γ) ⟩ bwd x hx = subst (λ t → ⟨ t ∈ fst (lookup v γ) ⟩) (memS-fst (relAt k) x hx) (PT.rec (snd (fst (memS (relAt k) x hx) ∈ fst (lookup v γ))) (λ ro → RelStep-back v b f γ ob h (memS (relAt k) x hx) (subst (StepOf b f γ) (sym (memS-fst (relAt k) x hx)) (from x ro))) (relAt-out k x hx)) pt : (x : V ℓ) → (x ∈ fst (lookup v γ)) ≡ (x ∈ fst (relAt k)) pt x = ⇔toPath (fwd x) (bwd x) rel-step : fst (lookup v γ) ≡ fst (relAt k) → ⟨ γ ⊨ RelStepAt v b f ⟩ rel-step q = RelStep-in v b f γ ob toStep backStep where toStep : (w : S) → ⟨ fst w ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ (fst w) ∥₁ toStep w hw = PT.map (from (fst w)) (relAt-out k (fst w) (subst (λ t → ⟨ fst w ∈ t ⟩) q hw)) backStep : (w : S) → StepOf b f γ (fst w) → ⟨ fst w ∈ fst (lookup v γ) ⟩ backStep w st = subst (λ t → ⟨ fst w ∈ t ⟩) (sym q) (into (fst w) st)
逼近所记录的每个取值
一次归纳，在数码上，在元语言中，逼近与它的定义域保持固定。动机说：逼近在这个数码处所记录的任何取值，都是这场递归在那里的取值。它对一切被记录的取值作量化，故单值性在任何地方都不是假设，而上一节那条裁定在此处白白收取。
这场归纳是良基的、不是结构的，因为某个数码处的那一步查阅的是逼近在它前趋处的取值，而实参是经定义域旅行、不是经构造子旅行。索引以下的完备性正是定义域那个合取项被花掉之处：索引以下的数码落在定义域中，故逼近在那里有取值，而归纳假设把它认同。rel-only 就是那个图为之而写的结论：凡在某个数码处满足它者，都是这场递归在那里的取值。
entryOf : ∀ {n} (f a : Fin n) (γ : S ^ n) (k : ℕ) → fst (lookup a γ) ≡ # k → ⟨ γ ⊨ ApproxAt f a ⟩ → (j : ℕ) → j < k → ((u : S) → ⟨ pr (# j) (fst u) ∈ fst (lookup f γ) ⟩ → fst u ≡ fst (relAt j)) → ⟨ pr (# j) (fst (relAt j)) ∈ fst (lookup f γ) ⟩ entryOf f a γ k qa h j hj vs = PT.rec (snd (pr (# j) (fst (relAt j)) ∈ fst (lookup f γ))) named (ApproxAt-value f a γ h (numS j) (subst (λ t → ⟨ fst (numS j) ∈ t ⟩) (sym qa) (subst (λ t → ⟨ t ∈ # k ⟩) (sym (numS-fst j)) (#mono j k hj)))) where named : Σ[ u ∈ S ] ⟨ pr (fst (numS j)) (fst u) ∈ fst (lookup f γ) ⟩ → ⟨ pr (# j) (fst (relAt j)) ∈ fst (lookup f γ) ⟩ named (u , p) = subst (λ t → ⟨ pr (# j) t ∈ fst (lookup f γ) ⟩) (vs u p') p' where p' : ⟨ pr (# j) (fst u) ∈ fst (lookup f γ) ⟩ p' = subst (λ t → ⟨ pr t (fst u) ∈ fst (lookup f γ) ⟩) (numS-fst j) p module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) (k : ℕ) (qa : fst (lookup a γ) ≡ # k) (h : ⟨ γ ⊨ ApproxAt f a ⟩) where private Val : ℕ → Type (ℓ-suc ℓ) Val m = (m < k) → (w : S) → ⟨ pr (# m) (fst w) ∈ fst (lookup f γ) ⟩ → fst w ≡ fst (relAt m) approx-val : (m : ℕ) → Val m approx-val = WFI.induction <-wellfounded go where go : (m : ℕ) → ((j : ℕ) → j < m → Val j) → Val m go m IH hm w hw = step-rel zero (suc zero) (sh2 f) (w ∷ numS m ∷ γ) m (numS-fst m) vals ents (ApproxAt-step f a γ h (numS m) w (subst (λ t → ⟨ pr t (fst w) ∈ fst (lookup f γ) ⟩) (sym (numS-fst m)) hw)) where vals : Values (lookup (sh2 f) (w ∷ numS m ∷ γ)) m vals j hj u hu = IH j hj (<-trans hj hm) u hu ents : Entries (lookup (sh2 f) (w ∷ numS m ∷ γ)) m ents j hj = entryOf f a γ k qa h j (<-trans hj hm) (λ u p → IH j hj (<-trans hj hm) u p) approx-ent : (m : ℕ) → m < k → ⟨ pr (# m) (fst (relAt m)) ∈ fst (lookup f γ) ⟩ approx-ent m hm = entryOf f a γ k qa h m hm (approx-val m hm) module _ {n : ℕ} (v b : Fin n) (γ : S ^ n) (k : ℕ) (qb : fst (lookup b γ) ≡ # k) where rel-only : ⟨ γ ⊨ RelGraphAt v b ⟩ → fst (lookup v γ) ≡ fst (relAt k) rel-only h = PT.rec (setIsSet (fst (lookup v γ)) (fst (relAt k))) read (RelGraph-out v b γ h) where read : GraphOf v b γ → fst (lookup v γ) ≡ fst (relAt k) read (g , (ha , hs)) = step-rel (suc v) (suc b) zero (g ∷ γ) k qb (λ m hm w hw → approx-val zero (suc b) (g ∷ γ) k qb ha m hm w hw) (λ m hm → approx-ent zero (suc b) (g ∷ γ) k qb ha m hm) hs
那个逼近，当场拿出来
图说仅仅存在一个逼近；消费方得拿出一个来。在数码 k 处，所要的逼近是有穷的，即 k 以下的诸数码与那里的关系所成的诸对，故它由 L 元素的一个有穷族张成，而基本那一章的 finSetL 只要那些成员共处一个阶段，就把这样的族变成模型的一个集合。smallStage 是把序数留在明面上的那条界层引理，也就是递归那一章的 smallDom 多出一个投影。
此处不花任何公式，而这正是本章的索引所买来的那笔省钱：逼近之所以有穷，是因为索引是数码，故它既不需要替换，也不需要自己的图。approxSet-approx 随后对着那个族核对「是一个逼近」的两个合取项，而 relAt-graph 是 rel-only 的逆：这场递归在某个数码处的取值满足那里的图。
smallStage : (X : Type ℓ) (g : X → S) → Σ[ σ ∈ V ℓ ] (IsOrd σ × ((x : X) → ⟨ fst (g x) ∈ Lset σ ⟩)) smallStage X g = bd .fst , (bd .snd .fst , mem) where bd = boundingOrd X (λ x → stage (fst (g x)) (g x .snd)) (λ x → stage-ord (fst (g x)) (g x .snd)) mem : (x : X) → ⟨ fst (g x) ∈ Lset (bd .fst) ⟩ mem x = Lset-mono {α = bd .fst} {β = stage (fst (g x)) (g x .snd)} (bd .snd .snd x) (stage-mem (fst (g x)) (g x .snd)) private famOf : (k : ℕ) → Fin k → S famOf k i = prS (numS (toℕ i)) (relAt (toℕ i)) famBnd : (k : ℕ) → Σ[ σ ∈ V ℓ ] (IsOrd σ × ((i : Lift {ℓ-zero} {ℓ} (Fin k)) → ⟨ fst (famOf k (lower i)) ∈ Lset σ ⟩)) famBnd k = smallStage (Lift {ℓ-zero} {ℓ} (Fin k)) (λ i → famOf k (lower i)) famEq : (k : ℕ) (i : Fin k) → fst (famOf k i) ≡ pr (# (toℕ i)) (fst (relAt (toℕ i))) famEq k i = prS-fst (numS (toℕ i)) (relAt (toℕ i)) ∙ cong (λ t → pr t (fst (relAt (toℕ i)))) (numS-fst (toℕ i)) opaque approxSet : ℕ → S approxSet k = finSet k (λ i → fst (famOf k i)) , FinOf.finSetL (famBnd k .fst) (famBnd k .snd .fst) k (λ i → fst (famOf k i)) (λ i → famBnd k .snd .snd (lift i)) approxSet-fst : (k : ℕ) → fst (approxSet k) ≡ finSet k (λ i → fst (famOf k i)) approxSet-fst k = refl approx-mem-in : (k j : ℕ) → j < k → ⟨ pr (# j) (fst (relAt j)) ∈ fst (approxSet k) ⟩ approx-mem-in k j hj = subst (λ t → ⟨ t ∈ fst (approxSet k) ⟩) (cong (λ i → pr (# i) (fst (relAt i))) (toℕ∘enum j hj)) (subst (λ t → ⟨ pr (# (toℕ (enum j hj))) (fst (relAt (toℕ (enum j hj)))) ∈ t ⟩) (sym (approxSet-fst k)) (finSet-in k (λ i → fst (famOf k i)) (pr (# (toℕ (enum j hj))) (fst (relAt (toℕ (enum j hj))))) ∣ enum j hj , famEq k (enum j hj) ∣₁)) approx-mem-out : (k : ℕ) (y : V ℓ) → ⟨ y ∈ fst (approxSet k) ⟩ → ∥ Σ[ j ∈ ℕ ] ((j < k) × (y ≡ pr (# j) (fst (relAt j)))) ∥₁ approx-mem-out k y h = PT.map named (finSet-out k (λ i → fst (famOf k i)) y (subst (λ t → ⟨ y ∈ t ⟩) (approxSet-fst k) h)) where named : Σ[ i ∈ Fin k ] (fst (famOf k i) ≡ y) → Σ[ j ∈ ℕ ] ((j < k) × (y ≡ pr (# j) (fst (relAt j)))) named (i , q) = toℕ i , (toℕ<n i , (sym q ∙ famEq k i)) approxVals : (k : ℕ) → Values (approxSet k) k approxVals k m hm u hu = PT.rec (setIsSet (fst u) (fst (relAt m))) named (approx-mem-out k (pr (# m) (fst u)) hu) where named : Σ[ j ∈ ℕ ] ((j < k) × (pr (# m) (fst u) ≡ pr (# j) (fst (relAt j)))) → fst u ≡ fst (relAt m) named (j , (hj , q)) = pr-inj q .snd ∙ cong (λ i → fst (relAt i)) (sym (#-inj′ (pr-inj q .fst))) approxEnts : (k : ℕ) → Entries (approxSet k) k approxEnts k m hm = approx-mem-in k m hm module _ (k : ℕ) {n : ℕ} (f a : Fin n) (γ : S ^ n) (qf : fst (lookup f γ) ≡ fst (approxSet k)) (qa : fst (lookup a γ) ≡ # k) where private onDom : (x : S) → (⟨ ⋁ S (λ y → pr (fst x) (fst y) ∈ fst (lookup f γ)) ⟩ → ⟨ fst x ∈ fst (lookup a γ) ⟩) × (⟨ fst x ∈ fst (lookup a γ) ⟩ → ⟨ ⋁ S (λ y → pr (fst x) (fst y) ∈ fst (lookup f γ)) ⟩) onDom x = fwd , bwd where fwd : ⟨ ⋁ S (λ y → pr (fst x) (fst y) ∈ fst (lookup f γ)) ⟩ → ⟨ fst x ∈ fst (lookup a γ) ⟩ fwd = PT.rec (snd (fst x ∈ fst (lookup a γ))) atY where atY : Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ fst x ∈ fst (lookup a γ) ⟩ atY (y , p) = PT.rec (snd (fst x ∈ fst (lookup a γ))) named (approx-mem-out k (pr (fst x) (fst y)) (subst (λ t → ⟨ pr (fst x) (fst y) ∈ t ⟩) qf p)) where named : Σ[ j ∈ ℕ ] ((j < k) × (pr (fst x) (fst y) ≡ pr (# j) (fst (relAt j)))) → ⟨ fst x ∈ fst (lookup a γ) ⟩ named (j , (hj , q)) = subst (λ t → ⟨ fst x ∈ t ⟩) (sym qa) (subst (λ t → ⟨ t ∈ # k ⟩) (sym (pr-inj q .fst)) (#mono j k hj)) bwd : ⟨ fst x ∈ fst (lookup a γ) ⟩ → ⟨ ⋁ S (λ y → pr (fst x) (fst y) ∈ fst (lookup f γ)) ⟩ bwd hx = PT.map named (∈#-elim k (fst x) (subst (λ t → ⟨ fst x ∈ t ⟩) qa hx)) where named : Σ[ j ∈ ℕ ] ((j < k) × (fst x ≡ # j)) → Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ named (j , (hj , q)) = relAt j , subst (λ t → ⟨ pr (fst x) (fst (relAt j)) ∈ t ⟩) (sym qf) (subst (λ t → ⟨ pr t (fst (relAt j)) ∈ fst (approxSet k) ⟩) (sym q) (approx-mem-in k j hj)) onStep : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ (y ∷ x ∷ γ) ⊨ RelStepAt zero (suc zero) (sh2 f) ⟩ onStep x y p = PT.rec (snd ((y ∷ x ∷ γ) ⊨ RelStepAt zero (suc zero) (sh2 f))) named (approx-mem-out k (pr (fst x) (fst y)) (subst (λ t → ⟨ pr (fst x) (fst y) ∈ t ⟩) qf p)) where named : Σ[ j ∈ ℕ ] ((j < k) × (pr (fst x) (fst y) ≡ pr (# j) (fst (relAt j)))) → ⟨ (y ∷ x ∷ γ) ⊨ RelStepAt zero (suc zero) (sh2 f) ⟩ named (j , (hj , q)) = rel-step zero (suc zero) (sh2 f) (y ∷ x ∷ γ) j (pr-inj q .fst) (λ i hi u hu → approxVals k i (<-trans hi hj) u (subst (λ t → ⟨ pr (# i) (fst u) ∈ t ⟩) qf hu)) (λ i hi → subst (λ t → ⟨ pr (# i) (fst (relAt i)) ∈ t ⟩) (sym qf) (approxEnts k i (<-trans hi hj))) (pr-inj q .snd) approxSet-approx : ⟨ γ ⊨ ApproxAt f a ⟩ approxSet-approx = ApproxAt-in f a γ (domAt-intro f a γ onDom) onStep relAt-graph : ∀ {n} (v b : Fin n) (γ : S ^ n) (k : ℕ) → fst (lookup b γ) ≡ # k → fst (lookup v γ) ≡ fst (relAt k) → ⟨ γ ⊨ RelGraphAt v b ⟩ relAt-graph v b γ k qb qv = RelGraph-in v b γ (approxSet k) (approxSet-approx k zero (suc b) (approxSet k ∷ γ) refl qb) (rel-step (suc v) (suc b) zero (approxSet k ∷ γ) k qb (approxVals k) (approxEnts k) qv)
那一族，作为 L 的一个元素
沿 ωʟ 作替换，以成对的那个图为定义公式，整个构造仅此而已。在 ωʟ 的某个成员处的函数性，就是 mereFunct 施于它仅仅所是的那个数码：取值由 relAt-graph 当场拿出，而别的东西都不满足那个图，这由 rel-only 保证。
那个框架把成对的图取作携带自己等式的变元，在唯一的调用处填 refl；而它交回来的是一个三元组，其中根本不出现任何公式：那一族，以及它对着这场递归的两个隶属方向。最后这一点是承重的。若把那一族的规格陈述成对着那个闭句子，其下的每个消费方都得去判定「那个句子的满足关系」与「它展开式的满足关系」相等，而本章就跑不完。陈述成对着这场递归，就没有什么可判定的了。
opaque PairRelGraphAt : ∀ {n} → Fin n → Fin n → Formula S n PairRelGraphAt e c = ∃̇ (prAtL (suc e) (suc c) zero ∧̇ RelGraphAt zero (suc c)) module _ {n : ℕ} (e c : Fin n) (γ : S ^ n) (φ : Formula S n) (qφ : φ ≡ PairRelGraphAt e c) where PairOf : Type (ℓ-suc ℓ) PairOf = Σ[ z ∈ S ] ( (fst (lookup e γ) ≡ pr (fst (lookup c γ)) (fst z)) × ⟨ (z ∷ γ) ⊨ RelGraphAt zero (suc c) ⟩ ) opaque unfolding PairRelGraphAt PairRelGraph-in : (z : S) → fst (lookup e γ) ≡ pr (fst (lookup c γ)) (fst z) → ⟨ (z ∷ γ) ⊨ RelGraphAt zero (suc c) ⟩ → ⟨ γ ⊨ φ ⟩ PairRelGraph-in z q hg = subst (λ ψ → ⟨ γ ⊨ ψ ⟩) (sym qφ) ∣ z , ( subst ⟨_⟩ (sym (prAtL-adequate (suc e) (suc c) zero (z ∷ γ))) q , hg ) ∣₁ PairRelGraph-out : ⟨ γ ⊨ φ ⟩ → ∥ PairOf ∥₁ PairRelGraph-out h = PT.map readPair (subst (λ ψ → ⟨ γ ⊨ ψ ⟩) qφ h) where readPair : Σ[ z ∈ S ] ⟨ (z ∷ γ) ⊨ (prAtL (suc e) (suc c) zero ∧̇ RelGraphAt zero (suc c)) ⟩ → PairOf readPair (z , (hq , hg)) = z , (subst ⟨_⟩ (prAtL-adequate (suc e) (suc c) zero (z ∷ γ)) hq , hg) private -- perf: the pair graph enters as a variable carrying its own equation, and -- nothing the frame hands back mentions a formula at all; with the closed -- sentence spelled out in the family's specification the chapter does not -- close (past 400 s) famBuild : (φ : Formula S 2) → φ ≡ PairRelGraphAt zero (suc zero) → Σ[ h ∈ S ] ( ((k : ℕ) → ⟨ pr (# k) (fst (relAt k)) ∈ fst h ⟩) × ((cS rS : S) (k : ℕ) → fst cS ≡ # k → ⟨ pr (fst cS) (fst rS) ∈ fst h ⟩ → fst rS ≡ fst (relAt k)) ) famBuild φ qφ = r .fst .fst , (inFam , outFam) where fc : (c : S) → ⟨ c ∈ˢ ωʟ ⟩ → isContr (Σ[ y ∈ S ] ⟨ (y ∷ c ∷ []) ⊨ φ ⟩) fc c c∈ = mereFunct φ c (PT.map atK c∈) where atK : Σ[ j ∈ Lift ℕ ] (# (lower j) ≡ fst c) → Σ[ y ∈ S ] ( ⟨ (y ∷ c ∷ []) ⊨ φ ⟩ × ((y' : S) → ⟨ (y' ∷ c ∷ []) ⊨ φ ⟩ → y' ≡ y) ) atK (j , qj) = prS c (relAt (lower j)) , (holds , only) where qc : fst c ≡ # (lower j) qc = sym qj holds : ⟨ (prS c (relAt (lower j)) ∷ c ∷ []) ⊨ φ ⟩ holds = PairRelGraph-in zero (suc zero) (prS c (relAt (lower j)) ∷ c ∷ []) φ qφ (relAt (lower j)) (prS-fst c (relAt (lower j))) (relAt-graph zero (sh2 zero) (relAt (lower j) ∷ prS c (relAt (lower j)) ∷ c ∷ []) (lower j) qc refl) only : (y' : S) → ⟨ (y' ∷ c ∷ []) ⊨ φ ⟩ → y' ≡ prS c (relAt (lower j)) only y' h = PT.rec (isSetS y' (prS c (relAt (lower j)))) read (PairRelGraph-out zero (suc zero) (y' ∷ c ∷ []) φ qφ h) where read : PairOf zero (suc zero) (y' ∷ c ∷ []) φ qφ → y' ≡ prS c (relAt (lower j)) read (z , (q , hg)) = Σ≡Prop (λ t → snd (isL t)) ( q ∙ cong (pr (fst c)) (rel-only zero (sh2 zero) (z ∷ y' ∷ c ∷ []) (lower j) qc hg) ∙ sym (prS-fst c (relAt (lower j))) ) r : isContr (SetOf (λ y → ⋁ S (λ c → (c ∈ˢ ωʟ) ⊓ ((y ∷ c ∷ []) ⊨ φ)))) r = hasReplacementL ωʟ φ fc inFam : (k : ℕ) → ⟨ pr (# k) (fst (relAt k)) ∈ fst (r .fst .fst) ⟩ inFam k = subst (λ t → ⟨ t ∈ fst (r .fst .fst) ⟩) qe (subst ⟨_⟩ (sym (r .fst .snd (prS (numS k) (relAt k)))) ∣ numS k , (inω , holds) ∣₁) where qe : fst (prS (numS k) (relAt k)) ≡ pr (# k) (fst (relAt k)) qe = prS-fst (numS k) (relAt k) ∙ cong (λ t → pr t (fst (relAt k))) (numS-fst k) inω : ⟨ numS k ∈ˢ ωʟ ⟩ inω = subst (λ t → ⟨ t ∈ ω ⟩) (sym (numS-fst k)) (#∈ω k) holds : ⟨ (prS (numS k) (relAt k) ∷ numS k ∷ []) ⊨ φ ⟩ holds = PairRelGraph-in zero (suc zero) (prS (numS k) (relAt k) ∷ numS k ∷ []) φ qφ (relAt k) (prS-fst (numS k) (relAt k)) (relAt-graph zero (sh2 zero) (relAt k ∷ prS (numS k) (relAt k) ∷ numS k ∷ []) k (numS-fst k) refl) outFam : (cS rS : S) (k : ℕ) → fst cS ≡ # k → ⟨ pr (fst cS) (fst rS) ∈ fst (r .fst .fst) ⟩ → fst rS ≡ fst (relAt k) outFam cS rS k qc h = PT.rec (setIsSet (fst rS) (fst (relAt k))) atD (subst ⟨_⟩ (r .fst .snd (prS cS rS)) (subst (λ t → ⟨ t ∈ fst (r .fst .fst) ⟩) (sym (prS-fst cS rS)) h)) where atD : Σ[ d ∈ S ] ( ⟨ d ∈ˢ ωʟ ⟩ × ⟨ (prS cS rS ∷ d ∷ []) ⊨ φ ⟩ ) → fst rS ≡ fst (relAt k) atD (d , (d∈ , hp)) = PT.rec (setIsSet (fst rS) (fst (relAt k))) read (PairRelGraph-out zero (suc zero) (prS cS rS ∷ d ∷ []) φ qφ hp) where read : PairOf zero (suc zero) (prS cS rS ∷ d ∷ []) φ qφ → fst rS ≡ fst (relAt k) read (z , (q , hg)) = pr-inj q' .snd ∙ rel-only zero (sh2 zero) (z ∷ prS cS rS ∷ d ∷ []) k qd hg where q' : pr (fst cS) (fst rS) ≡ pr (fst d) (fst z) q' = sym (prS-fst cS rS) ∙ q qd : fst d ≡ # k qd = sym (pr-inj q' .fst) ∙ qc opaque beforeFam : S beforeFam = famBuild (PairRelGraphAt zero (suc zero)) refl .fst beforeFam-in : (k : ℕ) → ⟨ pr (# k) (fst (relAt k)) ∈ fst beforeFam ⟩ beforeFam-in = famBuild (PairRelGraphAt zero (suc zero)) refl .snd .fst beforeFam-out : (cS rS : S) (k : ℕ) → fst cS ≡ # k → ⟨ pr (fst cS) (fst rS) ∈ fst beforeFam ⟩ → fst rS ≡ fst (relAt k) beforeFam-out = famBuild (PairRelGraphAt zero (suc zero)) refl .snd .snd
某个槽位所持数码处的那个序
这就是上一章所索取的那条公式，而它就是那个步进体，只改了两处。逼近那一位没了，因为那一族如今是个集合、可以被点名：appAtC 是在常元处的应用，一个有界存在量词加一次对读式，而模型那一章为槽位版所证的适足性，在此处为常元版证一遍。以及，被比较的那两个集合不被禁闭在任何阶段里，因为那个框架索取的是在模型任意成员处的双条件，而最先分歧处的比较本来也不需要它们被禁闭：只有那个见证与它以下的诸点在一个阶段上取值。
于是只剩四层绑定：前趋、那一族在那里所持有的关系、那里的阶段，此外再无其他。BeforeAt-out 与 BeforeAt-in 是两条读式，二者都站在变元环境的变元位上，而那个数码以携带自己定义等式的变元身份到场，那正是一章之前层号所据以实测的那条定律。
private sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n))) sh3 i = suc (suc (suc i)) appAtC : ∀ {n} → S → Fin n → Fin n → Formula S n appAtC F x y = ∃̇∈ (con F) (prAtL zero (suc x) (suc y)) appAtC-adequate : ∀ {n} (F : S) (x y : Fin n) (γ : S ^ n) → (γ ⊨ appAtC F x y) ≡ (pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst F) appAtC-adequate F x y γ = ⇔toPath fwd bwd where fwd : ⟨ γ ⊨ appAtC F x y ⟩ → ⟨ pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst F ⟩ fwd = PT.rec (snd (pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst F)) read where read : Σ[ z ∈ S ] ( ⟨ z ∈ˢ F ⟩ × ⟨ (z ∷ γ) ⊨ prAtL zero (suc x) (suc y) ⟩ ) → ⟨ pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst F ⟩ read (z , (z∈ , h)) = subst (λ t → ⟨ t ∈ fst F ⟩) (subst ⟨_⟩ (prAtL-adequate zero (suc x) (suc y) (z ∷ γ)) h) z∈ bwd : ⟨ pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst F ⟩ → ⟨ γ ⊨ appAtC F x y ⟩ bwd hp = ∣ memS F (pr (fst (lookup x γ)) (fst (lookup y γ))) hp , ( subst (λ t → ⟨ t ∈ fst F ⟩) (sym (memS-fst F (pr (fst (lookup x γ)) (fst (lookup y γ))) hp)) hp , subst ⟨_⟩ (sym (prAtL-adequate zero (suc x) (suc y) (memS F (pr (fst (lookup x γ)) (fst (lookup y γ))) hp ∷ γ))) (memS-fst F (pr (fst (lookup x γ)) (fst (lookup y γ))) hp) ) ∣₁ opaque BeforeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n BeforeAt b x y = ∃̇ ( (var zero ∈̇ var (suc b)) ∧̇ ( ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ∧̇ ∃̇ ( appAtC beforeFam (suc zero) zero ∧̇ ∃̇ ( LsetGraphAt zero (suc (suc zero)) ∧̇ PrecedesAt (suc zero) zero (sh3 x) (sh3 y) ) ) ) ) module _ {n : ℕ} (b x y : Fin n) (γ : S ^ n) (m : ℕ) (qb : fst (lookup b γ) ≡ # m) where private Inner : (c r A : S) → Type (ℓ-suc ℓ) Inner c r A = ⟨ (A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩ × ⟨ (A ∷ r ∷ c ∷ γ) ⊨ PrecedesAt (suc zero) zero (sh3 x) (sh3 y) ⟩ AtR : (c : S) → Type (ℓ-suc ℓ) AtR c = Σ[ r ∈ S ] ( ⟨ (r ∷ c ∷ γ) ⊨ appAtC beforeFam (suc zero) zero ⟩ × ∥ (Σ[ A ∈ S ] Inner c r A) ∥₁ ) AtC : Type (ℓ-suc ℓ) AtC = Σ[ c ∈ S ] ( ⟨ fst c ∈ fst (lookup b γ) ⟩ × ( ⟨ (c ∷ γ) ⊨ ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ⟩ × ∥ AtR c ∥₁ ) ) Goal : Type (ℓ-suc ℓ) Goal = ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩ atA : (c r A : S) (j : ℕ) → fst c ≡ # j → m ≡ suc j → ⟨ pr (fst c) (fst r) ∈ fst beforeFam ⟩ → Inner c r A → Goal atA c r A j qc qm hf (hg , hprec) = subst (λ i → ⟨ before i (fst (lookup x γ)) (fst (lookup y γ)) ⟩) (sym qm) (precedes-map (Rel j) (before j) (finiteStage j) (fst (lookup x γ)) (fst (lookup y γ)) (λ w t hw ht hbf → relAt-fill j w t hw ht hbf) atJ) where Rrep : (s t : S) → ⟨ pr (fst s) (fst t) ∈ fst (lookup (suc zero) (A ∷ r ∷ c ∷ γ)) ⟩ → ⟨ Held r (fst s) (fst t) ⟩ Rrep s t p = p Rfill : (s t : S) → ⟨ Held r (fst s) (fst t) ⟩ → ⟨ pr (fst s) (fst t) ∈ fst (lookup (suc zero) (A ∷ r ∷ c ∷ γ)) ⟩ Rfill s t p = p module P = Precedes (suc zero) zero (sh3 x) (sh3 y) (A ∷ r ∷ c ∷ γ) (Held r) Rrep Rfill qA : fst A ≡ finiteStage j qA = Lset-only zero (suc (suc zero)) (A ∷ r ∷ c ∷ γ) hg (subst IsOrd (sym qc) (numeral-ord j)) ∙ cong Lset qc atJ : ⟨ precedes (Rel j) (finiteStage j) (fst (lookup x γ)) (fst (lookup y γ)) ⟩ atJ = subst (λ t → ⟨ precedes (λ s u → pr s u ∈ t) (finiteStage j) (fst (lookup x γ)) (fst (lookup y γ)) ⟩) (beforeFam-out c r j qc hf) (subst (λ t → ⟨ precedes (Held r) t (fst (lookup x γ)) (fst (lookup y γ)) ⟩) qA (P.PrecedesAt-out hprec)) atR : (c : S) (j : ℕ) → fst c ≡ # j → m ≡ suc j → AtR c → Goal atR c j qc qm (r , (happ , hA)) = PT.rec (snd (before m (fst (lookup x γ)) (fst (lookup y γ)))) (λ { (A , hi) → atA c r A j qc qm hf hi }) hA where hf : ⟨ pr (fst c) (fst r) ∈ fst beforeFam ⟩ hf = subst ⟨_⟩ (appAtC-adequate beforeFam (suc zero) zero (r ∷ c ∷ γ)) happ atC : AtC → Goal atC (c , (c∈ , (hmax , hr))) = PT.rec (snd (before m (fst (lookup x γ)) (fst (lookup y γ)))) named (∈#-elim m (fst c) (subst (λ t → ⟨ fst c ∈ t ⟩) qb c∈)) where named : Σ[ j ∈ ℕ ] ((j < m) × (fst c ≡ # j)) → Goal named (j , (hj , qc)) = PT.rec (snd (before m (fst (lookup x γ)) (fst (lookup y γ)))) (atR c j qc qm) hr where qm : m ≡ suc j qm = decide (suc j ≟ m) where decide : NatOrder.Trichotomy (suc j) m → m ≡ suc j decide (NatOrder.lt hlt) = Empty.rec (hmax (numS (suc j)) (subst (λ t → ⟨ fst (numS (suc j)) ∈ t ⟩) (sym qb) (subst (λ t → ⟨ t ∈ # m ⟩) (sym (numS-fst (suc j))) (#mono (suc j) m hlt))) (subst (λ t → ⟨ fst c ∈ t ⟩) (sym (numS-fst (suc j))) (subst (λ t → ⟨ t ∈ # (suc j) ⟩) (sym qc) (#mono j (suc j) NatOrder.≤-refl)))) decide (NatOrder.eq e) = sym e decide (NatOrder.gt hgt) = Empty.rec (<-asym hj (pred-≤-pred hgt)) opaque unfolding BeforeAt BeforeAt-out : ⟨ γ ⊨ BeforeAt b x y ⟩ → ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩ BeforeAt-out h = PT.rec (snd (before m (fst (lookup x γ)) (fst (lookup y γ)))) atC h BeforeAt-in : ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩ → ⟨ γ ⊨ BeforeAt b x y ⟩ BeforeAt-in h = ∣ numS j , (c∈ , (hmax , ∣ relAt j , (happ , ∣ stageS j , (hg , hprec) ∣₁) ∣₁)) ∣₁ where j : ℕ j = before-suc m (fst (lookup x γ)) (fst (lookup y γ)) h .fst qm : m ≡ suc j qm = before-suc m (fst (lookup x γ)) (fst (lookup y γ)) h .snd hj : j < m hj = subst (λ i → j < i) (sym qm) NatOrder.≤-refl c∈ : ⟨ fst (numS j) ∈ fst (lookup b γ) ⟩ c∈ = subst (λ t → ⟨ fst (numS j) ∈ t ⟩) (sym qb) (subst (λ t → ⟨ t ∈ # m ⟩) (sym (numS-fst j)) (#mono j m hj)) hmax : ⟨ (numS j ∷ γ) ⊨ ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ⟩ hmax d hd hc = PT.rec Empty.isProp⊥ step (∈#-elim m (fst d) (subst (λ t → ⟨ fst d ∈ t ⟩) qb hd)) where step : Σ[ i ∈ ℕ ] ((i < m) × (fst d ≡ # i)) → Empty.⊥ step (i , (hi , qd)) = <-asym ji (pred-≤-pred (subst (λ t → i < t) qm hi)) where ji : j < i ji = #∈#-elim j i (subst (λ t → ⟨ t ∈ # i ⟩) (numS-fst j) (subst (λ t → ⟨ fst (numS j) ∈ t ⟩) qd hc)) happ : ⟨ (relAt j ∷ numS j ∷ γ) ⊨ appAtC beforeFam (suc zero) zero ⟩ happ = subst ⟨_⟩ (sym (appAtC-adequate beforeFam (suc zero) zero (relAt j ∷ numS j ∷ γ))) (subst (λ t → ⟨ pr t (fst (relAt j)) ∈ fst beforeFam ⟩) (sym (numS-fst j)) (beforeFam-in j)) hg : ⟨ (stageS j ∷ relAt j ∷ numS j ∷ γ) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩ hg = Lset-defines zero (suc (suc zero)) (stageS j ∷ relAt j ∷ numS j ∷ γ) (subst IsOrd (sym (numS-fst j)) (numeral-ord j)) (stageS-fst j ∙ cong Lset (sym (numS-fst j))) Rrep : (s t : S) → ⟨ pr (fst s) (fst t) ∈ fst (lookup (suc zero) (stageS j ∷ relAt j ∷ numS j ∷ γ)) ⟩ → ⟨ Held (relAt j) (fst s) (fst t) ⟩ Rrep s t p = p Rfill : (s t : S) → ⟨ Held (relAt j) (fst s) (fst t) ⟩ → ⟨ pr (fst s) (fst t) ∈ fst (lookup (suc zero) (stageS j ∷ relAt j ∷ numS j ∷ γ)) ⟩ Rfill s t p = p module P = Precedes (suc zero) zero (sh3 x) (sh3 y) (stageS j ∷ relAt j ∷ numS j ∷ γ) (Held (relAt j)) Rrep Rfill hprec : ⟨ (stageS j ∷ relAt j ∷ numS j ∷ γ) ⊨ PrecedesAt (suc zero) zero (sh3 x) (sh3 y) ⟩ hprec = P.PrecedesAt-in (subst (λ t → ⟨ precedes (Rel j) t (fst (lookup x γ)) (fst (lookup y γ)) ⟩) (sym (stageS-fst j)) (precedes-map (before j) (Rel j) (finiteStage j) (fst (lookup x γ)) (fst (lookup y γ)) (λ w t hw ht hR → relAt-rep j w t hw ht hR) (subst (λ i → ⟨ before i (fst (lookup x γ)) (fst (lookup y γ)) ⟩) qm h)))
那个框架，兑现
一行，而这就是整章为之而写的东西。有了 BeforeAt 与它的两条读式，上一章的 Described 便不再是一个框架：LimitOrdAt、它的两条读式、codeOrder、codeOrder-fill、codeOrder-rep 与 CodeKeys 在此处无条件可用，而本部中一切以「给定最先分歧之序的那一族」为前提的陈述，如今都是径直的陈述。
这兑现了什么、没兑现什么，值得说准。内化那一章的键之束取两个关系位，一个为诸码、一个为诸参数。为诸码所设的那一位如今被径直填上，故 L.Choice.Adequate 的步进适足性只还差为诸参数所设的那一位，即「命名所依托的那个载体上的序」，连同它的两个隶属方向。那个序正是 L.Choice.Table 在每个阶段处产出的东西，而它产在那场递归内部，而 L.Choice.Faithful 的 Stp 参数自身正在给那场递归供料。故 Faithful 的那个参数并未由本章兑现，而理由是结构性的、不是数学缺口：某个阶段处的步进条件要的是该阶段处已内化的序，而表只有在它自己的归纳内部才拥有它。把它闭合，是「步进适足性在何处供给」的一次重新裁切，而不是另一个构造；它是这条链上仅剩的那一件事。
open Described BeforeAt BeforeAt-in BeforeAt-out public
小结
relAt 是每个数码处最先分歧之序的那个关系，作为 L 的一个元素：在那个有穷阶段的诸对之上作一次分离，用上一章那条步进描述来雕，而那条描述的两个槽位被绑定、并用对象等词钉在诸常元上，于是一条描述同时服务于此处的分离与其下的那个图。relAt-out 与 relAt-in 是它的两条读式，对数码作归纳一并证出，每个方向都在前趋处花掉另一个，因为上一个关系只在一致性子句内部被查阅；precedes-map 就是在基底关系的两种写法之间搬运一次比较的那一行，而它是反变的。
RelBodyAt 是那一步，对成员、索引与逼近保持通用。前趋的说法不用对象等词：它是索引的 ∈-极大成员，两个原子；而在零处没有这样的成员，这使那一步恰好在这场递归为空之处为空。RelStepAt、ApproxAt 与 RelGraphAt 照模板而来，不带单值性合取项，而 step-rel 与 rel-step 是通往元语言的那座桥，两者合计用了四次。
approx-val 把逼近所记录的每个取值钉住，靠的是在数码上的一次良基归纳，任何地方都没有单值性假设，而 rel-only 是那个图的确定性。approxSet 是当场拿出来的那个逼近，而它根本不花任何公式：某个数码以下的逼近是有穷的，故只要 smallStage 把它的诸成员放进同一个阶段，finSetL 就把它张出来。beforeFam 是那一族本身，沿 ωʟ 的一次替换，在造出之处封印，而它的两个方向陈述成对着这场递归、而不对着任何公式。
BeforeAt 就是上一章所索取的东西：那一族在某个槽位所持数码处被读出，其中在常元处的应用用 appAtC，而被比较的那两个集合不加禁闭，因为那次比较本来就不需要它们被禁闭。有了它的两条读式，Described 便被实例化，而 codeOrder 连同 CodeKeys 成为无条件的。
一次实测，而它是本部记下的最大的一次。这场递归的四条描述必须在造出之处封印：不封印时，每一次在具体环境上的满足关系都要把一条内部装着两份完整层级描述的公式正规化，本章要花 376 秒；封印之后是 3.8 秒，九十九倍，而数学分毫未动。造出那一族的那个框架在高一层遵守同一条定律：它交回来的三元组中根本不出现任何公式。