BedrockThe constructible hierarchy inside L
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapA 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.
{-# 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
→ ⟨ γ ⊨ 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
, (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.
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.
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.
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.
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.
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.
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.
(λ 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.
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.
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.
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.
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 α.
∙ 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.
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.
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.
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.
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.
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.
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.
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.
(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.
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.
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.
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.
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.