BedrockRecognizing well-formed constructor keys
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapA 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.
{-# 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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))))))))))))