可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。

固定宇宙层级 ℓ，并假设 lem : LEM (ℓ-suc ℓ)。这个假设为相应层级的每个命题提供判定，并始终作为下文构造的显式参数。

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

在 L 内部，每条公式都被编码为载体的元素，且每条公式都有一个键：以元数数码居前、公式编码居后的有序对。某个界处的槽位收集一条公式及其全部子公式的键，因此槽位是一棵键树，而界只是相关引理的接口参数。本章证明槽位是闭合的：凡复合公式的键位于槽位中，其直接子公式的键也位于其中；这对带子公式的七种构造子逐一成立。

抽象的闭合原理在这里落实到具体对象：由公式语法树生成的诸键满足 closedAt。这正是沿这些键递归定义图时所需的闭合前提。

语言的构造子中有七个带子公式，其余三个不带，对后者无可闭合。七条子句各是四个动作：把槽位的元素求逆回「它是谁的键」的那条公式、从子句的标签算出那条公式的构造子、把部件的键放回复合公式自己的槽位、再把它们提升到整体的槽位。

本章围绕三个数学对象展开。元数为 j 的公式 χ 的键 keyʟ χ 是数码 j 与 χ 的编码构成的有序对，而编码本身是编码模块的编码 LCode.⌜ χ ⌝。槽位 slot B φ 是由这类键组成的集合，即 φ 及其整棵子公式树的键。closedAt 则陈述：一个槽位对七个构造子闭合，即合取、析取、蕴含、两个量词与两个有界量词。

公式即对象语言的公式，其满足在可构造结构中读取：下文的满足符号一律指那里的满足。外围层级提供键与槽位所由构成的底层元素。

有序对编码键，且分量可恢复，因此一个键可以拆开为元数分量与编码分量。可构造结构承载诸编码；编码模块定义公式的编码 ⌜_⌝ 与码上的配对运算；闭包模块则逐形状陈述七条闭合子句及其引入形式。

满足表一章是三个核心对象的出处。它定义了公式的键 keyʟ、按构造子标签分解公式的形状引理 keyʟ-shape、挂在公式与某个界上的槽位 slot、把槽位元素求逆回其键所属公式的 slot-inv，以及关于键树的部件引理 Parts。

槽位元素只能在命题截断下求逆，因此每条子句都把该截断消去到一个命题。保持元数的二元情形以两个成员关系命题的合取为目标；一元情形与有界情形的目标则各是一个成员关系命题。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )

元数以数码记录，而抬升元数的构造子记录的是数码的后继；二者都取自外围的无穷集合。

open InfinitySet using ( #_; sucV )

可构造结构的载体是本章一切码、键与槽位所居的类型。

open hPropView 𝒮ʟ

这里的 Vec S n 表示长度为 n 的环境向量；重命名为 _⊨_ 的关系，则是在这种环境下读取限制可构造结构中的满足。

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

把部件的键放回去

键树由部件引理支配。Parts.self 说公式自己的键在自己的槽位中；Parts.left、Parts.right 与 Parts.only 说复合公式的槽位包含其直接部件槽位中的键：这是沿构造子树的子树包含，由部件引理与求逆给出，从不来自界的任何序或向下的闭合。界 B 在其中只是作为接口参数传递。于是闭合子句所需做的，是把子句所读的对认作某个部件的键；下面两条引理恰完成此事。

module _ (B : S) where

private
  Sl : ∀ {n} → Formula S n → S
  Sl = slot B

键的计算，就元数为 j 的公式 χ 陈述：凡第一分量为元数数码 # j、第二分量为 ⌜ χ ⌝ 的编码分量的对，都等于键 (keyʟ χ) .fst。注意三个量互不相同：⌜ χ ⌝ 是公式的编码，其第一分量才是进入键的那个量，而键是数码居前的有序对。

key≡ : ∀ {j} (χ : Formula S j) (ar p : V ℓ) → # j ≡ ar
     → p ≡ (LCode.⌜ χ ⌝) .fst → pr ar p ≡ (keyʟ χ) .fst

两条假设都必须用到：元数等式与编码分量等式。证明是穿过两条计算法则的短链：j 的数码的第一分量是 # j，而编码对的第一分量是第一分量的对。

key≡ {j} χ ar p qa qp =
    cong₂ pr (sym qa) qp
  ∙ cong (λ w → pr w ((LCode.⌜ χ ⌝) .fst)) (sym (numeralL-fst j))
  ∙ sym (prʟ-fst (numeralL j) LCode.⌜ χ ⌝)

抬升形式对元数为 suc j 的公式 χ 陈述同一事实：此时键的第一分量是元数数码的后继，而这恰是构造子抬升元数时子句所读取的量。

keyS≡ : ∀ {j} (χ : Formula S (suc j)) (ar p : V ℓ) → # j ≡ ar
      → p ≡ (LCode.⌜ χ ⌝) .fst → pr (sucV ar) p ≡ (keyʟ χ) .fst

链是同一条，只是把后继沿元数等式推过去：suc j 的数码的第一分量是 suc (# j)，而子句的抬升读法与之相合。

keyS≡ {j} χ ar p qa qp =
    cong₂ pr (cong sucV (sym qa)) qp
  ∙ cong (λ w → pr w ((LCode.⌜ χ ⌝) .fst)) (sym (numeralL-fst (suc j)))
  ∙ sym (prʟ-fst (numeralL (suc j)) LCode.⌜ χ ⌝)

七条子句

子句按各构造子所要求的闭合形状组织。共证明四个主体，每种形状一个：保持元数的二元构造子、保持元数的一元构造子、抬升元数的一元构造子、把项与抬升元数公式配对的二元构造子。同一主体下两条子句的不同只在构造子的标签与其交还的部件，而两者都是参数。每条子句经四个动作运行：把槽位元素求逆成一条公式、按标签读出其构造子、把部件的键放回该公式自己的槽位、再提升到整体的槽位。

module _ {n : ℕ} (φ : Formula S n) {k : ℕ} (γ : Vec S k) where

private
  δ : Vec S (suc (suc (suc k)))
  δ = B ∷ satTable B φ ∷ Sl φ ∷ γ

被证明闭合的递归以固定公式 φ 的槽位为索引，其环境携带三个具名条目：界、φ 处的满足表，以及该槽位。环境的其余槽位留给具体实例。

  Ci : Fin (suc (suc (suc k)))
  Ci = suc (suc zero)

位置 Ci 是槽位在此环境中的索引；每条子句都恰在这个位置读取槽位。

binSame : (k' : ℕ) (op : ∀ {m} → Formula S m → Formula S m → Formula S m)
        → (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
           → Σ[ a' ∶ Formula S m ] (Σ[ b' ∶ Formula S m ] (ψ ≡ op a' b')))
        → (∀ {m} (a' b' : Formula S m)
           → LCode.payOf (op a' b') ≡ prʟ LCode.⌜ a' ⌝ LCode.⌜ b' ⌝)

第一个主体覆盖保持元数的二元构造子，即合取、析取、蕴含的形状。其假设描述标签 k'：一条公式与该标签匹配，当且仅当它由同元数的两条公式 op a' b' 构成，且这种复合的载荷是两个部件编码构成的有序对。

        → (∀ {m} (a' b' : Formula S m) (z : V ℓ)
           → ⟨ z ∈ (Sl a') .fst ⟩ → ⟨ z ∈ (Sl (op a' b')) .fst ⟩)
        → (∀ {m} (a' b' : Formula S m) (z : V ℓ)
           → ⟨ z ∈ (Sl b') .fst ⟩ → ⟨ z ∈ (Sl (op a' b')) .fst ⟩)
        → ⟨ δ ⊨ binShapeAt Ci k' (bothSameAt Ci) ⟩

两条闭合方向分别是部件引理给出的左、右子树包含；结论即子句自身：槽位对标签 k' 以「交还两个部件的键」的形状闭合。

binSame k' op get payOp inL inR = binSameClosed-in Ci k' δ
  (λ c ar a b c∈ sh → rec₁
    (isProp× ((pr (ar .fst) (a .fst) ∈ (Sl φ) .fst) .snd)
             ((pr (ar .fst) (b .fst) ∈ (Sl φ) .fst) .snd))
    (λ { (m , ψ , (q , incl)) →

第一步对槽位元素 c 求逆。它仅仅地是某条元数为 m 的公式 ψ 的键，求逆同时返回该键属于 φ 的槽位。目标是两个成员关系的合取，由 isProp× 是命题，这使截断消去合法。

      let r  = keyʟ-shape ψ k' (ar .fst) (pr (a .fst) (b .fst)) (sym q ∙ sh)
          g  = get ψ (r .fst)
          a' = g .fst
          b' = g .snd .fst
          eψ = g .snd .snd

第二步计算构造子。形状引理以子句的形状证明把 ψ 对上标签 k'，随同匹配返回元数等式与载荷等式；分解假设进而把 ψ 写成两个直接子公式的 op a' b'。

          pay = sym (prʟ-fst LCode.⌜ a' ⌝ LCode.⌜ b' ⌝)
              ∙ cong (λ p → p .fst) (sym (payOp a' b'))
              ∙ cong (λ w → (LCode.payOf w) .fst) (sym eψ) ∙ r .snd .snd

第三步是关于载荷的共享计算。元素 c 是键形的对，其载荷分量记录着两个部件的编码分量；链条证明这些被记录的分量按分量分别是编码 ⌜ a' ⌝ 与 ⌜ b' ⌝：由构造子自身的载荷法则，ψ 的载荷是两个部件编码构成的对，而形状引理的载荷等式把它与从 c 读出的对连接起来。此处切莫混淆三个量：整条公式的编码 ⌜ ψ ⌝、位于其中的载荷分量，以及第一槽携带元数的最终的键。

          inψ : (χ : Formula S m) → ⟨ (keyʟ χ) .fst ∈ (Sl ψ) .fst ⟩
              → ⟨ (keyʟ χ) .fst ∈ (Sl φ) .fst ⟩
          inψ χ h = incl ((keyʟ χ) .fst) h
      in subst (λ w → ⟨ w ∈ (Sl φ) .fst ⟩)
           (sym (key≡ a' (ar .fst) (a .fst) (r .snd .fst) (sym (pr-inj pay .fst))))

第四个动作把键送回。先由辅助函数借求逆返回的包含，把任一同元数公式的键从其槽位提升到 φ 的槽位；再由形状引理的元数等式与编码单射性供给的第一分量等式喂给 key≡，把子句所读对的成员关系改写为 a' 的键的成员关系。

           (inψ a' (subst (λ w → ⟨ (keyʟ a') .fst ∈ (Sl w) .fst ⟩) (sym eψ)
             (inL a' b' _ (Parts.self B keyʟ a'))))
       , subst (λ w → ⟨ w ∈ (Sl φ) .fst ⟩)
           (sym (key≡ b' (ar .fst) (b .fst) (r .snd .fst) (sym (pr-inj pay .snd))))

右分量以右侧闭合方向与单射性供给的第二分量等式重复同一组装，改写为含 b' 那个对的成员关系。两半合拢，子句证毕。

           (inψ b' (subst (λ w → ⟨ (keyʟ b') .fst ∈ (Sl w) .fst ⟩) (sym eψ)
             (inR a' b' _ (Parts.self B keyʟ b')))) })
    (slot-inv B φ (c .fst) c∈))

消去由求逆供给，那条包含正是从那里来的。两侧分量组装完毕，子句即告证成。

andC : ⟨ δ ⊨ binShapeAt Ci 2 (bothSameAt Ci) ⟩
andC = binSame 2 _∧̇_ (λ _ m → m) (λ _ _ → refl)
         (λ a' b' → Parts.left B keyʟ (a' ∧̇ b') a' b')
         (λ a' b' → Parts.right B keyʟ (a' ∧̇ b') a' b')

合取是第一个实例：a' ∧̇ b' 的槽位包含两个合取支槽位的键。

orC : ⟨ δ ⊨ binShapeAt Ci 3 (bothSameAt Ci) ⟩
orC = binSame 3 _∨̇_ (λ _ m → m) (λ _ _ → refl)
        (λ a' b' → Parts.left B keyʟ (a' ∨̇ b') a' b')
        (λ a' b' → Parts.right B keyʟ (a' ∨̇ b') a' b')

析取是形状相同的第二个实例，带自己的标签与自己的部件引理。

impC : ⟨ δ ⊨ binShapeAt Ci 4 (bothSameAt Ci) ⟩
impC = binSame 4 _⇒̇_ (λ _ m → m) (λ _ _ → refl)
         (λ a' b' → Parts.left B keyʟ (a' ⇒̇ b') a' b')
         (λ a' b' → Parts.right B keyʟ (a' ⇒̇ b') a' b')

蕴含是第三个：a' ⇒̇ b' 的槽位包含前件槽位的键与后件槽位的键，子句由同样四个动作证得。

unSame : (k' : ℕ) (op : ∀ {m} → Formula S m → Formula S m)
       → (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
          → Σ[ a' ∶ Formula S m ] (ψ ≡ op a'))
       → (∀ {m} (a' : Formula S m) → LCode.payOf (op a') ≡ LCode.⌜ a' ⌝)

辅助引理 unSame 证明了一个假想的、保持元数的一元运算所满足的相应闭合原理。本语言的十个构造子都不具有这种形状，因此 closedAt 不使用这一辅助引理。

       → (∀ {m} (a' : Formula S m) (z : V ℓ)
          → ⟨ z ∈ (Sl a') .fst ⟩ → ⟨ z ∈ (Sl (op a')) .fst ⟩)
       → ⟨ δ ⊨ unShapeAt Ci k' (oneSameAt Ci) ⟩

闭合方向与结论都是单部件形状：被要求交还的只有那唯一子公式的键。

unSame k' op get payOp inA = unSameClosed-in Ci k' δ
  (λ c ar a c∈ sh → rec₁ ((pr (ar .fst) (a .fst) ∈ (Sl φ) .fst) .snd)
    (λ { (m , ψ , (q , incl)) →
      let r  = keyʟ-shape ψ k' (ar .fst) (a .fst) (sym q ∙ sh)
          g  = get ψ (r .fst)

证明以一个分量运行同样的四个动作。求逆产出 ψ 及其到 φ 槽位的包含，形状引理按标签分解它，而此处的读取只涉及元数与那唯一的编码。

          a' = g .fst
          eψ = g .snd
          pay = cong (λ p → p .fst) (sym (payOp a'))
              ∙ cong (λ w → (LCode.payOf w) .fst) (sym eψ) ∙ r .snd .snd
      in subst (λ w → ⟨ w ∈ (Sl φ) .fst ⟩)

这里的共享计算更短：op a' 的载荷就是 a' 自己的编码，故链条把元素 c 中记录的编码分量直接认同为 a' 的编码分量，无须拆分任何对。

           (sym (key≡ a' (ar .fst) (a .fst) (r .snd .fst) (sym pay)))
           (incl ((keyʟ a') .fst)
             (subst (λ w → ⟨ (keyʟ a') .fst ∈ (Sl w) .fst ⟩) (sym eψ)
               (inA a' _ (Parts.self B keyʟ a')))) })
    (slot-inv B φ (c .fst) c∈))

第四个动作一次性组装该情形：a' 的键在自己的槽位中，inA 把它移入 op a' 的槽位，incl 提升到 φ 的槽位，key≡ 完成改写，元数等式包含在内。

unSucc : (k' : ℕ) (op : ∀ {m} → Formula S (suc m) → Formula S m)
       → (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
          → Σ[ a' ∶ Formula S (suc m) ] (ψ ≡ op a'))
       → (∀ {m} (a' : Formula S (suc m)) → LCode.payOf (op a') ≡ LCode.⌜ a' ⌝)
       → (∀ {m} (a' : Formula S (suc m)) (z : V ℓ)

第三个主体覆盖抬升元数的一元构造子，即两个量词的形状。其假设是抬升版本：标签恰与由抬升元数公式经 op 构成的公式匹配，载荷就是该公式自己的编码，且唯一一条闭合方向把它的键送入复合槽位。

          → ⟨ z ∈ (Sl a') .fst ⟩ → ⟨ z ∈ (Sl (op a')) .fst ⟩)
       → ⟨ δ ⊨ unShapeAt Ci k' (oneSuccAt Ci) ⟩

读取与结论使用抬升形式：子句读取的对以元数数码的后继居首，并要求子公式的键以单部件形状交还。

unSucc k' op get payOp inA = unSuccClosed-in Ci k' δ
  (λ c ar a c∈ sh → rec₁ ((pr (sucV (ar .fst)) (a .fst) ∈ (Sl φ) .fst) .snd)
    (λ { (m , ψ , (q , incl)) →
      let r  = keyʟ-shape ψ k' (ar .fst) (a .fst) (sym q ∙ sh)
          g  = get ψ (r .fst)

前两个动作照旧：把元素求逆成公式，再按标签分解出唯一的、元数抬升的子公式。

          a' = g .fst
          eψ = g .snd
          pay = cong (λ p → p .fst) (sym (payOp a'))
              ∙ cong (λ w → (LCode.payOf w) .fst) (sym eψ) ∙ r .snd .snd
      in subst (λ w → ⟨ w ∈ (Sl φ) .fst ⟩)

载荷计算把被记录的编码分量认同为子公式的编码。另一方面，形状等式给出 # m ≡ ar .fst；只有 keyS≡ 对该等式施加 sucV 时，后继才被引入。

           (sym (keyS≡ a' (ar .fst) (a .fst) (r .snd .fst) (sym pay)))
           (incl ((keyʟ a') .fst)
             (subst (λ w → ⟨ (keyʟ a') .fst ∈ (Sl w) .fst ⟩) (sym eψ)
               (inA a' _ (Parts.self B keyʟ a')))) })
    (slot-inv B φ (c .fst) c∈))

改写经由 keyS≡ 完成：它对 # m ≡ ar .fst 施加 sucV，再与编码分量等式合并，从而把子句所读的对认同为 a' 的键。

binSucc : (k' : ℕ)
        → (op : ∀ {m} → Term S m → Formula S (suc m) → Formula S m)
        → (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
           → Σ[ t ∶ Term S m ] (Σ[ a' ∶ Formula S (suc m) ] (ψ ≡ op t a')))
        → (∀ {m} (t : Term S m) (a' : Formula S (suc m))

第四个主体覆盖有界量词，其构造子把一个项与一个元数抬升的公式配对。这种复合的载荷按次序编码项与子公式，而只有子公式本身是公式，故被要求交回的只有它的键。

           → LCode.payOf (op t a') ≡ prʟ LCode.⌜ t ⌝ᵗ LCode.⌜ a' ⌝)
        → (∀ {m} (t : Term S m) (a' : Formula S (suc m)) (z : V ℓ)
           → ⟨ z ∈ (Sl a') .fst ⟩ → ⟨ z ∈ (Sl (op t a')) .fst ⟩)
        → ⟨ δ ⊨ binShapeAt Ci k' (succSndAt Ci) ⟩

结论是第二分量形状：子句读取的对以抬升的元数居前、公式的编码分量居后，并要求交回子公式的键。

binSucc k' op get payOp inA = binSuccClosed-in Ci k' δ
  (λ c ar a b c∈ sh → rec₁ ((pr (sucV (ar .fst)) (b .fst) ∈ (Sl φ) .fst) .snd)
    (λ { (m , ψ , (q , incl)) →
      let r  = keyʟ-shape ψ k' (ar .fst) (pr (a .fst) (b .fst)) (sym q ∙ sh)
          g  = get ψ (r .fst)

元素 c 是键形的对，其载荷携带两个分量：居前的项 t 的编码分量，与居后的子公式 a' 的编码分量。子句读取的是抬升元数连同第二分量。

          t  = g .fst
          a' = g .snd .fst
          eψ = g .snd .snd
          pay = sym (prʟ-fst LCode.⌜ t ⌝ᵗ LCode.⌜ a' ⌝)
              ∙ cong (λ p → p .fst) (sym (payOp t a'))

共享计算把元素中记录的载荷按分量认同为 ⌜ t ⌝ᵗ 与 ⌜ a' ⌝ 的编码对。改写所消耗的是由编码单射性供给的第二分量等式；项乘坐在第一分量里，随后退出。

              ∙ cong (λ w → (LCode.payOf w) .fst) (sym eψ) ∙ r .snd .snd
      in subst (λ w → ⟨ w ∈ (Sl φ) .fst ⟩)
           (sym (keyS≡ a' (ar .fst) (b .fst) (r .snd .fst)
             (sym (pr-inj pay .snd))))
           (incl ((keyʟ a') .fst)

keyS≡ 的改写使用元数等式与第二分量等式，落定为子句所读对的成员关系。第四个动作随后把 a' 的键经它自己的槽位与闭合方向提升到 φ 的槽位，而求逆供给那条包含。

             (subst (λ w → ⟨ (keyʟ a') .fst ∈ (Sl w) .fst ⟩) (sym eψ)
               (inA t a' _ (Parts.self B keyʟ a')))) })
    (slot-inv B φ (c .fst) c∈))

两个量词例示第三个主体。各自供给标签、分解、定义性成立的载荷等式，以及唯一一条闭合方向：∃̇ a' 的槽位包含 a' 槽位的键，全称量词亦然。

exC : ⟨ δ ⊨ unShapeAt Ci 6 (oneSuccAt Ci) ⟩
exC = unSucc 6 ∃̇_ (λ _ m → m) (λ _ → refl)
        (λ a' → Parts.only B keyʟ (∃̇ a') a')

全称量词是同一主体的第二个实例，带标签七与自己的部件引理。

allC : ⟨ δ ⊨ unShapeAt Ci 7 (oneSuccAt Ci) ⟩
allC = unSucc 7 ∀̇_ (λ _ m → m) (λ _ → refl)
         (λ a' → Parts.only B keyʟ (∀̇ a') a')

两个有界量词以标签八与九例示第四个主体：∀̇∈ t a' 的槽位包含 a' 槽位的键，存在有界量词亦然。

allInC : ⟨ δ ⊨ binShapeAt Ci 8 (succSndAt Ci) ⟩
allInC = binSucc 8 ∀̇∈ (λ _ m → m) (λ _ _ → refl)
           (λ t a' → Parts.only B keyʟ (∀̇∈ t a') a')

存在有界量词是七条子句中的最后一条。

exInC : ⟨ δ ⊨ binShapeAt Ci 9 (succSndAt Ci) ⟩
exInC = binSucc 9 ∃̇∈ (λ _ m → m) (λ _ _ → refl)
          (λ t a' → Parts.only B keyʟ (∃̇∈ t a') a')

七条子句组装成闭合陈述 closedAt：φ 在该界处的槽位对每个带子公式的构造子闭合。这就消解了对编码的递归对其索引集陈述的假设；也正因如此，这样的递归才能在每个复合码处求助于直接子公式键处记录的取值。本章的三个对象各尽其用：键识别了子句所读的对，槽位树供给了闭合方向，closedAt 汇集了结果。

slotClosed : ⟨ δ ⊨ closedAt Ci ⟩
slotClosed = andC , (orC , (impC
           , (exC , (allC , (allInC , exInC)))))

使编码槽位对七种构造闭合

把部件的键放回去

七条子句