BedrockThe description is faithful
The previous chapter turned the order at every stage into an object of L, and left that construction standing on two hypotheses saying what the step condition means. Filling them is not one obligation but three: the adequacy of the step description against the meta step, the birth stage said in the object language, which nothing said yet, and the code set at a carrier that moves with the birth. This chapter settles the second and the third, and turns the two hypotheses into one, which is the step at a single carrier.
The reduction is what the chapter is for, so it is worth stating exactly. The order family is birth-primary: two members of a stage are compared by the moments they were carved at, and only two carved at the same moment are compared by the machinery of that moment. So the condition the previous chapter asked for splits, and the birth half is the larger one. Written down, it needs no successor operation: a set's birth is the ordinal whose tower does not hold the set while the definable powerset of that tower does, and both of those are membership atoms over descriptions that already exist.
What does not close is the step itself. The chapter says so with a named parameter carrying its own meaning as a hypothesis, and never with an approximation.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Choice.Faithful {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; Term; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ¬̇_; ∃̇_ ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Model {ℓ} using ( ∈sucV-elim ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset; IsOrd; isPropIsOrd; Lset-mono; Lset→isL; 𝒟ₒ ) open import L.Ordinal {ℓ} using ( suc-ord; mem-ord ) open import L.Ordinal.Linear {ℓ} lem using ( ord-tri ) open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ ) open import L.Axioms.Basic {ℓ} using ( Lset-suc; LsetS; 𝒟ₒS; extensionalL ) open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem; stage-earliest ) open import L.Choice.Stage {ℓ} lem using ( ord-suc-inj ) open import L.Choice.Step {ℓ} lem using ( birth; birth-ord; birth-suc; birth-mem; birth-stage; birth-proof ; Mem; New; relOf; carry; Under; stepAt ; orderAt; orderAt-step; module Family ) open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO ) open import L.Coding.Model {ℓ} using ( extAt; extAt-in; extAt-out; extAt-in-both; prAtL; prAtL-adequate ) open import L.Coding.Sequence {ℓ} lem using ( LsetGraphAt ) open import L.Coding.Powerset {ℓ} lem using ( DefAt; DefAt-stage ) open import L.Coding.CodeSet {ℓ} lem using ( arityNumAtL; arityNumAtL-in; arityNumAtL-out; hasWitnessAt ; witnessAt-in; witnessAt-out; keyS; codeS ; AllCodes; AllCodes-in; AllCodes-out; IsKeyOverAny ) open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines ) open import L.Choice.Table {ℓ} lem using ( Ordering; strict; Related; IsRel; Values; Entries ; related-in; module Described ) open import V.Coding {ℓ} using ( pr ) import FOL.Absoluteness open import Cubical.Data.Sum using ( _⊎_; inl; inr ) open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.Foundations.Prelude using ( J; subst2 ) 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 ( ⟪_⟫ ) 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 _⊨_ ; ⟦_⟧ᵐ 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)) sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n)))) sh4 i = suc (suc (suc (suc i))) tm4 : ∀ {n} → Term S n → Term S (suc (suc (suc (suc n)))) tm4 (con k) = con k tm4 (var i) = var (sh4 i) tm4-val : ∀ {n} (t : Term S n) (a b c d : S) (γ : S ^ n) → ⟦ tm4 t ⟧ (d ∷ c ∷ b ∷ a ∷ γ) ≡ ⟦ t ⟧ γ tm4-val (con k) a b c d γ = refl tm4-val (var i) a b c d γ = refl -- perf: the two witnesses the birth description is satisfied at are sealed; -- unsealed, the chapter's first section alone runs 178 s instead of 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 birth stage, said inside
The description binds two sets and names no constant. There is a c which is the tower at b; x does not belong to it; and there is a d which is the definable powerset of c, to which x does belong. Lset-suc is what makes those two conditions equivalent to "b is one below the least stage containing x", and it is spent only on the meta side. That is why the sentence needs no successor operation of its own, and why the tower graph is used at the slot b itself rather than at a successor of it.
Both readings stand at variable slots in a variable environment, with ordinality at the b slot as the only hypothesis. Soundness is a trichotomy against the least stage, and it is a named helper with its conclusion written down: the first branch is refuted by stage-earliest, the second is
ord-suc-inj against birth-suc, and the third is
∈sucV-elim into two contradictions with the non-membership. Completeness is shorter, because Lset-defines and DefAt-stage each run one line the other way.
The two elements the description is satisfied at are sealed, and the marker records the measurement rather than a preference: unsealed, this section alone runs 178 s where sealed it runs 2 s. Lset and 𝒟ₒ are already sealed where they are built, but the pairs that carry their constructibility proofs are not, and it is the pair that reaches the slot.
BirthAt : ∀ {n} → Fin n → Fin n → Formula S n BirthAt b x = ∃̇ ( LsetGraphAt zero (suc b) ∧̇ ( ¬̇ (var (suc x) ∈̇ var zero) ∧̇ ∃̇ ( DefAt zero (suc zero) ∧̇ (var (sh2 x) ∈̇ var zero) ) ) ) module _ {n : ℕ} (b x : Fin n) (γ : S ^ n) where private β : V ℓ β = fst (lookup b γ) z : S z = lookup x γ Inner : S → Type (ℓ-suc ℓ) Inner c = Σ[ d ∈ S ] ( ⟨ (d ∷ c ∷ γ) ⊨ DefAt zero (suc zero) ⟩ × ⟨ fst z ∈ fst d ⟩ ) Outer : S → Type (ℓ-suc ℓ) Outer c = ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩ × ( (⟨ fst z ∈ fst c ⟩ → Empty.⊥) × ∥ Inner c ∥₁ ) decideBirth : IsOrd β → ⟨ fst z ∈ 𝒟ₒ (Lset β) ⟩ → (⟨ fst z ∈ Lset β ⟩ → Empty.⊥) → β ≡ birth (fst z) (snd z) decideBirth ob hin hout = go (ord-tri (sucV β) (suc-ord ob) (stage (fst z) (snd z)) (stage-ord (fst z) (snd z))) where mem : ⟨ fst z ∈ Lset (sucV β) ⟩ mem = subst (λ u → ⟨ fst z ∈ u ⟩) (sym (Lset-suc β)) hin early : ⟨ stage (fst z) (snd z) ∈ sucV β ⟩ → Empty.⊥ early h = Empty.rec* (∈sucV-elim {A = β} {x = stage (fst z) (snd z)} Empty.isProp⊥* h below same) where below : ⟨ stage (fst z) (snd z) ∈ β ⟩ → Empty.⊥* below k = Empty.rec (hout (Lset-mono {α = β} {β = stage (fst z) (snd z)} k {x = fst z} (stage-mem (fst z) (snd z)))) same : stage (fst z) (snd z) ≡ β → Empty.⊥* same e = Empty.rec (hout (subst (λ u → ⟨ fst z ∈ Lset u ⟩) e (stage-mem (fst z) (snd z)))) go : ⟨ sucV β ∈ stage (fst z) (snd z) ⟩ ⊎ ((sucV β ≡ stage (fst z) (snd z)) ⊎ ⟨ stage (fst z) (snd z) ∈ sucV β ⟩) → β ≡ birth (fst z) (snd z) go (inl h) = Empty.rec (stage-earliest (fst z) (snd z) (sucV β) (suc-ord ob) mem h) go (inr (inl e)) = ord-suc-inj β (birth (fst z) (snd z)) ob (e ∙ sym (birth-suc (fst z) (snd z))) go (inr (inr h)) = Empty.rec (early h) BirthAt-out : ⟨ γ ⊨ BirthAt b x ⟩ → IsOrd β → β ≡ birth (fst z) (snd z) BirthAt-out h ob = PT.rec (setIsSet β (birth (fst z) (snd z))) atCarrier h where atInner : (c : S) → ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩ → (⟨ fst z ∈ fst c ⟩ → Empty.⊥) → Inner c → β ≡ birth (fst z) (snd z) atInner c hg hn (d , (hd , hm)) = decideBirth ob (subst (λ u → ⟨ fst z ∈ u ⟩) qd hm) (λ k → hn (subst (λ u → ⟨ fst z ∈ u ⟩) (sym qc) k)) where qc : fst c ≡ Lset β qc = Lset-only zero (suc b) (c ∷ γ) hg ob qd : fst d ≡ 𝒟ₒ (Lset β) qd = subst ⟨_⟩ (DefAt-stage β ob zero (suc zero) (d ∷ c ∷ γ) qc) hd atCarrier : Σ[ c ∈ S ] Outer c → β ≡ birth (fst z) (snd z) atCarrier (c , (hg , (hn , hi))) = PT.rec (setIsSet β (birth (fst z) (snd z))) (atInner c hg hn) hi BirthAt-in : IsOrd β → β ≡ birth (fst z) (snd z) → ⟨ γ ⊨ BirthAt b x ⟩ BirthAt-in ob e = ∣ towerS β ob , (hg , (hn , ∣ powS β ob , (hd , hm) ∣₁)) ∣₁ where hg : ⟨ (towerS β ob ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩ hg = Lset-defines zero (suc b) (towerS β ob ∷ γ) ob (towerS-fst β ob) hn : ⟨ fst z ∈ fst (towerS β ob) ⟩ → Empty.⊥ hn k = stage-earliest (fst z) (snd z) β ob (subst (λ u → ⟨ fst z ∈ u ⟩) (towerS-fst β ob) k) (subst (λ u → ⟨ u ∈ stage (fst z) (snd z) ⟩) (sym e) (birth-stage (fst z) (snd z))) hd : ⟨ (powS β ob ∷ towerS β ob ∷ γ) ⊨ DefAt zero (suc zero) ⟩ hd = subst ⟨_⟩ (sym (DefAt-stage β ob zero (suc zero) (powS β ob ∷ towerS β ob ∷ γ) (towerS-fst β ob))) (powS-fst β ob) hm : ⟨ fst z ∈ fst (powS β ob) ⟩ hm = subst (λ u → ⟨ fst z ∈ u ⟩) (sym (powS-fst β ob)) (subst (λ u → ⟨ fst z ∈ u ⟩) (Lset-suc β) (subst (λ u → ⟨ fst z ∈ Lset (sucV u) ⟩) (sym e) (birth-mem (fst z) (snd z))))
The codes at any arity, at a carrier that is a slot
The third obligation asked for the code set at a carrier that moves with the birth. It is an instantiation and not a construction, and saying which is worth the paragraph. The powerset chapter already wrote the code predicate at a carrier held in a slot, isCodeAt, as two conjuncts: the argument is a key at arity one, and it has a closed and shaped witness over the slot. The code set chapter already wrote the arity-bound variant of the first conjunct,
arityNumAtL, because a recursion over subcodes has to be indexed by keys at every arity. Nothing else differs between the two.
So the predicate wanted here is the second conjunct joined to the arity-bound first, and its two readings are the existing two read at a slot: the arity conjunct hands over a numeral and a code, and the witness conjunct turns that pair into a formula over the carrier. No new machinery, no new side condition, and the carrier is a slot throughout.
isCodeAnyAt : ∀ {n} → Fin n → Fin n → Formula S n isCodeAnyAt c w = arityNumAtL c ∧̇ hasWitnessAt w c module _ (A : S) where codeAnyAt-in : ∀ {n k} (c w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A → (ψ : Formula ⟪ fst A ⟫ k) → fst (lookup c γ) ≡ fst (keyS A ψ) → ⟨ γ ⊨ isCodeAnyAt c w ⟩ codeAnyAt-in {k = k} c w γ qw ψ qc = arityNumAtL-in c γ k (codeS A ψ) qc , witnessAt-in A w c γ ψ qw qc codeAnyAt-out : ∀ {n} (c w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A → ⟨ γ ⊨ isCodeAnyAt c w ⟩ → ⟨ IsKeyOverAny A (lookup c γ) ⟩ codeAnyAt-out c w γ qw (hk , hw) = PT.rec squash₁ step (arityNumAtL-out c γ hk) where step : Σ[ m ∈ ℕ ] Σ[ z ∈ S ] (fst (lookup c γ) ≡ pr (# m) (fst z)) → ⟨ IsKeyOverAny A (lookup c γ) ⟩ step (m , (z , qz)) = PT.map (λ { (ψ , q) → m , (ψ , q) }) (witnessAt-out A w c γ qw hw m z qz)
The set, in one extension
The set 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. Its two readings join the predicate's to the code set's own membership equivalence, and what comes out is an equality of elements: at a carrier reached by an equation, the slot holds the code set over that carrier and nothing else.
That is what "moves with the birth" was asking for. The naming description takes its code set as a slot pinned by an equation supplied from outside; with this conjunct beside it the slot is pinned by the description instead, so a caller may bind the carrier first and let the code set follow it.
CodesAt : ∀ {n} → Fin n → Fin n → Formula S n CodesAt c w = extAt c (isCodeAnyAt zero (suc w)) module _ (A : S) {n : ℕ} (c w : Fin n) (γ : S ^ n) (qw : fst (lookup w γ) ≡ fst A) where CodesAt-out : ⟨ γ ⊨ CodesAt c w ⟩ → lookup c γ ≡ AllCodes A CodesAt-out h = extensionalL step where step : (x : S) → (x ∈ˢ lookup c γ) ≡ (x ∈ˢ AllCodes A) step x = ⇔toPath (λ hx → AllCodes-in A x (codeAnyAt-out A zero (suc w) (x ∷ γ) qw (extAt-out c (isCodeAnyAt zero (suc w)) γ h x hx))) (λ hx → extAt-in c (isCodeAnyAt zero (suc w)) γ h x (PT.rec (snd ((x ∷ γ) ⊨ isCodeAnyAt zero (suc w))) (λ { (k , (ψ , q)) → codeAnyAt-in A {k = k} zero (suc w) (x ∷ γ) qw ψ q }) (AllCodes-out A x hx))) CodesAt-in : lookup c γ ≡ AllCodes A → ⟨ γ ⊨ CodesAt c w ⟩ CodesAt-in q = extAt-in-both c (isCodeAnyAt zero (suc w)) γ into back where into : (x : S) → ⟨ fst x ∈ fst (lookup c γ) ⟩ → ⟨ (x ∷ γ) ⊨ isCodeAnyAt zero (suc w) ⟩ into x hx = PT.rec (snd ((x ∷ γ) ⊨ isCodeAnyAt zero (suc w))) (λ { (k , (ψ , qk)) → codeAnyAt-in A {k = k} zero (suc w) (x ∷ γ) qw ψ qk }) (AllCodes-out A x (subst (λ u → ⟨ fst x ∈ fst u ⟩) q hx)) back : (x : S) → ⟨ (x ∷ γ) ⊨ isCodeAnyAt zero (suc w) ⟩ → ⟨ fst x ∈ fst (lookup c γ) ⟩ back x hx = subst (λ u → ⟨ fst x ∈ fst u ⟩) (sym q) (AllCodes-in A x (codeAnyAt-out A zero (suc w) (x ∷ γ) qw hx))
The order at a stage, unfolded once
Three meta-language definitions, and one of them is the chapter's pivot.
order-unfold is the family's defining equation read at a stage: the comparison of two members is their births compared, or, at a shared birth, the step there. It is one cong over the recursion's computation rule, and everything the object language has to match now stands on its right-hand side.
bornIn is the converse of birth-in: a set whose birth lies below an ordinal lies in the tower at that ordinal. It is what lets the description drop the condition "both compared sets belong to the stage" and keep only "both births lie below it", which is two membership atoms at slots that are bound anyway, and one binder cheaper.
stepMoved moves a step comparison along an equality of carriers, by path induction, with the proof irrelevance of ordinality in the base case. The previous chapter has the same lemma privately. It is rebuilt here rather than exported, because data reached from another module is what this route pays for, and the cure is locality.
stepOrder : (δ : V ℓ) → IsOrd δ → SWO (New δ) stepOrder δ oδ = stepAt δ (carry (Lset δ) (orderAt δ oδ)) stepMoved : (δ δ' : V ℓ) (e : δ ≡ δ') (o : IsOrd δ) (o' : IsOrd δ') (x y : V ℓ) → Under δ (stepOrder δ o) x y → Under δ' (stepOrder δ' o') x y stepMoved δ δ' e = J Motive base e where Motive : (δ' : V ℓ) → δ ≡ δ' → Type (ℓ-suc ℓ) Motive δ' _ = (o : IsOrd δ) (o' : IsOrd δ') (x y : V ℓ) → Under δ (stepOrder δ o) x y → Under δ' (stepOrder δ' o') x y base : Motive δ refl base o o' x y = subst (λ w → Under δ (stepOrder δ w) x y) (isPropIsOrd δ o o') bornIn : (α : V ℓ) → IsOrd α → (x : V ℓ) (p : ⟨ isL x ⟩) → ⟨ birth x p ∈ α ⟩ → ⟨ x ∈ Lset α ⟩ bornIn α oα x p h = reach (suc∈or≡ (birth x p) α (birth-ord x p) oα h) where reach : ⟨ sucV (birth x p) ∈ α ⟩ ⊎ (sucV (birth x p) ≡ α) → ⟨ x ∈ Lset α ⟩ reach (inl k) = Lset-mono {α = α} {β = sucV (birth x p)} k {x = x} (birth-mem x p) reach (inr e) = subst (λ w → ⟨ x ∈ Lset w ⟩) e (birth-mem x p) module _ (α : V ℓ) (oα : IsOrd α) where private module Fam = Family α (λ δ _ → orderAt δ) oα memberL : (a : Mem (Lset α)) → ⟨ isL (fst a) ⟩ memberL a = Lset→isL α oα (fst a) (snd a) bornOf : (a : Mem (Lset α)) → V ℓ bornOf a = birth (fst a) (memberL a) bornOrd : (a : Mem (Lset α)) → IsOrd (bornOf a) bornOrd a = birth-ord (fst a) (memberL a) bornMem : (a : Mem (Lset α)) → ⟨ bornOf a ∈ α ⟩ bornMem a = Fam.bornAt a .snd order-unfold : (a b : Mem (Lset α)) → relOf (orderAt α oα) a b ≡ ( ⟨ bornOf a ∈ bornOf b ⟩ ⊎ ( (bornOf b ≡ bornOf a) × Under (bornOf a) (stepOrder (bornOf a) (mem-ord {A = α} oα (bornOf a) (bornMem a))) (fst a) (fst b) ) ) order-unfold a b = cong (λ z → relOf (z oα) a b) (orderAt-step α)
Four more elements reach slots inside a satisfaction, and they are sealed for the same measured reason. The equations the seal exposes are exactly the three the description consumes: the underlying set of a member, the underlying set of a birth, and the one that says a birth is the birth of the member beside it, so that the birth description is discharged by refl at each call site.
-- perf: the four elements the order description is satisfied at are sealed; -- unsealed, the reading back into the object language runs past 400 s opaque memS : (α : V ℓ) (oα : IsOrd α) → Mem (Lset α) → S memS α oα a = fst a , memberL α oα a memS-fst : (α : V ℓ) (oα : IsOrd α) (a : Mem (Lset α)) → fst (memS α oα a) ≡ fst a memS-fst α oα a = refl bornS : (α : V ℓ) (oα : IsOrd α) → ⟨ isL α ⟩ → Mem (Lset α) → S bornS α oα pα a = bornOf α oα a , isL-trans {x = α} {y = bornOf α oα a} (bornMem α oα a) pα bornS-fst : (α : V ℓ) (oα : IsOrd α) (pα : ⟨ isL α ⟩) (a : Mem (Lset α)) → fst (bornS α oα pα a) ≡ bornOf α oα a bornS-fst α oα pα a = refl bornS-birth : (α : V ℓ) (oα : IsOrd α) (pα : ⟨ isL α ⟩) (a : Mem (Lset α)) → fst (bornS α oα pα a) ≡ birth (fst (memS α oα a)) (snd (memS α oα a)) bornS-birth α oα pα a = refl
The order described, with the step as a parameter
Everything from here is generic in the step condition, which enters as a parameter with its meaning stated in both directions: at a carrier reached by a slot, with the table's value there in hand, the condition holds of two sets exactly when the step order at that carrier relates them. That parameter is the whole of what this chapter still owes, and it is deliberately one thing and not three.
The two directions take the table's value at that carrier differently, and the difference is not cosmetic. Completeness is handed a value, with the hypothesis that it realizes the order there, because that is what it has to put into the condition. Soundness is handed the hypothesis at every value the table records there, because the condition it is reading may have bound a value of its own, and only a supplier that can realize whatever it finds can say what that value is. Either side is what the frame above hands over, Values read at one argument.
The body binds four sets and no more. Two of them are the compared members, whose pair is the argument, and two are their births. Then five conditions: each birth is the birth of its member, each birth lies below the stage, and the comparison itself, which is one membership atom between the two births, or, at a shared birth, the step. The stage arrives as a term rather than a slot, and that is not decoration: the separation the next chapter runs wants the whole condition at constants, and a term takes a constant without a binder, where a slot would cost one. Measured, that binder is the difference between 3 s and 160 s.
module Ordered (Stp : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n) (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-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 ⟩) where OrdBody : ∀ {n} → Term S n → Fin n → Formula S (suc (suc (suc (suc n)))) OrdBody tb f = BirthAt (suc zero) (sh3 zero) ∧̇ ( BirthAt zero (sh2 zero) ∧̇ ( (var (suc zero) ∈̇ tm4 tb) ∧̇ ( (var zero ∈̇ tm4 tb) ∧̇ ( (var (suc zero) ∈̇ var zero) ∨̇ ( (var zero ≐ var (suc zero)) ∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ) ) ) -- perf: the order description is sealed where it is built; unsealed, its two -- readings at the constants the separation wants run 160 s each instead of 2 s opaque CondCore : ∀ {n} → Fin n → Term S n → Fin n → Formula S n CondCore z tb f = ∃̇ ( ∃̇ ( prAtL (sh2 z) (suc zero) zero ∧̇ ∃̇ (∃̇ (OrdBody tb f)) ) )
What the description says, both ways
The reading takes the stage's ordinality and the table's two correctness conditions below it, which is exactly what the frame it feeds hands over. They are spent apart. Soundness spends correctness alone, at the birth of the compared member, and hands it to the step parameter as it stands. Completeness spends both through value: at a birth below the stage the table has a value, merely, and that value realizes the order there, so the parameter can be filled. Uniqueness is never wanted, because the step condition is a proposition and a merely-existing value may be opened into it.
module _ {n : ℕ} (z : Fin n) (tb : Term S n) (f : Fin n) (γ : S ^ n) (oα : IsOrd (fst (⟦ tb ⟧ γ))) (vals : Values (lookup f γ) (fst (⟦ tb ⟧ γ))) (ents : Entries (lookup f γ) (fst (⟦ tb ⟧ γ))) where private α : V ℓ α = fst (⟦ tb ⟧ γ) shift : (u v du dv : S) → ⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ) ≡ ⟦ tb ⟧ γ shift u v du dv = tm4-val tb u v du dv γ value : (d : S) → ⟨ fst d ∈ α ⟩ → (P : Ω) → ((r : S) → ⟨ pr (fst d) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst d) r → ⟨ P ⟩) → ⟨ P ⟩ value d hd P k = PT.rec (snd P) (λ { (r , hr) → k r hr (vals d r hd hr) }) (ents d hd) Deep : (u v du : S) → S → Type (ℓ-suc ℓ) Deep u v du dv = ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ OrdBody tb f ⟩ Mid : (u v : S) → S → Type (ℓ-suc ℓ) Mid u v du = ∥ (Σ[ dv ∈ S ] Deep u v du dv) ∥₁ Pair : (u : S) → S → Type (ℓ-suc ℓ) Pair u v = ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩ × ∥ (Σ[ du ∈ S ] Mid u v du) ∥₁ Top : S → Type (ℓ-suc ℓ) Top u = ∥ (Σ[ v ∈ S ] Pair u v) ∥₁
Soundness reads the four bound sets back. The pair equation identifies the argument; the two birth readings pin the two bound ordinals to the two members' births; bornIn turns the two memberships below the stage into membership in the stage, which is what the class quantifies over; and the comparison is then the family's own, along order-unfold. The description is sealed here, so nothing in this proof normalizes the sentence it is about.
opaque unfolding CondCore CondCore-out : ⟨ γ ⊨ CondCore z tb f ⟩ → ⟨ Related α (fst (lookup z γ)) ⟩ CondCore-out = PT.rec (snd (Related α (fst (lookup z γ)))) atTop where Goal : Type (ℓ-suc ℓ) Goal = ⟨ Related α (fst (lookup z γ)) ⟩ atDeep : (u v du dv : S) → ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩ → Deep u v du dv → Goal atDeep u v du dv hp (hbu , (hbv , (hmu₀ , (hmv₀ , hcmp)))) = subst (λ w → ⟨ Related α w ⟩) (sym qz) (PT.rec (snd (Related α (pr (fst u) (fst v)))) atCase hcmp) where qz : fst (lookup z γ) ≡ pr (fst u) (fst v) qz = subst ⟨_⟩ (prAtL-adequate (sh2 z) (suc zero) zero (v ∷ u ∷ γ)) hp hmu : ⟨ fst du ∈ α ⟩ hmu = subst (λ w → ⟨ fst du ∈ fst w ⟩) (shift u v du dv) hmu₀ hmv : ⟨ fst dv ∈ α ⟩ hmv = subst (λ w → ⟨ fst dv ∈ fst w ⟩) (shift u v du dv) hmv₀ odu : IsOrd (fst du) odu = mem-ord {A = α} oα (fst du) hmu odv : IsOrd (fst dv) odv = mem-ord {A = α} oα (fst dv) hmv qu : fst du ≡ birth (fst u) (snd u) qu = BirthAt-out (suc zero) (sh3 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) hbu odu qv : fst dv ≡ birth (fst v) (snd v) qv = BirthAt-out zero (sh2 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) hbv odv a : Mem (Lset α) a = fst u , bornIn α oα (fst u) (snd u) (subst (λ w → ⟨ w ∈ α ⟩) qu hmu) c : Mem (Lset α) c = fst v , bornIn α oα (fst v) (snd v) (subst (λ w → ⟨ w ∈ α ⟩) qv hmv) qa : bornOf α oα a ≡ fst du qa = birth-proof (fst u) (memberL α oα a) (snd u) ∙ sym qu qc : bornOf α oα c ≡ fst dv qc = birth-proof (fst v) (memberL α oα c) (snd v) ∙ sym qv fill : relOf (orderAt α oα) a c → ⟨ Related α (pr (fst u) (fst v)) ⟩ fill = related-in α oα a c atCase : ⟨ fst du ∈ fst dv ⟩ ⊎ ( (fst dv ≡ fst du) × ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ⟩ ) → ⟨ Related α (pr (fst u) (fst v)) ⟩ atCase (inl h) = fill (transport (sym (order-unfold α oα a c)) (inl (subst2 (λ p q → ⟨ p ∈ q ⟩) (sym qa) (sym qc) h))) atCase (inr (e , hs)) = PT.rec (snd (Related α (pr (fst u) (fst v)))) atUnder (stp-out (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) odu (λ r hr → vals du r hmu hr) hs) where atUnder : Under (fst du) (stepOrder (fst du) odu) (fst u) (fst v) → ⟨ Related α (pr (fst u) (fst v)) ⟩ atUnder und = fill (transport (sym (order-unfold α oα a c)) (inr (qc ∙ e ∙ sym qa , stepMoved (fst du) (bornOf α oα a) (sym qa) odu (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a)) (fst u) (fst v) und))) atMid : (u v du : S) → ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩ → Mid u v du → Goal atMid u v du hp = PT.rec (snd (Related α (fst (lookup z γ)))) (λ { (dv , hd) → atDeep u v du dv hp hd }) atPair : (u v : S) → Pair u v → Goal atPair u v (hp , hm) = PT.rec (snd (Related α (fst (lookup z γ)))) (λ { (du , hd) → atMid u v du hp hd }) hm atTop : Σ[ u ∈ S ] Top u → Goal atTop (u , h) = PT.rec (snd (Related α (fst (lookup z γ)))) (λ { (v , hv) → atPair u v hv }) h
Completeness fills them in. The class is unpacked to a pair of members and a comparison, the comparison is untruncated by strict, and the four witnesses are the two members and their two births, each sealed. The two-way split on the comparison is a named helper and never a with: as a with this one split alone runs past 300 s, because the abstraction it performs is over a satisfaction and the satisfaction is the largest term in the chapter.
private Pairs : IsOrd α → Type (ℓ-suc ℓ) Pairs o = Σ[ a ∈ Mem (Lset α) ] ∥ (Σ[ c ∈ Mem (Lset α) ] ( (fst (lookup z γ) ≡ pr (fst a) (fst c)) × ⟨ Ordering α o a c ⟩ )) ∥₁ CondCore-in : ⟨ Related α (fst (lookup z γ)) ⟩ → ⟨ γ ⊨ CondCore z tb f ⟩ CondCore-in = PT.rec (snd (γ ⊨ CondCore z tb f)) atOrd where atRel : (o : IsOrd α) (a c : Mem (Lset α)) → fst (lookup z γ) ≡ pr (fst a) (fst c) → ⟨ Ordering α o a c ⟩ → ⟨ γ ⊨ CondCore z tb f ⟩ atRel o a c q hord = value (bornS α oα pα a) hmu (γ ⊨ CondCore z tb f) atValue where pα : ⟨ isL α ⟩ pα = snd (⟦ tb ⟧ γ) u v du dv : S u = memS α oα a v = memS α oα c du = bornS α oα pα a dv = bornS α oα pα c hmu : ⟨ fst du ∈ α ⟩ hmu = subst (λ w → ⟨ w ∈ α ⟩) (sym (bornS-fst α oα pα a)) (bornMem α oα a) hmv : ⟨ fst dv ∈ α ⟩ hmv = subst (λ w → ⟨ w ∈ α ⟩) (sym (bornS-fst α oα pα c)) (bornMem α oα c) odu : IsOrd (fst du) odu = mem-ord {A = α} oα (fst du) hmu odv : IsOrd (fst dv) odv = mem-ord {A = α} oα (fst dv) hmv cmp : ⟨ bornOf α oα a ∈ bornOf α oα c ⟩ ⊎ ( (bornOf α oα c ≡ bornOf α oα a) × Under (bornOf α oα a) (stepOrder (bornOf α oα a) (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a))) (fst a) (fst c) ) cmp = transport (order-unfold α oα a c) (strict α oα a c (subst (λ o' → ⟨ Ordering α o' a c ⟩) (isPropIsOrd α o oα) hord)) hp : ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩ hp = subst ⟨_⟩ (sym (prAtL-adequate (sh2 z) (suc zero) zero (v ∷ u ∷ γ))) (q ∙ cong₂ pr (sym (memS-fst α oα a)) (sym (memS-fst α oα c))) hbu : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ BirthAt (suc zero) (sh3 zero) ⟩ hbu = BirthAt-in (suc zero) (sh3 zero) (dv ∷ du ∷ v ∷ u ∷ γ) odu (bornS-birth α oα pα a) hbv : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ BirthAt zero (sh2 zero) ⟩ hbv = BirthAt-in zero (sh2 zero) (dv ∷ du ∷ v ∷ u ∷ γ) odv (bornS-birth α oα pα c) moved : Under (bornOf α oα a) (stepOrder (bornOf α oα a) (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a))) (fst a) (fst c) → Under (fst du) (stepOrder (fst du) odu) (fst u) (fst v) moved und = subst2 (λ p r → Under (fst du) (stepOrder (fst du) odu) p r) (sym (memS-fst α oα a)) (sym (memS-fst α oα c)) (stepMoved (bornOf α oα a) (fst du) (sym (bornS-fst α oα pα a)) (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a)) odu (fst a) (fst c) und) atValue : (r : S) → ⟨ pr (fst du) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst du) r → ⟨ γ ⊨ CondCore z tb f ⟩ atValue r hr hrel = ∣ u , ∣ v , (hp , ∣ du , ∣ dv , (hbu , (hbv , (hmu₀ , (hmv₀ , side)))) ∣₁ ∣₁) ∣₁ ∣₁ where hmu₀ : ⟨ fst du ∈ fst (⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ)) ⟩ hmu₀ = subst (λ w → ⟨ fst du ∈ fst w ⟩) (sym (shift u v du dv)) hmu hmv₀ : ⟨ fst dv ∈ fst (⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ)) ⟩ hmv₀ = subst (λ w → ⟨ fst dv ∈ fst w ⟩) (sym (shift u v du dv)) hmv -- perf: law of the route: a two-way split concluding in a -- satisfaction is a named helper, never a `with`; as a `with` this -- one alone runs past 300 s atCmp : ⟨ bornOf α oα a ∈ bornOf α oα c ⟩ ⊎ ( (bornOf α oα c ≡ bornOf α oα a) × Under (bornOf α oα a) (stepOrder (bornOf α oα a) (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a))) (fst a) (fst c) ) → ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ ( (var (suc zero) ∈̇ var zero) ∨̇ ( (var zero ≐ var (suc zero)) ∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ⟩ atCmp (inl h) = ∣ inl (subst2 (λ p q → ⟨ p ∈ q ⟩) (sym (bornS-fst α oα pα a)) (sym (bornS-fst α oα pα c)) h) ∣₁ atCmp (inr (e , und)) = ∣ inr ( bornS-fst α oα pα c ∙ e ∙ sym (bornS-fst α oα pα a) , stp-in (suc zero) (sh4 f) (sh3 zero) (sh2 zero) (dv ∷ du ∷ v ∷ u ∷ γ) odu r hr hrel (moved und) ) ∣₁ side : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ ( (var (suc zero) ∈̇ var zero) ∨̇ ( (var zero ≐ var (suc zero)) ∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ⟩ side = atCmp cmp atPairs : (o : IsOrd α) → Pairs o → ⟨ γ ⊨ CondCore z tb f ⟩ atPairs o (a , h) = PT.rec (snd (γ ⊨ CondCore z tb f)) (λ { (c , (q , hord)) → atRel o a c q hord }) h atOrd : Σ[ o ∈ IsOrd α ] ∥ Pairs o ∥₁ → ⟨ γ ⊨ CondCore z tb f ⟩ atOrd (o , h) = PT.rec (snd (γ ⊨ CondCore z tb f)) (atPairs o) h CondCore-spec : (γ ⊨ CondCore z tb f) ≡ Related α (fst (lookup z γ)) CondCore-spec = ⇔toPath CondCore-out CondCore-in
The frame's two hypotheses, discharged
The previous chapter asked for the condition 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. Both are the same body. At slots the stage is the term var b and nothing is bound; at constants the stage is the term con B and only the table is bound, by one existential, which the equation at that binder pins.
With those two filled, Described applies, and everything it proves is available here: the approximation, the graph, the table at every ordinal, the relation at every stage as an element of L, and its membership read at both shapes a member of a stage comes in. All of it is conditional on the step parameter, and on nothing else.
Cond : ∀ {n} → Fin n → Fin n → Formula S (suc n) Cond b f = CondCore zero (var (suc b)) (suc f) Cond₀ : S → S → Formula S 1 Cond₀ B F = ∃̇ ( (var zero ≐ con F) ∧̇ CondCore (suc zero) (con B) zero ) 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 γ ob vals ents z = CondCore-spec zero (var (suc b)) (suc f) (z ∷ γ) ob vals ents module _ (B F : S) (oB : IsOrd (fst B)) (vals : Values F (fst B)) (ents : Entries F (fst B)) (z : S) where private Held : S → Type (ℓ-suc ℓ) Held c = (fst c ≡ fst F) × ⟨ (c ∷ z ∷ []) ⊨ CondCore (suc zero) (con B) zero ⟩ cond₀-out : ⟨ (z ∷ []) ⊨ Cond₀ B F ⟩ → ⟨ Related (fst B) (fst z) ⟩ cond₀-out = PT.rec (snd (Related (fst B) (fst z))) atHeld where atHeld : Σ[ c ∈ S ] Held c → ⟨ Related (fst B) (fst z) ⟩ atHeld (c , (qc , hc)) = CondCore-out (suc zero) (con B) zero (c ∷ z ∷ []) oB (λ x r hx hp → vals x r hx (subst (λ w → ⟨ pr (fst x) (fst r) ∈ w ⟩) qc hp)) (λ x hx → PT.map (λ { (r , hr) → r , subst (λ w → ⟨ pr (fst x) (fst r) ∈ w ⟩) (sym qc) hr }) (ents x hx)) hc cond₀-in : ⟨ Related (fst B) (fst z) ⟩ → ⟨ (z ∷ []) ⊨ Cond₀ B F ⟩ cond₀-in h = ∣ F , (refl , CondCore-in (suc zero) (con B) zero (F ∷ z ∷ []) oB vals ents h) ∣₁ 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) cond₀-spec B F oB vals ents z = ⇔toPath (cond₀-out B F oB vals ents z) (cond₀-in B F oB vals ents z) open Described Cond Cond₀ cond-spec cond₀-spec public
Recap
BirthAt is the birth stage described in the object language, with no successor operation and no constant named: the tower at the slot does not hold the set, and the definable powerset of that tower does. BirthAt-out and
BirthAt-in are its two readings at variable slots, ordinality at the ordinal slot being the only hypothesis, and the two elements it is satisfied at are sealed, at a measured 178 s against 2 s.
isCodeAnyAt is the code predicate at any arity over a carrier held in a slot, and it is an instantiation rather than a construction: the arity-bound conjunct and the witness conjunct both already existed, one in the code set chapter and one in the powerset chapter, and only their meeting is new.
CodesAt is the set they cut out, one extAt, and
CodesAt-out and CodesAt-in pin the slot to the code set over the carrier in both directions, so the naming description's code-set slot can be pinned by description instead of by an outside equation. That is the third obligation.
order-unfold is the order family's defining equation at a stage, one
cong over the recursion's computation rule; bornIn is the converse of birth-in, and it is what buys the description one binder less;
stepMoved carries a step comparison along an equality of carriers, rebuilt here rather than reached for.
CondCore is the order at a stage described in full, birth-primary, generic in the step condition. It binds four sets, takes the stage as a term so that the constant form costs no binder, and it is sealed where it is built: unsealed, each of its two readings at constants runs 160 s. CondCore-out and
CondCore-in are its two halves, and Cond, Cond₀,
cond-spec and cond₀-spec are the two forms the previous chapter's frame asked for, together with their meanings. With them, Described applies.
What is not here is the step's own adequacy: L.Choice.Internal's
with stp-out and stp-in as its meaning, the first taking the table's correctness at every value recorded at the carrier and the second a single value that realizes the order there, and it is a chapter of bookkeeping against chapters that exist: the parameter sequence read back as a vector, the denotation identified with the meta name's, the least of the description's names identified with the least of the meta ones. The frame's two hypotheses are gone; this one is what stands between the construction and an unconditional theorem.