L 中递归定义的内部化

递归定义可以先在元理论中给出，而它的取值随后需要组成 L 中的集合。替换定理实现这一转换。给定 L 中的定义域，以及一条在定义域每一点恰有一个取值的对象语言公式，替换便形成所有这些取值构成的集合。图公式保留取值对索引的依赖；替换所得集合只是值域，因此不同索引产生的相同取值只出现一次。

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

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

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

定义取值的关系写成带两个自由变元的对象语言公式，读取次序为值在前、索引在后。公式的满足关系在可构造结构中解释。这样，替换谈论的是 L 内部的关系，而唯一性的证明仍可在元理论中使用。

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

构造还要使用 L 的层结构。每个可构造集合都出现在某一层，而由 Type ℓ 中的类型索引的一族集合，其所在层可以由同一个序数界定。需要统一的定义域上界时，这便给出一个包含整族元素的集合。

open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset-mono )
open import L.Ordinal {ℓ} using ( boundingOrd )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )

L 中的替换适用于具有所需元数的任意公式。在这里调用它时，无需另外证明公式是 Δ₀，也无需证明其全部常元位于某个预先选定的层；这些问题已经在一般替换定理的证明中处理。第二分量为命题的依值对之间的路径，将用来表达取值的唯一性。

open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Full {ℓ} lem using ( hasReplacementL )

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.Prelude using ( isPropIsContr )
import Cubical.HITs.PropositionalTruncation as PT

对可构造论域上的谓词，SetOf 表示一个集合连同一条成员关系规格，说明该集合实现这个谓词。替换以这种形式返回值域。命题截断记录某个来源索引的存在，而不选定其中一个。

open PT using ( ∣_∣₁; ∥_∥₁ )

open hPropStructure 𝒮ʟ

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

下文的满足记号表示公式在 𝒮ʟ 中的语义。一般替换定理已经把这一语义与证明替换时采用的逐层论证联系起来；本章使用所得定理，并不假定任意公式在 L 与外围层级之间绝对。

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

递归须提供什么

三样东西。定义域是索引集，它自己是模型中的元素；因此各个索引都是 L 的集合，整个索引集也是一个集合。图是二元公式，值在前、索引在后，与模型替换字段所用的次序一致。公式的常元可以是 L 的任意元素，读取已内化表的递归就在此处指名那张表；既无复杂度上界，也不限制常元所属的层。

record Recursion : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    dom   : S
    graph : Formula S 

这里的函数性同时包含存在性与唯一性。对定义域中的每个索引，一个取值连同其满足图的证明所成的类型必须是可缩的。其中心给出取值，而收缩则证明其他任何满足图的取值都与它相同。

    funct : (x : S) → ⟨ x ∈ˢ dom ⟩
          → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ graph ⟩)

引理 smallDom 为一族 f : X → S 给出共同的包含集合，其中 X : Type ℓ。它并不声称该集合恰好是 f 的像，也不会自动给出每项递归的定义域。若采用更大的层作为定义域，仍须对其中所有成员证明取值存在且唯一。

smallDom : (X : Type ℓ) (f : X → S) → Σ[ d ∈ S ] ((x : X) → ⟨ f x ∈ˢ d ⟩)
smallDom X f = LsetS β oβ , mem
  where

界定原理施加于取值的诸层：每个 f x 都可构造，故出现在某一层，而所有 f x 的层都低于单一序数 β。这个被证明为序数的序数，即指名用作定义域的层集。

  b = boundingOrd X (λ x → stage (fst (f x)) (f x .snd))
        (λ x → stage-ord (fst (f x)) (f x .snd))
  β = b .fst
  oβ : IsOrd β
  oβ = b .snd .fst

隶属随后分两步得到：每个取值出现在自己的层，而层是单调的，故在层序中低于 β 的取值是 β 处那个层的成员。于是每个 f x 都是该定义域集合的元素。

  mem : (x : X) → ⟨ f x ∈ˢ LsetS β oβ ⟩
  mem x = Lset-mono {α = β} {β = stage (fst (f x)) (f x .snd)} (b .snd .snd x)
            (stage-mem (fst (f x)) (f x .snd))

值域

对递归 R，令 Image y 表示存在定义域中的索引 x，使图把 x 与 y 联系起来。这个存在被命题截断，因此只记录 y 作为取值出现。替换把这一谓词实现为集合，并不构造索引与取值的有序对集合。

module Of (R : Recursion) where
  open Recursion R public

  private
    Image : S → hProp (ℓ-suc ℓ)
    Image y = ∃[ x ∶ S ] (x ∈ˢ dom) ⊓ ((y ∷ x ∷ []) ⊨ graph)

把替换应用于定义域、图和函数性证明，便得到实现 Image 的集合。结果同时包含值域集合，以及准确描述其成员关系的命题。

    r : SetOf Image
    r = hasReplacementL dom graph funct .fst

值域是这一结果的第一分量。其成员关系规格说明：y 属于值域，当且仅当仅仅存在定义域中的某个索引，使图在该处取值 y。

  table : S
  table = r .fst

  table-mem : (y : S) → (y ∈ˢ table) ≡ Image y
  table-mem = r .snd

这条规格的两个方向可以分别使用。具体的图见证把相应取值放入值域；反过来，值域中的成员只给出来源索引及图见证的截断存在性，并不选定该索引。

  table-in : (x y : S) → ⟨ x ∈ˢ dom ⟩ → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩
           → ⟨ y ∈ˢ table ⟩
  table-in x y x∈ h = subst ⟨_⟩ (sym (table-mem y)) ∣ x , (x∈ , h) ∣₁

  table-out : (y : S) → ⟨ y ∈ˢ table ⟩ → ⟨ Image y ⟩
  table-out y h = subst ⟨_⟩ (table-mem y) h

存在唯一性还为定义域的每个成员确定一个元理论取值，即可缩类型中心的第一分量。若另一个 y 在同一索引处满足图，则递归数据给出的收缩证明它等于该取值。

  val : (x : S) → ⟨ x ∈ˢ dom ⟩ → S
  val x x∈ = funct x x∈ .fst .fst

  val-uniq : (x : S) (x∈ : ⟨ x ∈ˢ dom ⟩) (y : S)
           → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → val x x∈ ≡ y
  val-uniq x x∈ y h = cong fst (funct x x∈ .snd (y , h))

从唯一存在到函数性

有些构造自然得到的只是：满足图的唯一取值仅仅存在。引理 mereFunct 把这一命题截断的唯一存在陈述转换成 Recursion 所需的可缩性。它不假定可判定性，也不会脱离唯一性证明另行选择取值。

mereFunct : (graph : Formula S ) (x : S)
          → ∥ (Σ[ y ∈ S ] (⟨ (y ∷ x ∷ []) ⊨ graph ⟩
                          × ((y' : S) → ⟨ (y' ∷ x ∷ []) ⊨ graph ⟩ → y' ≡ y))) ∥₁
          → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ graph ⟩)

由于可缩性是命题，可以把截断消去到这一目标。一个代表性的唯一取值给出收缩中心，其唯一性条款把其他每个对子与中心等同；图的证明分量是命题，因而取值的等式即可确定整个依值对的等式。

mereFunct graph x = PT.rec isPropIsContr
  (λ { (y , (hy , uniq)) → (y , hy)
     , (λ { (y' , hy') → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ graph))
                           (sym (uniq y' hy')) }) })

从元理论函数出发

若元理论中已经有全函数 fn : S → S，采用 Definition 形式较为方便。除定义域与图公式外，它还要求证明：在定义域上，公式对 fn x 成立，并且公式允许的每个取值都等于 fn x。

record Definition : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    dom     : S
    fn      : S → S
    graph   : Formula S 

说「公式定义了函数」，就是两条蕴含。一条说该公式在函数自身的取值处、对每个索引成立。另一条说别无他物满足它：图在某索引处允许的任何取值都等于函数在该处的值。二者合起来就是图公式充分性的两个方向。

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

这两条蕴含确定一个递归结构。定义域与图原样保留，余下只需证明：对定义域的每一点，满足图的取值所成的纤维都是可缩的。

asRecursion : Definition → Recursion
asRecursion D = record
  { dom   = D.dom
  ; graph = D.graph

函数性是导出的，不是假设的。中心是「函数的取值连同图对它成立的证明」这一对子。任何竞争的对子都经第二条蕴含被等同于中心，因为那条蕴含迫使它的取值等于函数的取值；该同一视沿对子搬运，而其满足分量是命题。因此，在指定定义域上，图的取值纤维是可缩的。

  ; funct = λ x x∈ → (D.fn x , D.defines x x∈)
          , λ { (y , h) → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ D.graph))
                            (sym (D.only x x∈ y h)) } }
  where module D = Definition D

可定义函数的像

把前述转换应用于一个 Definition，便得到其值域作为 L 中的集合。函数仍是元理论中的描述，而图公式与替换共同证明：它在指定定义域上的全部取值组成内部集合。

module Image (D : Definition) where
  open Definition D public
  private
    module R = Of (asRecursion D)

该模块以 table 为名给出这个值域。这里没有另外导出成员关系引理；需要完整规格时，仍使用底层 Recursion 已经证明的那一份。

  table : S
  table = R.table

构造的适用范围

这项结果要求满足三项条件：定义域是 L 中的集合；关系由可构造结构上的二元公式表达；它在定义域的每一点具有唯一取值。Definition 形式从一个元理论全函数及两条充分性证明导出最后一项。辅助引理 smallDom 可以为由 Type ℓ 中类型索引的一族元素给出共同的包含层，但若把该层用作定义域，仍须对其中新增的每个成员证明存在唯一性。

在此处调用替换时，无须限制图公式的复杂度，也无须另交常元位于同一层的证书。这一便利来自已经证明的一般替换定理；它并不声称任意公式都是绝对的，而且每次应用仍须给出公式及其充分性证明。

小结

替换把内部定义域上的函数性公式转换成 L 中的值域。Recursion 直接以可缩性陈述存在唯一性；mereFunct 从截断的唯一存在导出可缩性；Definition 则从元理论全函数以及图公式充分性的两个方向导出它。所得集合记录哪些取值出现，而哪个索引产生哪个取值仍由图公式记录。