BedrockThe environments over a set form a set
The chapter that wrote the twelve clauses said what it means for one thing to be an environment over a set, and disowned the question of whether all of them together form a set. This chapter answers it, and the answer is owed: the clause for negation takes a complement, and a complement is taken inside something.
The route is the one the axioms already sell. Environments over a set of L at a fixed length are indexed by a small type, each is an element of L, so they all lie below one stage; carving that stage by the description gives exactly them. Nothing here needs replacement, and nothing here needs a recursion.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Coding.EnvSet {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _≐_; _∧̇_; ∃̇_ ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV ) open import V.Coding {ℓ} using ( pr; #-inj′ ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono ) open import L.Ordinal {ℓ} using ( boundingOrd; ∈#-elim ) open import V.Coding {ℓ} using ( #mono; pr-inj ) open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem ) open import L.Axioms.Basic {ℓ} using ( LsetS ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL ) open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst ) open import L.Coding.Environment {ℓ} using ( env ) open import L.Coding.InL {ℓ} using ( envL ) open import L.Coding.Model {ℓ} using ( envOverAt; svAt; domAt; valuesInAt; pairsInAt; inDomAt ; prʟ; prʟ-fst; numL; svAt-in; svAt-out; inDomAt-adequate ; appAt-adequate; domAt-in; valuesInAt-out ; envOver-sv; envOver-dom; envOver-values; envOver-pairs ; pairsIn-in; pairsIn-out ) open import Cubical.Data.FinData using ( toℕ; inj-toℕ ) open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' ) open import Cubical.Data.Sigma using ( Σ≡Prop ) open import Cubical.Functions.Logic using ( ⇔toPath ) 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 import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_ ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
A stage under a small family
The move smallDom makes, with the ordinal kept rather than hidden, because what wants it here is a lemma stated about stages rather than about a set of the model.
stageFor : (X : Type ℓ) (f : X → S) → Σ[ β ∈ V ℓ ] (IsOrd β × ((x : X) → ⟨ fst (f x) ∈ Lset β ⟩)) stageFor X f = β , (oβ , mem) where b = boundingOrd X (λ x → stage (fst (f x)) (f x .snd)) (λ x → stage-ord (fst (f x)) (f x .snd)) β = b .fst oβ : IsOrd β oβ = b .snd .fst mem : (x : X) → ⟨ fst (f x) ∈ Lset β ⟩ mem x = Lset-mono {α = β} {β = stage (fst (f x)) (f x .snd)} (b .snd .snd x) (stage-mem (fst (f x)) (f x .snd))
One environment, as an element of the model
An environment over a set of L is a finite set of pairs of a numeral with a member, and a member of an element of L is an element of L, so the pairs are too and the stage lemma above closes it.
module _ (B : S) where private ix : ⟪ fst B ⟫ → S ix m = ⟪ fst B ⟫↪ m , isL-trans (∈∈ₛ {a = ⟪ fst B ⟫↪ m} {b = fst B} .snd (∈ₛ⟪ fst B ⟫↪ m)) (snd B) Ix : ℕ → Type ℓ Ix n = Fin n → ⟪ fst B ⟫ opaque envSL : {n : ℕ} (g : Ix n) → ⟨ isL (env (λ i → fst (ix (g i)))) ⟩ envSL {n} g = envL β oβ (λ i → fst (ix (g i))) mem where pairs : Lift {ℓ-zero} {ℓ} (Fin n) → S pairs i = prʟ (numeralL (toℕ (lower i))) (ix (g (lower i))) sf : Σ[ b ∈ V ℓ ] (IsOrd b × ((i : Lift {ℓ-zero} {ℓ} (Fin n)) → ⟨ fst (pairs i) ∈ Lset b ⟩)) sf = stageFor (Lift {ℓ-zero} {ℓ} (Fin n)) pairs β : V ℓ β = sf .fst oβ : IsOrd β oβ = sf .snd .fst mem : (i : Fin n) → ⟨ pr (# (toℕ i)) (fst (ix (g i))) ∈ Lset β ⟩ mem i = subst (λ w → ⟨ w ∈ Lset β ⟩) (prʟ-fst (numeralL (toℕ i)) (ix (g i)) ∙ cong₂ pr (numeralL-fst (toℕ i)) refl) (sf .snd .snd (lift i)) envS : {n : ℕ} → Ix n → S envS g = env (λ i → fst (ix (g i))) , envSL g
The set
The description takes three arguments and separation offers one variable, so the other two are bound and pinned to constants. That is three lines and it keeps the description as the chapter wrote it, which is worth more than saving them.
private nn : ℕ → S nn k = # k , numL k envFo : (n : ℕ) → Formula S 1 envFo n = ∃̇ (∃̇ ( (var (suc zero) ≐ con (nn n)) ∧̇ ((var zero ≐ con B) ∧̇ envOverAt (suc (suc zero)) (suc zero) zero) )) private sf : (n : ℕ) → Σ[ β ∈ V ℓ ] (IsOrd β × ((g : Ix n) → ⟨ fst (envS g) ∈ Lset β ⟩)) sf n = stageFor (Ix n) envS amb : (n : ℕ) → S amb n = LsetS (sf n .fst) (sf n .snd .fst) opaque envSet : (n : ℕ) → S envSet n = hasSeparationL (amb n) (envFo n) .fst .fst envSet-mem : (n : ℕ) (x : S) → (x ∈ˢ envSet n) ≡ ((x ∈ˢ amb n) ⊓ ((x ∷ []) ⊨ envFo n)) envSet-mem n = hasSeparationL (amb n) (envFo n) .fst .snd
Every environment is in it
Four conjuncts, and each is the description read against what an environment actually is. Single-valuedness and the two containments come straight off the membership specification, which is refl; the domain is the only one that does arithmetic, because saying the domain is the numeral n means saying that the indices below n are exactly the numerals below n.
module _ {n : ℕ} (g : Ix n) where private out : (s : V ℓ) → ⟨ s ∈ fst (envS g) ⟩ → ∥ (Σ[ i ∈ Fin n ] (pr (# (toℕ i)) (fst (ix (g i))) ≡ s)) ∥₁ out s = PT.map (λ { (li , e) → lower li , e }) into : (i : Fin n) → ⟨ pr (# (toℕ i)) (fst (ix (g i))) ∈ fst (envS g) ⟩ into i = ∣ lift i , refl ∣₁ val∈ : (i : Fin n) → ⟨ fst (ix (g i)) ∈ fst B ⟩ val∈ i = ∈∈ₛ {a = ⟪ fst B ⟫↪ (g i)} {b = fst B} .snd (∈ₛ⟪ fst B ⟫↪ (g i)) δ : S ^ 3 δ = B ∷ nn n ∷ envS g ∷ [] E : Fin 3 E = suc (suc zero) envOver : ⟨ δ ⊨ envOverAt E (suc zero) zero ⟩ envOver = sv , (dom , (vals , pairs)) where sv : ⟨ δ ⊨ svAt E ⟩ sv = svAt-in E δ (λ x y y' p q → PT.rec (setIsSet (fst y) (fst y')) (λ { (i , ei) → PT.rec (setIsSet (fst y) (fst y')) (λ { (j , ej) → sym (pr-inj ei .snd) ∙ cong (λ k → fst (ix (g k))) (inj-toℕ (#-inj′ (pr-inj ei .fst ∙ sym (pr-inj ej .fst)))) ∙ pr-inj ej .snd }) (out (pr (fst x) (fst y')) q) }) (out (pr (fst x) (fst y)) p)) dom : ⟨ δ ⊨ domAt E (suc zero) ⟩ dom x = fwd , bwd where fwd : ⟨ (x ∷ δ) ⊨ inDomAt (suc E) zero ⟩ → ⟨ fst x ∈ (# n) ⟩ fwd hd = PT.rec (snd (fst x ∈ (# n))) (λ { (y , p) → PT.rec (snd (fst x ∈ (# n))) (λ { (i , ei) → subst (λ w → ⟨ w ∈ (# n) ⟩) (pr-inj ei .fst) (#mono (toℕ i) n (toℕ<n i)) }) (out (pr (fst x) (fst y)) p) }) (subst ⟨_⟩ (inDomAt-adequate (suc E) zero (x ∷ δ)) hd) bwd : ⟨ fst x ∈ (# n) ⟩ → ⟨ (x ∷ δ) ⊨ inDomAt (suc E) zero ⟩ bwd hx = subst ⟨_⟩ (sym (inDomAt-adequate (suc E) zero (x ∷ δ))) (PT.map (λ { (m , m<n , e) → ix (g (fromℕ' n m m<n)) , subst (λ w → ⟨ pr w (fst (ix (g (fromℕ' n m m<n)))) ∈ fst (envS g) ⟩) (cong #_ (toFromId' n m m<n) ∙ sym e) (into (fromℕ' n m m<n)) }) (∈#-elim n (fst x) hx)) vals : ⟨ δ ⊨ valuesInAt E zero ⟩ vals x y hp = PT.rec (snd (fst y ∈ fst B)) (λ { (i , ei) → subst (λ w → ⟨ w ∈ fst B ⟩) (pr-inj ei .snd) (val∈ i) }) (out (pr (fst x) (fst y)) (subst ⟨_⟩ (appAt-adequate (suc (suc E)) (suc zero) zero (y ∷ x ∷ δ)) hp)) pairs : ⟨ δ ⊨ pairsInAt E (suc zero) zero ⟩ pairs = pairsIn-in E (suc zero) zero δ (λ s s∈ → PT.map (λ { (i , ei) → nn (toℕ i) , ( ix (g i) , ( #mono (toℕ i) n (toℕ<n i) , (val∈ i , sym ei) ) ) }) (out (fst s) s∈)) envSetIn : ⟨ (envS g ∷ []) ⊨ envFo n ⟩ envSetIn = ∣ nn n , ∣ B , (refl , (refl , envOver)) ∣₁ ∣₁
And every member of it is one
The other direction, which is what four clauses want when they read a bound variable off an environment, and which seven want in a weaker form: a clause binds its own ambient set and says only that its members are the environments, so a proof that consumes the clause has to turn that description back into this set. Both uses are the same recovery, which is why it takes the environment and the three slots as parameters rather than fixing them: a clause puts them where its own frame puts them, not where this chapter would. A set that satisfies the description is the graph of a function, and recovering the function is the only place the four conjuncts have to work together: the domain conjunct says every index below the length has an entry, single-valuedness says at most one, so the entry is a proposition and the truncation the domain gives comes off. Membership then names the index, which is untruncated because the fibers of a set's own indexing are.
Extensionality closes it, one direction from the entries and the other from the pairs conjunct, which is the conjunct whose absence would have let junk in.
module Recover (n : ℕ) {k : ℕ} (γ : S ^ k) (Ei di bi : Fin k) (qd : fst (lookup di γ) ≡ # n) (qb : fst (lookup bi γ) ≡ fst B) (h : ⟨ γ ⊨ envOverAt Ei di bi ⟩) where private e : S e = lookup Ei γ Entry : Fin n → Type (ℓ-suc ℓ) Entry i = Σ[ y ∈ S ] ⟨ pr (# (toℕ i)) (fst y) ∈ fst e ⟩ isPropEntry : (i : Fin n) → isProp (Entry i) isPropEntry i (y , p) (y' , p') = Σ≡Prop (λ w → snd (pr (# (toℕ i)) (fst w) ∈ fst e)) (Σ≡Prop (λ v → snd (isL v)) (svAt-out Ei γ (envOver-sv Ei di bi γ h) (nn (toℕ i)) y y' p p')) entry : (i : Fin n) → Entry i entry i = PT.rec (isPropEntry i) (λ z → z) (domAt-in Ei di γ (envOver-dom Ei di bi γ h) (nn (toℕ i)) (subst (λ z → ⟨ (# (toℕ i)) ∈ z ⟩) (sym qd) (#mono (toℕ i) n (toℕ<n i)))) fib : (i : Fin n) → Σ[ m ∈ ⟪ fst B ⟫ ] (⟪ fst B ⟫↪ m ≡ fst (entry i .fst)) fib i = ∈-asFiber {a = fst (entry i .fst)} {b = fst B} (subst (λ z → ⟨ fst (entry i .fst) ∈ z ⟩) qb (valuesInAt-out Ei bi γ (envOver-values Ei di bi γ h) (nn (toℕ i)) (entry i .fst) (entry i .snd))) g : Ix n g i = fib i .fst private val≡ : (i : Fin n) → fst (ix (g i)) ≡ fst (entry i .fst) val≡ i = fib i .snd fwd : (w : V ℓ) → ⟨ w ∈ fst (envS g) ⟩ → ⟨ w ∈ fst e ⟩ fwd w = PT.rec (snd (w ∈ fst e)) (λ { (li , q) → subst (λ z → ⟨ z ∈ fst e ⟩) (cong (pr (# (toℕ (lower li)))) (sym (val≡ (lower li))) ∙ q) (entry (lower li) .snd) }) bwd : (w : V ℓ) → ⟨ w ∈ fst e ⟩ → ⟨ w ∈ fst (envS g) ⟩ bwd w hw = PT.rec squash₁ (λ { (u , (v , (u∈ , (v∈ , eq)))) → PT.rec squash₁ (λ { (m , (m<n , um)) → let i = fromℕ' n m m<n iu : # (toℕ i) ≡ fst u iu = cong #_ (toFromId' n m m<n) ∙ sym um hv : ⟨ pr (# (toℕ i)) (fst v) ∈ fst e ⟩ hv = subst (λ z → ⟨ z ∈ fst e ⟩) (eq ∙ cong (λ z → pr z (fst v)) (sym iu)) hw same : fst v ≡ fst (entry i .fst) same = svAt-out Ei γ (envOver-sv Ei di bi γ h) (nn (toℕ i)) v (entry i .fst) hv (entry i .snd) in ∣ lift i , cong (pr (# (toℕ i))) (val≡ i ∙ sym same) ∙ cong (λ z → pr z (fst v)) iu ∙ sym eq ∣₁ }) (∈#-elim n (fst u) (subst (λ z → ⟨ fst u ∈ z ⟩) qd u∈)) }) (pairsIn-out Ei di bi γ (envOver-pairs Ei di bi γ h) (w , isL-trans {x = fst e} {y = w} hw (snd e)) hw) recovers : fst e ≡ fst (envS g) recovers = extensionalV (λ w → ⇔toPath (bwd w) (fwd w)) envSet-in : {n : ℕ} (g : Ix n) → ⟨ envS g ∈ˢ envSet n ⟩ envSet-in {n} g = subst ⟨_⟩ (sym (envSet-mem n (envS g))) (sf n .snd .snd g , envSetIn g) envSet-out : (n : ℕ) (x : S) → ⟨ x ∈ˢ envSet n ⟩ → ∥ (Σ[ g ∈ Ix n ] (fst x ≡ fst (envS g))) ∥₁ envSet-out n x hx = PT.rec squash₁ (λ { (d , hd) → PT.map (λ { (b , (qd , (qb , hov))) → Recover.g n (b ∷ d ∷ x ∷ []) (suc (suc zero)) (suc zero) zero qd qb hov , Recover.recovers n (b ∷ d ∷ x ∷ []) (suc (suc zero)) (suc zero) zero qd qb hov }) hd }) (subst ⟨_⟩ (envSet-mem n x) hx .snd)
Recap
envSet is the ambient set the negative clauses take their complements in, and it reads both ways: envSet-in puts every environment over the carrier into it, envSet-out recovers from any member the function whose graph it is. The second is what four clauses want when they read a bound variable off an environment, and it is the one that needed all four conjuncts of the description at once.
Two measurements, and the second is a sharper form of a rule the development already had. Proving the fourth conjunct with the environment written out did not finish in ten minutes; proving the same statement as a lemma whose environment is a variable, then applying it, takes no measurable time. A satisfaction substitution along an adequacy equation must be discharged where the arguments are variables: at concrete elements it drags the whole absoluteness bridge through normalization, and the elements' constructibility certificates with it. Sealing the certificate at the construction site was necessary and not sufficient. The recovery is written the same way, with the description's two constant slots left as parameters constrained by equations rather than written in, so that nothing substitutes underneath a satisfaction at a concrete environment.