BedrockThe step described, and the table made unconditional
Every chapter of this part has handed its remainder to the next one, and the remainder is now a single formula. The frame that turns the order at a stage from a description into an object (L.Choice.Table's Described, applied through L.Choice.Faithful's Ordered) asks for one thing it does not have: a description of the step, saying of two members of a stage's definable subsets that the naming comparison puts the first before the second.
Everything that description needs is already built. The naming comparison is described in the object language, and its adequacy against the meta comparison is proven, on a frame that hands every relation slot the hypothesis of which order it holds. The code slot of that frame is filled unconditionally by the order on the limit stage. The carrier slot is filled by the table's own readings, and those readings were restated at "whatever realizes the class", which is exactly what the step parameter is handed. So the two ends meet, and this chapter is assembly: no new idea, only the writing down.
The description binds six sets and pins two constants. The six are the tower at the stage, its definable subsets, the table's value at the stage, and the code set over the tower, together with the two pinned ones. The two pinned by an object equality are the order on the codes and the code set at the empty alphabet, because a slot takes a variable and those two are particular sets, not descriptions. The body at those seven slots is the internalized step. Then two readings, by unpacking and packing the six binders, and then one line opens the frame.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Choice.Order {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ∃̇_ ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd; 𝒟ₒ ) open import L.Ordinal {ℓ} using ( suc-ord ) open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc ) open import L.Axioms.Basic {ℓ} using ( LsetS; 𝒟ₒS; ∅ʟ; Lset-suc ) open import L.Choice.Stage {ℓ} lem using ( stageBound ) open import L.Choice.Step {ℓ} lem using ( Mem; New; relOf; carry; orderAt; Under ; stepAt-fill; stepAt-read; IsLeastName; leastNameOf ) open import L.Choice.Name {ℓ} lem using ( module Naming ) open import L.Choice.Internal {ℓ} lem using ( StepAt ) open import L.Choice.Table {ℓ} lem using ( IsRel; ixRel-fill; ixRel-rep ) open import L.Choice.Faithful {ℓ} lem using ( CodesAt; CodesAt-in; CodesAt-out; stepOrder; module Ordered ) open import L.Choice.Adequate {ℓ} lem using ( module At ) open import L.Choice.Before {ℓ} lem using ( codeOrder; codeOrder-fill; codeOrder-rep ) open import L.Coding.Sequence {ℓ} lem using ( LsetGraphAt ) open import L.Coding.Powerset {ℓ} lem using ( DefAt; DefAt-stage ) open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate ) open import L.Coding.CodeSet {ℓ} lem using ( AllCodes ) open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines ) open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO ) import FOL.Absoluteness open import Cubical.Data.Sigma using ( Σ≡Prop ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( sucV ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ 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) sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n))) sh3 i = suc (suc (suc i)) sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n)))))) sh6 i = suc (suc (suc (suc (suc (suc i))))) iTow iRel iCod iOrd iNil : ∀ {n} → Fin (suc (suc (suc (suc (suc (suc n)))))) iTow = suc (suc (suc (suc (suc zero)))) iRel = suc (suc (suc zero)) iCod = suc (suc zero) iOrd = suc zero iNil = zero
The elements the description binds
Two of the six sets are computed from the stage: the tower there, and its definable subsets. Both are elements of the model, that is, pairs of a set and a proof that it is constructible, and both are sealed where they are built, with one reading each saying what the set half is. This is the law the birth description measured at 178 s against 2 s, and nothing about that measurement was local to it: an element that reaches a slot inside a satisfaction is unfolded by conversion every time the satisfaction is read, and the seal is what stops that.
-- perf: the elements the step description binds are sealed where they are built, -- as the birth description's were (measured there at 178 s against 2 s) opaque towerS : (β : V ℓ) → IsOrd β → S towerS β ob = LsetS β ob towerS-fst : (β : V ℓ) (ob : IsOrd β) → fst (towerS β ob) ≡ Lset β towerS-fst β ob = refl powS : (β : V ℓ) → IsOrd β → S powS β ob = 𝒟ₒS β ob powS-fst : (β : V ℓ) (ob : IsOrd β) → fst (powS β ob) ≡ 𝒟ₒ (Lset β) powS-fst β ob = refl
The description
Six binders, in the order in which each one's condition can be stated. The first binds the tower at the slot d, reached the only way the hierarchy can be reached, through the sequence chapter's graph. The second binds its definable subsets through the powerset chapter's DefAt, and the two compared sets are required to lie in it: that is how the step's two membership components are obtained, since a member of the next stage is exactly a definable subset of this one, and no separate lemma is needed. The third binds the table's value at d, said as an application of the slot f, which is what makes the description read against whatever table the caller holds rather than against a named one. The fourth binds the code set over the tower through the previous chapter's
CodesAt, which was written for exactly this slot.
The last two binders pin constants by an object equality, because the internalized step takes seven slots and a slot holds a variable: the order on the codes, and the code set at the empty alphabet, which is the one that says a skeleton is parameter-free. Both are particular sets of the model, both are already sealed where they were built, and pinning them costs one conjunct each.
The whole formula is sealed. It is read at constants downstream, and that is the law the family chapter measured at 376 s against 3.8 s.
-- perf: the description is read at constants, so it is sealed where it is built opaque Stp : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n Stp d f u v = ∃̇ ( LsetGraphAt zero (suc d) ∧̇ ∃̇ ( DefAt zero (suc zero) ∧̇ ( (var (sh2 u) ∈̇ var zero) ∧̇ ( (var (sh2 v) ∈̇ var zero) ∧̇ ∃̇ ( appAt (sh3 f) (sh3 d) zero ∧̇ ∃̇ ( CodesAt zero (sh3 zero) ∧̇ ∃̇ ( (var zero ≐ con codeOrder) ∧̇ ∃̇ ( (var zero ≐ con (AllCodes ∅ʟ)) ∧̇ StepAt iOrd iRel iTow iCod iNil (sh6 u) (sh6 v) ) ) ) ) ) ) ) )
The six binders, layer by layer
Six existential binders under conjunctions unfold into six nested truncations, and the two readings walk that nesting in opposite directions. Each layer gets a name,
One through Six, so that neither reading ever writes the nesting out and every truncation payload is named, which is the standing law for payloads.
StepHolds is the innermost layer, the satisfaction of the internalized step at the six bound elements, and it is sealed. That is a law measured here for the first time, and it is the difference between this chapter finishing and not finishing. The step adequacy is proved on a frame generic in those elements; instantiating that frame at the concrete elements this description binds forces the frame's conclusion type to be normalized, and unsealed it does not finish (over 200 s, against 7 s for the whole chapter with the seal). The rule is the same one the descriptions themselves obey, applied one level up: the type a frame concludes in is sealed where it is built.
module Reading {n : ℕ} (d f u v : Fin n) (γ : S ^ n) (od : IsOrd (fst (lookup d γ))) where private δ : V ℓ δ = fst (lookup d γ) ordW : SWO ⟪ Lset δ ⟫ ordW = carry (Lset δ) (orderAt δ od) module NM = Naming (Lset δ) ordW Goal : Type (ℓ-suc ℓ) Goal = ∥ Under δ (stepOrder δ od) (fst (lookup u γ)) (fst (lookup v γ)) ∥₁ -- perf: the type the step adequacy concludes in is sealed where it is built; -- unsealed, instantiating the frame at the concrete elements this description -- binds does not finish (over 200 s against 7 s for the whole chapter) opaque StepHolds : (tw pw rl cs ro c0 : S) → Type (ℓ-suc ℓ) StepHolds tw pw rl cs ro c0 = ⟨ (c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ StepAt iOrd iRel iTow iCod iNil (sh6 u) (sh6 v) ⟩ Six : (tw pw rl cs ro c0 : S) → Type (ℓ-suc ℓ) Six tw pw rl cs ro c0 = ⟨ (c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ (var zero ≐ con (AllCodes ∅ʟ)) ⟩ × StepHolds tw pw rl cs ro c0 Five : (tw pw rl cs ro : S) → Type (ℓ-suc ℓ) Five tw pw rl cs ro = ⟨ (ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ (var zero ≐ con codeOrder) ⟩ × ∥ (Σ[ c0 ∈ S ] Six tw pw rl cs ro c0) ∥₁ Four : (tw pw rl cs : S) → Type (ℓ-suc ℓ) Four tw pw rl cs = ⟨ (cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩ × ∥ (Σ[ ro ∈ S ] Five tw pw rl cs ro) ∥₁ Three : (tw pw rl : S) → Type (ℓ-suc ℓ) Three tw pw rl = ⟨ (rl ∷ pw ∷ tw ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ × ∥ (Σ[ cs ∈ S ] Four tw pw rl cs) ∥₁ Two : (tw pw : S) → Type (ℓ-suc ℓ) Two tw pw = ⟨ (pw ∷ tw ∷ γ) ⊨ DefAt zero (suc zero) ⟩ × ( ⟨ fst (lookup u γ) ∈ fst pw ⟩ × ( ⟨ fst (lookup v γ) ∈ fst pw ⟩ × ∥ (Σ[ rl ∈ S ] Three tw pw rl) ∥₁ ) ) One : (tw : S) → Type (ℓ-suc ℓ) One tw = ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ × ∥ (Σ[ pw ∈ S ] Two tw pw) ∥₁
The step adequacy at a stage
Slots is where all six arguments of the step adequacy are supplied, and it is generic in the six sets, each carrying its defining equation as a hypothesis. The carrier is the tower at the stage and the well-order on it is the one this part's family gives there; the code side is filled by the limit chapter's order and its two representation lemmas, which the family chapter made unconditional; the parameter side is filled by the table's readings at the value the description binds, which is where the step parameter's own hypothesis is spent. The remaining five arguments are the equations pinning the five slots, and nothing else is used.
What comes out is two readings of the innermost layer and, on either side of them, the two translations between the frame's spelling of "is the least name of" and the step chapter's exported predicate. The translations are only sym on each of two components, but they are placed here, where the name is still a variable, and not at the call sites, where it is the value of the least-name search.
module Slots (tw pw rl cs ro c0 : S) (qtw : fst tw ≡ Lset δ) (hrel : IsRel δ rl) (qcs : fst cs ≡ fst (AllCodes (LsetS δ od))) (qro : fst ro ≡ fst codeOrder) (qc0 : fst c0 ≡ fst (AllCodes ∅ʟ)) where private module A6 = At (Lset δ) (snd (LsetS δ od)) ordW module L6 = A6.Least codeOrder rl codeOrder-rep codeOrder-fill (ixRel-rep δ od rl hrel) (ixRel-fill δ od rl hrel) module St = L6.Step iOrd iRel iTow iCod iNil (sh6 u) (sh6 v) (c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) qro refl (Σ≡Prop (λ x → snd (isL x)) qtw) qcs qc0 LeastFst : NM.Name → Type (ℓ-suc ℓ) LeastFst = St.LeastOf (sh6 u) LeastSnd : NM.Name → Type (ℓ-suc ℓ) LeastSnd = St.LeastOf (sh6 v) leastFst-in : (t : NM.Name) → IsLeastName δ ordW t (fst (lookup u γ)) → LeastFst t leastFst-in t (q , mn) = sym q , λ t' q' → mn t' (sym q') leastSnd-in : (t : NM.Name) → IsLeastName δ ordW t (fst (lookup v γ)) → LeastSnd t leastSnd-in t (q , mn) = sym q , λ t' q' → mn t' (sym q') leastFst-out : (t : NM.Name) → LeastFst t → IsLeastName δ ordW t (fst (lookup u γ)) leastFst-out t (q , mn) = sym q , λ t' q' → mn t' (sym q') leastSnd-out : (t : NM.Name) → LeastSnd t → IsLeastName δ ordW t (fst (lookup v γ)) leastSnd-out t (q , mn) = sym q , λ t' q' → mn t' (sym q') opaque unfolding StepHolds holds-in : (t₁ t₂ : NM.Name) → LeastFst t₁ → LeastSnd t₂ → NM._≺ₙ_ t₁ t₂ → StepHolds tw pw rl cs ro c0 holds-in = St.StepAt-fill holds-out : StepHolds tw pw rl cs ro c0 → ∥ Σ[ t₁ ∈ NM.Name ] Σ[ t₂ ∈ NM.Name ] (LeastFst t₁ × (LeastSnd t₂ × NM._≺ₙ_ t₁ t₂)) ∥₁ holds-out = St.StepAt-read
Unpacking
atAll takes the six sets and everything the six binders held, and returns the meta step. The tower's graph pins the first set to the tower, the definable subsets' description pins the second to the definable subsets of it, and those two equations together turn the two membership conjuncts into memberships of the next stage, which is what the meta step's two components are. The application at f turns into a pair in the table, which is what the step parameter's hypothesis consumes, and it is consumed at whatever value the description bound, not at one the caller chose: that is why the hypothesis quantifies over every value the table records there. The code set reading pins the fourth, and the two pinned constants are already equations. Then the frame's reading gives two names, least for the two sets, with the naming comparison between them, and the step chapter's own reading turns that into the comparison at the stage.
private atAll : (tw pw rl cs ro c0 : S) → ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ → ⟨ (pw ∷ tw ∷ γ) ⊨ DefAt zero (suc zero) ⟩ → ⟨ fst (lookup u γ) ∈ fst pw ⟩ → ⟨ fst (lookup v γ) ∈ fst pw ⟩ → ⟨ (rl ∷ pw ∷ tw ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ → ⟨ (cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩ → ((r : S) → ⟨ pr δ (fst r) ∈ fst (lookup f γ) ⟩ → IsRel δ r) → fst ro ≡ fst codeOrder → fst c0 ≡ fst (AllCodes ∅ʟ) → StepHolds tw pw rl cs ro c0 → Goal atAll tw pw rl cs ro c0 hg hdef hu hv happ hcs vals qro qc0 hstep = PT.map atNames (K.holds-out hstep) where qtw : fst tw ≡ Lset δ qtw = Lset-only zero (suc d) (tw ∷ γ) hg od qpw : fst pw ≡ 𝒟ₒ (Lset δ) qpw = subst ⟨_⟩ (DefAt-stage δ od zero (suc zero) (pw ∷ tw ∷ γ) qtw) hdef inSuc : (x : V ℓ) → ⟨ x ∈ fst pw ⟩ → ⟨ x ∈ Lset (sucV δ) ⟩ inSuc x h = subst (λ z → ⟨ x ∈ z ⟩) (sym (Lset-suc δ)) (subst (λ z → ⟨ x ∈ z ⟩) qpw h) a : New δ a = fst (lookup u γ) , inSuc (fst (lookup u γ)) hu b : New δ b = fst (lookup v γ) , inSuc (fst (lookup v γ)) hv hrel : IsRel δ rl hrel = vals rl (subst ⟨_⟩ (appAt-adequate (sh3 f) (sh3 d) zero (rl ∷ pw ∷ tw ∷ γ)) happ) qcs : fst cs ≡ fst (AllCodes (LsetS δ od)) qcs = cong fst (CodesAt-out (LsetS δ od) zero (sh3 zero) (cs ∷ rl ∷ pw ∷ tw ∷ γ) qtw hcs) module K = Slots tw pw rl cs ro c0 qtw hrel qcs qro qc0 atNames : Σ[ t₁ ∈ NM.Name ] Σ[ t₂ ∈ NM.Name ] ( K.LeastFst t₁ × ( K.LeastSnd t₂ × NM._≺ₙ_ t₁ t₂ ) ) → Under δ (stepOrder δ od) (fst (lookup u γ)) (fst (lookup v γ)) atNames (t₁ , (t₂ , (l₁ , (l₂ , lt)))) = a .snd , ( b .snd , stepAt-fill δ ordW a b t₁ t₂ (K.leastFst-out t₁ l₁) (K.leastSnd-out t₂ l₂) lt )
Packing
The other direction chooses the six sets and discharges the six conditions. The tower and its definable subsets are the sealed elements, and their conditions are the sequence chapter's "this is the tower" and the powerset chapter's "this is the definable subsets of it", each read off a single equation. The table's value is the one the caller hands over, and the code set is the one the previous chapter's description carves, so its condition is that description read at the tower. The two constants are pinned by refl, because the element bound is the constant itself. The innermost conjunct is the frame's other reading, applied to the two least names the step chapter's search returns, and to the naming comparison the step chapter reads off the comparison at the stage.
module Pack (rl : S) (hpr : ⟨ pr δ (fst rl) ∈ fst (lookup f γ) ⟩) (hrel : IsRel δ rl) (hx : ⟨ fst (lookup u γ) ∈ Lset (sucV δ) ⟩) (hy : ⟨ fst (lookup v γ) ∈ Lset (sucV δ) ⟩) where private module K = Slots (towerS δ od) (powS δ od) rl (AllCodes (LsetS δ od)) codeOrder (AllCodes ∅ʟ) (towerS-fst δ od) hrel refl refl refl a : New δ a = fst (lookup u γ) , hx b : New δ b = fst (lookup v γ) , hy n₁ : Σ[ t ∈ NM.Name ] IsLeastName δ ordW t (fst (lookup u γ)) n₁ = leastNameOf δ ordW a n₂ : Σ[ t ∈ NM.Name ] IsLeastName δ ordW t (fst (lookup v γ)) n₂ = leastNameOf δ ordW b hg : ⟨ (towerS δ od ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ hg = Lset-defines zero (suc d) (towerS δ od ∷ γ) od (towerS-fst δ od) hdef : ⟨ (powS δ od ∷ towerS δ od ∷ γ) ⊨ DefAt zero (suc zero) ⟩ hdef = subst ⟨_⟩ (sym (DefAt-stage δ od zero (suc zero) (powS δ od ∷ towerS δ od ∷ γ) (towerS-fst δ od))) (powS-fst δ od) inPow : (x : V ℓ) → ⟨ x ∈ Lset (sucV δ) ⟩ → ⟨ x ∈ fst (powS δ od) ⟩ inPow x h = subst (λ z → ⟨ x ∈ z ⟩) (sym (powS-fst δ od)) (subst (λ z → ⟨ x ∈ z ⟩) (Lset-suc δ) h) happ : ⟨ (rl ∷ powS δ od ∷ towerS δ od ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ happ = subst ⟨_⟩ (sym (appAt-adequate (sh3 f) (sh3 d) zero (rl ∷ powS δ od ∷ towerS δ od ∷ γ))) hpr hcs : ⟨ (AllCodes (LsetS δ od) ∷ rl ∷ powS δ od ∷ towerS δ od ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩ hcs = CodesAt-in (LsetS δ od) zero (sh3 zero) (AllCodes (LsetS δ od) ∷ rl ∷ powS δ od ∷ towerS δ od ∷ γ) (towerS-fst δ od) refl hstep : relOf (stepOrder δ od) a b → StepHolds (towerS δ od) (powS δ od) rl (AllCodes (LsetS δ od)) codeOrder (AllCodes ∅ʟ) hstep cmp = K.holds-in (n₁ .fst) (n₂ .fst) (K.leastFst-in (n₁ .fst) (n₁ .snd)) (K.leastSnd-in (n₂ .fst) (n₂ .snd)) (stepAt-read δ ordW a b (n₁ .fst) (n₂ .fst) (n₁ .snd) (n₂ .snd) cmp) packAll : relOf (stepOrder δ od) a b → ∥ (Σ[ tw ∈ S ] One tw) ∥₁ packAll cmp = ∣ towerS δ od , ( hg , ∣ powS δ od , ( hdef , ( inPow (fst (lookup u γ)) hx , ( inPow (fst (lookup v γ)) hy , ∣ rl , ( happ , ∣ AllCodes (LsetS δ od) , ( hcs , ∣ codeOrder , ( refl , ∣ AllCodes ∅ʟ , ( refl , hstep cmp ) ∣₁ ) ∣₁ ) ∣₁ ) ∣₁ ) ) ) ∣₁ ) ∣₁
The two readings
Only here is the seal opened, and only for the two readings, which peel the six layers by named helpers, one per layer, each with its conclusion written down. No
with appears: a case split concluding in a satisfaction is a named helper with its conclusion written down, and that is the law the faithfulness chapter measured past 300 s. The exported stp-out and stp-in are the two readings at the exact types the frame demands, and they carry the frame's own asymmetry: soundness quantifies over every value the table records at the carrier, because the description it reads may have bound a value of its own, while completeness takes the single value the caller realizes with.
opaque unfolding Stp StepHolds read : ((r : S) → ⟨ pr δ (fst r) ∈ fst (lookup f γ) ⟩ → IsRel δ r) → ⟨ γ ⊨ Stp d f u v ⟩ → Goal read vals = PT.rec PT.squash₁ atOne where atSix : (tw pw rl cs ro c0 : S) → ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ → ⟨ (pw ∷ tw ∷ γ) ⊨ DefAt zero (suc zero) ⟩ → ⟨ fst (lookup u γ) ∈ fst pw ⟩ → ⟨ fst (lookup v γ) ∈ fst pw ⟩ → ⟨ (rl ∷ pw ∷ tw ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ → ⟨ (cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩ → fst ro ≡ fst codeOrder → Six tw pw rl cs ro c0 → Goal atSix tw pw rl cs ro c0 hg hdef hu hv happ hcs qro (qc0 , hstep) = atAll tw pw rl cs ro c0 hg hdef hu hv happ hcs vals qro qc0 hstep atFive : (tw pw rl cs ro : S) → ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ → ⟨ (pw ∷ tw ∷ γ) ⊨ DefAt zero (suc zero) ⟩ → ⟨ fst (lookup u γ) ∈ fst pw ⟩ → ⟨ fst (lookup v γ) ∈ fst pw ⟩ → ⟨ (rl ∷ pw ∷ tw ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ → ⟨ (cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩ → Five tw pw rl cs ro → Goal atFive tw pw rl cs ro hg hdef hu hv happ hcs (qro , h) = PT.rec PT.squash₁ (λ { (c0 , hsix) → atSix tw pw rl cs ro c0 hg hdef hu hv happ hcs qro hsix }) h atFour : (tw pw rl cs : S) → ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ → ⟨ (pw ∷ tw ∷ γ) ⊨ DefAt zero (suc zero) ⟩ → ⟨ fst (lookup u γ) ∈ fst pw ⟩ → ⟨ fst (lookup v γ) ∈ fst pw ⟩ → ⟨ (rl ∷ pw ∷ tw ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ → Four tw pw rl cs → Goal atFour tw pw rl cs hg hdef hu hv happ (hcs , h) = PT.rec PT.squash₁ (λ { (ro , hfive) → atFive tw pw rl cs ro hg hdef hu hv happ hcs hfive }) h atThree : (tw pw rl : S) → ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ → ⟨ (pw ∷ tw ∷ γ) ⊨ DefAt zero (suc zero) ⟩ → ⟨ fst (lookup u γ) ∈ fst pw ⟩ → ⟨ fst (lookup v γ) ∈ fst pw ⟩ → Three tw pw rl → Goal atThree tw pw rl hg hdef hu hv (happ , h) = PT.rec PT.squash₁ (λ { (cs , hfour) → atFour tw pw rl cs hg hdef hu hv happ hfour }) h atTwo : (tw pw : S) → ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ → Two tw pw → Goal atTwo tw pw hg (hdef , (hu , (hv , h))) = PT.rec PT.squash₁ (λ { (rl , hthree) → atThree tw pw rl hg hdef hu hv hthree }) h atOne : Σ[ tw ∈ S ] One tw → Goal atOne (tw , (hg , h)) = PT.rec PT.squash₁ (λ { (pw , htwo) → atTwo tw pw hg htwo }) h fill : (r : S) → ⟨ pr δ (fst r) ∈ fst (lookup f γ) ⟩ → IsRel δ r → Under δ (stepOrder δ od) (fst (lookup u γ)) (fst (lookup v γ)) → ⟨ γ ⊨ Stp d f u v ⟩ fill r hpr hrel (hx , (hy , cmp)) = Pack.packAll r hpr hrel hx hy cmp
stp-out : ∀ {n} (d f u v : Fin n) (γ : S ^ n) (od : IsOrd (fst (lookup d γ))) → ((r : S) → ⟨ pr (fst (lookup d γ)) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst (lookup d γ)) r) → ⟨ γ ⊨ Stp d f u v ⟩ → ∥ Under (fst (lookup d γ)) (stepOrder (fst (lookup d γ)) od) (fst (lookup u γ)) (fst (lookup v γ)) ∥₁ stp-out = Reading.read stp-in : ∀ {n} (d f u v : Fin n) (γ : S ^ n) (od : IsOrd (fst (lookup d γ))) → (r : S) → ⟨ pr (fst (lookup d γ)) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst (lookup d γ)) r → Under (fst (lookup d γ)) (stepOrder (fst (lookup d γ)) od) (fst (lookup u γ)) (fst (lookup v γ)) → ⟨ γ ⊨ Stp d f u v ⟩ stp-in = Reading.fill
The frame opened
One line. It supplies the frame's last parameter, and with it the whole of the order table becomes unconditional. Said plainly, the following now hold with no hypothesis beyond this part's standing one, excluded middle:
- from L.Choice.Faithful:
CondCorewith its two readings,
Cond, Cond₀, cond-spec and cond₀-spec, that is, the order at a stage completely described, in both the forms the table's construction asks for;
- from L.Choice.Table: the step condition StepAt with
step-rel and step-table; the approximation ApproxAt
and the graph GraphAt with their readings, approx-val and
approx-uniq, graph-only and graph-table;
PairGraphAt; Recorded, IsTable, Bundle,
table-out, table-in and bound; the construction
tableAt itself; and the relation it carries at every ordinal,
relL and relL-spec, with all four representation lemmas
relL-fill, relL-rep, ix-fill and ix-rep.
This was checked the way the re-cut checked its own claim: the results were imported into a throwaway module assuming nothing but excluded middle, each restated at its type spelled out by hand, and used to derive that the order at the bounding ordinal is an element of the model whose membership is irreflexive. The probe was then deleted.
open Ordered Stp stp-out stp-in public
The order at the bounding ordinal
The last chapter will want one particular instance, in one particular shape. Given a set of L, the stage chapter's bounding ordinal is an ordinal above that set's own stage, hence above its members and their members, and above ω as well. It is constructible, because an ordinal appears at the stage after itself. So the family has an order on the members of the tower there, and the table has that order as an element of the model, with the two representation lemmas reading membership in that element against the meta comparison in both directions. That triple, the element and its two lemmas, is what a separation will be run against.
module Bound (a : V ℓ) (p : ⟨ isL a ⟩) where boundOrd : V ℓ boundOrd = stageBound a p .fst boundOrd-ord : IsOrd boundOrd boundOrd-ord = stageBound a p .snd .fst boundOrd-isL : ⟨ isL boundOrd ⟩ boundOrd-isL = Lset→isL (sucV boundOrd) (suc-ord boundOrd-ord) boundOrd (ord∈Lset-suc boundOrd boundOrd-ord) boundOrder : SWO (Mem (Lset boundOrd)) boundOrder = orderAt boundOrd boundOrd-ord orderL : S orderL = relL boundOrd boundOrd-isL boundOrd-ord orderL-fill : (x y : Mem (Lset boundOrd)) → relOf boundOrder x y → ⟨ pr (fst x) (fst y) ∈ fst orderL ⟩ orderL-fill = relL-fill boundOrd boundOrd-isL boundOrd-ord orderL-rep : (x y : Mem (Lset boundOrd)) → ⟨ pr (fst x) (fst y) ∈ fst orderL ⟩ → relOf boundOrder x y orderL-rep = relL-rep boundOrd boundOrd-isL boundOrd-ord
Recap
Stp is the step described: a sealed formula binding six sets and pinning two constants. The six are the tower at the stage, reached through the sequence chapter's graph; its definable subsets, reached through the powerset chapter's DefAt, with the two compared sets required to lie in it, which is how the step's two membership components arrive without a lemma nobody has; the table's value at the stage, reached as an application, which is what keeps the description reading against whatever table the caller holds; and the code set over the tower, reached through the previous chapter's CodesAt, which was written for this slot. The two pinned by an object equality are the order on the codes and the code set at the empty alphabet, because a slot holds a variable and those two are particular sets. The body at those seven slots is the internalized step.
Reading.read and Reading.fill are unpack and pack over the six binders, and stp-out and stp-in are those two at the frame's types. Slots is where the step adequacy is supplied its six arguments, generic in the six sets with their equations as hypotheses: the code side from the limit and family chapters, unconditional; the carrier side from the table's readings at the bound value, which is the step parameter's own hypothesis and the only input this chapter takes from outside.
One measurement, and it is a law at a new place: the type a frame concludes in is sealed where it is built. StepHolds is the step adequacy's conclusion; instantiating the frame at the concrete elements this description binds normalizes it, and unsealed that does not finish (over 200 s, against 7 s for the whole chapter). Two inherited laws are obeyed without new measurement: the elements reaching the slots are sealed, and the description itself is sealed because it is read at constants.
open Ordered is the one line, and with it the order table is unconditional: the construction and all four of its readings, together with everything the two frames export. Bound is the shape the last chapter separates with: the bounding ordinal of a set of L, the order on the members of the tower there as an element of the model, and its two representation lemmas.