Subcode-closed domains

A domain of formula codes is closed under immediate subformula codes when every constructor key it contains brings along the formula subcodes that its constructor demands; the atomic constructors and bottom carry no such obligations, since their term and numeral components are not demands of closedAt. This chapter explains why such a demand is needed and what it says. The subcode clauses of L.Coding.Expressions constrain a table only where the codes they consult actually carry entries, so a table satisfying all ten of them can be almost empty; what pins a value is a property of the index set itself, and the closure predicate closedAt states exactly that property as a single object-language formula. The chapter builds the predicate from two quantifier frames, one for binary and one for unary constructors, instantiates three payload relations to obtain its seven clauses, and proves both directions between satisfaction of those clauses and meta-level closure data: eliminations that read a satisfied clause into the subcodes it demands, and introductions that assemble satisfaction from such membership data. Once available, closedAt supports structural induction over codes stored inside L.

The chapter begins with a defect in what the coding clauses already say. In L.Coding.Expressions, each compound constructor came with a clause tying a table's entry at a code to entries at its immediate subcodes. Such a clause constrains a table only where the codes it consults actually carry entries, so a table can satisfy all ten clauses while being almost empty: take the index set to be a single compound code, put one entry there with any value at all, and every clause that looks for an entry at a subcode goes vacuous, since the subcodes carry no entry. The clauses alone do not pin a value. What pins it is a demand on the index set itself, that it contain the immediate subformula codes of each of its members. That demand, stated as a formula of the object language, is the closure predicate closedAt built in this chapter.

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

open import Base.Prelude

The counterexample also shows what would go wrong without repair. The entry sits at a compound code, and closure is precisely the property the empty subcodes cannot fake: if the index set contains a compound code, it must contain the subcodes that code decodes into. Compound matters here. Put the single entry at the code of the bottom formula ⊥̇ instead, and the clause for ⊥̇ pins the value outright, because that clause makes no subcode lookup at all. That small failure is the shape of the whole argument in miniature.

module L.Coding.Closure {ℓ : Level} where

The repair is a quantifier pattern, and it needs the same two frames as the clauses, minus the table. What remains is the shape reader and the implication: for every key of that shape in the set, such and such keys are in the set too. A key is an arity paired with a code, so a subkey is built either from the same arity, or from its successor for the four constructors that bind a variable. The bounded universal ranges over members of the set, the further universals range over the decoded parts, and the implication guards the demand behind the shape check.

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; _∧̇_; _⇒̇_; ∀̇_; ∀̇∈; ∃̇_ )

The demands split into two shapes. The three binary connectives each contribute two formula children at the same arity; the two unbounded quantifiers contribute one child at the successor arity, and the two bounded quantifiers follow only their second, formula component at that same higher level, because their first component is a term. That gives seven constructors with an obligation. The two atoms and bottom add none: their term and numeral components are not obligations of closedAt, and bottom is pinned by its own clause as in the counterexample.

import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Axioms.Numerals {ℓ} using ( sucʟ; sucʟ-fst )

A relation to state in a frame is a parameter, and the seven concrete clauses arise by instantiating that parameter. Three instantiations cover the classification above: a same-arity demand for both components, a same-arity demand for one component, and a successor-arity demand in which the higher arity is supplied existentially. Each is a plain object-language formula over the extended environment that the frame itself opens.

open import Cubical.Data.Nat using ( _+_ )

The existentially supplied successor is the one place where mere existence appears. Inside the arity-raising relations, the bound variable is witnessed to be the successor of the frame's arity, and that witness is packaged only truncated: the proposition records existence without retaining a chosen witness as data. Later the readers of these clauses discharge the truncation, which is legitimate because the membership claims they feed are propositions.

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )

Everything is stated at the level of sets and membership. A code stored in L is read as an element of the cumulative hierarchy; the subcode demand is literally a list of membership statements, a pair pr pairing an arity with a payload being a member of the domain set. This is what makes the predicate transportable: satisfaction of an object-language formula about membership, nothing more.

open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; sucV )

The formulas are evaluated over the carrier S of L, in an environment γ : S ^ n of n carriers for a formula of arity n. Satisfaction here means satisfaction in the restricted structure over L; the satisfaction relation of the ambient hierarchy is kept under a separate name, so the two readings never blur. The frames extend such an environment by the slots they bind, which is why their arities are shifted sums like 4 + n.

open hPropStructure 𝒮ʟ using ( S )

Inside an extended environment, each frame names its own slots by de Bruijn indices counted from the inside out. The binary frame binds four slots, payload, payload, arity, code, so its code sits at the outermost index; the unary frame binds three. Shifting maps push the ambient variables of the original n past the bound slots, so a variable that named a value outside the frame still names that same value inside the quantified body.

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

Four object-language readers supply the building blocks, each with an adequacy proof equating its satisfaction with the meta-level claim it reads. One reads membership in the set stored at an environment slot; two check that a code is the tagged pair of an arity with its one or two payload components; one expresses having the successor of a stored arity as a payload. With shape, membership, and successor all readable inside the object language, the whole closure demand collapses into one formula, and the rest of the chapter unfolds what that formula says and how to satisfy it.

open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate )
open import L.Coding.Expressions {ℓ}
  using ( arityTagAtL; arityTagAtL-adequate; arityTagPairAtL; arityTagPairAtL-adequate
        ; sucAtL; sucAtL-adequate )

A domain that is closed under subcodes

The closure demand of the previous section is a quantified statement about decoded keys, and this section builds the two formulas that express it. The only classification needed is by shape: a decoded key of a unary constructor exhibits three witnesses, the code, the arity, and one payload component, while a decoded key of a binary constructor exhibits a fourth, the second component. A frame quantifying over a decoded key therefore quantifies over three values in the unary case and four in the binary case, and the obligations of the seven active constructors attach to these two frames.

The closure demand to be formalized is a quantified statement about decoded keys. Fix an index C and let Cset be the set stored there. It reads: for every code c in Cset, if c decodes as an arity ar tagged with the constructor numeral k and carrying payload components, then a relation rel holds of those data. How many payload components there are depends on the constructor's shape. A decoded key of a unary constructor exhibits three witnesses, the code, the arity, and one component; a decoded key of a binary constructor exhibits four, adding the second component. So two frames are needed, one quantifying three values and one quantifying four.

module _ {n : ℕ} where

Both frames live at an ambient free-variable count n: they quantify inside an environment of length n and extend it by the slots they bind themselves, four for the binary frame and three for the unary one. An ambient variable must survive this extension unchanged, so a shift like sh4 sends each of the n indices past the freshly bound slots. Inside the quantified body it then names the same value it named outside.

  private
    sh4 : Fin n → Fin ( + n)
    sh4 i = suc (suc (suc (suc i)))

Inside the extended environment the frame's own values must be addressable, and de Bruijn numbering does this with the innermost variable at 0. For the binary frame that puts the two payload components at the two innermost slots, the arity next, and the code outermost of the four. These four names are what let the frame's body point at exactly the value playing each role, however deeply the frame is nested.

    c4 n4 a4 b4 : Fin ( + n)
    c4 = suc (suc (suc zero))
    n4 = suc (suc zero)
    a4 = suc zero
    b4 = zero

The unary frame binds one slot fewer, so its shift moves ambient variables past three slots instead of four; everything else about the extension is the same.

    sh3 : Fin n → Fin ( + n)
    sh3 i = suc (suc (suc i))

Its three bound slots follow the same inside-out order: the single payload component innermost, then the arity, then the code. With both frames fixed once, every clause built on the binary shape reuses the four-slot layout and every clause built on the unary shape reuses the three-slot layout, so the quantifier structure of the closure statement is written down twice in total.

    c3 n3 a3 : Fin ( + n)
    c3 = suc (suc zero)
    n3 = suc zero
    a3 = zero

binShapeAt is the binary frame itself, the closure demand minus any table. Its quantifier structure is exact: a bounded universal first chooses c from the domain C, then three further values ar, a, and b are quantified; under the hypothesis that the pair reader certifies c to be the tagged pair of arity ar with tag k and payload a, b, the relation rel must hold in the extended environment b ∷ a ∷ ar ∷ c ∷ γ. The relation is a parameter, so each clause instantiates the same frame with its own payload demand.

  binShapeAt : Fin n → ℕ → Formula S ( + n) → Formula S n
  binShapeAt C k rel =
    ∀̇∈ (var C) (∀̇ (∀̇ (∀̇ ( arityTagPairAtL c4 n4 k a4 b4 ⇒̇ rel))))

unShapeAt is the same frame for unary constructors: one payload component instead of two, hence one fewer bound slot, and the shape reader arityTagAtL in place of the pair version. Everything else, the bounded universal over the domain and the implication into rel, is identical.

  unShapeAt : Fin n → ℕ → Formula S ( + n) → Formula S n
  unShapeAt C k rel =
    ∀̇∈ (var C) (∀̇ (∀̇ ( arityTagAtL c3 n3 k a3 ⇒̇ rel)))

binShape-out is the elimination direction for the binary frame. Its type takes a proof that the environment γ satisfies the frame for an arbitrary relation rel, then the chosen code c with arity ar and components a, b, together with the membership hypothesis that c belongs to the domain.

  binShape-out : (C : Fin n) (k : ℕ) (rel : Formula S ( + n)) (γ : S ^ n)
    → ⟨ γ ⊨ binShapeAt C k rel ⟩
    → (c ar a b : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩

The remaining hypothesis is the shape equation saying that c really is the tagged pair ar with tag k and payload a, b. Under these hypotheses the conclusion is the instance of rel in the extended environment, where the bound slots are filled with exactly those values in the order b ∷ a ∷ ar ∷ c ∷ γ.

    → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
    → ⟨ (b ∷ a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩

The proof is short because the frame was designed for this reading. The hypothesis h is a function, and applying it at c with membership and shape produces what is wanted, except that the shape argument must be transported along the adequacy path for arityTagPairAtL in the extended environment: adequacy is stated as a path between propositions, and subst along it moves the proof to the form the conclusion needs.

  binShape-out C k rel γ h c ar a b c∈ shape =
    h c c∈ ar a b
      (subst ⟨_⟩ (sym (arityTagPairAtL-adequate c4 n4 k a4 b4 (b ∷ a ∷ ar ∷ c ∷ γ)))
        shape)

unShape-out is the same elimination for the unary frame. It takes satisfaction of unShapeAt C k rel in γ, a code c with a single payload component a and arity ar, and the membership hypothesis for c.

  unShape-out : (C : Fin n) (k : ℕ) (rel : Formula S ( + n)) (γ : S ^ n)
    → ⟨ γ ⊨ unShapeAt C k rel ⟩
    → (c ar a : S)

The shape equation reads c as the tagged pair ar with tag k and single payload a, checked through the unary shape reader arityTagAtL. The conclusion then lives in the shorter extended environment a ∷ ar ∷ c ∷ γ, whose bound slots are filled with exactly those values.

    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (fst a))
    → ⟨ (a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩

As with the binary case, the proof applies the frame's function at the chosen components and transports the shape proof along the adequacy path for arityTagAtL. These two eliminations are all a consumer needs: the seven concrete closure clauses below are obtained from them by instantiating the relation.

  unShape-out C k rel γ h c ar a c∈ shape =
    h c c∈ ar a
      (subst ⟨_⟩ (sym (arityTagAtL-adequate c3 n3 k a3 (a ∷ ar ∷ c ∷ γ))) shape)

Four generic relations cover the payload shapes. The seven active closure clauses use three of them: the three binary connectives require both components at the current arity; the two unbounded quantifiers require their single component one arity higher, with the successor supplied existentially; and the two bounded quantifiers require only their second component at that same higher level, because the first component is a term.

The two arity-preserving relations are plain conjunctions of subcode membership. Given the four fresh entries of a binary frame, bothSameAt C asserts that both subformula slots, named by the indices a4 and b4, already belong to the set that entry sh4 C points to. Its unary counterpart oneSameAt C is a single such membership claim over the three fresh entries of a unary frame, for constructors whose sole component lives at the same arity.

  bothSameAt : Fin n → Formula S ( + n)
  bothSameAt C = appAt (sh4 C) n4 a4 ∧̇ appAt (sh4 C) n4 b4

  oneSameAt : Fin n → Formula S ( + n)
  oneSameAt C = appAt (sh3 C) n3 a3

  oneSuccAt : Fin n → Formula S ( + n)

The two arity-raising relations quantify the successor existentially. The bound variable at position zero is witnessed to be the successor sucV of the frame's arity, via sucAtL, and the same witness is required to pair with the component slot, now shifted to suc a3 or suc b4 inside the extended environment. For succSndAt the pair mentions only b4, the second slot, since for the bounded quantifiers the first slot of the binary key carries a term rather than a subformula.

  oneSuccAt C = ∃̇ (sucAtL (suc n3) zero ∧̇ appAt (suc (sh3 C)) zero (suc a3))

  succSndAt : Fin n → Formula S ( + n)
  succSndAt C = ∃̇ (sucAtL (suc n4) zero ∧̇ appAt (suc (sh4 C)) zero (suc b4))

Reading them back is what a consumer does, so each is stated at the clause, already composed with its frame: given a key of that shape in the set, the keys the constructor demands are in the set. The two that change arity discharge a truncation on the way, which the target admits because membership is a proposition.

Four readings unfold the clauses back into concrete membership data, one per payload shape. The first handles the binary connectives at the same arity. Its input is a satisfaction proof of the full clause binShapeAt C k (bothSameAt C), together with a key of the right shape: model elements c, ar, a, b, membership of c in the set at C, and the shape equation presenting c as the ordered pair of the arity ar with the coded application to a and b.

  binSameClosed-out : (C : Fin n) (k : ℕ) (γ : S ^ n)
    → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩
    → (c ar a b : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))

Its conclusion is the conjunction the constructor demands: both subformula keys, the pairs of the same arity ar with a and with b, are members of the set. The proof runs the generic frame elimination and then applies adequacy, which converts a satisfaction statement about the coded membership reader into the plain membership claim it means; this conversion is the one proof step shared by all four readings.

    → ⟨ pr (fst ar) (fst a) ∈ fst (lookup C γ) ⟩
    × ⟨ pr (fst ar) (fst b) ∈ fst (lookup C γ) ⟩
  binSameClosed-out C k γ h c ar a b c∈ shape =
      subst ⟨_⟩ (appAt-adequate (sh4 C) n4 a4 δ) (r .fst)
    , subst ⟨_⟩ (appAt-adequate (sh4 C) n4 b4 δ) (r .snd)

The second reading covers the unary constructors at the same arity. Its hypotheses mirror the first with one component fewer: a satisfaction proof of the clause built from oneSameAt, the key's parts c, ar, a, membership of c, and the shape equation presenting c as the pair of the arity ar with the coded numeral k applied to a alone.

    where
    δ : S ^ ( + n)
    δ = b ∷ a ∷ ar ∷ c ∷ γ
    r = binShape-out C k (bothSameAt C) γ h c ar a b c∈ shape

  unSameClosed-out : (C : Fin n) (k : ℕ) (γ : S ^ n)

The conclusion is a single membership, of the pair of ar with a. Since oneSameAt never raised the arity, no truncation appears, and the proof is just the unary frame elimination followed by the adequacy conversion. The third reading turns to the successor arity: unSuccClosed-out reads the clause built from oneSuccAt.

    → ⟨ γ ⊨ unShapeAt C k (oneSameAt C) ⟩
    → (c ar a : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (fst a))
    → ⟨ pr (fst ar) (fst a) ∈ fst (lookup C γ) ⟩

Its hypotheses match the previous unary reading, but the conclusion names the successor: the required subformula key pairs a with sucV (fst ar), the successor of the key's arity, not with ar itself. This fits the unbounded quantifiers, which bind a variable and so store their body one arity higher. The next three paragraphs explain how the existential witness and its adequacy proofs establish this conclusion.

  unSameClosed-out C k γ h c ar a c∈ shape =
    subst ⟨_⟩ (appAt-adequate (sh3 C) n3 a3 (a ∷ ar ∷ c ∷ γ))
      (unShape-out C k (oneSameAt C) γ h c ar a c∈ shape)

  unSuccClosed-out : (C : Fin n) (k : ℕ) (γ : S ^ n)
    → ⟨ γ ⊨ unShapeAt C k (oneSuccAt C) ⟩

The third reading, for the unbounded quantifiers, raises the arity. Its hypotheses are the usual unary ones: satisfaction of unShapeAt C k (oneSuccAt C), the key's parts c, ar, a, membership of c, and the shape equation. The conclusion replaces the arity ar by its successor: the required subformula key pairs a with sucV (fst ar), the successor of the key's arity, not with ar itself. This is the reading appropriate to the unbounded quantifiers, which bind a variable and so store their body one arity higher.

    → (c ar a : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (fst a))
    → ⟨ pr (sucV (fst ar)) (fst a) ∈ fst (lookup C γ) ⟩
  unSuccClosed-out C k γ h c ar a c∈ shape =

This is where the existential inside oneSuccAt matters. The successor is demanded only merely: the frame elimination hands over a propositionally truncated witness, together with certificates that it is the successor of the arity and that it pairs with a into the set. Such a truncation may be eliminated here because the goal is a proposition: membership in a set is an hProp, so PT.rec converts the mere existence into the concrete membership claim without choosing a canonical witness.

    PT.rec (snd target)
      (λ { (z , (sz , ap)) →
        subst (λ w → ⟨ pr w (fst a) ∈ fst (lookup C γ) ⟩)
          (subst ⟨_⟩ (sucAtL-adequate (suc n3) zero (z ∷ δ)) sz)
          (subst ⟨_⟩ (appAt-adequate (suc (sh3 C)) zero (suc a3) (z ∷ δ)) ap) })

The adequacy lemmas of the two readers then turn those satisfactions into equations and memberships about the actual model values, and the transport along the first equation re-expresses the membership at the witness as membership at sucV (fst ar). So the reading ends exactly where it should: with the membership of the successor key.

      (unShape-out C k (oneSuccAt C) γ h c ar a c∈ shape)
    where
    δ : S ^ ( + n)
    δ = a ∷ ar ∷ c ∷ γ
    target = pr (sucV (fst ar)) (fst a) ∈ fst (lookup C γ)

The fourth reading covers the bounded quantifiers. Its hypotheses copy the binary pattern: satisfaction of binShapeAt C k (succSndAt C), the four model values c, ar, a, b, membership of c, and the shape equation presenting c as the pair of ar with the coded application to a, b.

  binSuccClosed-out : (C : Fin n) (k : ℕ) (γ : S ^ n)
    → ⟨ γ ⊨ binShapeAt C k (succSndAt C) ⟩
    → (c ar a b : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))

The conclusion asks only about the second component: sucV (fst ar) paired with b must be in the set, since the first slot carries the bounding term rather than a subformula. As in the unbounded case, the existential inside succSndAt supplies the successor merely, and the elimination of that truncation is legitimate because the membership target is a proposition.

    → ⟨ pr (sucV (fst ar)) (fst b) ∈ fst (lookup C γ) ⟩
  binSuccClosed-out C k γ h c ar a b c∈ shape =
    PT.rec (snd target)
      (λ { (z , (sz , ap)) →
        subst (λ w → ⟨ pr w (fst b) ∈ fst (lookup C γ) ⟩)

The proof body is the binary counterpart of the previous one: the two certificates are converted by sucAtL-adequate and appAt-adequate, and the transport along the successor equation re-expresses the pairing membership at sucV (fst ar).

          (subst ⟨_⟩ (sucAtL-adequate (suc n4) zero (z ∷ δ)) sz)
          (subst ⟨_⟩ (appAt-adequate (suc (sh4 C)) zero (suc b4) (z ∷ δ)) ap) })
      (binShape-out C k (succSndAt C) γ h c ar a b c∈ shape)
    where
    δ : S ^ ( + n)

The propositionhood of the membership conclusion is what licenses the truncation elimination in each successor-arity reading. These four readings, in two same-arity and two successor-arity forms, are all a consumer needs: every closure clause can be unfolded into concrete membership data.

    δ = b ∷ a ∷ ar ∷ c ∷ γ
    target = pr (sucV (fst ar)) (fst b) ∈ fst (lookup C γ)

The seven clauses, and their conjunction. On the elimination side, a consumer reading a satisfied closedAt conjunction selects the clause it wants and applies the reader that goes with it. The introduction directions appear in the next section.

The seven clause names are declared first, all of the same type: at each index C they are formulas over the n-environment, at the very arity of the key stored there. No environment extension appears in their types, since each frame is applied internally with its freshly shifted indices.

  andClosedAt orClosedAt impClosedAt : Fin n → Formula S n
  existClosedAt forallClosedAt allInClosedAt exInClosedAt : Fin n → Formula S n

  andClosedAt    C = binShapeAt C  (bothSameAt C)
  orClosedAt     C = binShapeAt C  (bothSameAt C)
  impClosedAt    C = binShapeAt C  (bothSameAt C)

Each definition pairs a constructor key with the right relation: the numerals 2, 3, 4 are the binary connectives, whose clauses use bothSameAt; 6 and 7 are the unbounded quantifiers, using oneSuccAt; and 8 and 9 are the bounded quantifiers, using succSndAt. The frame binShapeAt or unShapeAt is chosen according to whether the constructor's code carries two payload components or one: the binary connectives and the bounded quantifiers have two and so use binShapeAt, while the unbounded quantifiers have one and use unShapeAt. Quantifier bodies live at the successor arity, and for the bounded quantifiers only the second payload component is a formula, which is why their relation follows only that component.

  existClosedAt  C = unShapeAt  C  (oneSuccAt C)
  forallClosedAt C = unShapeAt  C  (oneSuccAt C)
  allInClosedAt  C = binShapeAt C  (succSndAt C)
  exInClosedAt   C = binShapeAt C  (succSndAt C)

  closedAt : Fin n → Formula S n

closedAt C conjoins all seven clauses at the single index C. This is the object-language predicate later transported into L: a set is subcode closed at C when this conjunction is satisfied, and structural induction over codes then proceeds conjunct by conjunct, each with its own reader.

  closedAt C =
    andClosedAt C ∧̇ (orClosedAt C ∧̇ (impClosedAt C ∧̇ (existClosedAt C
      ∧̇ (forallClosedAt C ∧̇ (allInClosedAt C ∧̇ exInClosedAt C)))))

The converse starts from actual meta-level subcode closure and turns it into satisfaction of each object-language frame. For same-arity clauses, the supplied membership facts directly establish the required payload memberships. For arity-raising clauses, the L-numeral sucʟ ar supplies the existential successor witness together with the equations and membership certificate that the frame demands.

The introduction direction answers the converse need: given meta-level closure data, produce satisfaction of the clause. For the binary frame, binShape-in takes a function g which, from a key's parts c, ar, a, b, membership of c, and the shape equation, returns satisfaction of the arbitrary relation rel in the extended environment; it concludes satisfaction of the whole shape binShapeAt C k rel.

  binShape-in : (C : Fin n) (k : ℕ) (rel : Formula S ( + n)) (γ : S ^ n)
    → ((c ar a b : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
       → ⟨ (b ∷ a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩)

This is the semantic content of the quantifiers read backward: satisfaction of a bounded universal is a function defined on members of the set, and satisfaction of an implication is a function on the proof of its premise. So g applied to the key's data is already the required satisfaction; the only conversion is along arityTagPairAtL-adequate, aligning the tag equation the frame reads with the shape equation g was handed.

    → ⟨ γ ⊨ binShapeAt C k rel ⟩
  binShape-in C k rel γ g c c∈ ar a b sh =
    g c ar a b c∈
      (subst ⟨_⟩ (arityTagPairAtL-adequate c4 n4 k a4 b4 (b ∷ a ∷ ar ∷ c ∷ γ)) sh)

  unShape-in : (C : Fin n) (k : ℕ) (rel : Formula S ( + n)) (γ : S ^ n)

The unary version drops one component: g receives c, ar, a and returns satisfaction of rel over the unary frame's extended environment, the goal being satisfaction of unShapeAt C k rel. The concrete introductions below instantiate rel at the four relations; for the two arity-raising ones, the clause demands the successor only existentially, and the numeral chapter's L-numeral sucʟ ar then serves as a concrete witness, injected into the truncation together with its certificates.

    → ((c ar a : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (fst a))
       → ⟨ (a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩)
    → ⟨ γ ⊨ unShapeAt C k rel ⟩

The same-arity introductions are now built by composing the generic frame introductions with the concrete relations. For the unary frame, the tag equation delivered by arityTagAtL-adequate aligns the shape the frame reads with the data a caller supplies. The first composed introduction binSameClosed-in instantiates the binary frame at bothSameAt C: instead of an arbitrary relation, the caller now owes meta-level membership data, and the lemma repackages that data as satisfaction of the clause.

  unShape-in C k rel γ g c c∈ ar a sh =
    g c ar a c∈
      (subst ⟨_⟩ (arityTagAtL-adequate c3 n3 k a3 (a ∷ ar ∷ c ∷ γ)) sh)

  binSameClosed-in : (C : Fin n) (k : ℕ) (γ : S ^ n)
    → ((c ar a b : S)

Here g is the closure obligation itself, stated as data: from a key of the given shape it must produce membership of both subformula keys, the pairs of the arity ar with a and with b. The lemma converts that data into satisfaction of the full clause, so a recursion over codes can discharge the binary-connective obligations by supplying exactly this membership data.

       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
       → ⟨ pr (fst ar) (fst a) ∈ fst (lookup C γ) ⟩
       × ⟨ pr (fst ar) (fst b) ∈ fst (lookup C γ) ⟩)
    → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩

To build satisfaction of the conjunction, the two membership claims that g returns must be recast as satisfaction of the two appAt conjuncts. The adequacy lemma for appAt equates the two forms, and here it is used in the direction opposite to the elimination side, since the goal now reads from data to satisfaction.

  binSameClosed-in C k γ g = binShape-in C k (bothSameAt C) γ
    (λ c ar a b c∈ sh →
        subst ⟨_⟩ (sym (appAt-adequate (sh4 C) n4 a4 (b ∷ a ∷ ar ∷ c ∷ γ)))
          (g c ar a b c∈ sh .fst)
      , subst ⟨_⟩ (sym (appAt-adequate (sh4 C) n4 b4 (b ∷ a ∷ ar ∷ c ∷ γ)))

The two components are handled by the same reading, one conjunct at a time. The unary same-arity introduction unSameClosed-in then repeats the construction for the one-component relation, with the same data shape minus the second component.

          (g c ar a b c∈ sh .snd))

  unSameClosed-in : (C : Fin n) (k : ℕ) (γ : S ^ n)
    → ((c ar a : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (fst a))

For the unary same-arity clause a single membership claim suffices: g returns membership of the one subformula key, and the composition with the generic unary introduction, with rel fixed to oneSameAt C, turns it into satisfaction of the clause.

       → ⟨ pr (fst ar) (fst a) ∈ fst (lookup C γ) ⟩)
    → ⟨ γ ⊨ unShapeAt C k (oneSameAt C) ⟩
  unSameClosed-in C k γ g = unShape-in C k (oneSameAt C) γ
    (λ c ar a c∈ sh →
      subst ⟨_⟩ (sym (appAt-adequate (sh3 C) n3 a3 (a ∷ ar ∷ c ∷ γ)))

The last two introductions raise the arity, starting with unSuccClosed-in. Its hypothesis g receives the usual unary key data but must conclude membership of the successor key: the pair of sucV (fst ar), the successor of the key's arity, with a.

        (g c ar a c∈ sh))

  unSuccClosed-in : (C : Fin n) (k : ℕ) (γ : S ^ n)
    → ((c ar a : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (fst a))

The relation oneSuccAt demands its successor only existentially and merely, so any witness carrying the two certificates is acceptable, and the proof supplies a concrete one: the L-numeral sucʟ ar. It is a valid witness because its first-projection law sucʟ-fst ar identifies its first component with sucV (fst ar), and the adequacy lemma for sucAtL converts that defining equation into the satisfaction the clause reads.

       → ⟨ pr (sucV (fst ar)) (fst a) ∈ fst (lookup C γ) ⟩)
    → ⟨ γ ⊨ unShapeAt C k (oneSuccAt C) ⟩
  unSuccClosed-in C k γ g = unShape-in C k (oneSuccAt C) γ
    (λ c ar a c∈ sh → ∣ sucʟ ar
      , ( subst ⟨_⟩ (sym (sucAtL-adequate (suc n3) zero

The second certificate is the pairing claim. g already yields membership of the successor key, and the numeral's projection law re-expresses that as membership of pr (sucʟ ar) (fst a), which the adequacy lemma for appAt converts into the satisfaction of the pairing conjunct. Injecting the witness with its certificates into propositional truncation needs no propositionhood premise; that requirement belongs to elimination, not introduction.

            (sucʟ ar ∷ a ∷ ar ∷ c ∷ γ))) (sucʟ-fst ar)
        , subst ⟨_⟩ (sym (appAt-adequate (suc (sh3 C)) zero (suc a3)
            (sucʟ ar ∷ a ∷ ar ∷ c ∷ γ)))
            (subst (λ w → ⟨ pr w (fst a) ∈ fst (lookup C γ) ⟩)
              (sym (sucʟ-fst ar)) (g c ar a c∈ sh)) ) ∣₁)

The final introduction binSuccClosed-in covers the bounded quantifiers. Its hypothesis g receives the binary key's four values and must produce membership of the second component under the successor arity: the pair of sucV (fst ar) with b, since the first slot carries the bounding term rather than a subformula.

  binSuccClosed-in : (C : Fin n) (k : ℕ) (γ : S ^ n)
    → ((c ar a b : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
       → ⟨ pr (sucV (fst ar)) (fst b) ∈ fst (lookup C γ) ⟩)

The construction is the same as the unary successor introduction, applied at the binary frame with rel fixed to succSndAt C: the witness is again the L-numeral sucʟ ar, its projection law again certifies the successor, and the pairing claim now concerns only the second component b, after which the bounded-quantifier clause is satisfied.

    → ⟨ γ ⊨ binShapeAt C k (succSndAt C) ⟩
  binSuccClosed-in C k γ g = binShape-in C k (succSndAt C) γ
    (λ c ar a b c∈ sh → ∣ sucʟ ar
      , ( subst ⟨_⟩ (sym (sucAtL-adequate (suc n4) zero
            (sucʟ ar ∷ b ∷ a ∷ ar ∷ c ∷ γ))) (sucʟ-fst ar)

The binary successor case uses the same witness and the same two adequacy facts, now for the formula component of a bounded quantifier. Thus every active constructor clause has both readings: satisfaction yields the required subcode memberships, and actual closure data yields satisfaction. These two directions make closedAt C the object-language form of meta-level closure under immediate formula subcodes.

        , subst ⟨_⟩ (sym (appAt-adequate (suc (sh4 C)) zero (suc b4)
            (sucʟ ar ∷ b ∷ a ∷ ar ∷ c ∷ γ)))
            (subst (λ w → ⟨ pr w (fst b) ∈ fst (lookup C γ) ⟩)
              (sym (sucʟ-fst ar)) (g c ar a b c∈ sh)) ) ∣₁)

Recap

closedAt requires every compound code in the domain to bring along the subformula codes its clause reads. Its elimination lemmas expose those subcodes, and its introduction lemmas build the same seven obligations from meta-level membership facts.