---
title: "Recognizing well-formed constructor keys"
module: L.Coding.CodeShape
lang: en
site: "Bedrock"
description: "Recognizing well-formed constructor keys"
stage: "Internal coding: tables and uniform satisfaction"
reading_order: 54
canonical: https://bedrock.institute/en/L.Coding.CodeShape.html
html: L.Coding.CodeShape.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/CodeShape.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Expressions, L.Coding.Closure, L.Coding.CodeConstructibility, L.Coding.SubformulaClosure, L.Axioms.Numerals, L.Ordinal]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.CodeShape.md, https://bedrock.institute/ja/L.Coding.CodeShape.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Recognizing well-formed constructor keys

A code is well formed when it has one of the term or formula constructor shapes and its payloads occupy the expected frames. This chapter defines the ten-way shape predicate, proves its flat witness characterization in both directions, and recovers or constructs term codes and immediate subcodes.

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

open import Base.Prelude

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Term; Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊤̇; ⊥̇
        ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; #mono; module VCode )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; sucV )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Expressions {ℓ} using ( tagAtL; tagAtL-adequate; arityTagAtL; arityTagAtL-adequate; arityTagPairAtL; arityTagPairAtL-adequate; numL )
open import L.Coding.Closure {ℓ} using ( closedAt; binShapeAt; unShapeAt; bothSameAt; oneSameAt; oneSuccAt; succSndAt; binSameClosed-out; unSameClosed-out; unSuccClosed-out; binSuccClosed-out )
open import L.Coding.CodeConstructibility {ℓ} using ( closure-inv; key; codeL; codeTmL )
open import L.Coding.SubformulaClosure {ℓ} using ( clo )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Ordinal {ℓ} using ( ∈#-elim )

open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( fromℕ'; toFromId'; toℕ<n )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
import Cubical.Data.Sum as Sum
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )

open hPropStructure 𝒮ʟ

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

## The two payload frames

A tag whose payload is a pair, and a tag whose payload is a single code. Ten
tags, two shapes: which one a tag takes is the only thing that varies, and the
rest of what a tag demands of its payload is a relation the frame carries. That
is the same division the closedness predicate makes, and for the same reason.

```agda
module _ {n : ℕ} where
  binForm : ℕ → Formula S (4 + n) → Formula S (suc n)
  binForm k rel = ∃̇ (∃̇ (∃̇ (arityTagPairAtL
    (suc (suc (suc zero))) (suc (suc zero)) k (suc zero) zero ∧̇ rel)))

  unForm : ℕ → Formula S (3 + n) → Formula S (suc n)
  unForm k rel = ∃̇ (∃̇ (arityTagAtL (suc (suc zero)) (suc zero) k zero ∧̇ rel))
```

## Term codes

The four tags whose payloads reach outside the formula codes need one predicate,
and it is not recursive: a term is a constant or a variable, and neither has a
part. Both alternatives are bounded, and by different things.

A variable's index must lie below the arity, which is what makes the formula the
code of a term *at that arity* rather than at some larger one. A constant must be
a member of the carrier, which is what makes it the code of a term *over that
alphabet* rather than over the whole model. This second conjunct is the one the
code set was caught between two statements without: with no bound on a constant,
a payload read back as one is an arbitrary element of `L`, and the class the
decode lands in is wider than the class the introduction starts from.

Both bounds are memberships at a slot, and both slots are named by the caller.
The carrier is a slot rather than a constant on purpose. A constant would pin
every predicate below this line to one carrier, and everything indexed by them
would be re-indexed at the pair; a slot is threaded, and threading is free.

```agda
isTmAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
isTmAt t N A = ∃̇ (tagAtL (suc t) 0 zero ∧̇ (var zero ∈̇ var (suc A)))
            ∨̇ ∃̇ (tagAtL (suc t) 1 zero ∧̇ (var zero ∈̇ var (suc N)))
```

## The ten, as one predicate

Every member is a well-formed key: an arity-tagged pair carrying one of the
ten tags, with the payload that tag calls for. The relations say what
closedness does not: that an atom's two parts are term codes, that a bounded
quantifier's first part is one, and that a constant's payload is zero. The
formula parts are left to closedness, which is where they belong, since they are
the only parts anything descends into.

Being shaped is therefore relative to two slots and not one: the set, and the
carrier its terms name their constants from. Only the four relations that mention
a term look at the second, and they are the only four that could.

```agda
module _ {n : ℕ} where
  bothTm fstTm : Fin n → Formula S (4 + n)
  bothTm A = isTmAt (suc zero) (suc (suc zero)) (suc (suc (suc (suc A))))
          ∧̇ isTmAt zero (suc (suc zero)) (suc (suc (suc (suc A))))
  fstTm  A = isTmAt (suc zero) (suc (suc zero)) (suc (suc (suc (suc A))))

  noneB : Formula S (4 + n)
  noneB = ⊤̇ {n = 4 + n}

  zeroPay noneU : Formula S (3 + n)
  zeroPay = var zero ≐ con (numeralL 0)
  noneU   = ⊤̇ {n = 3 + n}

  shapes : Fin n → Formula S (suc n)
  shapes A = binForm 0 (bothTm A) ∨̇ (binForm 1 (bothTm A)
           ∨̇ (binForm 2 noneB ∨̇ (binForm 3 noneB ∨̇ (binForm 4 noneB
           ∨̇ (unForm 5 zeroPay ∨̇ (unForm 6 noneU ∨̇ (unForm 7 noneU
           ∨̇ (binForm 8 (fstTm A) ∨̇ binForm 9 (fstTm A)))))))))

  shapedAt : Fin n → Fin n → Formula S n
  shapedAt C A = ∀̇∈ (var C) (shapes A)
```

## What a member is, read flat

Ten alternatives. The two frames are read once each, generically in the
relation they carry, so that the reading along the disjunction below is ten
applications of two readers rather than ten copies of the same unnesting.

```agda
BinWit : ∀ {n} → ℕ → Formula S (4 + n) → S ^ n → S → Type (ℓ-suc ℓ)
BinWit k rel γ c = Σ[ N ∈ S ] (Σ[ a ∈ S ] (Σ[ b ∈ S ]
  ((fst c ≡ pr (fst N) (pr (# k) (pr (fst a) (fst b))))
   × ⟨ (b ∷ a ∷ N ∷ c ∷ γ) ⊨ rel ⟩)))

UnWit : ∀ {n} → ℕ → Formula S (3 + n) → S ^ n → S → Type (ℓ-suc ℓ)
UnWit k rel γ c = Σ[ N ∈ S ] (Σ[ a ∈ S ]
  ((fst c ≡ pr (fst N) (pr (# k) (fst a))) × ⟨ (a ∷ N ∷ c ∷ γ) ⊨ rel ⟩))

binForm-out : ∀ {n} (k : ℕ) (rel : Formula S (4 + n)) (γ : S ^ n) (c : S)
            → ⟨ (c ∷ γ) ⊨ binForm k rel ⟩ → ∥ BinWit k rel γ c ∥₁
binForm-out k rel γ c = PT.rec squash₁ (λ { (N , hN) →
  PT.rec squash₁ (λ { (a , ha) → PT.map
    (λ { (b , (hb , hr)) → N , (a , (b , (subst ⟨_⟩
       (arityTagPairAtL-adequate (suc (suc (suc zero))) (suc (suc zero)) k
          (suc zero) zero (b ∷ a ∷ N ∷ c ∷ γ)) hb , hr))) })
    ha }) hN })

unForm-out : ∀ {n} (k : ℕ) (rel : Formula S (3 + n)) (γ : S ^ n) (c : S)
           → ⟨ (c ∷ γ) ⊨ unForm k rel ⟩ → ∥ UnWit k rel γ c ∥₁
unForm-out k rel γ c = PT.rec squash₁ (λ { (N , hN) → PT.map
  (λ { (a , (ha , hr)) → N , (a , (subst ⟨_⟩
     (arityTagAtL-adequate (suc (suc zero)) (suc zero) k zero
        (a ∷ N ∷ c ∷ γ)) ha , hr)) })
  hN })

ShapeWit : ∀ {n} → Fin n → S ^ n → S → Type (ℓ-suc ℓ)
ShapeWit A γ c =
    BinWit 0 (bothTm A) γ c ⊎ (BinWit 1 (bothTm A) γ c
  ⊎ (BinWit 2 noneB γ c ⊎ (BinWit 3 noneB γ c ⊎ (BinWit 4 noneB γ c
  ⊎ (UnWit 5 zeroPay γ c ⊎ (UnWit 6 noneU γ c ⊎ (UnWit 7 noneU γ c
  ⊎ (BinWit 8 (fstTm A) γ c ⊎ BinWit 9 (fstTm A) γ c))))))))

private
  sum-out : {A B C D : Type (ℓ-suc ℓ)}
          → (A → ∥ C ∥₁) → (B → ∥ D ∥₁) → ∥ A ⊎ B ∥₁ → ∥ C ⊎ D ∥₁
  sum-out f g = PT.rec squash₁
    (Sum.rec (λ x → PT.map inl (f x)) (λ y → PT.map inr (g y)))

  sum-in : {A B C D : Type (ℓ-suc ℓ)}
         → (A → C) → (B → D) → A ⊎ B → ∥ C ⊎ D ∥₁
  sum-in f g x = ∣ Sum.map f g x ∣₁

shaped-out : ∀ {n} (C A : Fin n) (γ : S ^ n) → ⟨ γ ⊨ shapedAt C A ⟩
           → (c : S) → ⟨ c ∈ˢ lookup C γ ⟩ → ∥ ShapeWit A γ c ∥₁
shaped-out C A γ h c c∈ = read (h c c∈)
  where
  read : ⟨ (c ∷ γ) ⊨ shapes A ⟩ → ∥ ShapeWit A γ c ∥₁
  read =
    sum-out (binForm-out 0 (bothTm A) γ c)
    (sum-out (binForm-out 1 (bothTm A) γ c)
    (sum-out (binForm-out 2 noneB γ c)
    (sum-out (binForm-out 3 noneB γ c)
    (sum-out (binForm-out 4 noneB γ c)
    (sum-out (unForm-out 5 zeroPay γ c)
    (sum-out (unForm-out 6 noneU γ c)
    (sum-out (unForm-out 7 noneU γ c)
    (sum-out (binForm-out 8 (fstTm A) γ c)
    (binForm-out 9 (fstTm A) γ c)))))))))
```

## The same ten, written

A predicate written to be consumed proves nothing until something satisfies it.
The decode takes a shaped set as a hypothesis, so whoever supplies the set owes
that hypothesis, and owing it means building: an existential frame has its
witnesses to produce and a disjunct to choose, where the elimination had only to
take them apart.

The two frames are introduced once each, generically in the relation, for the
reason that decided the elimination and for one more. The adequacy equation each
frame carries is discharged here, with the tag, the relation and the environment
all still variables. Discharged at a named tag instead, it would be ten
unfoldings of a formula three quantifiers deep, and that is the difference
between a second and an afternoon.

```agda
binForm-in : ∀ {n} (k : ℕ) (rel : Formula S (4 + n)) (γ : S ^ n) (c : S)
           → BinWit k rel γ c → ⟨ (c ∷ γ) ⊨ binForm k rel ⟩
binForm-in k rel γ c (N , (a , (b , (e , hr)))) =
  ∣ N , ∣ a , ∣ b , (subst ⟨_⟩ (sym (arityTagPairAtL-adequate
     (suc (suc (suc zero))) (suc (suc zero)) k (suc zero) zero
     (b ∷ a ∷ N ∷ c ∷ γ))) e , hr) ∣₁ ∣₁ ∣₁

unForm-in : ∀ {n} (k : ℕ) (rel : Formula S (3 + n)) (γ : S ^ n) (c : S)
          → UnWit k rel γ c → ⟨ (c ∷ γ) ⊨ unForm k rel ⟩
unForm-in k rel γ c (N , (a , (e , hr))) =
  ∣ N , ∣ a , (subst ⟨_⟩ (sym (arityTagAtL-adequate
     (suc (suc zero)) (suc zero) k zero (a ∷ N ∷ c ∷ γ))) e , hr) ∣₁ ∣₁
```

The walk over the disjunction mirrors its reading: each level injects one
summand and carries its own truncation. The shared maps operate on semantic
types, with each constructor's reader supplied explicitly. They never recover
a formula from its meaning. The caller supplies exactly one thing per member:
which of the ten shapes that member has.

```agda
shaped-in : ∀ {n} (C A : Fin n) (γ : S ^ n)
          → ((c : S) → ⟨ c ∈ˢ lookup C γ ⟩ → ∥ ShapeWit A γ c ∥₁)
          → ⟨ γ ⊨ shapedAt C A ⟩
shaped-in C A γ g c c∈ = PT.rec (snd ((c ∷ γ) ⊨ shapes A)) fill (g c c∈)
  where
  fill : ShapeWit A γ c → ⟨ (c ∷ γ) ⊨ shapes A ⟩
  fill =
    sum-in (binForm-in 0 (bothTm A) γ c)
    (sum-in (binForm-in 1 (bothTm A) γ c)
    (sum-in (binForm-in 2 noneB γ c)
    (sum-in (binForm-in 3 noneB γ c)
    (sum-in (binForm-in 4 noneB γ c)
    (sum-in (unForm-in 5 zeroPay γ c)
    (sum-in (unForm-in 6 noneU γ c)
    (sum-in (unForm-in 7 noneU γ c)
    (sum-in (binForm-in 8 (fstTm A) γ c)
    (binForm-in 9 (fstTm A) γ c)))))))))
```

## Terms, recovered

The first decode, and the only one that needs no induction. A term is a constant
or a variable: the constant case reads its payload back as a constant of the
alphabet, and the variable case reads an index out of the arity numeral. Each
case uses exactly the bound its disjunct carries, and neither could be written
without one. No case here descends into a subcode, which is why this decode is
separable from the recursion that follows and why it is written first.

What the term is produced *over* is a parameter, and it is what the chapter is
for. The alphabet is any type with an embedding into the hierarchy, and the
constant case needs one thing the shape predicate cannot supply: that the
carrier's members are the alphabet's image. That is a hypothesis, because it is
a fact about the pair (alphabet, carrier) and not about the code. At the one
instantiation that matters, the alphabet is the carrier's own member type and
the hypothesis is the presentation of a set by its members, so it costs a
discharge rather than a construction.

The two disjuncts are read by two named lemmas and the reader is their case
split, which is not a matter of taste. Written as two clauses of one function,
each carrying its own truncation under a disjunction that also carries one, the
chapter did not finish in ten minutes; with each disjunct's reading given a
written type of its own it checks in under two seconds. The rule is the
elaborator's, not the mathematics': a branch whose type is written is solved
against that type, and a branch whose type is inferred is solved against the
whole disjunction.

```agda
module _ {K : Type ℓ} (f : K → V ℓ) where

  TmWit : ℕ → V ℓ → Type (ℓ-suc ℓ)
  TmWit n x = Σ[ t ∈ Term K n ] (VCode.⌜ mapTm f t ⌝ᵗ ≡ x)

  Onto : ∀ {m} → Fin m → S ^ m → Type (ℓ-suc ℓ)
  Onto A γ = (y : V ℓ) → ⟨ y ∈ fst (lookup A γ) ⟩ → ∥ Σ[ c ∈ K ] (f c ≡ y) ∥₁

  tmCon : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ) → Onto A γ
        → ⟨ γ ⊨ ∃̇ (tagAtL (suc t) 0 zero ∧̇ (var zero ∈̇ var (suc A))) ⟩
        → ∥ TmWit n (fst (lookup t γ)) ∥₁
  tmCon t N A γ n onto = PT.rec squash₁
    (λ { (y , (hy , y∈)) → PT.map
         (λ { (c , qc) → con c
            , ( cong (VCode.mkTag 0) qc ∙ sym
                (subst ⟨_⟩ (tagAtL-adequate (suc t) 0 zero (y ∷ γ)) hy) ) })
         (onto (fst y) y∈) })

  tmVar : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ)
        → fst (lookup N γ) ≡ # n
        → ⟨ γ ⊨ ∃̇ (tagAtL (suc t) 1 zero ∧̇ (var zero ∈̇ var (suc N))) ⟩
        → ∥ TmWit n (fst (lookup t γ)) ∥₁
  tmVar t N A γ n qN = PT.rec squash₁
    (λ { (z , (hz , z∈)) → PT.map
         (λ { (j , (j<n , ez)) →
           var (fromℕ' n j j<n)
           , ( cong (VCode.mkTag 1) (cong #_ (toFromId' n j j<n) ∙ sym ez)
             ∙ sym (subst ⟨_⟩ (tagAtL-adequate (suc t) 1 zero (z ∷ γ)) hz) ) })
         (∈#-elim n (fst z) (subst (λ w → ⟨ fst z ∈ w ⟩) qN z∈)) })

  isTmAt-decode : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ)
                → fst (lookup N γ) ≡ # n → Onto A γ
                → ⟨ γ ⊨ isTmAt t N A ⟩ → ∥ TmWit n (fst (lookup t γ)) ∥₁
  isTmAt-decode t N A γ n qN onto = PT.rec squash₁
    (λ { (inl h) → tmCon t N A γ n onto h
       ; (inr h) → tmVar t N A γ n qN h })
```

## Terms, encoded

The same two clauses read backwards, and the only place in the introduction half
where anything has to be computed rather than repackaged. Each clause now needs
its own bound as well as its tag equation, and the two bounds are different.
A constant is its own code, so its tag equation is nothing at all, and
what it needs is that the constant is a member of the carrier: a hypothesis here,
because only the caller knows which carrier it meant. A variable has to put its
index *inside* the arity numeral, which is the other bound working in the
direction it was designed for: the decode read an index out of a numeral, and
here a numeral is shown to hold one. That second fact was already available, since
a smaller numeral belonging to a larger one is exactly what made distinct
numerals distinct.

```agda
module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where

  isTmAt-in : ∀ {m} (t N A : Fin m) (γ : S ^ m) (n : ℕ)
            → fst (lookup N γ) ≡ # n
            → ((c : K) → ⟨ f c ∈ fst (lookup A γ) ⟩)
            → TmWit f n (fst (lookup t γ)) → ⟨ γ ⊨ isTmAt t N A ⟩
  isTmAt-in t N A γ n qN into (con c , e) = ∣ inl ∣ y
    , ( subst ⟨_⟩ (sym (tagAtL-adequate (suc t) 0 zero (y ∷ γ))) (sym e)
      , into c ) ∣₁ ∣₁
    where
    y : S
    y = f c , h c
  isTmAt-in t N A γ n qN into (var i , e) = ∣ inr ∣ z
    , ( subst ⟨_⟩ (sym (tagAtL-adequate (suc t) 1 zero (z ∷ γ)))
          (sym e ∙ cong (VCode.mkTag 1) (sym (numeralL-fst (toℕ i))))
      , subst (λ w → ⟨ fst z ∈ w ⟩) (sym qN)
          (subst (λ w → ⟨ w ∈ (# n) ⟩) (sym (numeralL-fst (toℕ i)))
            (#mono (toℕ i) n (toℕ<n i))) ) ∣₁ ∣₁
    where
    z : S
    z = numeralL (toℕ i)
```

## One layer off

The two halves meet. Shapedness says which of the ten a member is and hands
back its parts; closedness says those parts are members too, at the arity the
tag calls for. Neither half alone gives a step of a recursion, and together they
give exactly one.

The equation shapedness produces is, letter for letter, the one closedness
consumes, so the two compose with nothing in between. That is not luck: both
were written against the same reading of an arity-tagged pair.

```agda
module Peel {m : ℕ} (C A : Fin m) (γ : S ^ m)
            (hcl : ⟨ γ ⊨ closedAt C ⟩) (hsh : ⟨ γ ⊨ shapedAt C A ⟩) where
  private
    D : V ℓ
    D = fst (lookup C γ)

  BinSame BinSucc : ℕ → S → Type (ℓ-suc ℓ)
  BinSame k c = Σ[ N ∈ S ] (Σ[ a ∈ S ] (Σ[ b ∈ S ]
    ((fst c ≡ pr (fst N) (pr (# k) (pr (fst a) (fst b))))
     × (⟨ pr (fst N) (fst a) ∈ D ⟩ × ⟨ pr (fst N) (fst b) ∈ D ⟩))))
  BinSucc k c = Σ[ N ∈ S ] (Σ[ a ∈ S ] (Σ[ b ∈ S ]
    ((fst c ≡ pr (fst N) (pr (# k) (pr (fst a) (fst b))))
     × (⟨ (a ∷ N ∷ c ∷ γ) ⊨ isTmAt zero (suc zero) (suc (suc (suc A))) ⟩
        × ⟨ pr (sucV (fst N)) (fst b) ∈ D ⟩))))

  UnSame UnSucc : ℕ → S → Type (ℓ-suc ℓ)
  UnSame k c = Σ[ N ∈ S ] (Σ[ a ∈ S ]
    ((fst c ≡ pr (fst N) (pr (# k) (fst a))) × ⟨ pr (fst N) (fst a) ∈ D ⟩))
  UnSucc k c = Σ[ N ∈ S ] (Σ[ a ∈ S ]
    ((fst c ≡ pr (fst N) (pr (# k) (fst a))) × ⟨ pr (sucV (fst N)) (fst a) ∈ D ⟩))

  PeelWit : S → Type (ℓ-suc ℓ)
  PeelWit c =
      BinWit 0 (bothTm A) γ c ⊎ (BinWit 1 (bothTm A) γ c
    ⊎ (BinSame 2 c ⊎ (BinSame 3 c ⊎ (BinSame 4 c
    ⊎ (UnWit 5 zeroPay γ c ⊎ (UnSucc 6 c ⊎ (UnSucc 7 c
    ⊎ (BinSucc 8 c ⊎ BinSucc 9 c))))))))

  peel : (c : S) → ⟨ c ∈ˢ lookup C γ ⟩ → ∥ PeelWit c ∥₁
  peel c c∈ = PT.map fill (shaped-out C A γ hsh c c∈)
    where
    bs : (k : ℕ) → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩ → BinWit k noneB γ c
       → BinSame k c
    bs k h (N , (a , (b , (e , _)))) =
      N , (a , (b , (e , binSameClosed-out C k γ h c N a b c∈ e)))

    us : (k : ℕ) → ⟨ γ ⊨ unShapeAt C k (oneSameAt C) ⟩ → UnWit k noneU γ c
       → UnSame k c
    us k h (N , (a , (e , _))) =
      N , (a , (e , unSameClosed-out C k γ h c N a c∈ e))

    uz : (k : ℕ) → ⟨ γ ⊨ unShapeAt C k (oneSuccAt C) ⟩ → UnWit k noneU γ c
       → UnSucc k c
    uz k h (N , (a , (e , _))) =
      N , (a , (e , unSuccClosed-out C k γ h c N a c∈ e))

    bz : (k : ℕ) → ⟨ γ ⊨ binShapeAt C k (succSndAt C) ⟩ → BinWit k (fstTm A) γ c
       → BinSucc k c
    bz k h (N , (a , (b , (e , hr)))) =
      N , (a , (b , (e , (hr , binSuccClosed-out C k γ h c N a b c∈ e))))

    fill : ShapeWit A γ c → PeelWit c
    fill =
      Sum.map id
      (Sum.map id
      (Sum.map (bs 2 (hcl .fst))
      (Sum.map (bs 3 (hcl .snd .fst))
      (Sum.map (bs 4 (hcl .snd .snd .fst))
      (Sum.map id
      (Sum.map (uz 6 (hcl .snd .snd .snd .fst))
      (Sum.map (uz 7 (hcl .snd .snd .snd .snd .fst))
      (Sum.map (bz 8 (hcl .snd .snd .snd .snd .snd .fst))
      (bz 9 (hcl .snd .snd .snd .snd .snd .snd))))))))))
```

## The closure is shaped

What the predicate is for. A recursion over codes is handed an index set, and
that set has to be closed or the clauses constrain nothing, and shaped or they
admit junk. Closedness was discharged for the closure a chapter ago; this is the
other half, and it is the shorter one, because shapedness asks nothing about
what a member drags in with it. Half of what the inversion returns is therefore
dropped on the floor.

The analysis is on the constructor alone. The tag is not a second index to be
matched against: it is computed from the constructor, exactly as
`byTag` computes the closedness demand from it, so the table is ten
lines and not ten times ten. Nothing here recurses either, because the key
of a named constructor already computes to the arity-tagged pair the witness
type asks for, and no transport is needed anywhere in the ten tuples.

The one thing a tuple cannot compute is the term witness: a payload slot holding
a term code must be certified as one, and the certificate is the encoder above
applied to the term the constructor carries. That certificate now has a second
half, supplied by the caller: every constant of the alphabet is a member of the
carrier. It is one hypothesis, discharged once per call rather than once per
constructor, because the alphabet is fixed before the formula is.

The first half, on the other hand, becomes easier. The witness a term owes is that
its code is the code of *some* term, and over the alphabet the code of a term
already is that: the encoder is the identity with `refl` beside it. On the
model's own coding it must first establish a correspondence between the two codings.

```agda
module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where
  private
    cd : ∀ {n} → Formula K n → S
    cd φ = VCode.⌜ mapFo f φ ⌝ , codeL f h φ

    ct : ∀ {n} → Term K n → S
    ct t = VCode.⌜ mapTm f t ⌝ᵗ , codeTmL f h t

    nn : ℕ → S
    nn n = # n , numL n

    tw : ∀ {n} (t : Term K n) → TmWit f n (fst (ct t))
    tw t = t , refl

  closureShaped : ∀ {n m} (φ : Formula K n) (A : Fin m) (γ : S ^ m)
                → ((k : K) → ⟨ f k ∈ fst (lookup A γ) ⟩)
                → ⟨ (clo f h φ ∷ γ) ⊨ shapedAt zero (suc A) ⟩
  closureShaped φ A γ into = shaped-in zero (suc A) (clo f h φ ∷ γ)
    (λ c c∈ → PT.map (λ { (_ , ψ , q , _) → go ψ c q })
      (closure-inv f h φ (fst c) c∈))
    where
    tm1 : ∀ {k} (t : Term K k) (b c : S)
        → ⟨ (b ∷ ct t ∷ nn k ∷ c ∷ clo f h φ ∷ γ)
            ⊨ isTmAt (suc zero) (suc (suc zero))
                (suc (suc (suc (suc (suc A))))) ⟩
    tm1 {k} t b c = isTmAt-in f h (suc zero) (suc (suc zero))
      (suc (suc (suc (suc (suc A)))))
      (b ∷ ct t ∷ nn k ∷ c ∷ clo f h φ ∷ γ) k refl into (tw t)

    tm0 : ∀ {k} (u : Term K k) (a c : S)
        → ⟨ (ct u ∷ a ∷ nn k ∷ c ∷ clo f h φ ∷ γ)
            ⊨ isTmAt zero (suc (suc zero))
                (suc (suc (suc (suc (suc A))))) ⟩
    tm0 {k} u a c = isTmAt-in f h zero (suc (suc zero))
      (suc (suc (suc (suc (suc A)))))
      (ct u ∷ a ∷ nn k ∷ c ∷ clo f h φ ∷ γ) k refl into (tw u)

    go : ∀ {k} (ψ : Formula K k) (c : S) → fst c ≡ key f h ψ
       → ShapeWit (suc A) (clo f h φ ∷ γ) c
    go {k} (t ∈̇ u) c q =
      inl (nn k , (ct t , (ct u , (q , (tm1 t (ct u) c , tm0 u (ct t) c)))))
    go {k} (t ≐ u) c q =
      inr (inl
        (nn k , (ct t , (ct u , (q , (tm1 t (ct u) c , tm0 u (ct t) c))))))
    go {k} (a ∧̇ b) c q = inr (inr (inl (nn k , (cd a , (cd b , (q , (λ z → z)))))))
    go {k} (a ∨̇ b) c q =
      inr (inr (inr (inl (nn k , (cd a , (cd b , (q , (λ z → z))))))))
    go {k} (a ⇒̇ b) c q =
      inr (inr (inr (inr (inl (nn k , (cd a , (cd b , (q , (λ z → z)))))))))
    go {k} ⊥̇ c q =
      inr (inr (inr (inr (inr (inl (nn k , (nn 0 , (q , sym (numeralL-fst 0)))))))))
    go {k} (∃̇ a) c q =
      inr (inr (inr (inr (inr (inr (inl (nn k , (cd a , (q , (λ z → z))))))))))
    go {k} (∀̇ a) c q =
      inr (inr (inr (inr (inr (inr (inr (inl (nn k , (cd a , (q , (λ z → z)))))))))))
    go {k} (∀̇∈ t a) c q =
      inr (inr (inr (inr (inr (inr (inr (inr (inl
        (nn k , (ct t , (cd a , (q , tm1 t (cd a) c))))))))))))
    go {k} (∃̇∈ t a) c q =
      inr (inr (inr (inr (inr (inr (inr (inr (inr
        (nn k , (ct t , (cd a , (q , tm1 t (cd a) c))))))))))))
```