Bedrock良构构造子键的识别
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图一个码若具有某种词项或公式构造子的形状，且其载荷位于预期框架中，就是良构的。本章定义十路形状谓词，双向证明其平铺见证的刻画，并恢复或构造词项码与直接子码。
{-# 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 _⊨_ )
两个载荷框架
一类标签的载荷是一个对，另一类的载荷是单个码。十个标签，两种形状：其中变动的只有标签取哪一种，而载荷须满足的其余条件，是框架所携带的一条关系。这一划分与封闭性谓词所作的划分相同，理由也相同。
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))
词项码
那四个载荷超出公式码范围的标签，需要一条谓词，而这条谓词不是递归的：词项要么是常元，要么是变元，二者都没有部件。两支各有一道界，但两道界的性质不同。
变元的序号必须落在元数之下，正是这一点使那条公式成为在该元数上的词项之码，而非在某个更大的元数上。常元则必须是载体的成员，正是这一点使它成为在该字母表之上的词项之码，而非在整个模型之上。第二个合取项，正是当初以两条陈述界住码集时所缺的那一条：常元一旦不受界，一个被读回作常元的载荷就可能是 L 的任意元素，而解码所落进的那一类，便比引入时所出发的那一类更宽。
两道界都是「在某一位上的成员关系」，而这两位都由调用方指定。载体取一位而不取一个常元，是有意为之：常元会把这条线以下的每条谓词固定到一个载体上，而以它们为索引的一切也都要在那个对上重新索引；一位则只是被传递下去，传递本身不增加代价。
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)))
十路合为一个谓词
每个成员都是一个良构的键：一个带元数标签的对，携带那十个标签之一，且载荷是该标签所要求的那种。诸关系说出封闭性没有说的事：原子的两个部件是词项码，有界量词的第一个部件是词项码，常元的载荷是零。公式部件留给封闭性，那也正是它们该在的地方，因为它们是唯一有东西会下降进去的部件。
于是「成形」相对的是两位，而非一位：那个集合，以及它的诸词项从中点名常元的那个载体。只有那四条提到词项的关系去看第二位，而它们也是仅有的四条能去看的。
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)
成员的平铺读取
共十种可能。两个框架各提供一条读式，且对它们所携带的关系是泛型的，这样，下文沿析取进行的读取便是两条读式的十次施用，而不是同一段解嵌套的十份拷贝。
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)))))))))
同样十路的写入
谓词只有在证明某个对象满足它之后才产生结论。解码以「集合成形」为假设，因此构造供解码使用的集合时，必须同时证明这一假设。对存在式框架，引入方向需要给出各个见证并选定一个析取分支；消去方向则从已有证明中取出这些数据。
两个框架各引入一次，且对关系泛型，理由与决定消去的那个相同，此外还有一个。每个框架所携带的充分性等式在此处给出，其时标签、关系与环境都还是变元。若改在标签已被具体指名的位置才给出，就等于把一条嵌套三层量词的公式展开十遍，那是一秒与一下午的差别。
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) ∣₁ ∣₁
走过那个析取的路与读它的路互为镜像：每层注入一个和项，并各自携带截断。共用映射作用于语义类型，各构造子的读式由调用方显式提供，无须从含义反推公式。调用者为每个成员提供的，恰是它属于十种形状中的哪一种。
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)))))))))
词项的恢复
这是第一个解码，也是唯一不需要归纳的解码。词项分为常元与变元：常元分支把载荷解释为字母表中的常元，变元分支从元数数码中恢复序号。两个分支分别使用对应析取项携带的边界证明；没有这些边界，两个分支都无法构造。这里不递归进入任何子码，因此可以与后续递归分开并先行定义。
词项相对于哪个字母表构造，是本章的一个参数。字母表可以是任何带有到层级嵌入的类型；常元分支还需要一项形状谓词无法提供的假设：载体成员恰好是字母表嵌入的像。这是关于字母表与载体的假设，而不是关于码的性质。在后文所需的实例中，字母表取载体自身的成员类型，这项假设正是「一个集合由其成员呈现」。因此，该事实由调用方提供，无需在词项解码中重新构造。
两个析取支由两条点了名的引理去读，那条读式就是它们的分情形，这里并无选择余地。写成一个函数的两条子句时，每支各带一个截断，而它们所在的析取自己也带一个，本章十分钟内没跑完；把每支的读法各给一个写出来的类型之后，两秒不到就查完。这条规矩是归约器的，不是数学的：类型被写出来的分支对着那个类型求解，类型靠推断的分支对着整个析取求解。
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 })
词项的符号化
同样的两支反过来读，也是引入这一半里唯一需要真正计算、而不只是重新包装的地方。如今每一支除标签等式外还各需要一道界，而两支所需的界并不相同。常元就是自己的码，故它的标签等式没有内容，它真正需要的是「该常元是载体的成员」：在这里这是一条假设，因为只有调用方知道它指的是哪个载体。变元则要把它的序号放进元数数码里，这正是另一道界按其设计发挥功用之处：解码从一个数码里读出一个序号，而此处则表明一个数码里含有一个序号。至于第二件事，早已成立，因为「较小的数码属于较大的」正是使相异的数码彼此相异的那一点。
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)
剥去一层
这里结合形状与封闭性。形状判定一个成员属于十种构造中的哪一种，并给出它的各个部件；封闭性证明这些部件也是成员，且位于该标签要求的元数处。任一性质单独都不足以建立递归步骤，二者合用则恰好满足该步骤的条件。
形状所给出的那条等式，正是封闭性所需要的那一条，二者逐字相同，故中间无需任何东西即可衔接。这不是巧合：两者都是对「带元数标签的对」按同一条读法写下的。
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))))))))))
闭包具有形状
这条谓词有什么用。对码的递归得到一个索引集，而那个集合必须封闭，否则诸子句什么也约束不了；也必须成形，否则它们会把垃圾放进来。封闭性已在一章之前为闭包给出；这里是另一半，而且较短，因为成形性对「一个成员含有哪些子成员」不作任何要求。于是那个反演所返回的东西有一半被弃置不用。
这里只需按构造子分情形。标签不是另一个需要匹配的索引；它由构造子计算，正如 byTag 从构造子计算封闭性要求。因此，这张表只有十行，而非十乘十。这里也没有递归：指定构造子后，其键已经计算为见证类型要求的带元数标签的对，十个元组中都不需要任何搬运。
元组唯一算不出来的是词项见证：载荷位上放着的词项码必须被认证为词项码，而那份认证正是上面的编码式施于该构造子所携的词项。这份认证如今有了第二半，由调用方提供：字母表的每个常元都是载体的成员。它是一条假设，每次调用提供一次，而不是每个构造子提供一次，因为字母表早在公式之前就已固定。
另一方面，第一半变得更容易了。一个词项所需的见证是「它的码是某个词项的码」，而在字母表之上，一个词项的码本来就是这个：编码式就是恒等，旁边配一个 refl。若在模型自己的编码上，则它还得先在两套编码之间建立对应。
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))))))))))))