The set of fixed-length environments

Read this chapter directly, or use the reading guide and dependency map to choose another route.

Reading guide · Dependency map

For a constructible set B and a natural number n, this chapter constructs an element envSet n of L whose members are exactly the length-n environments with values in B.

The chapter that wrote the ten clauses said what it means for one thing to be an environment over a set, and set aside the question of whether all of them together form a set. This chapter answers it: the satisfaction predicates will be separated from this common set of environments.

The route is the one the axioms already provide. 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, and separating that stage by the description gives exactly them. Nothing here needs replacement, and nothing here needs recursion.

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Coding.EnvironmentSet {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _≐_; _∧̇_; ∃̇_ )
import FOL.Absoluteness
import FOL.ZFModel
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.CodeConstructibility {ℓ} using ( envL )
open import L.Coding.Model {ℓ} using ( envOverAt; svAt; domAt; valuesInAt; pairsInAt; inDomAt; prʟ; prʟ-fst; 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 L.Coding.Expressions {ℓ} using ( numL )

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 hPropStructure 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

A stage under a small family

stageFor finds one ordinal stage containing every member of any small family of constructible sets, providing the common ambient stage needed by separation.

The move smallDom makes, with the ordinal kept rather than hidden, because what is needed 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

For each g : Fin n → ⟪ B ⟫, envSL proves that its finite graph is constructible, so the packaged envS g can be bounded by stageFor.

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

Separating the environment set

envFo n specializes envOverAt to the fixed length n and base set B; separation in the common stage defines envSet n and its membership equation.

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

For g : Fin n → ⟪ B ⟫, the proof checks that its graph is single-valued, has domain n, and contains exactly the required values and pairs, hence belongs to envSet n.

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)) ∣₁ ∣₁

Recovering an environment from a member

Conversely, the four envOverAt clauses for a member x determine a function g : Fin n → ⟪ B ⟫, and extensionality identifies x with envS g.

The other direction is what four clauses need when they read a bound variable off an environment, and seven further clauses use it 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 recognize that description as this set. Both uses come from the same recovery, which is why it takes the environment and the three slots as parameters rather than fixing them: a clause places them where its own frame places them, not where this chapter would. A set satisfying the description is the graph of a function, and recovering that function is the only place the four conjuncts must work together: the domain conjunct says every index below the length has an entry, and single-valuedness says there is at most one, so the existence of that entry is a proposition and the truncation given by the domain conjunct can be eliminated. Membership then names the index, which is untruncated because the fibers of a set's own indexing are.

Extensionality completes the proof: one direction comes from the entries and the other from the pairs conjunct, which is the conjunct without which unwanted elements could enter.

  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

The two directions specify envSet n: membership is equivalent to being the graph of a length-n assignment into B, so later constructions can quantify over environments inside L.

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.