BedrockThe order, internalized as a set
The previous chapter wrote the order down in the object language; this chapter turns the description into an object. A formula is not something the model can quantify over, and the choosing ahead needs a relation it can quantify over: a set of ordered pairs, living inside L, whose members are exactly the pairs the order relates. That set is what this chapter builds, one at every ordinal.
The shape is the hierarchy chapter's, followed closely, because the problem is the same problem. A recursion whose values are sets cannot be named by a graph, so what is described instead is an approximation: a table recording, at each ordinal below its domain, the relation there. A graph quantifies over approximations; a value lemma pins every value an approximation records; and replacement inside L collects the table, with the functionality obligation filled through
mereFunct, because the value at an ordinal is a construction and not a decision.
One thing here is not the hierarchy chapter's, and it is why this chapter needs two constructions rather than one. The tower has a meta-language term, Lset, so the hierarchy's induction could always exhibit the value it was about to record. The order at a stage has no such term: the set of related pairs is exactly what is being built. So the induction carries two things at once, the table below an ordinal and the relation at it, and the second is cut out by the model's own separation from a bound the pairs cannot escape.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Choice.Table {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; _∧̇_; _⇒̇_; ∃̇_; ∀̇_ ) import FOL.Absoluteness import FOL.ZFModel open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction ) open import V.Coding {ℓ} using ( pr; pr-inj ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd; isPropIsOrd ) open import L.Ordinal {ℓ} using ( mem-ord ) open import L.Axioms.Basic {ℓ} using ( extensionalL ) open import L.Axioms.Full {ℓ} lem using ( hasReplacementL; hasSeparationL ) open import L.Recursion {ℓ} lem using ( mereFunct; smallDom ) open import L.Coding.Model {ℓ} using ( extAt; extAt-in; extAt-out; extAt-in-both; appAt; appAt-adequate ; domAt; domAt-in; domAt-out; domAt-intro ; prAtL; prAtL-adequate; prʟ; prʟ-fst ) open import L.Choice.Step {ℓ} lem using ( Mem; relOf; orderAt; memOf; carry ) open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; Tri; lt; eq; gt ) open import Cubical.Data.Sigma using ( Σ≡Prop; _×_ ) open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ ) open import Cubical.Foundations.Prelude using ( subst2 ) open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module ModelL = FOL.ZFModel 𝒮ʟ open ModelL using ( SetOf ) module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ) private sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i)
The comparison, read back whole
A class of the model is a proposition-valued predicate, and the comparison at a stage is not known to be proposition-valued: it is a sum of two keys, and nothing so far says a set comes before another in only one way. So the class below carries the comparison truncated, and the truncation has to come off again, since the naming chapter's consumers take an honest comparison.
It comes off for free, and for a reason that belongs to every strict well-order rather than to this one. Split on trichotomy first: in the strict case the comparison is already in hand and no truncation is eliminated at all; in the other two cases the goal is absurdity, which is a proposition, so the truncation may be opened there. Irreflexivity closes the equal case and transitivity the reversed one. Two lines of mathematics, and the truncation never has to be avoided anywhere else in the chapter.
Ordering : (α : V ℓ) → IsOrd α → Mem (Lset α) → Mem (Lset α) → Ω Ordering α oα a b = ∥ relOf (orderAt α oα) a b ∥₁ , squash₁ strict : (α : V ℓ) (oα : IsOrd α) (a b : Mem (Lset α)) → ⟨ Ordering α oα a b ⟩ → relOf (orderAt α oα) a b strict α oα a b h = decide (SWO.tri∙ W a b) where W = orderAt α oα decide : Tri (relOf W a b) (a ≡ b) (relOf W b a) → relOf W a b decide (lt k) = k decide (eq q) = Empty.rec (PT.rec Empty.isProp⊥ (λ k → SWO.irr∙ W a (subst (relOf W a) (sym q) k)) h) decide (gt k) = Empty.rec (PT.rec Empty.isProp⊥ (λ j → SWO.irr∙ W a (SWO.trans∙ W a b a j k)) h)
What the relation at a stage is
Related is the class the object realizes: the ordered pairs of two members of the stage that the order there relates. Ordinality is bound inside the class rather than carried beside it, so nothing below ever transports a comparison along a proof that an ordinal is one; the one place a chosen proof is wanted, the reading, moves it in a single subst, because being an ordinal is a proposition.
Realizes says a set of the model realizes that class, member for member, and it is written as an indexed conjunction of two implications rather than as a pointwise equality of propositions. That is a level constraint and not a preference: an equality of propositions lives one universe above the propositions themselves, and this statement has to be a proposition of the model, because the table records it. The two forms are interchangeable, and where an equality is wanted ⇔toPath supplies it.
Related : V ℓ → V ℓ → Ω Related α z = ⋁ (IsOrd α) (λ oα → ⋁ (Mem (Lset α)) (λ a → ⋁ (Mem (Lset α)) (λ b → ((z ≡ pr (fst a) (fst b)) , setIsSet z (pr (fst a) (fst b))) ⊓ Ordering α oα a b))) Realizes : V ℓ → S → Ω Realizes α r = ⋀ S (λ z → ((fst z ∈ fst r) ⇒ Related α (fst z)) ⊓ (Related α (fst z) ⇒ (fst z ∈ fst r))) IsRel : V ℓ → S → Type (ℓ-suc ℓ) IsRel α r = ⟨ Realizes α r ⟩ rel-path : (α : V ℓ) (r : S) → IsRel α r → (z : S) → (fst z ∈ fst r) ≡ Related α (fst z) rel-path α r p z = ⇔toPath {P = fst z ∈ fst r} {Q = Related α (fst z)} (p z .fst) (p z .snd) rel-unique : (α : V ℓ) (r r' : S) → IsRel α r → IsRel α r' → r ≡ r' rel-unique α r r' p q = extensionalL (λ z → rel-path α r p z ∙ sym (rel-path α r' q z)) module _ (α : V ℓ) (oα : IsOrd α) (a b : Mem (Lset α)) where related-in : relOf (orderAt α oα) a b → ⟨ Related α (pr (fst a) (fst b)) ⟩ related-in h = ∣ oα , ∣ a , ∣ b , (refl , ∣ h ∣₁) ∣₁ ∣₁ ∣₁ related-out : ⟨ Related α (pr (fst a) (fst b)) ⟩ → relOf (orderAt α oα) a b related-out h = strict α oα a b (PT.rec squash₁ atOrd h) where atPair : (o : IsOrd α) (a' b' : Mem (Lset α)) → (pr (fst a) (fst b) ≡ pr (fst a') (fst b')) → ⟨ Ordering α o a' b' ⟩ → ⟨ Ordering α oα a b ⟩ atPair o a' b' q = PT.map (λ k → subst2 (relOf (orderAt α oα)) (sym ea) (sym eb) (subst (λ o' → relOf (orderAt α o') a' b') (isPropIsOrd α o oα) k)) where ea : a ≡ a' ea = Σ≡Prop (λ x → snd (x ∈ Lset α)) (pr-inj q .fst) eb : b ≡ b' eb = Σ≡Prop (λ x → snd (x ∈ Lset α)) (pr-inj q .snd) atOrd : Σ[ o ∈ IsOrd α ] ⟨ ⋁ (Mem (Lset α)) (λ a' → ⋁ (Mem (Lset α)) (λ b' → ((pr (fst a) (fst b) ≡ pr (fst a') (fst b')) , setIsSet _ (pr (fst a') (fst b'))) ⊓ Ordering α o a' b')) ⟩ → ⟨ Ordering α oα a b ⟩ atOrd (o , h₁) = PT.rec squash₁ (λ { (a' , h₂) → PT.rec squash₁ (λ { (b' , (q , hr)) → atPair o a' b' q hr }) h₂ }) h₁
Whatever realizes the class, read at both shapes
The two readings a consumer wants are membership in a set that realizes the class, and they are stated of any such set rather than of the one this chapter builds. That is not generality for its own sake. The set the naming machinery must be handed is the relation at the stage below the one being built, and inside the construction that set arrives from the table, as a value with the hypothesis that it realizes the class there; whereas the set this chapter finally returns exists only after the construction is finished. Stated of any realizing set, the two readings are available a stage earlier than the construction, and that is exactly where they are wanted.
Both are two lines. A member of a stage reaches the model as a pair with its constructibility proof, Related is read at the pair the model builds rather than at the meta pair, and one congruence along prʟ-fst moves between them.
module _ (α : V ℓ) (oα : IsOrd α) (r : S) (hr : IsRel α r) where private memL : Mem (Lset α) → S memL c = fst c , Lset→isL α oα (fst c) (snd c) atRel : (a b : Mem (Lset α)) → (fst (prʟ (memL a) (memL b)) ∈ fst r) ≡ (pr (fst a) (fst b) ∈ fst r) atRel a b = cong (λ x → x ∈ fst r) (prʟ-fst (memL a) (memL b)) atRelated : (a b : Mem (Lset α)) → ⟨ Related α (fst (prʟ (memL a) (memL b))) ⟩ ≡ ⟨ Related α (pr (fst a) (fst b)) ⟩ atRelated a b = cong (λ x → ⟨ Related α x ⟩) (prʟ-fst (memL a) (memL b)) rel-fill : (a b : Mem (Lset α)) → relOf (orderAt α oα) a b → ⟨ pr (fst a) (fst b) ∈ fst r ⟩ rel-fill a b h = subst ⟨_⟩ (atRel a b) (hr (prʟ (memL a) (memL b)) .snd (transport (sym (atRelated a b)) (related-in α oα a b h))) rel-rep : (a b : Mem (Lset α)) → ⟨ pr (fst a) (fst b) ∈ fst r ⟩ → relOf (orderAt α oα) a b rel-rep a b h = related-out α oα a b (transport (atRelated a b) (hr (prʟ (memL a) (memL b)) .fst (subst ⟨_⟩ (sym (atRel a b)) h))) private atIx : ⟪ Lset α ⟫ → Mem (Lset α) atIx m = ⟪ Lset α ⟫↪ m , memOf (Lset α) m open SWO (carry (Lset α) (orderAt α oα)) using () renaming ( _<∙_ to _≺ᶜ_ ) ixRel-fill : (u v : ⟪ Lset α ⟫) → u ≺ᶜ v → ⟨ pr (⟪ Lset α ⟫↪ u) (⟪ Lset α ⟫↪ v) ∈ fst r ⟩ ixRel-fill u v = rel-fill (atIx u) (atIx v) ixRel-rep : (u v : ⟪ Lset α ⟫) → ⟨ pr (⟪ Lset α ⟫↪ u) (⟪ Lset α ⟫↪ v) ∈ fst r ⟩ → u ≺ᶜ v ixRel-rep u v = rel-rep (atIx u) (atIx v)
What a table records
Three conditions, one line each, and they are kept apart for the reason the hierarchy chapter kept its own apart: the two consumers need different subsets of them. Values says a value recorded below B realizes the relation there.
Entries says every argument below B has some value recorded at it, and merely so, which is all the step ever asks. Domain says nothing outside B is recorded, which the induction on an approximation cannot have and the finished table does.
Values : S → V ℓ → Type (ℓ-suc ℓ) Values h B = (c r : S) → ⟨ fst c ∈ B ⟩ → ⟨ pr (fst c) (fst r) ∈ fst h ⟩ → IsRel (fst c) r Entries : S → V ℓ → Type (ℓ-suc ℓ) Entries h B = (c : S) → ⟨ fst c ∈ B ⟩ → ∥ (Σ[ r ∈ S ] ⟨ pr (fst c) (fst r) ∈ fst h ⟩) ∥₁ Domain : S → V ℓ → Type (ℓ-suc ℓ) Domain h B = (c r : S) → ⟨ pr (fst c) (fst r) ∈ fst h ⟩ → ⟨ fst c ∈ B ⟩
The step, as a parameter
The step at an ordinal says which pairs the relation there holds, given the table below. Everything after this section is generic in that condition, which enters as a parameter in two forms with one meaning: at slots, because the graph must bind the table it consults, and at constants, because separation carves with a formula of one free variable and the table it consults is, at the moment of carving, a definite element of the model. The meaning is the hypothesis, stated once for each form: at a correct and complete table below an ordinal, the condition holds of a set exactly when that set is a pair the order there relates.
That is the whole of what the description owes, and naming it is deliberate. It is also more than one chapter's worth, and understating it would cost the next author the discovery. The previous chapter's StepAt is one part of what fills it, and only one: it describes a single successor step over the new members, while the condition here must describe orderAt at every ordinal, and that family is birth-primary, with the step entering only as the secondary key at a shared birth. So filling this needs three things and not one:
StepAt's own adequacy against the meta step, which is unproved; the birth described in the object language, which nothing describes yet; and the code set at a carrier that moves with the birth. What this chapter proves is that given it, the relation at every stage is an element of L whose members are exactly the right pairs.
The step itself is one extAt, for the reason every set-valued clause on this route is one: a value is the set of exactly the things meeting a condition, and writing that as a pair of inclusions would say the condition twice.
module Described (Cond : ∀ {n} → Fin n → Fin n → Formula S (suc n)) (Cond₀ : S → S → Formula S 1) (cond-spec : ∀ {n} (b f : Fin n) (γ : S ^ n) → IsOrd (fst (lookup b γ)) → Values (lookup f γ) (fst (lookup b γ)) → Entries (lookup f γ) (fst (lookup b γ)) → (z : S) → ((z ∷ γ) ⊨ Cond b f) ≡ Related (fst (lookup b γ)) (fst z)) (cond₀-spec : (b f : S) → IsOrd (fst b) → Values f (fst b) → Entries f (fst b) → (z : S) → ((z ∷ []) ⊨ Cond₀ b f) ≡ Related (fst b) (fst z)) where StepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n StepAt v b f = extAt v (Cond b f) module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) (ob : IsOrd (fst (lookup b γ))) (vals : Values (lookup f γ) (fst (lookup b γ))) (ents : Entries (lookup f γ) (fst (lookup b γ))) where private same : (z : S) → ((z ∷ γ) ⊨ Cond b f) ≡ Related (fst (lookup b γ)) (fst z) same = cond-spec b f γ ob vals ents step-rel : ⟨ γ ⊨ StepAt v b f ⟩ → IsRel (fst (lookup b γ)) (lookup v γ) step-rel h z = (λ hz → subst ⟨_⟩ (same z) (extAt-out v (Cond b f) γ h z hz)) , (λ hz → extAt-in v (Cond b f) γ h z (subst ⟨_⟩ (sym (same z)) hz)) step-table : IsRel (fst (lookup b γ)) (lookup v γ) → ⟨ γ ⊨ StepAt v b f ⟩ step-table sp = extAt-in-both v (Cond b f) γ (λ z hz → subst ⟨_⟩ (sym (same z)) (sp z .fst hz)) (λ z h → sp z .snd (subst ⟨_⟩ (same z) h))
Approximations and the graph
Two conjuncts and no third: the table is defined on the argument, and every value it records is the step at that argument from the table itself. The pair is a membership equivalence, which is what makes the existence claim below a proposition; single-valuedness is not a conjunct, because it is a corollary, and the corollary is collected two sections down.
The graph binds the table, and it has to: a graph may not name the object it defines, and the tower of relations is defined here. The value stands at the first slot and the argument at the second, which is the order the model's replacement field reads a graph in.
ApproxAt : ∀ {n} → Fin n → Fin n → Formula S n ApproxAt f a = domAt f a ∧̇ ∀̇ (∀̇ ( appAt (sh2 f) (suc zero) zero ⇒̇ StepAt zero (suc zero) (sh2 f) )) GraphAt : ∀ {n} → Fin n → Fin n → Formula S n GraphAt w b = ∃̇ (ApproxAt zero (suc b) ∧̇ StepAt (suc w) (suc b) zero) module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) where ApproxAt-dom : ⟨ γ ⊨ ApproxAt f a ⟩ → Domain (lookup f γ) (fst (lookup a γ)) ApproxAt-dom h = domAt-out f a γ (h .fst) ApproxAt-value : ⟨ γ ⊨ ApproxAt f a ⟩ → Entries (lookup f γ) (fst (lookup a γ)) ApproxAt-value h = domAt-in f a γ (h .fst) ApproxAt-step : ⟨ γ ⊨ ApproxAt f a ⟩ → (c r : S) → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩ → ⟨ (r ∷ c ∷ γ) ⊨ StepAt zero (suc zero) (sh2 f) ⟩ ApproxAt-step h c r p = h .snd c r (subst ⟨_⟩ (sym (appAt-adequate (sh2 f) (suc zero) zero (r ∷ c ∷ γ))) p) ApproxAt-in : ⟨ γ ⊨ domAt f a ⟩ → ((c r : S) → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩ → ⟨ (r ∷ c ∷ γ) ⊨ StepAt zero (suc zero) (sh2 f) ⟩) → ⟨ γ ⊨ ApproxAt f a ⟩ ApproxAt-in hd hs = hd , λ c r p → hs c r (subst ⟨_⟩ (appAt-adequate (sh2 f) (suc zero) zero (r ∷ c ∷ γ)) p) module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where GraphOf : Type (ℓ-suc ℓ) GraphOf = Σ[ f ∈ S ] ( ⟨ (f ∷ γ) ⊨ ApproxAt zero (suc b) ⟩ × ⟨ (f ∷ γ) ⊨ StepAt (suc w) (suc b) zero ⟩ ) Graph-in : (f : S) → ⟨ (f ∷ γ) ⊨ ApproxAt zero (suc b) ⟩ → ⟨ (f ∷ γ) ⊨ StepAt (suc w) (suc b) zero ⟩ → ⟨ γ ⊨ GraphAt w b ⟩ Graph-in f ha hs = ∣ f , (ha , hs) ∣₁ Graph-out : ⟨ γ ⊨ GraphAt w b ⟩ → ∥ GraphOf ∥₁ Graph-out h = h
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 realizes the relation there. It quantifies over all recorded values, and that is why single-valuedness is nowhere a hypothesis: two values recorded at one argument realize one class, so extensionality in L makes them equal, and approx-uniq is those three lines.
The step of the induction is the step condition read at the recorded value. Correctness below the argument is the induction hypothesis, verbatim. Completeness below the argument is where the domain hypothesis is spent: an argument below this one is below the approximation's domain, because the domain is an ordinal and ordinals are transitive, so the approximation has a value there.
module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) where private Value : V ℓ → Type (ℓ-suc ℓ) Value u = ⟨ isL u ⟩ → IsOrd u → (r : S) → ⟨ pr u (fst r) ∈ fst (lookup f γ) ⟩ → IsRel u r approx-val : ⟨ γ ⊨ ApproxAt f a ⟩ → IsOrd (fst (lookup a γ)) → (c : S) → IsOrd (fst c) → (r : S) → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst c) r approx-val h oa c = ∈-induction {P = Value} go (fst c) (snd c) where go : (u : V ℓ) → ((t : V ℓ) → ⟨ t ∈ u ⟩ → Value t) → Value u go u IH hu ou r p = step-rel zero (suc zero) (sh2 f) (r ∷ d ∷ γ) ou vals ents (ApproxAt-step f a γ h d r p) where d : S d = u , hu u∈a : ⟨ u ∈ fst (lookup a γ) ⟩ u∈a = ApproxAt-dom f a γ h d r p vals : Values (lookup f γ) u vals e t e∈ q = IH (fst e) e∈ (snd e) (mem-ord {A = u} ou (fst e) e∈) t q ents : Entries (lookup f γ) u ents e e∈ = ApproxAt-value f a γ h e (oa .fst {x = u} {y = fst e} e∈ u∈a) approx-uniq : ⟨ γ ⊨ ApproxAt f a ⟩ → IsOrd (fst (lookup a γ)) → (c r r' : S) → IsOrd (fst c) → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩ → ⟨ pr (fst c) (fst r') ∈ fst (lookup f γ) ⟩ → r ≡ r' approx-uniq h oa c r r' oc p q = rel-unique (fst c) r r' (approx-val h oa c oc r p) (approx-val h oa c oc r' q)
The graph holds of nothing else
Read the graph and everything is already in hand: unpack the approximation, take correctness from approx-val, take completeness from the approximation's own domain projection, and read the step once more. The conclusion is that the graph determines its value, and the converse is a table: a correct, complete, bounded table satisfies the graph, because it satisfies both conjuncts of "is an approximation" and the outer step as well.
Both readings stand at variable slots, and that is not decoration. Their consumers instantiate them at two different concrete environments, and a statement made at either would have to be converted to the other through a satisfaction carrying the whole description inside it.
module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where graph-only : ⟨ γ ⊨ GraphAt w b ⟩ → IsOrd (fst (lookup b γ)) → IsRel (fst (lookup b γ)) (lookup w γ) graph-only h ob = PT.rec (snd (Realizes (fst (lookup b γ)) (lookup w γ))) read (Graph-out w b γ h) where read : GraphOf w b γ → IsRel (fst (lookup b γ)) (lookup w γ) read (f , (ha , hs)) = step-rel (suc w) (suc b) zero (f ∷ γ) ob vals ents hs where vals : Values f (fst (lookup b γ)) vals c r c∈ p = approx-val zero (suc b) (f ∷ γ) ha ob c (mem-ord {A = fst (lookup b γ)} ob (fst c) c∈) r p ents : Entries f (fst (lookup b γ)) ents = ApproxAt-value zero (suc b) (f ∷ γ) ha graph-table : (h : S) → IsOrd (fst (lookup b γ)) → Values h (fst (lookup b γ)) → Entries h (fst (lookup b γ)) → Domain h (fst (lookup b γ)) → IsRel (fst (lookup b γ)) (lookup w γ) → ⟨ γ ⊨ GraphAt w b ⟩ graph-table h ob vals ents dom sp = Graph-in w b γ h approx (step-table (suc w) (suc b) zero (h ∷ γ) ob vals ents sp) where onDom : (c : S) → (⟨ ⋁ S (λ r → pr (fst c) (fst r) ∈ fst h) ⟩ → ⟨ fst c ∈ fst (lookup b γ) ⟩) × (⟨ fst c ∈ fst (lookup b γ) ⟩ → ⟨ ⋁ S (λ r → pr (fst c) (fst r) ∈ fst h) ⟩) onDom c = (λ hr → PT.rec (snd (fst c ∈ fst (lookup b γ))) (λ { (r , p) → dom c r p }) hr) , ents c onStep : (c r : S) → ⟨ pr (fst c) (fst r) ∈ fst h ⟩ → ⟨ (r ∷ c ∷ h ∷ γ) ⊨ StepAt zero (suc zero) (suc (suc zero)) ⟩ onStep c r p = step-table zero (suc zero) (suc (suc zero)) (r ∷ c ∷ h ∷ γ) oc vals' ents' (vals c r c∈ p) where c∈ : ⟨ fst c ∈ fst (lookup b γ) ⟩ c∈ = dom c r p oc : IsOrd (fst c) oc = mem-ord {A = fst (lookup b γ)} ob (fst c) c∈ vals' : Values h (fst c) vals' e t _ q = vals e t (dom e t q) q ents' : Entries h (fst c) ents' e e∈ = ents e (ob .fst {x = fst c} {y = fst e} e∈ c∈) approx : ⟨ (h ∷ γ) ⊨ ApproxAt zero (suc b) ⟩ approx = ApproxAt-in zero (suc b) (h ∷ γ) (domAt-intro zero (suc b) (h ∷ γ) onDom) onStep
The pair graph
The table has to be built, and the only builder is replacement, which asks for a graph. This is that graph, packaged: the value at an argument is the ordered pair of the argument with the relation there. Its two readings take the sentence as a parameter, with the sentence's own equation as a hypothesis, refl at the single call site. That is the shape rule the hierarchy chapter measured at eighty-five seconds, met here again: written directly against the closed sentence, Agda decides the equality of two spellings of one formula by normalizing a satisfaction that carries the entire description inside it.
PairGraphAt : ∀ {n} → Fin n → Fin n → Formula S n PairGraphAt e c = ∃̇ (prAtL (suc e) (suc c) zero ∧̇ GraphAt zero (suc c)) module _ {n : ℕ} (e c : Fin n) (γ : S ^ n) (φ : Formula S n) (qφ : φ ≡ PairGraphAt e c) where PairOf : Type (ℓ-suc ℓ) PairOf = Σ[ r ∈ S ] ( (fst (lookup e γ) ≡ pr (fst (lookup c γ)) (fst r)) × ⟨ (r ∷ γ) ⊨ GraphAt zero (suc c) ⟩ ) PairGraph-in : (r : S) → fst (lookup e γ) ≡ pr (fst (lookup c γ)) (fst r) → ⟨ (r ∷ γ) ⊨ GraphAt zero (suc c) ⟩ → ⟨ γ ⊨ φ ⟩ PairGraph-in r q hg = subst (λ ψ → ⟨ γ ⊨ ψ ⟩) (sym qφ) ∣ r , (subst ⟨_⟩ (sym (prAtL-adequate (suc e) (suc c) zero (r ∷ γ))) q , hg) ∣₁ PairGraph-out : ⟨ γ ⊨ φ ⟩ → ∥ PairOf ∥₁ PairGraph-out h = PT.map (λ { (r , (hq , hg)) → r , (subst ⟨_⟩ (prAtL-adequate (suc e) (suc c) zero (r ∷ γ)) hq , hg) }) (subst (λ ψ → ⟨ γ ⊨ ψ ⟩) qφ h)
The table, and the relation at the bound
Recorded names the class the table realizes: the pairs of an ordinal below B with the relation there, and nothing besides. IsTable says a set of the model realizes it, member for member, and that is a membership equivalence for the reason the hierarchy chapter recorded: said one way it would not say the table holds only such pairs, the existence claim would not be a proposition, and the induction's motive would not be either.
Bundle is what the induction carries, and its second component is what this chapter has that the hierarchy chapter did not need: the relation at the ordinal, not merely below it. Both components are unique, the table by extensionality against the class it realizes and the relation by
rel-unique, so the bundle is a proposition and the induction may be run against it.
The construction is one membership induction. At α the pair graph is functional at every argument below: the induction hypothesis hands over both the table up to that argument and the relation at it, graph-table turns the pair into a satisfaction of the graph, and graph-only says nothing else satisfies it. Replacement collects the pairs. Then the relation at α itself is separated out of a bound, and the bound is the one thing here that is not the hierarchy chapter's: the pairs of two members of a stage are a small family of elements of L, indexed by the stage's own index type twice over, so one appeal to
smallDom confines all of them at once. Ordinality of each argument is taken from mem-ord untruncated, and the whole construction is sealed where it is built.
Recorded : V ℓ → V ℓ → Ω Recorded B z = ⋁ S (λ c → (fst c ∈ B) ⊓ ⋁ S (λ r → ((z ≡ pr (fst c) (fst r)) , setIsSet z (pr (fst c) (fst r))) ⊓ Realizes (fst c) r)) IsTable : V ℓ → S → Type (ℓ-suc (ℓ-suc ℓ)) IsTable B h = (z : S) → (fst z ∈ fst h) ≡ Recorded B (fst z) Bundle : V ℓ → Type (ℓ-suc (ℓ-suc ℓ)) Bundle α = Σ[ h ∈ S ] Σ[ r ∈ S ] (IsTable α h × IsRel α r) isPropBundle : (α : V ℓ) → isProp (Bundle α) isPropBundle α (h , u) (h' , u') = Σ≡Prop inner (extensionalL (λ z → u .snd .fst z ∙ sym (u' .snd .fst z))) where inner : (k : S) → isProp (Σ[ r ∈ S ] (IsTable α k × IsRel α r)) inner k (r , t) (r' , t') = Σ≡Prop (λ s → isProp× (isPropΠ (λ z → isSetHProp (fst z ∈ fst k) (Recorded α (fst z)))) (snd (Realizes α s))) (rel-unique α r r' (t .snd) (t' .snd)) module _ (B : V ℓ) (oB : IsOrd B) (h : S) (sp : IsTable B h) where private atPair : (c r : S) → (pr (fst c) (fst r) ∈ fst h) ≡ Recorded B (pr (fst c) (fst r)) atPair c r = subst (λ x → (x ∈ fst h) ≡ Recorded B x) (prʟ-fst c r) (sp (prʟ c r)) table-out : Domain h B × Values h B table-out = (λ c r p → read c r p .fst) , (λ c r _ p → read c r p .snd) where read : (c r : S) → ⟨ pr (fst c) (fst r) ∈ fst h ⟩ → ⟨ fst c ∈ B ⟩ × IsRel (fst c) r read c r p = PT.rec isPropBoth outer (subst ⟨_⟩ (atPair c r) p) where isPropBoth : isProp (⟨ fst c ∈ B ⟩ × IsRel (fst c) r) isPropBoth = isProp× (snd (fst c ∈ B)) (snd (Realizes (fst c) r)) inner : (d t : S) → ⟨ fst d ∈ B ⟩ → (pr (fst c) (fst r) ≡ pr (fst d) (fst t)) → IsRel (fst d) t → ⟨ fst c ∈ B ⟩ × IsRel (fst c) r inner d t d∈ q hr = subst (λ x → ⟨ x ∈ B ⟩) (sym (pr-inj q .fst)) d∈ , subst2 IsRel (sym (pr-inj q .fst)) (sym rt) hr where rt : r ≡ t rt = Σ≡Prop (λ x → snd (isL x)) (pr-inj q .snd) outer : Σ[ d ∈ S ] ( ⟨ fst d ∈ B ⟩ × ⟨ ⋁ S (λ t → ((pr (fst c) (fst r) ≡ pr (fst d) (fst t)) , setIsSet _ (pr (fst d) (fst t))) ⊓ Realizes (fst d) t) ⟩ ) → ⟨ fst c ∈ B ⟩ × IsRel (fst c) r outer (d , (d∈ , hs)) = PT.rec isPropBoth (λ { (t , (q , hr)) → inner d t d∈ q hr }) hs table-in : (c r : S) → ⟨ fst c ∈ B ⟩ → IsRel (fst c) r → ⟨ pr (fst c) (fst r) ∈ fst h ⟩ table-in c r c∈ hr = subst ⟨_⟩ (sym (atPair c r)) ∣ c , (c∈ , ∣ r , (refl , hr) ∣₁) ∣₁ bound : (α : V ℓ) (oα : IsOrd α) → Σ[ D ∈ S ] ((z : S) → ⟨ Related α (fst z) ⟩ → ⟨ fst z ∈ fst D ⟩) bound α oα = d .fst , confine where ixL : ⟪ Lset α ⟫ → S ixL m = ⟪ Lset α ⟫↪ m , Lset→isL α oα (⟪ Lset α ⟫↪ m) (memOf (Lset α) m) d : Σ[ D ∈ S ] ((p : ⟪ Lset α ⟫ × ⟪ Lset α ⟫) → ⟨ prʟ (ixL (fst p)) (ixL (snd p)) ∈ˢ D ⟩) d = smallDom (⟪ Lset α ⟫ × ⟪ Lset α ⟫) (λ p → prʟ (ixL (fst p)) (ixL (snd p))) onPair : (a b : Mem (Lset α)) → ⟨ pr (fst a) (fst b) ∈ fst (d .fst) ⟩ onPair a b = subst (λ x → ⟨ x ∈ fst (d .fst) ⟩) (prʟ-fst (ixL (fa .fst)) (ixL (fb .fst)) ∙ cong₂ pr (fa .snd) (fb .snd)) (d .snd (fa .fst , fb .fst)) where fa = ∈-asFiber {a = fst a} {b = Lset α} (snd a) fb = ∈-asFiber {a = fst b} {b = Lset α} (snd b) confine : (z : S) → ⟨ Related α (fst z) ⟩ → ⟨ fst z ∈ fst (d .fst) ⟩ confine z = PT.rec (snd (fst z ∈ fst (d .fst))) (λ { (_ , h₁) → PT.rec (snd (fst z ∈ fst (d .fst))) (λ { (a , h₂) → PT.rec (snd (fst z ∈ fst (d .fst))) (λ { (b , (q , _)) → subst (λ x → ⟨ x ∈ fst (d .fst) ⟩) (sym q) (onPair a b) }) h₂ }) h₁ }) opaque tableAt : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → Bundle α tableAt = ∈-induction {P = λ α → ⟨ isL α ⟩ → IsOrd α → Bundle α} (build (PairGraphAt zero (suc zero)) refl) where -- perf: the pair graph enters as a variable with its own equation build : (φ : Formula S 2) → φ ≡ PairGraphAt zero (suc zero) → (α : V ℓ) → ((δ : V ℓ) → ⟨ δ ∈ α ⟩ → ⟨ isL δ ⟩ → IsOrd δ → Bundle δ) → ⟨ isL α ⟩ → IsOrd α → Bundle α build φ qφ α IH hα oα = rep .fst .fst , (sep .fst .fst , (spec , rspec)) where A : S A = α , hα ordOf : (c : S) → ⟨ fst c ∈ α ⟩ → IsOrd (fst c) ordOf c c∈ = mem-ord {A = α} oα (fst c) c∈ bun : (c : S) → ⟨ fst c ∈ α ⟩ → Bundle (fst c) bun c c∈ = IH (fst c) c∈ (snd c) (ordOf c c∈) value : (c : S) → ⟨ fst c ∈ α ⟩ → S value c c∈ = bun c c∈ .snd .fst relOK : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) → IsRel (fst c) (value c c∈) relOK c c∈ = bun c c∈ .snd .snd .snd entry : (c : S) → ⟨ fst c ∈ α ⟩ → S entry c c∈ = prʟ c (value c c∈) below : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) (k : S) → ⟨ (value c c∈ ∷ k ∷ c ∷ []) ⊨ GraphAt zero (suc (suc zero)) ⟩ below c c∈ k = graph-table zero (suc (suc zero)) (value c c∈ ∷ k ∷ c ∷ []) (bun c c∈ .fst) (ordOf c c∈) (reads .snd) ents (reads .fst) (relOK c c∈) where reads : Domain (bun c c∈ .fst) (fst c) × Values (bun c c∈ .fst) (fst c) reads = table-out (fst c) (ordOf c c∈) (bun c c∈ .fst) (bun c c∈ .snd .snd .fst) ents : Entries (bun c c∈ .fst) (fst c) ents e e∈ = ∣ value e e∈' , table-in (fst c) (ordOf c c∈) (bun c c∈ .fst) (bun c c∈ .snd .snd .fst) e (value e e∈') e∈ (relOK e e∈') ∣₁ where e∈' : ⟨ fst e ∈ α ⟩ e∈' = oα .fst {x = fst c} {y = fst e} e∈ c∈ holds : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) → ⟨ (entry c c∈ ∷ c ∷ []) ⊨ φ ⟩ holds c c∈ = PairGraph-in zero (suc zero) (entry c c∈ ∷ c ∷ []) φ qφ (value c c∈) (prʟ-fst c (value c c∈)) (below c c∈ (entry c c∈)) only : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) (k : S) → ⟨ (k ∷ c ∷ []) ⊨ φ ⟩ → k ≡ entry c c∈ only c c∈ k h = PT.rec (isSetS k (entry c c∈)) read (PairGraph-out zero (suc zero) (k ∷ c ∷ []) φ qφ h) where read : PairOf zero (suc zero) (k ∷ c ∷ []) φ qφ → k ≡ entry c c∈ read (r , (q , hg)) = Σ≡Prop (λ x → snd (isL x)) ( q ∙ cong (pr (fst c)) (cong fst (rel-unique (fst c) r (value c c∈) (graph-only zero (suc (suc zero)) (r ∷ k ∷ c ∷ []) hg (ordOf c c∈)) (relOK c c∈))) ∙ sym (prʟ-fst c (value c c∈)) ) fc : (c : S) → ⟨ c ∈ˢ A ⟩ → isContr (Σ[ k ∈ S ] ⟨ (k ∷ c ∷ []) ⊨ φ ⟩) fc c c∈ = mereFunct φ c ∣ entry c c∈ , (holds c c∈ , only c c∈) ∣₁ rep : isContr (SetOf (λ z → ⋁ S (λ c → (c ∈ˢ A) ⊓ ((z ∷ c ∷ []) ⊨ φ)))) rep = hasReplacementL A φ fc H : S H = rep .fst .fst spec : IsTable α H spec z = ⇔toPath toRec fromRec where toRec : ⟨ fst z ∈ fst H ⟩ → ⟨ Recorded α (fst z) ⟩ toRec hz = PT.rec squash₁ (λ { (c , (c∈ , hp)) → ∣ c , (c∈ , ∣ value c c∈ , ( cong fst (only c c∈ z hp) ∙ prʟ-fst c (value c c∈) , relOK c c∈ ) ∣₁) ∣₁ }) (subst ⟨_⟩ (rep .fst .snd z) hz) fromRec : ⟨ Recorded α (fst z) ⟩ → ⟨ fst z ∈ fst H ⟩ fromRec hz = subst ⟨_⟩ (sym (rep .fst .snd z)) (PT.map (λ { (c , (c∈ , hr)) → c , (c∈ , PT.rec (snd ((z ∷ c ∷ []) ⊨ φ)) (λ { (r , (q , hs)) → subst (λ t → ⟨ (t ∷ c ∷ []) ⊨ φ ⟩) (sym (Σ≡Prop (λ x → snd (isL x)) (q ∙ cong (pr (fst c)) (cong fst (rel-unique (fst c) r (value c c∈) hs (relOK c c∈))) ∙ sym (prʟ-fst c (value c c∈))))) (holds c c∈) }) hr) }) hz) tvals : Values H α tvals = table-out α oα H spec .snd tents : Entries H α tents c c∈ = ∣ value c c∈ , table-in α oα H spec c (value c c∈) c∈ (relOK c c∈) ∣₁ sep : isContr (SetOf (λ x → (x ∈ˢ bound α oα .fst) ⊓ ((x ∷ []) ⊨ Cond₀ A H))) sep = hasSeparationL (bound α oα .fst) (Cond₀ A H) rspec : IsRel α (sep .fst .fst) rspec z = (λ hz → subst ⟨_⟩ (cond₀-spec A H oα tvals tents z) (subst ⟨_⟩ (sep .fst .snd z) hz .snd)) , (λ hz → subst ⟨_⟩ (sym (sep .fst .snd z)) ( bound α oα .snd z hz , subst ⟨_⟩ (sym (cond₀-spec A H oα tvals tents z)) hz )) relL : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → S relL α hα oα = tableAt α hα oα .snd .fst relL-spec : (α : V ℓ) (hα : ⟨ isL α ⟩) (oα : IsOrd α) → IsRel α (relL α hα oα) relL-spec α hα oα = tableAt α hα oα .snd .snd .snd
The members are the pairs the order relates
The last four statements are the chapter's deliverable, and each is one of the readings above at the set this chapter builds: the relation at the stage realizes the class, so it is a set the readings apply to. Nothing new is proved here; what is fixed is which realizing set is meant.
Nothing here is an approximation to the statement. The membership is an equivalence, so a separation that carves with this set carves with the order itself, and that is what the last chapter of the part will do.
module _ (α : V ℓ) (hα : ⟨ isL α ⟩) (oα : IsOrd α) where relL-fill : (a b : Mem (Lset α)) → relOf (orderAt α oα) a b → ⟨ pr (fst a) (fst b) ∈ fst (relL α hα oα) ⟩ relL-fill = rel-fill α oα (relL α hα oα) (relL-spec α hα oα) relL-rep : (a b : Mem (Lset α)) → ⟨ pr (fst a) (fst b) ∈ fst (relL α hα oα) ⟩ → relOf (orderAt α oα) a b relL-rep = rel-rep α oα (relL α hα oα) (relL-spec α hα oα) open SWO (carry (Lset α) (orderAt α oα)) using () renaming ( _<∙_ to _≺ᶜ_ ) ix-fill : (u v : ⟪ Lset α ⟫) → u ≺ᶜ v → ⟨ pr (⟪ Lset α ⟫↪ u) (⟪ Lset α ⟫↪ v) ∈ fst (relL α hα oα) ⟩ ix-fill = ixRel-fill α oα (relL α hα oα) (relL-spec α hα oα) ix-rep : (u v : ⟪ Lset α ⟫) → ⟨ pr (⟪ Lset α ⟫↪ u) (⟪ Lset α ⟫↪ v) ∈ fst (relL α hα oα) ⟩ → u ≺ᶜ v ix-rep = ixRel-rep α oα (relL α hα oα) (relL-spec α hα oα)
Recap
Related is the class the chapter realizes, the pairs of two members of a stage that the order there relates, with the comparison carried truncated because it is not known to be proposition-valued, and strict takes the truncation off again for every strict well-order at once, by splitting on trichotomy before eliminating anything. Realizes says a set of the model realizes that class, written as an indexed conjunction of two implications so that it is a proposition of the model rather than an equality one universe up.
rel-fill, rel-rep, ixRel-fill and ixRel-repread the membership of any realizing set at the two shapes a member of a stage comes in, and they are stated of any such set on purpose: the naming machinery has to be handed the relation at the stage below the one being built, and inside the construction that set arrives from the table with the hypothesis that it realizes the class there, a stage before the set this chapter returns exists.
ApproxAt and GraphAt are the approximation and its graph, generic in the step condition, which enters as a parameter in two forms, at slots for the graph and at constants for the separation, each with the hypothesis that says what it means. approx-val pins every value an approximation records by one membership induction on the argument, with no single-valuedness hypothesis anywhere, and approx-uniq is the corollary. graph-only and
graph-table are the graph's two directions against a table.
tableAt is the construction, sealed where it is built, and it carries two things at every ordinal: the table of relations below it, collected by replacement through mereFunct, and the relation at it, separated out of a bound. The bound is the one piece with no counterpart in the hierarchy chapter, and it costs one appeal: the pairs of two members of a stage form a small family of elements of L, so smallDom confines them all at once. relL is the second component, and relL-fill, relL-rep,
ix-fill and ix-rep are the four readings above instantiated at it, the second pair being the shape a separation and the naming chapter's parameter order both consume.
What the chapter does not do is prove the step condition's own adequacy, named here as the two hypotheses of Described. That is not one thing but three: the previous chapter's StepAt against the meta step, the birth stage described in the object language, which nothing describes yet, and the code set at a carrier that moves with the birth. Together they are what stands between this construction and an unconditional theorem.