The set of fixed-length environments

Fix a universe level ℓ and assume lem : LEM (ℓ-suc ℓ). This hypothesis supplies a decision for each proposition at that level; it remains an explicit parameter of the constructions below.

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

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.

open import Cubical.Data.FinData using ( inj-toℕ )

open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )
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 hPropView 𝒮ʟ

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) → ⟨ (f x) .fst ∈ Lset β ⟩))
stageFor X f = β , (oβ , mem)
  where
  b = boundingOrd X (λ x → stage ((f x) .fst) (f x .snd))
        (λ x → stage-ord ((f x) .fst) (f x .snd))
  β = b .fst
  oβ : IsOrd β
  oβ = b .snd .fst
  mem : (x : X) → ⟨ (f x) .fst ∈ Lset β ⟩
  mem x = Lset-mono {α = β} {β = stage ((f x) .fst) (f x .snd)} (b .snd .snd x)
            (stage-mem ((f x) .fst) (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 : ⟪ B .fst ⟫ → S
  ix m = ⟪ B .fst ⟫↪ m
       , isL-trans (∈∈ₛ {a = ⟪ B .fst ⟫↪ m} {b = B .fst} .snd (∈ₛ⟪ B .fst ⟫↪ m))
           (B .snd)

Ix : ℕ → Type ℓ
Ix n = Fin n → ⟪ B .fst ⟫

opaque
  envSL : {n : ℕ} (g : Ix n) → ⟨ isL (env (λ i → (ix (g i)) .fst)) ⟩
  envSL {n} g = envL β oβ (λ i → (ix (g i)) .fst) 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)) → ⟨ (pairs i) .fst ∈ 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)) ((ix (g i)) .fst) ∈ 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 → (ix (g i)) .fst) , envSL g

private
  nn : ℕ → S
  nn k = # k , numL k

envFo : (n : ℕ) → Formula S 
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) → ⟨ (envS g) .fst ∈ 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

module _ {n : ℕ} (g : Ix n) where

private
  out : (s : V ℓ) → ⟨ s ∈ (envS g) .fst ⟩
      → ∥ (Σ[ i ∶ Fin n ] (pr (# (toℕ i)) ((ix (g i)) .fst) ≡ s)) ∥₁
  out s = map₁ (λ { (li , e) → lower li , e })

  into : (i : Fin n) → ⟨ pr (# (toℕ i)) ((ix (g i)) .fst) ∈ (envS g) .fst ⟩
  into i = ∣ lift i , refl ∣₁

  val∈ : (i : Fin n) → ⟨ (ix (g i)) .fst ∈ B .fst ⟩
  val∈ i = ∈∈ₛ {a = ⟪ B .fst ⟫↪ (g i)} {b = B .fst} .snd (∈ₛ⟪ B .fst ⟫↪ (g i))

  δ : Vec S 
  δ = B ∷ nn n ∷ envS g ∷ []

  E : Fin 
  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 →
    rec₁ (setIsSet (y .fst) (y' .fst))
      (λ { (i , ei) → rec₁ (setIsSet (y .fst) (y' .fst))
        (λ { (j , ej) → sym (pr-inj ei .snd)
           ∙ cong (λ k → (ix (g k)) .fst)
               (inj-toℕ (#-inj′ (pr-inj ei .fst ∙ sym (pr-inj ej .fst))))
           ∙ pr-inj ej .snd })
        (out (pr (x .fst) (y' .fst)) q) })
      (out (pr (x .fst) (y .fst)) p))

  dom : ⟨ δ ⊨ domAt E (suc zero) ⟩
  dom x = fwd , bwd
    where
    fwd : ⟨ (x ∷ δ) ⊨ inDomAt (suc E) zero ⟩ → ⟨ x .fst ∈ (# n) ⟩
    fwd hd = rec₁ ((x .fst ∈ (# n)) .snd)
      (λ { (y , p) → rec₁ ((x .fst ∈ (# n)) .snd)
        (λ { (i , ei) → subst (λ w → ⟨ w ∈ (# n) ⟩) (pr-inj ei .fst)
               (#mono (toℕ i) n (toℕ<n i)) })
        (out (pr (x .fst) (y .fst)) p) })
      (subst ⟨_⟩ (inDomAt-adequate (suc E) zero (x ∷ δ)) hd)

    bwd : ⟨ x .fst ∈ (# n) ⟩ → ⟨ (x ∷ δ) ⊨ inDomAt (suc E) zero ⟩
    bwd hx = subst ⟨_⟩ (sym (inDomAt-adequate (suc E) zero (x ∷ δ)))
      (map₁
        (λ { (m , m<n , e) →
          ix (g (fromℕ' n m m<n))
          , subst (λ w → ⟨ pr w ((ix (g (fromℕ' n m m<n))) .fst)
                             ∈ (envS g) .fst ⟩)
              (cong #_ (toFromId' n m m<n) ∙ sym e) (into (fromℕ' n m m<n)) })
        (∈#-elim n (x .fst) hx))

  vals : ⟨ δ ⊨ valuesInAt E zero ⟩
  vals x y hp = rec₁ ((y .fst ∈ B .fst) .snd)
    (λ { (i , ei) → subst (λ w → ⟨ w ∈ B .fst ⟩) (pr-inj ei .snd) (val∈ i) })
    (out (pr (x .fst) (y .fst))
      (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∈ → map₁
      (λ { (i , ei) → nn (toℕ i)
         , ( ix (g i)
           , ( #mono (toℕ i) n (toℕ<n i) , (val∈ i , sym ei) ) ) })
      (out (s .fst) s∈))

envSetIn : ⟨ (envS g ∷ []) ⊨ envFo n ⟩
envSetIn = ∣ nn n , ∣ B , (refl , (refl , envOver)) ∣₁ ∣₁

module Recover (n : ℕ) {k : ℕ} (γ : Vec S k) (Ei di bi : Fin k)
  (qd : (lookup di γ) .fst ≡ # n) (qb : (lookup bi γ) .fst ≡ B .fst)
  (h : ⟨ γ ⊨ envOverAt Ei di bi ⟩)
  where

private
  e : S
  e = lookup Ei γ

  Entry : Fin n → Type (ℓ-suc ℓ)
  Entry i = Σ[ y ∶ S ] ⟨ pr (# (toℕ i)) (y .fst) ∈ e .fst ⟩

  isPropEntry : (i : Fin n) → isProp (Entry i)
  isPropEntry i (y , p) (y' , p') =
    Σ≡Prop (λ w → (pr (# (toℕ i)) (w .fst) ∈ e .fst) .snd)
      (Σ≡Prop (λ v → (isL v) .snd)
        (svAt-out Ei γ (envOver-sv Ei di bi γ h)
          (nn (toℕ i)) y y' p p'))

  entry : (i : Fin n) → Entry i
  entry i = 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 ∶ ⟪ B .fst ⟫ ] (⟪ B .fst ⟫↪ m ≡ (entry i .fst) .fst)
  fib i = ∈-asFiber {a = (entry i .fst) .fst} {b = B .fst}
    (subst (λ z → ⟨ (entry i .fst) .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) → (ix (g i)) .fst ≡ (entry i .fst) .fst
  val≡ i = fib i .snd

  fwd : (w : V ℓ) → ⟨ w ∈ (envS g) .fst ⟩ → ⟨ w ∈ e .fst ⟩
  fwd w = rec₁ ((w ∈ e .fst) .snd)
    (λ { (li , q) → subst (λ z → ⟨ z ∈ e .fst ⟩)
           (cong (pr (# (toℕ (lower li)))) (sym (val≡ (lower li))) ∙ q)
           (entry (lower li) .snd) })

  bwd : (w : V ℓ) → ⟨ w ∈ e .fst ⟩ → ⟨ w ∈ (envS g) .fst ⟩
  bwd w hw = rec₁ squash₁
    (λ { (u , (v , (u∈ , (v∈ , eq)))) → rec₁ squash₁
      (λ { (m , (m<n , um)) →
        let i = fromℕ' n m m<n
            iu : # (toℕ i) ≡ u .fst
            iu = cong #_ (toFromId' n m m<n) ∙ sym um
            hv : ⟨ pr (# (toℕ i)) (v .fst) ∈ e .fst ⟩
            hv = subst (λ z → ⟨ z ∈ e .fst ⟩)
                   (eq ∙ cong (λ z → pr z (v .fst)) (sym iu)) hw
            same : v .fst ≡ (entry i .fst) .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 (v .fst)) iu ∙ sym eq ∣₁ })
      (∈#-elim n (u .fst) (subst (λ z → ⟨ u .fst ∈ z ⟩) qd u∈)) })
    (pairsIn-out Ei di bi γ
      (envOver-pairs Ei di bi γ h)
      (w , isL-trans {x = e .fst} {y = w} hw (e .snd)) hw)

recovers : e .fst ≡ (envS g) .fst
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 ] (x .fst ≡ (envS g) .fst)) ∥₁
envSet-out n x hx = rec₁ squash₁
  (λ { (d , hd) → 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.