把可定义单射化为内部编码

在 L 外部描述一条取值规则，并不等于已经有了一个可供 L 量化的对象。要在模型内部比较基数，需要一个由有序对组成的可构造集合来记录这些取值。因此，本章的中心问题是：可定义性与逐点唯一性怎样使替换定理能够收集这张函数图。

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

唯一的经典参数是层级 ℓ-suc ℓ 上的排中律。本章中的初等步骤，例如证明唯一性、运输成员关系，以及把命题截断消去到命题中，都是构造性的。这个参数在一般替换定理把函数图收集成 L 的元素时起作用；全程不使用任何形式的选择公理。

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

固定宇宙层级 ℓ 与这一排中律实例。这里的数学问题，是怎样从宿主层的取值规则得到一个可由 L 量化的集合。取值规则本身不会被放入 L；一条公式在 L 的某个集合上描述它的值，替换据此形成可构造的函数图，再由单射性证明为该图配上内部基数比较所需的编码。

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

这里须区分三类对象。公式属于一阶语言，其常元是可构造论域的元素；满足关系在 L 上的结构中解释该公式；pr 则是在外围层级中编码底层集合有序对的柯拉托夫斯基对。稍后读取定义公式时，值在前、输入在后；收集所得函数图的条目则是 pr(输入,值)。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )

证明依次经过三种数学形式。递归由定义域、取值公式，以及定义域每一点的满足值纤维可缩这一证明组成。函数图构造用替换收集有序对，并证明单值性与恰当定义域。最后，injAt 表达尚缺的单射条件：两个条目若有相同输出，其输入便相等。

open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Recursion {ℓ} lem using ( Recursion )
open import L.Recursion.Graph {ℓ} lem
  using () renaming ( module Graph to RecursionGraph )
open import L.Coding.Injection {ℓ} lem using ( injAt; injAt-in )

对集合 a 与 b，InjCode F a b 恰有四个分量：函数图 F 是单值的，其定义域恰为 a，它满足单射性，并且其中出现的每个值都属于 b。前三项是对象语言公式的满足判断，第四项是宿主层的取值范围条件。InjL a b 则把这样的 F 及其编码之存在作命题截断。

open import L.Cardinal {ℓ} lem using ( InjCode; InjL )

两项类型论事实控制着这段证明。若依值对的第二分量取值于命题，Σ≡Prop 就能把第一分量之间的路径提升为整对之间的路径。命题截断只保留是否有元素。函数图的读回引理 pair-out 可以消去一个经命题截断的来源见证，因为它的目标纤维是命题；最后一步则用 ∣_∣₁ 隐去具体的函数图与编码。这两次操作都没有全局选出一族见证。

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )

论域 S 来自 L 上的结构：元素 x : S 由外围集合 fst x 与它可构造的命题性证书组成。成员记号取自外围层级，所以记录中的表达式明确比较底层集合，例如 fst x ∈ˢ fst dom。当构造必须返回 L 的元素时，可构造性证书仍保留在第二分量中。

open hPropStructure 𝒮ʟ using ( S )
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

记号 _⊨_ 表示外围层级限制到可构造集合所得结构中的满足关系。因此，(y ∷ x ∷ []) ⊨ graph 用 L 的元素填入 graph 的两个自由槽位来解释它。名称 AbsL 并不声称任意公式在 L 与外围层级之间绝对；本章使用的是限制结构的语义与已经证明的替换定理。

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

函数可定义的含义

一项 DefinableMap 首先指定 L 的两个元素 dom 与 cod，并不假设它们是序数或基数。宿主层取值规则 fn 只对一对数据有定义：x : S 以及 x 属于 dom 的证据 m；定义域之外无需给出值。类型允许 fn x m 提及 m。由于成员关系是命题，任意两份此类证明都相等，再由合同性可知相应取值相等。字段 into 证明每个选定值都属于 cod。

record DefinableMap : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    dom cod : S
    fn      : (x : S) → ⟨ fst x ∈ˢ fst dom ⟩ → S
    into    : (x : S) (m : ⟨ fst x ∈ˢ fst dom ⟩) → ⟨ fst (fn x m) ∈ˢ fst cod ⟩

其余字段把宿主层取值与对象语言公式联系起来。graph 有两个自由槽位，可以含有来自 S 的常元，并不要求是 Δ₀ 公式。对每个 x ∈ dom，defines 证明以所选值在前、x 在后的环境满足该公式；only 则证明任何满足公式的 y 都在 S 中等于该所选值。这些条件不约束 dom 之外的输入，only 也不假设候选 y 属于 cod。所选值落入陪域由独立的字段 into 给出。

    graph   : Formula S 
    defines : (x : S) (m : ⟨ fst x ∈ˢ fst dom ⟩)
            → ⟨ (fn x m ∷ x ∷ []) ⊨ graph ⟩
    only    : (x : S) (m : ⟨ fst x ∈ˢ fst dom ⟩) (y : S)
            → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x m

把图的表项编码成有序对

函数图由一个集合表示，因此每个输入输出表项都要先表示为有序对。定义公式在第一个语义槽位中读取函数值，在第二个槽位中读取输入；集合编码则把相应表项存为 pr(输入,函数值)。构造函数图并在随后读回其内容时，必须始终区分这两种次序。

在 L 内部构造函数图

第一项构造只假设可定义性与函数性。它从 M 形成一个属于 L 的完整函数图，并给出准确写入与读取有序对条目的方法。单射性留到下一阶段：同一函数图构造也适用于无需单射的可定义映射，例如最小见证表。

module Graph (M : DefinableMap) where
  open DefinableMap M public

为满足递归所需的假设，保留 dom 与 graph，并证明定义域每一点的满足值纤维都有中心。该中心是 (fn x m, defines x m)，即给定取值及其满足证明。成员证据 m 直接传给 fn，所以这一步不会把取值规则扩张到 dom 之外。此处既不需要 into，也不需要单射性。

  private
    R : Recursion
    R = record
      { dom = dom ; graph = graph
      ; funct = λ x m → (fn x m , defines x m)

还须把每个候选 (y,h) 收缩到该中心。字段 only 给出 y ≡ fn x m，而可缩性要求一条从中心到候选的路径，因此代码使用 sym。第二分量是满足证明，因而为命题；所以 Σ≡Prop 能把反向后的取值相等提升为整个依值对的相等。这样便构造性地证明了所需的唯一存在。

          , λ { (y , h) → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ graph)) (sym (only x m y h)) } }

现在由替换把有序对取值收集成可构造集合 F。辅助配对公式协调两种次序：原关系按 (值,输入) 解释，而 F 的成员是 pr(输入,值)。F-in 写入每个指定条目，F-out 则在命题截断下说明每个成员都来自这样的条目。固定 x 与 y 后，pair-out 把 pr(x,y) 属于 F 加强为一份定义域证明与等式 y = fn(x)。这次消去是合法的，因为 Fib x y 是命题，其中用到成员证明的证明无关性以及 V 中相等取值于命题。由这些读式可证明 sv 所表达的单值性，以及 dm 所表达的定义域恰为 dom。形成 F 的步骤使用替换定理，因而依赖给定的排中律；后续读取没有引入选择。

  open RecursionGraph R public
    using ( Mem; isPropMem; F; F-in; F-out; Fib; isPropFib; pair-out; γ; sv; dm )

最终编码的第四项条件是取值落入陪域。给定实际函数图条目 pr(fst x,fst y) ∈ fst F，pair-out 给出 m : x ∈ dom 与 e : fst y ≡ fst(fn x m)。字段 into x m 证明 fst(fn x m) 属于 fst cod。因此，成员关系必须沿 sym e 从所选值运输回 y，从而得到 y ∈ cod。这只证明像包含于陪域，并不证明陪域的每个元素都会出现。

  ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → ⟨ fst y ∈ fst cod ⟩
  ran x y h = subst (λ w → ⟨ w ∈ fst cod ⟩) (sym e) (into x m)
    where
    m = fst (pair-out x y h)
    e = snd (pair-out x y h)

从外部单射性得到编码单射

要把这张函数图变成单射编码，还须加入真正新的单射性假设。对两个各自带有 dom 成员证明的输入，它断言：若所选取值的底层集合相等，则输入的底层集合相等。成员实参仍然显式出现，因为 fn 的类型依值地依赖于它们。证明无关性保证不同成员证明之间相容，但这条假设仍按两个输入处实际给出的证据陈述。其结论的强度恰好符合 injAt 的相等条款。

module Inj (M : DefinableMap)
           (inj : (x : S) (m : ⟨ fst x ∈ˢ fst (DefinableMap.dom M) ⟩)
                  (x' : S) (m' : ⟨ fst x' ∈ˢ fst (DefinableMap.dom M) ⟩)
                → fst (DefinableMap.fn M x m) ≡ fst (DefinableMap.fn M x' m')
                → fst x ≡ fst x') where

打开 Graph M 后，已经构造出的 F 及其性质可用于单射情形。于是同时保留两种数学上有用的结论：当后续构造必须指名或组合函数图时，可以保留这个具体的 F 及其编码；也可以使用 injL，只记住某个编码单射存在。两者的区别在于具体数据与其命题性存在。

  open Graph M public

公式 injAt zero 固定输出 y，比较两个输入 x 与 x'：若 pr(x,y) 和 pr(x',y) 都属于 F，则两个输入相等。对第一条目应用 pair-out 得到 e : y = fn(x)，对第二条目应用它则得到 e' : y = fn(x')，并同时得到所需的两份定义域证明。因此，sym e ∙ e' 正是路径 fn(x) = fn(x')；宿主层假设 inj 把它化为 x = x'，injAt-in 再把这一性质转成满足判断 ij。这段论证使用的是单射性，而不仅是 only；only 比较固定输入处的输出，它支持的是单值性。

  ij : ⟨ γ ⊨ injAt zero ⟩
  ij = injAt-in zero γ (λ y x x' p q →
    let (m , e)   = pair-out x y p
        (m' , e') = pair-out x' y q
    in inj x m x' m' (sym e ∙ e'))

四元组 sv , dm , ij , ran 依次填入 InjCode F dom cod 的四个字段。其中，sv 证明单值性，dm 证明函数图的定义域恰为 dom，ij 证明对象语言中的单射性；三者都在环境 F ∷ dom ∷ [] 中陈述。最后的 ran 在宿主层断言 F 中出现的值属于 cod。这份编码没有断言满射性，所以它描述的是到 cod 的单射，而不是双射。

  code : InjCode F dom cod
  code = sv , dm , ij , ran

最后，把具体的对 (F,code) 放入命题截断。所得项 injL : InjL dom cod 断言存在一张带单射编码的可构造函数图，同时忘去所构造的是哪一张图。基数比较需要的正是这个命题，并可在目标仍为命题时对它作消去。若某项构造需要具体数据，实例化后的模块中仍可分别使用 F 与 code。因此，被内化到 L 中的是编码后的函数图，而不是外部取值规则本身。

  injL : InjL dom cod
  injL = ∣ F , code ∣₁