BedrockEnvironments as sets
A certificate that talks about satisfaction has to talk about environments, and an environment is a function from variable indices to sets. Functions are not sets of the hierarchy, so this chapter encodes them: an environment becomes its graph, the set of pairs of an index with the value there.
The encoding pays off immediately, because the index side is a numeral and the previous chapter already made numerals injective. So the graph really is a function graph: at the key for i there sits exactly the value at i, and nothing else. That lemma is the whole point of the chapter, and the atomic clause of a satisfaction certificate is where it gets spent.
Two more readers follow, for the two things a certificate does with an environment: look a value up, and extend the environment when it goes under a quantifier. Extension is von Neumann successor at the index side, so the second reader characterizes the successor. The chapter closes with the set of all finite sequences over a given set, which is the canonical place an environment lives when a certificate has to quantify over environments rather than exhibit one.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth module L.Coding.Environment {ℓ : Level} where open import FOL.Syntax using ( var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; ∀̇∈; ∃̇∈ ) open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-∀∈; δ-∃∈ ) import FOL.Semantics open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Model {ℓ} using ( self∈sucV; ∈sucV-inl; ∈sucV-elim ) open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′ ) open import L.Coding.Base {ℓ} using ( prAt; Δ₀-prAt; prAt-adequate; tagAt; Δ₀-tagAt; tagAt-adequate ; ∈pair-introL; ∈pair-introR ) import Cubical.Data.Sum as Sum open Sum using ( _⊎_; inl; inr ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.Data.Vec using ( lookup ) open import Cubical.Data.FinData using ( toℕ; inj-toℕ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; sett; setIsSet; _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( _∈ₛ_; ∈∈ₛ; _⊆_; extensionality; ⟪_⟫; ⟪_⟫↪ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ⁅_,_⁆; ⁅_⁆s; module InfinitySet ) open InfinitySet using ( sucV; #_ ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) module Sem = FOL.Semantics (hPropAlgebra (ℓ-suc ℓ)) 𝒮ᵥ open Sem using ( _^_ ) open Sem.At (V ℓ) id using ( _⊨_; ⟦_⟧ )
The graph of an environment
An environment of length n becomes the set of pairs of the numeral for an index with the value there. The index type is finite, hence small, so the gathering is legitimate; membership is definitional.
env : ∀ {n} → (Fin n → V ℓ) → V ℓ env {n} g = sett (Lift {ℓ-zero} {ℓ} (Fin n)) (λ li → pr (# (toℕ (lower li))) (g (lower li))) envOf : ∀ {n} → (V ℓ) ^ n → V ℓ envOf γ = env (λ i → lookup i γ) env-spec : ∀ {n} (g : Fin n → V ℓ) (s : V ℓ) → ⟨ s ∈ env g ⟩ ≡ ∥ Σ[ li ∈ Lift {ℓ-zero} {ℓ} (Fin n) ] (pr (# (toℕ (lower li))) (g (lower li)) ≡ s) ∥₁ env-spec g s = refl
And the lemma the chapter exists for: the graph is functional. A pair sits in it at key i exactly when its second component is the value at i. Forwards, the Kuratowski pair is injective, so the key of the witnessing entry equals the key asked about; numerals are injective, so the indices agree; and the index type embeds in the naturals, so the two indices are the same. Backwards is the entry itself.
lookup-spec : ∀ {n} (g : Fin n → V ℓ) (i : Fin n) (v : V ℓ) → (pr (# (toℕ i)) v ∈ env g) ≡ ((v ≡ g i) , setIsSet v (g i)) lookup-spec {n} g i v = ⇔toPath fwd bwd where step : (lj : Lift {ℓ-zero} {ℓ} (Fin n)) → pr (# (toℕ (lower lj))) (g (lower lj)) ≡ pr (# (toℕ i)) v → v ≡ g i step lj e = sym (ps .snd) ∙ cong g (inj-toℕ (#-inj′ (ps .fst))) where ps : (# (toℕ (lower lj)) ≡ # (toℕ i)) × (g (lower lj) ≡ v) ps = pr-inj e fwd : ⟨ pr (# (toℕ i)) v ∈ env g ⟩ → v ≡ g i fwd = PT.rec (setIsSet v (g i)) (λ { (lj , e) → step lj e }) bwd : v ≡ g i → ⟨ pr (# (toℕ i)) v ∈ env g ⟩ bwd e = ∣ lift i , cong (pr (# (toℕ i))) (sym e) ∣₁
Looking a value up
The object-language form: some member of the environment is the pair of these two. One bounded existential over the previous chapter's Kuratowski reader, so Δ₀ and adequate at once.
memPairAt : ∀ {n} → Fin n → Fin n → Fin n → Formula (V ℓ) n memPairAt e i v = ∃̇∈ (var e) (prAt zero (suc i) (suc v)) Δ₀-memPairAt : ∀ {n} (e i v : Fin n) → Δ₀ (memPairAt e i v) Δ₀-memPairAt e i v = δ-∃∈ (Δ₀-prAt zero (suc i) (suc v)) memPairAt-adequate : ∀ {n} (e i v : Fin n) (γ : (V ℓ) ^ n) → (γ ⊨ memPairAt e i v) ≡ (pr (⟦ var i ⟧ γ) (⟦ var v ⟧ γ) ∈ ⟦ var e ⟧ γ) memPairAt-adequate e i v γ = ⇔toPath fwd bwd where I = ⟦ var i ⟧ γ Vv = ⟦ var v ⟧ γ E = ⟦ var e ⟧ γ fwd : ⟨ γ ⊨ memPairAt e i v ⟩ → ⟨ pr I Vv ∈ E ⟩ fwd = PT.rec ((pr I Vv ∈ E) .snd) (λ { (q , q∈E , sat) → subst (λ z → ⟨ z ∈ E ⟩) (subst ⟨_⟩ (prAt-adequate zero (suc i) (suc v) (q ∷ γ)) sat) q∈E }) bwd : ⟨ pr I Vv ∈ E ⟩ → ⟨ γ ⊨ memPairAt e i v ⟩ bwd h = ∣ pr I Vv , h , subst ⟨_⟩ (sym (prAt-adequate zero (suc i) (suc v) (pr I Vv ∷ γ))) refl ∣₁
Going under a quantifier
Extending an environment shifts every index up by one, and on numerals that is the von Neumann successor. So a certificate that descends under a binder needs to say "this index is the successor of that one", which is three clauses: the smaller belongs to the larger, everything below the smaller is below the larger, and everything below the larger is below the smaller or equal to it.
sucAt : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n sucAt i j = (var i ∈̇ var j) ∧̇ ((∀̇∈ (var i) (var zero ∈̇ var (suc j))) ∧̇ (∀̇∈ (var j) ((var zero ∈̇ var (suc i)) ∨̇ (var zero ≐ var (suc i))))) Δ₀-sucAt : ∀ {n} (i j : Fin n) → Δ₀ (sucAt i j) Δ₀-sucAt i j = δ-∧ δ-∈ (δ-∧ (δ-∀∈ δ-∈) (δ-∀∈ (δ-∨ δ-∈ δ-≐))) private suc-char : (I J : V ℓ) → ⟨ I ∈ J ⟩ → ((z : V ℓ) → ⟨ z ∈ I ⟩ → ⟨ z ∈ J ⟩) → ((z : V ℓ) → ⟨ z ∈ J ⟩ → ∥ ⟨ z ∈ I ⟩ ⊎ (z ≡ I) ∥₁) → J ≡ sucV I suc-char I J hIJ mono cover = extensionality J (sucV I) (sub₁ , sub₂) where sub₁ : ⟨ J ⊆ sucV I ⟩ sub₁ z z∈ₛJ = PT.rec ((z ∈ₛ sucV I) .snd) (Sum.rec (λ h → ∈∈ₛ {a = z} {b = sucV I} .fst (∈sucV-inl {A = I} {x = z} h)) (λ e → subst (λ w → ⟨ w ∈ₛ sucV I ⟩) (sym e) (∈∈ₛ {a = I} {b = sucV I} .fst (self∈sucV I)))) (cover z (∈∈ₛ {a = z} {b = J} .snd z∈ₛJ)) sub₂ : ⟨ sucV I ⊆ J ⟩ sub₂ z z∈ₛs = ∈∈ₛ {a = z} {b = J} .fst (∈sucV-elim {A = I} {x = z} {P = ⟨ z ∈ J ⟩} ((z ∈ J) .snd) (∈∈ₛ {a = z} {b = sucV I} .snd z∈ₛs) (λ h → mono z h) (λ e → subst (λ w → ⟨ w ∈ J ⟩) (sym e) hIJ)) suc-intro : (I J : V ℓ) → J ≡ sucV I → ⟨ I ∈ J ⟩ × (((z : V ℓ) → ⟨ z ∈ I ⟩ → ⟨ z ∈ J ⟩) × ((z : V ℓ) → ⟨ z ∈ J ⟩ → ∥ ⟨ z ∈ I ⟩ ⊎ (z ≡ I) ∥₁)) suc-intro I J e = subst (λ w → ⟨ I ∈ w ⟩) (sym e) (self∈sucV I) , (λ z h → subst (λ w → ⟨ z ∈ w ⟩) (sym e) (∈sucV-inl {A = I} {x = z} h)) , (λ z z∈J → ∈sucV-elim {A = I} {x = z} {P = ∥ ⟨ z ∈ I ⟩ ⊎ (z ≡ I) ∥₁} squash₁ (subst (λ w → ⟨ z ∈ w ⟩) e z∈J) (λ h → ∣ inl h ∣₁) (λ q → ∣ inr q ∣₁)) sucAt-adequate : ∀ {n} (i j : Fin n) (γ : (V ℓ) ^ n) → (γ ⊨ sucAt i j) ≡ ((⟦ var j ⟧ γ ≡ sucV (⟦ var i ⟧ γ)) , setIsSet _ _) sucAt-adequate i j γ = ⇔toPath (λ { (h₁ , h₂ , h₃) → suc-char (⟦ var i ⟧ γ) (⟦ var j ⟧ γ) h₁ h₂ h₃ }) (suc-intro (⟦ var i ⟧ γ) (⟦ var j ⟧ γ))
All sequences over a set
Finally, every finite sequence of members of a given set, encoded and gathered. The index is the length paired with a function into the set's small member type, which is small again, so this is another harvest of the smallness that has been paying for everything since Part 3. A certificate that must quantify over environments quantifies over this.
envIn : (A : V ℓ) {n : ℕ} → (Fin n → ⟪ A ⟫) → V ℓ envIn A g = env (λ i → ⟪ A ⟫↪ (g i)) cons : ∀ {ℓ'} {X : Type ℓ'} {n : ℕ} → X → (Fin n → X) → Fin (suc n) → X cons m g zero = m cons m g (suc i) = g i seqSet : V ℓ → V ℓ seqSet A = sett (Σ[ n ∈ ℕ ] (Fin n → ⟪ A ⟫)) (λ p → envIn A (p .snd)) seqSet-spec : (A s : V ℓ) → ⟨ s ∈ seqSet A ⟩ ≡ ∥ Σ[ p ∈ (Σ[ n ∈ ℕ ] (Fin n → ⟪ A ⟫)) ] (env (λ i → ⟪ A ⟫↪ (p .snd i)) ≡ s) ∥₁ seqSet-spec A s = refl seqSet-mem : {A : V ℓ} {n : ℕ} (f : Fin n → ⟪ A ⟫) → ⟨ env (λ i → ⟪ A ⟫↪ (f i)) ∈ seqSet A ⟩ seqSet-mem {A} {n} f = ∣ (n , f) , refl ∣₁
Shifting an entry
Extending an environment does not only add an entry, it renumbers the ones already there: what was at index i is now at index i + 1. The formula below recognizes one such renumbering, relating an entry to its shifted counterpart.
Five nested bounded quantifiers, which is what it costs to reach the components of two pairs at once: the entry, its index, its value, the shifted entry and its index. The body is then two Kuratowski readers and the successor reader from above, saying that the two entries share a value and that the indices are one apart. Everything the reader chapters built is spent here at once, which is why this is the last formula the coding stack needs.
shiftPairAt : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n shiftPairAt p' p = ∃̇∈ (var p) (∃̇∈ (var zero) (∃̇∈ (var (suc zero)) (∃̇∈ (var (suc (suc (suc p')))) (∃̇∈ (var zero) ( prAt (suc (suc (suc (suc (suc p))))) (suc (suc (suc zero))) (suc (suc zero)) ∧̇ ( prAt (suc (suc (suc (suc (suc p'))))) zero (suc (suc zero)) ∧̇ sucAt (suc (suc (suc zero))) zero )))))) Δ₀-shiftPairAt : ∀ {n} (p' p : Fin n) → Δ₀ (shiftPairAt p' p) Δ₀-shiftPairAt p' p = δ-∃∈ (δ-∃∈ (δ-∃∈ (δ-∃∈ (δ-∃∈ (δ-∧ (Δ₀-prAt (suc (suc (suc (suc (suc p))))) (suc (suc (suc zero))) (suc (suc zero))) (δ-∧ (Δ₀-prAt (suc (suc (suc (suc (suc p'))))) zero (suc (suc zero))) (Δ₀-sucAt (suc (suc (suc zero))) zero))))))) shiftPairAt-adequate : ∀ {n} (p' p : Fin n) (γ : (V ℓ) ^ n) → (γ ⊨ shiftPairAt p' p) ≡ (∥ Σ[ i ∈ V ℓ ] Σ[ v ∈ V ℓ ] ((⟦ var p ⟧ γ ≡ pr i v) × (⟦ var p' ⟧ γ ≡ pr (sucV i) v)) ∥₁ , squash₁) shiftPairAt-adequate p' p γ = ⇔toPath fwd bwd where P = ⟦ var p ⟧ γ P' = ⟦ var p' ⟧ γ Tgt : Type (ℓ-suc ℓ) Tgt = ∥ Σ[ i ∈ V ℓ ] Σ[ v ∈ V ℓ ] ((P ≡ pr i v) × (P' ≡ pr (sucV i) v)) ∥₁ conclude : (c i v c' j : V ℓ) → ⟨ (j ∷ c' ∷ v ∷ i ∷ c ∷ γ) ⊨ prAt (suc (suc (suc (suc (suc p))))) (suc (suc (suc zero))) (suc (suc zero)) ⟩ → ⟨ (j ∷ c' ∷ v ∷ i ∷ c ∷ γ) ⊨ prAt (suc (suc (suc (suc (suc p'))))) zero (suc (suc zero)) ⟩ → ⟨ (j ∷ c' ∷ v ∷ i ∷ c ∷ γ) ⊨ sucAt (suc (suc (suc zero))) zero ⟩ → Tgt conclude c i v c' j sat₁ sat₂ sat₃ = ∣ i , v , subst ⟨_⟩ (prAt-adequate (suc (suc (suc (suc (suc p))))) (suc (suc (suc zero))) (suc (suc zero)) (j ∷ c' ∷ v ∷ i ∷ c ∷ γ)) sat₁ , (subst ⟨_⟩ (prAt-adequate (suc (suc (suc (suc (suc p'))))) zero (suc (suc zero)) (j ∷ c' ∷ v ∷ i ∷ c ∷ γ)) sat₂ ∙ cong (λ z → pr z v) (subst ⟨_⟩ (sucAt-adequate (suc (suc (suc zero))) zero (j ∷ c' ∷ v ∷ i ∷ c ∷ γ)) sat₃)) ∣₁ fwd : ⟨ γ ⊨ shiftPairAt p' p ⟩ → Tgt fwd = PT.rec squash₁ (λ { (c , _ , h₁) → PT.rec squash₁ (λ { (i , _ , h₂) → PT.rec squash₁ (λ { (v , _ , h₃) → PT.rec squash₁ (λ { (c' , _ , h₄) → PT.rec squash₁ (λ { (j , _ , sat₁ , sat₂ , sat₃) → conclude c i v c' j sat₁ sat₂ sat₃ }) h₄ }) h₃ }) h₂ }) h₁ }) build : (i v : V ℓ) → P ≡ pr i v → P' ≡ pr (sucV i) v → ⟨ γ ⊨ shiftPairAt p' p ⟩ build i v eP eP' = ∣ ⁅ i , v ⁆ , subst (λ z → ⟨ ⁅ i , v ⁆ ∈ z ⟩) (sym eP) (∈pair-introR {u = ⁅ i ⁆s} {v = ⁅ i , v ⁆} {y = ⁅ i , v ⁆} refl) , ∣ i , ∈pair-introL {u = i} {v = v} {y = i} refl , ∣ v , ∈pair-introR {u = i} {v = v} {y = v} refl , ∣ ⁅ sucV i , v ⁆ , subst (λ z → ⟨ ⁅ sucV i , v ⁆ ∈ z ⟩) (sym eP') (∈pair-introR {u = ⁅ sucV i ⁆s} {v = ⁅ sucV i , v ⁆} {y = ⁅ sucV i , v ⁆} refl) , ∣ sucV i , ∈pair-introL {u = sucV i} {v = v} {y = sucV i} refl , subst ⟨_⟩ (sym (prAt-adequate (suc (suc (suc (suc (suc p))))) (suc (suc (suc zero))) (suc (suc zero)) (sucV i ∷ ⁅ sucV i , v ⁆ ∷ v ∷ i ∷ ⁅ i , v ⁆ ∷ γ))) eP , subst ⟨_⟩ (sym (prAt-adequate (suc (suc (suc (suc (suc p'))))) zero (suc (suc zero)) (sucV i ∷ ⁅ sucV i , v ⁆ ∷ v ∷ i ∷ ⁅ i , v ⁆ ∷ γ))) eP' , subst ⟨_⟩ (sym (sucAt-adequate (suc (suc (suc zero))) zero (sucV i ∷ ⁅ sucV i , v ⁆ ∷ v ∷ i ∷ ⁅ i , v ⁆ ∷ γ))) refl ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ bwd : Tgt → ⟨ γ ⊨ shiftPairAt p' p ⟩ bwd = PT.rec ((γ ⊨ shiftPairAt p' p) .snd) (λ { (i , v , eP , eP') → build i v eP eP' })
Extending an environment
And the formula the quantifier clauses need: the extended environment is the old one with a new value at index zero. Three clauses. The entry at key zero holds the new value; every entry of the old environment appears shifted in the new one; and every entry of the new one is either that first entry or a shift of an old one.
Adequacy is stated against an encoded environment, because that is the form the certificates hold. Given that the old environment is the graph of g, satisfaction of the formula says exactly that the new one is the graph of g with the value consed on. The two sides match key by key, and the match is definitional at the index: the numeral for suc k is the successor of the numeral for k, and consing shifts indices by exactly that.
consAt : ∀ {n} → Fin n → Fin n → Fin n → Formula (V ℓ) n consAt e' m e = (∃̇∈ (var e') (tagAt zero 0 (suc m))) ∧̇ ((∀̇∈ (var e) (∃̇∈ (var (suc e')) (shiftPairAt zero (suc zero)))) ∧̇ (∀̇∈ (var e') ((tagAt zero 0 (suc m)) ∨̇ (∃̇∈ (var (suc e)) (shiftPairAt (suc zero) zero))))) Δ₀-consAt : ∀ {n} (e' m e : Fin n) → Δ₀ (consAt e' m e) Δ₀-consAt e' m e = δ-∧ (δ-∃∈ (Δ₀-tagAt zero 0 (suc m))) (δ-∧ (δ-∀∈ (δ-∃∈ (Δ₀-shiftPairAt zero (suc zero)))) (δ-∀∈ (δ-∨ (Δ₀-tagAt zero 0 (suc m)) (δ-∃∈ (Δ₀-shiftPairAt (suc zero) zero))))) consAt-adequate : ∀ {n} (e' m e : Fin n) (γ : (V ℓ) ^ n) {k : ℕ} (g : Fin k → V ℓ) → ⟦ var e ⟧ γ ≡ env g → (γ ⊨ consAt e' m e) ≡ ((⟦ var e' ⟧ γ ≡ env (cons (⟦ var m ⟧ γ) g)) , setIsSet _ _) consAt-adequate e' m e γ {k} g hE = ⇔toPath fwd bwd where M = ⟦ var m ⟧ γ E = ⟦ var e ⟧ γ E' = ⟦ var e' ⟧ γ G' : Fin (suc k) → V ℓ G' = cons M g classify : ((y : V ℓ) → ⟨ y ∈ E' ⟩ → ∥ ⟨ (y ∷ γ) ⊨ tagAt zero 0 (suc m) ⟩ ⊎ ⟨ (y ∷ γ) ⊨ ∃̇∈ (var (suc e)) (shiftPairAt (suc zero) zero) ⟩ ∥₁) → (y : V ℓ) → ⟨ y ∈ₛ E' ⟩ → ⟨ y ∈ₛ env G' ⟩ classify h₃ y y∈ₛE' = PT.rec ((y ∈ₛ env G') .snd) (Sum.rec (λ tsat → ∈∈ₛ {a = y} {b = env G'} .fst ∣ lift zero , sym (subst ⟨_⟩ (tagAt-adequate zero 0 (suc m) (y ∷ γ)) tsat) ∣₁) (λ ssat → PT.rec ((y ∈ₛ env G') .snd) (λ { (p , p∈E , sh) → PT.rec ((y ∈ₛ env G') .snd) (λ { (li , peq) → PT.rec ((y ∈ₛ env G') .snd) (λ { (i , v , epv , eyv) → ∈∈ₛ {a = y} {b = env G'} .fst ∣ lift (suc (lower li)) , sym (cong₂ (λ a b → pr (sucV a) b) (pr-inj {a = i} {b = v} {c = # (toℕ (lower li))} {d = g (lower li)} (sym epv ∙ sym peq) .fst) (pr-inj {a = i} {b = v} {c = # (toℕ (lower li))} {d = g (lower li)} (sym epv ∙ sym peq) .snd)) ∙ sym eyv ∣₁ }) (subst ⟨_⟩ (shiftPairAt-adequate (suc zero) zero (p ∷ y ∷ γ)) sh) }) (subst (λ z → ⟨ p ∈ z ⟩) hE p∈E) }) ssat)) (h₃ y (∈∈ₛ {a = y} {b = E'} .snd y∈ₛE')) covered : ⟨ γ ⊨ ∃̇∈ (var e') (tagAt zero 0 (suc m)) ⟩ → ((p : V ℓ) → ⟨ p ∈ E ⟩ → ⟨ (p ∷ γ) ⊨ ∃̇∈ (var (suc e')) (shiftPairAt zero (suc zero)) ⟩) → (y : V ℓ) → ⟨ y ∈ₛ env G' ⟩ → ⟨ y ∈ₛ E' ⟩ covered h₁ h₂ y y∈ₛG' = PT.rec ((y ∈ₛ E') .snd) (λ { (lj , eq) → byKey (lower lj) eq }) (∈∈ₛ {a = y} {b = env G'} .snd y∈ₛG') where byKey : (j : Fin (suc k)) → pr (# (toℕ j)) (G' j) ≡ y → ⟨ y ∈ₛ E' ⟩ byKey zero eq = PT.rec ((y ∈ₛ E') .snd) (λ { (q , q∈E' , tsat) → subst (λ z → ⟨ z ∈ₛ E' ⟩) (subst ⟨_⟩ (tagAt-adequate zero 0 (suc m) (q ∷ γ)) tsat ∙ eq) (∈∈ₛ {a = q} {b = E'} .fst q∈E') }) h₁ byKey (suc i₀) eq = PT.rec ((y ∈ₛ E') .snd) (λ { (p' , p'∈E' , sh) → PT.rec ((y ∈ₛ E') .snd) (λ { (i , v , epv , ep'v) → subst (λ z → ⟨ z ∈ₛ E' ⟩) (ep'v ∙ cong₂ (λ a b → pr (sucV a) b) (pr-inj {a = i} {b = v} {c = # (toℕ i₀)} {d = g i₀} (sym epv) .fst) (pr-inj {a = i} {b = v} {c = # (toℕ i₀)} {d = g i₀} (sym epv) .snd) ∙ eq) (∈∈ₛ {a = p'} {b = E'} .fst p'∈E') }) (subst ⟨_⟩ (shiftPairAt-adequate zero (suc zero) (p' ∷ pr (# (toℕ i₀)) (g i₀) ∷ γ)) sh) }) (h₂ (pr (# (toℕ i₀)) (g i₀)) (subst (λ z → ⟨ pr (# (toℕ i₀)) (g i₀) ∈ z ⟩) (sym hE) ∣ lift i₀ , refl ∣₁)) fwd : ⟨ γ ⊨ consAt e' m e ⟩ → E' ≡ env G' fwd (h₁ , h₂ , h₃) = extensionality E' (env G') ( (λ y y∈ₛE' → classify h₃ y y∈ₛE') , (λ y y∈ₛG' → covered h₁ h₂ y y∈ₛG') ) bwd : E' ≡ env G' → ⟨ γ ⊨ consAt e' m e ⟩ bwd e'eq = ∣ pr (# 0) M , subst (λ z → ⟨ pr (# 0) M ∈ z ⟩) (sym e'eq) ∣ lift zero , refl ∣₁ , subst ⟨_⟩ (sym (tagAt-adequate zero 0 (suc m) (pr (# 0) M ∷ γ))) refl ∣₁ , (λ p p∈E → PT.rec (((p ∷ γ) ⊨ ∃̇∈ (var (suc e')) (shiftPairAt zero (suc zero))) .snd) (λ { (li , peq) → ∣ pr (# (suc (toℕ (lower li)))) (g (lower li)) , subst (λ z → ⟨ pr (# (suc (toℕ (lower li)))) (g (lower li)) ∈ z ⟩) (sym e'eq) ∣ lift (suc (lower li)) , refl ∣₁ , subst ⟨_⟩ (sym (shiftPairAt-adequate zero (suc zero) (pr (# (suc (toℕ (lower li)))) (g (lower li)) ∷ p ∷ γ))) ∣ # (toℕ (lower li)) , g (lower li) , sym peq , refl ∣₁ ∣₁ }) (subst (λ z → ⟨ p ∈ z ⟩) hE p∈E)) , (λ p' p'∈E' → PT.rec squash₁ (λ { (lj , eq) → byKey' p' (lower lj) eq }) (subst (λ z → ⟨ p' ∈ z ⟩) e'eq p'∈E')) where byKey' : (p' : V ℓ) (j : Fin (suc k)) → pr (# (toℕ j)) (G' j) ≡ p' → ∥ ⟨ (p' ∷ γ) ⊨ tagAt zero 0 (suc m) ⟩ ⊎ ⟨ (p' ∷ γ) ⊨ ∃̇∈ (var (suc e)) (shiftPairAt (suc zero) zero) ⟩ ∥₁ byKey' p' zero eq = ∣ inl (subst ⟨_⟩ (sym (tagAt-adequate zero 0 (suc m) (p' ∷ γ))) (sym eq)) ∣₁ byKey' p' (suc i₀) eq = ∣ inr ∣ pr (# (toℕ i₀)) (g i₀) , subst (λ z → ⟨ pr (# (toℕ i₀)) (g i₀) ∈ z ⟩) (sym hE) ∣ lift i₀ , refl ∣₁ , subst ⟨_⟩ (sym (shiftPairAt-adequate (suc zero) zero (pr (# (toℕ i₀)) (g i₀) ∷ p' ∷ γ))) ∣ # (toℕ i₀) , g i₀ , refl , sym eq ∣₁ ∣₁ ∣₁
Recap
An environment is its graph (env), and the graph is functional (lookup-spec), which is what makes the encoding usable rather than merely definable. memPairAt reads a value out of it and
sucAt recognizes the index shift that going under a quantifier performs, both Δ₀ and adequate. seqSet collects all finite sequences over a set, for the certificates that quantify over environments instead of naming one. shiftPairAt recognizes the renumbering that extension performs, and consAt puts it to work: the extended environment is the old one with a value consed on, stated against the encoded form the certificates actually hold. That is the last formula the coding stack owes the certificates.