递归定义的图

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

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

    at : (z e p : S)
       → ⟨ (z ∷ e ∷ p ∷ []) ⊨ prAtL (suc zero) (suc (suc zero)) zero ⟩
       ≡ (e .fst ≡ pr (p .fst) (z .fst))
    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 ] ((e .fst ≡ pr (p .fst) (z .fst)) × ⟨ (z ∷ p ∷ []) ⊨ φ ⟩) ∥₁
  pair-out e p = map₁ (λ { (z , (q , h)) →

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

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

  pair-in : (e p z : S) → e .fst ≡ pr (p .fst) (z .fst) → ⟨ (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 = ⟨ x .fst ∈ dom .fst ⟩

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

集合的成员关系取值于命题，因此 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 (λ p → p .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 (x .fst) ((fn x m) .fst)。

  uniq : (x : S) (m : Mem x) (p : S) → ⟨ (p ∷ x ∷ []) ⊨ Fo.fo ⟩ → p ≡ pairOf x m
  uniq x m p h = rec₁ (isSetS p (pairOf x m))
    (λ { (z , (e , g)) → Σ≡Prop (λ v → (isL v) .snd)
      (e ∙ cong (λ w → pr (x .fst) (w .fst)) (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 → ((w ∷ x ∷ []) ⊨ Fo.fo) .snd) (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 (x .fst) ((fn x m) .fst) ∈ F .fst ⟩
F-in x m = subst (λ w → ⟨ w ∈ F .fst ⟩) (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 ∈ F .fst ⟩
      → ∥ Σ[ x ∶ S ] Σ[ m ∶ Mem x ] (p ≡ pr (x .fst) ((fn x m) .fst)) ∥₁
F-out p h = rec₁ squash₁ step (T.table-out pS h)
  where
  pS : S

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

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

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

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

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

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 (y .fst) ((fn x m) .fst))

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

恢复两个坐标

固定 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 → (isL v) .snd) (sym (pr-inj e .fst))) (m' , pr-inj e .snd)

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

若有序对编码 pr(x,fst .fst y) 属于 F，向外刻画便给出 x'、m'，以及它与 pr(x',fst .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 (λ p → p .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 (x .fst) (y .fst) ∈ F .fst) ⟩ → Mem x
  fwd x = rec₁ (isPropMem x) (λ { (y , p) → (pair-out x y p) .fst })

最后，从两个方向证明定义域公式。若 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 (x .fst) (y .fst) ∈ F .fst) ⟩
  bwd x m = ∣ fn x m , F-in x m ∣₁