The hierarchy, inside

The previous chapter wrote the sentence; this chapter proves it says what it was meant to say. LsetGraphAt describes the tower by quantifying over approximations, and nothing so far connects it to Lset, the tower the book actually built. Three statements make that connection, and they are the chapter: a value the graph assigns is the meta tower's value there, the meta tower's value is one the graph assigns, and the collection of all of them below an ordinal is a single element of L.

The last of the three is the deliverable, and it is worth saying plainly what it is for. hierL is the internal hierarchy: the set of pairs of an ordinal with the tower's value at it, living inside the model rather than beside it. That set is what an internal definition of L is made of, and the internal well-order of L is read off it. To say "this set comes before that one" is to say at which stage each first appears, and a stage is speakable inside the model only once the tower is an object of the model. Nothing here defines the well-order; everything here is what the well-order will be defined from.

One shape repeats throughout. A table is a set of ordered pairs; it is correct on a set when every value it records below that set is the meta tower there, and complete when it records a value at every argument below. Correct and complete tables are exactly what the graph's step condition reads and what it can be written from, so one pair of lemmas serves the elimination and the introduction, and the rest of the chapter is those two lemmas applied at four places.

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; _∧̇_; ∃̇_ )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV )
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; 𝒟ₒ; Lset; Lset-in; Lset-out; IsOrd )
open import L.Ordinal {ℓ} using ( mem-ord )
open import L.Axioms.Basic {ℓ} using ( LsetS; isL-𝒟ₒ; extensionalL )
open import L.Axioms.Full {ℓ} lem using ( hasReplacementL )
open import L.Recursion {ℓ} lem using ( mereFunct )
open import L.Coding.Model {ℓ}
  using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; domAt-intro )
open import L.Coding.Sequence {ℓ} lem
  using ( StepAt; StepOf; PowOK; StepAt-in; StepAt-out; StepAt-back
        ; ApproxAt; ApproxAt-dom; ApproxAt-value; ApproxAt-step; ApproxAt-in
        ; LsetGraphAt; LsetGraph-in; LsetGraph-out; GraphOf )

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )

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)

What a table records

Three conditions, one line each, because each is one direction of one statement.

Values says a value recorded at an argument below B is the meta tower there. Entries says every argument below B has the meta tower recorded at it. Domain says nothing outside B is recorded at all.

They are kept apart rather than bundled, because the two consumers need different subsets of them. The induction over an approximation has the first two and cannot have the third: an approximation's entries lie below its own domain, not below whichever argument the induction currently stands at. The internal hierarchy has all three, because it is built as exactly the set of the right pairs. Bundled, the weaker consumer would be asked for a condition it cannot prove.

B is a plain set of the hierarchy here, not an element of the model. None of the three asks for constructibility; that enters with the ordinals, one section down.

Values : S → V ℓ → Type (ℓ-suc ℓ)
Values h B = (c z : S) → ⟨ fst c ∈ B ⟩
           → ⟨ pr (fst c) (fst z) ∈ fst h ⟩ → fst z ≡ Lset (fst c)

Entries : S → V ℓ → Type (ℓ-suc ℓ)
Entries h B = (c : S) → ⟨ fst c ∈ B ⟩ → ⟨ pr (fst c) (Lset (fst c)) ∈ fst h ⟩

Domain : S → V ℓ → Type (ℓ-suc ℓ)
Domain h B = (c z : S) → ⟨ pr (fst c) (fst z) ∈ fst h ⟩ → ⟨ fst c ∈ B ⟩

The step, against the tower

This is the chapter's engine, and both halves of it come out of the same three private lines. The step at an argument b collects, over the arguments c below b and the values w recorded there, the members of the definable powerset of w. The meta tower at b collects the same thing with Lset c in place of w. So if the table is correct the two have the same members, and that is the whole mathematics: step-Lset reads a satisfied step and gets the tower back,

step-table writes the step from the tower.

The previous chapter's side condition is discharged here, once, for both directions. PowOK asks that the definable powerset of every recorded value be an element of L; a recorded value is the tower at an argument below B, that argument is an ordinal because B is one, and the definable powerset of a stage is constructible. So correctness plus a single ordinality hypothesis is all the step ever needs, and neither reading carries the condition in its statement.

The two directions are named apart because they are used apart. Going up is the definable powerset of a recorded value sitting inside the tower at B, which is

Lset-in. Coming down is the tower's own decomposition,

Lset-out, followed by naming the ordinal it produces as an element of the model, which transitivity of the class supplies for free.

module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) where
  private
    ok : IsOrd (fst (lookup b γ)) → Values (lookup f γ) (fst (lookup b γ))
       → PowOK b f γ
    ok ob vals c z rec = subst (λ u → ⟨ isL (𝒟ₒ u) ⟩)
      (sym (vals c z (rec .fst) (rec .snd)))
      (isL-𝒟ₒ (fst c) (mem-ord {A = fst (lookup b γ)} ob (fst c) (rec .fst)))

    below : IsOrd (fst (lookup b γ)) → Entries (lookup f γ) (fst (lookup b γ))
          → (z : S)
          → Σ[ δ ∈ V ℓ ] (⟨ δ ∈ fst (lookup b γ) ⟩ × ⟨ fst z ∈ 𝒟ₒ (Lset δ) ⟩)
          → StepOf b f γ z
    below ob ents z (δ , (δ∈ , hz)) =
      d , (LsetS δ oδ , ((δ∈ , ents d δ∈) , hz))
      where
      oδ : IsOrd δ
      oδ = mem-ord {A = fst (lookup b γ)} ob δ δ∈
      d : S
      d = δ , isL-trans {x = fst (lookup b γ)} {y = δ} δ∈ (lookup b γ .snd)

    above : Values (lookup f γ) (fst (lookup b γ)) → (z : S) → StepOf b f γ z
          → ⟨ fst z ∈ Lset (fst (lookup b γ)) ⟩
    above vals z (c , (w , (rec , hz))) =
      Lset-in (fst (lookup b γ)) (fst c) (fst z) (rec .fst)
        (subst (λ u → ⟨ fst z ∈ 𝒟ₒ u ⟩) (vals c w (rec .fst) (rec .snd)) hz)

  step-Lset : ⟨ γ ⊨ StepAt v b f ⟩ → IsOrd (fst (lookup b γ))
            → Values (lookup f γ) (fst (lookup b γ))
            → Entries (lookup f γ) (fst (lookup b γ))
            → fst (lookup v γ) ≡ Lset (fst (lookup b γ))
  step-Lset h ob vals ents =
    extensionalV {a = fst (lookup v γ)} {b = Lset (fst (lookup b γ))} pt
    where
    fwd : (x : V ℓ) → ⟨ x ∈ fst (lookup v γ) ⟩
        → ⟨ x ∈ Lset (fst (lookup b γ)) ⟩
    fwd x hx = PT.rec (snd (x ∈ Lset (fst (lookup b γ)))) (above vals z)
      (StepAt-out v b f γ h (ok ob vals) z hx)
      where
      z : S
      z = x , isL-trans {x = fst (lookup v γ)} {y = x} hx (lookup v γ .snd)

    bwd : (x : V ℓ) → ⟨ x ∈ Lset (fst (lookup b γ)) ⟩
        → ⟨ x ∈ fst (lookup v γ) ⟩
    bwd x hx = PT.rec (snd (x ∈ fst (lookup v γ))) put
      (Lset-out (fst (lookup b γ)) x hx)
      where
      z : S
      z = x , isL-trans {x = Lset (fst (lookup b γ))} {y = x} hx
                (LsetS (fst (lookup b γ)) ob .snd)
      put : Σ[ δ ∈ V ℓ ] (⟨ δ ∈ fst (lookup b γ) ⟩ × ⟨ x ∈ 𝒟ₒ (Lset δ) ⟩)
          → ⟨ x ∈ fst (lookup v γ) ⟩
      put s = StepAt-back v b f γ h (ok ob vals) z (below ob ents z s)

    pt : (x : V ℓ) → (x ∈ fst (lookup v γ)) ≡ (x ∈ Lset (fst (lookup b γ)))
    pt x = ⇔toPath (fwd x) (bwd x)

  step-table : IsOrd (fst (lookup b γ))
             → Values (lookup f γ) (fst (lookup b γ))
             → Entries (lookup f γ) (fst (lookup b γ))
             → fst (lookup v γ) ≡ Lset (fst (lookup b γ))
             → ⟨ γ ⊨ StepAt v b f ⟩
  step-table ob vals ents q = StepAt-in v b f γ (ok ob vals) into back
    where
    into : (z : S) → ⟨ fst z ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ z ∥₁
    into z hz = PT.map (below ob ents z)
      (Lset-out (fst (lookup b γ)) (fst z)
        (subst (λ u → ⟨ fst z ∈ u ⟩) q hz))

    back : (z : S) → StepOf b f γ z → ⟨ fst z ∈ fst (lookup v γ) ⟩
    back z s = subst (λ u → ⟨ fst z ∈ u ⟩) (sym q) (above vals z s)

Every value an approximation records

One induction, on the argument, in the meta-language, with the approximation and its domain held fixed. The motive says: whatever value the approximation records at this argument is the meta tower there. It quantifies over all recorded values, and that is why single-valuedness is nowhere a hypothesis. Two values recorded at one argument are both pinned to the same tower value, so they are equal; the previous chapter's ruling that the approximation carries no single-valuedness conjunct is collected here, as approx-uniq, in three lines.

The step of the induction is step-Lset at the recorded value. Correctness below the argument is the induction hypothesis, verbatim. Completeness below the argument is where the domain hypothesis is spent: an argument below this one is below the approximation's domain, because the domain is an ordinal and ordinals are transitive; the approximation therefore has a value there; and the induction hypothesis identifies it with the tower's. That value is produced only merely, which is enough, because what is being proved of it is a membership.

module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) where
  private
    Value : V ℓ → Type (ℓ-suc ℓ)
    Value u = ⟨ isL u ⟩ → (z : S)
            → ⟨ pr u (fst z) ∈ fst (lookup f γ) ⟩ → fst z ≡ Lset u

  approx-val : ⟨ γ ⊨ ApproxAt f a ⟩ → IsOrd (fst (lookup a γ))
             → (x z : S) → ⟨ pr (fst x) (fst z) ∈ fst (lookup f γ) ⟩
             → fst z ≡ Lset (fst x)
  approx-val h oa x = ∈-induction {P = Value} go (fst x) (snd x)
    where
    go : (u : V ℓ) → ((t : V ℓ) → ⟨ t ∈ u ⟩ → Value t) → Value u
    go u IH hu z p = step-Lset zero (suc zero) (sh2 f) (z ∷ d ∷ γ)
      (ApproxAt-step f a γ h d z p) ou vals ents
      where
      d : S
      d = u , hu
      u∈a : ⟨ u ∈ fst (lookup a γ) ⟩
      u∈a = ApproxAt-dom f a γ h d z p
      ou : IsOrd u
      ou = mem-ord {A = fst (lookup a γ)} oa u u∈a
      vals : Values (lookup f γ) u
      vals c y c∈ q = IH (fst c) c∈ (snd c) y q
      ents : Entries (lookup f γ) u
      ents c c∈ = PT.rec
        (snd (pr (fst c) (Lset (fst c)) ∈ fst (lookup f γ))) named
        (ApproxAt-value f a γ h c (oa .fst {x = u} {y = fst c} c∈ u∈a))
        where
        named : Σ[ y ∈ S ] ⟨ pr (fst c) (fst y) ∈ fst (lookup f γ) ⟩
              → ⟨ pr (fst c) (Lset (fst c)) ∈ fst (lookup f γ) ⟩
        named (y , q) = subst (λ t → ⟨ pr (fst c) t ∈ fst (lookup f γ) ⟩)
          (IH (fst c) c∈ (snd c) y q) q

  approx-uniq : ⟨ γ ⊨ ApproxAt f a ⟩ → IsOrd (fst (lookup a γ))
              → (x y z : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
              → ⟨ pr (fst x) (fst z) ∈ fst (lookup f γ) ⟩ → y ≡ z
  approx-uniq h oa x y z p q = Σ≡Prop (λ u → snd (isL u))
    (approx-val h oa x y p ∙ sym (approx-val h oa x z q))

The graph holds of nothing else

The graph says there merely is an approximation on the argument whose step at the argument is the value. Read it and everything is already in hand: unpack the approximation, take correctness from approx-val, take completeness from

ApproxAt-value composed with approx-val again, and apply

step-Lset one last time. The conclusion is that the graph determines its value: whatever satisfies it at an ordinal is the meta tower there.

The reading stands at variable slots, and that is not decoration. Its two consumers instantiate it at two different concrete environments, and a statement made at either would have to be converted to the other through a satisfaction carrying the whole tower description inside it.

module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where
  Lset-only : ⟨ γ ⊨ LsetGraphAt w b ⟩ → IsOrd (fst (lookup b γ))
            → fst (lookup w γ) ≡ Lset (fst (lookup b γ))
  Lset-only h ob = PT.rec
    (setIsSet (fst (lookup w γ)) (Lset (fst (lookup b γ)))) read
    (LsetGraph-out w b γ h)
    where
    read : GraphOf w b γ → fst (lookup w γ) ≡ Lset (fst (lookup b γ))
    read (f , (ha , hs)) =
      step-Lset (suc w) (suc b) zero (f ∷ γ) hs ob vals ents
      where
      vals : Values f (fst (lookup b γ))
      vals c z _ p = approx-val zero (suc b) (f ∷ γ) ha ob c z p
      ents : Entries f (fst (lookup b γ))
      ents c c∈ = PT.rec (snd (pr (fst c) (Lset (fst c)) ∈ fst f)) named
        (ApproxAt-value zero (suc b) (f ∷ γ) ha c c∈)
        where
        named : Σ[ y ∈ S ] ⟨ pr (fst c) (fst y) ∈ fst f ⟩
              → ⟨ pr (fst c) (Lset (fst c)) ∈ fst f ⟩
        named (y , q) = subst (λ t → ⟨ pr (fst c) t ∈ fst f ⟩)
          (approx-val zero (suc b) (f ∷ γ) ha ob c y q) q

A table is an approximation

The converse direction needs a witness, and a correct, complete table is one.

graph-table turns such a table into a satisfaction of the graph by filling in the previous chapter's projections and doing nothing else.

The domain conjunct is Domain one way and Entries the other. The step conjunct at a recorded pair is step-table at that argument, whose correctness and completeness are the table's own restricted below it; the restriction is where transitivity of the ordinal is spent for the second and last time. The value the graph is asked about is the step at the whole argument, which is step-table once more. So one table serves both conjuncts of "is an approximation" and the outer step as well.

module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where
  graph-table : (h : S) → IsOrd (fst (lookup b γ))
              → Values h (fst (lookup b γ)) → Entries h (fst (lookup b γ))
              → Domain h (fst (lookup b γ))
              → fst (lookup w γ) ≡ Lset (fst (lookup b γ))
              → ⟨ γ ⊨ LsetGraphAt w b ⟩
  graph-table h ob vals ents dom q = LsetGraph-in w b γ h approx
    (step-table (suc w) (suc b) zero (h ∷ γ) ob vals ents q)
    where
    onDom : (c : S)
          → (⟨ ⋁ S (λ y → pr (fst c) (fst y) ∈ fst h) ⟩
             → ⟨ fst c ∈ fst (lookup b γ) ⟩)
          × (⟨ fst c ∈ fst (lookup b γ) ⟩
             → ⟨ ⋁ S (λ y → pr (fst c) (fst y) ∈ fst h) ⟩)
    onDom c = (λ hy → PT.rec (snd (fst c ∈ fst (lookup b γ))) named hy)
            , (λ c∈ → ∣ LsetS (fst c) (mem-ord {A = fst (lookup b γ)} ob (fst c) c∈)
                     , ents c c∈ ∣₁)
      where
      named : Σ[ y ∈ S ] ⟨ pr (fst c) (fst y) ∈ fst h ⟩
            → ⟨ fst c ∈ fst (lookup b γ) ⟩
      named (y , p) = dom c y p

    onStep : (c y : S) → ⟨ pr (fst c) (fst y) ∈ fst h ⟩
           → ⟨ (y ∷ c ∷ h ∷ γ) ⊨ StepAt zero (suc zero) (suc (suc zero)) ⟩
    onStep c y p = step-table zero (suc zero) (suc (suc zero)) (y ∷ c ∷ h ∷ γ)
      oc vals' ents' (vals c y c∈ p)
      where
      c∈ : ⟨ fst c ∈ fst (lookup b γ) ⟩
      c∈ = dom c y p
      oc : IsOrd (fst c)
      oc = mem-ord {A = fst (lookup b γ)} ob (fst c) c∈
      vals' : Values h (fst c)
      vals' e t _ r = vals e t (dom e t r) r
      ents' : Entries h (fst c)
      ents' e e∈ = ents e (ob .fst {x = fst c} {y = fst e} e∈ c∈)

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

The pair graph

The table has to be built, and the only builder is replacement, which asks for a graph. This is that graph, and it is the previous chapter's packaged: the value at an argument is the ordered pair of the argument with the tower's value there. One existential binds the tower's value, the pair reader equates the entry with the pair, and the tower graph says the bound value is the right one.

Its two readings take the sentence as a parameter, with the sentence's own equation as a hypothesis, refl at the single call site. That is the shape rule for a frame generic in a construction, and this chapter is where it was measured on a sentence rather than on a constructor: written directly against the closed sentence, the readings cost 85 seconds, because Agda decides the equality of two spellings of one formula by normalizing a satisfaction that carries the entire definable-powerset description inside it. With the sentence a variable there is nothing to normalize.

PairGraphAt : ∀ {n} → Fin n → Fin n → Formula S n
PairGraphAt e c = ∃̇ (prAtL (suc e) (suc c) zero ∧̇ LsetGraphAt zero (suc c))

module _ {n : ℕ} (e c : Fin n) (γ : S ^ n)
         (φ : Formula S n) (qφ : φ ≡ PairGraphAt e c) where
  PairOf : Type (ℓ-suc ℓ)
  PairOf = Σ[ z ∈ S ] ( (fst (lookup e γ) ≡ pr (fst (lookup c γ)) (fst z))
                      × ⟨ (z ∷ γ) ⊨ LsetGraphAt zero (suc c) ⟩ )

  private
    readPair : Σ[ z ∈ S ] ⟨ (z ∷ γ) ⊨
                 (prAtL (suc e) (suc c) zero ∧̇ LsetGraphAt zero (suc c)) ⟩
             → PairOf
    readPair (z , (hq , hg)) =
      z , (subst ⟨_⟩ (prAtL-adequate (suc e) (suc c) zero (z ∷ γ)) hq , hg)

  PairGraph-in : (z : S) → fst (lookup e γ) ≡ pr (fst (lookup c γ)) (fst z)
               → ⟨ (z ∷ γ) ⊨ LsetGraphAt zero (suc c) ⟩
               → ⟨ γ ⊨ φ ⟩
  PairGraph-in z q hg = subst (λ ψ → ⟨ γ ⊨ ψ ⟩) (sym qφ)
    ∣ z , (subst ⟨_⟩
      (sym (prAtL-adequate (suc e) (suc c) zero (z ∷ γ))) q , hg) ∣₁

  PairGraph-out : ⟨ γ ⊨ φ ⟩ → ∥ PairOf ∥₁
  PairGraph-out h = PT.map readPair (subst (λ ψ → ⟨ γ ⊨ ψ ⟩) qφ h)

The internal hierarchy

Recorded names the class the internal hierarchy realizes: the pairs of an ordinal below α with the tower's value there, and nothing besides.

IsHier says a set of the model realizes it, member for member. That is a membership equivalence and not a one-directional collection, for the reason the previous chapter recorded: said one way it would not say the collection holds only such pairs, the existence claim would then not be a proposition, and every step below would need an internal function-extensionality lemma to pass from two collections to one. Said as an equivalence, two realizers are equal by extensionality in L, HierOf is a proposition, and so is the motive of the induction that builds it.

The two readings stand at a variable collection reached by its specification, never at the sealed construction. Reading out is injectivity of the pair applied to a member; reading in exhibits the pair as an element of the model, which the model's own pairing supplies, and needs ordinality of the argument in order to name the value at all.

Then the construction, one membership induction on the ordinal. At α the pair graph is functional at every argument below: the induction hypothesis hands over the hierarchy up to that argument, graph-table turns it into a satisfaction of the tower graph, and Lset-only says nothing else satisfies it. Replacement collects the pairs, and the collected set realizes the class in both directions through those same two facts. Ordinality of each argument is taken from mem-ord untruncated, which is why no decidable-ordinality branch appears anywhere on this route, and the functionality obligation is filled through mereFunct, because the value at an argument is a construction rather than a decision.

The construction is sealed where it is built. Everything below reaches it through its specification, and no induction is ever unfolded into a conversion.

Recorded : V ℓ → V ℓ → Ω
Recorded B z = ⋁ S (λ c → (fst c ∈ B)
  ⊓ ((z ≡ pr (fst c) (Lset (fst c))) , setIsSet z (pr (fst c) (Lset (fst c)))))

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

HierOf : V ℓ → Type (ℓ-suc (ℓ-suc ℓ))
HierOf B = Σ[ h ∈ S ] IsHier B h

hier-unique : (B : V ℓ) (h k : S) → IsHier B h → IsHier B k → h ≡ k
hier-unique B h k sp sq = extensionalL (λ z → sp z ∙ sym (sq z))

isPropHierOf : (B : V ℓ) → isProp (HierOf B)
isPropHierOf B (h , sp) (k , sq) = Σ≡Prop
  (λ m → isPropΠ (λ z → isSetHProp (fst z ∈ fst m) (Recorded B (fst z))))
  (hier-unique B h k sp sq)

module _ (B : V ℓ) (oB : IsOrd B) (h : S) (sp : IsHier B h) where
  hier-out : (c z : S) → ⟨ pr (fst c) (fst z) ∈ fst h ⟩
           → ⟨ fst c ∈ B ⟩ × (fst z ≡ Lset (fst c))
  hier-out c z p = PT.rec
    (isProp× (snd (fst c ∈ B)) (setIsSet (fst z) (Lset (fst c)))) read
    (subst ⟨_⟩ (sp k) p)
    where
    k : S
    k = pr (fst c) (fst z)
      , isL-trans {x = fst h} {y = pr (fst c) (fst z)} p (h .snd)
    read : Σ[ d ∈ S ] (⟨ fst d ∈ B ⟩
             × (pr (fst c) (fst z) ≡ pr (fst d) (Lset (fst d))))
         → ⟨ fst c ∈ B ⟩ × (fst z ≡ Lset (fst c))
    read (d , (d∈ , eq)) =
        subst (λ t → ⟨ t ∈ B ⟩) (sym (pr-inj eq .fst)) d∈
      , (pr-inj eq .snd ∙ cong Lset (sym (pr-inj eq .fst)))

  hier-in : (c : S) → ⟨ fst c ∈ B ⟩ → ⟨ pr (fst c) (Lset (fst c)) ∈ fst h ⟩
  hier-in c c∈ = subst (λ t → ⟨ t ∈ fst h ⟩) (prʟ-fst c (LsetS (fst c) oc))
    (subst ⟨_⟩ (sym (sp k)) ∣ c , (c∈ , prʟ-fst c (LsetS (fst c) oc)) ∣₁)
    where
    oc : IsOrd (fst c)
    oc = mem-ord {A = B} oB (fst c) c∈
    k : S
    k = prʟ c (LsetS (fst c) oc)

opaque
  hierAt : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → HierOf α
  hierAt = ∈-induction {P = λ α → ⟨ isL α ⟩ → IsOrd α → HierOf α}
    (build (PairGraphAt zero (suc zero)) refl)
    where
    -- perf: the pair graph enters as a variable with its own equation; spelled
    -- out as the closed sentence, three conversions cost 85 s between them
    build : (φ : Formula S ) → φ ≡ PairGraphAt zero (suc zero)
          → (α : V ℓ)
          → ((δ : V ℓ) → ⟨ δ ∈ α ⟩ → ⟨ isL δ ⟩ → IsOrd δ → HierOf δ)
          → ⟨ isL α ⟩ → IsOrd α → HierOf α
    build φ qφ α IH hα oα = r .fst .fst , spec
      where
      A : S
      A = α , hα

      value : (c : S) → ⟨ fst c ∈ α ⟩ → S
      value c c∈ = LsetS (fst c) (mem-ord {A = α} oα (fst c) c∈)

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

      below : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) (k : S)
            → ⟨ (value c c∈ ∷ k ∷ c ∷ []) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩
      below c c∈ k = graph-table zero (suc (suc zero)) (value c c∈ ∷ k ∷ c ∷ [])
        (hc .fst) oc
        (λ d z _ p → hier-out (fst c) oc (hc .fst) (hc .snd) d z p .snd)
        (hier-in (fst c) oc (hc .fst) (hc .snd))
        (λ d z p → hier-out (fst c) oc (hc .fst) (hc .snd) d z p .fst)
        refl
        where
        oc : IsOrd (fst c)
        oc = mem-ord {A = α} oα (fst c) c∈
        hc : HierOf (fst c)
        hc = IH (fst c) c∈ (snd c) oc

      holds : (c : S) (c∈ : ⟨ fst c ∈ α ⟩)
            → ⟨ (entry c c∈ ∷ c ∷ []) ⊨ φ ⟩
      holds c c∈ = PairGraph-in zero (suc zero) (entry c c∈ ∷ c ∷ []) φ qφ
        (value c c∈) (prʟ-fst c (value c c∈)) (below c c∈ (entry c c∈))

      only : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) (k : S)
           → ⟨ (k ∷ c ∷ []) ⊨ φ ⟩ → k ≡ entry c c∈
      only c c∈ k h = PT.rec (isSetS k (entry c c∈)) read
        (PairGraph-out zero (suc zero) (k ∷ c ∷ []) φ qφ h)
        where
        read : PairOf zero (suc zero) (k ∷ c ∷ []) φ qφ → k ≡ entry c c∈
        read (z , (q , hg)) = Σ≡Prop (λ t → snd (isL t))
          ( q
          ∙ cong (pr (fst c))
              (Lset-only zero (suc (suc zero)) (z ∷ k ∷ c ∷ []) hg
                (mem-ord {A = α} oα (fst c) c∈))
          ∙ sym (prʟ-fst c (value c c∈)) )

      fc : (c : S) → ⟨ c ∈ˢ A ⟩
         → isContr (Σ[ k ∈ S ] ⟨ (k ∷ c ∷ []) ⊨ φ ⟩)
      fc c c∈ = mereFunct φ c ∣ entry c c∈ , (holds c c∈ , only c c∈) ∣₁

      r : isContr (SetOf (λ z → ⋁ S (λ c → (c ∈ˢ A) ⊓ ((z ∷ c ∷ []) ⊨ φ))))
      r = hasReplacementL A φ fc

      spec : IsHier α (r .fst .fst)
      spec z = ⇔toPath toRec fromRec
        where
        toRec : ⟨ fst z ∈ fst (r .fst .fst) ⟩ → ⟨ Recorded α (fst z) ⟩
        toRec hz = PT.rec squash₁ conv (subst ⟨_⟩ (r .fst .snd z) hz)
          where
          conv : Σ[ c ∈ S ] (⟨ fst c ∈ α ⟩ × ⟨ (z ∷ c ∷ []) ⊨ φ ⟩)
               → ⟨ Recorded α (fst z) ⟩
          conv (c , (c∈ , hp)) = ∣ c , (c∈ , cong fst (only c c∈ z hp)
                                            ∙ prʟ-fst c (value c c∈)) ∣₁

        fromRec : ⟨ Recorded α (fst z) ⟩ → ⟨ fst z ∈ fst (r .fst .fst) ⟩
        fromRec hz = subst ⟨_⟩ (sym (r .fst .snd z)) (PT.map conv hz)
          where
          conv : Σ[ c ∈ S ] (⟨ fst c ∈ α ⟩
                   × (fst z ≡ pr (fst c) (Lset (fst c))))
               → Σ[ c ∈ S ] (⟨ fst c ∈ α ⟩ × ⟨ (z ∷ c ∷ []) ⊨ φ ⟩)
          conv (c , (c∈ , eq)) = c , (c∈
            , subst (λ t → ⟨ (t ∷ c ∷ []) ⊨ φ ⟩) (sym zeq) (holds c c∈))
            where
            zeq : z ≡ entry c c∈
            zeq = Σ≡Prop (λ t → snd (isL t))
              (eq ∙ sym (prʟ-fst c (value c c∈)))

hierL : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → S
hierL α hα oα = hierAt α hα oα .fst

hierL-spec : (α : V ℓ) (hα : ⟨ isL α ⟩) (oα : IsOrd α)
           → IsHier α (hierL α hα oα)
hierL-spec α hα oα = hierAt α hα oα .snd

The tower satisfies the graph

The last statement is one line, because the internal hierarchy at an ordinal is a correct, complete table on it and graph-table was written for exactly that. With Lset-only beside it, the graph and the meta tower now agree in both directions at every ordinal, which is what the chapter was for.

module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where
  Lset-defines : IsOrd (fst (lookup b γ))
               → fst (lookup w γ) ≡ Lset (fst (lookup b γ))
               → ⟨ γ ⊨ LsetGraphAt w b ⟩
  Lset-defines ob q = graph-table w b γ H ob
    (λ c z _ p → hier-out (fst (lookup b γ)) ob H sp c z p .snd)
    (hier-in (fst (lookup b γ)) ob H sp)
    (λ c z p → hier-out (fst (lookup b γ)) ob H sp c z p .fst)
    q
    where
    H : S
    H = hierL (fst (lookup b γ)) (lookup b γ .snd) ob
    sp : IsHier (fst (lookup b γ)) H
    sp = hierL-spec (fst (lookup b γ)) (lookup b γ .snd) ob

Recap

approx-val pins every value an approximation records to the meta tower, by one membership induction on the argument, with no single-valuedness hypothesis anywhere; approx-uniq is the corollary the previous chapter left to be collected here. Lset-only and Lset-defines are the graph's two directions against the tower, and hierL is what the second is built from: the internal hierarchy, an element of L whose members are exactly the pairs of an ordinal with the tower's value at it, unique because its specification is a membership equivalence, and sealed where it is built.

Nothing here recomputes the last chapter. The step's three readings, the approximation's four projections and the graph's two are used as delivered; what is added is the bridge to the meta tower, and the bridge is two lemmas,

step-Lset and step-table, applied four times between them.

Two measurements are worth keeping, and both are about a name rather than about mathematics. Letting the pair graph enter as a variable carrying its own equation, rather than as the closed sentence it will be instantiated to, is worth 85 seconds; the mechanism is the one the last two chapters met, that two spellings of one formula are compared by normalizing a satisfaction with the whole definable-powerset description inside it. And the set argument of

mem-ord has to be given explicitly at every use:

IsOrd unfolds to a quantified membership, so nothing in the hypothesis determines the set it is about, and left implicit the chapter does not close at all.

What the chapter delivers is the object the next part consumes. L now has a name for its own tower, and a well-order of L is read off a tower: one set before another when it appears at an earlier stage, or at the same stage under an earlier formula. The first half of that is now sayable inside the model.