关于语法的内部论证从 L 中的一组公式键开始。本章从两个方向比较候选码域与外部公式文法：域中每个成员都纯粹地可解码为某条公式的键，而每条真实公式的键都属于该域。这些结论只涉及码的隶属，不涉及被编码公式的真值或满足关系。

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

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

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

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

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

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

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

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

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 )

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

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

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

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

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

  ; 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 沿生成方向陈述：合法词项与已有子键会产生相应的新键。

  ( 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 的元素；其自然数值选取十个载荷谓词之一，并自动小于十。环境是有限向量，而层级中存放的码则是嵌套的集合论有序对。

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 ( _×_ )

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

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

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

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，以下每个环境与每条公式读法都居于其上。

open hPropStructure 𝒮ʟ using ( S )

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

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

读取描述

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

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

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

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 ≡ # 

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

  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 ⟩)) ∥₁

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

  PayN : ℕ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
  PayN  = AtomP
  PayN  = AtomP
  PayN  = BinP
  PayN  = BinP

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

  PayN  = BinP
  PayN  = ConP
  PayN  = QuP
  PayN  = QuP
  PayN  = BqP

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

  PayN  = BqP
  PayN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) _ _ = Empty.⊥*

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

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

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

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

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

  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  w)) δ h)

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

       ; (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  ar)) δ h) })

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

  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  w)) x∈ N0 refl) ∣₁

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

       ; (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  ar)) i∈ N1 refl) ∣₁ })

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

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。所有截断见证都只消去到这条隶属命题中。

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

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

        h' })
      h })

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

  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  r) (ar' ∷ c .fst ∷ c' ∷ δ) (sym (cong (λ a → pr a (fst (lookup r δ))) (sucʟ-fst (lookup ar δ))))
      , suc-in (sh  ar) i0 (ar' ∷ c .fst ∷ c' ∷ δ) (sucʟ-fst (lookup ar δ)) )) ∣₁) ∣₁) ∣₁
    where

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

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

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。有序对表达式的充分性把对象语言中的隶属转换为这条宿主层集合隶属陈述。

  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 的满足。因此，这条键子句与其宿主层读法双向一致。

  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)) 的载荷；元数与标签仍占据和一元情形相同的外层位置。

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)) 的载荷。

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

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

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

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

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

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

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 仍是环境中的任意标签值；在实例化原子封闭情形时，才要求它们为零或一。

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

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

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

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

  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。

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。词项在当前元数处检查，而主体键在后继元数处检查；把二者保留为不同载荷分量，正好记录这一文法不对称性。

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

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

  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 在后继元数处的隶属由外围载荷谓词另行给出。

  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 比较。

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

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

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

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

    module Sh = Shape C w N
  open CodesSem Wv Cv

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

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

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

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

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

  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  w) (sh  (N f0)) (sh  (N f1)) (u ∷ t ∷ s ∷ δ) q0 q1 ht
               , isTm-out i0 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (u ∷ t ∷ s ∷ δ) q0 q1 hu ) ) })

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

    (bothEx-out i0 tmBody δ h)

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

  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  w) (sh  (N f0)) (sh  (N f1)) (δ12 t u e) q0 q1 ht

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

        , isTm-in i0 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (δ12 t u e) q0 q1 hu ) })
    where
    δ12 : (t u : V ℓ) (e : R ≡ pr t u) → S ^ ( + 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 都属于码集的证明。两个应用原子的充分性在扩展环境中识别出这两份隶属关系。

  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  C) i8 i1 (b ∷ a ∷ s ∷ δ)) ha
               , subst ⟨_⟩ (appAt-adequate (sh  C) i8 i0 (b ∷ a ∷ s ∷ δ)) hb ) ) })

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

    (bothEx-out i0 binBody δ h)

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

  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  C) i8 i1 (δ12 a b e))) ha

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

        , subst ⟨_⟩ (sym (appAt-adequate (sh  C) i8 i0 (δ12 a b e))) hb ) })
    where
    δ12 : (a b : V ℓ) (e : R ≡ pr a b) → S ^ ( + 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；与零标签等式复合便得到向外方向。

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

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

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

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

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

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

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

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

  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  w) (sh  (N f0)) (sh  (N f1)) (a ∷ t ∷ s ∷ δ) q0 q1 ht
               , keyUp-out (sh  C) i8 i0 (a ∷ t ∷ s ∷ δ) ha ) ) })

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

    (bothEx-out i0 bqBody δ h)

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

  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  w) (sh  (N f0)) (sh  (N f1)) (δ12 t a e) q0 q1 ht

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

        , keyUp-in (sh  C) i8 i0 (δ12 t a e) ha ) })
    where
    δ12 : (t a : V ℓ) (e : R ≡ pr t a) → S ^ ( + 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 ∷ δ

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

  payN-out : (k : ℕ) → ⟨ δ ⊨ Sh.payN k ⟩ → PayN k A R
  payN-out  = atom-out
  payN-out  = atom-out
  payN-out  = bin-out
  payN-out  = bin-out

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

  payN-out  = bin-out
  payN-out  = con-out
  payN-out  = qu-out
  payN-out  = qu-out
  payN-out  = bq-out

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

  payN-out  = bq-out
  payN-out (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) h = h

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

  payN-in : (k : ℕ) → PayN k A R → ⟨ δ ⊨ Sh.payN k ⟩
  payN-in  = atom-in
  payN-in  = atom-in
  payN-in  = bin-in
  payN-in  = bin-in

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

  payN-in  = bin-in
  payN-in  = con-in
  payN-in  = qu-in
  payN-in  = qu-in
  payN-in  = bq-in

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

  payN-in  = bq-in
  payN-in (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) h = h

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

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

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

    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 处的读式读取。

  at-out : (j : Fin ) → ⟨ δ ⊨ 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 ) })

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

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

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

  at-in : (j : Fin ) (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  (N j)) δ) rS e' (Sh.pay j)
      (PayRead.payN-in C w N (rS ∷ container pS (lookup (sh  (N j)) δ) rS e' .fst ∷ δ) tg (toℕ j) pay)
      (sh  (N j)) refl

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

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

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

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

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

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

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

module ShapeRead {m : ℕ} (C w E : Fin m) (N : Fin  → 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。这样，嵌套见证分别显露外层元数与内层带标签载荷。

    module Sh = Shape C w N
    inner : Formula S ( + 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 处合法的带标签载荷。所有存在数据都经过命题截断，并不声称分解唯一。

  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，以及十路载荷公式的满足。

  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。

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

    (h c c∈)

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

  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  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。两个配对容器共同提供嵌套存在公式所需的环境。

          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

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

          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 相符。

    (k c c∈)

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

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

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

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

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

  atomClose-out : (k Nx Ny : Fin ) (X : Fin ( + m)) (Y : Fin ( + 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∈ =

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

    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  C) i3 (sh  (N k)) (sh  (N Nx)) i1 (sh  (N Ny)) i0 (y ∷ x ∷ δ) (h x x∈ y y∈))

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

  atomClose-in : (k Nx Ny : Fin ) (X : Fin ( + m)) (Y : Fin ( + 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∈ =

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

    atomKey-in (sh  C) i3 (sh  (N k)) (sh  (N Nx)) i1 (sh  (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) 为载荷的二元键仍属于码集。

  binClose-out : (k : Fin ) → ⟨ δ ⊨ 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₂ =

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

    subst (λ u → ⟨ u ∈ Cv ⟩) (cong (pr A) (cong (λ v → pr v (pr (fst a) (fst b))) (tg k)))
      (binKey-out (sh  C) i7 (sh  (N k)) i3 i0 δ10
        (useSnd i0 δ8 arS b e₂ (binKey (sh  C) i7 (sh  (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₂ 的两次分解。

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

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

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

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

  binClose-in : (k : Fin )
              → ((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 所要求的数码对齐。

  binClose-in k g c₁ c₁∈ = sndAll-in i0 i2 (∀̇∈ (var (sh  C)) (sndAll i0 i5 (binKey (sh  C) i7 (sh  (N k)) i3 i0))) (c₁ ∷ δ) (λ a s s∈ a∈ e₁ c₂ c₂∈ →
    sndAll-in i0 i5 (binKey (sh  C) i7 (sh  (N k)) i3 i0) (c₂ ∷ a ∷ s ∷ c₁ ∷ δ) (λ b s' s'∈ b∈ e₂ →
      binKey-in (sh  C) i7 (sh  (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₂))))

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

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

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

  conClose-in : (k : Fin ) → ⟨ pr A (pr (# (toℕ k)) (# )) ∈ Cv ⟩ → ⟨ δ ⊨ Cl.conClose k ⟩
  conClose-in k h =
    unKey-in (sh  C) i1 (sh  (N k)) (sh  (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，当前元数处的量词键便属于该域。这三条假设恰是前驱切片成员的全部数据。

  quClose-out : (k : Fin ) → ⟨ δ ⊨ 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 所表示数码对应的隶属。

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

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

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

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

  quClose-in : (k : Fin )
             → ((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  C) i5 (sh  (N k)) i0) (c₁ ∷ δ) (λ ar' a s s∈ ar'∈ a∈ e₁ hs →

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

    unKey-in (sh  C) i5 (sh  (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、该词项以及主体载荷。

  bqClose-out : (k Nx : Fin ) (X : Fin ( + 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∈ =

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

    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  C) i6 (sh  (N k)) (sh  (N Nx)) i0 i1 (x ∷ δ8)
        (useBoth i0 (c₁ ∷ δ) ar' a e₁ (sucAtL i5 i1 ⇒̇ ∀̇∈ (var X) (bndKey (sh  C) i6 (sh  (N k)) (sh  (N Nx)) i0 i1))
          (h c₁ c₁∈) (suc-in i5 i1 δ8 es) x x∈))

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

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

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

  bqClose-in : (k Nx : Fin ) (X : Fin ( + 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 所要求的隶属，从而完成有界量词子句的向内读法。

  bqClose-in k Nx X g c₁ c₁∈ = bothAll-in i0 (sucAtL i5 i1 ⇒̇ ∀̇∈ (var X) (bndKey (sh  C) i6 (sh  (N k)) (sh  (N Nx)) i0 i1)) (c₁ ∷ δ) (λ ar' a s s∈ ar'∈ a∈ e₁ hs x x∈ →
    bndKey-in (sh  C) i6 (sh  (N k)) (sh  (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 把这些码重新联系到外部公式文法。相关性质都是命题，因此可以消去截断见证而不必选取代表。

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

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

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

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

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

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

  isPropPayN : (n : ℕ) (ar r : V ℓ) → isProp (PayN n ar r)
  isPropPayN  ar r = squash₁
  isPropPayN  ar r = squash₁
  isPropPayN  ar r = squash₁
  isPropPayN  ar r = squash₁

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

  isPropPayN  ar r = squash₁
  isPropPayN  ar r = setIsSet r (# )
  isPropPayN  ar r = snd (pr (sucV ar) r ∈ Cv)
  isPropPayN  ar r = snd (pr (sucV ar) r ∈ Cv)
  isPropPayN  ar r = squash₁

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

  isPropPayN  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 是命题，故截断的键可消去到它。

  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。

    key

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

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 的元素。标签充分性运输有序对等式，原有的隶属证明则给出另一个合取项；所得证据进入形状谓词的左析取支。

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