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

交互式目录 · 依赖图

固定宇宙层级 ℓ。保留这个层级参数，使构造可以在所需的各个大小处实例化，而不必把不同的宇宙视为同一个。

module L.Coding.SubformulaClosure {ℓ : Level} where

公式编码上的递归需要一个索引集，其中包含每个构造子所要求的直接子公式键。本章先对任意具有 Peel 性质的集合证明七条对象语言闭包条件，再把结果用于公式的实际子公式闭包。

证明之所以短，是因为它所需的两个部分本就是为在此处结合而构造的。闭包的元素是某条公式的键，而该公式自身带有含于其中的闭包；给定构造子形状的键有已知的诸子键，具体是哪几个由该形状的标签算出。故七条子句里的每一条都是同样四步：把元素拆开、读出它的标签、由该标签确定需要什么，再给出该公式自己的闭包早已含有的那些键。

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

open hPropView 𝒮ʟ using ( S )

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

作为模型元素的闭包

clo φ 把外部构造的集合 closure f h φ 与其可构造性证明封装起来，使其成为 L 的元素，因而可以在它上面求值 closedAt。

module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where

private
  Cl : ∀ {n} → Formula K n → V ℓ
  Cl = closure f h

clo : ∀ {n} → Formula K n → S
clo φ = closure f h φ , closureL f h φ

恢复子公式键

Peel C 表示 C 的每个元素都是某个公式的键，而且该公式自身的闭包包含于 C。这恰是根据构造子标签恢复所需直接子公式键的信息。

把它单独陈述出来不是为了整洁。后面有一章从一层里切出一个码集，须为它证同一条封闭性，而那个集合不是任何东西的闭包；它手上有的是「其诸元素即诸键」这条刻画，而 Peel 正是一条刻画所化成的东西。故七条子句只证一次，对任何可剥开的集合成立，而闭包是那两个实例中的头一个，不是主角。

Peel : V ℓ → Type (ℓ-suc ℓ)
Peel C = (x : V ℓ) → ⟨ x ∈ C ⟩
       → ∥ (Σ[ m ∶ ℕ ] Σ[ ψ ∶ Formula K m ]
             ((x ≡ key f h ψ) × ((z : V ℓ) → ⟨ z ∈ Cl ψ ⟩ → ⟨ z ∈ C ⟩))) ∥₁

七条闭包子句

辅助构造 same、one、up 与 sndUp 把剥出的公式键转成二元、一元、提升元数及有界量词构造子所需的子键；它们在七个标签上的实例证明七条闭包条件。

剥开所返回的那个截断当场消掉，这是允许的，因为要产出的是一条成员关系、或一对成员关系，而成员关系是命题。

module _ (D : S) (peel : Peel (D .fst)) where

private
  C : V ℓ
  C = D .fst

  viaKey : (k : ℕ) (c : S) (ar p : V ℓ)
         → ⟨ c .fst ∈ C ⟩ → c .fst ≡ pr ar (pr (# k) p)
         → (T : Type (ℓ-suc ℓ)) → isProp T
         → (Concl f h C k ar p → T) → T
  viaKey k c ar p c∈ sh T pT g = rec₁ pT
    (λ { (m , ψ , q , incl) →
      g (byTag f h C ψ k ar p incl (sym q ∙ sh)) })
    (peel (c .fst) c∈)

  same : ∀ {m} (γ : Vec S m) (k : ℕ)
       → ((ar a b : V ℓ) → Concl f h C k ar (pr a b)
          → ⟨ pr ar a ∈ C ⟩ × ⟨ pr ar b ∈ C ⟩)
       → ⟨ (D ∷ γ) ⊨ binShapeAt zero k (bothSameAt zero) ⟩
  same γ k use = binSameClosed-in zero k (D ∷ γ)
    (λ c ar a b c∈ sh →
      viaKey k c (ar .fst) (pr (a .fst) (b .fst)) c∈ sh _
        (isProp× ((pr (ar .fst) (a .fst) ∈ C) .snd)
                 ((pr (ar .fst) (b .fst) ∈ C) .snd))
        (use (ar .fst) (a .fst) (b .fst)))

  one : ∀ {m} (γ : Vec S m) (k : ℕ)
      → ((ar a : V ℓ) → Concl f h C k ar a → ⟨ pr ar a ∈ C ⟩)
      → ⟨ (D ∷ γ) ⊨ unShapeAt zero k (oneSameAt zero) ⟩
  one γ k use = unSameClosed-in zero k (D ∷ γ)
    (λ c ar a c∈ sh →
      viaKey k c (ar .fst) (a .fst) c∈ sh _
        ((pr (ar .fst) (a .fst) ∈ C) .snd) (use (ar .fst) (a .fst)))

  up : ∀ {m} (γ : Vec S m) (k : ℕ)
     → ((ar a : V ℓ) → Concl f h C k ar a → ⟨ pr (sucV ar) a ∈ C ⟩)
     → ⟨ (D ∷ γ) ⊨ unShapeAt zero k (oneSuccAt zero) ⟩
  up γ k use = unSuccClosed-in zero k (D ∷ γ)
    (λ c ar a c∈ sh →
      viaKey k c (ar .fst) (a .fst) c∈ sh _
        ((pr (sucV (ar .fst)) (a .fst) ∈ C) .snd) (use (ar .fst) (a .fst)))

  sndUp : ∀ {m} (γ : Vec S m) (k : ℕ)
        → ((ar a b : V ℓ) → Concl f h C k ar (pr a b)
           → ⟨ pr (sucV ar) b ∈ C ⟩)
        → ⟨ (D ∷ γ) ⊨ binShapeAt zero k (succSndAt zero) ⟩
  sndUp γ k use = binSuccClosed-in zero k (D ∷ γ)
    (λ c ar a b c∈ sh →
      viaKey k c (ar .fst) (pr (a .fst) (b .fst)) c∈ sh _
        ((pr (sucV (ar .fst)) (b .fst) ∈ C) .snd)
        (use (ar .fst) (a .fst) (b .fst)))

七条子句的合取

closedOf 把七个标签实例合成任意底层集合满足 Peel 的模型元素的合取 closedAt；closureClosed 提供 closure-inv，得到 clo φ 的结论。

closureClosed 于是就是落在闭包处的那个实例，而它的剥开就是原样的 closure-inv：两条陈述是同一个类型，因为 Peel 本就是照着那条引理的结论读出来的。

closedOf : ∀ {m} (γ : Vec S m) → ⟨ (D ∷ γ) ⊨ closedAt zero ⟩
closedOf γ =
    same γ 2 (λ _ a b r → r a b refl)
  , ( same γ 3 (λ _ a b r → r a b refl)
  , ( same γ 4 (λ _ a b r → r a b refl)
  , ( up γ 6 (λ _ _ r → r)
  , ( up γ 7 (λ _ _ r → r)
  , ( sndUp γ 8 (λ _ a b r → r a b refl)
  , sndUp γ 9 (λ _ a b r → r a b refl) )))))

closureClosed : ∀ {n m} (φ : Formula K n) (γ : Vec S m)
              → ⟨ (clo φ ∷ γ) ⊨ closedAt zero ⟩
closureClosed φ γ = closedOf (clo φ) (closure-inv f h φ) γ

小结

closedOf 给出对子码递归的索引集所需的假设，并适用于任何可剥开的集合；closureClosed 则将该结论用于闭包。两者都不涉及满足关系：七条子句只说明给定形状的键会引入哪些键，而可剥开的集合恰好包含这些键。

它的代价值得记下，因为满足关系那个实例要付的是同样的形状。四个读式、七行实例化、每个读式一条引理；内容在早一章的 byTag 里，那里把十个构造子与七项要求一次性对上，而不是对上十乘七次。byTag 本就是对着任意目标集写的，这正是此处的一般性免费的原因：闭包从来不是主角，只是头一个被递进来的东西。