The earliest-disagreement family, internalized

The previous chapter left one hypothesis open, and named it exactly: a formula saying that the earliest-disagreement order at the numeral held in one slot puts a second slot before a third, together with its two readings against the finite chapter's before. Everything else in the limit order is already unconditional. This chapter discharges that hypothesis, and with it the chapter before it.

What has to be built is a recursion along the numerals whose values are relations: at zero the empty relation, and at the numeral after n the comparison at the earliest disagreement over the stage at n, with the relation at n as its base. A recursion whose values are sets cannot be named by a term, so what gets described is an approximation, exactly as the tower and the order table were described: an approximation predicate, a graph quantifying over approximations, a value lemma pinning every value an approximation records, and the object itself sealed where it is built.

Two things make this cheaper than the tower was. The index is a member of

ωʟ, which is a set, so the outer induction is on a natural number and the class-collection half of the hierarchy chapter does not arise; and the step is already written, since the previous chapter's PrecedesAt holds the base relation and the base stage in slots precisely so it can stand where the relation is a recursion value. Two things make it dearer. The value at a numeral is a relation rather than a stage, so every step pays a separation over the pairs of a finite stage; and the previous relation reaches a slot inside the agreement clause, which is the shape that walls, so it arrives as a variable carrying its defining equation and never as an application.

{-# 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

Each stage's relation, as an element of L

The pairs the relation at a stage can relate cannot escape a single set: the members of a finite stage are a small family of elements of L and so are their pairs, and the recursion chapter's bounding lemma confines them all at once. The separation that carves the relation out of that bound is where the extra cost over the tower sits, and it is paid once per numeral.

The condition it carves with is the previous chapter's step description and nothing else. That description holds the base relation and the base stage in slots, and a separation is done with a formula of one free variable, so the two are bound by existentials and pinned to constants by the object equality. That is what lets the step description be used here exactly as it was delivered, with no second copy written against constants: one formula, two consumers.

relAt-out and relAt-in are the recursion's two readings, and they are proved together, by the ordinary induction on the numeral. Each direction spends the other at the predecessor, because the previous relation is consulted only inside the agreement clause, and precedes-map is the one line that carries it across: agreement is contravariant in the base relation, so passing from the recorded relation to before needs the reading in the opposite direction. relAt-rep and relAt-fill are the corollaries a consumer wants, at a pair rather than at a member.

-- 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 
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 
  s1 = suc zero
  s2 : Fin 
  s2 = sh2 zero
  s3 : Fin 
  s3 = sh2 (suc zero)
  s4 : Fin 
  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)))))

The step, generic in everything it consults

The body of the recursion's step is written once, with the member, the index and the approximation all in slots, and six binders under it: the predecessor of the index, the relation the approximation records there, the stage at the predecessor, the stage at the index, and the two sets being compared.

The predecessor is not a term of the object language and does not have to be. A numeral is a finite linear order under membership, so its predecessor is its ∈-maximal member, and that is two atoms: c belongs to the index, and no member of the index has c as a member. Written that way no object equality is needed anywhere, and at the numeral zero there is no such c, so the step is empty there, which is what the recursion wants.

The two stages are reached by the sequence chapter's graph, which is the only way to reach a stage, and the stage at the index is what confines the value: without it the extension would be a proper class, since the comparison at the earliest disagreement never mentions where the two compared sets live. StepOf writes the payload out rather than leaving it to inference, and both readings stand at variable slots in a variable environment with ordinality at the index as their only hypothesis.

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

The approximation and the graph

Off the template, and shorter than the template, because the domain machinery and the extension machinery are used exactly as delivered. RelStepAt is one

extAt over the body. ApproxAt is two conjuncts, the domain and the step condition, and there is deliberately no single-valuedness conjunct: the step condition already pins every value recorded at an argument, so single-valuedness is a corollary. RelGraphAt is one existential over the approximation with those two conjuncts under it.

All four descriptions are sealed where they are built, and this is the chapter's own measurement rather than an inherited habit. Unsealed, every satisfaction of the graph at a concrete environment normalizes a formula carrying two copies of the whole hierarchy description inside it, and the chapter takes 376 s; sealed, with each reading unfolding its own description and nothing else, it takes 3.8 s. That is a factor of ninety-nine, and no mathematics changed.

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

The step, against the recursion

The bridge, and both halves come out of the same two private lines. Given a correct and complete table below the index, the step at the index is exactly the relation the meta-language computes there: step-rel reads a satisfied step and gets the relation back, rel-step writes the step from the relation.

Both spend the predecessor analysis, and it is the only place trichotomy on the naturals is used in this chapter: a member of the index that is ∈-maximal in it is its predecessor, because a numeral strictly between would contradict maximality on one side and the membership on the other. Once the index is known to be a successor the rest is bookkeeping: the recorded relation there is the recursion's value by correctness, the stage there is the tower's value by the sequence chapter's graph, and precedes-map carries the comparison between the two spellings of the base relation.

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)