--- title: "Finite environments as set-coded graphs" module: L.Coding.Environment lang: en site: "Bedrock" description: "Finite environments as set-coded graphs" stage: "Internal coding: expressions and domains" reading_order: 41 canonical: https://bedrock.institute/en/L.Coding.Environment.html html: L.Coding.Environment.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Environment.lagda.md prerequisites: [Base.Prelude, FOL.Syntax, FOL.LevyHierarchy, FOL.Semantics, V.Hierarchy, V.Model, V.Coding, L.Coding.PairFormulas] routes: [internal-satisfaction] translations: [https://bedrock.institute/zh/L.Coding.Environment.md, https://bedrock.institute/ja/L.Coding.Environment.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Finite environments as set-coded graphs A satisfaction clause of the first-order language speaks about the value of a variable, but it can only quantify over sets. So before satisfaction can be computed inside set theory, a variable assignment itself must become a set. This chapter performs that encoding: a finite assignment, a function from variable indices to sets of `V ℓ`, is represented by its graph, the set of ordered pairs of the numeral for an index with the value there. The encoding is designed so that lookup inside the graph is exact. Because the key side consists of numerals, and numerals are injective, a pair sitting at the key for `i` in the graph has as its second component exactly the value at `i`, and nothing else. That functionality statement is the main lemma here. The second concern is extension. When satisfaction descends under a quantifier, the new value is placed at index zero and every old index moves up by one; on the key side this is precisely the von Neumann successor. The chapter therefore builds bounded formulas that say, in membership alone, that one index is the successor of another, that one pair is obtained from another by shifting its key, and finally that a whole set is the graph of the extended assignment. Each of these is proved as an adequacy statement: satisfaction of the formula is a path of truth values to the corresponding external fact about sets, and the graphs involved are compared by extensionality, member by member, never by selecting witnesses out of the truncated membership data. Everything in this chapter takes place at one fixed universe level `ℓ`: the sets being manipulated are elements of `V ℓ`, and the formulas of the language quantify over those sets. Keeping the level as an explicit parameter means the whole construction can be instantiated wherever a hierarchy at that level is available. ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module L.Coding.Environment {ℓ : Level} where open import FOL.Syntax using ( var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; ∀̇∈; ∃̇∈; ⊥̇ ) ``` The chapter works inside the bounded fragment of the first-order language: a Δ₀ formula is one whose every quantifier is bounded by a variable of the environment, so its satisfaction under an assignment depends only on membership in the exhibited bounding sets. Two host-level facts do the mathematical work of the encoding. The Kuratowski pair `pr` is injective, so a pair determines its components; and the numerals `# n` are injective, so a numeral determines its index. Between them, these two injections are what make the graph of an assignment behave like the graph of a function. ```agda open import FOL.LevyHierarchy using ( checkΔ₀; Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-∀∈ ) import FOL.Semantics open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV ) open import V.Model {ℓ} using ( self∈sucV; ∈sucV-inl; ∈sucV-elim ) open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′ ) ``` The bounded reader `prAt`, proved adequate in the chapter on pair formulas, says of a set at a given variable slot that it is the Kuratowski pair of the sets at two other slots. Its adequacy lemma and the two introduction rules placing a component inside a pair are reused here directly, since a shifted entry is still a Kuratowski pair, only with a moved key. The binary sum type serves on the host side wherever a formula produces a disjunction: a value is one thing or another, recorded as a choice of side without claiming uniqueness of the witness. ```agda open import L.Coding.PairFormulas {ℓ} using ( prAt; prAt-adequate; prChar-fwd; prChar-bwd ; ∈pair-introL; ∈pair-introR ) open import Cubical.Data.Unit using ( tt ) import Cubical.Data.Sum as Sum ``` Membership in a set of the hierarchy is a proposition, so a proof that some entry of the graph is related to a given pair is always a *merely exists*: it records that a witness exists without providing it as ordinary data. Eliminating such a truncation is legitimate only into a proposition-valued target, and no chosen witness can be recovered from it globally. Whenever two propositions are identified in this chapter, the identification is built by `⇔toPath`, which turns an if-and-only-if into a path between truth values; that is the shape every adequacy lemma here takes. ```agda open Sum using ( _⊎_; inl; inr ) import Cubical.Data.Empty as E hiding ( elim ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open import Cubical.Functions.Logic using ( ⇔toPath ) ``` The ambient universe is the cubical cumulative hierarchy. A set is introduced as `sett A f`, an index type together with a family of elements, and its membership relation is truncated like any other membership in this setting. The principle `extensionality` says that two sets with the same members are equal as paths. This is the tool by which encoded graphs will be compared: to show that one candidate graph equals another, one proves, for each element, that membership in the first is a path of truth values away from membership in the second. ```agda 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 ) ``` The constructions of the hierarchy supply the pieces the encoding uses: the empty set, singletons, the unordered pair `⁅_,_⁆`, and the numerals. The numeral recursion is the key point: `# 0` is `∅` and `# (suc n)` is `sucV (# n)`, the von Neumann successor. So incrementing an index and taking the successor of its key are the same operation, which is exactly why extending an environment can be described by a bounded formula. On the semantic side, truth values are propositions packaged with proofs of propositionhood, so the satisfaction of a formula is itself a proposition and can be identified with an external set-theoretic statement by a path. ```agda open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ⁅_,_⁆; ⁅_⁆s; ∅; ∅-empty; module InfinitySet ) open InfinitySet using ( sucV; #_ ) module Sem = FOL.Semantics 𝒮ᵥ ``` Finally, the satisfaction relation `_⊨_` and the term interpretation `⟦_⟧` are taken over the carrier `V ℓ` itself, with the identity embedding of constants. An environment for a formula of arity `n` is then an honest function `(V ℓ) ^ n`, a finite tuple of sets. What this chapter encodes is the assignment carried inside certificate data, not this semantic carrier: the tuple form is what the semantics evaluates, while the graph form is what certificates can store and manipulate as a single set. ```agda open Sem using ( _^_ ) open Sem.At (V ℓ) id using ( _⊨_; ⟦_⟧ ) ``` ## The graph of an environment An assignment `g : Fin n → V ℓ` becomes the set `env g` whose entry at the key for index `i` is the ordered pair of the numeral `# (toℕ i)` with the value `g i`. The section proves the statement that makes this representation usable: `lookup-spec` identifies membership of a pair at key `i` in `env g` with the proposition that its second component equals `g i`. Membership in `env g` is truncated, as all hierarchy membership is; the point of `lookup-spec` is that this truncated fiber data nevertheless determines the value exactly. The gathering is an instance of the set constructor `sett`, which takes an index type and a family of elements. The finite index type `Fin n` lives below level `ℓ`, so it is lifted first; `Lift` adjusts only the universe, and `lower` recovers the index. Each index `li` then contributes one entry, the pair of the numeral for its index with the value of `g` there. The entries themselves are ordinary data; it is only membership in the resulting set that is truncated. The index is turned into a key `# (toℕ i)` rather than used directly, because the formula language must be able to talk about keys, and what formulas talk about are sets, here the numerals. ```agda env : ∀ {n} → (Fin n → V ℓ) → V ℓ env {n} g = sett (Lift {ℓ-zero} {ℓ} (Fin n)) (λ li → pr (# (toℕ (lower li))) (g (lower li))) ``` The graph is *functional*: a pair belongs to `env g` at key `i` exactly when its second component is the value `g i`. This is an extensional statement about membership, and it is what makes the encoding usable for lookup rather than merely definable. The argument reads off the three layers of the key. The witnessing entry is a Kuratowski pair, and the pair is injective, so its key equals the key asked about. The keys are numerals, and numerals are injective, so the underlying indices agree as natural numbers. Finally `Fin n` embeds in the naturals, so the two indices are the same index, and the value component says it holds `g i`. The reverse direction simply exhibits the entry at `i` itself. The statement is an equality of propositions: membership of the pair at key `i` in the graph is the proposition `v ≡ g i`, packaged with its proof of propositionhood, which comes from the fact that `V ℓ` is an h-set. An equivalence between propositions converts into a path of truth values, so the lemma is proved from two implications, one in each direction. ```agda 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)) ``` The forward direction works on a truncated witness, so the case analysis is factored into an ordinary function on an explicit entry. Its input is a path saying that some entry of the graph equals the pair asked about, and its output is the goal `v ≡ g i`. Since the goal is a proposition, eliminating the truncation into it is legitimate; no entry is extracted into ordinary data. ```agda → 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) ``` Injectivity of the pair splits the assumed equality into a path of keys and a path of values. The reversed value path is one half of the goal. The key path says the two numerals agree; injectivity of numerals together with the embedding into the naturals turns that into equality of the indices themselves, and applying `g` gives the other half. The backward direction exhibits the entry at `i` directly: the truncated witness is the lifted index, and the path is filled by applying the pair constructor to the reversed assumption. No canonical witness is chosen, and uniqueness of the witness is not claimed. ```agda 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) ∣₁ ``` ## Recognizing successor indices `sucAt i j` is a bounded formula saying that the value at `j` is the von Neumann successor of the value at `i`; `sucAt-adequate` proves that satisfaction of the formula under an environment is exactly this equality of values. The extension of an environment shifts every index up by one, and on numerals that shift is the von Neumann successor. So the certificate machinery, which descends under a binder, must be able to say "this index is the successor of that one". The language has no successor symbol, so the relation is said with membership alone, in three clauses: the smaller belongs to the larger, everything belonging to the smaller belongs to the larger, and everything belonging to the larger merely belongs to the smaller or equals it. Three bounded clauses do it: the smaller set belongs to the larger; membership in the smaller transfers into the larger; and membership in the larger is merely classified, as belonging to the smaller or being the smaller itself. The bounded quantifiers bind `var zero`, and inside a quantifier body every other variable is read at its shifted slot, so `var (suc i)` in the body refers to the value that `var i` had before descending. The second and third clauses say exactly that the larger set has no members beyond those of the smaller together with the smaller itself, which is the extensional content of being its successor. Boundedness is recorded separately by `Δ₀-sucAt`: conjunction, bounded universal quantification, and the leaves, membership and equality, all preserve Δ₀. ```agda 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) ``` The adequacy proof rests on a host-level characterization, stated first at the level of sets. It says that the three formula clauses, read as facts about sets `I` and `J`, hold exactly when `J` and `sucV I` are equal as sets. ```agda Δ₀-sucAt i j = δ-∧ δ-∈ (δ-∧ (δ-∀∈ δ-∈) (δ-∀∈ (δ-∨ δ-∈ δ-≐))) private suc-char : (I J : V ℓ) → ⟨ I ∈ J ⟩ → ((z : V ℓ) → ⟨ z ∈ I ⟩ → ⟨ z ∈ J ⟩) ``` The forward lemma takes the three clauses as hypotheses, now at the level of sets: `I` is a member of `J`, membership in `I` transfers into `J`, and every member of `J` is merely in `I` or equal to `I`. Its conclusion is a path `J ≡ sucV I`, a genuine equality of sets, not merely a biconditional of memberships. ```agda → ((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 ⟩ ``` The equality is produced by extensionality, split into two inclusions. The first inclusion sends each member of `J` across. The classification hypothesis yields a truncated disjunction, and both disjuncts are eliminated into the proposition-valued membership in `sucV I`: in the left case the member transfers through the union clause of the successor, in the right case the member is `I` itself, which belongs to `sucV I` as its own top element. ```agda 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)))) ``` The second inclusion reads members of `sucV I` back into `J`. Membership in a successor is classified by an eliminator with two cases, and this is where the truncation of the classification hypothesis is discharged: the eliminator's target is the proposition `z ∈ J`, so case analysis on the truncated classification is legitimate. The two cases use the two clauses already in hand, transferring the member from `I` or rewriting it to `I`. ```agda (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) ``` The converse lemma `suc-intro` runs the characterization in the opposite direction. Given `J ≡ sucV I`, it transports the first two successor-membership facts to `J`. For the third clause it transports a member of `J` to `sucV I` and applies the successor-membership eliminator, whose result is already the required truncated classification. Thus this direction does not consume an assumed truncated classification. ```agda (λ 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 ⟩) ``` Each clause is produced by transporting a membership fact about `sucV I` along the assumed path, in whichever direction lands it at `J`. The first clause transports the fact that `I` belongs to its own successor; the second transports the transfer rule `∈sucV-inl` member by member. ```agda × ((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₁ ``` The third clause is the classification of the members of `J`, and its target is the truncated disjunction itself. The successor eliminator is applied with that truncation as the elimination target, so each of its two cases is met by simply re-truncating the corresponding branch. With all three clauses assembled, the adequacy statement takes the same shape as `lookup-spec`: satisfaction of `sucAt i j` under `γ` is the proposition that the value at `j` equals the von Neumann successor of the value at `i`. ```agda (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 _ _) ``` The two lemmas fit the adequacy statement exactly. Forwards, the satisfaction of the conjunction unpacks into three clauses, which `suc-char` receives as its three hypotheses and turns into the semantic equation; since the conclusion is a proposition, the truncated structure of the quantifier data passes through the elimination legally. Backwards, `suc-intro` produces the three clauses from the semantic equation. The two directions compose into the path of truth values that an adequacy lemma is. ```agda sucAt-adequate i j γ = ⇔toPath (λ { (h₁ , h₂ , h₃) → suc-char (⟦ var i ⟧ γ) (⟦ var j ⟧ γ) h₁ h₂ h₃ }) (suc-intro (⟦ var i ⟧ γ) (⟦ var j ⟧ γ)) ``` ## Shifting an entry `shiftPairAt p' p` recognizes when the pair at `p'` is obtained from the pair at `p` by replacing its numeral key with its von Neumann successor and keeping the value unchanged. Extending an environment does not only insert a new entry at key zero; it renumbers the old ones, so that what was keyed `# i` becomes keyed `# (suc i)`. This section isolates one step of that renumbering and gives it a bounded description. Since a single bounded quantifier can only bind one member of a set, and one entry of a Kuratowski pair yields its index and value one at a time, the formula runs five bounded quantifiers in sequence to hold the two entries, their two indices and their shared value simultaneously. Its body is then the two Kuratowski readers of the pair-reader chapter, plus the successor reader of the previous section, and together they say precisely that the two entries share a value while the keys are one successor step apart. The formula is a five-fold bounded quantification over the value at `p`. Each bounded existential extends the environment by one slot, so the bound witnesses are read at positions determined by how many quantifiers have been entered: the first three quantifiers produce the entry at `p`, its index, and its value. ```agda shiftPairAt : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n shiftPairAt p' p = ∃̇∈ (var p) (∃̇∈ (var zero) (∃̇∈ (var (suc zero)) ``` The remaining two quantifiers produce the entry at `p'` and its index. At that point all five pieces are simultaneously available to the body: the original entry, its index, its value, the shifted entry, and the shifted index. ```agda (∃̇∈ (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)) ``` The body is the conjunction of three bounded assertions about those five witnesses. The two Kuratowski readers say that the original entry is the pair of its index and value, and that the shifted entry is the pair of the shifted index and the same value; the successor reader says that the shifted index is the von Neumann successor of the original one. Read together, the shifted entry carries the same value at a key one successor step higher. ```agda ∧̇ 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₁) ``` The adequacy statement records what satisfaction of such nested quantification actually provides: a merely-exists claim. It says that the set at slot `p` is, merely, the pair of some index and value, and the set at slot `p'` is, merely, the pair of the successor of that index and the same value. The truncation is faithful to the formula: nothing in it singles out a particular decomposition of either entry, and none is needed. ```agda shiftPairAt-adequate p' p γ = ⇔toPath fwd bwd where P = ⟦ var p ⟧ γ P' = ⟦ var p' ⟧ γ Tgt : Type (ℓ-suc ℓ) ``` The forward direction must convert a chain of truncated witnesses into one inhabitant of the truncated target, and it does so by working with all five witnesses at once once they are explicit. The hypotheses available at that point are the three body conjuncts, each asserted in the environment extended by all five bound witnesses, and the conclusion is a single inhabitant of the truncated existence statement. ```agda 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 ∷ γ) ``` Once the five witnesses are explicit, the truncated target is filled by the index `i`, the value `v`, and two path equations. The three satisfaction hypotheses yield those equations through the adequacy lemmas already proved; transporting along the resulting paths aligns their endpoints with the target. The propositionhood of the outer target matters for the surrounding truncation eliminations, while path transport itself requires no such assumption. ```agda ⊨ 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 ``` The adequacy lemma for the pair reader reinterprets its satisfaction hypothesis at slot `p`: it says precisely that the entry there is the Kuratowski pair of the bound index and the bound value. This turns the first satisfaction proof into the first of the two recorded equations, `P ≡ pr i v`. ```agda , subst ⟨_⟩ (prAt-adequate (suc (suc (suc (suc (suc p))))) (suc (suc (suc zero))) (suc (suc zero)) (j ∷ c' ∷ v ∷ i ∷ c ∷ γ)) sat₁ , (subst ⟨_⟩ ``` The second pair reader's hypothesis yields the equation `P' ≡ pr j v`, and the successor reader's hypothesis yields `j ≡ sucV i`. Composing the second into the first and mapping the successor operation over the first component of the pair produces the second recorded equation, `P' ≡ pr (sucV i) v`. Together with the first equation this is exactly the target: the two entries share a value, and the second key is the von Neumann successor of the first. ```agda (prAt-adequate (suc (suc (suc (suc (suc p'))))) zero (suc (suc zero)) (j ∷ c' ∷ v ∷ i ∷ c ∷ γ)) sat₂ ∙ cong (λ z → pr z v) (subst ⟨_⟩ ``` The assembled index, value and two equations are then truncated into the target. This completes the forward direction of adequacy, which unwraps the five quantifiers one at a time. Each is a truncated existential, so each elimination must land in a proposition; the target is truncated precisely so that this nesting of eliminations is legal. ```agda (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₁ ``` The innermost elimination reaches the three satisfaction proofs, and with them the forward proof is done. Note that the five witnesses never become ordinary data outside the eliminations: each elimination consumes a truncated layer into a proposition, so the witnesses exist only inside that chain. ```agda (λ { (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₄ }) ``` The backward direction runs on introduction instead of analysis. Given an index, a value, and the two equations identifying the slots with the corresponding pairs, a satisfaction proof must be produced, and everything it needs is ordinary set construction: the entry sets are built with the pairing operation, and their memberships follow from the component introduction rules. ```agda h₃ }) h₂ }) h₁ }) build : (i v : V ℓ) → P ≡ pr i v → P' ≡ pr (sucV i) v → ⟨ γ ⊨ shiftPairAt p' p ⟩ build i v eP eP' = ``` The first witness for the outer existential is the pair `⁅ i , v ⁆` itself. It belongs to the set at slot `p` because the assumed equation identifies that set with `pr i v`, and by the component introduction rule the unordered pair `⁅ i , v ⁆` sits inside its own Kuratowski encoding; transporting along the equation moves the membership to the right side. Opening the pair then needs no work: its index witness is `i` and its value witness is `v`, each supplied by one of the two component rules. ```agda ∣ ⁅ 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 ``` The shifted entry is built from `sucV i` and `v` by the same construction, with the shifted index witness being the successor set itself. The remaining clauses are satisfied by the two assumed equations, which the adequacy lemmas read back as satisfaction proofs. Where the forward direction had to analyze a hypothetical witness, the backward direction simply assembles the five witnesses the formula asks for, and the truncated outer layer receives a single explicit one. ```agda , ∣ ⁅ 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 ``` The innermost witness is the shifted entry `⁅ sucV i , v ⁆`, and its index witness is the successor set `sucV i` itself, introduced by the left-component rule for a Kuratowski pair. The two clauses about the entries remain. The first is filled from the assumed equation `eP : ⟦ var p ⟧ γ ≡ pr i v`. The clause is evaluated in the environment extended five times, holding `sucV i`, the shifted pair, `v`, `i` and the original pair in slots zero through four; the bound variables occupy those slots, so slot `p` still reads `⟦ var p ⟧ γ`, which is exactly the left side of `eP`. The adequacy lemma for the pair reader identifies the clause's satisfaction with that equation, so transporting `eP` along the symmetric adequacy path fills the clause. ```agda , ∈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 ⁆ ∷ γ))) ``` The second clause about the entries is filled the same way from `eP'`. The pair reader at slot `p'` reads its index from slot zero, which now holds `sucV i`, and its value from slot two, which holds `v`; so the equation the adequacy lemma expects is precisely `⟦ var p' ⟧ γ ≡ pr (sucV i) v`, the second assumption. Note that the shifted entry itself never needs to be taken apart here: the pair readers supply the two decompositions, and the successor reader, filled by `refl` since slot zero holds the successor of slot three, records that the new key is the successor of the old one with the value preserved. ```agda 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' ``` The last conjunct of the body is the successor reader of the previous section, applied to the two index witnesses. In the assembled environment the value at slot three is the index `i` and the value at slot zero is its von Neumann successor `sucV i`, so the characterization of that reader is witnessed by the reflexive path `sucV i ≡ sucV i`, transported through its adequacy lemma into the satisfaction clause. With this, all three assertions of the body hold: the two entries are genuine pairs sharing a value, and the second key is the successor of the first. This is exactly the mathematical content of one renumbered entry. ```agda , subst ⟨_⟩ (sym (sucAt-adequate (suc (suc (suc zero))) zero (sucV i ∷ ⁅ sucV i , v ⁆ ∷ v ∷ i ∷ ⁅ i , v ⁆ ∷ γ))) refl ∣₁ ``` What remains is bookkeeping across the five nested bounded existentials. Each layer is a proposition, so supplying one witness at a time and sealing it as merely present is legitimate: no choice among candidates is being made, because no candidate was competing. Once each existential has its witness, the satisfaction proof of the whole formula stands assembled. ```agda ∣₁ ∣₁ ∣₁ ∣₁ ``` The backward direction closes the adequacy theorem. Its input is the truncated existence of an index and value with the two equations, and its output is a satisfaction proof, itself a proposition. Elimination of a truncation into a proposition-valued target is exactly what the rules allow, so the assumed pair decomposition may be used inside the elimination even though it is not recovered as ordinary data outside. The constructed witness then matches the formula clause by clause, completing the identification: satisfaction of the shift formula is, as a truth value, the truncated statement that the two entries are pairs sharing a value with successor-related keys. ```agda bwd : Tgt → ⟨ γ ⊨ shiftPairAt p' p ⟩ bwd = PT.rec ((γ ⊨ shiftPairAt p' p) .snd) (λ { (i , v , eP , eP') → build i v eP eP' }) ``` ## Coding the empty entry The new zeroth entry of an extended environment is a Kuratowski pair tagged with `# 0`, and `# 0` is the empty set by definition. This section builds readers that recognize such a pair while mentioning the tag only through its mathematical property: a member is empty, expressible by bounded quantification into the falsity formula, with no constant needed. The three formulas `sgl0At`, `pair0At` and `tag0At` say, respectively, that a set is the singleton of the empty set, the unordered pair of the empty set with a given set, and the tagged pair assembled from these. The metalevel work converts the satisfaction reading of these formulas, phrased with the predicate `Empty'` saying that a set has no members, into the shapes that the pair characterization `prChar-fwd` and `prChar-bwd` of the pair-reader chapter already accept, where the empty set appears by name. Since a set with no members is equal to `∅` by extensionality, the two phrasings describe the same mathematics, and the adequacy lemma `tag0At-adequate` identifies satisfaction of the tag reader with the equation that the tagged set is `pr ∅` applied to the value at the second slot. The first reader describes the singleton `{∅}` without naming the empty set. `sgl0At k` conjoins two bounded clauses about the value at `k`: merely some member satisfies the body `∀̇∈ (var zero) ⊥̇`, and every member does. Under the bounded quantifier, the body `⊥̇` holds exactly when the bound member has no members of its own, so each clause says its subject is empty. The existential clause is what allows the value to be inhabited at all; without it, the condition would also be satisfied by the empty set itself. Together the two clauses say that the value at `k` has a member and all its members are empty, which pins it down extensionally as `{∅}`. ```agda sgl0At : ∀ {n} → Fin n → Formula (V ℓ) n sgl0At k = (∃̇∈ (var k) (∀̇∈ (var zero) ⊥̇)) ∧̇ (∀̇∈ (var k) (∀̇∈ (var zero) ⊥̇)) pair0At : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n pair0At k j = (∃̇∈ (var k) (∀̇∈ (var zero) ⊥̇)) ``` The second reader `pair0At k j` describes the unordered pair `{∅, W}`, where `W` is the value at slot `j` of the original assignment; under the new binder it is addressed by `suc j`. Its three clauses are: the value at `k` merely has an empty member; the value at `j` belongs to it; and every member of it merely is empty or equals `W`. The first clause is the same empty-member existence the singleton reader used, and the third is the pair classification with the first component fixed at `∅`. The third formula `tag0At s x` combines the two readers: the value at `s` merely has a member satisfying the empty singleton clause, merely has one satisfying the empty pair clause, and every member merely satisfies one or the other. ```agda ∧̇ ((var j ∈̇ var k) ∧̇ (∀̇∈ (var k) ((∀̇∈ (var zero) ⊥̇) ∨̇ (var zero ≐ var (suc j))))) tag0At : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n tag0At s x = (∃̇∈ (var s) (sgl0At zero)) ∧̇ ((∃̇∈ (var s) (pair0At zero (suc x))) ``` On the metalevel side, emptiness is expressed by the private predicate `Empty' z`, a function that takes any member `y` of `z` and returns an inhabitant of the empty type `⊥*`. This function expresses that `z` has no members: any alleged membership produces a term of `⊥*`, and `⊥*` is the empty type. It is distinct from the object-language falsity formula `⊥̇`, which is syntax. The first lemma, `empty'→∅`, is the bridge to the named empty set: any set of which `Empty'` holds equals `∅`. ```agda ∧̇ (∀̇∈ (var s) (sgl0At zero ∨̇ pair0At zero (suc x)))) private Empty' : V ℓ → Type (ℓ-suc ℓ) Empty' z = (y : V ℓ) → ⟨ y ∈ z ⟩ → E.⊥* {ℓ-suc ℓ} empty'→∅ : (z : V ℓ) → Empty' z → z ≡ ∅ ``` The proof of the bridge is extensionality with both directions vacuous. To show each `y` belongs to `z` exactly when it belongs to `∅`, suppose `y` belonged to `z`: applying `Empty' z` to that membership yields an inhabitant of the empty type, from which anything follows, in particular membership in `∅`. In the other direction, `∅-empty` refutes any membership in `∅`, and from that refutation membership in `z` follows as well. The converse bridge `∅→empty'` needs only the defining path: a membership of `z` transported along `e : z ≡ ∅` lands in `∅`, where `∅-empty` again contradicts it. Thus `Empty' z` and `z ≡ ∅` are interchangeable. ```agda empty'→∅ z hz = extensionalV (λ y → ⇔toPath (λ h → E.rec (lower (hz y h))) (λ h → E.rec (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst h)))) ∅→empty' : (z : V ℓ) → z ≡ ∅ → Empty' z ∅→empty' z e y y∈z = lift (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst (subst (λ w → ⟨ y ∈ w ⟩) e y∈z))) ``` The satisfaction of the two readers, once unfolded, takes the shape of two metalevel packages. `EmptySgl w` consists of a truncated existence of a member of `w` that is empty, and an untruncated universal clause demanding that every member is empty. `EmptyPair W w` keeps the truncated empty-member existence and replaces the rest by a membership of `W` in `w` together with a truncated classification: every member is merely empty or equals `W`. The truncations sit exactly where the bounded existentials and the truncated disjunction of the formulas put them; in particular no chosen pair decomposition is ever extracted. ```agda EmptySgl : V ℓ → Type (ℓ-suc ℓ) EmptySgl w = ∥ Σ[ z ∈ V ℓ ] (⟨ z ∈ w ⟩ × Empty' z) ∥₁ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → Empty' z) EmptyPair : V ℓ → V ℓ → Type (ℓ-suc ℓ) EmptyPair W w = ∥ Σ[ z ∈ V ℓ ] (⟨ z ∈ w ⟩ × Empty' z) ∥₁ ``` The counterpart packages name the empty set outright. `SglOf∅ w` states that `∅` belongs to `w` and every member of `w` equals `∅`, with no truncation since the witness is given. `PairOf∅ W w` states that `∅` and `W` belong to `w` and every member is merely `∅` or `W`; the classification stays truncated, matching the unordered-pair membership of the hierarchy, from which one does not get to choose a side. These are exactly the shapes the pair characterization of the pair-reader chapter consumes, with its first component instantiated at `∅`, so the whole remaining task is to pass between the two phrasings of the same membership facts. ```agda × (⟨ W ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → ∥ Empty' z ⊎ (z ≡ W) ∥₁)) SglOf∅ : V ℓ → Type (ℓ-suc ℓ) SglOf∅ w = ⟨ ∅ ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → z ≡ ∅) PairOf∅ : V ℓ → V ℓ → Type (ℓ-suc ℓ) PairOf∅ W w = ⟨ ∅ ∈ w ⟩ × (⟨ W ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → ∥ (z ≡ ∅) ⊎ (z ≡ W) ∥₁)) ``` The forward conversion turns the truncated existence of an empty member into the plain fact that `∅` belongs to `w`. Membership in a set of the hierarchy is a proposition, so eliminating the truncation into `⟨ ∅ ∈ w ⟩` is legitimate. Inside, an explicitly given witness `z`, with a membership proof and a proof of `Empty' z`, is first identified with `∅` by the previous lemma; its membership in `w` then transports along that path to a membership of `∅`. The rest of `EmptySgl w` converts wholesale: the untruncated universal clause hands back `Empty' z` for each member `z` of `w`, and the same lemma rewrites that into `z ≡ ∅`. ```agda empty-member : (w : V ℓ) → ∥ Σ[ z ∈ V ℓ ] (⟨ z ∈ w ⟩ × Empty' z) ∥₁ → ⟨ ∅ ∈ w ⟩ empty-member w = PT.rec ((∅ ∈ w) .snd) (λ { (z , hz , ez) → subst (λ u → ⟨ u ∈ w ⟩) (empty'→∅ z ez) hz }) EmptySgl→SglOf∅ : (w : V ℓ) → EmptySgl w → SglOf∅ w EmptySgl→SglOf∅ w (h₁ , hall) = empty-member w h₁ , (λ z hz → empty'→∅ z (hall z hz)) ``` The pair case follows the same plan. `EmptyPair→PairOf∅` reuses the empty-member conversion for the first component, keeps the membership of `W` unchanged, and rewrites the classification member by member: a truncated statement that each member is empty or equals `W` maps to the corresponding truncated statement with `Empty'` replaced by equality with `∅`. The result is exactly the `∅`-based classification, and the truncation is preserved throughout rather than resolved into a chosen side. ```agda EmptyPair→PairOf∅ : (W w : V ℓ) → EmptyPair W w → PairOf∅ W w EmptyPair→PairOf∅ W w (h₁ , hW , hall) = empty-member w h₁ , hW , (λ z hz → PT.map (Sum.map (empty'→∅ z) (λ e → e)) (hall z hz)) SglOf∅→EmptySgl : (w : V ℓ) → SglOf∅ w → EmptySgl w SglOf∅→EmptySgl w (h∅ , hall) = ``` The converse direction needs no witness at all, since the empty set is named from the start. `SglOf∅→EmptySgl` produces the truncated witness directly: `∅` belongs to `w` by assumption, and it is empty by the converse lemma applied to the definitional path `∅ ≡ ∅`. The universal clause converts by the same lemma in the other direction. `PairOf∅→EmptyPair` keeps that witness, carries the membership of `W` over unchanged, and rewrites the classification clause pointwise. ```agda (∣ ∅ , (h∅ , ∅→empty' ∅ refl) ∣₁) , (λ z z∈w → ∅→empty' z (hall z z∈w)) PairOf∅→EmptyPair : (W w : V ℓ) → PairOf∅ W w → EmptyPair W w PairOf∅→EmptyPair W w (h∅ , hW , hall) = (∣ ∅ , (h∅ , ∅→empty' ∅ refl) ∣₁) ``` In that pair conversion, the classification runs in the opposite direction: a member known merely to be `∅` or `W` becomes one that is empty or equals `W`, using `∅→empty'` on the first branch and nothing on the second. The section then abstracts the pattern both directions share. `PairWitness P R Q` packages the three clauses that a Kuratowski-pair characterization reads off a set `Q`: a truncated existence of a member of `Q` carrying `P`, the same for `R`, and a truncated dichotomy assigning to every member of `Q` one of `P` or `R`. ```agda , (hW , λ z z∈w → PT.map (Sum.rec (λ e → inl (∅→empty' z e)) (λ e → inr e)) (hall z z∈w)) PairWitness : (V ℓ → Type (ℓ-suc ℓ)) → (V ℓ → Type (ℓ-suc ℓ)) → V ℓ → Type (ℓ-suc ℓ) PairWitness P R Q = ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × P w) ∥₁ × (∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × R w) ∥₁ ``` Everything above is one conversion applied three times. `map-witness` takes a `PairWitness P R Q` together with two pointwise implications, one sending each `P w` to `P' w` and one sending each `R w` to `R' w`, and returns a `PairWitness P' R' Q`. This is exactly the shape of the whole section: the empty-based predicates and the `∅`-based predicates package the same three-clause structure about the same set, and the four conversion lemmas supply the required pointwise implications in both directions. ```agda × ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ P y ⊎ R y ∥₁)) map-witness : {P R P' R' : V ℓ → Type (ℓ-suc ℓ)} (Q : V ℓ) → ((w : V ℓ) → P w → P' w) → ((w : V ℓ) → R w → R' w) → PairWitness P R Q → PairWitness P' R' Q map-witness Q f g (h₁ , h₂ , h₃) = ``` The forward theorem `prChar∅-fwd` now takes the three empty-based hypotheses, in the truncated shapes in which satisfaction of `tag0At` presents them, and concludes the path `Q ≡ pr ∅ W`. The conversion lemma is applied once, transforming the hypotheses into the three clauses about `∅`; the general pair characterization then identifies `Q` with the Kuratowski pair of `∅` and `W` by extensionality. The truncated witnesses are never extracted into ordinary data; they are used only inside conversions whose outputs are the proposition-shaped clauses the characterization accepts. ```agda PT.map (λ { (w , hw , h) → w , hw , f w h }) h₁ , PT.map (λ { (w , hw , h) → w , hw , g w h }) h₂ , (λ y hy → PT.map (Sum.map (f y) (g y)) (h₃ y hy)) prChar∅-fwd : (Q W : V ℓ) → ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × EmptySgl w) ∥₁ ``` The backward theorem `prChar∅-bwd` mirrors this: from the path `Q ≡ pr ∅ W` it returns the three empty-based clauses, by running the general pair characterization backwards with its first component at `∅` and its second at `W`, and then converting each resulting clause into its empty-based counterpart. With both theorems in place, satisfaction of `tag0At s x` is interchangeable with the equality of the value at slot `s` with the tagged pair `pr ∅ (⟦ var x ⟧ γ)`, which is the reading the extension clauses of the next section consume. ```agda → ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × EmptyPair W w) ∥₁ → ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ EmptySgl y ⊎ EmptyPair W y ∥₁) → Q ≡ pr ∅ W prChar∅-fwd Q W h₁ h₂ h₃ = prChar-fwd Q ∅ W (fst h) (fst (snd h)) (snd (snd h)) where ``` The intermediate predicate `PairWitness` keeps the argument independent of any particular construction of `Q`. Only the pointwise meaning of its two possible components changes: first emptiness is replaced by equality with `∅`, or conversely, and the general pair characterization then applies without reopening the truncated witnesses. ```agda h : PairWitness SglOf∅ (PairOf∅ W) Q h = map-witness Q EmptySgl→SglOf∅ (EmptyPair→PairOf∅ W) (h₁ , h₂ , h₃) prChar∅-bwd : (Q W : V ℓ) → Q ≡ pr ∅ W → ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × EmptySgl w) ∥₁ × (∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × EmptyPair W w) ∥₁ ``` The adequacy lemma is stated as a path between truth values, in the same form the earlier readers used. On the left is the satisfaction of `tag0At s x`; on the right, the proposition that the value at slot `s` equals `pr ∅ (⟦ var x ⟧ γ)`, the Kuratowski pair whose tag is the empty set and whose second component is the value at slot `x`, packaged with the proof that the equality type is a proposition because `V ℓ` is an h-set. This says exactly that the encoded zeroth entry is the pair of the empty tag with the new value. ```agda × ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ EmptySgl y ⊎ EmptyPair W y ∥₁)) prChar∅-bwd Q W e = map-witness Q SglOf∅→EmptySgl (PairOf∅→EmptyPair W) (prChar-bwd Q ∅ W e) tag0At-adequate : ∀ {n} (s x : Fin n) (γ : (V ℓ) ^ n) → (γ ⊨ tag0At s x) ≡ ((⟦ var s ⟧ γ ≡ pr ∅ (⟦ var x ⟧ γ)) , setIsSet _ _) tag0At-adequate s x γ = ⇔toPath ``` The proof composes the two lemmas of this section in each direction. Unfolding the satisfaction of the conjunction and the three bounded quantifiers turns the left side into exactly the truncated existence of an empty singleton member, the truncated existence of an empty pair member, and the truncated classification, which is what `prChar∅-fwd` consumes. Backwards, the path `e` goes to `prChar∅-bwd`, whose output the semantics reassembles into satisfaction. Neither direction inspects how any set was built; emptiness is handled entirely through the equivalence between `Empty'` and equality with `∅`. ```agda (λ { (h₁ , h₂ , h₃) → prChar∅-fwd _ _ h₁ h₂ h₃ }) (λ e → prChar∅-bwd _ _ e) ``` ## Extending an environment Consing a value onto an assignment does two things at once: the new value lands at index zero, and every old index moves up by one. This section proves that a bounded formula, `consAt`, expresses exactly this transformation on encoded graphs, and that its adequacy holds against an *encoded* environment. The formula has three clauses: an entry of the new set carries the empty tag and the new value; every entry of the old graph appears in the new one shifted; and every entry of the new one either is that new entry or is a shift of an old one. The adequacy statement is not that the formula merely relates two sets in a cons-like way. Given a function `g` and the hypothesis that the old slot equals the graph `env g`, it concludes the path from the new slot to the graph `env (cons M g)`. Both sides of that equation are sets of the hierarchy, so the proof is extensional: two inclusions are shown, member by member. One direction classifies each member of the new set using the readers of this chapter, the other walks the graph of `cons M g` key by key. At the index the agreement is definitional, since the numeral for `suc k` is the successor of the numeral for `k`. The host-level operation `cons m g` is the function on `Fin (suc n)` returning `m` at index zero and `g i` at index `suc i`: one value is prepended, and each old value keeps its value only after its index has moved up by one. The formula `consAt e' m e` names three environment variables: the value at `e'` is the candidate extended graph, the value at `m` is the element being consed on, and the value at `e` is the graph being extended. ```agda cons : ∀ {ℓ'} {X : Type ℓ'} {n : ℕ} → X → (Fin n → X) → Fin (suc n) → X cons m g zero = m cons m g (suc i) = g i consAt : ∀ {n} → Fin n → Fin n → Fin n → Formula (V ℓ) n consAt e' m e = ``` The three clauses of `consAt` mirror the three defining equations of `cons`. Read under `γ`: the value at `e'` merely has a member satisfying the tagged-pair reader `tag0At zero (suc m)`, so it holds an entry whose tag is empty and whose second component is the value at `m`; every entry of the value at `e` merely has a shift inside the value at `e'`, said by `shiftPairAt` with the old entry in the later slot; and every entry of the value at `e'` merely is that tagged zero entry or the shift of an entry of the value at `e`. Each subformula is built from bounded quantifiers, equations and the two earlier readers, so the checker certifies the whole conjunction as Δ₀, recorded once and for all by `Δ₀-consAt`. ```agda (∃̇∈ (var e') (tag0At zero (suc m))) ∧̇ ((∀̇∈ (var e) (∃̇∈ (var (suc e')) (shiftPairAt zero (suc zero)))) ∧̇ (∀̇∈ (var e') ((tag0At zero (suc m)) ∨̇ (∃̇∈ (var (suc e)) (shiftPairAt (suc zero) zero))))) Δ₀-consAt : ∀ {n} (e' m e : Fin n) → Δ₀ (consAt e' m e) ``` The adequacy lemma carries one extra hypothesis, and it is what makes the conclusion true. Satisfaction of `consAt` alone says only that the new set stands to the old one in the cons relation; to name the old set as a graph, the lemma is given a function `g` of length `k` together with the path `⟦ var e ⟧ γ ≡ env g`. This is the encoded form that certificates hold: a candidate environment appears in a slot as a set, and the hypothesis identifies that set with the graph of the assignment it encodes. ```agda Δ₀-consAt e' m e = checkΔ₀ (consAt e' m e) tt consAt-adequate : ∀ {n} (e' m e : Fin n) (γ : (V ℓ) ^ n) {k : ℕ} (g : Fin k → V ℓ) → ⟦ var e ⟧ γ ≡ env g → (γ ⊨ consAt e' m e) ``` The conclusion is the analogous identification for the new slot: the value at `e'` equals the graph of `cons M g`, where `M` is the value at `m`. As with the earlier readers, the statement is a path of truth values, with the h-set property of `V ℓ` supplying the propositionhood of the equality. The abbreviations `M`, `E`, `E'` name the values at the three slots, and `⇔toPath` reduces the claim to the two inclusions. ```agda ≡ ((⟦ 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 ⟧ γ ``` The auxiliary `shift-path` records the renumbering arithmetic once: if two encoded entries are equal as pairs, then the entries with both keys replaced by their von Neumann successors and the values kept are equal as well. The injectivity of the Kuratowski pair `pr-inj` splits the assumed path into a path of keys and a path of values, and `cong₂` recombines them under the shifted pair constructor. ```agda E' = ⟦ var e' ⟧ γ G' : Fin (suc k) → V ℓ G' = cons M g shift-path : {a b x y : V ℓ} → pr a x ≡ pr b y → pr (sucV a) x ≡ pr (sucV b) y shift-path {a} {b} {x} {y} e = cong₂ (λ a b → pr (sucV a) b) (fst p) (snd p) ``` The forward inclusion takes the third clause of the formula and turns it into a genuine membership statement. Its hypothesis says: every member `y` of `E'` merely either satisfies the tagged zero reader in the environment extended by `y`, or satisfies the bounded existential whose witness is an entry of `E` shifting to `y`. The goal is that `y` belongs to `env G'`, the graph of the extended assignment. Note the shape of the hypothesis: it is the truncated disjunction exactly as the bounded universal quantifier of the formula produces it. ```agda where p : (a ≡ b) × (x ≡ y) p = pr-inj e classify : ((y : V ℓ) → ⟨ y ∈ E' ⟩ → ∥ ⟨ (y ∷ γ) ⊨ tag0At zero (suc m) ⟩ ``` The truncated disjunction can be eliminated only into a proposition-valued target, and membership in `env G'` is one. The two branches are then handled separately: the first receives the satisfaction of the tagged zero reader and produces the zero key of the graph. ```agda ⊎ ⟨ (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 → ``` In the first branch, the member `y` satisfies `tag0At zero (suc m)` in `y ∷ γ`, and the adequacy lemma for that reader converts the satisfaction into the path `y ≡ pr ∅ M`: the value in slot zero is `y` itself, and the original value at slot `m` is still addressed by `suc m` under the new binder. Reversing this path gives `pr ∅ M ≡ y`, which is exactly the entry of `env G'` at key zero, since `G' zero` computes to `M` and the numeral of zero computes to the empty set. The witness is therefore `lift zero` with that path. ```agda ∣ lift zero , sym (subst ⟨_⟩ (tag0At-adequate zero (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) ``` The second branch is the shift case, and it opens three nested truncations in turn. The satisfaction of the bounded existential yields merely an entry `p` of `E` together with a shift clause about the two-entry environment `p ∷ y ∷ γ`; the adequacy lemma for `shiftPairAt` converts that clause into the mere existence of sets `i` and `v` with `p ≡ pr i v` and `y ≡ pr (sucV i) v`. Here the roles of the two slots matter: in `shiftPairAt (suc zero) zero` the old entry sits in the later slot and the shifted one in slot zero, which is why `y` is the pair with the successor key. ```agda (λ { (i , v , epv , eyv) → ∣ lift (suc (lower li)) , sym (shift-path (sym epv ∙ sym peq)) ∙ sym eyv ∣₁ }) (subst ⟨_⟩ (shiftPairAt-adequate (suc zero) zero (p ∷ y ∷ γ)) sh) }) ``` In the shift case, once the index `i` and value `v` behind the old entry are explicit, the membership in `env G'` is assembled from what the graph of the extended assignment holds. Its entry at the successor of the old key carries the old value, so the required witness is the index `suc (lower li)` together with a path from that entry to `y`. The path is composed from three equations: the old entry equals the pair `pr i v`, shifting both keys by the von Neumann successor turns it into the pair with the shifted key and the same value, and the entry of `env G'` at that key equals `y`. What the composition records is exactly the mathematical content of the case: the new key is the successor of the old one and the value is preserved. ```agda (subst (λ z → ⟨ p ∈ z ⟩) hE p∈E) }) ssat)) (h₃ y y∈E') covered : ⟨ γ ⊨ ∃̇∈ (var e') (tag0At zero (suc m)) ⟩ → ((p : V ℓ) → ⟨ p ∈ E ⟩ ``` One step of the shift case remains. The entry `p` was found as a member of `E`, but the graph membership the argument needs sits in `env g`, and the hypothesis `E ≡ env g` transports the membership across. Inside the graph, the lookup lemma of the first section identifies the value stored at the key for the index the witness names. With this the first inclusion is complete: every member of the new set merely lands in the graph of the extended assignment. ```agda → ⟨ (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 }) y∈G' ``` The reverse inclusion must show that every member of the graph of the extended assignment belongs to the new set. Membership in a graph is truncated fiber data: an index of the graph together with a path saying that the entry at that index equals the given element. So a member `y` is read off with its index and entry path, and the proof then splits on the index, because the two defining equations of `cons` produce exactly two kinds of entries: the new one at index zero and the shifted old ones at successor indices. ```agda 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' ⟩) ``` In the zero case the entry equation computes to the statement that the entry with the empty tag and the value `M` equals `y`. The first clause of the formula supplies, merely, a member `q` of the new set whose tagged entry is the pair of the empty tag and `M`; its adequacy lemma turns the satisfaction into exactly that equality. Chaining the two paths gives `q ≡ y`, and transporting the membership of `q` along it yields the membership of `y` in the new set. Nothing about `q` beyond this equation is used, so the truncated witness inside the first clause is eliminated only into a proposition, as required. The successor case runs the argument the other way: the entry equation now names an old entry of `g`, and the second clause of the formula must produce its shift inside the new set. ```agda (subst ⟨_⟩ (tag0At-adequate zero (suc m) (q ∷ γ)) tsat ∙ eq) q∈E' }) h₁ byKey (suc i₀) eq = PT.rec ((y ∈ E') .snd) (λ { (p' , p'∈E' , sh) → PT.rec ((y ∈ E') .snd) ``` In the successor case, the shift clause of the formula yields an index `i`, a value `v`, and two equations: the old entry equals the pair `pr i v`, and the candidate equals the shifted pair `pr (sucV i) v`. The goal is a path from the candidate to the member `y`, and the fiber equation provides the shifted graph entry at the successor key, which equals `y`. Since the numeral of the successor index is the successor of the numeral, replacing both keys of the pair `pr i v` by their successors lands exactly on that graph entry. The three equations compose into the required path, and transporting the candidate's membership along it closes the case. ```agda (λ { (i , v , epv , ep'v) → subst (λ z → ⟨ z ∈ E' ⟩) (ep'v ∙ shift-path (sym epv) ∙ eq) ``` One input was still missing. The shift clause is a satisfaction statement evaluated in an environment whose second slot must hold the old entry `pr (# (toℕ i₀)) (g i₀)` itself, and the second clause of the formula supplies the corresponding membership. This is where the lookup lemma is spent: at the key for `i₀` the graph of `g` holds exactly `g i₀`, and the canonical fiber consisting of the index and `refl` witnesses that membership. Transporting it along the hypothesis that the old set equals the graph of `g` turns it into membership in the encoded environment. ```agda 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 ∣₁)) ``` With both inclusions established, the forward direction of the adequacy lemma is a single appeal to extensionality of the cumulative hierarchy: two sets with the same members are equal. The three clauses of the formula supply, for each element `y`, the two directions of the membership comparison: from a member of the new set into the graph of the extended assignment, and back. Read in this direction, satisfaction of the formula is converted into an equality of encoded graphs. The remaining direction of the lemma constructs the satisfaction from such an equality. ```agda fwd : ⟨ γ ⊨ consAt e' m e ⟩ → E' ≡ env G' fwd (h₁ , h₂ , h₃) = extensionalV (λ y → ⇔toPath (classify h₃ y) (covered h₁ h₂ y)) bwd : E' ≡ env G' → ⟨ γ ⊨ consAt e' m e ⟩ bwd e'eq = ``` The backward direction starts from a path identifying the new set with the graph of the extended assignment and builds the three satisfaction clauses directly. The first clause exhibits the entry at key zero: membership in the graph at index zero holds by the defining equation of `cons`, and the assumed path transfers it to membership in the new set. The tagged-entry clause then holds outright, since the entry with the empty tag and the value `M` is by construction the pair `pr ∅ M`, and the numeral of zero is the empty set. ```agda ∣ pr (# 0) M , subst (λ z → ⟨ pr (# 0) M ∈ z ⟩) (sym e'eq) ∣ lift zero , refl ∣₁ , subst ⟨_⟩ (sym (tag0At-adequate zero (suc m) (pr (# 0) M ∷ γ))) refl ∣₁ , (λ p p∈E → PT.rec (((p ∷ γ) ⊨ ∃̇∈ (var (suc e')) (shiftPairAt zero (suc zero))) .snd) ``` The second clause must produce, for every member of the old environment, its shifted counterpart inside the new set. The member's membership transports along the hypothesis to the graph of `g`, where the lookup lemma reads off an index and the equation identifying the entry with the member. The shifted entry is then the pair with the successor numeral as key and the same value; its membership in the new set again comes from the graph of the extended assignment, at the successor index, transferred through the assumed path. What remains is the satisfaction certificate for the shift formula itself. ```agda (λ { (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 ⟨_⟩ ``` The certificate is produced by running the shift adequacy lemma backwards. Its reading of the formula asks for an index, a value, and two equations: one identifying the old entry with the pair at the index found by lookup, and one saying that the shifted pair is the shifted entry itself, which holds by computation. Because the adequacy statement is an equality of propositions, transporting `refl` along it yields the required satisfaction, and the second clause of the formula is complete for this member. ```agda (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₁ ``` The third clause is the classification clause: every member of the new environment must satisfy one of the two tagged clauses, merely. To use it, a member `p'` of `E'` is first transported along the path `e'eq` into membership in the encoded graph `env G'`, which is truncated fiber data: an index `j` and the equation `pr (# (toℕ j)) (G' j) ≡ p'` saying that the entry at that key is `p'`. The proof now splits on the index, because the consed graph has exactly two kinds of entries, one for each equation defining `cons`. Since the goal is a truncated disjunction of two propositions, each case may return its clause under the corresponding disjunct, and the truncation wraps the case distinction. ```agda (λ { (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' ``` At index zero the entry of `G'` is the new one: the equation is `pr (# 0) M ≡ p'`. This is the statement, up to the direction of the path, that `p'` carries the empty tag with value `M`. The adequacy lemma for the tagged reader identifies its satisfaction proposition with the equality `⟦ var zero ⟧ (p' ∷ γ) ≡ pr ∅ M`, and `# 0` computes to `∅`. So the reversed equation, transported along the adequacy path, yields the left disjunct. ```agda → ∥ ⟨ (p' ∷ γ) ⊨ tag0At zero (suc m) ⟩ ⊎ ⟨ (p' ∷ γ) ⊨ ∃̇∈ (var (suc e)) (shiftPairAt (suc zero) zero) ⟩ ∥₁ byKey' p' zero eq = ∣ inl (subst ⟨_⟩ (sym (tag0At-adequate zero (suc m) (p' ∷ γ))) (sym eq)) ∣₁ byKey' p' (suc i₀) eq = ``` At a successor index, the entry of `G'` is a shifted old entry, and the right disjunct must certify this with the shift formula. The fiber the shift formula asks for has five components, of which the index-as-set and the value slot are straightforward. The old entry slot needs `pr (# (toℕ i₀)) (g i₀)` to be a member of the old environment, which follows from `lookup-spec`: at index `i₀` of `env g`, the entry at that key is the pair with value `g i₀`, and this membership is transported along `hE` into membership in `E`. The shifted entry slot is filled by the numeral-keyed entry `pr (# (toℕ i₀)) (g i₀)` itself, which by `eq` equals `p'`, up to orientation. ```agda ∣ 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 ``` The two remaining paths complete the fiber. The old-entry path is definitional: the chosen index and value are exactly the numeral of `i₀` and `g i₀`. The shifted path is the reversed `eq`, since the shifted entry is required to equal the candidate pair with the successor key, and that pair is `p'` by assumption. Running the adequacy lemma of `shiftPairAt (suc zero) zero` backwards converts the assembled fiber into its satisfaction, which sits in the right disjunct. Both branches of the case split thus supply their clause merely, exactly as the truncated disjunction of the third clause demands. ```agda (pr (# (toℕ i₀)) (g i₀) ∷ p' ∷ γ))) ∣ # (toℕ i₀) , g i₀ , refl , sym eq ∣₁ ∣₁ ∣₁ ``` ## Recap The chapter turned the two environment operations that satisfaction clauses need into statements about sets: looking a value up, and extending an assignment under a quantifier. The encoding itself is `env`, which stores an assignment as the graph of numeral-keyed pairs, and `lookup-spec` shows the graph is functional: membership of a pair at key `i` holds exactly when its value is `g i`. On the operation side, `sucAt` characterizes the von Neumann successor of a set by the three membership clauses the language can express, and `shiftPairAt` recognizes a single renumbered entry. `consAt` assembles these into the whole transformation: assuming the old slot is the graph of `g`, satisfaction of the formula is the equality of the new slot with the graph of `cons M g`, proved by two inclusions compared through set extensionality, with the truncated witnesses eliminated only into propositions.