BedrockFinite environments as set-coded graphs
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapA 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.
{-# 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.
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.
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.
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.
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.
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.
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.
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.
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.
→ 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.
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 Δ₀.
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.
Δ₀-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.
→ ((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.
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.
(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.
(λ 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.
× ((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.
(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.
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.
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.
(∃̇∈ (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.
∧̇ 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.
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.
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.
⊨ 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.
, 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.
(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.
(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.
(λ { (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.
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.
∣ ⁅ 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.
, ∣ ⁅ 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.
, ∈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.
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.
, 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.
∣₁ ∣₁ ∣₁ ∣₁
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.
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 {∅}.
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.
∧̇ ((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 ∅.
∧̇ (∀̇∈ (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.
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.
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.
× (⟨ 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 ≡ ∅.
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.
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.
(∣ ∅ , (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.
, (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.
× ((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.
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.
→ ∥ Σ[ 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.
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.
× ((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 ∅.
(λ { (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.
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.
(∃̇∈ (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.
Δ₀-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.
≡ ((⟦ 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.
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.
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.
⊎ ⟨ (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.
∣ 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.
(λ { (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.
(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.
→ ⟨ (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.
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.
(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.
(λ { (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.
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.
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.
∣ 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.
(λ { (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.
(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.
(λ { (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.
→ ∥ ⟨ (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.
∣ 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.
(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.