BedrockThe satisfaction graph formula
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapThe recursive construction Sat assigns a set of satisfying environments to each formula, but that metatheoretic assignment cannot simply be named inside a first-order definition over L. The task of this chapter is to give a binary object-language formula that can later serve as the relation for such queries. Its witnesses will describe enough local data to satisfy the recursion equations around the queried key, without assuming in advance that a canonical or single-valued table has already been obtained.
{-# OPTIONS --cubical --safe --guardedness #-}
Excluded middle is available at the required universe level because the environment-tower interface used below carries that assumption. The formula assembled in this chapter does not itself decide propositions by cases; its quantifiers and connectives receive their meaning from the established first-order semantics.
open import Base.Prelude open import Base.Classical using ( LEM )
Fix a universe level and this one classical parameter. The relation to be defined holds of a formula key x and a set y exactly when some locally qualified candidate satisfaction table over the carrier records y at x. At this stage it asserts only the existence of such local data; it neither selects a canonical table nor proves that every key has a unique value.
module L.Coding.SatisfactionGraph {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
The formula language provides variables, constants, equality, conjunction, and existential quantification. Constants allow fixed constructible sets, such as the standard numerals used for tags, to occur directly in a formula, while pr encodes the ordered pairs used as graph entries. The ambient hierarchy supplies the semantics in which these formulas will be read.
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _≐_; _∧̇_; ∃̇_ ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr )
Three descriptions organize the candidate data. appAt reads an encoded pair as a graph entry, domAt T C says that the key domain of the table T is exactly C, and closedAt C requires the keys in C to contain the direct subformula keys needed by compound formulas. The domain in domAt is the table's domain of keys; it is distinct from the environment sets that later occur as table values.
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Model {ℓ} using ( domAt; appAt; appAt-adequate ) open import L.Coding.Closure {ℓ} using ( closedAt ) open import L.Coding.Quantification {ℓ} using ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9; i0; i1; i2; i3; i4; i5; i6; i7; i8; i9; i10; i11; i12; i13; sh )
The remaining descriptions prepare the local recursion equations. towerAt supplies candidate rows of encoded environments, Tags calibrates the ten constructor-tag slots, and tableAt combines propositional totality on the candidate key set, restriction of table entries to that set, and ten local extensional equations. These ingredients still describe only a candidate relation. PinnedRecursion proves the conditional uniqueness needed at a genuine formula key, while SatisfactionBridge independently interprets membership in the external value Sat as satisfaction in the restricted structure. UniformSatisfaction then combines existence with pinned uniqueness on AllCodes B to obtain a uniform table.
open import L.Coding.EnvironmentTower {ℓ} lem using ( nn; towerAt ) open import L.Coding.CodeDomain {ℓ} using ( Tags ) open import L.Coding.SatisfactionClauses {ℓ} using ( tableAt ) open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.FinData using ( toℕ )
An interpretation environment for a formula with n free positions is a vector of n carrier elements. lookup reads the element assigned to a position, while cons extends an environment at its innermost end. This fixed convention will let fourteen auxiliary witnesses be placed in front of an arbitrary outer environment without losing the original query positions.
open import Cubical.Data.Vec using ( _∷_; []; lookup )
Object-language existence is interpreted by propositional truncation. Thus a proof of an existential formula records that a witness exists while forgetting which witness was used. This is essential for the satisfaction graph: the public reading may establish that suitable tags, a tower, a key set, and a table exist, but it does not expose data from which a caller could choose one candidate table globally.
import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
From now on S is the carrier of the constructible structure: an element consists of a hierarchy set together with evidence of constructibility. Relations in this structure have proposition-valued truth values, and brackets expose the underlying proposition whose inhabitants are proofs. Equality or membership of the underlying hierarchy sets must therefore remain distinct from an object-language formula that asserts equality or membership.
open hPropStructure 𝒮ʟ
The judgment γ ⊨ φ now means that the object-language formula φ holds under the constructible environment γ. It connects the finite vector of semantic values to the syntax of the formula. In particular, the outer environment used to ask about a key and a proposed value is a metatheoretic assignment; it is not one of the encoded environment sets arranged in the tower.
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
The guarded recursion frame
The first four names describe the structural core of the fourteen new positions. From the innermost position outward they hold the carrier b, the candidate satisfaction table T, its candidate key set C, and the candidate environment tower E. Keeping these roles separate prevents two tempting confusions: elements of C are formula keys, whereas elements of T encode key-value pairs, and the rows represented through E organize encoded environments by arity.
Bi Ti Ci Ei : ∀ {n} → Fin (14 + n) Bi = i0 Ti = i1 Ci = i2 Ei = i3
The next ten positions are constructor tags. NN begins their common address map by sending constructor indices zero through three to positions i4 through i7. Before calibration these positions may contain arbitrary carrier elements, so the local clauses merely use them as parameters identifying code shapes.
NN : ∀ {n} → Fin 10 → Fin (14 + n) NN zero = i4 NN (suc zero) = i5 NN (suc (suc zero)) = i6 NN (suc (suc (suc zero))) = i7
The same map continues consecutively through constructor eight. This uniform indexing matters because closure and the ten table equations must agree on which numeral marks each formula constructor. Once that agreement is fixed, one family of clauses can cover atoms, the three binary connectives, falsity, the two unbounded quantifiers, and the two bounded quantifiers.
NN (suc (suc (suc (suc zero)))) = i8 NN (suc (suc (suc (suc (suc zero))))) = i9 NN (suc (suc (suc (suc (suc (suc zero)))))) = i10 NN (suc (suc (suc (suc (suc (suc (suc zero))))))) = i11 NN (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = i12
The last equation places constructor nine at i13, completing the layout b, T, C, E, N0, ..., N9 from the innermost position outward. The environment tower occupies one position as the candidate set E; its arity-indexed rows are encoded entries described by towerAt, rather than ten further positions in this vector.
NN (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = i13
The query key and proposed value remain in the caller's environment outside these fourteen positions. The shift sh14 moves either original position across all fourteen binders, so a later occurrence such as appAt Ti (sh14 x) (sh14 y) still asks whether the original pair (x,y) is recorded in T.
sh14 : ∀ {n} → Fin n → Fin (14 + n) sh14 i = sh 14 i
The function ev is the semantic realization of this position map. It places b, T, C, E, and the ten values supplied by ν in front of the outer environment γ. Consequently every named slot used by Tags, towerAt, closedAt, domAt, and tableAt refers to the same witness throughout the argument.
ev : ∀ {n} → (Fin 10 → S) → S → S → S → S → S ^ n → S ^ (14 + n) ev ν E C T b γ = b ∷ T ∷ C ∷ E ∷ ν f0 ∷ ν f1 ∷ ν f2 ∷ ν f3 ∷ ν f4 ∷ ν f5 ∷ ν f6 ∷ ν f7 ∷ ν f8 ∷ ν f9 ∷ γ
For the canonical tag assignment, constructor index k is sent to the model numeral nn (toℕ k). Its underlying hierarchy set is the finite ordinal representing k, while its second component certifies constructibility. Packaging the numeral as an element of S lets the object language name it by a constant.
numν : Fin 10 → S numν k = nn (toℕ k)
Tags γ NN asks, for every constructor index k, whether the underlying set at position NN k is the numeral for k. In the environment built from numν, the first four cases hold by reflexivity because lookup and first projection compute to that numeral. The statement compares underlying sets, so it does not require the constructibility certificates themselves to be definitionally equal.
numTags : ∀ {n} (E C T b : S) (γ : S ^ n) → Tags (ev numν E C T b γ) NN numTags E C T b γ zero = refl numTags E C T b γ (suc zero) = refl numTags E C T b γ (suc (suc zero)) = refl numTags E C T b γ (suc (suc (suc zero))) = refl
Reflexivity also proves the cases for indices four through eight. The longer successor patterns carry only the finite-index bookkeeping: NN k selects the slot occupied by numν k, whose first projection is the required numeral. Thus the proof remains pointwise and introduces no constructor-specific semantic assumption.
numTags E C T b γ (suc (suc (suc (suc zero)))) = refl numTags E C T b γ (suc (suc (suc (suc (suc zero))))) = refl numTags E C T b γ (suc (suc (suc (suc (suc (suc zero)))))) = refl numTags E C T b γ (suc (suc (suc (suc (suc (suc (suc zero))))))) = refl numTags E C T b γ (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = refl
Index nine exhausts Fin 10, so the same reflexivity argument completes a total proof of Tags for the canonical assignment. Other assignments may still serve as candidate witnesses, but they must carry their own proof of this pointwise agreement before the ten constructor clauses acquire the intended tags.
numTags E C T b γ (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = refl
The object-language formula numsAt begins the same calibration as a right-associated conjunction of equations. Its first eight equations say that the values at positions i4 through i11 are the constants nn 0 through nn 7. Thus the later variable-carrier form of the graph avoids naming the carrier as a constant, but the graph formula still names these fixed standard numerals.
numsAt : ∀ {n} → Formula S (14 + n) numsAt = (var i4 ≐ con (nn 0)) ∧̇ ((var i5 ≐ con (nn 1)) ∧̇ ((var i6 ≐ con (nn 2)) ∧̇ ((var i7 ≐ con (nn 3)) ∧̇ ((var i8 ≐ con (nn 4)) ∧̇ ((var i9 ≐ con (nn 5)) ∧̇ ((var i10 ≐ con (nn 6)) ∧̇ ((var i11 ≐ con (nn 7)) ∧̇
The equations for i12 and i13 finish the calibration with numerals eight and nine. Satisfaction of the complete conjunction therefore carries exactly the ten equations required by Tags; the following read lemma extracts those equations from the nested conjunction. This calibration identifies constructor tags only and adds no claim that the candidate key set is the complete set of well-formed formula codes.
((var i12 ≐ con (nn 8)) ∧̇ (var i13 ≐ con (nn 9))))))))))
nums-out turns satisfaction of numsAt into the host-level family Tags. Since conjunction is interpreted as a pair, the case for tag zero takes the first projection, and the cases for tags one and two follow the second projection before taking the next first projection. The lemma works for an arbitrary tag assignment ν, so it can decode the calibration carried by any candidate graph witness.
nums-out : ∀ {n} (ν : Fin 10 → S) (E C T b : S) (γ : S ^ n) → ⟨ ev ν E C T b γ ⊨ numsAt ⟩ → Tags (ev ν E C T b γ) NN nums-out ν E C T b γ h zero = h .fst nums-out ν E C T b γ h (suc zero) = h .snd .fst nums-out ν E C T b γ h (suc (suc zero)) = h .snd .snd .fst
For every higher index, nums-out follows the second projection of the right-associated product until it reaches the corresponding equality. This is only elimination of conjunction: it neither chooses tag values nor proves them unique. When the fourteen existential witnesses are later eliminated under propositional truncation, these projections recover the tag certificate already present in the formula's satisfaction.
nums-out ν E C T b γ h (suc (suc (suc zero))) = h .snd .snd .snd .fst nums-out ν E C T b γ h (suc (suc (suc (suc zero)))) = h .snd .snd .snd .snd .fst nums-out ν E C T b γ h (suc (suc (suc (suc (suc zero))))) = h .snd .snd .snd .snd .snd .fst nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc zero)))))) = h .snd .snd .snd .snd .snd .snd .fst nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc (suc zero))))))) = h .snd .snd .snd .snd .snd .snd .snd .fst
The deepest component of the right-associated conjunction is the pair of equations for tags eight and nine. Its two projections complete the pointwise family, so satisfaction of numsAt yields agreement at every index of Fin 10 at once. This step only repackages the ten equations; it adds no condition on the candidate key set or table.
nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = h .snd .snd .snd .snd .snd .snd .snd .snd .fst nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = h .snd .snd .snd .snd .snd .snd .snd .snd .snd
The converse reading nums-in starts from Tags: for each constructor index, the chosen tag has the same underlying set as the corresponding standard numeral. Placing these ten equalities into the right-associated conjunction proves numsAt. Together, nums-out and nums-in let the rest of the chapter move in either direction between the object-language calibration and its host-level family of equalities.
nums-in : ∀ {n} (ν : Fin 10 → S) (E C T b : S) (γ : S ^ n) → Tags (ev ν E C T b γ) NN → ⟨ ev ν E C T b γ ⊨ numsAt ⟩ nums-in ν E C T b γ tg = tg f0 , (tg f1 , (tg f2 , (tg f3 , (tg f4 , (tg f5 , (tg f6 , (tg f7 , (tg f8 , tg f9))))))))
The auxiliary family satGraphOn now assembles the complete frame. Its parameter pin is a formula over the extended environment and specifies only how the newly bound carrier is related to an outer reference; the query positions x and y remain in the outer environment. Fourteen nested existentials bind the ten tags, the tower, the key set, the table, and finally the innermost carrier. Their first conjunct is pin, so changing the carrier policy leaves every other condition of the candidate graph unchanged.
private satGraphOn : ∀ {n} → Formula S (14 + n) → Fin n → Fin n → Formula S n satGraphOn pin x y = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (( pin
After the pin, the conjunction records the conditions needed to interpret one table entry. The calibration numsAt identifies the ten tag slots with the standard numerals. The clause towerAt Ei Bi (NN f0) requires the candidate tower to have the row structure used by the recursive clauses over the bound carrier; it does not assert that the tower is canonical. The clause closedAt Ci closes the candidate key set under the seven possible immediate subformula keys. Next, domAt Ti Ci says that the key domain of the table is exactly C, while appAt Ti (sh14 x) (sh14 y) says that the original query pair is an entry after x and y have been shifted past all fourteen binders.
∧̇ ( numsAt ∧̇ ( towerAt Ei Bi (NN f0) ∧̇ ( closedAt Ci ∧̇ ( domAt Ti Ci ∧̇ ( appAt Ti (sh14 x) (sh14 y)
The final conjunct tableAt Ti Bi Ci Ei NN supplies the local recursion specification. Its first domain condition gives, under propositional truncation, some value for every key in C; its second says that every member of T can be decomposed, again under truncation, as a key from C paired with a value. The remaining ten clauses characterize matching entries by extensional equations, one for each formula constructor. These conditions describe a candidate relation locally. They neither make T single-valued nor choose a value for each key. Uniqueness at a genuine formula key is proved later by structural induction in PinnedRecursion.
∧̇ tableAt Ti Bi Ci Ei NN ))))))))))))))))))))
Witnesses for the satisfaction graph
The host-level type GraphWitOn flattens the same information into five pieces of data, ν, E, C, T, and b, followed by seven certificates. They assert equality of the underlying sets of b and the reference W, agreement of all ten tags, satisfaction of the tower, closure, and exact-domain clauses at the assembled environment, membership of the query pair in the underlying table, and satisfaction of tableAt. The two domain certificates have different later uses: domAt lets a consumer infer that a queried key lies in C, whereas the totality component inside tableAt supplies values for subkeys during structural induction. Public readings expose this concrete record only through propositional truncation, so they establish existence without selecting a particular candidate table.
private GraphWitOn : ∀ {n} → S → Fin n → Fin n → S ^ n → Type (ℓ-suc ℓ) GraphWitOn W x y γ = Σ[ ν ∈ (Fin 10 → S) ] (Σ[ E ∈ S ] (Σ[ C ∈ S ] (Σ[ T ∈ S ] (Σ[ b ∈ S ] ((fst b ≡ fst W) × (Tags (ev ν E C T b γ) NN × (⟨ (ev ν E C T b γ) ⊨ towerAt Ei Bi (NN f0) ⟩ × (⟨ (ev ν E C T b γ) ⊨ closedAt Ci ⟩ × (⟨ (ev ν E C T b γ) ⊨ domAt Ti Ci ⟩ × (⟨ pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst T ⟩ × ⟨ (ev ν E C T b γ) ⊨ tableAt Ti Bi Ci Ei NN ⟩))))))))))
To compare satisfaction of satGraphOn with the flat record, fix the pin, its reference W, the query positions, and the outer environment. Every field of the record except the carrier equation already has a fixed interpretation among the frame's conjuncts. The only extra hypothesis is therefore a reading rd for the pin. The inward implication turns an equality fst b ≡ fst W into satisfaction of pin; the outward implication reads satisfaction of pin back as that equality.
module _ {n : ℕ} (pin : Formula S (14 + n)) (W : S) (x y : Fin n) (γ : S ^ n) where
The inward reading turns a truncated witness record into satisfaction of the whole frame. Its hypothesis rd says how the pin is to be read: for any choice of the ten tag values, the tower, the index set, the table and the carrier, if the carrier agrees with the reference, then the pin is satisfied at the assembled environment. The input is a truncation and the output is a satisfaction, itself a truncation, so the whole proof is a map inside truncations: it sends the flat record, matched component by component, to the fourteen-level witness the formula demands. No witness is selected anywhere; a map between truncations transports only the fact that witnesses exist.
graphOn-in : ((ν : Fin 10 → S) (E C T b : S) → fst b ≡ fst W → ⟨ ev ν E C T b γ ⊨ pin ⟩) → ∥ GraphWitOn W x y γ ∥₁ → ⟨ γ ⊨ satGraphOn pin x y ⟩ graphOn-in rd = PT.map (λ { (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12))))))))))) →
The flat record is re-nested in the reverse of the layout order. The outermost existential receives the tag of the ninth constructor, the next one the eighth, and so on, until the innermost existential receives the carrier; this is exactly the de Bruijn order of the layout, read from the outside in. The pin's satisfaction is supplied by rd, applied to the assembled witnesses and to the carrier equation the record carries. The calibration is converted by nums-in from the host-level agreement into satisfaction of the ten equations, so that every later conjunct meets standard numerals.
ν f9 , ∣ ν f8 , ∣ ν f7 , ∣ ν f6 , ∣ ν f5 , ∣ ν f4 , ∣ ν f3 , ∣ ν f2 , ∣ ν f1 , ∣ ν f0 , ∣ E , ∣ C , ∣ T , ∣ b , ( rd ν E C T b eb , ( nums-in ν E C T b γ tg
The three guard certificates pass through unchanged: they are satisfactions of formulas read at the very environment the frame assembles, so they can stand where the conjuncts stand. The query entry is the one component that must change languages. On the host side it is an ordinary membership: the ordered pair of the two query values belongs to the underlying set of the table. The adequacy law of the application atom identifies satisfaction of the atom with exactly this membership, and the proof transports along that one path. This is the single substantial bridge of the inward direction; everything else is re-packing.
, ( hE , ( hc , ( hd , ( subst ⟨_⟩ (sym (appAt-adequate Ti (sh14 x) (sh14 y) (ev ν E C T b γ))) ha
After the clause-family certificate has been placed in the last conjunct, the only remaining work is to restore the nested truncations. The call to PT.map supplies the outermost truncation: its mapping function returns the witness pair for the outermost existential. Inside that pair, the thirteen explicit insertions supply the remaining existential layers down to the carrier. Thus the construction turns the truncated flat record into satisfaction of all fourteen nested existentials without exposing any of its chosen data outside a truncation.
, h12 )))))) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ })
The outward reading reverses the journey, and its hypothesis rd now runs the pin the other way: from a satisfaction of the pin at an assembled environment, it recovers the carrier equation. The input is a satisfaction of the whole frame, whose fourteen existentials are all truncated, and the output is the truncated witness record. The proof eliminates the existentials one level at a time, and every elimination targets the truncation of the record, a proposition, so each one is legitimate: the lemma never claims to produce the record itself, only the fact that one exists.
graphOn-out : ((ν : Fin 10 → S) (E C T b : S) → ⟨ ev ν E C T b γ ⊨ pin ⟩ → fst b ≡ fst W) → ⟨ γ ⊨ satGraphOn pin x y ⟩ → ∥ GraphWitOn W x y γ ∥₁ graphOn-out rd h = PT.rec squash₁ (λ { (n9 , h9) → PT.rec squash₁ (λ { (n8 , h8) →
Each application of PT.rec removes one truncated tag witness while keeping the same propositional target ∥ GraphWitOn W x y γ ∥₁. The values recovered for slots nine through three may therefore be passed to the next continuation, but none can escape into untruncated data. Repeating this one legitimate elimination is what makes the nested object-language existentials compatible with one flat truncated record.
PT.rec squash₁ (λ { (n7 , h7) → PT.rec squash₁ (λ { (n6 , h6) → PT.rec squash₁ (λ { (n5 , h5) → PT.rec squash₁ (λ { (n4 , h4) → PT.rec squash₁ (λ { (n3 , h3) →
Once all ten tag values have been recovered, the same propositional elimination reaches the candidate tower E and key set C. The names hE' and hC' denote the truncated tails that still contain the table, carrier, and certificates; they are not proofs of the tower or closure conditions. Those proofs remain inside the final conjunction and will enter the record only after T and b have also been exposed within the truncation.
PT.rec squash₁ (λ { (n2 , h2) → PT.rec squash₁ (λ { (n1 , h1) → PT.rec squash₁ (λ { (n0 , h0) → PT.rec squash₁ (λ { (E , hE') → PT.rec squash₁ (λ { (C , hC') →
At the innermost level the proof maps rather than eliminates further. What remains is a truncation whose content is the carrier record, and a map sends it, component by component, into the truncated flat witness. The tag function is rebuilt from the ten named slots by a small function defined below the readings, and rd, applied to the rebuilt function, the three structural witnesses, the carrier and the pin's satisfaction, delivers the carrier equation that heads the record. Every operation here stays inside truncations: the map transports the fact that a record exists, and constructs the corresponding fact on the other side.
PT.rec squash₁ (λ { (T , hT') → PT.map (λ { (b , (hpin , (hnum , (hE , (hc , (hd , (ha , h12))))))) → let ν : Fin 10 → S ν = ν' n0 n1 n2 n3 n4 n5 n6 n7 n8 n9 in ν , (E , (C , (T , (b , (rd ν E C T b hpin
The remaining fields are recovered in the directions required by the flat record. The calibration conjunct is read by nums-out as the host-level Tags family. The tower, closure, and exact-domain satisfactions already have the required types and are retained unchanged. Satisfaction of the query atom is the one field that crosses back to an ordinary membership: transport along appAt-adequate turns it into membership of the ordered query pair in the underlying set of T.
, ( nums-out ν E C T b γ hnum , ( hE , ( hc , ( hd , ( subst ⟨_⟩
Satisfaction of tableAt supplies the last certificate of the record. Applying the accumulated continuations then discharges the nested eliminations and yields an element of ∥ GraphWitOn W x y γ ∥₁. Together, the two readings show that frame satisfaction and the truncated existence of a qualified flat record imply one another. This is a pair of implications between propositions, not a procedure for choosing a canonical table, and it contains no uniqueness claim for table values.
(appAt-adequate Ti (sh14 x) (sh14 y) (ev ν E C T b γ)) ha , h12 )))))))))) }) hT' }) hC' }) hE' }) h0 }) h1 }) h2 }) h3 }) h4 }) h5 }) h6 }) h7 }) h8 }) h9 }) h where
The existential formula presents the ten tags as ten separate bound values, whereas GraphWitOn expects one function Fin 10 → S. The local function ν' reconciles these presentations by case analysis on the constructor index. Its first four branches return a0 through a3; no semantic fact is used here, only the fixed correspondence between indices and the slots already recovered from the formula.
ν' : S → S → S → S → S → S → S → S → S → S → Fin 10 → S ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 zero = a0 ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc zero) = a1 ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc zero)) = a2 ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc zero))) = a3
For constructor indices four through eight, the same case analysis returns the correspondingly named values a4 through a8. Because these branches follow the indexing map NN, the equalities extracted by nums-out apply to the reconstructed function at precisely the slots where the table and closure clauses expect those tags.
ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc zero)))) = a4 ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc zero))))) = a5 ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc zero)))))) = a6 ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc (suc zero))))))) = a7 ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = a8
The case at index nine exhausts Fin 10 and makes ν' a total function. Thus the fourteen separate object-language witnesses are represented in the host record by exactly one ten-entry tag function together with E, C, T, and b. This is only a change of presentation: it creates no new tag and discards none of the existential data.
ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = a9
The carrier supplied by a variable
The variable-carrier witness type chooses its reference from the ambient environment. In GraphWitAt B x y γ, the internal carrier b is required to have the same underlying set as lookup B γ; the proof does not identify the packaged elements themselves. Because the reference is obtained by lookup, the same witness type remains meaningful when later formulas add binders around the graph and shift the carrier slot accordingly.
GraphWitAt : ∀ {n} → Fin n → Fin n → Fin n → S ^ n → Type (ℓ-suc ℓ) GraphWitAt B x y γ = GraphWitOn (lookup B γ) x y γ
The formula satGraphAt B x y implements this reference by using the pin var Bi ≐ var (sh14 B): the newly bound carrier slot is equated with the original carrier slot after that slot has been shifted past all fourteen internal binders. This instance therefore does not insert the carrier as a constant, although the ten standard numeral constants in numsAt remain. The formula is opaque so that larger descriptions can use it as one relation; its witness readings provide the public way to establish or consume its satisfaction.
opaque satGraphAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n satGraphAt B x y = satGraphOn (var Bi ≐ var (sh14 B)) x y
The body of satGraphAt is unfolded only while its two witness implications are established. Inside this scope the proof may compare the large formula with GraphWitAt field by field. Outside it, later mathematics uses the exact statements of graphAt-in and graphAt-out, so the fourteen binders remain an internal presentation of the same relation.
opaque unfolding satGraphAt
For the inward reading, the pin hypothesis is the identity: satisfaction of the variable equality is exactly the underlying-set equality already stored in GraphWitAt. Hence a truncated witness record at any ambient environment gives satisfaction of satGraphAt there. This flexibility is used concretely in DefAt, where DefBody places the graph below the element slot and two adjacent existentials, and in DenoteBody, where the graph reaches the same carrier through five added slots. In both cases the carrier stays in the caller's environment rather than being substituted into the graph as a constant.
graphAt-in : ∀ {n} (B x y : Fin n) (γ : S ^ n) → ∥ GraphWitAt B x y γ ∥₁ → ⟨ γ ⊨ satGraphAt B x y ⟩ graphAt-in B x y γ = graphOn-in (var Bi ≐ var (sh14 B)) (lookup B γ) x y γ (λ _ _ _ _ _ e → e)
The outward reading completes the variable-carrier interface. From a proof of satGraphAt B x y, it recovers, under propositional truncation, the same candidate data and certificates recorded by GraphWitAt B x y γ. In particular, the internally bound carrier agrees on underlying sets with the value of the outer slot B, while the queried key and value are still read from the outer slots x and y. The identity passed to graphOn-out reflects exactly this variable-to-variable pin. A consumer may eliminate the resulting truncation when proving a proposition, as the later uniqueness arguments do, but it cannot retain a chosen tower, closed key set, or table.
graphAt-out : ∀ {n} (B x y : Fin n) (γ : S ^ n) → ⟨ γ ⊨ satGraphAt B x y ⟩ → ∥ GraphWitAt B x y γ ∥₁ graphAt-out B x y γ = graphOn-out (var Bi ≐ var (sh14 B)) (lookup B γ) x y γ (λ _ _ _ _ _ h → h)
The carrier fixed as a constant
When the carrier is already available as an element B, the second instance uses the constant B instead of referring to an outer carrier slot. It has exactly two free positions: suc zero is the input key and zero is the proposed output value. The rest of the frame is unchanged, so the formula still says merely that some locally suitable candidate package records this query. In particular, SatisfactionClauses supplies totality and domain restriction for the candidate table together with its ten local equations; neither those clauses nor this instance by itself makes the graph single-valued.
opaque satGraph : S → Formula S 2 satGraph B = satGraphOn (var Bi ≐ con B) (suc zero) zero
The witness type makes the direction of this binary relation explicit. In the environment y ∷ x ∷ [], the innermost position contains y and the next contains x; hence GraphWit B x y says that the candidate table contains the encoded pair with key x and value y. Its reference carrier is the fixed element B. The record also contains calibrated tags, a candidate environment tower, a subcode-closed candidate key set, a table whose key domain is exactly that set, and the certificates required by tableAt. The key set is only locally closed; this definition does not identify it with the set of all genuine formula keys.
GraphWit : (B x y : S) → Type (ℓ-suc ℓ) GraphWit B x y = GraphWitOn B (suc zero) zero (y ∷ x ∷ [])
The constant pin admits the same two witness implications, proved by unfolding satGraph only in this scope. They turn the large existential formula into a stable binary relation: graph-in establishes the relation from a propositionally truncated candidate record, and graph-out recovers exactly such a truncation from the relation. This is the form in which UniformSatisfaction can use satGraph B as the graph parameter of abstract recursion.
opaque unfolding satGraph
The inward reading applies the general conversion with the constant pin. A record begins with an equality between the underlying sets of its bound carrier and B; satisfaction of the object-language equation var Bi ≐ con B has exactly that content, so the pin reader is the identity. The remaining fields already certify the tag calibration, tower and closure conditions, exact key domain, queried table entry, and packaged table conditions. Mapping this record through graphOn-in preserves its propositional truncation: it proves that a suitable package exists, without choosing one for later use.
graph-in : (B x y : S) → ∥ GraphWit B x y ∥₁ → ⟨ (y ∷ x ∷ []) ⊨ satGraph B ⟩ graph-in B x y = graphOn-in (var Bi ≐ con B) B (suc zero) zero (y ∷ x ∷ []) (λ _ _ _ _ _ e → e)
The outward reading reverses this conversion and completes the chapter: a satisfaction of the binary formula yields only the propositional truncation of a candidate record with the queried entry. This is the exact limit of the satisfaction graph formula. PinnedRecursion subsequently proves, by structural recursion on a genuine formula, that if its key lies in the candidate key set and the candidate table records a value there, then that value has the same underlying set as the externally defined value Sat. SatisfactionBridge separately gives that value its semantics by relating membership in it to satisfaction in the restricted structure. Finally, UniformSatisfaction uses satGraph B on the genuine domain AllCodes B; existence together with the pinned uniqueness there allows the abstract recursion theorem to assemble one uniform table. The present two readings supply the represented relation on which those later arguments operate, but do not themselves choose, prove unique, or semantically interpret a table.
graph-out : (B x y : S) → ⟨ (y ∷ x ∷ []) ⊨ satGraph B ⟩ → ∥ GraphWit B x y ∥₁ graph-out B x y = graphOn-out (var Bi ≐ con B) B (suc zero) zero (y ∷ x ∷ []) (λ _ _ _ _ _ h → h)