BedrockRead this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapThe specification tableAt combines two domain conditions, total and onC, with ten constructor clauses. How does one constructor clause become a step in the semantic recursion? This chapter first reads each clause as an exact extensional condition on a candidate value set, then proves the same condition for the recursively constructed set SatW. Extensionality can identify the two values once the surrounding argument also supplies the matching code, its subvalues, and a table entry. The local bridges alone do not prove that a whole table is functional or uniquely determined.
{-# OPTIONS --cubical --safe --guardedness #-}
The argument takes excluded middle at level ℓ-suc ℓ as an explicit parameter. Decoding witnesses will nevertheless remain merely existent when their type has been propositionally truncated; the classical hypothesis does not turn those witnesses into chosen data.
open import Base.Prelude open import Base.Classical using ( LEM )
All subsequent constructions are relative to the fixed hypothesis lem. This keeps the logical cost visible when the local clause readers are later imported into the global soundness and completeness proofs.
module L.Coding.SatisfactionClauseSemantics {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
Two languages meet in this proof. The internal formulas describe coded tables inside L; the external formulas are interpreted recursively in the structure presented by W. The bridge must respect each formula constructor, including bounded quantifiers whose bounds are term values in the current environment.
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; Term; var; con; _∈̇_; _∧̇_; _∨̇_; _⇒̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∃̇∈; ∀̇∈ ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
A finite environment is represented internally by its graph of ordered pairs (i,v). Pair injectivity recovers an index and its value, while lookup-spec states that the canonical graph contains exactly the pair belonging to each host-level slot. Membership in envSet W n later says, merely, that a set is the graph of some length-n assignment into W.
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′ ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Coding.Environment {ℓ} using ( env; lookup-spec ) open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet ) open import L.Coding.Model {ℓ} using ( prAtL; container )
The internal clauses can inspect pair components only through bounded formulas. A container supplies one constructible set containing both components, so the pair readers can bind them without an unbounded search. The analogous consAtL reader connects the graph of x ∷ δ with the graph of δ, which is the semantic step needed for quantifiers.
open import L.Coding.Expressions {ℓ} using ( sucAtL; consAtL ) import L.Coding.Expressions {ℓ} as CodingExpressions module E = CodingExpressions.PairExpression open import L.Axioms.Basic {ℓ} using ( extensionalL ) open import L.Coding.Quantification {ℓ} using
Three kinds of finite index must remain distinct. A natural n is a formula arity, # n is its set-theoretic numeral inside a code, and Fin m selects a slot of a host-level vector of length m. The names i0 through i19 and the shift sh only manage the last of these: when a binder adds a value at the head, every older slot is shifted past it.
( i0; i1; i2; i3; i4; i5; i6; i8; i9; i11; i12; i14; i16; i17; i19; sh ; pr-out; pr-in; down; sndS; suc-out; suc-in ; sndEx; sndAll; bothEx ; sndEx-out; sndAll-in; bothEx-out; bothAll-in ; fillSnd; fillBoth; useSnd; useBoth )
The common table frame has a fixed nested shape. An environment-tower entry codes (ar,F), a formula key codes (ar,p), its payload codes (tag,r), and a table entry codes (c,yc). The readers below repeatedly peel these pairs so that a constructor relation can speak about the candidate value yc over the environment set F.
open import L.Coding.CodeDomain {ℓ} using ( Tags ) open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet ) open import L.Coding.SatisfactionClauses {ℓ} using ( extB; fstAll; subAt; subSucAt; tmIs; module Rel; module Clause )
The external environment is a finite vector, but the table stores a set-theoretic graph. Moving between them requires both host-level finite lookup and object-level pair membership. Products and coproducts then record the alternatives exposed by formula and term constructors without conflating those alternatives with the coded sets themselves.
open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.FinData using ( toℕ ) open import Cubical.Data.Vec using ( _∷_; []; lookup ) open import Cubical.Data.Sigma using ( _×_ ) open import Cubical.Data.Sum using ( _⊎_; inl; inr )
Most semantic comparisons are paths between propositions, obtained from implications in both directions. Propositional truncation is equally essential: pair decompositions and decoded environments may be used inside a proposition, while no global choice of their witnesses is produced.
open import Cubical.Foundations.Prelude using ( subst2 ) open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
All codes live in the cumulative hierarchy. Ordered-pair codes and the numerals # n are therefore actual sets, and their injectivity lets later proofs recover arities, tags, and payloads from equations between codes. The h-set structure of the hierarchy ensures that these recovered equalities are proposition-valued.
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet {ℓ} using ( #_; sucV )
The internal assignments range over the constructible carrier S, but their equations and memberships concern the underlying sets selected by fst. Bounded absoluteness supplies the interpretation of internal formulas in this carrier. Every reader therefore ends with a concrete statement about projected sets, ready to be compared with the external recursion.
open hPropStructure 𝒮ʟ using ( S ) module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ ) open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
Reading the shared frame
The central type records an extensional fact about a set y: every member of y belongs to F and satisfies the property, and conversely every member of F satisfying the property belongs to y. A value set is described by such a fact rather than by a chosen enumeration.
ExtFact : (y F : V ℓ) (P : S → Type (ℓ-suc ℓ)) → Type (ℓ-suc ℓ) ExtFact y F P = ((z : S) → ⟨ fst z ∈ y ⟩ → ⟨ fst z ∈ F ⟩ × P z) × ((z : S) → ⟨ fst z ∈ F ⟩ → P z → ⟨ fst z ∈ y ⟩)
The extensional set builder is read definitionally: satisfaction of the builder is literally the pair of the two membership directions, with the property evaluated in the environment extended by the bound variable.
module _ {j : ℕ} (y F : Fin j) (φ : Formula S (1 + j)) (δ : S ^ j) where extB-out : ⟨ δ ⊨ extB y F φ ⟩ → ExtFact (fst (lookup y δ)) (fst (lookup F δ)) (λ z → ⟨ (z ∷ δ) ⊨ φ ⟩) extB-out h = h
Filling is likewise definitional: an extensional fact is exactly satisfaction of the builder.
extB-in : ExtFact (fst (lookup y δ)) (fst (lookup F δ)) (λ z → ⟨ (z ∷ δ) ⊨ φ ⟩) → ⟨ δ ⊨ extB y F φ ⟩ extB-in h = h
Suppose y and y' satisfy the same extension condition over F: among the elements of F, membership in either set is characterized by the property P. Extensionality reduces equality of their underlying sets to two membership conversions. In the first direction, a member of y passes through the outward half of its extension fact and then through the inward half for y'.
ext-unique : (y y' F : S) (P : S → Type (ℓ-suc ℓ)) → ExtFact (fst y) (fst F) P → ExtFact (fst y') (fst F) P → fst y ≡ fst y' ext-unique y y' F P (o1 , i1') (o2 , i2') = cong fst (extensionalL {a = y} {b = y'} (λ z → ⇔toPath (λ hz → i2' z (o1 z hz .fst) (o1 z hz .snd))
The backward conversion closes the biconditional: a member of the right-hand side is first recognized as a member of F satisfying the property, and the second half of the extensional fact then returns its membership in y. Composing the two conversions gives the equality of the underlying sets of y and y'; what is identified is the underlying set, not any chosen coding evidence.
(λ hz → i1' z (o2 z hz .fst) (o2 z hz .snd))))
To use a subformula value, fix a table slot T, an arity slot ar, a payload slot a, and a body that expects four new entries. The reader will expose a matching table pair (c₁,ya) and place, in front of the old environment, the value ya, its key c₁, a container for the pair components, and a constructible representative of the table entry itself.
module _ {j : ℕ} (T ar a : Fin j) (body : Formula S (4 + j)) (δ : S ^ j) where private Tv = fst (lookup T δ) TS = lookup T δ A = fst (lookup ar δ)
Write A for the projected arity and Av for the projected payload. The matching condition for the subkey is then the single equation fst c₁ ≡ pr A Av, which keeps the coded key separate from the host-level slots that supplied its two components.
Av = fst (lookup a δ)
If subAt holds, every table entry whose underlying pair is (c₁,ya) and whose key satisfies c₁=(A,Av) yields the body. The body is evaluated at ya ∷ c₁ ∷ s ∷ e' ∷ δ, where e' represents that table entry and s is only a container exposing the two pair components. Neither auxiliary object is an additional semantic value.
subAt-out : ⟨ δ ⊨ subAt T ar a body ⟩ → (c₁ ya : S) (m : ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩) → fst c₁ ≡ pr A Av → ⟨ (ya ∷ c₁ ∷ container (down TS (pr (fst c₁) (fst ya)) m) c₁ ya refl .fst ∷ down TS (pr (fst c₁) (fst ya)) m ∷ δ) ⊨ body ⟩ subAt-out h c₁ ya m e =
The proof first applies the table-bounded universal to the concrete representative e' of (c₁,ya). The pair reader then supplies the two components c₁ and ya; finally pr-in turns the equation c₁=(A,Av) into the antecedent required by the internal implication. What remains is exactly the requested body at the four-slot extension.
useBoth i0 (down TS (pr (fst c₁) (fst ya)) m ∷ δ) c₁ ya refl (prAtL i1 (sh 4 ar) (sh 4 a) ⇒̇ body) (h (down TS (pr (fst c₁) (fst ya)) m) m) (pr-in i1 (sh 4 ar) (sh 4 a) (ya ∷ c₁ ∷ container (down TS (pr (fst c₁) (fst ya)) m) c₁ ya refl .fst ∷ down TS (pr (fst c₁) (fst ya)) m ∷ δ) e)
Filling is the converse: given a proof of the body for every matching table entry with its own container, the bounded universal over table entries holds. Note what this reader does not do: it does not select one entry, and it does not assert that the value ya is unique; it quantifies over all matching entries.
subAt-in : ((c₁ ya s e' : S) → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr A Av → ⟨ (ya ∷ c₁ ∷ s ∷ e' ∷ δ) ⊨ body ⟩) → ⟨ δ ⊨ subAt T ar a body ⟩ subAt-in g e' e'∈ = bothAll-in i0 (prAtL i1 (sh 4 ar) (sh 4 a) ⇒̇ body) (e' ∷ δ) (λ c₁ ya s s∈ c₁∈ ya∈ e hp → g c₁ ya s e' e'∈ e (pr-out i1 (sh 4 ar) (sh 4 a) (ya ∷ c₁ ∷ s ∷ e' ∷ δ) hp))
The second subclause reader is stated for the raised-arity shape: its body is extended by six slots, because the subformula of a quantified formula is read at the raised arity.
module _ {j : ℕ} (T ar a : Fin j) (body : Formula S (6 + j)) (δ : S ^ j) where private Tv = fst (lookup T δ) TS = lookup T δ A = fst (lookup ar δ)
The arity value of the outer formula is named, and the raised one is recovered separately inside the proof.
Av = fst (lookup a δ)
The raised reader uses a table entry at a key (ar',Av) together with the equation fst ar' ≡ sucV A. Its body is evaluated at ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ: the two containers s' and s merely make the components of the raised key and the table entry available to bounded formulas.
subSucAt-out : ⟨ δ ⊨ subSucAt T ar a body ⟩ → (c₁ ya ar' : S) (m : ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩) → (e : fst c₁ ≡ pr (fst ar') Av) → fst ar' ≡ sucV A → ⟨ (ar' ∷ container c₁ ar' (lookup a δ) e .fst ∷ ya ∷ c₁ ∷ container (down TS (pr (fst c₁) (fst ya)) m) c₁ ya refl .fst ∷ down TS (pr (fst c₁) (fst ya)) m ∷ δ) ⊨ body ⟩
Starting from the given table entry, the proof first obtains the four-slot statement h4 by decomposing (c₁,ya). It then supplies the candidate first component ar' to fstAll, proves c₁=(ar',Av) with pr-in, and proves ar'=suc A with suc-in. These two equations are precisely the guards needed before the body may be used.
subSucAt-out h c₁ ya ar' m e es = (h4 (container c₁ ar' (lookup a δ) e .fst) (container c₁ ar' (lookup a δ) e .snd .fst) ar' (container c₁ ar' (lookup a δ) e .snd .snd .fst) (pr-in (sh 2 i1) i0 (sh 2 (sh 4 a)) δ6 e)) (suc-in (sh 6 ar) i0 δ6 es)
The local name e'S is a constructible representative of the particular table entry (c₁,ya), obtained from its membership in T. The environment δ4 then places ya, c₁, a container for their pair, and e'S before δ; it does not contain a presentation of the whole table.
where e'S = down TS (pr (fst c₁) (fst ya)) m δ4 : S ^ (4 + j) δ4 = ya ∷ c₁ ∷ container e'S c₁ ya refl .fst ∷ e'S ∷ δ δ6 : S ^ (6 + j)
Applying useBoth to the chosen table entry removes the outer table quantifier and the pair decomposition in one step. The result h4 is the remaining fstAll statement at δ4; it still requires a candidate first component of c₁ and the equations identifying that component with the successor arity.
δ6 = ar' ∷ container c₁ ar' (lookup a δ) e .fst ∷ δ4 h4 : ⟨ δ4 ⊨ fstAll i1 (sh 4 a) (sucAtL (sh 6 ar) i0 ⇒̇ body) ⟩ h4 = useBoth i0 (e'S ∷ δ) c₁ ya refl (fstAll i1 (sh 4 a) (sucAtL (sh 6 ar) i0 ⇒̇ body)) (h e'S m)
For the converse direction, it is enough to prove the body uniformly for every possible table-entry decomposition and every possible first-component decomposition of its key. The two equations in the hypothesis ensure that only entries at (suc A,Av) matter; no particular entry or raised arity is selected globally.
subSucAt-in : ((c₁ ya ar' s s' e' : S) → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr (fst ar') Av → fst ar' ≡ sucV A → ⟨ (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) ⊨ body ⟩) → ⟨ δ ⊨ subSucAt T ar a body ⟩ subSucAt-in g e' e'∈ = bothAll-in i0 (fstAll i1 (sh 4 a) (sucAtL (sh 6 ar) i0 ⇒̇ body)) (e' ∷ δ)
The introduction proof receives the components exposed by the two universal pair readers. It uses pr-out to recover the equation c₁=(ar',Av) and suc-out to recover ar'=suc A, then passes those equations, the table memberships, and the six-slot environment to the uniform hypothesis g.
(λ c₁ ya s s∈ c₁∈ ya∈ e s' s'∈ ar' ar'∈ hp hs → g c₁ ya ar' s s' e' e'∈ e (pr-out (sh 2 i1) i0 (sh 2 (sh 4 a)) (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) hp) (suc-out (sh 6 ar) i0 (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) hs))
TmIsV t z v records the two possible term-code shapes, under propositional truncation. Either t=(#0,v), the constant case, or there merely exists an index i with t=(#1,i) and the graph entry (i,v) belonging to z, the variable case. For an arbitrary relation z, this statement contains no functionality or uniqueness claim.
TmIsV : V ℓ → V ℓ → V ℓ → Type (ℓ-suc ℓ) TmIsV t z v = ∥ (t ≡ pr (# 0) v) ⊎ (Σ[ i ∈ V ℓ ] ((t ≡ pr (# 1) i) × ⟨ pr i v ∈ z ⟩)) ∥₁
The local reader is parameterized by five host-level slots: the term code, the environment graph, its proposed value, and the two tag numerals. The hypotheses q0 and q1 identify the last two slots with #0 and #1; the local names Tv and Z project the term code and graph to the hierarchy where the coding equations live.
module _ {j : ℕ} (t z v N0 N1 : Fin j) (δ : S ^ j) (q0 : fst (lookup N0 δ) ≡ # 0) (q1 : fst (lookup N1 δ) ≡ # 1) where private Tv = fst (lookup t δ) Z = fst (lookup z δ)
The remaining projections name the proposed value Vv and the actual set stored in the tag-one slot, N1v. The proof must carry equations through q1 because the internal formula refers to N1v, whereas TmIsV states its variable branch with the canonical numeral #1.
Vv = fst (lookup v δ) N1v = fst (lookup N1 δ)
The inner bounded existential ranges over entries q of the graph z, not over indices themselves. Its pair atom asserts q=(i,v), where the index i was already recovered as the second component of the term code. Thus the internal formula says that the graph contains the entry pairing that fixed index with the proposed value.
inner : Formula S (2 + j) inner = ∃̇∈ (var (sh 2 z)) (prAtL i0 i1 (sh 3 v))
Inner i s repackages the semantics of that bounded existential. It merely supplies a graph entry q, a proof that q∈Z, and satisfaction of the atom saying q=(i,Vv) at q ∷ i ∷ s ∷ δ. The slot s is the container used to expose the components of the term code.
Inner : (i s : S) → Type (ℓ-suc ℓ) Inner i s = ∥ Σ[ q ∈ S ] (⟨ fst q ∈ Z ⟩ × ⟨ (q ∷ i ∷ s ∷ δ) ⊨ prAtL i0 i1 (sh 3 v) ⟩) ∥₁
Outer packages the whole variable branch read from sndEx: there merely exist a payload representative i and a container s such that Tv=pr N1v (fst i) and the inner bounded existential holds at i ∷ s ∷ δ. The equation identifies the term code with the tag-one pair; it does not identify i with the tag.
Outer : Type (ℓ-suc ℓ) Outer = ∥ Σ[ i ∈ S ] Σ[ s ∈ S ] ((Tv ≡ pr N1v (fst i)) × ⟨ (i ∷ s ∷ δ) ⊨ inner ⟩) ∥₁
From an inner witness q, pr-out gives fst q=pr (fst i) Vv; transporting the known membership q∈Z along this equation yields the required graph membership of (i,Vv). In parallel, q1 changes the outer equation from the actual tag slot N1v to #1. These are exactly the two fields of the variable branch of TmIsV.
viaQ : (i s : S) → Tv ≡ pr N1v (fst i) → Inner i s → TmIsV Tv Z Vv viaQ i s e = PT.map (λ { (q , (q∈ , hp)) → inr (fst i , ( e ∙ cong (λ a → pr a (fst i)) q1 , subst (λ u → ⟨ u ∈ Z ⟩) (pr-out i0 i1 (sh 3 v) (q ∷ i ∷ s ∷ δ) hp) q∈ )) })
viaI eliminates the merely existing outer decomposition into TmIsV. This elimination is allowed because TmIsV is itself propositionally truncated, so the construction transforms each local pair decomposition without choosing one decomposition for later use.
viaI : Outer → TmIsV Tv Z Vv viaI = PT.rec squash₁ (λ { (i , s , (e , hq)) → viaQ i s e hq })
The object formula tmIs is a disjunction of two code shapes. In the constant branch, pr-out reads Tv=pr(q0,Vv) and the equation q0=#0 converts it to the first branch of TmIsV. In the variable branch, sndEx-out produces Outer, which viaI converts to the graph-membership branch.
cases : ⟨ δ ⊨ prAtL t N0 v ⟩ ⊎ ⟨ δ ⊨ sndEx t N1 inner ⟩ → TmIsV Tv Z Vv cases (inl h) = ∣ inl (pr-out t N0 v δ h ∙ cong (λ a → pr a Vv) q0) ∣₁ cases (inr h) = viaI (sndEx-out t N1 inner δ h)
The public elimination tmIs-out performs that case analysis under the outer disjunction's propositional truncation. Its conclusion concerns one proposed value Vv; it does not show that two proposed values agree. If Z is an arbitrary multivalued relation, the same variable code may satisfy tmIs at more than one value.
tmIs-out : ⟨ δ ⊨ tmIs t z v N0 N1 ⟩ → TmIsV Tv Z Vv tmIs-out h = PT.rec squash₁ cases h
For the converse, build turns either concrete code shape back into satisfaction of tmIs. The constant equation is converted by pr-in. In the variable case, the proof must represent the payload index and the graph entry as elements of S, then rebuild the nested bounded existentials of sndEx.
private build : (Tv ≡ pr (# 0) Vv) ⊎ (Σ[ i ∈ V ℓ ] ((Tv ≡ pr (# 1) i) × ⟨ pr i Vv ∈ Z ⟩)) → ⟨ δ ⊨ tmIs t z v N0 N1 ⟩ build (inl e) = ∣ inl (pr-in t N0 v δ (e ∙ cong (λ a → pr a Vv) (sym q0))) ∣₁ build (inr (i , (e , hp))) = ∣ inr (fillSnd t δ (lookup N1 δ) iS e' inner hq N1 refl) ∣₁
iS is the constructible representative of the payload i, recovered as the second component of the pair equation Tv=(#1,i). The term qS is the constructible representative of the graph entry (i,Vv), obtained from its membership in Z. These are witnesses inside S, not new semantic indices or values.
where iS : S iS = sndS (lookup t δ) (# 1) i e qS : S qS = down (lookup z δ) (pr i Vv) hp
The equation e' rewrites the canonical tag equation into the actual tag-one slot required by sndEx. The auxiliary environment δ3 places the graph entry qS, the payload representative iS, and the container for the outer term-code pair before δ. The remaining goal hq is exactly the inner bounded existential at iS ∷ container ∷ δ.
e' : Tv ≡ pr N1v (fst iS) e' = e ∙ cong (λ a → pr a i) (sym q1) δ3 : S ^ (3 + j) δ3 = qS ∷ iS ∷ container (lookup t δ) (lookup N1 δ) iS e' .fst ∷ δ hq : ⟨ (iS ∷ container (lookup t δ) (lookup N1 δ) iS e' .fst ∷ δ) ⊨ inner ⟩
To prove hq, choose qS from the graph. Its membership is the given fact hp, and pr-in proves by reflexivity that its underlying set is the pair of iS and Vv. This supplies exactly the graph entry demanded by the variable branch.
hq = ∣ qS , (hp , pr-in i0 i1 (sh 3 v) δ3 refl) ∣₁
Finally, tmIs-in eliminates the propositional truncation in TmIsV into the proposition expressing satisfaction of tmIs, applying build to either branch. Together with tmIs-out, this gives both semantic directions while preserving the absence of any global choice or uniqueness claim.
tmIs-in : TmIsV Tv Z Vv → ⟨ δ ⊨ tmIs t z v N0 N1 ⟩ tmIs-in = PT.rec (snd (δ ⊨ tmIs t z v N0 N1)) build
Frame fixes the host-level slots for the table T, carrier w, code domain C, and environment tower E, together with the ten tag slots N and the surrounding assignment γ. The hypothesis Tags γ N identifies each tag slot with its numeral, allowing a clause selected by k : Fin 10 to be read as the relation relN (toℕ k).
module Frame {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where private Tv = fst (lookup T γ) Cv = fst (lookup C γ) Ev = fst (lookup E γ)
The frame is peeled by a sequence of bounded universals. At the innermost stage, inner9 k ranges over every table entry and uses sndAll to expose a value yc whenever that entry has first component c; the resulting twelve-slot environment is where relN (toℕ k) must hold. This is a universal condition on matching entries, not an existential search for one value.
module Cl = Clause T w C E N module R = Rel T w N inner9 : Fin 10 → Formula S (9 + m) inner9 k = ∀̇∈ (var (sh 9 T)) (sndAll i0 i5 (R.relN (toℕ k))) inner7 : Fin 10 → Formula S (7 + m)
The preceding stages expose the nested key. inner4 k ranges over every c∈C whose first component is the current arity ar, obtaining its payload p; inner7 k then requires p to have the tag stored at N k and exposes its residual data r. Each pair decomposition adds its components and a container at the head, so the shifts preserve access to the older frame slots.
inner7 k = sndAll i0 (sh 7 (N k)) (inner9 k) inner4 : Fin 10 → Formula S (4 + m) inner4 k = ∀̇∈ (var (sh 4 C)) (sndAll i0 i2 (inner7 k))
For one clause instance, At fixes a tower pair (ar,F), a formula key c=(ar,p), a tagged payload p=(N k,r), and a table pair (c,yc). The memberships q∈ and e∈ concern the projected pairs in E and T; the module does not itself prove that c∈C, decode r, or show that the table value is unique.
module At (ar F c p r yc : S) (q∈ : ⟨ pr (fst ar) (fst F) ∈ Ev ⟩) (ec : fst c ≡ pr (fst ar) (fst p)) (k : Fin 10) (ep : fst p ≡ pr (fst (lookup (N k) γ)) (fst r)) (e∈ : ⟨ pr (fst c) (fst yc) ∈ Tv ⟩) where qS eS : S
qS and eS lift the two projected pair memberships back to elements of the constructible carrier. Their underlying sets are definitionally pr (fst ar) (fst F) and pr (fst c) (fst yc), respectively. They serve only as representatives to which the bounded pair readers can be applied when the twelve-slot environment is assembled.
qS = down (lookup E γ) (pr (fst ar) (fst F)) q∈ eS = down (lookup T γ) (pr (fst c) (fst yc)) e∈
The frame begins with an actual tower member qS whose underlying pair is (ar,F). The four new slots record F, ar, a witness for the pair decomposition, and qS; the next three record the payload p, a witness that c=(ar,p), and the code c. Thus the successive environments retain both the mathematical data and the bounded witnesses by which the object-language clause obtained them.
δ4 : S ^ (4 + m) δ4 = F ∷ ar ∷ container qS ar F refl .fst ∷ qS ∷ γ δ7 : S ^ (7 + m) δ7 = p ∷ container c ar p ec .fst ∷ c ∷ δ4 δ9 : S ^ (9 + m)
The twelve-slot environment completes the nesting. At the front is the candidate value yc, followed by a container exposing the components of the table pair (c,yc) and the actual table member eS whose underlying set is that pair; the nine earlier objects follow. This is the environment at which the relation body is read.
δ9 = r ∷ container p (lookup (N k) γ) r ep .fst ∷ δ7 δ12 : S ^ (12 + m) δ12 = yc ∷ container eS c yc refl .fst ∷ eS ∷ δ9
The outward reading starts from satisfaction of clause k and fixes all data matching one instance of its frame: ar and F from a tower pair, a code c=(ar,p) in C, a tagged payload p=(#k,r), and a candidate value yc with (c,yc) in T. It then returns satisfaction of relN (toℕ k) at the corresponding twelve-slot environment. The table hypothesis here is membership of the pair (c,yc); the representative table member and its container are constructed locally.
clause-out : (k : Fin 10) → ⟨ γ ⊨ Cl.clause k ⟩ → (ar F c p r yc : S) (q∈ : ⟨ pr (fst ar) (fst F) ∈ Ev ⟩) → ⟨ fst c ∈ Cv ⟩ → (ec : fst c ≡ pr (fst ar) (fst p)) → (ep : fst p ≡ pr (# (toℕ k)) (fst r)) → (e∈ : ⟨ pr (fst c) (fst yc) ∈ Tv ⟩) → ⟨ At.δ12 ar F c p r yc q∈ ec k (ep ∙ cong (λ a → pr a (fst r)) (sym (tg k))) e∈ ⊨ R.relN (toℕ k) ⟩
With the matching data fixed, the module A gives one coherent realization of all twelve frame slots. The first elimination opens the tower pair, and the final useSnd opens the actual table member as (c,yc). Between them, the proof must still pass through the code and tag layers; naming h4 before those steps makes explicit that the conclusion follows by successively specializing the single outer clause, rather than by assuming the constructor relation separately.
clause-out k h ar F c p r yc q∈ c∈ ec ep e∈ = useSnd i0 (A.eS ∷ A.δ9) c yc refl (R.relN (toℕ k)) i5 refl (h9 A.eS e∈) where module A = At ar F c p r yc q∈ ec k (ep ∙ cong (λ a → pr a (fst r)) (sym (tg k))) e∈ h4 : ⟨ A.δ4 ⊨ inner4 k ⟩
The three intermediate judgments mark the three semantic layers of the common frame. At δ4, h4 has opened the tower entry (ar,F) and is ready to range over codes in C; at δ7, h7 has also decomposed c=(ar,p); at δ9, h9 has identified p as the tag-k payload r and is ready to inspect entries of T. The final elimination then decomposes the chosen table member as (c,yc) and reaches the constructor relation.
h4 = useBoth i0 (A.qS ∷ γ) ar F refl (inner4 k) (h A.qS q∈) h7 : ⟨ A.δ7 ⊨ inner7 k ⟩ h7 = useSnd i0 (c ∷ A.δ4) ar p ec (inner7 k) i2 refl (h4 c c∈) h9 : ⟨ A.δ9 ⊨ inner9 k ⟩ h9 = useSnd i0 A.δ7 (lookup (N k) γ) r (ep ∙ cong (λ a → pr a (fst r)) (sym (tg k))) (inner9 k) (sh 7 (N k)) refl h7
For the converse direction, suppose the constructor relation can be proved from every complete matching frame. Such a frame consists of a tower member q=(ar,F), a code c=(ar,p) in C, a tag decomposition p=(#k,r), and a table member e=(c,yc), together with the four pair witnesses s, s1, s2, and s3. Proving the relation in the displayed environment for all this data is exactly the premise needed to reconstruct clause k.
clause-in : (k : Fin 10) → ((q ar F s c p s1 r s2 e yc s3 : S) → ⟨ fst q ∈ Ev ⟩ → fst q ≡ pr (fst ar) (fst F) → ⟨ fst c ∈ Cv ⟩ → fst c ≡ pr (fst ar) (fst p) → fst p ≡ pr (# (toℕ k)) (fst r) → ⟨ fst e ∈ Tv ⟩ → fst e ≡ pr (fst c) (fst yc) → ⟨ (yc ∷ s3 ∷ e ∷ r ∷ s2 ∷ p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) ⊨ R.relN (toℕ k) ⟩)
The proof rebuilds the universally quantified frame in its logical order. It handles an arbitrary q in E together with every exposed decomposition q=(ar,F), then an arbitrary c in C together with every matching decomposition c=(ar,p). It next identifies the tag and payload of p, and finally handles an arbitrary e in T together with every decomposition e=(c,yc). Each bounded introduction places its new value at the head of the environment, while the accompanying s-variables retain the pair-decomposition witnesses required by the formulas.
→ ⟨ γ ⊨ Cl.clause k ⟩ clause-in k g q q∈ = bothAll-in i0 (inner4 k) (q ∷ γ) (λ ar F s s∈ ar∈ F∈ eq c c∈ → sndAll-in i0 i2 (inner7 k) (c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ p s1 s1∈ p∈ ec → sndAll-in i0 (sh 7 (N k)) (inner9 k) (p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ r s2 s2∈ r∈ ep e e∈ → sndAll-in i0 i5 (R.relN (toℕ k)) (e ∷ r ∷ s2 ∷ p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ yc s3 s3∈ yc∈ ee →
Before the host-level rule g is applied, the payload equation is composed with tg k, replacing the set stored in the tag slot by the canonical numeral #k. The rule therefore receives exactly the equation p=(#k,r) appearing in the outward reading. Thus clause-in and clause-out give the two directions between clause k and its relation at every matching frame.
g q ar F s c p s1 r s2 e yc s3 q∈ eq c∈ ec (ep ∙ cong (λ a → pr a (fst r)) (tg k)) e∈ ee))))
Totality is read outward as truncated existence: for each member of the code domain, the totality clause guarantees that some table entry with that first component exists, and the truncated decomposition of the table entry recovers the value yc.
total-out : ⟨ γ ⊨ Cl.total ⟩ → (c : S) → ⟨ fst c ∈ Cv ⟩ → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ ∥₁ total-out h c c∈ = PT.rec squash₁ (λ { (e , (e∈ , hs)) → PT.map (λ { (yc , s , (ee , _)) → yc , subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈ }) (sndEx-out i0 i1 ⊤̇ (e ∷ c ∷ γ) hs) })
For a fixed c∈C, applying the standing hypothesis h yields, under propositional truncation, a table member e together with its membership in T and a decomposition statement. The reader sndEx-out decomposes e as (c,yc), and transporting the membership of e along that equation proves (c,yc)∈T. Both decompositions remain hidden by the truncation, so the result supplies existence without selecting a canonical value.
(h c c∈)
Conversely, assume that every c in C has, propositionally truncated, a value yc with (c,yc) in T. The membership proof is turned by down into an element e : S of T whose underlying set is that pair; fillSnd supplies the bounded witnesses that decompose e back into c and yc. The remaining body is truth, so this data constructs the totality clause without choosing a value globally and without asserting uniqueness.
total-in : ((c : S) → ⟨ fst c ∈ Cv ⟩ → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ ∥₁) → ⟨ γ ⊨ Cl.total ⟩ total-in g c c∈ = PT.map (λ { (yc , m) → down (lookup T γ) (pr (fst c) (fst yc)) m , ( m , fillSnd i0 (down (lookup T γ) (pr (fst c) (fst yc)) m ∷ c ∷ γ) c yc refl ⊤̇ (λ b → b) i1 refl ) }) (g c c∈)
The on-domain condition starts with an arbitrary element e of T, rather than with a pair already chosen in advance. Its outward reading recovers, under propositional truncation, objects c and yc such that e=(c,yc) and c belongs to C. Thus every member of the table has a code from the stated domain as its first component, but the result says neither that the decomposition is selected canonically nor that a code has only one value.
onC-out : ⟨ γ ⊨ Cl.onC ⟩ → (e : S) → ⟨ fst e ∈ Tv ⟩ → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ Cv ⟩) ∥₁ onC-out h e e∈ = PT.map (λ { (c , yc , s , (ee , c∈)) → c , yc , (ee , c∈) }) (bothEx-out i0 (var i1 ∈̇ var (sh 4 C)) (e ∷ γ) (h e e∈))
The converse asks for precisely that truncated decomposition of every member of T and inserts it into the two bounded existentials of onC. Together the two readings identify onC with the claim that the first projection of every table member lies in C. Combined with totality this fixes the table's domain projection, but it still does not make the table single-valued.
onC-in : ((e : S) → ⟨ fst e ∈ Tv ⟩ → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ Cv ⟩) ∥₁) → ⟨ γ ⊨ Cl.onC ⟩ onC-in g e e∈ = PT.rec (snd ((e ∷ γ) ⊨ bothEx i0 (var i1 ∈̇ var (sh 4 C)))) (λ { (c , yc , (ee , c∈)) → fillBoth i0 (e ∷ γ) c yc ee (var i1 ∈̇ var (sh 4 C)) c∈ }) (g e e∈)
Reading the constructor relations
The constructor readers work over a frame δ with twelve slots added in front of the original m-environment. The original slots T and w, and the ten numeral slots N, therefore live beyond this prefix, while the frame itself places the candidate value yc at i0 and the constructor payload r at i3. Fixing these positions lets every relation reader use the same outer frame, regardless of the constructor being read.
module RelRead {m : ℕ} (T w : Fin m) (N : Fin 10 → Fin m) (δ : S ^ (12 + m)) where private module R = Rel T w N yc = lookup i0 δ r = lookup i3 δ
The remaining local names identify the environment-set slot F and the arity slot ar. They project the underlying table set Tv, the arity value A, and the constructor payload Rv once, so the relation readers can state their hypotheses directly in the cumulative hierarchy.
F = lookup i8 δ ar = lookup i9 δ Tv = fst (lookup (sh 12 T) δ) A = fst ar Rv = fst r
For any further local environment env, Ext env φ states the exact extension property for the outer table value yc. An element z belongs to yc exactly when it belongs to the arity-appropriate environment set F and the formula φ holds after z is placed in the new head slot of env. The old slots of env are consequently read one position later inside φ.
Ext : ∀ {k} (env : S ^ k) (φ : Formula S (1 + k)) → Type (ℓ-suc ℓ) Ext env φ = ExtFact (fst yc) (fst F) (λ z → ⟨ (z ∷ env) ⊨ φ ⟩)
For a binary connective, the payload r must decompose as the two child codes a and b. The keys c₁=(A,a) and c₂=(A,b) must have table values ya and yb. From these hypotheses, bin-out returns five auxiliary witnesses under propositional truncation: one container for r=(a,b), and for each child both an actual member of T and a container witnessing its decomposition. The mathematical conclusion is an Ext fact for the outer value yc, whose body tests membership in ya and yb using the connective op.
bin-out : (op : ∀ {j} → Formula S j → Formula S j → Formula S j) → ⟨ δ ⊨ R.binRel op ⟩ → (a b c₁ ya c₂ yb : S) → Rv ≡ pr (fst a) (fst b) → ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩ → fst c₁ ≡ pr A (fst a) → ⟨ pr (fst c₂) (fst yb) ∈ Tv ⟩ → fst c₂ ≡ pr A (fst b) → ∥ Σ[ s ∈ S ] Σ[ s₁ ∈ S ] Σ[ e₁ ∈ S ] Σ[ s₂ ∈ S ] Σ[ e₂ ∈ S ]
The five witnesses are packaged only because the object-language bounded quantifiers hide the pair decompositions. After the payload has been opened, the first subAt-out reads the value at the left child key and the second reads the value at the right child key. The innermost extB then yields the exact extension of yc; it does not assert that either child value was uniquely selected by the table.
Ext (yb ∷ c₂ ∷ s₂ ∷ e₂ ∷ ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b ∷ a ∷ s ∷ δ) (R.binBody op) ∥₁ bin-out op h a b c₁ ya c₂ yb er m₁ e₁ m₂ e₂ = ∣ container r a b er .fst , container e₁S c₁ ya refl .fst , e₁S , container e₂S c₂ yb refl .fst , e₂S , subAt-out (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op)) δ19 (subAt-out (sh 15 T) i12 i1 (subAt (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op))) δ15
The first step is to open the payload equation r=(a,b) inside the twelve-slot frame. This contributes the pair container and produces δ15, the old frame prefixed by b, a, and that container. The two nested subvalue readings then proceed from left to right, so their hidden table witnesses remain inside the outer propositional truncation.
(useBoth i3 δ a b er (subAt (sh 15 T) i12 i1 (subAt (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op)))) h) c₁ ya m₁ e₁) c₂ yb m₂ e₂ ∣₁ where δ15 : S ^ (15 + m)
The membership proof for (c₁,ya) does not itself supply an element of the structure S; down realizes it as e₁S : S, an actual member of T with that underlying pair. The environment δ19 then prefixes ya, c₁, their pair container, and e₁S to δ15. These four slots are exactly the frame expected by the first subAt reading.
δ15 = b ∷ a ∷ container r a b er .fst ∷ δ e₁S : S e₁S = down (lookup (sh 15 T) δ15) (pr (fst c₁) (fst ya)) m₁ δ19 : S ^ (19 + m) δ19 = ya ∷ c₁ ∷ container e₁S c₁ ya refl .fst ∷ e₁S ∷ δ15
The same construction realizes the second membership proof as e₂S : S, an actual table member with underlying pair (c₂,yb). The second subAt-out supplies its accompanying pair container when it extends δ19. Hence both child values are available to binBody, while neither membership proof has been turned into a global choice from the table.
e₂S : S e₂S = down (lookup (sh 19 T) δ19) (pr (fst c₂) (fst yb)) m₂
The converse begins with a rule for every possible decomposition of the binary frame. Besides the child codes and values, the rule receives the payload container, the two actual table members, their pair containers, and the equations proving that their keys are (A,a) and (A,b). Its conclusion must be the Ext fact for the outer value yc in the environment obtained by adding these eleven objects to the original twelve-slot frame.
bin-in : (op : ∀ {j} → Formula S j → Formula S j → Formula S j) → ((a b s c₁ ya s₁ e₁ c₂ yb s₂ e₂ : S) → Rv ≡ pr (fst a) (fst b) → ⟨ fst e₁ ∈ Tv ⟩ → fst e₁ ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr A (fst a) → ⟨ fst e₂ ∈ Tv ⟩ → fst e₂ ≡ pr (fst c₂) (fst yb) → fst c₂ ≡ pr A (fst b) → Ext (yb ∷ c₂ ∷ s₂ ∷ e₂ ∷ ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b ∷ a ∷ s ∷ δ) (R.binBody op))
The proof introduces the two argument quantifiers and the relation container, then opens the two nested subAt clauses for the left and right table entries, each introducing its code, value, and pair equation.
→ ⟨ δ ⊨ R.binRel op ⟩ bin-in op g = bothAll-in i3 (subAt (sh 15 T) i12 i1 (subAt (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op)))) δ (λ a b s s∈ a∈ b∈ er → subAt-in (sh 15 T) i12 i1 (subAt (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op))) (b ∷ a ∷ s ∷ δ) (λ c₁ ya s₁ e₁ e₁∈ ee₁ e₁' →
At the innermost level, the host-side rule receives all eleven objects and produces the extension fact, which is transported into the innermost subAt clause. The nesting of introductions mirrors the nesting of the quantified clause.
subAt-in (sh 19 T) i16 i4 (extB i11 i19 (R.binBody op)) (ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b ∷ a ∷ s ∷ δ) (λ c₂ yb s₂ e₂ e₂∈ ee₂ e₂' → g a b s c₁ ya s₁ e₁ c₂ yb s₂ e₂ er e₁∈ ee₁ e₁' e₂∈ ee₂ e₂')))
For an unbounded quantifier, the payload r is the child formula code. A matching child key has the form c₁=(ar',r), where ar' is the successor of the outer arity A, and (c₁,ya) belongs to the table. From these data, qu-out returns three hidden witnesses and an Ext fact for the outer value yc. In that extension fact, ya supplies the child satisfaction set used by the quantified body; ya itself is not the set being characterized.
qu-out : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j) → ⟨ δ ⊨ R.quRel q ⟩ → (c₁ ya ar' : S) → ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩ → fst c₁ ≡ pr (fst ar') Rv → fst ar' ≡ sucV A → ∥ Σ[ s ∈ S ] Σ[ s' ∈ S ] Σ[ e' ∈ S ] Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) (R.quBody q) ∥₁ qu-out q h c₁ ya ar' mem e es = ∣ container e'S c₁ ya refl .fst , container c₁ ar' r e .fst , e'S
The three witnesses have distinct roles. e'S is an actual member of T realizing the pair (c₁,ya); one container witnesses that pair, and the other witnesses c₁=(ar',r). The general successor-arity reader already knows how to combine these witnesses with ar'=suc A and then expose the innermost extension fact.
, subSucAt-out (sh 12 T) i9 i3 (extB i6 i14 (R.quBody q)) δ h c₁ ya ar' mem e es ∣₁ where e'S : S e'S = down (lookup (sh 12 T) δ) (pr (fst c₁) (fst ya)) mem
Conversely, suppose every actual table member e'=(c₁,ya) whose key satisfies c₁=(ar',r) and ar'=suc A yields the required Ext fact, for every choice of the two pair containers. This universal premise is strong enough to rebuild the bounded structure of quRel. It concerns all matching entries and does not presume that the child value ya is unique.
qu-in : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j) → ((c₁ ya ar' s s' e' : S) → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr (fst ar') Rv → fst ar' ≡ sucV A → Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) (R.quBody q)) → ⟨ δ ⊨ R.quRel q ⟩
No additional payload decomposition is needed for an unbounded quantifier: its payload r already is the child formula code. Consequently the general converse for a successor-arity subvalue has exactly the premise and conclusion required by quRel. Applying it once reconstructs the whole relation while preserving the universal reading over all matching table entries.
qu-in q g = subSucAt-in (sh 12 T) i9 i3 (extB i6 i14 (R.quBody q)) δ g
The bounded-quantifier payload has two syntactic components: the bound term code t and the child formula code a, so r=(t,a). The child key is c₁=(ar',a) at successor arity, and its table value is ya. The four truncated witnesses record the payload pair, the child table member, and the two relevant pair decompositions. The resulting Ext fact characterizes the outer value yc; inside its body, the term code is evaluated and its value bounds the quantification.
bq-out : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j) → (c : ∀ {j} → Formula S j → Formula S j → Formula S j) → ⟨ δ ⊨ R.bqRel q c ⟩ → (t a c₁ ya ar' : S) → Rv ≡ pr (fst t) (fst a) → ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A → ∥ Σ[ s ∈ S ] Σ[ s₁ ∈ S ] Σ[ s' ∈ S ] Σ[ e' ∈ S ]
The proof packages exactly four witnesses: a container for r=(t,a), a container and an actual table member for (c₁,ya), and a container for c₁=(ar',a). After useBoth opens the payload, subSucAt-out reads the child value at successor arity. The environment supplied to Ext adds nine local slots to the twelve-slot frame, and Ext itself places the candidate encoded environment z in one further head slot, matching the arity of bqBody.
Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s₁ ∷ e' ∷ a ∷ t ∷ s ∷ δ) (R.bqBody q c) ∥₁ bq-out q c h t a c₁ ya ar' er mem e es = ∣ container r t a er .fst , container e'S c₁ ya refl .fst , container c₁ ar' a e .fst , e'S , subSucAt-out (sh 15 T) i12 i0 (extB i9 i17 (R.bqBody q c)) δ15 (useBoth i3 δ t a er (subSucAt (sh 15 T) i12 i0 (extB i9 i17 (R.bqBody q c))) h)
Opening the payload extends the original frame by three slots: the child formula code a, the bound term code t, and a container witnessing r=(t,a). This is the environment δ15. The notation records a fifteen-slot prefix over the original m-environment because δ already contained the twelve common frame slots.
c₁ ya ar' mem e es ∣₁ where δ15 : S ^ (15 + m) δ15 = a ∷ t ∷ container r t a er .fst ∷ δ e'S : S
The hypothesis mem is membership of the underlying pair (c₁,ya) in the table set. Applying down at the shifted table slot realizes that proof as e'S : S, an actual table element with the required underlying set. This realization is local to the proof; it does not choose a child value from totality.
e'S = down (lookup (sh 15 T) δ15) (pr (fst c₁) (fst ya)) mem
The converse premise ranges over nine objects because it must accept every realization of the payload and child-table decompositions. Here s₁ is a pair container for the table member, while s' is a container for the successor-arity child key; neither is the semantic witness bound by the quantified formula. Given the membership and pair equations, the premise supplies the Ext fact for yc and thereby determines the bounded relation locally.
bq-in : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j) → (c : ∀ {j} → Formula S j → Formula S j → Formula S j) → ((t a s c₁ ya ar' s₁ s' e' : S) → Rv ≡ pr (fst t) (fst a) → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
To rebuild bqRel, bothAll-in first handles every decomposition r=(t,a) of the constructor payload. At that extended environment, subSucAt-in handles every table entry for the child key (suc A,a). The supplied rule then proves the exact extension condition for yc; the semantic bound value itself is quantified later inside bqBody, where tmIs relates it to the term code t.
→ Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s₁ ∷ e' ∷ a ∷ t ∷ s ∷ δ) (R.bqBody q c)) → ⟨ δ ⊨ R.bqRel q c ⟩ bq-in q c g = bothAll-in i3 (subSucAt (sh 15 T) i12 i0 (extB i9 i17 (R.bqBody q c))) δ (λ t a s s∈ t∈ a∈ er → subSucAt-in (sh 15 T) i12 i0 (extB i9 i17 (R.bqBody q c)) (a ∷ t ∷ s ∷ δ)
At the innermost stage all structural obligations have become explicit: the payload is (t,a), the child table member is (c₁,ya), its key is (ar',a), and ar' is the successor of A. These are exactly the hypotheses of the assumed rule g, so its extension fact closes the successor-arity subvalue clause. No assertion about the uniqueness of ya is used in this reconstruction.
(λ c₁ ya ar' s₁ s' e' e'∈ ee e es → g t a s c₁ ya ar' s₁ s' e' er e'∈ ee e es))
For an atomic formula, t and u are the two term codes stored in the payload, not their semantic values. Opening r=(t,u) contributes one pair container and leaves an Ext fact for the outer table value yc. The formula atomBody evaluated there will separately quantify candidate values of the two terms, verify them with tmIs, and apply the chosen atomic relation.
atom-out : (rel : Formula S (18 + m)) → ⟨ δ ⊨ R.atomRel rel ⟩ → (t u : S) → Rv ≡ pr (fst t) (fst u) → ∥ Σ[ s ∈ S ] Ext (u ∷ t ∷ s ∷ δ) (R.atomBody rel) ∥₁ atom-out rel h t u er = ∣ container r t u er .fst , useBoth i3 δ t u er (extB i3 i11 (R.atomBody rel)) h ∣₁
Conversely, assume the extension condition can be proved for every decomposition of the payload into term codes t and u and every accompanying pair container. The bounded-universal introduction reconstructs that payload decomposition and hence the atomic relation. The later existential choices of actual term values remain inside atomBody; they are not parameters of atom-in.
atom-in : (rel : Formula S (18 + m)) → ((t u s : S) → Rv ≡ pr (fst t) (fst u) → Ext (u ∷ t ∷ s ∷ δ) (R.atomBody rel)) → ⟨ δ ⊨ R.atomRel rel ⟩ atom-in rel g = bothAll-in i3 (extB i3 i11 (R.atomBody rel)) δ (λ t u s s∈ t∈ u∈ er → g t u s er)
Bridging clauses to semantic satisfaction
The relation readings are complete: each constructor's clause has been converted into its extension fact, and each extension fact into its clause. The chapter now turns to the bridge that connects these object-language relations to the meta-level satisfaction semantics.
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapTm ) open import L.Coding.Satisfaction {ℓ} lem using ( Sat; Sat-mem; cond ) open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst ) import L.Coding.SatisfactionBridge {ℓ} lem as Semantic open import Cubical.Data.Nat using ( znots; snotz )
The bridge module is parameterized by a set W of the hierarchy whose members form the constant alphabet of the internal language. The definability and semantic modules are opened at W, so that formulas over the alphabet Ab can be interpreted in the small model carried by W.
module Bridge (W : S) where open Alphabet W private module DB = Semantic.DB W module Sem = Semantic.SemB W
The small model's satisfaction judgment is renamed to ⊨ᴮ and its term valuation to ⟦_⟧ᴮ, so the bridge can distinguish them from the ambient-hierarchy satisfaction ⊨ used earlier in the chapter.
open Sem.At DB.SM id using () renaming ( _⊨_ to _⊨ᴮ_ ; ⟦_⟧ to ⟦_⟧ᴮ )
The meta-level meaning of a formula ψ at a meta-level environment δ is the satisfaction of the constant-relabeled formula in the small model carried by W. This is the target semantics that the bridges will relate to the object-language table entries.
Meaning : ∀ {n} → Formula Ab n → DB.SM ^ n → hProp (ℓ-suc ℓ) Meaning ψ δ = δ ⊨ᴮ mapFo DB.ι ψ
The underlying set Wv is the carrier over which the small-model quantifiers range. Keeping it separate from the presentation W : S matters in the later bridges: object-language membership uses the set Wv, while constructibility evidence remains in the second component of W. Thus the bridges quantify over members of the fixed model, not over every constructible set.
private Wv = fst W
The map toS relabels every constant of a formula over the alphabet Ab into the corresponding constant of the structure S, producing a formula over S that can be judged by the ambient satisfaction.
toS : ∀ {n} → Formula Ab n → Formula S n toS = mapFo (asConst W)
The constructible satisfaction set SatW ψ collects the coded environments that satisfy the relabeled formula. It is an element of L, being the output of the internal recursion that defines satisfaction.
SatW : ∀ {n} → Formula Ab n → S SatW ψ = Sat W (toS ψ)
The outward reading of membership in SatW ψ follows from the membership specification of the internal satisfaction: a member of SatW ψ is a coded environment that lies in the environment set at the correct arity and satisfies the relabeled formula's condition.
Sat-out : ∀ {n} (ψ : Formula Ab n) (z : S) → ⟨ fst z ∈ fst (SatW ψ) ⟩ → ⟨ fst z ∈ fst (envSet W n) ⟩ × ⟨ (z ∷ []) ⊨ cond W (toS ψ) ⟩ Sat-out ψ z h = subst ⟨_⟩ (Sat-mem W (toS ψ) z) h
The inward direction starts from membership in the correct environment set together with the recursive condition, transports that pair backward along Sat-mem, and obtains membership in SatW ψ. Thus Sat-out and Sat-in are exactly the two transports supplied by the membership specification; they require no additional semantic hypothesis.
Sat-in : ∀ {n} (ψ : Formula Ab n) (z : S) → ⟨ fst z ∈ fst (envSet W n) ⟩ → ⟨ (z ∷ []) ⊨ cond W (toS ψ) ⟩ → ⟨ fst z ∈ fst (SatW ψ) ⟩ Sat-in ψ z hz hc = subst ⟨_⟩ (sym (Sat-mem W (toS ψ) z)) (hz , hc)
The lemma extension-path turns a pointwise path of truth values into an exact extension theorem for SatW ψ. For each encoded environment z, its premise identifies the recursive condition cond W (toS ψ) with the target proposition P z. Using the two directions of Sat-mem, the conclusion says that the members of SatW ψ are exactly the members of envSet W n satisfying P; it neither decodes z nor chooses a representative environment vector.
private extension-path : ∀ {n} (ψ : Formula Ab n) (P : S → hProp (ℓ-suc ℓ)) → ((z : S) → ((z ∷ []) ⊨ cond W (toS ψ)) ≡ P z) → ExtFact (fst (SatW ψ)) (fst (envSet W n)) (λ z → ⟨ P z ⟩) extension-path ψ P e =
The outward direction reads the two components of membership in SatW ψ through Sat-out and transports the condition along the pointwise equality. The inward direction transports the property back and applies Sat-in. Both directions use only the pointwise equality, not any choice of representatives.
(λ z hz → Sat-out ψ z hz .fst , subst ⟨_⟩ (e z) (Sat-out ψ z hz .snd)) , (λ z hz hp → Sat-in ψ z hz (subst ⟨_⟩ (sym (e z)) hp))
For falsity, the target property has no inhabitants for any z. If z belonged to SatW ⊥̇, Sat-out would expose the impossible satisfaction of falsity; conversely, an assumed proof of that impossible property eliminates the candidate immediately. The remaining component merely records that every hypothetical member would have the correct arity, so botBridge gives the empty extension inside envSet W n.
botBridge : (n : ℕ) {k : ℕ} (env : S ^ k) → ExtFact (fst (SatW (⊥̇ {n = n}))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ ⊥̇ ⟩) botBridge n env = (λ z hz → Sat-out ⊥̇ z hz .fst , Sat-out ⊥̇ z hz .snd) , (λ z hz b → Empty.rec* b)
Assume slots ya and yb of env contain the underlying satisfaction sets of a and b. The conjunction bridge then characterizes SatW (a ∧̇ b) as the encoded environments z belonging to both child sets. Since z is prepended before the body is evaluated, the old slots are addressed as suc ya and suc yb, while i0 names z; this shift is exactly the host Fin boundary recorded in the displayed formula.
andBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : S ^ k) (ya yb : Fin k) → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b) → ExtFact (fst (SatW (a ∧̇ b))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∧̇ (var i0 ∈̇ var (suc yb)) ⟩) andBridge a b env ya yb qa qb = extension-path (a ∧̇ b)
For conjunction, the pointwise path compares two descriptions of the same candidate environment z. The recursive condition says that z belongs to both SatW a and SatW b; transporting those two memberships along qa and qb gives exactly the two object-language membership atoms in the clause body. No child environment is decoded at this step.
(λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∧̇ (var i0 ∈̇ var (suc yb))) (λ z i → (fst z ∈ sym qa i) ⊓ (fst z ∈ sym qb i))
The disjunction bridge gives an exact extension description. An environment belongs to SatW (a ∨̇ b) exactly when it lies in envSet W n and, after being placed at the head of the clause environment, satisfies the object-language disjunction saying that it belongs to the value of a or to the value of b.
orBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : S ^ k) (ya yb : Fin k) → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b) → ExtFact (fst (SatW (a ∨̇ b))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∨̇ (var i0 ∈̇ var (suc yb)) ⟩) orBridge a b env ya yb qa qb = extension-path (a ∨̇ b)
The pointwise comparison for disjunction transports membership of the same z along the two slot equations. Its two alternatives are membership in SatW a and membership in SatW b; the object-language disjunction records precisely that alternative, without producing an additional environment witness.
(λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∨̇ (var i0 ∈̇ var (suc yb))) (λ z i → (fst z ∈ sym qa i) ⊔ (fst z ∈ sym qb i))
The implication bridge likewise characterizes SatW (a ⇒̇ b) inside the environment set. At a candidate environment z, its clause body says that membership of z in the value of the antecedent entails membership of that same z in the value of the consequent.
impBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : S ^ k) (ya yb : Fin k) → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b) → ExtFact (fst (SatW (a ⇒̇ b))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ⇒̇ (var i0 ∈̇ var (suc yb)) ⟩) impBridge a b env ya yb qa qb = extension-path (a ⇒̇ b)
The required path is pointwise: qa and qb rename the antecedent and consequent value slots as SatW a and SatW b. Transporting along those equations turns the object-language implication into the recursive condition for implication, with no change of environment.
(λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ⇒̇ (var i0 ∈̇ var (suc yb))) (λ z i → (fst z ∈ sym qa i) ⇒ (fst z ∈ sym qb i))
Both unbounded quantifier bodies range first over the carrier named by wi. The existential body asks for some carrier member x, while the universal body treats every such x; in either case an inner bounded existential chooses an entry of the child value and requires it to be the graph obtained by consing x onto the old environment.
quEx quAll : ∀ {k} → Fin k → Fin k → Formula S (1 + k) quEx wi yai = ∃̇∈ (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2)) quAll wi yai = ∀̇∈ (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2))
The lemma direct-extension isolates the argument shared by the quantifier and atom bridges. Once z is identified with the graph of a vector δ, it asks for maps in both directions between Meaning ψ δ and the proposed clause property P z; from them it proves that SatW ψ is exactly the part of envSet W n satisfying P. Recovery of δ remains truncated throughout.
private direct-extension : ∀ {n} (ψ : Formula Ab n) (P : S → hProp (ℓ-suc ℓ)) → ((δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ → ⟨ Meaning ψ δ ⟩ → ⟨ P z ⟩) → ((δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ → ⟨ P z ⟩ → ⟨ Meaning ψ δ ⟩) → ExtFact (fst (SatW ψ)) (fst (envSet W n)) (λ z → ⟨ P z ⟩)
For the outward half, Sat-out first supplies membership of z in the environment set. The truncated recovery theorem then gives a vector δ and an equation identifying z with its graph; inside the proposition P z, Sat-small-spec changes the original membership in SatW ψ into Meaning ψ δ, and the forward hypothesis finishes the argument.
direct-extension {n} ψ P f b = out , inn where out : (z : S) → ⟨ fst z ∈ fst (SatW ψ) ⟩ → ⟨ fst z ∈ fst (envSet W n) ⟩ × ⟨ P z ⟩ out z hz = Sat-out ψ z hz .fst , PT.rec (snd (P z)) (λ { (δ , q) → f δ z q (subst ⟨_⟩ (Semantic.Sat-small-spec W ψ δ z q) hz) })
For the inward half, membership in the environment set again yields only a truncated pair δ , q. The backward hypothesis sends P z to Meaning ψ δ, and the inverse direction of Sat-small-spec returns membership in SatW ψ. This elimination is valid because the membership goal is a proposition, so no global choice of a decoding vector is made.
(Semantic.envSet-vectors W z (Sat-out ψ z hz .fst)) inn : (z : S) → ⟨ fst z ∈ fst (envSet W n) ⟩ → ⟨ P z ⟩ → ⟨ fst z ∈ fst (SatW ψ) ⟩ inn z hz hp = PT.rec (snd (fst z ∈ fst (SatW ψ))) (λ { (δ , q) → subst ⟨_⟩ (sym (Semantic.Sat-small-spec W ψ δ z q)) (b δ z q hp) }) (Semantic.envSet-vectors W z hz)
The lemma child aligns the encoded and semantic views of one bound variable. If the old coded environment is the graph of δ and the named child value is SatW a, then saying that some member of that child value is the graph obtained by consing x onto the old environment is propositionally equal to Meaning a (x ∷ δ).
child : ∀ {n k} (a : Formula Ab (suc n)) (δ : DB.SM ^ n) (x : DB.SM)
(γ : S ^ k) (zi yai : Fin k) → fst (lookup zi γ) ≡ Semantic.graph W δ
→ fst (lookup yai γ) ≡ fst (SatW a)
→ ((Semantic.intoL W x ∷ γ) ⊨ ∃̇∈ (var (suc yai)) (consAtL i0 i1 (sh 2 zi)))
≡ Meaning a (x ∷ δ)
The proof is a pair of implications joined by ⇔toPath. The outward direction consumes the truncated witness of the bounded existential: an entry of the child value together with evidence from consAtL that this entry is the graph obtained by consing x onto the old environment.
child a δ x γ zi yai qz qa = ⇔toPath out inn where out : ⟨ (Semantic.intoL W x ∷ γ) ⊨ ∃̇∈ (var (suc yai)) (consAtL i0 i1 (sh 2 zi)) ⟩ → ⟨ Meaning a (x ∷ δ) ⟩ out = PT.rec (snd (Meaning a (x ∷ δ))) (λ { (e , he , hc) →
In the outward direction, the bounded existential is eliminated into the proposition Meaning a (x ∷ δ). The cons clause and the equation for the old graph identify its witness e with the graph of x ∷ δ; after qa turns e's membership into membership in SatW a, Sat-small-spec yields the desired semantic satisfaction.
subst ⟨_⟩ (Semantic.Sat-small-spec W a (x ∷ δ) e (Semantic.consAtL-out W δ x (e ∷ Semantic.intoL W x ∷ γ) i0 i1 (sh 2 zi) qz refl hc)) (subst (λ X → ⟨ fst e ∈ X ⟩) qa he) }) inn : ⟨ Meaning a (x ∷ δ) ⟩ → ⟨ (Semantic.intoL W x ∷ γ) ⊨ ∃̇∈ (var (suc yai)) (consAtL i0 i1 (sh 2 zi)) ⟩
The inward direction builds the canonical extension environment envFor W (x ∷ δ). Reading the small-spec path backward turns the semantic satisfaction into membership of this environment in SatW a; consAtL-in then proves that the same environment has the required graph-extension relation to the old one.
inn h = ∣ Semantic.envFor W (x ∷ δ) , subst (λ X → ⟨ fst (Semantic.envFor W (x ∷ δ)) ∈ X ⟩) (sym qa) (subst ⟨_⟩ (sym (Semantic.Sat-small-spec W a (x ∷ δ) (Semantic.envFor W (x ∷ δ)) (Semantic.envFor-graph W (x ∷ δ)))) h) , Semantic.consAtL-in W δ x (Semantic.envFor W (x ∷ δ) ∷ Semantic.intoL W x ∷ γ)
The remaining arguments to consAtL-in supply the old graph equation qz, the reflexive identification of the new head x, and envFor-graph for the extended vector. These data close the inward witness and complete the equivalence.
i0 i1 (sh 2 zi) qz refl (Semantic.envFor-graph W (x ∷ δ)) ∣₁
The existential bridge is the first quantifier result: membership in the internal value of ∃̇ a over the environment set is the same as satisfying the bounded-existential shape quEx over the carrier, with the two slot equations naming the carrier and the child value.
exBridge : ∀ {n} (a : Formula Ab (suc n)) {k : ℕ} (γ : S ^ k) (wi yai : Fin k) → fst (lookup wi γ) ≡ Wv → fst (lookup yai γ) ≡ fst (SatW a) → ExtFact (fst (SatW (∃̇ a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ γ) ⊨ quEx wi yai ⟩) exBridge a γ wi yai qw qa = direct-extension (∃̇ a) (λ z → (z ∷ γ) ⊨ quEx wi yai) (λ δ z qz → PT.map (λ { (x , h) → Semantic.intoL W x
For the existential bridge, direct-extension leaves only the two translations supplied by child. From semantic satisfaction, a truncated model element x is embedded into L and becomes the outer bounded witness; conversely, an object-language witness in the named carrier is turned into an element of the restricted model and then read through child. Both transformations stay under propositional truncation.
, subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd x) , subst ⟨_⟩ (sym (child a δ x (z ∷ γ) i0 (suc yai) qz qa)) h })) (λ δ z qz → PT.map (λ { (x , hx , h) → (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx) , subst ⟨_⟩ (child a δ (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx) (z ∷ γ) i0 (suc yai) qz qa) h }))
The universal bridge states the same extensional fact for ∀̇ a: the internal value contains an environment exactly when every carrier member, consed onto the environment, satisfies the child formula.
allBridge : ∀ {n} (a : Formula Ab (suc n)) {k : ℕ} (γ : S ^ k) (wi yai : Fin k) → fst (lookup wi γ) ≡ Wv → fst (lookup yai γ) ≡ fst (SatW a) → ExtFact (fst (SatW (∀̇ a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ γ) ⊨ quAll wi yai ⟩) allBridge a γ wi yai qw qa = direct-extension (∀̇ a) (λ z → (z ∷ γ) ⊨ quAll wi yai) (λ δ z qz h x hx → subst ⟨_⟩
In the forward map required by direct-extension, an arbitrary object-level member of the named carrier is converted to a restricted-model element, the semantic universal hypothesis is applied to it, and child is read from semantic satisfaction back to the encoded extension clause. In the reverse map, a restricted-model element is embedded into the carrier, the encoded universal is applied, and child is read outward to recover semantic satisfaction.
(sym (child a δ (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx) (z ∷ γ) i0 (suc yai) qz qa)) (h (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx))) (λ δ z qz h x → subst ⟨_⟩ (child a δ x (z ∷ γ) i0 (suc yai) qz qa) (h (Semantic.intoL W x) (subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd x))))
The bounded quantifiers are stated in the object language with three nested bounded layers: the value of the bounding term, a member of the carrier inside it, and the extension entry, in the same order for both quantifiers.
bqAll bqEx : ∀ {k} → Fin k → Fin k → Fin k → Fin k → Fin k → Formula S (1 + k) bqAll wi ti yai N0i N1i = ∀̇∈ (var (suc wi)) (tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) ⇒̇ ∀̇∈ (var (suc (suc wi))) ((var i0 ∈̇ var i1) ⇒̇ ∃̇∈ (var (suc (suc (suc yai)))) (consAtL i0 i1 i3))) bqEx wi ti yai N0i N1i =
The existential form conjoins the three layers; the universal form nests them as implications. The bounding term's value is read by its own term clause, and the innermost clause uses the same graph-extension equation as in the unbounded case.
∃̇∈ (var (suc wi)) (tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) ∧̇ ∃̇∈ (var (suc (suc wi))) ((var i0 ∈̇ var i1) ∧̇ ∃̇∈ (var (suc (suc (suc yai)))) (consAtL i0 i1 i3)))
The semantic value of a term is obtained by mapping each constant from the alphabet of members of W into the restricted model and then evaluating the resulting term at δ. Constants are interpreted by the embedding DB.ι, while variables are read directly from the corresponding positions of δ; set-coded numerals belong to the later representation of variable indices, not to this evaluation function.
private value : ∀ {n} → Term Ab n → DB.SM ^ n → DB.SM value t δ = ⟦ mapTm DB.ι t ⟧ᴮ δ
For a constant term, term-out eliminates the truncated TmIsV evidence into an equality of sets. In the constant branch, injectivity of the pair code compares the second components and identifies the proposed value with the constant; the variable-shaped branch would equate the distinct tags # 0 and # 1 and is therefore impossible.
term-out : ∀ {n} (t : Term Ab n) (δ : DB.SM ^ n) (z v : S) → fst z ≡ Semantic.graph W δ → TmIsV (ct t) (fst z) (fst v) → fst v ≡ fst (value t δ) term-out (con q) δ z v qz = PT.rec (setIsSet _ _) (λ { (inl e) → sym (pr-inj e .snd)
For a variable term, the constant-shaped branch is ruled out by the same tag distinction. In the variable-shaped branch, pair injectivity identifies the stored index with the numeral of i; the equation qz moves its membership into the canonical graph, and lookup-spec then says that the proposed value is exactly the ith entry of δ. The truncation is eliminated only into this propositional equality.
; (inr (i , e , _)) → Empty.rec (znots (#-inj′ {0} {1} (pr-inj e .fst))) }) term-out (var i) δ z v qz = PT.rec (setIsSet _ _) (λ { (inl e) → Empty.rec (snotz (#-inj′ {1} {0} (pr-inj e .fst))) ; (inr (j , e , hp)) → subst ⟨_⟩ (lookup-spec (Semantic.values W δ) i (fst v)) (subst2 (λ a E → ⟨ pr a (fst v) ∈ E ⟩) (sym (pr-inj e .snd)) qz hp) })
The converse lemma reconstructs TmIsV from the actual semantic value. For a constant, the supplied equality is reversed and transported through the pair constructor with tag # 0, producing the constant-shaped alternative under propositional truncation.
term-in : ∀ {n} (t : Term Ab n) (δ : DB.SM ^ n) (z v : S)
→ fst z ≡ Semantic.graph W δ → fst v ≡ fst (value t δ)
→ TmIsV (ct t) (fst z) (fst v)
term-in (con q) δ z v qz e = ∣ inl (cong (pr (# 0)) (sym e)) ∣₁
term-in (var i) δ z v qz e = ∣ inr (# (toℕ i) , refl
For a variable, the witness uses the numeral # (toℕ i) as its stored index. The supplied equality identifies the proposed value with the ith semantic entry; lookup-spec turns that equality into membership of the corresponding pair in the canonical graph, and transport backward along qz places the pair in the given coded environment.
, subst (λ E → ⟨ pr (# (toℕ i)) (fst v) ∈ E ⟩) (sym qz) (subst ⟨_⟩ (sym (lookup-spec (Semantic.values W δ) i (fst v))) e)) ∣₁
The bounded-quantifier module fixes the bounding term, the subformula, five slots, and five equations: the carrier, the term's coding, the subformula's value, and the two numeral slots, all read at a shared context.
module BqBridge {n : ℕ} (t : Term Ab n) (a : Formula Ab (suc n)) {k : ℕ} (Γ : S ^ k) (wi ti yai N0i N1i : Fin k) (qw : fst (lookup wi Γ) ≡ Wv) (qt : fst (lookup ti Γ) ≡ ct t) (qa : fst (lookup yai Γ) ≡ fst (SatW a)) (q0 : fst (lookup N0i Γ) ≡ # 0) (q1 : fst (lookup N1i Γ) ≡ # 1) where
The remaining proof must connect the object-language term clause used by the bounded quantifier with the semantic term value just established. The local lemmas keep that connection at the fixed slots and equations of BqBridge, so every later quantifier argument uses the same carrier, term code, child value, and numeral tags.
private
If the object-language term clause holds at v ∷ z ∷ Γ, tmIs-out first reads it as TmIsV for the code occupying the term slot. Transport along qt then replaces that slot value by the actual code ct t, yielding the representation-level statement needed by term-out.
tmOut : (z v : S) → ⟨ (v ∷ z ∷ Γ) ⊨ tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) ⟩ → TmIsV (ct t) (fst z) (fst v) tmOut z v h = subst (λ u → TmIsV u (fst z) (fst v)) qt (tmIs-out (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) (v ∷ z ∷ Γ) q0 q1 h)
Conversely, a TmIsV statement for ct t is transported backward along qt and passed to tmIs-in. The result is precisely the object-language term clause at v ∷ z ∷ Γ, so the bridge can move between the coded clause and semantic term evaluation in either direction.
tmIn' : (z v : S) → TmIsV (ct t) (fst z) (fst v) → ⟨ (v ∷ z ∷ Γ) ⊨ tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) ⟩ tmIn' z v h = tmIs-in (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) (v ∷ z ∷ Γ) q0 q1 (subst (λ u → TmIsV u (fst z) (fst v)) (sym qt) h)
For a semantic environment δ, bound δ is the value of the bounding term embedded back into L. It serves as the canonical witness for the outer value slot of the coded bounded quantifier, and its members are the elements over which the bounded formula ranges.
bound : DB.SM ^ n → S bound δ = Semantic.intoL W (value t δ)
The bound belongs to the carrier: the value's second component is its membership in the carrier, transported along the carrier's naming equation.
bound∈W : (δ : DB.SM ^ n) → ⟨ fst (bound δ) ∈ fst (lookup wi Γ) ⟩ bound∈W δ = subst (λ X → ⟨ fst (value t δ) ∈ X ⟩) (sym qw) (snd (value t δ))
When z is the graph of δ, the underlying set of bound δ is definitionally the underlying set of the semantic value of t, so reflexivity supplies the equality required by term-in. The result is TmIsV (ct t) (fst z) (fst (bound δ)), certifying that the chosen bound represents the coded term's value at the encoded environment.
bound-term : (δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ → TmIsV (ct t) (fst z) (fst (bound δ)) bound-term δ z qz = term-in t δ z (bound δ) qz refl
The representation-level certificate from bound-term is then converted by tmIn' into the object-language tmIs formula at the exact shifted slots used by the bounded-quantifier body. Thus the canonical semantic bound can be inserted into that body's outer quantified layer.
bound-read : (δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ → ⟨ (bound δ ∷ z ∷ Γ) ⊨ tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)) ⟩ bound-read δ z qz = tmIn' z (bound δ) (bound-term δ z qz)
For the forward half of the bounded universal bridge, consider an arbitrary candidate value v satisfying the term clause and an arbitrary carrier member x lying in v. The lemma term-out identifies the underlying set of v with the underlying set of the actual semantic value of t, so membership of x transports to the semantic bound. The universal semantic hypothesis gives the child's truth, and child converts it back to the encoded extension clause.
allInBridge : ExtFact (fst (SatW (∀̇∈ t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ Γ) ⊨ bqAll wi ti yai N0i N1i ⟩) allInBridge = direct-extension (∀̇∈ t a) (λ z → (z ∷ Γ) ⊨ bqAll wi ti yai N0i N1i) (λ δ z qz h v hv ht x hx hxv → subst ⟨_⟩ (sym (child a δ (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx) (v ∷ z ∷ Γ) i1 (sh 2 yai) qz qa))
For the reverse half, an arbitrary restricted-model element x lying in the semantic bound must satisfy the child. The coded universal is instantiated with the canonical value bound δ, using bound∈W and bound-read, and with the embedded element intoL W x, using its carrier membership and the assumed bound membership. Reading child outward then gives Meaning a (x ∷ δ).
(h (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx) (subst (λ V → ⟨ fst x ∈ V ⟩) (term-out t δ z v qz (tmOut z v ht)) hxv))) (λ δ z qz h x hx → subst ⟨_⟩ (child a δ x (bound δ ∷ z ∷ Γ) i1 (sh 2 yai) qz qa) (h (bound δ) (bound∈W δ) (bound-read δ z qz)
The last argument is exactly the hypothesis that x lies in the semantic value of the bounding term. Supplying it completes the universal verifier for every such x, and hence completes the reverse implication required by direct-extension.
(Semantic.intoL W x) (subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd x)) hx))
The bounded existential bridge states the same extensional fact for ∃̇∈ t a: membership in the internal value is equivalent, within the environment set, to satisfaction of the three-layer bounded-existential formula over the carrier.
exInBridge : ExtFact (fst (SatW (∃̇∈ t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ Γ) ⊨ bqEx wi ti yai N0i N1i ⟩) exInBridge = direct-extension (∃̇∈ t a) (λ z → (z ∷ Γ) ⊨ bqEx wi ti yai N0i N1i) (λ δ z qz → PT.map (λ { (x , hx , h) → bound δ , bound∈W δ , bound-read δ z qz
From a semantic witness x for the bounded existential, the forward map chooses the canonical outer value bound δ, supplies its carrier membership and term certificate, and embeds x as the inner carrier witness. Its membership in the semantic bound is retained, while child read backward produces the required encoded extension witness. Every existential witness remains under propositional truncation.
, ∣ Semantic.intoL W x , subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd x) , hx , subst ⟨_⟩ (sym (child a δ x (bound δ ∷ z ∷ Γ) i1 (sh 2 yai) qz qa)) h ∣₁ })) (λ δ z qz → PT.rec squash₁ (λ { (v , hv , ht , h) → PT.map (λ { (x , hx , hxv , hc) → (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx) , subst (λ V → ⟨ fst x ∈ V ⟩) (term-out t δ z v qz (tmOut z v ht)) hxv
In the reverse map, the outer truncated witness supplies a candidate term value v, and the inner one supplies a carrier member x lying in v together with an encoded child extension. Reading the term clause outward identifies the underlying set of v with the underlying set of the actual semantic bound. That equality transports x's membership to the true bound, and child transports the encoded child evidence to semantic satisfaction.
, subst ⟨_⟩ (child a δ (fst x , subst (λ X → ⟨ fst x ∈ X ⟩) qw hx) (v ∷ z ∷ Γ) i1 (sh 2 yai) qz qa) hc }) h }))
The atomic body binds two values, not three: a carrier element v proposed as the value of t, and a carrier element x proposed as the value of u. It then conjoins the two tmIs clauses with the given relation formula rel, evaluated in the context x ∷ v ∷ z ∷ Γ; the coded environment z is already free, and rel is a formula rather than a bound entry.
atomEx : ∀ {k} → Fin k → Fin k → Fin k → Fin k → Fin k → Formula S (3 + k) → Formula S (1 + k) atomEx wi ti ui N0i N1i rel = ∃̇∈ (var (suc wi)) (∃̇∈ (var (suc (suc wi))) (tmIs (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) ∧̇ (tmIs (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) ∧̇ rel)))
AtomBridge abstracts the common proof for membership and equality atoms. The terms t and u and the five slot equations determine how their codes and the tags # 0, # 1 are read; the parameters op, R, and rel then specify the meta-level atom, its ambient binary relation, and the object-language formula that represents that relation.
module AtomBridge {n : ℕ} (t u : Term Ab n) {k : ℕ} (Γ : S ^ k) (wi ti ui N0i N1i : Fin k) (qw : fst (lookup wi Γ) ≡ Wv) (qt : fst (lookup ti Γ) ≡ ct t) (qu : fst (lookup ui Γ) ≡ ct u) (q0 : fst (lookup N0i Γ) ≡ # 0) (q1 : fst (lookup N1i Γ) ≡ # 1) (op : ∀ {j} → Term Ab j → Term Ab j → Formula Ab j)
The agreement hypothesis states the exact interface between rel and R at the three newly prepended entries. Satisfaction of rel in x ∷ v ∷ z ∷ Γ yields R (fst v) (fst x), and a proof of that relation reconstructs satisfaction of rel. Thus the bridge may use an arbitrary representing formula only when both directions are supplied.
(R : V ℓ → V ℓ → Type (ℓ-suc ℓ)) (rel : Formula S (3 + k)) (agree : (z v x : S) → (⟨ (x ∷ v ∷ z ∷ Γ) ⊨ rel ⟩ → R (fst v) (fst x)) × (R (fst v) (fst x) → ⟨ (x ∷ v ∷ z ∷ Γ) ⊨ rel ⟩)) (cnd-out : (δ : DB.SM ^ n) → ⟨ Meaning (op t u) δ ⟩ → R (fst (value t δ)) (fst (value u δ)))
Two further hypotheses connect the chosen relation to the intended atomic semantics. The first sends Meaning (op t u) δ to R of the two evaluated term values, while the second reconstructs that meaning from the same relation. These hypotheses keep the generic bridge neutral between membership and equality.
(cnd-in : (δ : DB.SM ^ n) → R (fst (value t δ)) (fst (value u δ)) → ⟨ Meaning (op t u) δ ⟩) where
The context δ3 z v x = x ∷ v ∷ z ∷ Γ places the proposed value of u at slot i0, the proposed value of t at i1, and the coded environment at i2. These are the three newly exposed entries used by the two term clauses and the relation interface; the inherited entries of Γ remain available to the generic formula rel. Only x and v are newly bound by atomEx, while z is already the free environment argument.
private δ3 : (z v x : S) → S ^ (3 + k) δ3 z v x = x ∷ v ∷ z ∷ Γ
The two outward readers turn the object-language term clauses in δ3 z v x into TmIsV statements. Transport along qt makes the first statement concern the actual code ct t and proposed value v; transport along qu does the same for ct u and proposed value x. The coded environment remains the common argument z.
tOut : (z v x : S) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) ⟩ → TmIsV (ct t) (fst z) (fst v) tOut z v x h = subst (λ w → TmIsV w (fst z) (fst v)) qt (tmIs-out (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1 h) uOut : (z v x : S) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) ⟩ → TmIsV (ct u) (fst z) (fst x) uOut z v x h = subst (λ w → TmIsV w (fst z) (fst x)) qu
The converse readers rebuild the two object-language term clauses from TmIsV. For t, the code is first transported backward along qt and then passed to tmIs-in; the declaration for uIn sets up the identical construction for u at its own value slot.
(tmIs-out (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1 h) tIn : (z v x : S) → TmIsV (ct t) (fst z) (fst v) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) ⟩ tIn z v x h = tmIs-in (suc (suc (suc ti))) i2 i1 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1 (subst (λ w → TmIsV w (fst z) (fst v)) (sym qt) h) uIn : (z v x : S) → TmIsV (ct u) (fst z) (fst x) → ⟨ δ3 z v x ⊨ tmIs (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) ⟩
For u, backward transport along qu changes TmIsV (ct u) (fst z) (fst x) into the code named by the caller's slot, and tmIs-in rebuilds the second object-language term clause. The bridge now has both read and write directions for each proposed term value.
uIn z v x h = tmIs-in (suc (suc (suc ui))) i2 i0 (sh 3 N0i) (sh 3 N1i) (δ3 z v x) q0 q1 (subst (λ w → TmIsV w (fst z) (fst x)) (sym qu) h)
The theorem atomBridge now asks direct-extension to compare the atomic semantic value with atomEx on every encoded environment. Its outward map must start from Meaning (op t u) δ and construct the two bounded value witnesses, their term clauses, and the relation formula in x ∷ v ∷ z ∷ Γ; the inward map will reverse the same data.
atomBridge : ExtFact (fst (SatW (op t u))) (fst (envSet W n)) (λ z → ⟨ (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel ⟩) atomBridge = direct-extension (op t u) (λ z → (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel) out inn where out : (δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ → ⟨ Meaning (op t u) δ ⟩ → ⟨ (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel ⟩
The outward construction chooses the actual semantic values of t and u, embedded into L, as the two bounded witnesses. The second components of the restricted-model values prove their membership in the carrier; term-in followed by tIn and uIn supplies the two term clauses, and cnd-out followed by the reverse half of agree supplies the object-language relation. The nested witnesses are introduced under the two propositional truncations.
out δ z qz h = ∣ v , subst (λ X → ⟨ fst v ∈ X ⟩) (sym qw) (snd (value t δ)) , ∣ x , subst (λ X → ⟨ fst x ∈ X ⟩) (sym qw) (snd (value u δ)) , tIn z v x (term-in t δ z v qz refl) , uIn z v x (term-in u δ z x qz refl) , agree z v x .snd (cnd-out δ h) ∣₁ ∣₁
The local names v and x are the embeddings into L of the evaluated terms t and u. They are canonical witnesses for the two value quantifiers of atomEx; the atomic code itself names the two term codes, while these witnesses supply their values at the particular environment δ.
where v x : S v = Semantic.intoL W (value t δ) x = Semantic.intoL W (value u δ)
The reverse implication of atomBridge starts with a meta-level environment δ, a coded environment z, and an identification of z with the canonical graph of δ. Its remaining hypothesis says that atomEx holds at z. The outer propositionally truncated bounded existential supplies a candidate v, a proof hv that it lies in W, and an inner existential proof h. Since Meaning (op t u) δ is a proposition, PT.rec may eliminate this truncation, and then the inner one, into that target. At this point v is only a candidate for the value of t; the term-value record extracted from the inner witness will identify it with the actual semantic value.
inn : (δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ → ⟨ (z ∷ Γ) ⊨ atomEx wi ti ui N0i N1i rel ⟩ → ⟨ Meaning (op t u) δ ⟩ inn δ z qz = PT.rec (snd (Meaning (op t u) δ)) (λ { (v , hv , h) → PT.rec (snd (Meaning (op t u) δ)) (λ { (x , hx , ht , hu , hr) → cnd-in δ (subst2 R (term-out t δ z v qz (tOut z v x ht))
The inner witness supplies a second candidate x, its membership proof hx : x ∈ W, proofs ht and hu of the two term clauses, and a proof hr of the object-language relation. The proofs hv and hx record the bounds of the two existential quantifiers, but no further use of them is needed here. First, agree z v x .fst reads hr as R (fst v) (fst x). Because z is the canonical graph of δ, tOut and uOut feed the two term-clause proofs to term-out, which identifies the underlying sets of v and x with those of the semantic values of t and u. Then subst2 transports R along those identifications, and cnd-in turns the transported relation into Meaning (op t u) δ. This completes the atomic bridge. Downstream it is instantiated for membership and equality. In SatSoundC, subcode closure and structural recursion pin table entries to SatW by comparing extension facts; in SatHoldsC, decoding, prescribed table values, totality, and the stated domain let the same bridges fill all ten clauses. SatisfactionDescription supplies the code-domain and environment-tower facts, proves that the canonical graph SatGraph.pairs W satisfies tableAt, and packages towerAt, codesAt, and tableAt as satAt. Its SatRead module exposes two-way membership readers for the resulting table graph, code set, and environment tower.
(term-out u δ z x qz (uOut z v x hu)) (agree z v x .fst hr)) }) h })
Recap
The clause semantics is now tied to ordinary satisfaction in both directions. Environment graphs interpret variables, the recursive bridges handle the logical constructors, and the atomic bridge transports membership and equality through the values of their terms. The proof uses only the existence and extensional facts stated by the coded table; it does not assume that an arbitrary table relation is already functional.