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

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

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

本章利用封闭码定义域分离出一个可构造集合，其中恰好包含所有元数上携带所需形状与封闭见证的公式码。其成员关系定理给出码、元数数码与解码公式三者之间的相互转换。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( #_ )

open hPropView 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )

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

是某个已言明元数处的键

本节给出一条读式，也是本章唯一新增的对象语言陈述。元数 k 处的键是第一分量为数码 k 的对；已有的标签读式描述第二分量已被点名的情形。这里不指定第二分量，因此把标签读式置于一个存在量词之下。两个方向分别来自该存在量词的引入与消去，并在内部使用标签读式的充分性等式。

该等式在索引、数码与环境仍为变元时证明；保持这些参数为变元，才能避免后续实例化产生额外的转换检查开销。

keyArityAtL : ∀ {n} → Fin n → ℕ → Formula S n
keyArityAtL c k = ∃̇ (tagAtL (suc c) k zero)

keyArityAtL-out : ∀ {n} (c : Fin n) (k : ℕ) (γ : Vec S n)
                → ⟨ γ ⊨ keyArityAtL c k ⟩
                → ∥ (Σ[ z ∶ S ] ((lookup c γ) .fst ≡ pr (# k) (z .fst))) ∥₁
keyArityAtL-out c k γ = map₁
  (λ { (z , hz) →
    z , subst ⟨_⟩ (tagAtL-adequate (suc c) k zero (z ∷ γ)) hz })

keyArityAtL-in : ∀ {n} (c : Fin n) (k : ℕ) (γ : Vec S n) (z : S)
               → (lookup c γ) .fst ≡ pr (# k) (z .fst)
               → ⟨ γ ⊨ keyArityAtL c k ⟩
keyArityAtL-in c k γ z e =
  ∣ z , subst ⟨_⟩ (sym (tagAtL-adequate (suc c) k zero (z ∷ γ))) e ∣₁

是某个元数处的键

上一条读式把元数指定为一个元语言的数码，而正是这一点把元数固定为一；一个必须容纳诸子码的集合无法做到这一点，因为量词的子公式位于高一级的元数上。因此元数必须变成一个被绑定的集合，而还须有某个东西向那个集合说明 # k 直接给出的事实：它是一个数码。

表达它只需一个常元。ωʟ 是 L 的元素，其元素恰是诸数码，故「元数分量属于 ωʟ」就是那个条件，而且写法与第二个合取项已经在用的那种无界成员关系相同。全式共有两个存在量词，分别约束元数与载荷，中间是对读式，再加上落在元数上的那条成员关系。

从反方向读时，这一选择的作用才显现出来。ω-specL 是命题之间的等式而非蕴含，故 ωʟ 的元素就是一个被截断的自然数；与链的投影等式复合一次，就把它变成 recover 作为元数实参所接受的那个 # m。两个方向都不需要归纳；数码那一章已经完成了。

arityNumAtL : ∀ {n} → Fin n → Formula S n
arityNumAtL c = ∃̇ (∃̇ (prAtL (suc (suc c)) (suc zero) zero
                     ∧̇ (var (suc zero) ∈̇ con ωʟ)))

arityNumAtL-out : ∀ {n} (c : Fin n) (γ : Vec S n)
                → ⟨ γ ⊨ arityNumAtL c ⟩
                → ∥ (Σ[ m ∶ ℕ ] Σ[ z ∶ S ]
                      ((lookup c γ) .fst ≡ pr (# m) (z .fst))) ∥₁
arityNumAtL-out c γ = rec₁ squash₁ (λ { (ar , h) →
  rec₁ squash₁ (λ { (z , (hp , hω)) → map₁
    (λ { (m , qm) → lower m , z
       , ( subst ⟨_⟩
             (prAtL-adequate (suc (suc c)) (suc zero) zero (z ∷ ar ∷ γ)) hp
         ∙ cong (λ w → pr w (z .fst)) (qm ∙ numeralL-fst (lower m)) ) })
    (subst ⟨_⟩ (ω-specL ar) hω) }) h })

arityNumAtL-in : ∀ {n} (c : Fin n) (γ : Vec S n) (m : ℕ) (z : S)
               → (lookup c γ) .fst ≡ pr (# m) (z .fst)
               → ⟨ γ ⊨ arityNumAtL c ⟩
arityNumAtL-in c γ m z e = ∣ numeralL m , ∣ z
  , ( subst ⟨_⟩ (sym (prAtL-adequate (suc (suc c)) (suc zero) zero
        (z ∷ numeralL m ∷ γ)))
        (e ∙ cong (λ w → pr w (z .fst)) (sym (numeralL-fst m)))
    , subst ⟨_⟩ (sym (ω-specL (numeralL m))) ∣ lift m , refl ∣₁ ) ∣₁ ∣₁

谓词

两个合取项都落在同一个自由变元上。第一项从外部固定元数，而这正是上一章明确要求的那一项。第二项是解码那两条假设的见证：一个装着实参、既封闭又成形的集合。

第二项里没有任何东西是有界的，也不需要有。引入一方由一条公式自己的子公式闭包给出该见证，消去一方则把它作为 L 的一个集合来使用，两种读法都发生在类模型处。

第二个合取项有两种写法：一般形式使用载体与实参两个槽位；常元形式则把载体固定为常元。一般形式只用一个存在量词绑定相应集合；常元形式在外层再加入一个以 A 命名的绑定。这个额外绑定是两种写法的全部差别。

hasWitnessAt : ∀ {n} → Fin n → Fin n → Formula S n
hasWitnessAt A x = ∃̇ ((var (suc x) ∈̇ var zero)
                      ∧̇ (closedAt zero ∧̇ shapedAt zero (suc A)))

hasWitness : S → Formula S 1
hasWitness A = ∃̇ ((var zero ≐ con A) ∧̇ hasWitnessAt zero (suc zero))

isCodeAny : S → Formula S 1
isCodeAny A = arityNumAtL zero ∧̇ hasWitness A

超集与集合

载体固定后，使用方会把它取为某一层。载体的元素构成字母表，正好提供编码章要求的两项参数：到层级的嵌入，以及该嵌入每个取值可构造的证明。后一项由 L 的传递性得到。相应的成员关系单独命名，因为形状谓词直接以该关系为参数。

接着构造所需超集。smallDom 接收 L 元素的小族，并返回包含该族所有元素的层。这里的小族以「一个元数及该元数处的一条公式」组成的对为索引。其尺寸满足要求，因为语法是字母表所在层级上的归纳类型，而自然数索引不会提高该尺寸。所得层含有每个键，也含有其他元素；最后用分离去除这些额外元素。

这个集合在构造处被封印。若不封印，此后每个提到它的类型都会把分离定义的展开带入转换检查，而这里导出的事实已经足够所有使用方使用。封印内部只保留读取分离结果所需的引理；由这些方向复合得到的等式放在封印外部，因为它们不依赖该集合从哪个超集中分离出来。

module _ (A : S) where

private
  ι : ⟪ A .fst ⟫ → V ℓ
  ι = ⟪ A .fst ⟫↪

  ι∈ : (m : ⟪ A .fst ⟫) → ⟨ ι m ∈ A .fst ⟩
  ι∈ m = ∈∈ₛ {a = ι m} {b = A .fst} .snd (∈ₛ⟪ A .fst ⟫↪ m)

  ιL : (m : ⟪ A .fst ⟫) → ⟨ isL (ι m) ⟩
  ιL m = isL-trans {x = A .fst} {y = ι m} (ι∈ m) (A .snd)

codeS : ∀ {n} → Formula ⟪ A .fst ⟫ n → S
codeS φ = VCode.⌜ mapFo ι φ ⌝ , codeL ι ιL φ

keyS : ∀ {n} → Formula ⟪ A .fst ⟫ n → S
keyS φ = key ι ιL φ , keyL ι ιL φ

private
  smallAny : Σ[ d ∶ S ] ((p : Σ[ n ∶ ℕ ] Formula ⟪ A .fst ⟫ n)
                        → ⟨ keyS (p .snd) ∈ˢ d ⟩)
  smallAny = smallDom (Σ[ n ∶ ℕ ] Formula ⟪ A .fst ⟫ n) (λ p → keyS (p .snd))

  sepAny : isContr
    (SetOf (λ x → (x ∈ˢ smallAny .fst) ⊓ ((x ∷ []) ⊨ isCodeAny A)))
  sepAny = hasSeparationL (smallAny .fst) (isCodeAny A)

见证的引入与消去

第二个合取项的两半都在此处证明，且是在变元元数、变元载体位与变元环境上一次证成，下面的一切只是把它们再应用一遍。元数可以是变元，因为那个合取项根本不提及它：引入为任意元数的一条公式产出一个既封闭又成形的集合，消去则接受这样的集合并调用解码，而解码从一开始就把元数作为实参。载体与环境可以是变元，则是因为两半所依赖的每条引理本来就是这样陈述的。

引入是其中不涉及额外内容的那一半。那个见证是子公式闭包，它的三个组成部分 key∈closure、closureClosed 与 closureShaped 各有一章专门处理，且都已完成。其中最后一条还多需要一件东西，即每个常元都是载体的元素；在这个字母表上，这正是当初据以定义字母表的那件事，沿那一位的等式搬过去即可。

消去是另一半。它从一个元素出发，这个元素以某个已言明元数处的键的形式给出，这正是 recover 所要求的，也是第二个合取项无法直接提供的。载体那一位的等式把「属于那一位所持有的东西」变成「属于 A」，解码那条假设因此得以应用：A 的诸元素恰是 ⟪ A ⟫ 的像，依据是「一个集合由其自身诸元素所呈现」。读出那个存在量词，就得到一个既封闭又成形的集合。随后运行解码，其答案是载体之上、落在所给定的那个元数处的一条公式。

这两个方向都应用于由外层具名绑定构造的环境，其中载体由等式固定。引入方向为该绑定提供 A，并用 refl 证明等式；消去方向读出该绑定，再把其中的数据传给一般形式。读取绑定之处必须显式写出载荷类型。 若让类型检查器推断，载体处的截断载荷会成为一个元变元，表示尚未确定公式的满足关系。同样两行代码，显式写出类型时两秒完成，不写时超过 140 秒后终止。该现象来自具体环境处的 rec₁，与图本身无关。

witnessAt-in : ∀ {n k} (b c : Fin n) (γ : Vec S n) (φ : Formula ⟪ A .fst ⟫ k)
             → (lookup b γ) .fst ≡ A .fst
             → (lookup c γ) .fst ≡ (keyS φ) .fst
             → ⟨ γ ⊨ hasWitnessAt b c ⟩
witnessAt-in b c γ φ qb qc = ∣ clo ι ιL φ
  , ( subst (λ w → ⟨ w ∈ (clo ι ιL φ) .fst ⟩) (sym qc) (key∈closure ι ιL φ)
    , ( closureClosed ι ιL φ γ
      , closureShaped ι ιL φ b γ
          (λ m → subst (λ w → ⟨ ι m ∈ w ⟩) (sym qb) (ι∈ m)) ) ) ∣₁

witnessAt-out : ∀ {n} (b c : Fin n) (γ : Vec S n)
              → (lookup b γ) .fst ≡ A .fst
              → ⟨ γ ⊨ hasWitnessAt b c ⟩
              → (k : ℕ) (z : S) → (lookup c γ) .fst ≡ pr (# k) (z .fst)
              → ∥ (Σ[ ψ ∶ Formula ⟪ A .fst ⟫ k ]
                    ((lookup c γ) .fst ≡ (keyS ψ) .fst)) ∥₁
witnessAt-out b c γ qb hw k z qz = rec₁ squash₁ viaSlot hw
  where
  Target : Type (ℓ-suc ℓ)
  Target = ∥ (Σ[ ψ ∶ Formula ⟪ A .fst ⟫ k ]
               ((lookup c γ) .fst ≡ (keyS ψ) .fst)) ∥₁

  onto : (y : V ℓ) → ⟨ y ∈ (lookup b γ) .fst ⟩
       → ∥ Σ[ m ∶ ⟪ A .fst ⟫ ] (ι m ≡ y) ∥₁
  onto y y∈ = ∣ ∈-asFiber {a = y} {b = A .fst}
    (subst (λ w → ⟨ y ∈ w ⟩) qb y∈) ∣₁

  viaSlot : Σ[ C ∶ S ] ⟨ (C ∷ γ) ⊨ ((var (suc c) ∈̇ var zero)
              ∧̇ (closedAt zero ∧̇ shapedAt zero (suc b))) ⟩
          → Target
  viaSlot (C , (x∈C , (hcl , hsh))) = map₁
    (λ { (ψ , qψ) → ψ , (qz ∙ cong (pr (# k)) (sym qψ)) })
    (Decode.recover ι zero (suc b) (C ∷ γ) onto hcl hsh k z
      (subst (λ w → ⟨ w ∈ C .fst ⟩) (qz ∙ sym (keyOf-fst k z)) x∈C))

private
  witness-in : ∀ {n} (φ : Formula ⟪ A .fst ⟫ n)
             → ⟨ (keyS φ ∷ []) ⊨ hasWitness A ⟩
  witness-in φ = ∣ A , ( refl
    , witnessAt-in zero (suc zero) (A ∷ keyS φ ∷ []) φ refl refl ) ∣₁

  witness-out : (x : S) → ⟨ (x ∷ []) ⊨ hasWitness A ⟩
              → (k : ℕ) (z : S) → x .fst ≡ pr (# k) (z .fst)
              → ∥ (Σ[ ψ ∶ Formula ⟪ A .fst ⟫ k ] (x .fst ≡ (keyS ψ) .fst)) ∥₁
  witness-out x hw k z qz = rec₁ squash₁ viaCarrier hw
    where
    viaCarrier : Σ[ B ∶ S ] ⟨ (B ∷ x ∷ [])
                   ⊨ ((var zero ≐ con A) ∧̇ hasWitnessAt zero (suc zero)) ⟩
               → ∥ (Σ[ ψ ∶ Formula ⟪ A .fst ⟫ k ] (x .fst ≡ (keyS ψ) .fst)) ∥₁
    viaCarrier (B , (qB , hB)) =
      witnessAt-out zero (suc zero) (B ∷ x ∷ []) qB hB k z qz

每个元数上的集合

得到的是载体之上诸公式在任意元数处的诸键之类，而「对诸子码作递归」必须以这一类为索引，因为量词的子公式位于高一级的元数上，一元那一类容纳不下它。

IsKeyOverAny : S → hProp (ℓ-suc ℓ)
IsKeyOverAny x =
  ∥ (Σ[ n ∶ ℕ ] Σ[ ψ ∶ Formula ⟪ A .fst ⟫ n ] (x .fst ≡ (keyS ψ) .fst)) ∥₁
  , squash₁

opaque
  AllCodes : S
  AllCodes = sepAny .fst .fst

  key∈AllCodes : ∀ {n} (φ : Formula ⟪ A .fst ⟫ n) → ⟨ keyS φ ∈ˢ AllCodes ⟩
  key∈AllCodes {n} φ = subst ⟨_⟩ (sym (sepAny .fst .snd (keyS φ)))
    ( smallAny .snd (n , φ)
    , ( arityNumAtL-in zero (keyS φ ∷ []) n (codeS φ) refl
      , witness-in φ ) )

  AllCodes-out : (x : S) → ⟨ x ∈ˢ AllCodes ⟩ → ⟨ IsKeyOverAny x ⟩
  AllCodes-out x x∈ = rec₁ squash₁
    (λ { (k , z , qz) → map₁ (λ { (ψ , q) → k , ψ , q })
      (witness-out x (sat .snd) k z qz) })
    (arityNumAtL-out zero (x ∷ []) (sat .fst))
    where
    sat : ⟨ (x ∷ []) ⊨ isCodeAny A ⟩
    sat = subst ⟨_⟩ (sepAny .fst .snd x) x∈ .snd

AllCodes-in : (x : S) → ⟨ IsKeyOverAny x ⟩ → ⟨ x ∈ˢ AllCodes ⟩
AllCodes-in x = rec₁ ((x ∈ˢ AllCodes) .snd)
  (λ { (n , ψ , q) →
    subst (λ w → ⟨ w ∈ AllCodes .fst ⟩) (sym q) (key∈AllCodes ψ) })

小结

一个集合，一条谓词。AllCodes 是 L 的元素，凭 AllCodes-out 与 AllCodes-in，它的诸元素恰是载体之上诸公式在每个元数处的诸键。

全部内容都在两个合取项里，而两者同类。封闭性与成形性合起来刻画的是码的形状，对一个键所携带的元数以及它的诸常元出自哪个字母表则完全未提，故一条针对它们写下的解码必须被给予这两样，而一个由它们造出的集合必须说明这两样。smallDom 与任意公式的分离处理其余，而两者所依赖的都只是前几章已经建立的结果。

这个集合的存在，是为了它所刻画的那一类，而不是为了某条关于它的定理。对码的递归必须在一个码的诸子码处给出答案，而量词的子公式位于高一级的元数上，一元那一类容纳不下它，故定义域只能是每个元数处的诸键。

全体公式码之集

是某个已言明元数处的键

是某个元数处的键

谓词

超集与集合

见证的引入与消去

每个元数上的集合

小结