Internal reasoning about syntax begins with a set of formula keys inside L. This chapter compares such a candidate domain with the external formula grammar in two directions: every member merely decodes to a formula key, and every genuine formula key belongs to the domain. These claims concern code membership, not the truth or satisfaction of the encoded formulas.

{-# OPTIONS --cubical --safe --guardedness #-}

The argument uses excluded middle together with propositional truncation. Truncation records that a decoding witness exists without choosing one, and it may be eliminated only when the target is again a proposition.

open import Base.Prelude
open import Base.Classical using ( LEM )

Assume lem : LEM (ℓ-suc ℓ). Every construction in the chapter is relative to this hypothesis, but the hypothesis does not strengthen the decoding conclusion: witnesses to decoded formulas remain propositionally truncated.

module L.Coding.CodeDomainAdequacy {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

The chapter speaks about the full first-order language of set theory: formulas with the two bounded quantifiers as well as the unbounded ones, and terms built from variables and constants. These are the objects whose codes the domain must gather and describe.

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; Term; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∃̇∈; ∀̇∈ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

Formula keys are nested ordered pairs, so injectivity of pairing recovers their arity, tag, and payload from an equality of keys. Natural-number arities are represented by von Neumann numerals, and constructible environment sets provide internal representatives for finite parameter vectors.

open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; #mono )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Environment {ℓ} using ( env )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )
open import L.Axioms.Numerals {ℓ} using ( numeralL-fst; sucʟ; sucʟ-fst )

The object language can express that a structurally assembled key belongs to a candidate domain. Ordered-pair expressions build the nested key, and their adequacy theorem identifies satisfaction of the resulting formula with membership of the corresponding host-level pair code.

open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate )
open import L.Coding.Expressions {ℓ} using ( sucAtL )
open import L.Coding.Model {ℓ} using ( container )
import L.Coding.Expressions {ℓ} as CodingExpressions
module E = CodingExpressions.PairExpression

Quantifier codes change arity. The body of either kind of quantifier is a key at the successor arity, while a bounded quantifier also carries a term legal at the current arity. The semantic lemmas for pairs, successors, and extended environments express precisely these changes under binders.

open import L.Coding.Quantification {ℓ} using
  ( i0; i1; i2; i3; i4; i5; i6; i7; i8; sh
  ; pr-out; pr-in; down; fstS; sndS; suc-out; suc-in
  ; sndEx; sndAll; bothEx
  ; sndEx-out; sndAll-in; bothEx-out; bothAll-in

Existential payload descriptions are propositionally truncated, sometimes through two nested witnesses. Their inward and outward readings preserve that truncation. The ten constructor tags are represented by the numerals zero through nine, and a separate environment tower records the arity at which each code is read.

  ; fillSnd; fillBoth; useSnd; useBoth
  ; f0; f1; f2; f3; f4; f5; f6; f7; f8; f9
  ; bigOr-in; bigOr-out )
open import L.Coding.EnvironmentTower {ℓ} lem using ( module Tower; nn )
open import L.Coding.CodeDomain {ℓ} using

The description codesAt has two complementary halves. shapeAt reads an existing domain member as one of the ten constructor shapes and, for composite codes, requires its immediate subkeys to remain in the domain. closeAt goes in the generating direction: legal terms and existing subkeys produce the corresponding new key.

  ( isTm; keyUp; keyExpr; atomKeyExpr; bndKeyExpr
  ; unKey; binKey; atomKey; bndKey
  ; Tags; shN; module Shape; shapeAt; module Close; closeAt; codesAt )
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet )

A constructor tag is an element of Fin 10; its natural-number value selects one of the ten payload predicates and is automatically less than ten. Environments are finite vectors, while the codes stored in the hierarchy are nested set-theoretic pairs.

open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( toℕ<n )
open import Cubical.Data.Vec using ( _∷_; lookup )
open import Cubical.Data.Sigma using ( _×_ )

Decoding branches over disjoint constructor cases and often returns only a propositionally truncated witness. Pair equalities are transported componentwise, and impossible tags lead to the empty type. None of these operations turns a merely existing formula into a globally chosen decoder.

open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.Prelude using ( subst2 )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

The cumulative hierarchy supplies set-valued ordered-pair codes, von Neumann numerals, and the successor operation on arities. Membership has a small fibre presentation, and equality of hierarchy sets is a proposition; these facts justify the truncated decompositions and their elimination into membership or equality claims.

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; sucV )

The carrier of the constructible structure is fixed as S, so every environment and every formula reading below lives over it.

open hPropStructure 𝒮ʟ using ( S )

All code descriptions are interpreted in the first-order structure carried by L. Thus“this assembled key belongs to C”has both an object-language formulation and a host-level membership reading; the adequacy lemmas identify these two forms of the same assertion.

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )

Reading the description

Term codes are described first. A set t is a term code at arity ar when, merely, it is the pair of the tag zero with an element of the working set Wv, or the pair of the tag one with an element of the set ar. Note that ar is still an arbitrary set here; only when it is known to be a numeral does the second branch recover a bounded variable index.

IsTmV : V ℓ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
IsTmV Wv t ar = ∥ (Σ[ x ∈ V ℓ ] ((t ≡ pr (# ) x) × ⟨ x ∈ Wv ⟩))
                ⊎ (Σ[ i ∈ V ℓ ] ((t ≡ pr (# ) i) × ⟨ i ∈ ar ⟩)) ∥₁

The first three payload predicates cover atomic formulas, binary connectives, and falsity. An atomic payload merely decomposes into two legal term codes; a binary payload merely decomposes into two same-arity subkeys already in the candidate domain; the falsity payload is directly the equality r = # 0 and carries no existential witness.

module CodesSem (Wv Cv : V ℓ) where
  AtomP BinP ConP QuP BqP : V ℓ → V ℓ → Type (ℓ-suc ℓ)
  AtomP ar r = ∥ Σ[ t ∈ V ℓ ] Σ[ u ∈ V ℓ ] ((r ≡ pr t u) × (IsTmV Wv t ar × IsTmV Wv u ar)) ∥₁
  BinP ar r = ∥ Σ[ a ∈ V ℓ ] Σ[ b ∈ V ℓ ] ((r ≡ pr a b) × (⟨ pr ar a ∈ Cv ⟩ × ⟨ pr ar b ∈ Cv ⟩)) ∥₁
  ConP ar r = r ≡ # 

The quantifier payloads complete the list. An unbounded-quantifier payload is a subkey at the successor arity. A bounded-quantifier payload pairs a term code legal at the current arity with such a subkey. This asymmetry comes from the grammar itself: the body has successor arity, whereas the bounding term has the arity of the quantified formula.

  QuP ar r = ⟨ pr (sucV ar) r ∈ Cv ⟩
  BqP ar r = ∥ Σ[ t ∈ V ℓ ] Σ[ a ∈ V ℓ ] ((r ≡ pr t a) × (IsTmV Wv t ar × ⟨ pr (sucV ar) a ∈ Cv ⟩)) ∥₁

The payload table begins: tags zero and one carry the two atom shapes, and tags two and three carry the binary shapes of conjunction and disjunction.

  PayN : ℕ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
  PayN  = AtomP
  PayN  = AtomP
  PayN  = BinP
  PayN  = BinP

The table continues: tag four carries implication, tag five the constant falsity, tags six and seven the two unbounded quantifiers, and tag eight the bounded universal.

  PayN  = BinP
  PayN  = ConP
  PayN  = QuP
  PayN  = QuP
  PayN  = BqP

Tag nine carries the bounded existential payload. The auxiliary family PayN is empty at every natural number at least ten, but a legal Key chooses its tag from Fin 10; hence only the ten cases zero through nine can occur in a key.

  PayN  = BqP
  PayN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) _ _ = Empty.⊥*

A key at arity ar is, merely, a tag from the ten together with a payload of the matching shape. Note what a key is not: it is not an inductive syntax tree, and the decomposition is not claimed to be unique data. A key is the truncated evidence that a set-coded pair splits into one of ten known shapes.

  Key : V ℓ → V ℓ → Type (ℓ-suc ℓ)
  Key ar p = ∥ Σ[ k ∈ Fin  ] Σ[ r ∈ V ℓ ] ((p ≡ pr (# (toℕ k)) r) × PayN (toℕ k) ar r) ∥₁

Fix an environment containing a proposed term code t, an arity set ar, a working set Wv, and two entries known to be the numerals zero and one. Under these tag equations, the object-language predicate isTm can be compared exactly with the ambient predicate IsTmV Wv t ar.

module _ {k : ℕ} (t ar w N0 N1 : Fin k) (δ : S ^ k)
  (q0 : fst (lookup N0 δ) ≡ # ) (q1 : fst (lookup N1 δ) ≡ # ) where
  private
    Wv = fst (lookup w δ)

The outward reading eliminates the truncated disjunction of the object-language formula. In the constant branch, the existential recovers the second component of the pair, the numeral equation aligns the tag, and the membership travels into IsTmV; the result is the left branch of the truncated definition.

  isTm-out : ⟨ δ ⊨ isTm t ar w N0 N1 ⟩ → IsTmV Wv (fst (lookup t δ)) (fst (lookup ar δ))
  isTm-out = PT.rec squash₁
    (λ { (inl h) → PT.map
           (λ { (v , s , (e , v∈)) → inl (fst v , (e ∙ cong (λ a → pr a (fst v)) q0 , v∈)) })
           (sndEx-out t N0 (var i0 ∈̇ var (sh  w)) δ h)

The variable branch repeats the same three moves with the numeral one and the arity set, producing the right branch. Together the two branches say the object-language recognition and the set-level IsTmV are exactly equivalent.

       ; (inr h) → PT.map
           (λ { (v , s , (e , v∈)) → inr (fst v , (e ∙ cong (λ a → pr a (fst v)) q1 , v∈)) })
           (sndEx-out t N1 (var i0 ∈̇ var (sh  ar)) δ h) })

The inward reading runs the conversion the other way. In the constant branch, the filling lemma places the witness x under the existential at slot zero, and the pair equation is transported along the reversed numeral equation so that the satisfaction matches the shape of the object-language formula.

  isTm-in : IsTmV Wv (fst (lookup t δ)) (fst (lookup ar δ)) → ⟨ δ ⊨ isTm t ar w N0 N1 ⟩
  isTm-in = PT.rec (snd (δ ⊨ isTm t ar w N0 N1))
    (λ { (inl (x , (e , x∈))) →
           ∣ inl (fillSnd t δ (lookup N0 δ) (down (lookup w δ) x x∈)
                    (e ∙ cong (λ a → pr a x) (sym q0)) (var i0 ∈̇ var (sh  w)) x∈ N0 refl) ∣₁

The variable branch fills the witness i under the existential at the numeral-one slot, transported by the corresponding reversed equation. The two branches close the equivalence in both directions.

       ; (inr (i , (e , i∈))) →
           ∣ inr (fillSnd t δ (lookup N1 δ) (down (lookup ar δ) i i∈)
                    (e ∙ cong (λ a → pr a i) (sym q1)) (var i0 ∈̇ var (sh  ar)) i∈ N1 refl) ∣₁ })

The predicate keyUp C ar r expresses one precise membership statement: the pair (suc ar,r) belongs to C. Its bounded existential presentation chooses an actual member of C and then exposes enough of that member to verify both its pair shape and the successor equation.

module _ {k : ℕ} (C ar r : Fin k) (δ : S ^ k) where
  keyUp-out : ⟨ δ ⊨ keyUp C ar r ⟩ → ⟨ pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ) ⟩
  keyUp-out = PT.rec (snd (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ)))
    (λ { (c' , (c'∈ , h)) → PT.rec (snd (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ)))
      (λ { (s , (s∈ , h')) → PT.rec (snd (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ)))

In the outward direction, the pair formula identifies the chosen member of C with (ar',r), while the successor formula identifies ar' with suc ar. Transporting membership along these two equalities yields (suc ar,r) ∈ C. All truncated witnesses are eliminated only into this membership proposition.

        (λ { (ar' , (ar'∈ , (e , hs))) →
          subst (λ u → ⟨ u ∈ fst (lookup C δ) ⟩)
            (pr-out i2 i0 (sh  r) (ar' ∷ s ∷ c' ∷ δ) e
             ∙ cong (λ a → pr a (fst (lookup r δ))) (suc-out (sh  ar) i0 (ar' ∷ s ∷ c' ∷ δ) hs))
            c'∈ })

The three bounded witnesses therefore serve only to certify the displayed member of C; after their truncations are eliminated, keyUp-out has exactly the ambient membership statement (suc ar,r) ∈ C.

        h' })
      h })

For the inward direction, start with (suc ar,r) ∈ C. Present the successor arity as a constructible set, package the ordered pair with r, and use these objects as the three bounded witnesses. The pair and successor formulas then reconstruct satisfaction of keyUp C ar r.

  keyUp-in : ⟨ pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ) ⟩ → ⟨ δ ⊨ keyUp C ar r ⟩
  keyUp-in h = ∣ c' , (h , ∣ c .fst , (c .snd .fst , ∣ ar' , (c .snd .snd .fst
    , ( pr-in i2 i0 (sh  r) (ar' ∷ c .fst ∷ c' ∷ δ) (sym (cong (λ a → pr a (fst (lookup r δ))) (sucʟ-fst (lookup ar δ))))
      , suc-in (sh  ar) i0 (ar' ∷ c .fst ∷ c' ∷ δ) (sucʟ-fst (lookup ar δ)) )) ∣₁) ∣₁) ∣₁
    where

Concretely, ar' represents suc ar, c' represents the member (suc ar,r) of C, and the containing set supplied with c' witnesses the bounded-membership chain used by the formula. Their underlying-set equations ensure that the internal witnesses denote the intended ambient pair.

    ar' : S
    ar' = sucʟ (lookup ar δ)
    c' : S
    c' = down (lookup C δ) (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ))) h
    c = container c' ar' (lookup r δ) (cong (λ a → pr a (fst (lookup r δ))) (sym (sucʟ-fst (lookup ar δ))))

Fix a candidate domain C, an arity value A, a tag value N, and a payload a. The unary key assembled from these data is the nested pair (A,(N,a)).

module _ {k : ℕ} (C ar N a : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)

The outward reading of unKey states precisely that the nested key (A,(N,a)) belongs to C. Adequacy of the ordered-pair expression turns object-language membership into this host-level set-membership statement.

  unKey-out : ⟨ δ ⊨ unKey C ar N a ⟩ → ⟨ pr A (pr Nv (fst (lookup a δ))) ∈ Cv ⟩
  unKey-out = E.member-out (keyExpr ar N (E.slot a)) (var C) δ

Adequacy works in the reverse direction as well: membership (A,(N,a)) ∈ C yields satisfaction of the object-language predicate unKey. The key clause and its host-level reading therefore agree in both directions.

  unKey-in : ⟨ pr A (pr Nv (fst (lookup a δ))) ∈ Cv ⟩ → ⟨ δ ⊨ unKey C ar N a ⟩
  unKey-in = E.member-in (keyExpr ar N (E.slot a)) (var C) δ

For a binary constructor, fix two payload components a and b. Their ordered pair P=(a,b) becomes the payload of the key (A,(N,P)); the arity and tag occupy the same outer positions as in the unary case.

module _ {k : ℕ} (C ar N a b : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)

The two argument values form the ordered pair P = (a,b). This pair is the payload in the nested binary key (A,(N,P)).

    P = pr (fst (lookup a δ)) (fst (lookup b δ))

The outward reading of binKey is precisely the membership (A,(N,(a,b))) ∈ C. It preserves the three logical levels of the encoding: arity, constructor tag, and the paired arguments.

  binKey-out : ⟨ δ ⊨ binKey C ar N a b ⟩ → ⟨ pr A (pr Nv P) ∈ Cv ⟩
  binKey-out = E.member-out (keyExpr ar N (E.pair (E.slot a) (E.slot b))) (var C) δ

The inward reading is its reverse, and the two together identify the formula statement with the set membership, as with every key clause.

  binKey-in : ⟨ pr A (pr Nv P) ∈ Cv ⟩ → ⟨ δ ⊨ binKey C ar N a b ⟩
  binKey-in = E.member-in (keyExpr ar N (E.pair (E.slot a) (E.slot b))) (var C) δ

An atomic key has two term codes as its payload. Each term code carries its own term tag and argument, and the pair of these two term codes is placed beneath the atomic constructor tag and the common arity.

module _ {k : ℕ} (C ar N Nx x Ny y : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)

Write the two term codes as T=(Nx,x) and U=(Ny,y). At this stage Nx and Ny are arbitrary tag values from the environment; their being zero or one is imposed when the atomic closure cases are instantiated.

    T = pr (fst (lookup Nx δ)) (fst (lookup x δ))
    U = pr (fst (lookup Ny δ)) (fst (lookup y δ))

The atomic clause reads outward as (A,(N,(T,U))) ∈ C, where T and U are the two term codes. Thus the outer pair records the arity, the next records the atomic tag, and the innermost pair records the two terms.

  atomKey-out : ⟨ δ ⊨ atomKey C ar N Nx x Ny y ⟩ → ⟨ pr A (pr Nv (pr T U)) ∈ Cv ⟩
  atomKey-out = E.member-out (atomKeyExpr ar N Nx x Ny y) (var C) δ

The inward reading is its reverse, closing the atomic case in both directions like every key clause before it.

  atomKey-in : ⟨ pr A (pr Nv (pr T U)) ∈ Cv ⟩ → ⟨ δ ⊨ atomKey C ar N Nx x Ny y ⟩
  atomKey-in = E.member-in (atomKeyExpr ar N Nx x Ny y) (var C) δ

A bounded-quantifier key carries two different components in its payload: a term code for the bound and a subformula code for the body. The common outer data are again the current arity A and the bounded-quantifier tag N.

module _ {k : ℕ} (C ar N Nx x a : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)

Write the bound-term code as T=(Nx,x) and the body code as Av. The term is checked at the current arity, whereas the body key is checked at the successor arity; keeping them as separate payload components records this grammatical asymmetry.

    T = pr (fst (lookup Nx δ)) (fst (lookup x δ))
    Av = fst (lookup a δ)

The bounded-key clause reads outward as (A,(N,(T,Av))) ∈ C. The innermost pair contains the bound-term code and the body code in that order; it is not itself a claim that either component is already legal.

  bndKey-out : ⟨ δ ⊨ bndKey C ar N Nx x a ⟩ → ⟨ pr A (pr Nv (pr T Av)) ∈ Cv ⟩
  bndKey-out = E.member-out (bndKeyExpr ar N Nx x a) (var C) δ

Conversely, membership of (A,(N,(T,Av))) in C yields satisfaction of bndKey. Together the two readings establish only the structural membership equivalence; legality of T and successor-arity membership of Av are supplied by the surrounding payload predicate.

  bndKey-in : ⟨ pr A (pr Nv (pr T Av)) ∈ Cv ⟩ → ⟨ δ ⊨ bndKey C ar N Nx x a ⟩
  bndKey-in = E.member-in (bndKeyExpr ar N Nx x a) (var C) δ

Now fix a candidate code domain C, a working set W, and ten environment entries certified to be the numerals zero through nine. For each tag, the object-language payload description can then be compared with its ambient predicate AtomP, BinP, ConP, QuP, or BqP.

module PayRead {m : ℕ} (C w : Fin m) (N : Fin  → Fin m) (δ : S ^ ( + m))
  (tg : Tags δ (shN  N)) where
  private
    Cv = fst (lookup (sh  C) δ)
    Wv = fst (lookup (sh  w) δ)

In each payload reading, A denotes the recorded arity and R the raw payload. The equations for tags zero and one are singled out because both atomic and bounded-quantifier payloads must recognize term codes, whose two legal shapes use precisely these tags.

    A = fst (lookup i5 δ)
    R = fst (lookup i0 δ)
    q0 = tg f0
    q1 = tg f1
    rS = lookup i0 δ

Both sides of the comparison use the same underlying sets Wv and Cv. The syntactic payload formulas therefore describe term membership in Wv and subkey membership in Cv, exactly matching the parameters of the five ambient payload predicates.

    module Sh = Shape C w N
  open CodesSem Wv Cv

The atomic body requires both components of the payload to satisfy the term-code predicate at the recorded arity. The binary body instead requires both components to occur as keys of that same arity in the candidate domain. These are different conditions even though both payloads are encoded as pairs.

  private
    tmBody : Formula S ( + m)
    tmBody = isTm i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) ∧̇ isTm i0 i8 (sh  w) (sh  (N f0)) (sh  (N f1))
    binBody : Formula S ( + m)
    binBody = appAt (sh  C) i8 i1 ∧̇ appAt (sh  C) i8 i0

The last payload shape covers the two bounded quantifiers. Its body requires a legal term at the current arity for the bound and a body key in the code set at the successor arity.

    bqBody : Formula S ( + m)
    bqBody = isTm i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) ∧̇ keyUp (sh  C) i8 i0

Reading an atomic payload outward removes the two existential binders and produces terms t and u, an equation R ≡ pr t u, and proofs that both terms are legal at arity A. The term reader uses the tag equations for zero and one to turn the two satisfaction claims into the corresponding truncated term shapes.

  atom-out : ⟨ δ ⊨ Sh.atomPay ⟩ → AtomP A R
  atom-out h = PT.map
    (λ { (t , u , s , (e , (ht , hu))) → fst t , fst u
       , ( e , ( isTm-out i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (u ∷ t ∷ s ∷ δ) q0 q1 ht
               , isTm-out i0 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (u ∷ t ∷ s ∷ δ) q0 q1 hu ) ) })

The consumption itself is one application of the two-fold existential elimination: the witnesses t, u and the container are extracted, and the remaining conjunction is discharged into the payload data.

    (bothEx-out i0 tmBody δ h)

Reading inward rebuilds the satisfaction from the data. The truncated legality proofs are eliminated, since the goal is again a truncated satisfaction, and each of the two terms enters its legality atom through the shifted context.

  atom-in : AtomP A R → ⟨ δ ⊨ Sh.atomPay ⟩
  atom-in = PT.rec (snd (δ ⊨ Sh.atomPay))
    (λ { (t , u , (e , (ht , hu))) →
      fillBoth i0 δ (fstS rS t u e) (sndS rS t u e) e tmBody
        ( isTm-in i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (δ12 t u e) q0 q1 ht

The second legality claim is inserted in the same way. The auxiliary environment δ12 consists of the two components selected by R ≡ pr t u, a container witnessing that pairing, and the original environment; this is exactly the environment in which both term atoms are interpreted.

        , isTm-in i0 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (δ12 t u e) q0 q1 hu ) })
    where
    δ12 : (t u : V ℓ) (e : R ≡ pr t u) → S ^ ( + m)
    δ12 t u e = sndS rS t u e ∷ fstS rS t u e ∷ container rS (fstS rS t u e) (sndS rS t u e) e .fst ∷ δ

Reading a binary payload outward yields payloads a and b, an equation R ≡ pr a b, and membership of both pr A a and pr A b in the code set. Adequacy of the two application atoms identifies those memberships in the extended environment.

  bin-out : ⟨ δ ⊨ Sh.binPay ⟩ → BinP A R
  bin-out h = PT.map
    (λ { (a , b , s , (e , (ha , hb))) → fst a , fst b
       , ( e , ( subst ⟨_⟩ (appAt-adequate (sh  C) i8 i1 (b ∷ a ∷ s ∷ δ)) ha
               , subst ⟨_⟩ (appAt-adequate (sh  C) i8 i0 (b ∷ a ∷ s ∷ δ)) hb ) ) })

As with the atoms, the two existentials of the binary condition are consumed by a single elimination.

    (bothEx-out i0 binBody δ h)

Reading inward fills the two existentials with the named sub-codes. The two application atoms are satisfied by transporting along the adequacy in the reverse direction, back into the shifted context.

  bin-in : BinP A R → ⟨ δ ⊨ Sh.binPay ⟩
  bin-in = PT.rec (snd (δ ⊨ Sh.binPay))
    (λ { (a , b , (e , (ha , hb))) →
      fillBoth i0 δ (fstS rS a b e) (sndS rS a b e) e binBody
        ( subst ⟨_⟩ (sym (appAt-adequate (sh  C) i8 i1 (δ12 a b e))) ha

The binary helper records the same shifted-context shape, now built from the two ambient values a and b.

        , subst ⟨_⟩ (sym (appAt-adequate (sh  C) i8 i0 (δ12 a b e))) hb ) })
    where
    δ12 : (a b : V ℓ) (e : R ≡ pr a b) → S ^ ( + m)
    δ12 a b e = sndS rS a b e ∷ fstS rS a b e ∷ container rS (fstS rS a b e) (sndS rS a b e) e .fst ∷ δ

The falsity payload contains no subordinate data. Its formula says that R is the value stored in the zero-tag slot, while ConP A R says R ≡ # 0; composing with the zero-tag equation gives the outward direction.

  con-out : ⟨ δ ⊨ Sh.conPay ⟩ → ConP A R
  con-out h = h ∙ q0

Conversely, an equation R ≡ # 0 composes with the zero-tag equation in reverse to prove that R equals the value of the zero-tag slot, which is precisely satisfaction of the falsity payload.

  con-in : ConP A R → ⟨ δ ⊨ Sh.conPay ⟩
  con-in h = h ∙ sym q0

For either unbounded quantifier, the payload is a body key at the successor arity. The successor-key reader turns satisfaction of this payload formula into membership of pr (sucV A) R in the code set.

  qu-out : ⟨ δ ⊨ Sh.quPay ⟩ → QuP A R
  qu-out = keyUp-out (sh  C) i5 i0 δ

In the reverse direction, membership of pr (sucV A) R in the code set supplies the witnesses required by the successor-key formula and hence proves the quantifier payload.

  qu-in : QuP A R → ⟨ δ ⊨ Sh.quPay ⟩
  qu-in = keyUp-in (sh  C) i5 i0 δ

Reading a bounded-quantifier payload outward yields a term t, a body payload a, and an equation R ≡ pr t a. It also proves that t is legal at arity A and that the body key pr (sucV A) a belongs to the code set.

  bq-out : ⟨ δ ⊨ Sh.bqPay ⟩ → BqP A R
  bq-out h = PT.map
    (λ { (t , a , s , (e , (ht , ha))) → fst t , fst a
       , ( e , ( isTm-out i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (a ∷ t ∷ s ∷ δ) q0 q1 ht
               , keyUp-out (sh  C) i8 i0 (a ∷ t ∷ s ∷ δ) ha ) ) })

The two existentials of the bounded body are consumed by the same two-fold elimination as everywhere else.

    (bothEx-out i0 bqBody δ h)

Reading inward, the bounding term enters its legality atom through the shifted context.

  bq-in : BqP A R → ⟨ δ ⊨ Sh.bqPay ⟩
  bq-in = PT.rec (snd (δ ⊨ Sh.bqPay))
    (λ { (t , a , (e , (ht , ha))) →
      fillBoth i0 δ (fstS rS t a e) (sndS rS t a e) e bqBody
        ( isTm-in i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (δ12 t a e) q0 q1 ht

The body key enters through the successor-key lemma, and the helper records the shifted context built from the bounding value and its container.

        , keyUp-in (sh  C) i8 i0 (δ12 t a e) ha ) })
    where
    δ12 : (t a : V ℓ) (e : R ≡ pr t a) → S ^ ( + m)
    δ12 t a e = sndS rS t a e ∷ fstS rS t a e ∷ container rS (fstS rS t a e) (sndS rS t a e) e .fst ∷ δ

The reader for a label is selected by recursion on the label. Labels zero and one are the two atoms, and labels two, three and four are the three binary connectives.

  payN-out : (k : ℕ) → ⟨ δ ⊨ Sh.payN k ⟩ → PayN k A R
  payN-out  = atom-out
  payN-out  = atom-out
  payN-out  = bin-out
  payN-out  = bin-out

Labels five, six and seven cover falsity and the two unbounded quantifiers; label eight is the bounded universal.

  payN-out  = bin-out
  payN-out  = con-out
  payN-out  = qu-out
  payN-out  = qu-out
  payN-out  = bq-out

Label nine is the bounded existential. Labels ten and beyond name no constructor: their payload is empty, so the reader is the identity on that empty data.

  payN-out  = bq-out
  payN-out (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) h = h

The inward reader is selected by the same recursion, one clause per label.

  payN-in : (k : ℕ) → PayN k A R → ⟨ δ ⊨ Sh.payN k ⟩
  payN-in  = atom-in
  payN-in  = atom-in
  payN-in  = bin-in
  payN-in  = bin-in

Labels four through seven continue the list: the last binary connective, falsity, and the two unbounded quantifiers.

  payN-in  = bin-in
  payN-in  = con-in
  payN-in  = qu-in
  payN-in  = qu-in
  payN-in  = bq-in

Label nine completes the list; beyond ten there is nothing to read, since no legitimate key carries such a label.

  payN-in  = bq-in
  payN-in (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) h = h

The ten-way reader interprets a tagged payload in a seven-entry extension of the ambient environment. It reads the code set and constant alphabet from the ambient entries, while N selects ten ambient positions whose values are identified with the numerals zero through nine by the tag hypothesis.

module TenRead {m : ℕ} (C w : Fin m) (N : Fin  → Fin m) (δ : S ^ ( + m))
  (tg : Tags δ (shN  N)) where
  private
    Cv = fst (lookup (sh  C) δ)
    Wv = fst (lookup (sh  w) δ)

Among the newly bound entries, A is the arity and P is the tagged payload to be recognized as a key. Retaining the set-level representative of P allows the equation P ≡ pr (# (toℕ j)) r to be realized when a tag and its payload r are chosen.

    A = fst (lookup i3 δ)
    P = fst (lookup i0 δ)
    pS = lookup i0 δ
    module Sh = Shape C w N
  open CodesSem Wv Cv

The tag reader converts satisfaction of the j-th tag atom into a key. The truncated witness pairs an index r with a container; the coding equation is transported along the tag equation, which says that the j-th tag slot names the numeral of j, and the payload is read by the label reader at j.

  at-out : (j : Fin ) → ⟨ δ ⊨ Sh.at j ⟩ → Key A P
  at-out j h = PT.map
    (λ { (r , s , (e , hp)) → j , fst r
       , ( e ∙ cong (λ a → pr a (fst r)) (tg j)
         , PayRead.payN-out C w N (r ∷ s ∷ δ) tg (toℕ j) hp ) })

The two existentials of the tag atom are consumed by its own elimination, so the reader never chooses an index: it only unpacks the one that satisfaction provides.

    (sndEx-out i0 (sh  (N j)) (Sh.pay j) δ h)

The inward direction builds the satisfaction from a key: the witness entry is filled with the shifted value, the payload is read inward over the extended context, and the tag equation identifies the naming slot with the numeral of j.

  at-in : (j : Fin ) (r : V ℓ) (e : P ≡ pr (# (toℕ j)) r) → PayN (toℕ j) A r → ⟨ δ ⊨ Sh.at j ⟩
  at-in j r e pay =
    fillSnd i0 δ (lookup (sh  (N j)) δ) rS e' (Sh.pay j)
      (PayRead.payN-in C w N (rS ∷ container pS (lookup (sh  (N j)) δ) rS e' .fst ∷ δ) tg (toℕ j) pay)
      (sh  (N j)) refl

The renamed value pairs the numeral of j with the chosen entry, and the coding equation is composed with the tag equation in reverse, so the extended naming mentions the right slot.

    where
    rS : S
    rS = sndS pS (# (toℕ j)) r e
    e' : P ≡ pr (fst (lookup (sh  (N j)) δ)) (fst rS)
    e' = e ∙ cong (λ a → pr a r) (sym (tg j))

The ten-way outward reader consumes the disjunction and quotes the tag reader at whichever tag the witness names.

  ten-out : ⟨ δ ⊨ Sh.ten ⟩ → Key A P
  ten-out h = PT.rec squash₁ (λ { (j , hj) → at-out j hj }) (bigOr-out δ  Sh.at h)

The inward reader enters the disjunction at the witnessed tag, with the payload read inward at that tag. Both directions together say: satisfaction of the ten-way disjunction is the same thing as carrying a legitimate key.

  ten-in : Key A P → ⟨ δ ⊨ Sh.ten ⟩
  ten-in = PT.rec (snd (δ ⊨ Sh.ten))
    (λ { (j , r , (e , pay)) → bigOr-in δ  Sh.at j (at-in j r e pay) })

The shape reader fixes three ambient sets: the candidate code set C, the constant alphabet w, and the tower E of arity-family pairs. Their underlying iterative sets are used respectively for code membership, legal constant terms, and witnesses (ar,F) belonging to the tower.

module ShapeRead {m : ℕ} (C w E : Fin m) (N : Fin  → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Cv = fst (lookup C γ)
    Wv = fst (lookup w γ)
    Ev = fst (lookup E γ)

For a chosen member c and a tower witness (ar,F), the remaining formula chooses a payload p, requires c ≡ pr ar p, and tests p against the ten possible tag shapes. Thus the nested witnesses expose the outer arity and the inner tagged payload separately.

    module Sh = Shape C w N
    inner : Formula S ( + m)
    inner = sndEx i4 i1 Sh.ten
  open CodesSem Wv Cv

Shaped c records exactly the data extracted from the shape clause: there are ar, F, and p such that pr ar F belongs to E, c ≡ pr ar p, and p is a legitimate tagged payload at arity ar. All of this existence data is propositionally truncated; no unique decomposition is asserted.

  Shaped : V ℓ → Type (ℓ-suc ℓ)
  Shaped c = ∥ Σ[ ar ∈ V ℓ ] Σ[ F ∈ V ℓ ] Σ[ p ∈ V ℓ ]
               (⟨ pr ar F ∈ Ev ⟩ × ((c ≡ pr ar p) × Key ar p)) ∥₁

For each c in the code set, outward reading first obtains a member q of E. Decomposing q gives ar and F with q ≡ pr ar F; the inner existential then gives p with c ≡ pr ar p and satisfaction of the ten-way payload formula.

  shape-out : ⟨ γ ⊨ shapeAt C w E N ⟩ → (c : S) → ⟨ fst c ∈ Cv ⟩ → Shaped (fst c)
  shape-out h c c∈ = PT.rec squash₁
    (λ { (q , (q∈ , hb)) → PT.rec squash₁
      (λ { (ar , F , s , (eq , hs)) → PT.map
        (λ { (p , s' , (ec , ht)) →

The equation q ≡ pr ar F transports the known membership of q in E to membership of pr ar F. The equation for c is retained, and the ten-way reader converts the remaining satisfaction proof into Key ar p.

          fst ar , fst F , fst p
          , ( subst (λ u → ⟨ u ∈ Ev ⟩) eq q∈
            , ( ec , TenRead.ten-out C w N (p ∷ s' ∷ F ∷ ar ∷ s ∷ q ∷ c ∷ γ) tg ht ) ) })
        (sndEx-out i4 i1 Sh.ten (F ∷ ar ∷ s ∷ q ∷ c ∷ γ) hs) })
      (bothEx-out i0 inner (q ∷ c ∷ γ) hb) })

The original shape satisfaction is universally quantified over members of the code set. Applying it to c and its membership proof supplies the existential data consumed above, completing the construction of Shaped (fst c).

    (h c c∈)

For the inward direction, assume that every member c of the code set has truncated shape data. Eliminating that truncation yields ar, F, and p, together with membership of pr ar F in E, the equation for c, and Key ar p; the target is itself a proposition, so this elimination is valid.

  shape-in : ((c : S) → ⟨ fst c ∈ Cv ⟩ → Shaped (fst c)) → ⟨ γ ⊨ shapeAt C w E N ⟩
  shape-in k c c∈ = PT.rec (snd ((c ∷ γ) ⊨ ∃̇∈ (var (sh  E)) (bothEx i0 inner)))
    (λ { (ar , F , p , (q∈ , (ec , key))) →
      let qS = down (lookup E γ) (pr ar F) q∈
          arS = fstS qS ar F refl

Membership of pr ar F in E supplies a set-level representative qS, whose two components represent ar and F. Separately, the equation c ≡ pr ar p selects a representative pS of the payload inside c. The two pairing containers provide the environments required by the nested existential formulas.

          FS = sndS qS ar F refl
          δ2 = qS ∷ c ∷ γ
          cq = container qS arS FS refl
          δ5 = FS ∷ arS ∷ cq .fst ∷ δ2
          pS = sndS c ar p ec

The inner formula is filled with the arity-table data, and the ten-way disjunction is filled with the key, so the full shape satisfaction is assembled from the honest data.

          cp = container c arS pS ec
          δ7 = pS ∷ cp .fst ∷ δ5
      in ∣ qS , ( q∈ , fillBoth i0 δ2 arS FS refl inner
            (fillSnd i4 δ5 arS pS ec Sh.ten
              (TenRead.ten-in C w N δ7 tg key) i1 refl) ) ∣₁ })

Applying the assumed shape assignment to c and its membership supplies precisely the truncated witnesses used by the inward construction. Together with the outward direction, this identifies satisfaction of the shape formula with the proposition Shaped for every member of the code set.

    (k c c∈)

The closure clauses are interpreted after a tower member has been decomposed as q ≡ pr ar F. In the resulting four-entry extension, A is the fixed arity ar; the code set and constant alphabet remain available from the ambient environment, and the tag equations remain valid after the shift.

module CloseRead {m : ℕ} (C w : Fin m) (N : Fin  → Fin m) (δ : S ^ ( + m)) (tg : Tags δ (shN  N)) where
  private
    Cv = fst (lookup (sh  C) δ)
    A = fst (lookup i1 δ)
    arS = lookup i1 δ

At this fixed arity, the closure conditions say that applying any of the ten constructors to inputs of the required shapes produces another member of the code set. For each clause, the outward and inward readings identify its bounded formula with the corresponding closure property.

    CS = lookup (sh  C) δ
    module Cl = Close C w N

Outward reading of an atomic closure clause permits arbitrary x from the bound selected by X and arbitrary y from the bound selected by Y in the environment extended by x. It then yields membership in the code set of the atomic key at arity A, with constructor tag k and term-form tags Nx and Ny.

  atomClose-out : (k Nx Ny : Fin ) (X : Fin ( + m)) (Y : Fin ( + m))
                → ⟨ δ ⊨ Cl.atomClose k Nx Ny X Y ⟩
                → (x y : S) → ⟨ fst x ∈ fst (lookup X δ) ⟩ → ⟨ fst y ∈ fst (lookup Y (x ∷ δ)) ⟩
                → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (pr (# (toℕ Ny)) (fst y)))) ∈ Cv ⟩
  atomClose-out k Nx Ny X Y h x y x∈ y∈ =

The membership is transported along the tag equations, which rename the three slots to the numerals of the three tags, since the clause is stated at the tagged slots but the key is spelled with the numerals.

    subst (λ u → ⟨ u ∈ Cv ⟩)
      (cong (pr A) (cong₂ pr (tg k) (cong₂ pr (cong (λ a → pr a (fst x)) (tg Nx)) (cong (λ a → pr a (fst y)) (tg Ny)))))
      (atomKey-out (sh  C) i3 (sh  (N k)) (sh  (N Nx)) i1 (sh  (N Ny)) i0 (y ∷ x ∷ δ) (h x x∈ y y∈))

The inward direction rebuilds the clause: given the property for all pairs, it suffices to instantiate it at the given x and y, with the naming equations run in reverse.

  atomClose-in : (k Nx Ny : Fin ) (X : Fin ( + m)) (Y : Fin ( + m))
               → ((x y : S) → ⟨ fst x ∈ fst (lookup X δ) ⟩ → ⟨ fst y ∈ fst (lookup Y (x ∷ δ)) ⟩
                  → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (pr (# (toℕ Ny)) (fst y)))) ∈ Cv ⟩)
               → ⟨ δ ⊨ Cl.atomClose k Nx Ny X Y ⟩
  atomClose-in k Nx Ny X Y g x x∈ y y∈ =

The membership is transported into the tagged slots by the reversed renamings, and the introduction rule of the closure clause finishes the case.

    atomKey-in (sh  C) i3 (sh  (N k)) (sh  (N Nx)) i1 (sh  (N Ny)) i0 (y ∷ x ∷ δ)
      (subst (λ u → ⟨ u ∈ Cv ⟩)
        (sym (cong (pr A) (cong₂ pr (tg k) (cong₂ pr (cong (λ a → pr a (fst x)) (tg Nx)) (cong (λ a → pr a (fst y)) (tg Ny))))))
        (g x y x∈ y∈))

The binary closure clause ranges over two members c₁ and c₂ of the code set. The equations fst c₁ ≡ pr A (fst a) and fst c₂ ≡ pr A (fst b) expose their payloads a and b at the fixed arity A; the clause then places the binary key with payload pr (fst a) (fst b) back in the code set.

  binClose-out : (k : Fin ) → ⟨ δ ⊨ Cl.binClose k ⟩
               → (c₁ c₂ a b : S) → ⟨ fst c₁ ∈ Cv ⟩ → ⟨ fst c₂ ∈ Cv ⟩
               → fst c₁ ≡ pr A (fst a) → fst c₂ ≡ pr A (fst b)
               → ⟨ pr A (pr (# (toℕ k)) (pr (fst a) (fst b))) ∈ Cv ⟩
  binClose-out k h c₁ c₂ a b c₁∈ c₂∈ e₁ e₂ =

The membership is transported along the tag renaming of the label, and the two nested universal layers are discharged by the elimination lemmas of the bounded quantifiers, each entry entering the inner clause through its own pairing container.

    subst (λ u → ⟨ u ∈ Cv ⟩) (cong (pr A) (cong (λ v → pr v (pr (fst a) (fst b))) (tg k)))
      (binKey-out (sh  C) i7 (sh  (N k)) i3 i0 δ10
        (useSnd i0 δ8 arS b e₂ (binKey (sh  C) i7 (sh  (N k)) i3 i0) i5 refl
          (useSnd i0 (c₁ ∷ δ) arS a e₁ inner i2 refl (h c₁ c₁∈) c₂ c₂∈)))
    where

After c₁ has been chosen and written as pr A a, the inner formula quantifies over a second code c₂ in the code set and exposes it as pr A b. It then requires the binary key formed from tag k and the paired payload pr a b; the auxiliary environments record the two decompositions of c₁ and c₂.

    inner : Formula S ( + m)
    inner = ∀̇∈ (var (sh  C)) (sndAll i0 i5 (binKey (sh  C) i7 (sh  (N k)) i3 i0))
    δ7 : S ^ ( + m)
    δ7 = a ∷ container c₁ arS a e₁ .fst ∷ c₁ ∷ δ
    δ8 : S ^ ( + m)

For the quantifier clauses, the environment must remember both a subkey and the data that determine its arity. The environment δ8 contains the candidate argument a, a proposed successor arity ar', the pair witnessing their relation, and the subkey c₁; δ10 adds the term used as the bound in a bounded quantifier.

    δ8 = c₂ ∷ δ7
    δ10 : S ^ ( + m)
    δ10 = b ∷ container c₂ arS b e₂ .fst ∷ δ8

The inward direction for a binary closure clause starts from its mathematical closure rule: two subkeys of the same arity that belong to the domain determine a composite key that also belongs to it. The two universal quantifiers merely make the chosen subkeys explicit.

  binClose-in : (k : Fin )
              → ((c₁ c₂ a b : S) → ⟨ fst c₁ ∈ Cv ⟩ → ⟨ fst c₂ ∈ Cv ⟩
                 → fst c₁ ≡ pr A (fst a) → fst c₂ ≡ pr A (fst b)
                 → ⟨ pr A (pr (# (toℕ k)) (pr (fst a) (fst b))) ∈ Cv ⟩)
              → ⟨ δ ⊨ Cl.binClose k ⟩

Introducing the two quantified components extends the environment in the order prescribed by the formula. At the innermost implication, the assumed closure rule gives membership of the composite key; the tag equation tg k identifies its displayed tag with the numeral required by binKey.

  binClose-in k g c₁ c₁∈ = sndAll-in i0 i2 (∀̇∈ (var (sh  C)) (sndAll i0 i5 (binKey (sh  C) i7 (sh  (N k)) i3 i0))) (c₁ ∷ δ) (λ a s s∈ a∈ e₁ c₂ c₂∈ →
    sndAll-in i0 i5 (binKey (sh  C) i7 (sh  (N k)) i3 i0) (c₂ ∷ a ∷ s ∷ c₁ ∷ δ) (λ b s' s'∈ b∈ e₂ →
      binKey-in (sh  C) i7 (sh  (N k)) i3 i0 (b ∷ s' ∷ c₂ ∷ a ∷ s ∷ c₁ ∷ δ)
        (subst (λ u → ⟨ u ∈ Cv ⟩) (sym (cong (pr A) (cong (λ v → pr v (pr (fst a) (fst b))) (tg k))))
          (g c₁ c₂ a b c₁∈ c₂∈ e₁ e₂))))

For falsity there is no subordinate code to inspect. Reading its closure clause outward therefore reduces to the equation identifying the payload with the zero numeral, followed by transport along the tag equations.

  conClose-out : (k : Fin ) → ⟨ δ ⊨ Cl.conClose k ⟩ → ⟨ pr A (pr (# (toℕ k)) (# )) ∈ Cv ⟩
  conClose-out k h =
    subst (λ u → ⟨ u ∈ Cv ⟩) (cong (pr A) (cong₂ pr (tg k) (tg f0)))
      (unKey-out (sh  C) i1 (sh  (N k)) (sh  (N f0)) δ h)

Conversely, membership of the falsity key is transported back along the same equations to satisfy the closure clause. This case has no recursive premise: the zero payload completely determines the key.

  conClose-in : (k : Fin ) → ⟨ pr A (pr (# (toℕ k)) (# )) ∈ Cv ⟩ → ⟨ δ ⊨ Cl.conClose k ⟩
  conClose-in k h =
    unKey-in (sh  C) i1 (sh  (N k)) (sh  (N f0)) δ
      (subst (λ u → ⟨ u ∈ Cv ⟩) (sym (cong (pr A) (cong₂ pr (tg k) (tg f0)))) h)

The unbounded-quantifier clause is read outward with the quantified components explicit: given a subkey c₁ of the domain, a presentation c₁ = pr ar' a, and the equation ar' = sucV A, the quantifier key at the current arity belongs to the domain. The three hypotheses are exactly the data of a predecessor slice member.

  quClose-out : (k : Fin ) → ⟨ δ ⊨ Cl.quClose k ⟩
              → (c₁ ar' a : S) → ⟨ fst c₁ ∈ Cv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
              → ⟨ pr A (pr (# (toℕ k)) (fst a)) ∈ Cv ⟩
  quClose-out k h c₁ ar' a c₁∈ e₁ es =
    subst (λ u → ⟨ u ∈ Cv ⟩) (cong (pr A) (cong (λ v → pr v (fst a)) (tg k)))

The proof extends the environment by a, ar', and the container, opens the implication with the successor equation, and reads the unKey membership in the eight-slot environment. Transport along the tag equation then gives membership for the numeral represented by tag k.

      (unKey-out (sh  C) i5 (sh  (N k)) i0 δ8
        (useBoth i0 (c₁ ∷ δ) ar' a e₁ (sucAtL i5 i1 ⇒̇ unKey (sh  C) i5 (sh  (N k)) i0) (h c₁ c₁∈)
          (suc-in i5 i1 δ8 es)))
    where
    δ8 : S ^ ( + m)

The extended environment packages the three quantified components with the original one, in the order the implication reads them.

    δ8 = a ∷ ar' ∷ container c₁ ar' a e₁ .fst ∷ c₁ ∷ δ

For the inward direction, introduce the two quantified components of the clause. The extended environment contains the proposed successor arity ar' and the payload a; the successor equation then supplies the premise of the implication.

  quClose-in : (k : Fin )
             → ((c₁ ar' a : S) → ⟨ fst c₁ ∈ Cv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
                → ⟨ pr A (pr (# (toℕ k)) (fst a)) ∈ Cv ⟩)
             → ⟨ δ ⊨ Cl.quClose k ⟩
  quClose-in k g c₁ c₁∈ = bothAll-in i0 (sucAtL i5 i1 ⇒̇ unKey (sh  C) i5 (sh  (N k)) i0) (c₁ ∷ δ) (λ ar' a s s∈ ar'∈ a∈ e₁ hs →

Apply the assumed closure rule to these data, then transport the resulting membership along the tag equation to obtain the unKey conclusion. This completes the inward reading of the unbounded-quantifier clause.

    unKey-in (sh  C) i5 (sh  (N k)) i0 (a ∷ ar' ∷ s ∷ c₁ ∷ δ)
      (subst (λ u → ⟨ u ∈ Cv ⟩) (sym (cong (pr A) (cong (λ v → pr v (fst a)) (tg k))))
        (g c₁ ar' a c₁∈ e₁ (suc-out i5 i1 (a ∷ ar' ∷ s ∷ c₁ ∷ δ) hs))))

The bounded-quantifier clause has one additional premise. Besides a body key at the successor arity, it requires a legal bounding term x at the current arity; the resulting payload records the quantifier tag, the term tag Nx, the term itself, and the body payload as nested pairs.

  bqClose-out : (k Nx : Fin ) (X : Fin ( + m)) → ⟨ δ ⊨ Cl.bqClose k Nx X ⟩
              → (c₁ ar' a : S) → ⟨ fst c₁ ∈ Cv ⟩ → (e₁ : fst c₁ ≡ pr (fst ar') (fst a)) → fst ar' ≡ sucV A
              → (x : S) → ⟨ fst x ∈ fst (lookup X (a ∷ ar' ∷ container c₁ ar' a e₁ .fst ∷ c₁ ∷ δ)) ⟩
              → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (fst a))) ∈ Cv ⟩
  bqClose-out k Nx X h c₁ ar' a c₁∈ e₁ es x x∈ =

The proof extends the environment by the bounding term and applies bounded-key elimination there. The two tag equations, one for the quantifier constructor and one for the term constructor, transport the nested pair to the shape named in the conclusion.

    subst (λ u → ⟨ u ∈ Cv ⟩)
      (cong (pr A) (cong₂ pr (tg k) (cong (λ v → pr v (fst a)) (cong (λ v → pr v (fst x)) (tg Nx)))))
      (bndKey-out (sh  C) i6 (sh  (N k)) (sh  (N Nx)) i0 i1 (x ∷ δ8)
        (useBoth i0 (c₁ ∷ δ) ar' a e₁ (sucAtL i5 i1 ⇒̇ ∀̇∈ (var X) (bndKey (sh  C) i6 (sh  (N k)) (sh  (N Nx)) i0 i1))
          (h c₁ c₁∈) (suc-in i5 i1 δ8 es) x x∈))

The eight-slot environment repeats the packaging used by the unbounded case, with the bound slot consumed by the elimination.

    where
    δ8 : S ^ ( + m)
    δ8 = a ∷ ar' ∷ container c₁ ar' a e₁ .fst ∷ c₁ ∷ δ

For the inward direction, assume the mathematical closure rule displayed in the type. It is quantified over an arbitrary extended environment s, because the set from which the bounding term is chosen is evaluated in that environment.

  bqClose-in : (k Nx : Fin ) (X : Fin ( + m))
             → ((c₁ ar' a s : S) → ⟨ fst c₁ ∈ Cv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
                → (x : S) → ⟨ fst x ∈ fst (lookup X (a ∷ ar' ∷ s ∷ c₁ ∷ δ)) ⟩
                → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (fst a))) ∈ Cv ⟩)
             → ⟨ δ ⊨ Cl.bqClose k Nx X ⟩

Introduce the quantified subkey data and the bounding term, then apply the assumed closure rule in the resulting environment. Transport along the two tag equations turns its conclusion into the membership required by bndKey, completing the inward reading of the bounded-quantifier clause.

  bqClose-in k Nx X g c₁ c₁∈ = bothAll-in i0 (sucAtL i5 i1 ⇒̇ ∀̇∈ (var X) (bndKey (sh  C) i6 (sh  (N k)) (sh  (N Nx)) i0 i1)) (c₁ ∷ δ) (λ ar' a s s∈ ar'∈ a∈ e₁ hs x x∈ →
    bndKey-in (sh  C) i6 (sh  (N k)) (sh  (N Nx)) i0 i1 (x ∷ a ∷ ar' ∷ s ∷ c₁ ∷ δ)
      (subst (λ u → ⟨ u ∈ Cv ⟩)
        (sym (cong (pr A) (cong₂ pr (tg k) (cong (λ v → pr v (fst a)) (cong (λ v → pr v (fst x)) (tg Nx))))))
        (g c₁ ar' a s c₁∈ e₁ (suc-out i5 i1 (a ∷ ar' ∷ s ∷ c₁ ∷ δ) hs) x x∈)))

Soundness: decoding every member

To prove soundness, we now connect three descriptions already available: numerical tags identify the ten constructors, shape and closure formulas describe their internal set codes, and AllCodes relates those codes back to the external formula grammar. Propositionality will allow truncated witnesses to be eliminated without choosing representatives.

open import L.Coding.Expressions {ℓ} using ( tagAtL-adequate )
open import L.Coding.Closure {ℓ} using ( closedAt; binSameClosed-in; unSuccClosed-in; binSuccClosed-in )
open import L.Coding.CodeShape {ℓ} using
  ( shapedAt; shaped-in; ShapeWit; BinWit; bothTm; fstTm; noneB; isTmAt )
open import L.Coding.CodeSet {ℓ} lem using

The canonical code set provides both directions of this comparison: a member can be read as a formula key, and every formula has a canonical key. The remaining imports supply the witnesses for recorded arities and the fact that conjunctions of propositions are again propositions.

  ( AllCodes; AllCodes-out; key∈AllCodes; keyS; codeS; witnessAt-out )
open import Cubical.Foundations.HLevels using ( isProp× )

Fix a working set Wv, whose elements may occur as constants, and a candidate code domain Cv. The following argument is parametric in these two sets; no assumption yet identifies Cv with the canonical domain AllCodes.

module _ (Wv Cv : V ℓ) where
  open CodesSem Wv Cv

Every payload condition PayN n ar r is a proposition. For tags zero through four this follows immediately from propositional truncation: the condition asserts only that suitable components merely exist.

  isPropPayN : (n : ℕ) (ar r : V ℓ) → isProp (PayN n ar r)
  isPropPayN  ar r = squash₁
  isPropPayN  ar r = squash₁
  isPropPayN  ar r = squash₁
  isPropPayN  ar r = squash₁

The remaining constructor tags use the same principle in the form appropriate to their payloads. Falsity has a unique zero payload; unbounded quantifiers require membership in Cv, which is proposition-valued; bounded quantifiers again use truncated existence.

  isPropPayN  ar r = squash₁
  isPropPayN  ar r = setIsSet r (# )
  isPropPayN  ar r = snd (pr (sucV ar) r ∈ Cv)
  isPropPayN  ar r = snd (pr (sucV ar) r ∈ Cv)
  isPropPayN  ar r = squash₁

Tag nine is handled by truncated existence as well. Any numeral beyond the ten constructor tags has an empty payload type, and an empty type is a proposition. Thus PayN is proposition-valued for every natural-number tag.

  isPropPayN  ar r = squash₁
  isPropPayN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) ar r = Empty.isProp⊥*

The key-alignment lemma converts a Key at arity ar into a payload at any other decomposition p = (# n, r) of the same set. Pair injectivity and numeral injectivity align the tag and the payload separately, and because PayN n ar r is a proposition, the truncated key may be eliminated into it.

  keyAt : (ar p : V ℓ) → Key ar p → (n : ℕ) (r : V ℓ) → p ≡ pr (# n) r → PayN n ar r
  keyAt ar p key n r e = PT.rec (isPropPayN n ar r)
    (λ { (k , r' , (e' , pay)) →
      let q = pr-inj (sym e ∙ e')
      in subst2 (λ j x → PayN j ar x) (sym (#-inj′ (q .fst))) (sym (q .snd)) pay })

Applying this elimination to key completes the alignment: the tag and payload obtained from Key have already been transported to the prescribed numeral n and payload r.

    key

The first recovery lemma converts a term-code statement into a satisfaction of the shape chapter's term predicate. It is stated for arbitrary slots and proved by eliminating the truncated IsTmV into the proposition-valued satisfaction.

tmWit : ∀ {j} (ti Ni Ai : Fin j) (env : S ^ j)
      → IsTmV (fst (lookup Ai env)) (fst (lookup ti env)) (fst (lookup Ni env))
      → ⟨ env ⊨ isTmAt ti Ni Ai ⟩
tmWit ti Ni Ai env = PT.rec (snd (env ⊨ isTmAt ti Ni Ai))
  (λ { (inl (x , (e , x∈))) →

In the constant branch, down presents the witness x as an element of the working set Wv. Tag adequacy transports the pair equation, while the original membership proof supplies the other conjunct. The resulting evidence enters the left disjunct of the shape predicate.

         ∣ inl ∣ down (lookup Ai env) x x∈
           , ( subst ⟨_⟩ (sym (tagAtL-adequate (suc ti)  zero (down (lookup Ai env) x x∈ ∷ env))) e
             , x∈ ) ∣₁ ∣₁
     ; (inr (i , (e , i∈))) →
         ∣ inr ∣ down (lookup Ni env) i i∈