递归定义的图

L 中的递归在内部定义域的每一点给出唯一取值。集合论函数由其图表示，即输入在前、输出在后的有序对 pr(x , y) 所成的集合。本章把递归的取值关系转换成这样的集合 F，再证明 F 具有函数性，并且定义域恰为原来的定义域。

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )

图本身必须用对象语言描述。现有语法可以组成合取与存在陈述，而改名把已有的二元取值关系放到新的量词之下。外围运算 pr 给出有序对编码，其单射性随后可从编码相等恢复两个坐标。

open import FOL.Syntax using ( Formula; _∧̇_; ∃̇_ )
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj )

可构造的有序对运算产生 L 中的元素，其底层集合就是外围的有序对编码。于是，一般递归定理可以把替换应用于描述这些有序对的公式。由于可构造性证明是命题，可构造元素的相等可归结为其底层集合的相等。

open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Recursion {ℓ} lem using ( Recursion; module Of )
open import L.Coding.Model {ℓ}
  using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-in; domAt; domAt-intro )

open import Cubical.Data.Sigma using ( Σ≡Prop )

下文有若干命题由截断的存在陈述得到。截断只能消去到命题目标；累积层级中的成员关系与相等恰好具有这一性质。因此，可以使用存在见证，而不必作全局选择。

open import Cubical.Foundations.HLevels using ( isPropΣ )
open import Cubical.Functions.Logic using ( ∃[∶]-syntax )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )

公式在可构造结构中解释。局部的满足记号及其改名定理，把句法代换与环境变化联系起来；下文关于函数图的陈述都采用这一语义。

open hPropStructure 𝒮ʟ

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename )
module PairFo (φ : Formula S ) where

有序对公式

固定一条二元公式 φ，把它读作取值与索引之间的关系。模块 PairFo 构造另一条二元公式：给定候选有序对 e 与索引 p，它断言存在取值 z 满足 φ(z,p)，并且 e 是有序对 pr(p,z)。

  ρ : Fin  → Fin 
  ρ zero       = zero
  ρ (suc zero) = suc (suc zero)

改名映射记录 φ 的两个自由变元如何出现在存在量词之下。取值变元仍位于零号槽，并由该量词约束；索引变元移到二号槽。公式 pairFo 被声明为不透明，因此后续推理使用已经证明的语义刻画，而不展开其定义。

  opaque
    pairFo : Formula S 

该公式在存在量词之下合取两个断言。第一项说明 e 编码 p 与被量化取值组成的有序对；第二项是改名后的 φ。因此，这段语法直接对应函数图成员的数学描述。

    pairFo = ∃̇ (prAtL (suc zero) (suc (suc zero)) zero ∧̇ renameFo ρ φ)

一致性证明验证改名保持预期的环境。在较长环境 (z ∷ e ∷ p ∷ []) 中，改名后的取值槽读出 z，索引槽读出 p，与原公式在 (z ∷ p ∷ []) 中的读法完全相同。

    private
      ag : (z e p : S) → Ren.Agrees ρ (z ∷ e ∷ p ∷ []) (z ∷ p ∷ [])
      ag z e p zero       = refl
      ag z e p (suc zero) = refl

两条语义等式为向外方向作准备。有序对公式的正确性把其满足关系等同于外围等式 fst e ≡ pr (fst p) (fst z)；改名定理则把改名公式的满足关系等同于原公式 φ 在取值 z、索引 p 处的满足关系。

      at : (z e p : S)
         → ⟨ (z ∷ e ∷ p ∷ []) ⊨ prAtL (suc zero) (suc (suc zero)) zero ⟩
         ≡ (fst e ≡ pr (fst p) (fst z))
      at z e p = cong ⟨_⟩ (prAtL-adequate (suc zero) (suc (suc zero)) zero (z ∷ e ∷ p ∷ []))

      gr : (z e p : S)

向外读取 pairFo，得到一个经命题截断的取值 z，以及有序对等式和 φ(z,p) 的证明。向内读取则反向搬运这些数据：取值、等式与图证明共同构造 pairFo 的满足见证。下文使用的正是这两个语义方向。

         → ⟨ (z ∷ e ∷ p ∷ []) ⊨ renameFo ρ φ ⟩ ≡ ⟨ (z ∷ p ∷ []) ⊨ φ ⟩
      gr z e p = cong ⟨_⟩ (Ren.⊨-rename ρ φ (z ∷ e ∷ p ∷ []) (z ∷ p ∷ []) (ag z e p))

    pair-out : (e p : S) → ⟨ (e ∷ p ∷ []) ⊨ pairFo ⟩
             → ∥ Σ[ z ∈ S ] ((fst e ≡ pr (fst p) (fst z)) × ⟨ (z ∷ p ∷ []) ⊨ φ ⟩) ∥₁
    pair-out e p = PT.map (λ { (z , (q , h)) →

向内引理补全了语义等价，接下来固定一项递归。原来的定义域与取值关系保持不变；改变的只是送入替换的取值，它们将由单独的输出变成输入与输出组成的有序对。

      z , (transport (at z e p) q , transport (gr z e p) h) })

    pair-in : (e p z : S) → fst e ≡ pr (fst p) (fst z) → ⟨ (z ∷ p ∷ []) ⊨ φ ⟩
            → ⟨ (e ∷ p ∷ []) ⊨ pairFo ⟩
    pair-in e p z q h = ∣ z , (transport (sym (at z e p)) q , transport (sym (gr z e p)) h) ∣₁
module Graph (R₀ : Recursion) where

定义域与取值

递归给出定义域、原取值图公式，以及定义域每个成员处图取值纤维的可缩性。由此导出的取值记作 fn。局部谓词 Mem x 是 fn 所需的底层成员关系断言。

  open Of R₀ public using ( dom; graph; funct ) renaming ( val to fn )
  Mem : S → Type (ℓ-suc ℓ)
  Mem x = ⟨ fst x ∈ fst dom ⟩

  isPropMem : (x : S) → isProp (Mem x)
  isPropMem x = snd (fst x ∈ fst dom)

集合的成员关系取值于命题，因此 Mem x 是命题。于是，x 属于定义域的任意两份证明都相等。这一证明无关性保证取值 fn x m 不依赖所选的成员证书。

  private
    defines : (x : S) (m : Mem x) → ⟨ (fn x m ∷ x ∷ []) ⊨ graph ⟩
    defines x m = funct x m .fst .snd

    only : (x : S) (m : Mem x) (y : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x m
    only x m y h = sym (cong fst (funct x m .snd (y , h)))

可缩性给出关于原取值关系的两项事实。选定的中心证明公式 graph 在环境 (fn x m ∷ x ∷ []) 中得到满足；收缩则证明，在 x 处满足该公式的其他任何 y 都等于 fn x m。

    module Fo = PairFo graph renaming ( pairFo to fo; pair-out to out; pair-in to into )

    fn-irr : (x : S) (m m' : Mem x) → fn x m ≡ fn x m'
    fn-irr x m m' = cong (fn x) (isPropMem x m m')
    pairOf : (x : S) → Mem x → S
    pairOf x m = prʟ x (fn x m)

现在把有序对公式用于原取值关系。Mem x 的证明无关性给出 fn-irr；pairOf x m 则是 x 与其取值组成的可构造有序对，其底层集合为 pr (fst x) (fst (fn x m))。

    uniq : (x : S) (m : Mem x) (p : S) → ⟨ (p ∷ x ∷ []) ⊨ Fo.fo ⟩ → p ≡ pairOf x m
    uniq x m p h = PT.rec (isSetS p (pairOf x m))
      (λ { (z , (e , g)) → Σ≡Prop (λ v → snd (isL v))
        (e ∙ cong (λ w → pr (fst x) (fst w)) (only x m z g) ∙ sym (prʟ-fst x (fn x m))) })
      (Fo.out p x h)

设候选元素 p 在 x 处满足专门化后的有序对公式。向外引理仅仅给出取值 z、p 的底层集合与 pr(x,z) 之间的等式，以及 z 满足原图的证明。原取值的唯一性把 z 等同于 fn x m；复合所得等式便证明 p ≡ pairOf x m。

    R : Recursion
    R = record
      { dom   = dom
      ; graph = Fo.fo
      ; funct = λ x m →

收集函数图

构造一项新的递归，沿用原定义域，并以有序对公式作为取值关系。在 x 处，其中心为 pairOf x m；向内语义引理证明该有序对满足公式，而 uniq 证明其他所有满足公式的候选元素都与它相等。

          ( pairOf x m
          , Fo.into (pairOf x m) x (fn x m) (prʟ-fst x (fn x m)) (defines x m) )
        , λ { (p , h) → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ Fo.fo)) (sym (uniq x m p h)) } }

    module T = Of R using ( table; table-in; table-out )

  F : S

依值对的收缩把候选取值及其满足证明与选定中心比较。第一分量的相等由 uniq 给出；满足证明是命题，因此这一等式即可确定整个依值对的路径。所得记录是关于有序对的一项合法 Recursion。

  F = T.table

  F-in : (x : S) (m : Mem x) → ⟨ pr (fst x) (fst (fn x m)) ∈ fst F ⟩
  F-in x m = subst (λ w → ⟨ w ∈ fst F ⟩) (prʟ-fst x (fn x m))
    (T.table-in x (pairOf x m) m
      (Fo.into (pairOf x m) x (fn x m) (prʟ-fst x (fn x m)) (defines x m)))

把替换应用于这项递归，便形成其有序对取值的值域。这个值域就是所需的函数图 F。因此，F 是 L 的元素，其中放入的每个成员都是定义域元素与其递归确定取值组成的有序对。

  F-out : (p : V ℓ) → ⟨ p ∈ fst F ⟩
        → ∥ Σ[ x ∈ S ] Σ[ m ∈ Mem x ] (p ≡ pr (fst x) (fst (fn x m))) ∥₁
  F-out p h = PT.rec squash₁ step (T.table-out pS h)
    where
    pS : S

成员关系的向内方向直接来自替换规格。给定定义域见证 m，可构造有序对 pairOf x m 满足有序对公式，因此属于替换的值域。沿 prʟ-fst 搬运后，这被表述为外围编码 pr (fst x) (fst (fn x m)) 属于 F 的底层集合。

    pS = p , isL-trans {x = fst F} {y = p} h (snd F)

    step : Σ[ x ∈ S ] (Mem x × ⟨ (pS ∷ x ∷ []) ⊨ Fo.fo ⟩)
         → ∥ Σ[ x ∈ S ] Σ[ m ∈ Mem x ] (p ≡ pr (fst x) (fst (fn x m))) ∥₁
    step (x , (m , g)) = PT.map
      (λ { (z , (e , gz)) →

对向外方向，从外围集合 p ∈ fst F 出发。可构造性的向下封闭把 p 包装成 L 的元素 pS。替换规格首先仅仅给出索引 x、定义域证明 m，以及 pS 满足有序对公式的证明。

        x , m , (e ∙ cong (λ w → pr (fst x) (fst w)) (only x m z gz)) })
      (Fo.out pS x g)
  Fib : S → S → Type (ℓ-suc ℓ)
  Fib x y = Σ[ m ∈ Mem x ] (fst y ≡ fst (fn x m))

  isPropFib : (x y : S) → isProp (Fib x y)

随后，语义向外引理打开第二层截断，给出取值 z、有序对等式以及原取值关系的证明。原取值的唯一性把 z 替换为 fn x m。所得结论仅仅说明：对某个定义域元素 x，p 是编码 pr(x,fn x m)。

  isPropFib x y = isPropΣ (isPropMem x) (λ m → setIsSet (fst y) (fst (fn x m)))

  pair-out : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → Fib x y
  pair-out x y h = PT.rec (isPropFib x y) step (F-out (pr (fst x) (fst y)) h)
    where
    step : Σ[ x' ∈ S ] Σ[ m' ∈ Mem x' ] (pr (fst x) (fst y) ≡ pr (fst x') (fst (fn x' m')))

恢复两个坐标

固定 x 与 y 后，纤维 Fib x y 由两部分组成：定义域证明 m : Mem x，以及 y 的底层集合与 fn x m 的底层集合之间的等式。两部分都是命题：定义域成员关系取值于命题，而 V 中的相等也是命题。因此，整个纤维是命题。

         → Fib x y
    step (x' , m' , e) = subst (λ z → Fib z y)
      (Σ≡Prop (λ v → snd (isL v)) (sym (pr-inj e .fst))) (m' , pr-inj e .snd)

  γ : S ^ 
  γ = F ∷ dom ∷ []

若有序对编码 pr(fst x,fst y) 属于 F，向外刻画便给出 x'、m'，以及它与 pr(fst x',fst(fn x' m')) 的等式。pr 的单射性恢复两个坐标的等式。输入坐标的等式把 m' 搬运成 x 属于定义域的证明；输出坐标的等式给出 Fib x y 的第二分量。

  sv : ⟨ γ ⊨ svAt zero ⟩
  sv = svAt-in zero γ (λ x y y' p q →
    let (m , e)   = pair-out x y p
        (m' , e') = pair-out x y' q
    in e ∙ cong fst (fn-irr x m m') ∙ sym e')

环境 γ = F ∷ dom ∷ [] 为单值性公式与定义域公式的两个自由变元赋值。为证明单值性，取 F 中第一坐标同为 x 的两个有序对。相应纤维给出成员证明 m、m'，以及两个输出分别等于 fn x m、fn x m' 的等式。证明无关性使这两个函数值相等，因而两个输出相等。

  dm : ⟨ γ ⊨ domAt zero (suc zero) ⟩
  dm = domAt-intro zero (suc zero) γ (λ x → fwd x , bwd x)
    where
    fwd : (x : S) → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst F) ⟩ → Mem x
    fwd x = PT.rec (isPropMem x) (λ { (y , p) → fst (pair-out x y p) })

最后，从两个方向证明定义域公式。若 x 作为第一坐标出现在 F 的某个有序对中，pair-out 返回一个纤维，从而给出 Mem x 的证明。反过来，由 m : Mem x，F-in 说明有序对 pr(x,fn x m) 属于 F，所以 x 确实作为第一坐标出现。因此，所构造函数图的定义域恰为 dom。

    bwd : (x : S) → Mem x → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst F) ⟩
    bwd x m = ∣ fn x m , F-in x m ∣₁