---
title: "封闭码定义域的可靠性与完备性"
module: L.Coding.CodeDomainAdequacy
lang: zh
site: "Bedrock"
description: "封闭码定义域的可靠性与完备性"
stage: "证明 GCH"
reading_order: 99
canonical: https://bedrock.institute/zh/L.Coding.CodeDomainAdequacy.html
html: L.Coding.CodeDomainAdequacy.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/CodeDomainAdequacy.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Environment, L.Coding.EnvironmentSet, L.Axioms.Numerals, L.Coding.Model, L.Coding.Expressions, L.Coding.Quantification, L.Coding.EnvironmentTower, L.Coding.CodeDomain, L.Coding.CodeAlphabet, L.Coding.Closure, L.Coding.CodeShape, L.Coding.CodeSet, L.Ordinal]
routes: [gch-descriptions]
translations: [https://bedrock.institute/en/L.Coding.CodeDomainAdequacy.md, https://bedrock.institute/ja/L.Coding.CodeDomainAdequacy.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
关于语法的内部论证从 `L` 中的一组公式键开始。本章从两个方向比较候选码域与外部公式文法：域中每个成员都纯粹地可解码为某条公式的键，而每条真实公式的键都属于该域。这些结论只涉及码的隶属，不涉及被编码公式的真值或满足关系。

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

以下论证同时使用排中律与命题截断。命题截断只记录解码见证的存在，而不从中选定一个见证；只有当目标仍是命题时，才能消去这层截断。

```agda
open import Base.Prelude
open import Base.Classical using ( LEM )
```

假设 `lem : LEM (ℓ-suc ℓ)`。本章的所有构造都相对于这一假设展开，但它并不加强解码结论：解码得到的公式见证仍处于命题截断之中。

```agda
module L.Coding.CodeDomainAdequacy {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

本章谈论集合论的完整一阶语言：公式既含无界量词也含两个有界量词，词项由变元与常元建成。这些正是码域必须收集并描述的对象。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; Term; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∃̇∈; ∀̇∈ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

公式键是嵌套的有序对，因此有序对编码的单射性可从键的相等中恢复元数、标签与载荷。自然数元数由冯·诺伊曼数码表示，可构造环境集则为有限参数向量提供内部表示。

```agda
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; #mono )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Environment {ℓ} using ( env )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )
open import L.Axioms.Numerals {ℓ} using ( numeralL-fst; sucʟ; sucʟ-fst )
```

对象语言能够表达按结构组装的键属于候选域。有序对表达式构造嵌套键，其充分性定理则把所得公式的满足与对应宿主层有序对码的隶属等同起来。

```agda
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate )
open import L.Coding.Expressions {ℓ} using ( sucAtL )
open import L.Coding.Model {ℓ} using ( container )
import L.Coding.Expressions {ℓ} as CodingExpressions
module E = CodingExpressions.PairExpression
```

量词码会改变元数。无界与有界量词的主体都是后继元数处的键，而有界量词还携带一个在当前元数处合法的词项。关于配对、后继与扩展环境的语义引理恰好表达这些约束子下的变化。

```agda
open import L.Coding.Quantification {ℓ} using
  ( i0; i1; i2; i3; i4; i5; i6; i7; i8; sh
  ; pr-out; pr-in; down; fstS; sndS; suc-out; suc-in
  ; sndEx; sndAll; bothEx
  ; sndEx-out; sndAll-in; bothEx-out; bothAll-in
```

存在载荷的描述采用命题截断，有时包含两层嵌套见证；其向内与向外读法都保持这一截断。十个构造子标签由零至九的数码表示，另有一座环境塔记录每个码被读取时的元数。

```agda
  ; fillSnd; fillBoth; useSnd; useBoth
  ; f0; f1; f2; f3; f4; f5; f6; f7; f8; f9
  ; bigOr-in; bigOr-out )
open import L.Coding.EnvironmentTower {ℓ} lem using ( module Tower; nn )
open import L.Coding.CodeDomain {ℓ} using
```

描述 `codesAt` 有两个互补部分。`shapeAt` 把域中已有成员读成十种构造形状之一，并要求复合码的直接子键仍在域中。`closeAt` 沿生成方向陈述：合法词项与已有子键会产生相应的新键。

```agda
  ( isTm; keyUp; keyExpr; atomKeyExpr; bndKeyExpr
  ; unKey; binKey; atomKey; bndKey
  ; Tags; shN; module Shape; shapeAt; module Close; closeAt; codesAt )
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet )
```

构造子标签是 `Fin 10` 的元素；其自然数值选取十个载荷谓词之一，并自动小于十。环境是有限向量，而层级中存放的码则是嵌套的集合论有序对。

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( toℕ<n )
open import Cubical.Data.Vec using ( _∷_; lookup )
open import Cubical.Data.Sigma using ( _×_ )
```

解码按互斥的构造情形分支，并常常只返回命题截断的见证。对的等式按分量搬运，不可能的标签则导向空类型。这些操作都不会把纯粹存在的公式提升为全局选定的解码器。

```agda
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.Prelude using ( subst2 )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

累积层级提供集合值的有序对码、冯·诺伊曼数码以及元数的后继运算。隶属具有小纤维表示，而层级中集合的相等是命题；这些事实使截断分解及其到隶属或相等结论的消去成立。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; sucV )
```

可构造结构的载体被固定为 `S`，以下每个环境与每条公式读法都居于其上。

```agda
open hPropStructure 𝒮ʟ using ( S )
```

所有码描述都在 `L` 所承载的一阶结构中解释。因此，「这个组装出的键属于 `C`」既可以写成对象语言公式，也可以读作宿主层的隶属陈述；充分性引理把同一断言的这两种形式等同起来。

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

## 读取描述

先描述词项码。集合 `t` 是元数 `ar` 处的词项码，当它「仅仅」是：标签零与工作集 `Wv` 中一个元素组成的对，或标签一与集合 `ar` 中一个元素组成的对。注意此处 `ar` 仍是任意集合；只有当已知它是数码时，第二支才恢复出一个有界变元索引。

```agda
IsTmV : V ℓ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
IsTmV Wv t ar = ∥ (Σ[ x ∈ V ℓ ] ((t ≡ pr (# 0) x) × ⟨ x ∈ Wv ⟩))
                ⊎ (Σ[ i ∈ V ℓ ] ((t ≡ pr (# 1) i) × ⟨ i ∈ ar ⟩)) ∥₁
```

前三类载荷谓词分别对应原子公式、二元联结词与假。原子载荷纯粹地分解为两个合法词项码；二元载荷纯粹地分解为候选域中两个同元数子键；假的载荷则直接是等式 `r = # 0`，不含存在见证。

```agda
module CodesSem (Wv Cv : V ℓ) where
  AtomP BinP ConP QuP BqP : V ℓ → V ℓ → Type (ℓ-suc ℓ)
  AtomP ar r = ∥ Σ[ t ∈ V ℓ ] Σ[ u ∈ V ℓ ] ((r ≡ pr t u) × (IsTmV Wv t ar × IsTmV Wv u ar)) ∥₁
  BinP ar r = ∥ Σ[ a ∈ V ℓ ] Σ[ b ∈ V ℓ ] ((r ≡ pr a b) × (⟨ pr ar a ∈ Cv ⟩ × ⟨ pr ar b ∈ Cv ⟩)) ∥₁
  ConP ar r = r ≡ # 0
```

量词载荷补全了这份清单。无界量词的载荷是后继元数处的子键；有界量词的载荷还把一个在当前元数处合法的词项码与这样的子键配成一对。这种不对称来自文法本身：主体具有后继元数，界词项则具有被量化公式的元数。

```agda
  QuP ar r = ⟨ pr (sucV ar) r ∈ Cv ⟩
  BqP ar r = ∥ Σ[ t ∈ V ℓ ] Σ[ a ∈ V ℓ ] ((r ≡ pr t a) × (IsTmV Wv t ar × ⟨ pr (sucV ar) a ∈ Cv ⟩)) ∥₁
```

载荷表开始：标签零与一承载两种原子形状，标签二与三承载合取与析取的二元形状。

```agda
  PayN : ℕ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
  PayN 0 = AtomP
  PayN 1 = AtomP
  PayN 2 = BinP
  PayN 3 = BinP
```

表继续：标签四承载蕴涵，标签五承载常假，标签六与七承载两个无界量词，标签八承载有界全称。

```agda
  PayN 4 = BinP
  PayN 5 = ConP
  PayN 6 = QuP
  PayN 7 = QuP
  PayN 8 = BqP
```

标签九承载有界存在量词的载荷。辅助族 `PayN` 在每个不小于十的自然数处都是空类型，但合法 `Key` 的标签取自 `Fin 10`；因此键中只可能出现零至九这十种情形。

```agda
  PayN 9 = BqP
  PayN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) _ _ = Empty.⊥*
```

元数 `ar` 处的键「仅仅」是十个标签之一连同匹配形状的载荷。注意键不是什么：它不是归纳的语法树，其分解也不被主张为唯一数据。键只是「一个集合编码的对可拆成十种已知形状之一」的截断证据。

```agda
  Key : V ℓ → V ℓ → Type (ℓ-suc ℓ)
  Key ar p = ∥ Σ[ k ∈ Fin 10 ] Σ[ r ∈ V ℓ ] ((p ≡ pr (# (toℕ k)) r) × PayN (toℕ k) ar r) ∥₁
```

固定一个环境，其中含候选词项码 `t`、元数集合 `ar`、工作集 `Wv`，以及两个已知分别为数码零和一的元素。在这些标签等式下，对象语言谓词 `isTm` 可与外围谓词 `IsTmV Wv t ar` 作精确比较。

```agda
module _ {k : ℕ} (t ar w N0 N1 : Fin k) (δ : S ^ k)
  (q0 : fst (lookup N0 δ) ≡ # 0) (q1 : fst (lookup N1 δ) ≡ # 1) where
  private
    Wv = fst (lookup w δ)
```

向外读法消去对象语言公式的截断析取。常元支中，存在量词恢复对的第二分量，数码等式对齐标签，隶属则进入 `IsTmV`；结果即截断定义的左支。

```agda
  isTm-out : ⟨ δ ⊨ isTm t ar w N0 N1 ⟩ → IsTmV Wv (fst (lookup t δ)) (fst (lookup ar δ))
  isTm-out = PT.rec squash₁
    (λ { (inl h) → PT.map
           (λ { (v , s , (e , v∈)) → inl (fst v , (e ∙ cong (λ a → pr a (fst v)) q0 , v∈)) })
           (sndEx-out t N0 (var i0 ∈̇ var (sh 2 w)) δ h)
```

变元支以数码一与元数集合重复同样三步，产出右支。两支合起来说明：对象语言的识别与集合层面的 `IsTmV` 恰好等价。

```agda
       ; (inr h) → PT.map
           (λ { (v , s , (e , v∈)) → inr (fst v , (e ∙ cong (λ a → pr a (fst v)) q1 , v∈)) })
           (sndEx-out t N1 (var i0 ∈̇ var (sh 2 ar)) δ h) })
```

向内读法反向执行同一转换。常元支中，填充引理把见证 `x` 置于零号槽的存在量词之下，而对等式沿反向的数码等式运输，使满足与对象语言公式的形状相合。

```agda
  isTm-in : IsTmV Wv (fst (lookup t δ)) (fst (lookup ar δ)) → ⟨ δ ⊨ isTm t ar w N0 N1 ⟩
  isTm-in = PT.rec (snd (δ ⊨ isTm t ar w N0 N1))
    (λ { (inl (x , (e , x∈))) →
           ∣ inl (fillSnd t δ (lookup N0 δ) (down (lookup w δ) x x∈)
                    (e ∙ cong (λ a → pr a x) (sym q0)) (var i0 ∈̇ var (sh 2 w)) x∈ N0 refl) ∣₁
```

变元支在数码一槽位的存在量词下填充见证 `i`，由相应的反向等式运输。两条支线双向闭合该等价。

```agda
       ; (inr (i , (e , i∈))) →
           ∣ inr (fillSnd t δ (lookup N1 δ) (down (lookup ar δ) i i∈)
                    (e ∙ cong (λ a → pr a i) (sym q1)) (var i0 ∈̇ var (sh 2 ar)) i∈ N1 refl) ∣₁ })
```

谓词 `keyUp C ar r` 精确表达一条隶属：有序对 `(suc ar,r)` 属于 `C`。它用有界存在量词选出 `C` 的一个实际成员，再逐层显露该成员，以验证其配对形状与后继等式。

```agda
module _ {k : ℕ} (C ar r : Fin k) (δ : S ^ k) where
  keyUp-out : ⟨ δ ⊨ keyUp C ar r ⟩ → ⟨ pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ) ⟩
  keyUp-out = PT.rec (snd (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ)))
    (λ { (c' , (c'∈ , h)) → PT.rec (snd (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ)))
      (λ { (s , (s∈ , h')) → PT.rec (snd (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ)))
```

向外读取时，配对公式把选出的 `C` 成员认作 `(ar',r)`，后继公式再把 `ar'` 认作 `suc ar`。沿这两条等式搬运隶属，便得到 `(suc ar,r) ∈ C`。所有截断见证都只消去到这条隶属命题中。

```agda
        (λ { (ar' , (ar'∈ , (e , hs))) →
          subst (λ u → ⟨ u ∈ fst (lookup C δ) ⟩)
            (pr-out i2 i0 (sh 3 r) (ar' ∷ s ∷ c' ∷ δ) e
             ∙ cong (λ a → pr a (fst (lookup r δ))) (suc-out (sh 3 ar) i0 (ar' ∷ s ∷ c' ∷ δ) hs))
            c'∈ })
```

因此，三层有界见证只用于证明所展示的对象确为 `C` 的成员；消去其截断后，`keyUp-out` 得到的恰是外围隶属陈述 `(suc ar,r) ∈ C`。

```agda
        h' })
      h })
```

向内读取时，从 `(suc ar,r) ∈ C` 出发。把后继元数呈现为可构造集合，将它与 `r` 组成的有序对打包，再以这些对象充当三层有界见证；配对公式与后继公式由此重建 `keyUp C ar r` 的满足。

```agda
  keyUp-in : ⟨ pr (sucV (fst (lookup ar δ))) (fst (lookup r δ)) ∈ fst (lookup C δ) ⟩ → ⟨ δ ⊨ keyUp C ar r ⟩
  keyUp-in h = ∣ c' , (h , ∣ c .fst , (c .snd .fst , ∣ ar' , (c .snd .snd .fst
    , ( pr-in i2 i0 (sh 3 r) (ar' ∷ c .fst ∷ c' ∷ δ) (sym (cong (λ a → pr a (fst (lookup r δ))) (sucʟ-fst (lookup ar δ))))
      , suc-in (sh 3 ar) i0 (ar' ∷ c .fst ∷ c' ∷ δ) (sucʟ-fst (lookup ar δ)) )) ∣₁) ∣₁) ∣₁
    where
```

具体地，`ar'` 表示 `suc ar`，`c'` 表示 `C` 的成员 `(suc ar,r)`，而与 `c'` 一同给出的包含集则见证公式所用的有界隶属链。它们的底层集合等式保证内部见证确实表示预期的外围有序对。

```agda
    ar' : S
    ar' = sucʟ (lookup ar δ)
    c' : S
    c' = down (lookup C δ) (pr (sucV (fst (lookup ar δ))) (fst (lookup r δ))) h
    c = container c' ar' (lookup r δ) (cong (λ a → pr a (fst (lookup r δ))) (sym (sucʟ-fst (lookup ar δ))))
```

固定候选域 `C`、元数值 `A`、标签值 `N` 与载荷 `a`。由这些数据组装的一元键是嵌套有序对 `(A,(N,a))`。

```agda
module _ {k : ℕ} (C ar N a : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)
```

`unKey` 的向外读法精确说明嵌套键 `(A,(N,a))` 属于 `C`。有序对表达式的充分性把对象语言中的隶属转换为这条宿主层集合隶属陈述。

```agda
  unKey-out : ⟨ δ ⊨ unKey C ar N a ⟩ → ⟨ pr A (pr Nv (fst (lookup a δ))) ∈ Cv ⟩
  unKey-out = E.member-out (keyExpr ar N (E.slot a)) (var C) δ
```

充分性也可反向使用：由 `(A,(N,a)) ∈ C` 可以得到对象语言谓词 `unKey` 的满足。因此，这条键子句与其宿主层读法双向一致。

```agda
  unKey-in : ⟨ pr A (pr Nv (fst (lookup a δ))) ∈ Cv ⟩ → ⟨ δ ⊨ unKey C ar N a ⟩
  unKey-in = E.member-in (keyExpr ar N (E.slot a)) (var C) δ
```

对二元构造子，固定两个载荷分量 `a` 与 `b`。它们组成的有序对 `P=(a,b)` 成为键 `(A,(N,P))` 的载荷；元数与标签仍占据和一元情形相同的外层位置。

```agda
module _ {k : ℕ} (C ar N a b : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)
```

两个实参值组成有序对 `P = (a,b)`。该有序对就是嵌套二元键 `(A,(N,P))` 的载荷。

```agda
    P = pr (fst (lookup a δ)) (fst (lookup b δ))
```

`binKey` 的向外读法恰为隶属 `(A,(N,(a,b))) ∈ C`。它保持编码的三个逻辑层次：元数、构造子标签与成对实参。

```agda
  binKey-out : ⟨ δ ⊨ binKey C ar N a b ⟩ → ⟨ pr A (pr Nv P) ∈ Cv ⟩
  binKey-out = E.member-out (keyExpr ar N (E.pair (E.slot a) (E.slot b))) (var C) δ
```

向内读法是其反向；与每条键子句一样，二者把公式陈述与集合隶属等同。

```agda
  binKey-in : ⟨ pr A (pr Nv P) ∈ Cv ⟩ → ⟨ δ ⊨ binKey C ar N a b ⟩
  binKey-in = E.member-in (keyExpr ar N (E.pair (E.slot a) (E.slot b))) (var C) δ
```

原子键以两个词项码为载荷。每个词项码都带有自己的词项标签与实参；两个词项码组成一对，再置于原子构造子标签和共同元数之下。

```agda
module _ {k : ℕ} (C ar N Nx x Ny y : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)
```

把两个词项码写作 `T=(Nx,x)` 与 `U=(Ny,y)`。此处 `Nx`、`Ny` 仍是环境中的任意标签值；在实例化原子封闭情形时，才要求它们为零或一。

```agda
    T = pr (fst (lookup Nx δ)) (fst (lookup x δ))
    U = pr (fst (lookup Ny δ)) (fst (lookup y δ))
```

原子子句的向外读法是 `(A,(N,(T,U))) ∈ C`，其中 `T`、`U` 为两个词项码。因此，最外层有序对记录元数，下一层记录原子标签，最内层有序对记录两个词项。

```agda
  atomKey-out : ⟨ δ ⊨ atomKey C ar N Nx x Ny y ⟩ → ⟨ pr A (pr Nv (pr T U)) ∈ Cv ⟩
  atomKey-out = E.member-out (atomKeyExpr ar N Nx x Ny y) (var C) δ
```

向内读法是其反向；与此前每条键子句一样，原子情形双向闭合。

```agda
  atomKey-in : ⟨ pr A (pr Nv (pr T U)) ∈ Cv ⟩ → ⟨ δ ⊨ atomKey C ar N Nx x Ny y ⟩
  atomKey-in = E.member-in (atomKeyExpr ar N Nx x Ny y) (var C) δ
```

有界量词键的载荷含两种不同分量：表示界的词项码，以及表示主体的子公式码。共同的外层数据仍是当前元数 `A` 与有界量词标签 `N`。

```agda
module _ {k : ℕ} (C ar N Nx x a : Fin k) (δ : S ^ k) where
  private
    Cv = fst (lookup C δ)
    A = fst (lookup ar δ)
    Nv = fst (lookup N δ)
```

把界词项码写作 `T=(Nx,x)`，把主体码写作 `Av`。词项在当前元数处检查，而主体键在后继元数处检查；把二者保留为不同载荷分量，正好记录这一文法不对称性。

```agda
    T = pr (fst (lookup Nx δ)) (fst (lookup x δ))
    Av = fst (lookup a δ)
```

有界键子句的向外读法是 `(A,(N,(T,Av))) ∈ C`。最内层有序对依次含界词项码与主体码；这条隶属本身并不断言任一分量已经合法。

```agda
  bndKey-out : ⟨ δ ⊨ bndKey C ar N Nx x a ⟩ → ⟨ pr A (pr Nv (pr T Av)) ∈ Cv ⟩
  bndKey-out = E.member-out (bndKeyExpr ar N Nx x a) (var C) δ
```

反过来，`(A,(N,(T,Av)))` 属于 `C` 可推出 `bndKey` 的满足。两条读法合起来只建立结构隶属的等价；`T` 的合法性与 `Av` 在后继元数处的隶属由外围载荷谓词另行给出。

```agda
  bndKey-in : ⟨ pr A (pr Nv (pr T Av)) ∈ Cv ⟩ → ⟨ δ ⊨ bndKey C ar N Nx x a ⟩
  bndKey-in = E.member-in (bndKeyExpr ar N Nx x a) (var C) δ
```

现固定候选码域 `C`、工作集 `W`，以及十个已被证明分别为零至九数码的环境元素。于是，对每个标签，都可把对象语言载荷描述与相应的外围谓词 `AtomP`、`BinP`、`ConP`、`QuP` 或 `BqP` 比较。

```agda
module PayRead {m : ℕ} (C w : Fin m) (N : Fin 10 → Fin m) (δ : S ^ (9 + m))
  (tg : Tags δ (shN 9 N)) where
  private
    Cv = fst (lookup (sh 9 C) δ)
    Wv = fst (lookup (sh 9 w) δ)
```

在每条载荷读法中，`A` 表示所记录的元数，`R` 表示原始载荷。零与一的标签等式被单独取出，因为原子载荷和有界量词载荷都必须识别词项码，而词项恰有使用这两个标签的两种合法形状。

```agda
    A = fst (lookup i5 δ)
    R = fst (lookup i0 δ)
    q0 = tg f0
    q1 = tg f1
    rS = lookup i0 δ
```

比较的两侧使用相同的底层集合 `Wv` 与 `Cv`。因此，句法载荷公式所描述的 `Wv` 中词项隶属与 `Cv` 中子键隶属，恰好对应五个外围载荷谓词的参数。

```agda
    module Sh = Shape C w N
  open CodesSem Wv Cv
```

原子载荷体要求载荷的两个分量都在所记录元数处满足词项码谓词。二元载荷体则要求两个分量都作为该同一元数的键出现在候选域中。尽管两种载荷都编码为有序对，这两项条件并不相同。

```agda
  private
    tmBody : Formula S (12 + m)
    tmBody = isTm i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) ∧̇ isTm i0 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1))
    binBody : Formula S (12 + m)
    binBody = appAt (sh 12 C) i8 i1 ∧̇ appAt (sh 12 C) i8 i0
```

最后一种载荷形状涵盖两个有界量词。其主体要求作为界的词项在当前元数处合法，并要求主体的键在后继元数处属于码集。

```agda
    bqBody : Formula S (12 + m)
    bqBody = isTm i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) ∧̇ keyUp (sh 12 C) i8 i0
```

向外读取原子载荷时，消去两层存在量词，得到词项 `t`、`u`、等式 `R ≡ pr t u`，以及二者在元数 `A` 处合法的证明。词项读式利用零与一的标签等式，把两份满足证明转换为相应的截断词项形状。

```agda
  atom-out : ⟨ δ ⊨ Sh.atomPay ⟩ → AtomP A R
  atom-out h = PT.map
    (λ { (t , u , s , (e , (ht , hu))) → fst t , fst u
       , ( e , ( isTm-out i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) (u ∷ t ∷ s ∷ δ) q0 q1 ht
               , isTm-out i0 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) (u ∷ t ∷ s ∷ δ) q0 q1 hu ) ) })
```

这一消耗本身就是对双重存在消去的一次应用：抽出见证 `t`、`u` 与容器，然后把余下的合取兑现为载荷数据。

```agda
    (bothEx-out i0 tmBody δ h)
```

向内读取则从数据重建满足。两份截断的合法证明被消去，因为目标仍是截断的满足；两个词项各自经移位语境进入其合法原子。

```agda
  atom-in : AtomP A R → ⟨ δ ⊨ Sh.atomPay ⟩
  atom-in = PT.rec (snd (δ ⊨ Sh.atomPay))
    (λ { (t , u , (e , (ht , hu))) →
      fillBoth i0 δ (fstS rS t u e) (sndS rS t u e) e tmBody
        ( isTm-in i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) (δ12 t u e) q0 q1 ht
```

第二份合法性证明以同样方式填入。辅助环境 `δ12` 依次包含由 `R ≡ pr t u` 选出的两个分量、见证这次配对的容器以及原环境；两个词项原子正是在这个环境中解释的。

```agda
        , isTm-in i0 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) (δ12 t u e) q0 q1 hu ) })
    where
    δ12 : (t u : V ℓ) (e : R ≡ pr t u) → S ^ (12 + m)
    δ12 t u e = sndS rS t u e ∷ fstS rS t u e ∷ container rS (fstS rS t u e) (sndS rS t u e) e .fst ∷ δ
```

向外读取二元载荷得到载荷 `a`、`b`、等式 `R ≡ pr a b`，以及 `pr A a` 与 `pr A b` 都属于码集的证明。两个应用原子的充分性在扩展环境中识别出这两份隶属关系。

```agda
  bin-out : ⟨ δ ⊨ Sh.binPay ⟩ → BinP A R
  bin-out h = PT.map
    (λ { (a , b , s , (e , (ha , hb))) → fst a , fst b
       , ( e , ( subst ⟨_⟩ (appAt-adequate (sh 12 C) i8 i1 (b ∷ a ∷ s ∷ δ)) ha
               , subst ⟨_⟩ (appAt-adequate (sh 12 C) i8 i0 (b ∷ a ∷ s ∷ δ)) hb ) ) })
```

与原子情形一样，二元条件的两层存在量词由一次消去处理。

```agda
    (bothEx-out i0 binBody δ h)
```

向内读取则以被点名的子码填入两层存在量词。两个应用原子沿充分性反方向传输，回到移位语境之中而得到满足。

```agda
  bin-in : BinP A R → ⟨ δ ⊨ Sh.binPay ⟩
  bin-in = PT.rec (snd (δ ⊨ Sh.binPay))
    (λ { (a , b , (e , (ha , hb))) →
      fillBoth i0 δ (fstS rS a b e) (sndS rS a b e) e binBody
        ( subst ⟨_⟩ (sym (appAt-adequate (sh 12 C) i8 i1 (δ12 a b e))) ha
```

二元情形的辅助定义记录同样的移位语境形状，此时由两个外围值 `a` 与 `b` 构造。

```agda
        , subst ⟨_⟩ (sym (appAt-adequate (sh 12 C) i8 i0 (δ12 a b e))) hb ) })
    where
    δ12 : (a b : V ℓ) (e : R ≡ pr a b) → S ^ (12 + m)
    δ12 a b e = sndS rS a b e ∷ fstS rS a b e ∷ container rS (fstS rS a b e) (sndS rS a b e) e .fst ∷ δ
```

假的载荷不含下级数据。其公式说 `R` 等于零标签槽位中的值，而 `ConP A R` 说 `R ≡ # 0`；与零标签等式复合便得到向外方向。

```agda
  con-out : ⟨ δ ⊨ Sh.conPay ⟩ → ConP A R
  con-out h = h ∙ q0
```

反过来，等式 `R ≡ # 0` 与零标签等式的逆向复合，证明 `R` 等于零标签槽位中的值；这正是假载荷的满足。

```agda
  con-in : ConP A R → ⟨ δ ⊨ Sh.conPay ⟩
  con-in h = h ∙ sym q0
```

对任一无界量词，载荷都是后继元数处的主体键。后继键读式把这份载荷公式的满足转换为 `pr (sucV A) R` 属于码集。

```agda
  qu-out : ⟨ δ ⊨ Sh.quPay ⟩ → QuP A R
  qu-out = keyUp-out (sh 9 C) i5 i0 δ
```

反向上，`pr (sucV A) R` 属于码集为后继键公式提供所需见证，因而证明量词载荷。

```agda
  qu-in : QuP A R → ⟨ δ ⊨ Sh.quPay ⟩
  qu-in = keyUp-in (sh 9 C) i5 i0 δ
```

向外读取有界量词载荷得到词项 `t`、主体载荷 `a` 与等式 `R ≡ pr t a`。同时还得到 `t` 在元数 `A` 处合法，以及主体键 `pr (sucV A) a` 属于码集。

```agda
  bq-out : ⟨ δ ⊨ Sh.bqPay ⟩ → BqP A R
  bq-out h = PT.map
    (λ { (t , a , s , (e , (ht , ha))) → fst t , fst a
       , ( e , ( isTm-out i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) (a ∷ t ∷ s ∷ δ) q0 q1 ht
               , keyUp-out (sh 12 C) i8 i0 (a ∷ t ∷ s ∷ δ) ha ) ) })
```

有界主体的两层存在量词与其他情形一样，由同一个双重消去处理。

```agda
    (bothEx-out i0 bqBody δ h)
```

向内读取时，界限词项经移位语境进入其合法性原子。

```agda
  bq-in : BqP A R → ⟨ δ ⊨ Sh.bqPay ⟩
  bq-in = PT.rec (snd (δ ⊨ Sh.bqPay))
    (λ { (t , a , (e , (ht , ha))) →
      fillBoth i0 δ (fstS rS t a e) (sndS rS t a e) e bqBody
        ( isTm-in i1 i8 (sh 12 w) (sh 12 (N f0)) (sh 12 (N f1)) (δ12 t a e) q0 q1 ht
```

主体键经后继键引理进入；辅助定义记录由界限取值及其容器构造的移位语境。

```agda
        , keyUp-in (sh 12 C) i8 i0 (δ12 t a e) ha ) })
    where
    δ12 : (t a : V ℓ) (e : R ≡ pr t a) → S ^ (12 + m)
    δ12 t a e = sndS rS t a e ∷ fstS rS t a e ∷ container rS (fstS rS t a e) (sndS rS t a e) e .fst ∷ δ
```

标签的读式按标签递归选择。标签零与一是两条原子，标签二、三、四是三种二元联结词。

```agda
  payN-out : (k : ℕ) → ⟨ δ ⊨ Sh.payN k ⟩ → PayN k A R
  payN-out 0 = atom-out
  payN-out 1 = atom-out
  payN-out 2 = bin-out
  payN-out 3 = bin-out
```

标签五、六、七覆盖假与两个无界量词；标签八是有界全称。

```agda
  payN-out 4 = bin-out
  payN-out 5 = con-out
  payN-out 6 = qu-out
  payN-out 7 = qu-out
  payN-out 8 = bq-out
```

标签九是有界存在。标签十及以上不指名任何构造子：其载荷为空，读式就是这份空数据上的恒等。

```agda
  payN-out 9 = bq-out
  payN-out (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) h = h
```

向内读式按同样的递归选择，每个标签一条子句。

```agda
  payN-in : (k : ℕ) → PayN k A R → ⟨ δ ⊨ Sh.payN k ⟩
  payN-in 0 = atom-in
  payN-in 1 = atom-in
  payN-in 2 = bin-in
  payN-in 3 = bin-in
```

标签四至七继续这份清单：最后一个二元联结词、假，以及两个无界量词。

```agda
  payN-in 4 = bin-in
  payN-in 5 = con-in
  payN-in 6 = qu-in
  payN-in 7 = qu-in
  payN-in 8 = bq-in
```

标签九补全清单；十以上无可读取，因为没有合法的键携带这样的标签。

```agda
  payN-in 9 = bq-in
  payN-in (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) h = h
```

十路读式在外围环境之上的七条目扩展中解释带标签的载荷。它从外围条目读取码集与常元字母表，而 `N` 选出外围环境中的十个位置；标签假设把这些位置的值分别等同于数码零至九。

```agda
module TenRead {m : ℕ} (C w : Fin m) (N : Fin 10 → Fin m) (δ : S ^ (7 + m))
  (tg : Tags δ (shN 7 N)) where
  private
    Cv = fst (lookup (sh 7 C) δ)
    Wv = fst (lookup (sh 7 w) δ)
```

在新绑定的条目中，`A` 是元数，`P` 是要识别为键的带标签载荷。保留 `P` 的集合层表示后，选定标签及其载荷 `r` 时便可实现等式 `P ≡ pr (# (toℕ j)) r`。

```agda
    A = fst (lookup i3 δ)
    P = fst (lookup i0 δ)
    pS = lookup i0 δ
    module Sh = Shape C w N
  open CodesSem Wv Cv
```

标签读式把第 `j` 个标签原子的满足转换为一把键。截断的见证由索引 `r` 与容器配对；编码等式沿标签等式传输。这个等式表明，第 `j` 个标签槽位点名的正是 `j` 的数码；载荷则由标签 `j` 处的读式读取。

```agda
  at-out : (j : Fin 10) → ⟨ δ ⊨ Sh.at j ⟩ → Key A P
  at-out j h = PT.map
    (λ { (r , s , (e , hp)) → j , fst r
       , ( e ∙ cong (λ a → pr a (fst r)) (tg j)
         , PayRead.payN-out C w N (r ∷ s ∷ δ) tg (toℕ j) hp ) })
```

标签原子的两层存在量词由其自身的消去处理，因此读式从不自行选择索引：它只拆开满足所提供的那一个。

```agda
    (sndEx-out i0 (sh 7 (N j)) (Sh.pay j) δ h)
```

向内方向由键构造满足：见证条目以移位后的取值填入，载荷在扩展语境上向内读取，而标签等式把命名槽位与 `j` 的数码等同起来。

```agda
  at-in : (j : Fin 10) (r : V ℓ) (e : P ≡ pr (# (toℕ j)) r) → PayN (toℕ j) A r → ⟨ δ ⊨ Sh.at j ⟩
  at-in j r e pay =
    fillSnd i0 δ (lookup (sh 7 (N j)) δ) rS e' (Sh.pay j)
      (PayRead.payN-in C w N (rS ∷ container pS (lookup (sh 7 (N j)) δ) rS e' .fst ∷ δ) tg (toℕ j) pay)
      (sh 7 (N j)) refl
```

改名后的取值把 `j` 的数码与所选条目配对；编码等式与标签等式反向复合，使扩展后的命名提到的正是那个槽位。

```agda
    where
    rS : S
    rS = sndS pS (# (toℕ j)) r e
    e' : P ≡ pr (fst (lookup (sh 7 (N j)) δ)) (fst rS)
    e' = e ∙ cong (λ a → pr a r) (sym (tg j))
```

十路向外读式消耗该析取，并在见证所指名的那个标签处引用标签读式。

```agda
  ten-out : ⟨ δ ⊨ Sh.ten ⟩ → Key A P
  ten-out h = PT.rec squash₁ (λ { (j , hj) → at-out j hj }) (bigOr-out δ 9 Sh.at h)
```

向内读式在见证到的标签处进入析取，载荷也在该标签处向内读取。两个方向合起来说：十路析取的满足，与携带一把合法键，是同一回事。

```agda
  ten-in : Key A P → ⟨ δ ⊨ Sh.ten ⟩
  ten-in = PT.rec (snd (δ ⊨ Sh.ten))
    (λ { (j , r , (e , pay)) → bigOr-in δ 9 Sh.at j (at-in j r e pay) })
```

形状读式固定三个外围集合：候选码集 `C`、常元字母表 `w`，以及由「元数与族」对组成的塔 `E`。三者的底层迭代集合分别用于码的隶属、常元词项的合法性，以及属于该塔的见证 `(ar,F)`。

```agda
module ShapeRead {m : ℕ} (C w E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Cv = fst (lookup C γ)
    Wv = fst (lookup w γ)
    Ev = fst (lookup E γ)
```

对选定的成员 `c` 与塔中见证 `(ar,F)`，余下公式选择载荷 `p`，要求 `c ≡ pr ar p`，并按十种可能的标签形状检验 `p`。这样，嵌套见证分别显露外层元数与内层带标签载荷。

```agda
    module Sh = Shape C w N
    inner : Formula S (5 + m)
    inner = sndEx i4 i1 Sh.ten
  open CodesSem Wv Cv
```

`Shaped c` 恰好记录形状子句抽出的数据：存在 `ar`、`F`、`p`，使得 `pr ar F` 属于 `E`、`c ≡ pr ar p`，且 `p` 是元数 `ar` 处合法的带标签载荷。所有存在数据都经过命题截断，并不声称分解唯一。

```agda
  Shaped : V ℓ → Type (ℓ-suc ℓ)
  Shaped c = ∥ Σ[ ar ∈ V ℓ ] Σ[ F ∈ V ℓ ] Σ[ p ∈ V ℓ ]
               (⟨ pr ar F ∈ Ev ⟩ × ((c ≡ pr ar p) × Key ar p)) ∥₁
```

对码集中的每个 `c`，向外读取先得到 `E` 的成员 `q`。分解 `q` 得到 `ar`、`F` 与等式 `q ≡ pr ar F`；内层存在量词再给出 `p`、等式 `c ≡ pr ar p`，以及十路载荷公式的满足。

```agda
  shape-out : ⟨ γ ⊨ shapeAt C w E N ⟩ → (c : S) → ⟨ fst c ∈ Cv ⟩ → Shaped (fst c)
  shape-out h c c∈ = PT.rec squash₁
    (λ { (q , (q∈ , hb)) → PT.rec squash₁
      (λ { (ar , F , s , (eq , hs)) → PT.map
        (λ { (p , s' , (ec , ht)) →
```

等式 `q ≡ pr ar F` 把已知的 `q` 属于 `E` 传输为 `pr ar F` 属于 `E`。同时保留关于 `c` 的等式，并由十路读式把余下的满足证明转换为 `Key ar p`。

```agda
          fst ar , fst F , fst p
          , ( subst (λ u → ⟨ u ∈ Ev ⟩) eq q∈
            , ( ec , TenRead.ten-out C w N (p ∷ s' ∷ F ∷ ar ∷ s ∷ q ∷ c ∷ γ) tg ht ) ) })
        (sndEx-out i4 i1 Sh.ten (F ∷ ar ∷ s ∷ q ∷ c ∷ γ) hs) })
      (bothEx-out i0 inner (q ∷ c ∷ γ) hb) })
```

原形状满足对码集成员作全称量化。把它应用于 `c` 及其隶属证明，就得到上面所消去的存在数据，从而构造出 `Shaped (fst c)`。

```agda
    (h c c∈)
```

在向内方向，假设码集的每个成员 `c` 都有截断的形状数据。消去这份截断便得到 `ar`、`F`、`p`，连同 `pr ar F` 属于 `E`、关于 `c` 的等式及 `Key ar p`；目标本身是命题，因此可以作此消去。

```agda
  shape-in : ((c : S) → ⟨ fst c ∈ Cv ⟩ → Shaped (fst c)) → ⟨ γ ⊨ shapeAt C w E N ⟩
  shape-in k c c∈ = PT.rec (snd ((c ∷ γ) ⊨ ∃̇∈ (var (sh 1 E)) (bothEx i0 inner)))
    (λ { (ar , F , p , (q∈ , (ec , key))) →
      let qS = down (lookup E γ) (pr ar F) q∈
          arS = fstS qS ar F refl
```

`pr ar F` 属于 `E` 提供集合层表示 `qS`，其两个分量分别表示 `ar` 与 `F`。另一方面，等式 `c ≡ pr ar p` 在 `c` 内选出载荷的表示 `pS`。两个配对容器共同提供嵌套存在公式所需的环境。

```agda
          FS = sndS qS ar F refl
          δ2 = qS ∷ c ∷ γ
          cq = container qS arS FS refl
          δ5 = FS ∷ arS ∷ cq .fst ∷ δ2
          pS = sndS c ar p ec
```

内层公式以「元数与表」数据填充，十路析取以键填充，于是完整的形状满足由真实数据组装而成。

```agda
          cp = container c arS pS ec
          δ7 = pS ∷ cp .fst ∷ δ5
      in ∣ qS , ( q∈ , fillBoth i0 δ2 arS FS refl inner
            (fillSnd i4 δ5 arS pS ec Sh.ten
              (TenRead.ten-in C w N δ7 tg key) i1 refl) ) ∣₁ })
```

把所假设的形状赋值应用于 `c` 及其隶属，就恰好得到向内构造所用的截断见证。结合向外方向，这说明对码集的每个成员，形状公式的满足与命题 `Shaped` 相符。

```agda
    (k c c∈)
```

先把塔的一个成员分解为 `q ≡ pr ar F`，再解释各闭包子句。在所得的四条目扩展中，`A` 是固定元数 `ar`；码集与常元字母表仍从外围环境取得，标签等式在移位后仍然成立。

```agda
module CloseRead {m : ℕ} (C w : Fin m) (N : Fin 10 → Fin m) (δ : S ^ (4 + m)) (tg : Tags δ (shN 4 N)) where
  private
    Cv = fst (lookup (sh 4 C) δ)
    A = fst (lookup i1 δ)
    arS = lookup i1 δ
```

在这个固定元数处，闭包条件说：把十种构造子中的任意一种应用于具有所需形状的输入，结果仍属于码集。对每条子句，向外与向内读法都把其有界公式识别为相应的闭包性质。

```agda
    CS = lookup (sh 4 C) δ
    module Cl = Close C w N
```

向外读取原子闭包子句时，可任取属于 `X` 所选界的 `x`，再从以 `x` 扩展后的环境里任取属于 `Y` 所选界的 `y`。由此得到相应原子键属于码集；该键的元数为 `A`，构造子标签为 `k`，两个词项形状标签为 `Nx` 与 `Ny`。

```agda
  atomClose-out : (k Nx Ny : Fin 10) (X : Fin (4 + m)) (Y : Fin (5 + m))
                → ⟨ δ ⊨ Cl.atomClose k Nx Ny X Y ⟩
                → (x y : S) → ⟨ fst x ∈ fst (lookup X δ) ⟩ → ⟨ fst y ∈ fst (lookup Y (x ∷ δ)) ⟩
                → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (pr (# (toℕ Ny)) (fst y)))) ∈ Cv ⟩
  atomClose-out k Nx Ny X Y h x y x∈ y∈ =
```

该隶属沿三条标签等式传输：子句在带标签的槽位上陈述，而键则以三个标签的数码写出。

```agda
    subst (λ u → ⟨ u ∈ Cv ⟩)
      (cong (pr A) (cong₂ pr (tg k) (cong₂ pr (cong (λ a → pr a (fst x)) (tg Nx)) (cong (λ a → pr a (fst y)) (tg Ny)))))
      (atomKey-out (sh 6 C) i3 (sh 6 (N k)) (sh 6 (N Nx)) i1 (sh 6 (N Ny)) i0 (y ∷ x ∷ δ) (h x x∈ y y∈))
```

向内方向重建子句：既已给出对一切对的性质，只需在给定的 `x` 与 `y` 处实例化，并把命名等式反向运行。

```agda
  atomClose-in : (k Nx Ny : Fin 10) (X : Fin (4 + m)) (Y : Fin (5 + m))
               → ((x y : S) → ⟨ fst x ∈ fst (lookup X δ) ⟩ → ⟨ fst y ∈ fst (lookup Y (x ∷ δ)) ⟩
                  → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (pr (# (toℕ Ny)) (fst y)))) ∈ Cv ⟩)
               → ⟨ δ ⊨ Cl.atomClose k Nx Ny X Y ⟩
  atomClose-in k Nx Ny X Y g x x∈ y y∈ =
```

隶属沿反向改名被传输进带标签的槽位，闭包子句的引入规则随之完成这一情形。

```agda
    atomKey-in (sh 6 C) i3 (sh 6 (N k)) (sh 6 (N Nx)) i1 (sh 6 (N Ny)) i0 (y ∷ x ∷ δ)
      (subst (λ u → ⟨ u ∈ Cv ⟩)
        (sym (cong (pr A) (cong₂ pr (tg k) (cong₂ pr (cong (λ a → pr a (fst x)) (tg Nx)) (cong (λ a → pr a (fst y)) (tg Ny))))))
        (g x y x∈ y∈))
```

二元闭包子句量化码集中的两个成员 `c₁`、`c₂`。等式 `fst c₁ ≡ pr A (fst a)` 与 `fst c₂ ≡ pr A (fst b)` 显露它们在固定元数 `A` 处的载荷 `a`、`b`；子句随后断言以 `pr (fst a) (fst b)` 为载荷的二元键仍属于码集。

```agda
  binClose-out : (k : Fin 10) → ⟨ δ ⊨ Cl.binClose k ⟩
               → (c₁ c₂ a b : S) → ⟨ fst c₁ ∈ Cv ⟩ → ⟨ fst c₂ ∈ Cv ⟩
               → fst c₁ ≡ pr A (fst a) → fst c₂ ≡ pr A (fst b)
               → ⟨ pr A (pr (# (toℕ k)) (pr (fst a) (fst b))) ∈ Cv ⟩
  binClose-out k h c₁ c₂ a b c₁∈ c₂∈ e₁ e₂ =
```

该隶属沿标签的改名传输，两层嵌套的全称则由有界量词的消去引理兑现：每个条目都经由自己的配对容器进入内层子句。

```agda
    subst (λ u → ⟨ u ∈ Cv ⟩) (cong (pr A) (cong (λ v → pr v (pr (fst a) (fst b))) (tg k)))
      (binKey-out (sh 10 C) i7 (sh 10 (N k)) i3 i0 δ10
        (useSnd i0 δ8 arS b e₂ (binKey (sh 10 C) i7 (sh 10 (N k)) i3 i0) i5 refl
          (useSnd i0 (c₁ ∷ δ) arS a e₁ inner i2 refl (h c₁ c₁∈) c₂ c₂∈)))
    where
```

选定 `c₁` 并把它写成 `pr A a` 后，内层公式量化码集中的第二个码 `c₂`，并把它显露为 `pr A b`。随后要求由标签 `k` 与配对载荷 `pr a b` 形成的二元键属于码集；辅助环境记录 `c₁` 与 `c₂` 的两次分解。

```agda
    inner : Formula S (7 + m)
    inner = ∀̇∈ (var (sh 7 C)) (sndAll i0 i5 (binKey (sh 10 C) i7 (sh 10 (N k)) i3 i0))
    δ7 : S ^ (7 + m)
    δ7 = a ∷ container c₁ arS a e₁ .fst ∷ c₁ ∷ δ
    δ8 : S ^ (8 + m)
```

量词子句必须同时记住子键和决定其元数的数据。环境 `δ8` 包含候选实参 `a`、拟定的后继元数 `ar'`、见证二者关系的有序对以及子键 `c₁`；处理有界量词时，`δ10` 还加入充当界的词项。

```agda
    δ8 = c₂ ∷ δ7
    δ10 : S ^ (10 + m)
    δ10 = b ∷ container c₂ arS b e₂ .fst ∷ δ8
```

二元闭包子句的向内方向从相应的数学闭包规则出发：同一元数的两个子键若属于该域，由它们构成的复合键也属于该域。公式中的两层全称量化只是把所选的两个子键显式写出。

```agda
  binClose-in : (k : Fin 10)
              → ((c₁ c₂ a b : S) → ⟨ fst c₁ ∈ Cv ⟩ → ⟨ fst c₂ ∈ Cv ⟩
                 → fst c₁ ≡ pr A (fst a) → fst c₂ ≡ pr A (fst b)
                 → ⟨ pr A (pr (# (toℕ k)) (pr (fst a) (fst b))) ∈ Cv ⟩)
              → ⟨ δ ⊨ Cl.binClose k ⟩
```

依公式规定的次序引入两个量化分量，便得到相应的扩展环境。在最内层的蕴涵中，所假设的闭包规则给出复合键的隶属证明；标签等式 `tg k` 再把所展示的标签与 `binKey` 所要求的数码对齐。

```agda
  binClose-in k g c₁ c₁∈ = sndAll-in i0 i2 (∀̇∈ (var (sh 7 C)) (sndAll i0 i5 (binKey (sh 10 C) i7 (sh 10 (N k)) i3 i0))) (c₁ ∷ δ) (λ a s s∈ a∈ e₁ c₂ c₂∈ →
    sndAll-in i0 i5 (binKey (sh 10 C) i7 (sh 10 (N k)) i3 i0) (c₂ ∷ a ∷ s ∷ c₁ ∷ δ) (λ b s' s'∈ b∈ e₂ →
      binKey-in (sh 10 C) i7 (sh 10 (N k)) i3 i0 (b ∷ s' ∷ c₂ ∷ a ∷ s ∷ c₁ ∷ δ)
        (subst (λ u → ⟨ u ∈ Cv ⟩) (sym (cong (pr A) (cong (λ v → pr v (pr (fst a) (fst b))) (tg k))))
          (g c₁ c₂ a b c₁∈ c₂∈ e₁ e₂))))
```

假的编码没有需要检查的子码。因此，向外读取它的闭包子句，只需利用载荷等于零数码的等式，再沿标签等式运输。

```agda
  conClose-out : (k : Fin 10) → ⟨ δ ⊨ Cl.conClose k ⟩ → ⟨ pr A (pr (# (toℕ k)) (# 0)) ∈ Cv ⟩
  conClose-out k h =
    subst (λ u → ⟨ u ∈ Cv ⟩) (cong (pr A) (cong₂ pr (tg k) (tg f0)))
      (unKey-out (sh 4 C) i1 (sh 4 (N k)) (sh 4 (N f0)) δ h)
```

反过来，假键的隶属证明沿同一组等式反向运输，便得到闭包子句的满足。这个情形没有递归前提，因为零载荷已经完全确定了该键。

```agda
  conClose-in : (k : Fin 10) → ⟨ pr A (pr (# (toℕ k)) (# 0)) ∈ Cv ⟩ → ⟨ δ ⊨ Cl.conClose k ⟩
  conClose-in k h =
    unKey-in (sh 4 C) i1 (sh 4 (N k)) (sh 4 (N f0)) δ
      (subst (λ u → ⟨ u ∈ Cv ⟩) (sym (cong (pr A) (cong₂ pr (tg k) (tg f0)))) h)
```

无界量词子句的向外读法把被量化的分量显式给出：给定域的子键 `c₁`、呈现 `c₁ = pr ar' a` 与等式 `ar' = sucV A`，当前元数处的量词键便属于该域。这三条假设恰是前驱切片成员的全部数据。

```agda
  quClose-out : (k : Fin 10) → ⟨ δ ⊨ Cl.quClose k ⟩
              → (c₁ ar' a : S) → ⟨ fst c₁ ∈ Cv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
              → ⟨ pr A (pr (# (toℕ k)) (fst a)) ∈ Cv ⟩
  quClose-out k h c₁ ar' a c₁∈ e₁ es =
    subst (λ u → ⟨ u ∈ Cv ⟩) (cong (pr A) (cong (λ v → pr v (fst a)) (tg k)))
```

证明把 `a`、`ar'` 与容器加入环境，以后继等式进入蕴涵的结论，并在八槽环境中读取 `unKey` 的隶属。随后沿标签等式运输，得到由标签 `k` 所表示数码对应的隶属。

```agda
      (unKey-out (sh 8 C) i5 (sh 8 (N k)) i0 δ8
        (useBoth i0 (c₁ ∷ δ) ar' a e₁ (sucAtL i5 i1 ⇒̇ unKey (sh 8 C) i5 (sh 8 (N k)) i0) (h c₁ c₁∈)
          (suc-in i5 i1 δ8 es)))
    where
    δ8 : S ^ (8 + m)
```

扩展环境按蕴涵所读取的次序，把三个被量化的分量与原有分量打包在一起。

```agda
    δ8 = a ∷ ar' ∷ container c₁ ar' a e₁ .fst ∷ c₁ ∷ δ
```

向内读取时，先引入子句所量化的两个分量。扩展环境包含拟定的后继元数 `ar'` 与载荷 `a`，后继等式随后给出蕴涵的前提。

```agda
  quClose-in : (k : Fin 10)
             → ((c₁ ar' a : S) → ⟨ fst c₁ ∈ Cv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
                → ⟨ pr A (pr (# (toℕ k)) (fst a)) ∈ Cv ⟩)
             → ⟨ δ ⊨ Cl.quClose k ⟩
  quClose-in k g c₁ c₁∈ = bothAll-in i0 (sucAtL i5 i1 ⇒̇ unKey (sh 8 C) i5 (sh 8 (N k)) i0) (c₁ ∷ δ) (λ ar' a s s∈ ar'∈ a∈ e₁ hs →
```

对这些数据应用所假设的闭包规则，再沿标签等式运输所得隶属，便得到 `unKey` 的结论。无界量词子句的向内读法由此完成。

```agda
    unKey-in (sh 8 C) i5 (sh 8 (N k)) i0 (a ∷ ar' ∷ s ∷ c₁ ∷ δ)
      (subst (λ u → ⟨ u ∈ Cv ⟩) (sym (cong (pr A) (cong (λ v → pr v (fst a)) (tg k))))
        (g c₁ ar' a c₁∈ e₁ (suc-out i5 i1 (a ∷ ar' ∷ s ∷ c₁ ∷ δ) hs))))
```

有界量词子句多出一项前提。除了后继元数处的主体键，还需要一个在当前元数处合法的界词项 `x`；所得载荷以嵌套有序对依次记录量词标签、词项标签 `Nx`、该词项以及主体载荷。

```agda
  bqClose-out : (k Nx : Fin 10) (X : Fin (8 + m)) → ⟨ δ ⊨ Cl.bqClose k Nx X ⟩
              → (c₁ ar' a : S) → ⟨ fst c₁ ∈ Cv ⟩ → (e₁ : fst c₁ ≡ pr (fst ar') (fst a)) → fst ar' ≡ sucV A
              → (x : S) → ⟨ fst x ∈ fst (lookup X (a ∷ ar' ∷ container c₁ ar' a e₁ .fst ∷ c₁ ∷ δ)) ⟩
              → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (fst a))) ∈ Cv ⟩
  bqClose-out k Nx X h c₁ ar' a c₁∈ e₁ es x x∈ =
```

证明把界词项加入环境，并在该环境中应用有界键消去。两条标签等式分别对应量词构造子与词项构造子，它们把嵌套有序对运输到结论所指定的形状。

```agda
    subst (λ u → ⟨ u ∈ Cv ⟩)
      (cong (pr A) (cong₂ pr (tg k) (cong (λ v → pr v (fst a)) (cong (λ v → pr v (fst x)) (tg Nx)))))
      (bndKey-out (sh 9 C) i6 (sh 9 (N k)) (sh 9 (N Nx)) i0 i1 (x ∷ δ8)
        (useBoth i0 (c₁ ∷ δ) ar' a e₁ (sucAtL i5 i1 ⇒̇ ∀̇∈ (var X) (bndKey (sh 9 C) i6 (sh 9 (N k)) (sh 9 (N Nx)) i0 i1))
          (h c₁ c₁∈) (suc-in i5 i1 δ8 es) x x∈))
```

八槽环境重复无界情形的打包方式，而界槽由该消去消耗。

```agda
    where
    δ8 : S ^ (8 + m)
    δ8 = a ∷ ar' ∷ container c₁ ar' a e₁ .fst ∷ c₁ ∷ δ
```

向内读取时，假设类型中所写的数学闭包规则。该规则对任意扩展环境 `s` 量化，因为界词项所属的集合需要在这个环境中求值。

```agda
  bqClose-in : (k Nx : Fin 10) (X : Fin (8 + m))
             → ((c₁ ar' a s : S) → ⟨ fst c₁ ∈ Cv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
                → (x : S) → ⟨ fst x ∈ fst (lookup X (a ∷ ar' ∷ s ∷ c₁ ∷ δ)) ⟩
                → ⟨ pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (fst a))) ∈ Cv ⟩)
             → ⟨ δ ⊨ Cl.bqClose k Nx X ⟩
```

先引入量化的子键数据与界词项，再在所得环境中应用所假设的闭包规则。沿两条标签等式运输其结论，便得到 `bndKey` 所要求的隶属，从而完成有界量词子句的向内读法。

```agda
  bqClose-in k Nx X g c₁ c₁∈ = bothAll-in i0 (sucAtL i5 i1 ⇒̇ ∀̇∈ (var X) (bndKey (sh 9 C) i6 (sh 9 (N k)) (sh 9 (N Nx)) i0 i1)) (c₁ ∷ δ) (λ ar' a s s∈ ar'∈ a∈ e₁ hs x x∈ →
    bndKey-in (sh 9 C) i6 (sh 9 (N k)) (sh 9 (N Nx)) i0 i1 (x ∷ a ∷ ar' ∷ s ∷ c₁ ∷ δ)
      (subst (λ u → ⟨ u ∈ Cv ⟩)
        (sym (cong (pr A) (cong₂ pr (tg k) (cong (λ v → pr v (fst a)) (cong (λ v → pr v (fst x)) (tg Nx))))))
        (g c₁ ar' a s c₁∈ e₁ (suc-out i5 i1 (a ∷ ar' ∷ s ∷ c₁ ∷ δ) hs) x x∈)))
```

## 可靠性：解码每个成员

为证明可靠性，现在把三类已有描述联系起来：数值标签识别十种构造，形状公式与闭包公式描述它们在集合内部的编码，而 `AllCodes` 把这些码重新联系到外部公式文法。相关性质都是命题，因此可以消去截断见证而不必选取代表。

```agda
open import L.Coding.Expressions {ℓ} using ( tagAtL-adequate )
open import L.Coding.Closure {ℓ} using ( closedAt; binSameClosed-in; unSuccClosed-in; binSuccClosed-in )
open import L.Coding.CodeShape {ℓ} using
  ( shapedAt; shaped-in; ShapeWit; BinWit; bothTm; fstTm; noneB; isTmAt )
open import L.Coding.CodeSet {ℓ} lem using
```

典范码集提供这种比较的两个方向：它的成员可以读作公式键，而每条公式也都有典范键。其余引入给出已记录元数的见证，以及两个命题的合取仍为命题这一事实。

```agda
  ( AllCodes; AllCodes-out; key∈AllCodes; keyS; codeS; witnessAt-out )
open import Cubical.Foundations.HLevels using ( isProp× )
```

固定一个工作集 `Wv`，其元素可以作为常元出现；再固定一个候选码域 `Cv`。以下论证对这两个集合保持参数化，此时尚未假设 `Cv` 就是典范码域 `AllCodes`。

```agda
module _ (Wv Cv : V ℓ) where
  open CodesSem Wv Cv
```

每个载荷条件 `PayN n ar r` 都是命题。对标签零至四，这直接来自命题截断，因为相应条件只断言合适的分量纯粹存在。

```agda
  isPropPayN : (n : ℕ) (ar r : V ℓ) → isProp (PayN n ar r)
  isPropPayN 0 ar r = squash₁
  isPropPayN 1 ar r = squash₁
  isPropPayN 2 ar r = squash₁
  isPropPayN 3 ar r = squash₁
```

其余构造标签也依各自的载荷使用同一原则。假的载荷唯一地等于零；无界量词要求属于 `Cv`，而隶属关系取值于命题；有界量词则再次使用截断存在。

```agda
  isPropPayN 4 ar r = squash₁
  isPropPayN 5 ar r = setIsSet r (# 0)
  isPropPayN 6 ar r = snd (pr (sucV ar) r ∈ Cv)
  isPropPayN 7 ar r = snd (pr (sucV ar) r ∈ Cv)
  isPropPayN 8 ar r = squash₁
```

标签九同样由截断存在处理。超过十种构造标签的任何数码，其载荷类型都是空类型，而空类型是命题。因此，对每个自然数标签，`PayN` 都取值于命题。

```agda
  isPropPayN 9 ar r = squash₁
  isPropPayN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) ar r = Empty.isProp⊥*
```

键对齐引理把元数 `ar` 处的一个 `Key` 转换为同一集合的任何其他分解 `p = (# n, r)` 处的载荷。配对单射性与数码单射性分别对齐标签与载荷；而 `PayN n ar r` 是命题，故截断的键可消去到它。

```agda
  keyAt : (ar p : V ℓ) → Key ar p → (n : ℕ) (r : V ℓ) → p ≡ pr (# n) r → PayN n ar r
  keyAt ar p key n r e = PT.rec (isPropPayN n ar r)
    (λ { (k , r' , (e' , pay)) →
      let q = pr-inj (sym e ∙ e')
      in subst2 (λ j x → PayN j ar x) (sym (#-inj′ (q .fst))) (sym (q .snd)) pay })
```

把上述消去应用于 `key`，对齐便告完成：从 `Key` 取得的标签与载荷已经运输到指定的数码 `n` 和载荷 `r`。

```agda
    key
```

第一条恢复引理把词项码陈述转换成形状章的词项谓词的一个满足。它对任意槽位陈述，证明方法是把这个截断的 `IsTmV` 消去到命题值的满足之中。

```agda
tmWit : ∀ {j} (ti Ni Ai : Fin j) (env : S ^ j)
      → IsTmV (fst (lookup Ai env)) (fst (lookup ti env)) (fst (lookup Ni env))
      → ⟨ env ⊨ isTmAt ti Ni Ai ⟩
tmWit ti Ni Ai env = PT.rec (snd (env ⊨ isTmAt ti Ni Ai))
  (λ { (inl (x , (e , x∈))) →
```

常元支中，`down` 把见证 `x` 表示为工作集 `Wv` 的元素。标签充分性运输有序对等式，原有的隶属证明则给出另一个合取项；所得证据进入形状谓词的左析取支。

```agda
         ∣ inl ∣ down (lookup Ai env) x x∈
           , ( subst ⟨_⟩ (sym (tagAtL-adequate (suc ti) 0 zero (down (lookup Ai env) x x∈ ∷ env))) e
             , x∈ ) ∣₁ ∣₁
     ; (inr (i , (e , i∈))) →
         ∣ inr ∣ down (lookup Ni env) i i∈
```

变元支以数码槽呈现索引，重复同一构造。两支合起来说明：词项码到形状满足的转换无须任何选择。

```agda
           , ( subst ⟨_⟩ (sym (tagAtL-adequate (suc ti) 1 zero (down (lookup Ni env) i i∈ ∷ env))) e
             , i∈ ) ∣₁ ∣₁ })
```

现在可以陈述候选域 `C` 的可靠性。假设常元字母表是集合 `W`，十个标签槽包含正确的数码，环境集中记录的每个元数都是自然数数码，并且 `C` 满足形状描述。由这些假设，可以把 `C` 的每个成员恢复为公式键。

```agda
module CodesSound {m : ℕ} (C w E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N)
  (arity : (n F : S) → ⟨ pr (fst n) (fst F) ∈ fst (lookup E γ) ⟩ → ∥ Σ[ k ∈ ℕ ] (fst n ≡ # k) ∥₁)
  (hs : ⟨ γ ⊨ shapeAt C w E N ⟩) where
  private
```

记 `Cv` 为候选域的底层集合，记 `CS` 为它在可构造结构中的代表，其中把该集合与其可构造性证明打包在一起。类似地，`Wv` 与 `Ev` 分别表示工作集和环境集的底层集合。这些缩写区分隶属陈述所用的宿主层集合与一阶环境中所用的带证明代表。

```agda
    Cv = fst (lookup C γ)
    CS = lookup C γ
    Wv = fst (lookup w γ)
    Ev = fst (lookup E γ)
    module SR = ShapeRead C w E N γ tg
```

此后，所有载荷条件都相对于固定的工作集 `Wv` 与候选域 `Cv` 解释。

```agda
  open CodesSem Wv Cv
```

证明将通过若干辅助引理，逐步恢复形状公式所隐藏的载荷信息。

```agda
  private
```

对一个选定的成员 `c`，环境 `δ' c` 把候选域与 `c` 放在原环境之前。该成员的形状谓词正是在这个语境中解释的。

```agda
    δ' : S → S ^ (2 + m)
    δ' c = CS ∷ c ∷ γ
```

对齐引理 `at` 是可靠性的核心。由成员 `c` 处的形状满足，它恢复一个截断的形状见证，把对等式与目标分解相对齐，再应用 `keyAt` 把载荷搬到带编号的分解处。由于载荷是命题，这次消去是合法的。

```agda
    at : (c : S) → ⟨ fst c ∈ Cv ⟩ → (n : ℕ) (ar r : V ℓ) → fst c ≡ pr ar (pr (# n) r)
       → PayN n ar r
    at c c∈ n ar r e = PT.rec (isPropPayN Wv Cv n ar r)
      (λ { (ar' , F , p , (q∈ , (ec , key))) →
        let q = pr-inj (sym ec ∙ e)
```

元数等式最后运输，因为形状见证与目标分解可能用不同的集合呈现元数。载荷的来源，是章假设在该成员处的形状读取。

```agda
        in subst (λ a → PayN n a r) (q .fst) (keyAt Wv Cv ar' p key n r (q .snd)) })
      (SR.shape-out hs c c∈)
```

二元提取器把二元载荷转换为域中同元数的两个子键。其陈述显式名指标签等式，因为载荷是在某个带编号的分解处取得的，必须与所展示的对对齐。

```agda
    binAt : (k : ℕ) → PayN k ≡ BinP → (c ar a b : S) → ⟨ fst c ∈ Cv ⟩
          → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
          → ⟨ pr (fst ar) (fst a) ∈ Cv ⟩ × ⟨ pr (fst ar) (fst b) ∈ Cv ⟩
    binAt k eq c ar a b c∈ e = PT.rec (isProp× (snd (pr (fst ar) (fst a) ∈ Cv)) (snd (pr (fst ar) (fst b) ∈ Cv)))
      (λ { (a' , b' , (er , (ha , hb))) →
```

配对单射性把等式拆成两个分量等式，每个子键被运输到位。载荷的来源，是对该成员施用带编号标签的对齐引理。

```agda
        let q = pr-inj er
        in subst (λ u → ⟨ pr (fst ar) u ∈ Cv ⟩) (sym (q .fst)) ha
         , subst (λ u → ⟨ pr (fst ar) u ∈ Cv ⟩) (sym (q .snd)) hb })
      (subst (λ P → P (fst ar) (pr (fst a) (fst b))) eq (at c c∈ k (fst ar) (pr (fst a) (fst b)) e))
```

有界量词提取器把有界载荷转换为其主体键在后继元数处的隶属。证明消去截断的载荷，再沿有序对第二分量的等式运输内层隶属。

```agda
    bqAt : (k : ℕ) → PayN k ≡ BqP → (c ar a b : S) → ⟨ fst c ∈ Cv ⟩
         → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
         → ⟨ pr (sucV (fst ar)) (fst b) ∈ Cv ⟩
    bqAt k eq c ar a b c∈ e = PT.rec (snd (pr (sucV (fst ar)) (fst b) ∈ Cv))
      (λ { (t , a' , (er , (ht , ha))) →
```

有界载荷与所展示的嵌套有序对对齐后，其中的主体分量恰好是后继元数处的键。沿相应的分量等式运输这份隶属证明，便得到所需结论。

```agda
        subst (λ u → ⟨ pr (sucV (fst ar)) u ∈ Cv ⟩) (sym (pr-inj er .snd)) ha })
      (subst (λ P → P (fst ar) (pr (fst a) (fst b))) eq (at c c∈ k (fst ar) (pr (fst a) (fst b)) e))
```

这些提取引理给出对码作递归时所需的向下闭包。对三个二元联结词中的每一个，复合键属于该域都蕴含它的两个直接子键在同一元数处也属于该域。

```agda
    hcl : (c : S) → ⟨ δ' c ⊨ closedAt zero ⟩
    hcl c =
        binSameClosed-in zero 2 (δ' c) (binAt 2 refl)
      , ( binSameClosed-in zero 3 (δ' c) (binAt 3 refl)
      , ( binSameClosed-in zero 4 (δ' c) (binAt 4 refl)
```

量词也满足相应的结论，但元数按预期发生变化。元数 `n` 处的无界或有界量词键，都包含一个后继元数处的主体键；有界情形在核对载荷形状后，还需略去其中的界词项分量。

```agda
      , ( unSuccClosed-in zero 6 (δ' c) (λ c' ar a c'∈ e → at c' c'∈ 6 (fst ar) (fst a) e)
      , ( unSuccClosed-in zero 7 (δ' c) (λ c' ar a c'∈ e → at c' c'∈ 7 (fst ar) (fst a) e)
      , ( binSuccClosed-in zero 8 (δ' c) (bqAt 8 refl)
      ,   binSuccClosed-in zero 9 (δ' c) (bqAt 9 refl) )))))
```

还需恢复候选域任意成员 `c'` 的完整形状。形状描述给出一个截断分解，环境假设把其中的元数识别为自然数数码，而 `Key` 再识别其标签与载荷。整个恢复过程的结果始终保留在截断之内。

```agda
    wit : (c c' : S) → ⟨ fst c' ∈ Cv ⟩ → ∥ ShapeWit (sh 2 w) (δ' c) c' ∥₁
    wit c c' c'∈ = PT.rec squash₁
      (λ { (ar , F , p , (q∈ , (ec , key))) → PT.rec squash₁
        (λ { (k , r , (e' , pay)) →
          let qS = down (lookup E γ) (pr ar F) q∈
```

恢复出的数据分别由相关集合中的代表给出：`qS` 呈现环境条目，`arS` 呈现其元数，`pS` 呈现编码后的载荷，`rS` 呈现内层载荷。这些呈现等式复合成键等式 `ek`。

```agda
              arS = fstS qS ar F refl
              pS = sndS c' ar p ec
              rS = sndS pS (# (toℕ k)) r e'
              ek : fst c' ≡ pr (fst arS) (pr (# (toℕ k)) (fst rS))
              ek = ec ∙ cong (pr ar) e'
```

引理 `fill` 接着分析恢复出的标签。对十种可能标签中的每一种，它都把相应的载荷条件转换成形状公式对应分支的见证。

```agda
          in fill k c' arS rS pay ek })
        key })
      (SR.shape-out hs c' c'∈)
      where
      env4 : (c' arS b a : S) → S ^ (6 + m)
```

辅助环境记录两个载荷分量以及后继元数，从而提供解释二元联结词与量化公式各分支所需的变元。

```agda
      env4 c' arS b a = b ∷ a ∷ arS ∷ c' ∷ δ' c
```

二元载荷只断言存在两个分量：它们组成的有序对等于所展示的载荷，并且各自对应的键都属于该域。辅助引理 `pairWit` 恰好把这些数据转换成形状公式相应分支所要求的见证。

```agda
      pairWit : (k : ℕ) (rel : Formula S (4 + (2 + m))) (c' arS rS : S)
              → fst c' ≡ pr (fst arS) (pr (# k) (fst rS))
              → (t u : V ℓ) → fst rS ≡ pr t u
              → ((tS uS : S) → fst tS ≡ t → fst uS ≡ u → ⟨ env4 c' arS uS tS ⊨ rel ⟩)
              → BinWit k rel (δ' c) c'
```

有序对编码的单射性把载荷等式拆成两个分量等式。它们与元数呈现及复合键等式一起，把两份隶属证明放入 `BinWit` 所要求的四个字段。

```agda
      pairWit k rel c' arS rS ek t u er g =
        arS , (fstS rS t u er , (sndS rS t u er
        , ( ek ∙ cong (λ v → pr (fst arS) (pr (# k) v)) er
          , g (fstS rS t u er) (sndS rS t u er) refl refl )))
```

对原子公式，载荷的两个分量都必须是在所记录元数处合法的词项码。分别对两个分量应用 `tmWit`，便把这两项语义条件转换成 `bothTm` 的两个合取项。

```agda
      both : (c' arS : S) (t u : V ℓ) → IsTmV Wv t (fst arS) → IsTmV Wv u (fst arS)
           → (tS uS : S) → fst tS ≡ t → fst uS ≡ u → ⟨ env4 c' arS uS tS ⊨ bothTm (sh 2 w) ⟩
      both c' arS t u ht hu tS uS qt qu =
          tmWit (suc zero) (suc (suc zero)) (sh 4 (sh 2 w)) (env4 c' arS uS tS)
            (subst (λ x → IsTmV Wv x (fst arS)) (sym qt) ht)
```

第二分量以同样方式处理，于是恢复出的两个词项见证共同证明原子载荷所要求的合取。

```agda
        , tmWit zero (suc (suc zero)) (sh 4 (sh 2 w)) (env4 c' arS uS tS)
            (subst (λ x → IsTmV Wv x (fst arS)) (sym qu) hu)
```

有界量词只要求界词项在当前元数处合法，因此相应的辅助引理只对载荷的第一分量应用 `tmWit`。

```agda
      first : (c' arS : S) (t u : V ℓ) → IsTmV Wv t (fst arS)
            → (tS uS : S) → fst tS ≡ t → fst uS ≡ u → ⟨ env4 c' arS uS tS ⊨ fstTm (sh 2 w) ⟩
      first c' arS t u ht tS uS qt qu =
        tmWit (suc zero) (suc (suc zero)) (sh 4 (sh 2 w)) (env4 c' arS uS tS)
          (subst (λ x → IsTmV Wv x (fst arS)) (sym qt) ht)
```

标签零表示隶属。其载荷包含两个合法词项码，因此二元辅助引理利用恢复出的词项证明，给出形状公式最左侧分支的见证。

```agda
      fill : (k : Fin 10) (c' arS rS : S) → PayN (toℕ k) (fst arS) (fst rS)
           → fst c' ≡ pr (fst arS) (pr (# (toℕ k)) (fst rS))
           → ∥ ShapeWit (sh 2 w) (δ' c) c' ∥₁
      fill zero c' arS rS pay ek = PT.map
        (λ { (t , u , (er , (ht , hu))) → inl (pairWit 0 (bothTm (sh 2 w)) c' arS rS ek t u er (both c' arS t u ht hu)) })
```

标签一表示相等，在下一分支中由同样的双词项论证处理。标签二开始表示二元联结词；此时仍采用同样的有序对分析，但恢复出的两个分量是子公式键，而不是词项码。

```agda
        pay
      fill (suc zero) c' arS rS pay ek = PT.map
        (λ { (t , u , (er , (ht , hu))) → inr (inl (pairWit 1 (bothTm (sh 2 w)) c' arS rS ek t u er (both c' arS t u ht hu))) })
        pay
      fill (suc (suc zero)) c' arS rS pay ek = PT.map
```

三个二元联结词的填充情形是一致的：载荷点名两个子码 `a` 与 `b`，见证是处在该标签位置上的 `pairWit`，无界限项、载荷条件空洞，因为二元子句本无额外要求。析取的嵌套深度标出该标签在十路和中的位置。

```agda
        (λ { (a , b , (er , _)) → inr (inr (inl (pairWit 2 noneB c' arS rS ek a b er (λ _ _ _ _ b → b)))) })
        pay
      fill (suc (suc (suc zero))) c' arS rS pay ek = PT.map
        (λ { (a , b , (er , _)) → inr (inr (inr (inl (pairWit 3 noneB c' arS rS ek a b er (λ _ _ _ _ b → b))))) })
        pay
```

蕴涵占据第四个二元标签，仍沿用同一构造。假则有所不同：它的载荷是数码零，因此见证只需给出元数等式与载荷等式，其中 `numeralL-fst` 提供数码底层集合所需的等式。

```agda
      fill (suc (suc (suc (suc zero)))) c' arS rS pay ek = PT.map
        (λ { (a , b , (er , _)) → inr (inr (inr (inr (inl (pairWit 4 noneB c' arS rS ek a b er (λ _ _ _ _ b → b)))))) })
        pay
      fill (suc (suc (suc (suc (suc zero))))) c' arS rS pay ek =
        ∣ inr (inr (inr (inr (inr (inl (arS , (rS , (ek , pay ∙ sym (numeralL-fst 0))))))))) ∣₁
```

两个无界量词同样一致：其载荷是后继元数处的子键，见证条件是该数据上的恒等，因为量词子句不添加词项要求。只有标签位置区分存在与全称。

```agda
      fill (suc (suc (suc (suc (suc (suc zero)))))) c' arS rS pay ek =
        ∣ inr (inr (inr (inr (inr (inr (inl (arS , (rS , (ek , (λ b → b)))))))))) ∣₁
      fill (suc (suc (suc (suc (suc (suc (suc zero))))))) c' arS rS pay ek =
        ∣ inr (inr (inr (inr (inr (inr (inr (inl (arS , (rS , (ek , (λ b → b))))))))))) ∣₁
      fill (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) c' arS rS pay ek = PT.map
```

有界全称添加了词项层：其载荷除成员 `a` 外还包含合法的界限词项 `t`，见证对该词项使用单词项读式 `first`，并以 `fstTm` 指名有界键形状中的词项槽位。

```agda
        (λ { (t , a , (er , (ht , _))) → inr (inr (inr (inr (inr (inr (inr (inr (inl
          (pairWit 8 (fstTm (sh 2 w)) c' arS rS ek t a er (first c' arS t a ht)))))))))) })
        pay
      fill (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) c' arS rS pay ek = PT.map
        (λ { (t , a , (er , (ht , _))) → inr (inr (inr (inr (inr (inr (inr (inr (inr
```

有界存在与有界全称具有相同的载荷形状，但占据最后一个标签。至此，十种情形恰好覆盖公式的全部构造子：四种原子公式、三个二元联结词、假，以及有界和无界量词。

```agda
          (pairWit 9 (fstTm (sh 2 w)) c' arS rS ek t a er (first c' arS t a ht)))))))))) })
        pay
```

形状可靠性引理把上述构造逐成员汇集起来。对于码集中的每个 `c`，`shaped-in` 将刚构造的见证转化为 `shapedAt` 的满足证明；解码某个码时，所需的正是这种局部形状事实。

```agda
    hsh : (c : S) → ⟨ δ' c ⊨ shapedAt zero (sh 2 w) ⟩
    hsh c = shaped-in zero (sh 2 w) (δ' c) (wit c)
```

闭包子句对全部七个非原子构造子一次证得。三个二元联结词由 `binAt` 处理：它读取该标签的载荷，并经配对编码的单射性提取两个子码的隶属。

```agda
  closed : ⟨ γ ⊨ closedAt C ⟩
  closed =
      binSameClosed-in C 2 γ (binAt 2 refl)
    , ( binSameClosed-in C 3 γ (binAt 3 refl)
    , ( binSameClosed-in C 4 γ (binAt 4 refl)
```

两个无界量词通过在后继元数处引用读式兑现；两个有界量词由 `bqAt` 兑现，后者还额外读出界限词项。七条合起来在环境中认证了 `closedAt C`。

```agda
    , ( unSuccClosed-in C 6 γ (λ c' ar a c'∈ e → at c' c'∈ 6 (fst ar) (fst a) e)
    , ( unSuccClosed-in C 7 γ (λ c' ar a c'∈ e → at c' c'∈ 7 (fst ar) (fst a) e)
    , ( binSuccClosed-in C 8 γ (bqAt 8 refl)
    ,   binSuccClosed-in C 9 γ (bqAt 9 refl) )))))
```

解码定理是本章的第一个主要结果。对于满足描述的码集中的每个成员 `c`，都可在命题截断下得到一个自然数 `k` 和一条元数为 `k` 的公式 `ψ`，并有 `fst c ≡ fst (keyS W ψ)`。因此，定理只断言相应公式键的存在，并未选定解码函数，也未断言唯一性。

```agda
  key-out : (c : S) → ⟨ fst c ∈ Cv ⟩
          → ∥ Σ[ k ∈ ℕ ] Σ[ ψ ∈ Formula ⟪ fst W ⟫ k ] (fst c ≡ fst (keyS W ψ)) ∥₁
  key-out c c∈ = PT.rec squash₁
    (λ { (ar , F , p , (q∈ , (ec , key))) → PT.rec squash₁
      (λ { (k , qk) → PT.map (λ { (ψ , e) → k , ψ , e })
```

先从 `c` 的截断形状数据中取得元数条目、表和满足相应键条件的载荷。元数假设把所记录的元数等同于某个数码 `# k`。再结合前面得到的向下封闭性，`witnessAt-out` 便在仍受截断的意义下恢复一条元数为 `k` 的公式，其键的底层集合就是 `fst c`。

```agda
        (witnessAt-out W (suc w) zero (c ∷ γ) qw
          ∣ CS , (c∈ , (hcl c , hsh c)) ∣₁
          k (sndS c ar p ec) (ec ∙ cong (λ a → pr a p) qk)) })
      (arity (fstS (down (lookup E γ) (pr ar F) q∈) ar F refl)
             (sndS (down (lookup E γ) (pr ar F) q∈) ar F refl) q∈) })
```

所需的形状数据，正是将 `shape-out` 用于已知的形状子句和 `c` 的隶属证明所得的结果。

```agda
    (SR.shape-out hs c c∈)
```

## 完备性：编码每条公式

此处引入两条关于有穷索引的算术事实：把低于 `n` 的自然数转换为 `Fin n` 的合法索引，以及把索引经其自身数码往返。

```agda
open import L.Ordinal {ℓ} using ( ∈#-elim )
open import Cubical.Data.FinData.Properties using ( fromℕ'; toFromId' )
```

为证明完备性，固定码域槽位 `C`、字母表槽位 `w` 与元数塔槽位 `E`，并假设十个标签解释正确。再假设每个典范塔条目都属于 `E`，且向上闭包子句成立；目标是证明字母表上每条公式的键都属于 `C`。

```agda
module CodesComplete {m : ℕ} (C w E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N)
  (arity∈ : (n : ℕ) → ⟨ pr (# n) (fst (envSet W n)) ∈ fst (lookup E γ) ⟩)
  (hc : ⟨ γ ⊨ closeAt C w E N ⟩) where
  open Alphabet W
```

以 `Cv` 表示码域槽位所指的底层集合。完备性要证明每一条真实公式的键都属于这个集合。

```agda
  private
    Cv = fst (lookup C γ)
```

字母表的每个常元都属于字母表槽位：两个载体的等同，正是把嵌入的隶属传输进环境的依据。

```agda
    ι∈w : (q : Ab) → ⟨ ι q ∈ fst (lookup w γ) ⟩
    ι∈w q = subst (λ u → ⟨ ι q ∈ u ⟩) (sym qw) (ι∈ q)
```

每个字母表条目都由槽位 `w` 的一个内部元素表示。`down` 把它的外围表示与上面得到的隶属证明打包起来，得到相应的元素 `ιS q : S`。

```agda
    ιS : Ab → S
    ιS q = down (lookup w γ) (ι q) (ι∈w q)
```

元数 `n` 处的典范塔条目是数码 `n` 与长度 `n` 环境集组成的对。它也照此下降，使闭包子句能够在它那里引用。

```agda
    qS : ℕ → S
    qS n = down (lookup E γ) (pr (# n) (fst (envSet W n))) (arity∈ n)
```

四槽位语境装配被降下的塔条目、数码、它们的配对容器以及再次出现的被降条目，与闭包子句所期待的框架一致。

```agda
    δ4 : ℕ → S ^ (4 + m)
    δ4 n = envSet W n ∷ nn n ∷ container (qS n) (nn n) (envSet W n) refl .fst ∷ qS n ∷ γ
```

完整的闭包子句在该语境处成立，因为假设说：闭包子句在每个典范塔条目处都成立。

```agda
    frame : (n : ℕ) → ⟨ δ4 n ⊨ Close.all C w N ⟩
    frame n = useBoth i0 (qS n ∷ γ) (nn n) (envSet W n) refl (Close.all C w N) (hc (qS n) (arity∈ n))
```

闭包读式在每个数码自己的语境处重新打开，使每个元数都拥有十八条子句的一份副本。

```agda
    module CR (n : ℕ) = CloseRead C w N (δ4 n) tg
```

低于 `n` 的每个变元索引都指名低于 `n` 之数码的一个数码：冯·诺伊曼数码的单调性使变元索引能被认作其元数数码的成员。

```agda
    var∈ : (n : ℕ) (i : Fin n) → ⟨ # (toℕ i) ∈ # n ⟩
    var∈ n i = #mono (toℕ i) n (toℕ<n i)
```

结构归纳从成员关系原子的四种情形开始。每种情形都在固定元数 `n` 处实例化原子闭包子句；左右两个词项各自可以来自字母表常元或该元数下的变元，而前面的引理恰好提供相应的隶属证明。

```agda
  key-in : ∀ {n} (ψ : Formula Ab n) → ⟨ fst (keyS W ψ) ∈ Cv ⟩
  key-in {n} (con x ∈̇ con y) = CR.atomClose-out n f0 f0 f0 (sh 4 w) (sh 5 w) (frame n .fst) (ιS x) (ιS y) (ι∈w x) (ι∈w y)
  key-in {n} (con x ∈̇ var j) = CR.atomClose-out n f0 f0 f1 (sh 4 w) i2 (frame n .snd .fst) (ιS x) (nn (toℕ j)) (ι∈w x) (var∈ n j)
  key-in {n} (var i ∈̇ con y) = CR.atomClose-out n f0 f1 f0 i1 (sh 5 w) (frame n .snd .snd .fst) (nn (toℕ i)) (ιS y) (var∈ n i) (ι∈w y)
  key-in {n} (var i ∈̇ var j) = CR.atomClose-out n f0 f1 f1 i1 i2 (frame n .snd .snd .snd .fst) (nn (toℕ i)) (nn (toℕ j)) (var∈ n i) (var∈ n j)
```

四种相等原子公式以相等标签重复同一论证。对于合取，归纳假设先把两条子公式的键放入 `C`，二元闭包子句再把由它们配成的合取键放入 `C`。

```agda
  key-in {n} (con x ≐ con y) = CR.atomClose-out n f1 f0 f0 (sh 4 w) (sh 5 w) (frame n .snd .snd .snd .snd .fst) (ιS x) (ιS y) (ι∈w x) (ι∈w y)
  key-in {n} (con x ≐ var j) = CR.atomClose-out n f1 f0 f1 (sh 4 w) i2 (frame n .snd .snd .snd .snd .snd .fst) (ιS x) (nn (toℕ j)) (ι∈w x) (var∈ n j)
  key-in {n} (var i ≐ con y) = CR.atomClose-out n f1 f1 f0 i1 (sh 5 w) (frame n .snd .snd .snd .snd .snd .snd .fst) (nn (toℕ i)) (ιS y) (var∈ n i) (ι∈w y)
  key-in {n} (var i ≐ var j) = CR.atomClose-out n f1 f1 f1 i1 i2 (frame n .snd .snd .snd .snd .snd .snd .snd .fst) (nn (toℕ i)) (nn (toℕ j)) (var∈ n i) (var∈ n j)
  key-in {n} (a ∧̇ b) = CR.binClose-out n f2 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (keyS W b) (codeS W a) (codeS W b) (key-in a) (key-in b) refl refl
```

析取和蕴涵分别在各自的标签处采用同一个二元步骤，假则以零为载荷，经常量闭包子句进入 `C`。对于两种无界量词，归纳假设作用于元数为 `suc n` 的量词体；量词闭包子句再由量词体的键生成元数为 `n` 的键。

```agda
  key-in {n} (a ∨̇ b) = CR.binClose-out n f3 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (keyS W b) (codeS W a) (codeS W b) (key-in a) (key-in b) refl refl
  key-in {n} (a ⇒̇ b) = CR.binClose-out n f4 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (keyS W b) (codeS W a) (codeS W b) (key-in a) (key-in b) refl refl
  key-in {n} ⊥̇ = CR.conClose-out n f5 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst)
  key-in {n} (∃̇ a) = CR.quClose-out n f6 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (nn (suc n)) (codeS W a) (key-in a) refl refl
  key-in {n} (∀̇ a) = CR.quClose-out n f7 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (nn (suc n)) (codeS W a) (key-in a) refl refl
```

有界全称有两条闭包论证：后继元数处的子键，以及当前元数处的合法界限词项。界限为常元时，词项条目来自字母表嵌入；界限为变元时，来自数码隶属。

```agda
  key-in {n} (∀̇∈ (con x) a) =
    CR.bqClose-out n f8 f0 (sh 8 w) (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (nn (suc n)) (codeS W a) (key-in a) refl refl (ιS x) (ι∈w x)
  key-in {n} (∀̇∈ (var i) a) =
    CR.bqClose-out n f8 f1 i5 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (nn (suc n)) (codeS W a) (key-in a) refl refl (nn (toℕ i)) (var∈ n i)
  key-in {n} (∃̇∈ (con x) a) =
```

有界存在在其自身标签处重复同样两条论证，完成结构归纳：每个元数的每条公式，其键都在封闭域中。

```agda
    CR.bqClose-out n f9 f0 (sh 8 w) (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .fst) (keyS W a) (nn (suc n)) (codeS W a) (key-in a) refl refl (ιS x) (ι∈w x)
  key-in {n} (∃̇∈ (var i) a) =
    CR.bqClose-out n f9 f1 i5 (frame n .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd .snd ) (keyS W a) (nn (suc n)) (codeS W a) (key-in a) refl refl (nn (toℕ i)) (var∈ n i)
```

## 典范的封闭码定义域

最后还要证明典范码域确实满足这份描述。令码槽位表示 `AllCodes W`，令元数槽位表示 `W` 上的环境塔；等式 `qC` 与 `qE` 分别记录这两个等同。

```agda
module CodesHolds {m : ℕ} (C w E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (qC : fst (lookup C γ) ≡ fst (AllCodes W))
  (qE : fst (lookup E γ) ≡ fst (Tower.tower W)) (tg : Tags γ N) where
  open Alphabet W
  private
```

分别以 `Cv`、`Wv` 和 `Ev` 表示码域、字母表与元数塔槽位所指的底层集合。这三个名称区分了不同职责：公式键在 `Cv` 中检验，常元的表示在 `Wv` 中检验，典范元数条目则在 `Ev` 中检验。

```agda
    Cv = fst (lookup C γ)
    Wv = fst (lookup w γ)
    Ev = fst (lookup E γ)
    open CodesSem Wv Cv
```

假设集合 `Wv′` 含有每个字母表条目的表示，那么每个词项在 `Wv′` 上都有合法编码。常元使用其表示的给定隶属证明，变元使用索引数码属于元数数码这一事实。所得见证经过命题截断，因为这里仅把词项合法性当作编码的一项性质使用。

```agda
    tmV : ∀ {n} (Wv′ : V ℓ) → ((q : Ab) → ⟨ ι q ∈ Wv′ ⟩) → (t : Term Ab n) → IsTmV Wv′ (ct t) (# n)
    tmV Wv′ into (con q) = ∣ inl (ι q , (refl , into q)) ∣₁
    tmV {n} Wv′ into (var i) = ∣ inr (# (toℕ i) , (refl , #mono (toℕ i) n (toℕ<n i))) ∣₁
```

字母表的常元属于环境的字母表槽位，经由两个载体的等同传输。

```agda
    ι∈w : (q : Ab) → ⟨ ι q ∈ Wv ⟩
    ι∈w q = subst (λ u → ⟨ ι q ∈ u ⟩) (sym qw) (ι∈ q)
```

依照 `AllCodes W` 的定义，字母表上每条公式的键都属于其中。沿 `qC` 传输这份隶属证明，便得到同一个键属于码槽位所指的集合 `Cv`。

```agda
    mem : ∀ {n} (ψ : Formula Ab n) → ⟨ fst (keyS W ψ) ∈ Cv ⟩
    mem ψ = subst (λ u → ⟨ fst (keyS W ψ) ∈ u ⟩) (sym qC) (key∈AllCodes W ψ)
```

同样，环境塔包含由数码 `# n` 与环境集 `envSet W n` 配成的典范条目。沿 `qE` 传输其隶属证明，便知该条目属于元数集合 `Ev`。

```agda
    entry∈ : (n : ℕ) → ⟨ pr (# n) (fst (envSet W n)) ∈ Ev ⟩
    entry∈ n = subst (λ u → ⟨ pr (# n) (fst (envSet W n)) ∈ u ⟩) (sym qE) (Tower.tower-in′ W n)
```

词项读式就是刚证明的一般词项合法性在字母表处的实例。

```agda
    tm : ∀ {n} (t : Term Ab n) → IsTmV Wv (ct t) (# n)
    tm = tmV Wv ι∈w
```

每条公式都在自身元数处确定一个合法键。证明按公式结构递归进行：原子公式组合两个词项的合法编码，合取和析取则组合已经得到的两条子公式键的隶属证明。

```agda
    keyOf : ∀ {n} (ψ : Formula Ab n) → Key (# n) (cd ψ)
    keyOf (t ∈̇ u) = ∣ f0 , pr (ct t) (ct u) , (refl , ∣ ct t , ct u , (refl , (tm t , tm u)) ∣₁) ∣₁
    keyOf (t ≐ u) = ∣ f1 , pr (ct t) (ct u) , (refl , ∣ ct t , ct u , (refl , (tm t , tm u)) ∣₁) ∣₁
    keyOf (a ∧̇ b) = ∣ f2 , pr (cd a) (cd b) , (refl , ∣ cd a , cd b , (refl , (mem a , mem b)) ∣₁) ∣₁
    keyOf (a ∨̇ b) = ∣ f3 , pr (cd a) (cd b) , (refl , ∣ cd a , cd b , (refl , (mem a , mem b)) ∣₁) ∣₁
```

蕴涵重复这一配对；假携带零载荷及其定义性等式；两个无界量词直接包裹子公式键，无任何词项要求。

```agda
    keyOf (a ⇒̇ b) = ∣ f4 , pr (cd a) (cd b) , (refl , ∣ cd a , cd b , (refl , (mem a , mem b)) ∣₁) ∣₁
    keyOf ⊥̇ = ∣ f5 , # 0 , (refl , refl) ∣₁
    keyOf (∃̇ a) = ∣ f6 , cd a , (refl , mem a) ∣₁
    keyOf (∀̇ a) = ∣ f7 , cd a , (refl , mem a) ∣₁
    keyOf (∀̇∈ t a) = ∣ f8 , pr (ct t) (cd a) , (refl , ∣ ct t , cd a , (refl , (tm t , mem a)) ∣₁) ∣₁
```

有界量词将界限词项与子公式键配对，完成递归：对每条公式 `ψ`，`keyOf ψ` 都是在 `ψ` 自身元数处的合法键。

```agda
    keyOf (∃̇∈ t a) = ∣ f9 , pr (ct t) (cd a) , (refl , ∣ ct t , cd a , (refl , (tm t , mem a)) ∣₁) ∣₁
```

典范实例的形状子句随之得出：`AllCodes W` 的每个成员都解码为一条公式，其「元数与表」对属于塔，其载荷是合法键。形状读式逐成员接收这些数据。

```agda
    shape : ⟨ γ ⊨ shapeAt C w E N ⟩
    shape = ShapeRead.shape-in C w E N γ tg (λ c c∈ → PT.map
      (λ { (n , ψ , e) → # n , fst (envSet W n) , cd ψ , (entry∈ n , (e , keyOf ψ)) })
      (AllCodes-out W c (subst (λ u → ⟨ fst c ∈ u ⟩) qC c∈)))
```

解码辅助引理显式固定元数。若码域成员 `c` 的底层集合是 `pr (# n) z`，则在命题截断下存在一条元数恰为 `n` 的公式 `ψ`，满足 `z ≡ cd ψ`。也就是说，只有外层数码固定了元数之后，结论才恢复载荷所编码的公式。

```agda
    decodeAt : (c : S) → ⟨ fst c ∈ Cv ⟩ → (n : ℕ) (z : V ℓ) → fst c ≡ pr (# n) z
             → ∥ Σ[ ψ ∈ Formula Ab n ] (z ≡ cd ψ) ∥₁
    decodeAt c c∈ n z e = PT.map
      (λ { (n₁ , ψ₁ , e₁) →
        let q = pr-inj (sym e₁ ∙ e)
```

证明向外读出该成员，并用配对与数码的单射性对齐两个元数，沿元数等式传输公式。随后反向读取编码的等式以确定载荷。

```agda
            nq = #-inj′ (q .fst)
        in subst (Formula Ab) nq ψ₁ , (sym (q .snd) ∙ sym (cd-subst nq ψ₁)) })
      (AllCodes-out W c (subst (λ u → ⟨ fst c ∈ u ⟩) qC c∈))
```

词项解码陈述由一个界集合参数化：界中的每个成员都 (至截断) 解码为一个词项，其编码把标签数码与该成员本身配对。

```agda
    TmDec : ∀ {n} → Fin 10 → V ℓ → Type (ℓ-suc ℓ)
    TmDec {n} Nx bound = (x : V ℓ) → ⟨ x ∈ bound ⟩ → ∥ Σ[ t ∈ Term Ab n ] (ct t ≡ pr (# (toℕ Nx)) x) ∥₁
```

常元经字母表嵌入的纤维解码：字母表槽位的成员是某个字母表条目的嵌入像，而那个条目正是所求的常元。

```agda
    conDec : ∀ {n} → TmDec {n} f0 Wv
    conDec x x∈ = ∣ con (fib .fst) , cong (pr (# 0)) (fib .snd) ∣₁
      where
      fib : Σ[ q ∈ Ab ] (ι q ≡ x)
      fib = ∈-asFiber {a = x} {b = fst W} (subst (λ u → ⟨ x ∈ u ⟩) qw x∈)
```

变元经数码消去解码：元数数码的成员是低于 `n` 的自然数，可转换回合法索引，而编码等式沿该往返传输。

```agda
    varDec : (n : ℕ) (A : V ℓ) → A ≡ # n → TmDec {n} f1 A
    varDec n A qa x x∈ = PT.map
      (λ { (j , (p , ex)) → var (fromℕ' n j p) , cong (pr (# 1)) (cong #_ (toFromId' n j p) ∙ sym ex) })
      (∈#-elim n x (subst (λ u → ⟨ x ∈ u ⟩) qa x∈))
```

固定环境塔的一个条目 `q`，并假设其所记录的元数等同于 `# n`。局部语境 `δ4` 给出闭包公式所需的四个值：元数表、元数数码、把该条目与表联系起来的容器，以及条目本身。

```agda
    module At (q : S) (q∈ : ⟨ fst q ∈ Ev ⟩) (ar F s : S) (n : ℕ) (qa : fst ar ≡ # n) where
      private
        δ4 : S ^ (4 + m)
        δ4 = F ∷ ar ∷ s ∷ q ∷ γ
        A = fst ar
```

在这个固定语境中，`CloseRead` 把每条闭包公式的满足转换为相应的数学闭包性质，`Close` 则给出这些公式本身。

```agda
        module CR = CloseRead C w N δ4 tg
        module Cl = Close C w N
```

辅助引理 `in-key` 沿等式传输典范键的隶属证明。若 `x` 等于某条公式 `ψ` 的键的底层集合，那么由该典范键已知属于 `Cv`，即可推出 `x ∈ Cv`。

```agda
        in-key : ∀ {k} (ψ : Formula Ab k) (x : V ℓ) → x ≡ fst (keyS W ψ) → ⟨ x ∈ Cv ⟩
        in-key ψ x e = subst (λ u → ⟨ u ∈ Cv ⟩) (sym e) (mem ψ)
```

给定标签 `Nx` 和元素 `x`，`TmAt Nx x` 是一个 Σ 类型：其第一分量是词项 `t`，第二分量是一条等式，说明 `t` 的编码正是由 `Nx` 的数码与 `x` 配成的对。与前面的解码陈述不同，这个局部类型没有经过命题截断。

```agda
        TmAt : (Nx : Fin 10) (x : V ℓ) → Type (ℓ-suc ℓ)
        TmAt Nx x = Σ[ t ∈ Term Ab n ] (ct t ≡ pr (# (toℕ Nx)) x)
```

同样，`FoAt k z` 是一个 Σ 类型：其第一分量是元数为 `k` 的公式 `ψ`，第二分量是等式 `z ≡ cd ψ`。公式及其编码等式都作为可用数据保留下来。

```agda
        FoAt : (k : ℕ) (z : V ℓ) → Type (ℓ-suc ℓ)
        FoAt k z = Σ[ ψ ∈ Formula Ab k ] (z ≡ cd ψ)
```

原子闭包子句由两条词项解码证明。给定第一坐标成员的解码与第二坐标成员的解码，原子键由对象语言构造子从两个词项构造，而编码等式把它与被点名的键等同。

```agda
        atomIn : (k Nx Ny : Fin 10) (X : Fin (4 + m)) (Y : Fin (5 + m))
               → (op : Term Ab n → Term Ab n → Formula Ab n)
               → ((t u : Term Ab n) → cd (op t u) ≡ pr (# (toℕ k)) (pr (ct t) (ct u)))
               → TmDec Nx (fst (lookup X δ4)) → ((x : S) → TmDec Ny (fst (lookup Y (x ∷ δ4))))
               → ⟨ δ4 ⊨ Cl.atomClose k Nx Ny X Y ⟩
```

分别解码两个坐标。第一坐标给出词项 `t` 及其编码等式；把这个坐标加入语境后，第二坐标再给出词项 `u` 及其编码等式。

```agda
        atomIn k Nx Ny X Y op code dx dy = CR.atomClose-in k Nx Ny X Y (λ x y x∈ y∈ →
          let d1 : ∥ TmAt Nx (fst x) ∥₁
              d1 = dx (fst x) x∈
              d2 : ∥ TmAt Ny (fst y) ∥₁
              d2 = dy x (fst y) y∈
```

集合 `G` 是由元数、原子标签和两个已编码坐标组成的候选原子键。由于「属于 `Cv`」是命题，可以把两份经过截断的词项解码依次消去到这个目标中。它们的编码等式把 `G` 等同于公式 `op t u` 的键，而后者的隶属由 `in-key` 给出。

```agda
              G : V ℓ
              G = pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (pr (# (toℕ Ny)) (fst y))))
          in PT.rec (snd (G ∈ Cv))
            (λ { (t , et) → PT.rec (snd (G ∈ Cv))
              (λ { (u , eu) → in-key (op t u) G
```

最后的等式分三层拼合：`qa` 对齐外层元数，两条词项编码等式对齐成对载荷，而 `op` 的定义等式对齐原子标签。沿这条等式传输典范键的隶属证明，便完成原子闭包的证明。

```agda
                (cong₂ pr qa (cong (pr (# (toℕ k))) (cong₂ pr (sym et) (sym eu)) ∙ sym (code t u))) })
              d2 })
            d1)
```

对于二元联结词，两个直接子公式与复合公式具有相同的元数 `n`。假设已将两个子键的第一分量写成 `# n`；把这一分量与记录的元数对齐后，`decodeAt` 分别将两个载荷恢复为元数 `n` 的公式码。

```agda
        binIn : (k : Fin 10) (op : Formula Ab n → Formula Ab n → Formula Ab n)
              → ((a b : Formula Ab n) → cd (op a b) ≡ pr (# (toℕ k)) (pr (cd a) (cd b)))
              → ⟨ δ4 ⊨ Cl.binClose k ⟩
        binIn k op code = CR.binClose-in k (λ c₁ c₂ a b c₁∈ c₂∈ e₁ e₂ →
          let d1 : ∥ FoAt n (fst a) ∥₁
```

两次应用 `decodeAt`，分别纯粹地得到公式 `ψ₁` 与 `ψ₂`，其编码就是载荷的两个分量。集合 `G` 则是已经由记录的元数、所选联结词的标签以及这两个分量组装出的复合键。

```agda
              d1 = decodeAt c₁ c₁∈ n (fst a) (e₁ ∙ cong (λ v → pr v (fst a)) qa)
              d2 : ∥ FoAt n (fst b) ∥₁
              d2 = decodeAt c₂ c₂∈ n (fst b) (e₂ ∙ cong (λ v → pr v (fst b)) qa)
              G : V ℓ
              G = pr A (pr (# (toℕ k)) (pr (fst a) (fst b)))
```

依次消去两份截断见证后，只需处理实际的公式 `ψ₁` 与 `ψ₂`。它们的编码等式将 `G` 与 `op ψ₁ ψ₂` 的键同一视，因此典范隶属证明 `in-key` 给出所需的二元闭包子句。

```agda
          in PT.rec (snd (G ∈ Cv))
            (λ { (ψ₁ , ea) → PT.rec (snd (G ∈ Cv))
              (λ { (ψ₂ , eb) → in-key (op ψ₁ ψ₂) G
                (cong₂ pr qa (cong (pr (# (toℕ k))) (cong₂ pr ea eb) ∙ sym (code ψ₁ ψ₂))) })
              d2 })
```

外层消去代入第一个恢复出的公式，从而完成码域对所选二元联结词封闭的证明。

```agda
            d1)
```

假没有子公式，其载荷就是数码零。将记录的元数和所选标签与 `c₀` 的典范编码对齐后，`in-key` 便证明所得键属于码域。

```agda
        conIn : (k : Fin 10) (c₀ : Formula Ab n) → cd c₀ ≡ pr (# (toℕ k)) (# 0) → ⟨ δ4 ⊨ Cl.conClose k ⟩
        conIn k c₀ code = CR.conClose-in k (in-key c₀ (pr A (pr (# (toℕ k)) (# 0))) (cong₂ pr qa (sym code)))
```

约束一个变量会使主体的元数由 `n` 变为 `suc n`。因此，量词闭包的假设把直接子键置于后继元数处，而 `decodeAt` 恰好恢复出具有这一元数的公式主体。

```agda
        quIn : (k : Fin 10) (op : Formula Ab (suc n) → Formula Ab n)
             → ((a : Formula Ab (suc n)) → cd (op a) ≡ pr (# (toℕ k)) (cd a))
             → ⟨ δ4 ⊨ Cl.quClose k ⟩
        quIn k op code = CR.quClose-in k (λ c₁ ar' a c₁∈ e₁ es →
          let d1 : ∥ FoAt (suc n) (fst a) ∥₁
```

令 `G` 为由外层元数、量词标签与主体编码组装出的键。截断的主体恢复为 `ψ₁` 后，其编码等式将 `G` 与 `op ψ₁` 的键同一视；典范隶属关系随即证明量词闭包子句。

```agda
              d1 = decodeAt c₁ c₁∈ (suc n) (fst a) (e₁ ∙ cong (λ v → pr v (fst a)) (es ∙ cong sucV qa))
              G : V ℓ
              G = pr A (pr (# (toℕ k)) (fst a))
          in PT.rec (snd (G ∈ Cv))
            (λ { (ψ₁ , ea) → in-key (op ψ₁) G (cong₂ pr qa (cong (pr (# (toℕ k))) ea ∙ sym (code ψ₁))) })
```

消去所恢复的主体，便完成码域对所选无界量词封闭的证明。

```agda
            d1)
```

有界量词同时携带元数为 `suc n` 的主体和元数为 `n` 的界词项。因此，除了已有的主体键解码方式外，`bqIn` 还接收一项词项解码假设，用于存放界的环境分量。

```agda
        bqIn : (k Nx : Fin 10) (X : Fin (8 + m))
             → (op : Term Ab n → Formula Ab (suc n) → Formula Ab n)
             → ((t : Term Ab n) (a : Formula Ab (suc n)) → cd (op t a) ≡ pr (# (toℕ k)) (pr (ct t) (cd a)))
             → ((ar' a s' c₁ : S) → TmDec Nx (fst (lookup X (a ∷ ar' ∷ s' ∷ c₁ ∷ δ4))))
             → ⟨ δ4 ⊨ Cl.bqClose k Nx X ⟩
```

词项解码假设由界的隶属证明恢复界词项，`decodeAt` 则由后继元数处的子键恢复主体。两项结果都受命题截断，因为闭包目标只要求完整键的隶属证明，并不要求选定全局解码结果。

```agda
        bqIn k Nx X op code dx = CR.bqClose-in k Nx X (λ c₁ ar' a s' c₁∈ e₁ es x x∈ →
          let d1 : ∥ TmAt Nx (fst x) ∥₁
              d1 = dx ar' a s' c₁ (fst x) x∈
              d2 : ∥ FoAt (suc n) (fst a) ∥₁
              d2 = decodeAt c₁ c₁∈ (suc n) (fst a) (e₁ ∙ cong (λ v → pr v (fst a)) (es ∙ cong sucV qa))
```

此时键 `G` 的载荷是嵌套的：先放界词项的编码，再放主体的编码。第一次截断消去取出实际词项 `t`，第二次则将取出主体编码所对应的公式。

```agda
              G : V ℓ
              G = pr A (pr (# (toℕ k)) (pr (pr (# (toℕ Nx)) (fst x)) (fst a)))
          in PT.rec (snd (G ∈ Cv))
            (λ { (t , et) → PT.rec (snd (G ∈ Cv))
              (λ { (ψ₁ , ea) → in-key (op t ψ₁) G
```

有了恢复出的词项 `t` 与主体 `ψ₁`，二者的编码等式便将 `G` 与 `op t ψ₁` 的键同一视。典范隶属证明由此给出有界量词子句，两层截断消去再按见证引入的相反次序收束。

```agda
                (cong₂ pr qa (cong (pr (# (toℕ k))) (cong₂ pr (sym et) ea) ∙ sym (code t ψ₁))) })
              d2 })
            d1)
```

公式 `Cl.all` 将十八条闭包子句汇集在一起。开头八条处理两种原子关系：对于每种关系，左右两个词项都可以分别是常元或变元。常元通过其在 `w` 中的隶属关系解码，变元则通过其索引在元数数码中的隶属关系解码。

```agda
      all : ⟨ δ4 ⊨ Cl.all ⟩
      all =
          atomIn f0 f0 f0 (sh 4 w) (sh 5 w) _∈̇_ (λ _ _ → refl) conDec (λ _ → conDec)
        , ( atomIn f0 f0 f1 (sh 4 w) i2 _∈̇_ (λ _ _ → refl) conDec (λ _ → varDec n A qa)
        , ( atomIn f0 f1 f0 i1 (sh 5 w) _∈̇_ (λ _ _ → refl) (varDec n A qa) (λ _ → conDec)
```

其中四条覆盖成员关系原子中常元与变元的全部组合，另有四条以相同方式覆盖相等原子。这就给出了八条原子闭包子句；其余十条处理逻辑联结词与量词。

```agda
        , ( atomIn f0 f1 f1 i1 i2 _∈̇_ (λ _ _ → refl) (varDec n A qa) (λ _ → varDec n A qa)
        , ( atomIn f1 f0 f0 (sh 4 w) (sh 5 w) _≐_ (λ _ _ → refl) conDec (λ _ → conDec)
        , ( atomIn f1 f0 f1 (sh 4 w) i2 _≐_ (λ _ _ → refl) conDec (λ _ → varDec n A qa)
        , ( atomIn f1 f1 f0 i1 (sh 5 w) _≐_ (λ _ _ → refl) (varDec n A qa) (λ _ → conDec)
        , ( atomIn f1 f1 f1 i1 i2 _≐_ (λ _ _ → refl) (varDec n A qa) (λ _ → varDec n A qa)
```

接下来的六条子句处理合取、析取、蕴涵、假以及两个无界量词。每个构造子都配以其典范标签和定义性的编码等式，因此相应的辅助引理可以直接插入所构造的键。

```agda
        , ( binIn f2 _∧̇_ (λ _ _ → refl)
        , ( binIn f3 _∨̇_ (λ _ _ → refl)
        , ( binIn f4 _⇒̇_ (λ _ _ → refl)
        , ( conIn f5 ⊥̇ refl
        , ( quIn f6 ∃̇_ (λ _ → refl)
```

最后四条子句处理有界全称量化与有界存在量化。每种量化各有一条以常元为界，另一条以变元为界；`conDec` 与 `varDec` 分别证明它们是外层元数处的合法词项。至此，这个嵌套元组给出了 `Cl.all` 的全部分量。

```agda
        , ( quIn f7 ∀̇_ (λ _ → refl)
        , ( bqIn f8 f0 (sh 8 w) ∀̇∈ (λ _ _ → refl) (λ _ _ _ _ → conDec)
        , ( bqIn f8 f1 i5 ∀̇∈ (λ _ _ → refl) (λ _ _ _ _ → varDec n A qa)
        , ( bqIn f9 f0 (sh 8 w) ∃̇∈ (λ _ _ → refl) (λ _ _ _ _ → conDec)
        ,   bqIn f9 f1 i5 ∃̇∈ (λ _ _ → refl) (λ _ _ _ _ → varDec n A qa) ))))))))))))))))
```

还需在环境塔的每个条目 `q` 处证明这些闭包子句。环境塔定理在命题截断下把 `q` 表示为某个 `n` 对应的典范条目 `(# n, envSet W n)`；其中关于第一分量的等式将记录的元数与 `# n` 对齐，于是 `At.all` 汇集的十八条子句可以应用于该条目。

```agda
    close : ⟨ γ ⊨ closeAt C w E N ⟩
    close q q∈ = bothAll-in i0 (Close.all C w N) (q ∷ γ) (λ ar F s s∈ ar∈ F∈ e →
      PT.rec (snd ((F ∷ ar ∷ s ∷ q ∷ γ) ⊨ Close.all C w N))
        (λ { (n , qp) → At.all q q∈ ar F s n (pr-inj (sym e ∙ qp) .fst) })
        (Tower.tower-out W q (subst (λ u → ⟨ fst q ∈ u ⟩) qE q∈)))
```

典范码域 `AllCodes W` 至此满足 `codesAt` 的两个部分：`shape` 表明每个成员都具有记录的元数和十种合法载荷形状之一，`close` 则表明由合法的直接组成部分组装出的每个键都属于该域。这一结论确立了码域本身的充分性：它的语法描述恰好收录所有真实的公式键。

```agda
  holds : ⟨ γ ⊨ codesAt C w E N ⟩
  holds = shape , close
```

## 小结

两个方向在典范码域上汇合。可靠性把 `AllCodes W` 的每个成员解码为其记录元数处的公式键，完备性则把每个真实的公式键送回该码域；`CodesHolds` 证明内部的形状与封闭描述足以支撑这两个结论。