--- title: "The constructible hierarchy inside L" module: L.Hierarchy lang: en site: "Bedrock" description: "The constructible hierarchy inside L" stage: "Internal coding: tables and uniform satisfaction" reading_order: 71 canonical: https://bedrock.institute/en/L.Hierarchy.html html: L.Hierarchy.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Hierarchy.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, FOL.ZFModel, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Full, L.Recursion, L.Coding.Model, L.Coding.HierarchySequence] routes: [internal-satisfaction] translations: [https://bedrock.institute/zh/L.Hierarchy.md, https://bedrock.institute/ja/L.Hierarchy.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # The constructible hierarchy inside L A first-order graph inside `L` records the external constructible hierarchy up to a chosen ordinal. Tables are compared with the external tower, shown functional and exact, then collected into a constructible set whose members are precisely the earlier stages. The chapter constructs the internal hierarchy. For an ordinal `α` of the hierarchy, `hierL` at `α` is an element of `L` whose members are exactly the ordered pairs of an ordinal `β` below `α` with the tower's value `Lset β` at it. One pattern repeats throughout. A **table** is a set of ordered pairs; it is *correct* on a set `B` when every value it records below `B` is the meta tower there, and *complete* when it records a value at every argument below. Correct and complete tables are exactly what the step condition of the graph reads and what it can be written from, so the pair of lemmas connecting the step with the tower serves both elimination and introduction. ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Classical using ( LEM ) module L.Hierarchy {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where ``` The chapter runs at one excluded-middle instance, taken at the successor of the model's own level; every construction below is stated inside this module and carries that hypothesis only where an axiom chapter passed it on. ```agda open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula ) import FOL.Absoluteness import FOL.ZFModel ``` Two structures are in play. The ambient hierarchy contributes its structure `𝒮ᵥ`, whose membership induction and extensionality the chapter will use; the constructible structure `𝒮ʟ` contributes the carrier `S`, whose elements are sets of the hierarchy together with a proof that they are constructible, so every carrier element `x` has an underlying set `fst x`. ```agda open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV ) open import V.Coding {ℓ} using ( pr; pr-inj ) ``` From the hierarchy come three tools used throughout: induction along membership, extensionality of sets, and the ordered pair `pr` with the injectivity that recovers its components. The pair lives at the level of the hierarchy, which is where the recorded entries of a table live too. ```agda open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; 𝒟ₒ; Lset; Lset-in; Lset-out; IsOrd ) ``` From the constructible side come the tower `Lset`, which sends an ordinal of the hierarchy to the constructible stage at it; the definable powerset `𝒟ₒ`; the two membership readings `Lset-in` and `Lset-out`; ordinality `IsOrd`; and the facts that constructibility is carried along membership. The tower is indexed by ordinals, which are sets of the hierarchy, never by universe levels, which are size indices of types. ```agda open import L.Ordinal {ℓ} using ( mem-ord ) open import L.Axioms.Basic {ℓ} using ( LsetS; isL-𝒟ₒ ) open import L.Axioms.Full {ℓ} lem using ( hasReplacementL ) open import L.Recursion {ℓ} lem using ( mereFunct ) ``` Three further facts carry the chapter: a member of an ordinal is an ordinal; a stage can be presented as an element of `L`, written `LsetS`, and the definable powerset of a constructible set is constructible; and replacement is available inside `L`, in a form that accepts a value known only to exist uniquely. The model contributes its own ordered pair `prʟ`, with the reading `prʟ-fst` that identifies its first projection, and the domain clause `domAt-intro`. ```agda open import L.Coding.Model {ℓ} using ( prʟ; prʟ-fst; domAt-intro ) ``` The preceding coding chapter contributes the vocabulary this chapter assembles: the step condition with its witness and three readings, the approximation with its domain, value and step clauses, the tower graph with its two readings, and the pair graph. ```agda open import L.Coding.HierarchySequence {ℓ} 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 ; PairGraphAt; PairOf; PairGraph-in; PairGraph-out ) ``` The propositional machinery is the usual one: truncated existence, its injection and elimination, the fact that a pair with a propositional second component is equal when its first components are, and the conversion of a pointwise equivalence of memberships into a path of sets. ```agda 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₁ ) ``` The hierarchy itself appears as a type: its elements are the sets the chapter tabulates, its membership is the relation the three conditions speak about, and its h-setness makes equality of two tabulated sets a proposition. ```agda open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) ``` Inside the constructible structure, `S` is the carrier and `⊨` the satisfaction judgment; `SetOf` pairs a candidate set with the assertion that it realizes a class, the form in which the record's fields state their axioms. ```agda open hPropStructure 𝒮ʟ module ModelL = FOL.ZFModel 𝒮ʟ open ModelL using ( SetOf ) ``` Satisfaction is finally read at the constructible structure: the notation `γ ⊨ φ` throughout the chapter judges object-language formulas at environments of carrier elements, with constants drawn from `L`. ```agda module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ) ``` One private helper shifts variable slots by two: when a step is read in an environment extended by a value and then an argument, every old slot moves two places back. It appears whenever the step of a table is judged from inside its own entry. ```agda private sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i) ``` ## What a table records A **table** is a set of ordered pairs, here always pairs taken with the hierarchy's pairing: an argument together with a value. Three conditions describe a table over a bound set `B`, and they are complementary rather than three readings of one statement. `Values` requires every value recorded below `B` to be the tower's value there. `Entries` requires the canonical entry to be recorded at every argument below `B`. `Domain` requires that nothing outside `B` is recorded at all. ```agda 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) ``` Correctness is a statement about recorded entries. If the pair of an argument `c` below `B` with some `z` is an entry of the table, then `z` is the tower at `c`. The membership `fst c ∈ B` is membership in the hierarchy, `B` being a set of the hierarchy; the table `h` is a carrier element, and `fst h` is the set it presents. ```agda Entries : S → V ℓ → Type (ℓ-suc ℓ) Entries h B = (c : S) → ⟨ fst c ∈ B ⟩ → ⟨ pr (fst c) (Lset (fst c)) ∈ fst h ⟩ ``` Completeness is the mirror requirement on coverage: at each argument `c` below `B`, the canonical entry, the pair of `c` with the tower's value `Lset c`, is recorded. Between the two conditions, a correct and complete table records, below `B`, exactly the canonical entries and nothing distorted. ```agda Domain : S → V ℓ → Type (ℓ-suc ℓ) Domain h B = (c z : S) → ⟨ pr (fst c) (fst z) ∈ fst h ⟩ → ⟨ fst c ∈ B ⟩ ``` The conditions are kept apart because the applications need different subsets of them. The induction over an approximation uses the first two and cannot use the third: an approximation's entries lie below its own domain, not below the argument the induction stands at. The internal hierarchy will satisfy all three, being built as exactly the set of the right pairs. Note also what `B` is: the underlying bound set, a set of the hierarchy. In the semantic applications it arrives at a slot of the environment, as the underlying part of a carrier element that carries constructibility besides, and the ordinality of `B` is a separate hypothesis the conditions do not supply. The stages indexed here are sets of the hierarchy, indexed by ordinals; the universe levels of the host never enter the tabulation. ## The step, against the tower This section connects the step condition of the previous chapter with the tower. 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 tower at `b` collects the same members, with `Lset c` in place of the recorded `w`. Three private facts prepare the comparison: `ok` discharges the side condition `PowOK`, `below` turns a decomposition of the tower into a step witness, and `above` turns a step witness into a member of the tower. ```agda module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) where private ``` The three slots name the value, the argument, and the table, all read from one environment `γ` of carrier elements. ```agda ok : IsOrd (fst (lookup b γ)) → Values (lookup f γ) (fst (lookup b γ)) → PowOK b f γ ``` The side condition is discharged 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 indexed by an ordinal is constructible. 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. ```agda 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))) ``` The proof assembles the two hypotheses. The witness `rec` says `c` is below the argument, so `c` is an ordinal by the ordinality of the argument; correctness identifies the recorded value with the tower at `c`; and the definable powerset of a constructible stage is constructible, which is `isL-𝒟ₒ`. The transport lines the two facts up on the same value. ```agda 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` turns a decomposition of the tower into a step witness. The tower at `b` decomposes each member: a member `z` sits in the definable powerset of the stage at some `δ` below `b`. The witness must name an argument below the argument and a recorded value whose powerset contains `z`. ```agda below ob ents z (δ , (δ∈ , hz)) = d , (LsetS δ oδ , ((δ∈ , ents d δ∈) , hz)) ``` The witness is given at the argument `d`, the carrier element of `δ`, where the table records the canonical entry by completeness. The recorded value there is the stage at `δ`, presented as an element of `L`, and `z` lies in its definable powerset by the decomposition. ```agda where oδ : IsOrd δ oδ = mem-ord {A = fst (lookup b γ)} ob δ δ∈ d : S d = δ , isL-trans {x = fst (lookup b γ)} {y = δ} δ∈ (lookup b γ .snd) ``` Two bookkeeping facts complete the construction. The ordinality of `δ` follows from that of `b`, members of ordinals being ordinals; and `δ` is constructible because it belongs to the constructible set underlying the argument. The carrier element `d` packages the set with that certificate. ```agda above : Values (lookup f γ) (fst (lookup b γ)) → (z : S) → StepOf b f γ z → ⟨ fst z ∈ Lset (fst (lookup b γ)) ⟩ ``` `above` is the mirror: a step witness places a member into the tower. The witness names an argument `c` below the argument, a recorded value `w` there, and a membership of `z` in the definable powerset of `w`. ```agda 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) ``` Correctness identifies the recorded `w` with the tower at `c`, so `z` lies in the definable powerset of that stage; the upward reading of the tower then places `z` inside the tower at `b`, using the ordinality of `c` carried by the witness. ```agda 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 γ)) ``` The upward lemma reads: if the step condition is satisfied at the environment, if the argument is an ordinal, and if the table is correct and complete on it, then the value recorded at the value slot is the tower at the argument. ```agda step-Lset h ob vals ents = extensionalV {a = fst (lookup v γ)} {b = Lset (fst (lookup b γ))} pt where ``` Two sets of the hierarchy with the same members are equal, and this is extensionality of the ambient hierarchy. The proof exhibits the pointwise equivalence `pt` and lets extensionality assemble the path. ```agda 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) ``` The forward direction: a member `x` of the recorded value yields a step witness, because the step condition is satisfied; the witness is eliminated into the proposition that `x` belongs to the tower, and `above` proves that proposition from the witness. ```agda where z : S z = x , isL-trans {x = fst (lookup v γ)} {y = x} hx (lookup v γ .snd) ``` To apply `above`, `x` is needed as a carrier element; its constructibility follows from that of the recorded value, since `x` is a member of it. ```agda 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) ``` The backward direction: the tower decomposes each member `x`, exhibiting a stage below the argument whose definable powerset contains it. The decomposition is eliminated into the proposition that `x` belongs to the recorded value. ```agda where z : S z = x , isL-trans {x = Lset (fst (lookup b γ))} {y = x} hx (LsetS (fst (lookup b γ)) ob .snd) ``` Again `x` must be carried: its constructibility follows from belonging to the stage at the argument, whose element-of-`L` presentation is `LsetS` at the ordinality `ob`. ```agda 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) ``` The decomposition is converted into a step witness by `below`, and the backward reading of the step condition, `StepAt-back`, turns the witness into membership in the recorded value. ```agda pt : (x : V ℓ) → (x ∈ fst (lookup v γ)) ≡ (x ∈ Lset (fst (lookup b γ))) pt x = ⇔toPath (fwd x) (bwd x) ``` For each member, membership in the recorded value and membership in the tower are the same proposition; the two directions give the equivalence, and extensionality promotes it member by member to the equality of sets. ```agda 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 ⟩ ``` The downward lemma reverses the traffic: given the ordinality of the argument, correctness, completeness, and the fact that the recorded value is the tower, the step condition is satisfied. ```agda step-table ob vals ents q = StepAt-in v b f γ (ok ob vals) into back where ``` The step condition is introduced from its two directions, existence of a witness for each member and soundness of every witness, with `ok` supplying the side condition once for both. ```agda 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)) ``` A member `z` of the recorded value is first transported into the tower along the identification `q`, then decomposed by the tower, and `below` converts the decomposition into a witness, which only has to exist. ```agda 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) ``` Conversely, a witness places `z` into the tower by `above`, and the transportation runs the other way along `q`. ## 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. The motive 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 uniqueness of recorded values is read off the induction rather than assumed. 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 approximation's value clause 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. ```agda 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 ``` The motive `Value u` says: for a constructible `u`, every entry of the table whose first component is `u` records the tower at `u`. The hypothesis that `u` is constructible is carried because the table's entries are carrier elements, whose first components are constructible sets; the induction will supply it from membership in an ordinal. ```agda 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) ``` The theorem runs the induction on the underlying set of `x`, the argument whose recorded value is in question. Membership induction is available in the hierarchy directly: to prove the motive of `u`, prove it of every member of `u`. The ordinality hypothesis on `a` is consumed inside the induction step. ```agda 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 ``` The induction step is `step-Lset` applied to the approximation's own step clause. The step is read at the environment extended by the value `z` and the argument `u`, so the three slots of the step shift back by two, which is what `sh2` accounts for. The conclusion is exactly the motive: the recorded `z` is the tower at `u`. ```agda where d : S d = u , hu u∈a : ⟨ u ∈ fst (lookup a γ) ⟩ u∈a = ApproxAt-dom f a γ h d z p ``` The value and the argument travel as carrier elements: `d` packages `u` with the constructibility `hu`. The approximation's domain clause certifies that `u` is below the argument `a`, which is what lets the induction reach this step at all. ```agda ou : IsOrd u ou = mem-ord {A = fst (lookup a γ)} oa u u∈a ``` Ordinality of `u` follows from ordinality of `a`, since `u` is a member of `a`; this is what the step will need about the argument it stands at. ```agda vals : Values (lookup f γ) u vals c y c∈ q = IH (fst c) c∈ (snd c) y q ``` Correctness below `u` is the induction hypothesis, used exactly as stated: for a member `c` of `u`, a recorded pair with first component `c` records the tower at `c`. The constructibility of `c` arrives with the induction, which supplies it from membership. ```agda 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)) ``` Completeness below `u` is where the approximation's value clause is spent. For `c` below `u`, transitivity inside the ordinal `a` gives `c` below `a`, and the approximation records some value there; the entry merely exists, and the elimination targets the proposition that the canonical entry is recorded. ```agda 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 ``` The merely-given recorded value is identified with the tower by the induction hypothesis, so after the transport the canonical entry is recorded, which is what completeness asks. ## The graph holds of nothing else The tower graph says that the value at a slot is the tower's value at the argument, and it says this through an approximation: there merely is an approximation whose step at the argument is that value. Unpacked, everything is already in hand. Correctness below the argument comes from the induction just completed; completeness below the argument comes from the approximation's value clause, transported by the same induction; and `step-Lset` applied one last time identifies the recorded value with the tower. The graph therefore **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 instantiations live in different concrete environments, and a statement made in one of them would have to be transported to the other through a satisfaction carrying the whole tower description inside it. ```agda 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 γ)) ``` The statement takes the satisfaction of the tower graph at the value and argument slots, the ordinality of the argument, and concludes that the recorded value is the tower. Nothing about the graph is assumed beyond its holding. ```agda Lset-only h ob = PT.rec (setIsSet (fst (lookup w γ)) (Lset (fst (lookup b γ)))) read (LsetGraph-out w b γ h) where ``` The graph unfolds to a mere witness: an approximation together with its satisfaction and its step at the value. The elimination is legitimate because the goal is an equality of two h-sets, hence a proposition; the witness itself is only ever needed inside that proposition. ```agda 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 ``` The witness hands over an approximation `f` on the argument, its satisfaction `ha`, and its step `hs` at the value. The step lemma is applied in the environment extended by `f`: the approximation occupies the new slot zero, while the value and the argument have moved up one place each. ```agda where vals : Values f (fst (lookup b γ)) vals c z _ p = approx-val zero (suc b) (f ∷ γ) ha ob c z p ``` Correctness for the step lemma is the induction of the previous section, applied to the approximation `ha`: every value that `f` records below the argument is the tower there. ```agda 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∈) ``` Completeness comes from the approximation's value clause: at each argument below, some entry is recorded, merely. The elimination targets the proposition that the canonical entry is recorded, so the missing witness is never needed. ```agda 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 ``` The merely-given recorded value is identified with the tower by the induction once more, and after the transport the canonical entry is exactly what is recorded. ## 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 tower graph by filling in the previous chapter's clauses and doing nothing else. The domain conjunct of the approximation is the equivalence between two ways of saying that an argument is in the domain, and `Domain` and `Entries` prove its two directions: an entry recorded at `c` puts `c` below the bound, and the canonical entry at `c` is recorded whenever `c` is below the bound. The step conjunct at a recorded pair `(c, y)` is `step-table` at `c`; the ordinal's transitivity restricts correctness and completeness of the table to the arguments below `c`, which is what the step lemma consumes there. The value the graph asks about is the step at the whole argument, and that again is `step-table`, at the identification of the recorded value with the tower. The statement takes a table `h`, the ordinality of the argument, the three conditions of the table on the argument, and the assertion that the recorded value is the tower. ```agda 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 γ)) ``` It concludes that the tower graph is satisfied at the value and argument slots. ```agda → ⟨ γ ⊨ 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 ``` The tower graph is introduced from an approximation and an outer step. The approximation is the table itself, placed in the extended environment; the outer step is `step-table` at the argument, for which correctness, completeness and the identification with the tower are exactly the hypotheses in hand. ```agda onDom : (c : S) → (⟨ ∃[ y ∶ S ] pr (fst c) (fst y) ∈ fst h ⟩ → ⟨ fst c ∈ fst (lookup b γ) ⟩) × (⟨ fst c ∈ fst (lookup b γ) ⟩ → ⟨ ∃[ y ∶ S ] pr (fst c) (fst y) ∈ fst h ⟩) ``` The approximation's domain clause is an equivalence between two ways of saying that `c` is in the domain: that some entry with first component `c` is recorded, and that `c` is below the argument. Both directions are needed, since the approximation's domain condition reads them in opposite orders. ```agda 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∈ ∣₁) ``` Reading the equivalence to the right: a recorded entry at `c`, together with completeness of the table, exhibits the canonical entry, which is the record of the stage at `c` presented as an element of `L`, with ordinality of `c` from that of the argument. Reading to the left: the domain condition of the table puts `c` below the argument. ```agda where named : Σ[ y ∈ S ] ⟨ pr (fst c) (fst y) ∈ fst h ⟩ → ⟨ fst c ∈ fst (lookup b γ) ⟩ named (y , p) = dom c y p ``` The auxiliary `named` is the domain condition read on the witness: an entry with first component `c` exists, so `c` is below the argument. Its content is one application of the table's third condition. ```agda 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) ``` The step conjunct is proved at each recorded pair `(c, y)`. In the environment extended by the value `y`, the argument `c` and the table `h`, the step condition relates the value slot to the argument slot through the table slot; `step-table` at `c` establishes exactly that, with the identification `fst y ≡ Lset (fst c)` supplied by correctness at the recorded pair. ```agda 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∈ ``` Two facts about `c` are read off the recorded pair. Its underlying set is below the argument, by the domain condition; and it is an ordinal, by the ordinality of the argument. ```agda 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∈) ``` Correctness and completeness below `c` are the table's own conditions, restricted to arguments below `c`: correctness restricts the domain hypothesis, and completeness uses the transitivity of the argument to see that an argument below `c` is below the argument. This is the second and last use of that transitivity in the chapter. ```agda approx : ⟨ (h ∷ γ) ⊨ ApproxAt zero (suc b) ⟩ approx = ApproxAt-in zero (suc b) (h ∷ γ) (domAt-intro zero (suc b) (h ∷ γ) onDom) onStep ``` Assembling the two conjuncts, the table itself is an approximation: its domain clause is the equivalence just proved, its step clause the one before. This is the sense in which a correct, complete table contains a recording of the hierarchy below the argument. ## The pair graph The table has to be **built**, and the only builder available inside `L` is replacement, which asks for a graph. Replacement collects the table after the functional-graph description: an entry of the table is the ordered pair of an argument `c` with a value `z`, and the graph holds of an entry when `z` satisfies the tower graph at `c`, with the carrier over which the tower ranges pinned to a constant. One existential binds the tower's value, the pair reader equates the entry with the pair of the argument and the bound value, 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 call site of this chapter. The frame is generic in the sentence: the readings speak of whatever formula is passed, under the assumption that it spells the pair graph. The equation travels with the sentence, so the readings are applied without further argument. ## The internal hierarchy `Recorded` names the class of pairs that the internal hierarchy at `α` is to collect: an argument `c` whose underlying set lies below `α`, together with the tower's value at `c`, and nothing besides. `IsHier` says that a set of the model realizes this class member for member: for every carrier element `z`, membership in the set holds exactly when `z` presents such a pair. Both directions of this statement are used. `HierOf` gathers a realizing set together with its specification, which is the form the construction builds and the form its two readings consume. The two readings stand at a **variable** realizing set reached by its specification, so that the construction to come can apply them to the set it is building. Reading out applies the injectivity of the hierarchy's pair to a member: an entry of the realizing set names an argument below `B` and the tower's value there. Reading in exhibits the canonical pair as an element of the model, which the model's own pairing supplies; it also needs ordinality of the argument, without which the tower's value could not be named 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 into a set of the model. Ordinality of each argument comes from `mem-ord`, and the functionality requirement is met through `mereFunct`, because the value at an argument is a construction. ```agda Recorded : V ℓ → V ℓ → hProp (ℓ-suc ℓ) Recorded B z = ∃[ c ∶ S ] (fst c ∈ B) ⊓ ((z ≡ pr (fst c) (Lset (fst c))) , setIsSet z (pr (fst c) (Lset (fst c)))) ``` `Recorded B z` is a proposition, and it says: for some carrier element `c` whose underlying set lies below `B`, the underlying set of `z` is the ordered pair of `fst c` with the tower's value at `c`. The equality of two h-sets is itself a proposition, so the join is a join of propositions. ```agda IsHier : V ℓ → S → Type (ℓ-suc (ℓ-suc ℓ)) IsHier B h = (z : S) → (fst z ∈ fst h) ≡ Recorded B (fst z) ``` `IsHier B h` says that the set presented by `h` realizes the recorded class member for member: at each `z`, membership in the set and being recorded are the same proposition. Neither direction is dropped, because each is used: membership without recordedness would let strangers in, recordedness without membership would leave pairs out. ```agda HierOf : V ℓ → Type (ℓ-suc (ℓ-suc ℓ)) HierOf B = Σ[ h ∈ S ] IsHier B h ``` `HierOf B` collects a realizing set with its specification. The pair is what the induction will build at each ordinal, and its two components answer the two questions one asks of a construction: what is it, and why does it qualify. ```agda module _ (B : V ℓ) (oB : IsOrd B) (h : S) (sp : IsHier B h) where ``` The two readings are stated for a variable realizing set with its specification, so that the construction to come can apply them to the set it is building, at whatever stage the induction currently stands. ```agda hier-out : (c z : S) → ⟨ pr (fst c) (fst z) ∈ fst h ⟩ → ⟨ fst c ∈ B ⟩ × (fst z ≡ Lset (fst c)) ``` Reading out: if the pair of `c` and `z` is a member of the realizing set, then `c` lies below `B` and `z` is the tower at `c`. Both conclusions follow from the specification applied at the member. ```agda hier-out c z p = PT.rec (isProp× (snd (fst c ∈ B)) (setIsSet (fst z) (Lset (fst c)))) read (subst ⟨_⟩ (sp k) p) where ``` The member's membership is transported along the specification into the recorded proposition, which is a truncated existence; the target of the elimination is a pair of propositions, hence a proposition, so the witness may be consumed here. ```agda k : S k = pr (fst c) (fst z) , isL-trans {x = fst h} {y = pr (fst c) (fst z)} p (h .snd) ``` The member itself must be named as a carrier element: the ordered pair of the underlying sets is constructible, because it belongs to the constructible set presented by `h`. ```agda 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∈ ``` The recorded proposition exhibits `d` below `B` with the member equal to the pair of `d` and the tower at `d`. Injectivity of the hierarchy's pair splits the equation: the first components identify `c` with `d`, which moves the membership into `c` being below `B`, and the second components identify `z` with the tower at `d`, which the first identification turns into the tower at `c`. ```agda , (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)) ∣₁) ``` Reading in: the canonical entry, the model's own pair of `c` with the tower at `c`, is a member. The specification says the recorded class is realized, the canonical pair is a witness of the recorded proposition with `c` itself as the argument, and the entry equals the model's pair by its defining reading. ```agda where oc : IsOrd (fst c) oc = mem-ord {A = B} oB (fst c) c∈ k : S k = prʟ c (LsetS (fst c) oc) ``` Ordinality of `c` comes from that of `B`, and with it the tower's value at `c` can be presented as an element of `L`, which is what the model's pair needs as its second component. ```agda opaque hierAt : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → HierOf α hierAt = ∈-induction {P = λ α → ⟨ isL α ⟩ → IsOrd α → HierOf α} (build (PairGraphAt zero (suc zero)) refl) where ``` The step function keeps the pair graph as a **variable sentence carrying its own equation**, rather than writing out the closed sentence it is instantiated to. The equation travels with the sentence, so every reading below is applied with `refl` at the call. ```agda build : (φ : Formula S 2) → φ ≡ PairGraphAt zero (suc zero) → (α : V ℓ) → ((δ : V ℓ) → ⟨ δ ∈ α ⟩ → ⟨ isL δ ⟩ → IsOrd δ → HierOf δ) → ⟨ isL α ⟩ → IsOrd α → HierOf α ``` The step receives the sentence with its equation, the ordinal `α`, its two certificates, and the induction hypothesis: the hierarchy is already built at every member of `α`. It must return the hierarchy at `α` with its specification. ```agda build φ qφ α IH hα oα = r .fst .fst , spec where A : S A = α , hα ``` The hierarchy at `α` is the first component of a realizer, extracted once replacement has produced it; `A` is `α` presented as a carrier element, the form in which replacement consumes a domain. ```agda 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 `α`, two auxiliary constructions name the data. The value at an argument `c` is the stage at `c`, an element of `L` by the stage presentation, with ordinality of `c` from that of `α`. The entry at `c` is the model's ordered pair of `c` with its value, the form the recorded class asks for. ```agda 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 ``` The tower graph is satisfied at the value recorded for a member `c` of `α`. This is where the induction hypothesis is spent: it hands over the hierarchy at `c`, a correct and complete table on the argument `c`, which is precisely what `graph-table` asks for. The environment carries the value, a fresh slot for the graph's own quantifier, and the argument. ```agda (λ 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 ``` The three table conditions are read off the specification of the hierarchy at `c`: correctness says every recorded value is the tower there, completeness says the canonical entries are recorded, and the domain condition says nothing else is recorded. The last argument, `refl`, is the pair graph's own equation. ```agda 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 ``` Ordinality of `c` comes from that of `α`, and with it the induction hypothesis delivers the hierarchy at `c`, constructible set and specification together. (holds) Every canonical entry satisfies the pair graph: the fiber over `c` is exhibited, with the bound tower value, the equation identifying the entry with the model's pair, and the satisfaction of the tower graph at the value and the argument. The witness is a member of the fiber, that is, of the type whose merely-existence the graph statement asserts. ```agda 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) Every other inhabitant of the graph at `c` equals the canonical entry. The graph unfolds to a tower value `z` with the tower graph satisfied at `(z, c)`; the tower graph determines its value, the pair's injectivity identifies the two entries, and the equation is the composition of these paths. ```agda 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) ``` The pair witness splits into the tower value `z` and the equation `q` identifying `k` with the pair of `c` and `z`. The carrier elements are equal once their underlying sets are, which is what `Σ≡Prop` reduces the goal to. ```agda where read : PairOf zero (suc zero) (k ∷ c ∷ []) φ qφ → k ≡ entry c c∈ read (z , (q , hg)) = Σ≡Prop (λ t → snd (isL t)) ( q ``` The tower graph at `(z, c)` determines the tower value: `z` is the tower at `c`, by `Lset-only` applied in the environment extended by the value, the canonical entry and the argument, with ordinality of `c` from that of `α`. ```agda ∙ 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∈)) ) ``` Composing the three paths, `k` is the pair of `c` and the tower at `c`, which is the canonical entry read through its own defining equation. (fc) Functionality at `c` is the contractible fiber that replacement asks for: the canonical entry inhabits the graph, and every inhabitant equals it. `mereFunct` assembles the two halves, presented merely, into exactly that contractible fiber. ```agda fc : (c : S) → ⟨ c ∈ˢ A ⟩ → isContr (Σ[ k ∈ S ] ⟨ (k ∷ c ∷ []) ⊨ φ ⟩) fc c c∈ = mereFunct φ c ∣ entry c c∈ , (holds c c∈ , only c c∈) ∣₁ ``` Replacement now collects the entries: over the arguments in `α`, the pairs of each argument with its uniquely determined value form a set of the model, presented with the assertion that it realizes exactly the class of those pairs. This is the moment the internal hierarchy at `α` exists as a set of `L`. ```agda r : isContr (SetOf (λ z → ∃[ c ∶ S ] (c ∈ˢ A) ⊓ ((z ∷ c ∷ []) ⊨ φ))) r = hasReplacementL A φ fc spec : IsHier α (r .fst .fst) spec z = ⇔toPath toRec fromRec where ``` It remains to verify that the collected set realizes the recorded class. The specification compares, member by member, membership in the collected set with being a recorded pair; both directions of the comparison are proved separately and joined into the pointwise equivalence. ```agda toRec : ⟨ fst z ∈ fst (r .fst .fst) ⟩ → ⟨ Recorded α (fst z) ⟩ toRec hz = PT.rec squash₁ conv (subst ⟨_⟩ (r .fst .snd z) hz) where ``` Reading the collected membership out: the replacement specification turns it into a member `c` of `α` whose value at `c` satisfies the pair graph. The elimination is legitimate because the recorded class is a proposition. ```agda 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∈)) ∣₁ ``` For the witness, uniqueness says the value recorded at `c` equals the canonical entry, and the canonical entry equals the model's pair of `c` with the tower at `c`; the underlying sets follow, which is exactly what being recorded asks. ```agda fromRec : ⟨ Recorded α (fst z) ⟩ → ⟨ fst z ∈ fst (r .fst .fst) ⟩ fromRec hz = subst ⟨_⟩ (sym (r .fst .snd z)) (PT.map conv hz) where ``` Reading in: a recorded pair exhibits an argument below `α` with the tower value at it; the pair graph is satisfied at the canonical entry of that argument, and the collected set contains it. ```agda conv : Σ[ c ∈ S ] (⟨ fst c ∈ α ⟩ × (fst z ≡ pr (fst c) (Lset (fst c)))) → Σ[ c ∈ S ] (⟨ fst c ∈ α ⟩ × ⟨ (z ∷ c ∷ []) ⊨ φ ⟩) ``` The witness converts from the recorded presentation to the graph presentation: the argument stays, and the equality of the underlying set with the canonical pair becomes satisfaction of the pair graph at it. ```agda 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)) ``` The equality says `z` presents the same set as the canonical entry of `c`; the pair elements are therefore equal, and `holds` transported along that path gives satisfaction of the pair graph at `z` and `c`. ```agda (eq ∙ sym (prʟ-fst c (value c c∈))) hierL : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → S hierL α hα oα = hierAt α hα oα .fst ``` The internal hierarchy at an ordinal is the realizing set of the induction, presented as an element of `L`. It exists for every constructible ordinal, which is to say: the model now contains, for each of its ordinals, a set whose members are exactly the pairs of an ordinal below it with the tower's value there. ```agda hierL-spec : (α : V ℓ) (hα : ⟨ isL α ⟩) (oα : IsOrd α) → IsHier α (hierL α hα oα) hierL-spec α hα oα = hierAt α hα oα .snd ``` The specification travels with the construction: the realizing set delivered by the induction satisfies `IsHier` at its ordinal, in both directions. This is the account against which every later use of the internal hierarchy is checked. ## The tower satisfies the graph The internal hierarchy was built with `graph-table` and `Lset-only`: at each ordinal, the induction hypothesis provided the table below, and the two lemmas turned it into a satisfied graph with a unique value. The last statement now runs the other way. The specification `hierL-spec` hands over the table conditions on the argument, and `Lset-defines` feeds them to `graph-table`: the tower graph is satisfied at the recorded value, and `Lset-only` beside it says nothing else is. The internal graph and the meta tower therefore agree in both directions at every constructible ordinal. ```agda 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 ⟩ ``` The statement takes the ordinality of the argument and the assertion that the recorded value is the tower at it, and concludes that the tower graph is satisfied. It is the reading-in direction of the previous section, available at every constructible ordinal because the internal hierarchy exists at each of them. ```agda 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 ``` The set named here is the internal hierarchy at the argument, and its specification is read as the three table conditions. Correctness and completeness are the two directions of `hier-out`: an entry of the internal table has its argument below and its value the tower there, and the canonical entry is recorded at every argument below. The domain condition is `hier-in`'s counterpart: only such pairs are recorded. The proof names the internal hierarchy at the argument and reads its specification in both directions. Correctness says every value the internal table records below the argument is the tower there; completeness says the canonical entries are recorded; the domain condition closes the table; and the final hypothesis `q` identifies the recorded value with the tower. The four inputs are exactly what `graph-table` consumes. ```agda 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 ``` The internal hierarchy at the argument exists because the argument is a constructible ordinal, and its specification is exactly the membership equivalence proved by the induction. The two facts together say that the tower is recorded inside the model, at every stage, with nothing besides. ## Recap `approx-val` proves, by one membership induction on the argument, that every value an approximation records equals the meta tower's value at that argument, with no single-valuedness hypothesis anywhere; equality of two values recorded at one argument is read off it directly. `Lset-only` and `Lset-defines` are the graph's two directions against the tower, and the second is what `hierL` is built from: the internal hierarchy at an ordinal, an element of `L` whose members are exactly the pairs of an ordinal below it with the tower's value at it, specified by the membership equivalence proved by the induction. The stages tabulated here are indexed by ordinals, which are sets of the hierarchy; the universe levels of the host are size indices of types and never index the tower.