---
title: "良构构造子键的识别"
module: L.Coding.CodeShape
lang: zh
site: "Bedrock"
description: "良构构造子键的识别"
stage: "内部编码：表与统一满足关系"
reading_order: 54
canonical: https://bedrock.institute/zh/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/en/L.Coding.CodeShape.md, https://bedrock.institute/ja/L.Coding.CodeShape.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 良构构造子键的识别

一个码若具有某种词项或公式构造子的形状，且其载荷位于预期框架中，就是良构的。本章定义十路形状谓词，双向证明其平铺见证的刻画，并恢复或构造词项码与直接子码。

```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 _⊨_ )
```

## 两个载荷框架

一类标签的载荷是一个对，另一类的载荷是单个码。十个标签，两种形状：其中变动的只有标签取哪一种，而载荷须满足的其余条件，是框架所携带的一条关系。这一划分与封闭性谓词所作的划分相同，理由也相同。

```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))
```

## 词项码

那四个载荷超出公式码范围的标签，需要一条谓词，而这条谓词不是递归的：词项要么是常元，要么是变元，二者都没有部件。两支各有一道界，但两道界的性质不同。

变元的序号必须落在元数之下，正是这一点使那条公式成为**在该元数上**的词项之码，而非在某个更大的元数上。常元则必须是载体的成员，正是这一点使它成为**在该字母表之上**的词项之码，而非在整个模型之上。第二个合取项，正是当初以两条陈述界住码集时所缺的那一条：常元一旦不受界，一个被读回作常元的载荷就可能是 `L` 的任意元素，而解码所落进的那一类，便比引入时所出发的那一类更宽。

两道界都是「在某一位上的成员关系」，而这两位都由调用方指定。载体取一位而不取一个常元，是有意为之：常元会把这条线以下的每条谓词固定到一个载体上，而以它们为索引的一切也都要在那个对上重新索引；一位则只是被传递下去，传递本身不增加代价。

```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)))
```

## 十路合为一个谓词

每个成员都是一个良构的键：一个带元数标签的对，携带那十个标签之一，且载荷是该标签所要求的那种。诸关系说出封闭性没有说的事：原子的两个部件是词项码，有界量词的第一个部件是词项码，常元的载荷是零。公式部件留给封闭性，那也正是它们该在的地方，因为它们是唯一有东西会下降进去的部件。

于是「成形」相对的是两位，而非一位：那个集合，以及它的诸词项从中点名常元的那个载体。只有那四条提到词项的关系去看第二位，而它们也是仅有的四条能去看的。

```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)
```

## 成员的平铺读取

共十种可能。两个框架各提供一条读式，且对它们所携带的关系是泛型的，这样，下文沿析取进行的读取便是两条读式的十次施用，而不是同一段解嵌套的十份拷贝。

```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)))))))))
```

## 同样十路的写入

谓词只有在证明某个对象满足它之后才产生结论。解码以「集合成形」为假设，因此构造供解码使用的集合时，必须同时证明这一假设。对存在式框架，引入方向需要给出各个见证并选定一个析取分支；消去方向则从已有证明中取出这些数据。

两个框架各引入一次，且对关系泛型，理由与决定消去的那个相同，此外还有一个。每个框架所携带的充分性等式在此处给出，其时标签、关系与环境都还是变元。若改在标签已被具体指名的位置才给出，就等于把一条嵌套三层量词的公式展开十遍，那是一秒与一下午的差别。

```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) ∣₁ ∣₁
```

走过那个析取的路与读它的路互为镜像：每层注入一个和项，并各自携带截断。共用映射作用于语义类型，各构造子的读式由调用方显式提供，无须从含义反推公式。调用者为每个成员提供的，恰是它属于十种形状中的哪一种。

```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)))))))))
```

## 词项的恢复

这是第一个解码，也是唯一不需要归纳的解码。词项分为常元与变元：常元分支把载荷解释为字母表中的常元，变元分支从元数数码中恢复序号。两个分支分别使用对应析取项携带的边界证明；没有这些边界，两个分支都无法构造。这里不递归进入任何子码，因此可以与后续递归分开并先行定义。

词项相对于哪个字母表构造，是本章的一个参数。字母表可以是任何带有到层级嵌入的类型；常元分支还需要一项形状谓词无法提供的假设：载体成员恰好是字母表嵌入的像。这是关于字母表与载体的假设，而不是关于码的性质。在后文所需的实例中，字母表取载体自身的成员类型，这项假设正是「一个集合由其成员呈现」。因此，该事实由调用方提供，无需在词项解码中重新构造。

两个析取支由两条点了名的引理去读，那条读式就是它们的分情形，这里并无选择余地。写成一个函数的两条子句时，每支各带一个截断，而它们所在的析取自己也带一个，本章十分钟内没跑完；把每支的读法各给一个写出来的类型之后，两秒不到就查完。这条规矩是归约器的，不是数学的：类型被写出来的分支对着那个类型求解，类型靠推断的分支对着整个析取求解。

```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 })
```

## 词项的符号化

同样的两支反过来读，也是引入这一半里唯一需要真正计算、而不只是重新包装的地方。如今每一支除标签等式外还各需要一道界，而两支所需的界并不相同。常元就是自己的码，故它的标签等式没有内容，它真正需要的是「该常元是载体的成员」：在这里这是一条假设，因为只有调用方知道它指的是哪个载体。变元则要把它的序号放**进**元数数码里，这正是另一道界按其设计发挥功用之处：解码从一个数码里读出一个序号，而此处则表明一个数码里含有一个序号。至于第二件事，早已成立，因为「较小的数码属于较大的」正是使相异的数码彼此相异的那一点。

```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)
```

## 剥去一层

这里结合形状与封闭性。形状判定一个成员属于十种构造中的哪一种，并给出它的各个部件；封闭性证明这些部件也是成员，且位于该标签要求的元数处。任一性质单独都不足以建立递归步骤，二者合用则恰好满足该步骤的条件。

形状所给出的那条等式，正是封闭性所需要的那一条，二者逐字相同，故中间无需任何东西即可衔接。这不是巧合：两者都是对「带元数标签的对」按同一条读法写下的。

```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))))))))))
```

## 闭包具有形状

这条谓词有什么用。对码的递归得到一个索引集，而那个集合必须封闭，否则诸子句什么也约束不了；也必须成形，否则它们会把垃圾放进来。封闭性已在一章之前为闭包给出；这里是另一半，而且较短，因为成形性对「一个成员含有哪些子成员」不作任何要求。于是那个反演所返回的东西有一半被弃置不用。

这里只需按构造子分情形。标签不是另一个需要匹配的索引；它由构造子计算，正如 `byTag` 从构造子计算封闭性要求。因此，这张表只有十行，而非十乘十。这里也没有递归：指定构造子后，其键已经计算为见证类型要求的带元数标签的对，十个元组中都不需要任何搬运。

元组唯一算不出来的是词项见证：载荷位上放着的词项码必须被认证为词项码，而那份认证正是上面的编码式施于该构造子所携的词项。这份认证如今有了第二半，由调用方提供：字母表的每个常元都是载体的成员。它是一条假设，每次调用提供一次，而不是每个构造子提供一次，因为字母表早在公式之前就已固定。

另一方面，第一半变得更容易了。一个词项所需的见证是「它的码是**某个**词项的码」，而在字母表之上，一个词项的码本来就是这个：编码式就是恒等，旁边配一个 `refl`。若在模型自己的编码上，则它还得先在两套编码之间建立对应。

```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))))))))))))
```