可构造层内的最小见证映射

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

阅读指南 · 依赖地图

设对每个输入 x ∈ X，我们只在命题截断下知道存在某个 w ∈ Lset γ 满足 P(w,x)。这种逐点存在还不能给出 L 内的函数图，因为必须有同一条公式确定唯一取值。本章利用固定层的典范严格良序，选取其中最小的满足候选，再以公式表达这一选取，并把图收集为 L 的集合。这里的最小元只相对于这个层与这条序，而 P 本身可以有许多见证。

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

经典逻辑经由固定的排中律假设进入，而层上的典范序本身已经依赖这一假设。在实际搜索最小元时，它承担一个明确职责：沿良基序下降的每一步，判定是否仅仅存在一个更小且满足谓词的层成员。命题截断只在「最小见证的总类型」已经证明为命题之后消去到该类型；这并不提供从任意命题截断中抽取见证的一般方法。

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

固定宇宙层级 ℓ，并假设层级 ℓ-suc ℓ 上命题的排中律。下文选出的每个见证和构造的每个图，都相对于这一条假设以及稍后固定的层序。

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

所需的图必须用集合论的一阶对象语言表达。除了断言 P(w,x) 成立，其公式还须断言 w 位于选定层中，并且该层中没有更小的成员也满足 P。后一个条件由有界全称量词表达；把更小候选插入环境后，改名使原二元公式仍保持原义。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_; ¬̇_; ∀̇∈ )
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

这里需要层序的两种读法。宿主层的严格良序支持最小元搜索；由编码有序对构成的可构造集合 Rγ 则让同一比较能出现在对象语言的图公式中。表示引理在两种读法之间转换，但二者并非按定义相同。

open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset→isL )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Choice.StageOrders {ℓ} lem using ( orderAt; relOf ) renaming ( Mem to MemOf )
open import L.Choice.InternalWellOrder {ℓ} lem using ( relL; relL-fill; relL-rep )

严格良序同时提供最小元操作与三歧性。前者从仅仅非空的候选族中选出一个值；后者证明，任何两个满足完整最小性规格的候选必然重合。把这一规格写成公式后，替换把所得的输入值对收集为 L 的集合。

open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
  using ( SWO; leastOf; lt; eq; gt ) renaming ( Tri to Tri∙ )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Graph )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( isL-ord )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )

命题截断有意隐藏初始候选究竟是哪一个。只有先把目标改为「最小元的总类型」并证明该目标本身是命题，证明才能消去这层截断。可构造集合的相等同样不依赖其证明分量，因此整个论证中底层集合相等便已足够。

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

载体 S 把外围集合与其可构造性证明打包在一起。因此，输入与候选可以占据满足环境中的各项，而打包后的层 Lγ 与序关系 Rγ 可以作为公式常元出现。第一投影则取回隶属关系与有序对编码所需的底层集合。

open hPropStructure 𝒮ʟ using ( S )

满足关系在可构造结构 𝒮ʟ 中读取。特别地，P 已经是一条对象语言公式；本章为这条可定义关系选取见证，并不声称能把任意宿主层谓词变成可定义谓词。

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

原公式在二项环境 (w,x) 中求值。最小性引入有界竞争者后，环境变成 (w',w,x)，所以输入所在的变元必须移动，而新候选 w' 占据第一槽位。满足关系与改名的相容性将证明这次移位正确。

module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename )

指标 i0 与 i1 分别指向最前面的两个 De Bruijn 槽位；它们的数学角色随环境而定。在 (w,x) 中，二者指向提议的取值与输入；在有界环境 (w',w,x) 中，二者则指向竞争者与提议的取值。

private
  i0 : ∀ {k} → Fin (suc k)
  i0 = zero
  i1 : ∀ {k} → Fin (suc (suc k))
  i1 = suc i0

底层集合相等的两个可构造集合相等，依据是可构造性的命题性；后文对可构造集合的每个同一视都经此提升。

  S≡ : {x y : S} → fst x ≡ fst y → x ≡ y
  S≡ = Σ≡Prop (λ v → snd (isL v))

选取最小的满足成员

最小见证模块收取四份数据。带序数性的序数指数 γ 确定层；集合 X 约束输入；二元公式 P 是谓词；假设则仅仅地断言：对 X 中每个输入，都存在来自该层的候选满足谓词。候选取自整个层 Lset γ，而输入被约束在 X 之中。

module Least (γ : V ℓ) (oγ : IsOrd γ) (X : S) (P : Formula S 2)
  (have : (x : S) → ⟨ fst x ∈ fst X ⟩
        → ∥ Σ[ w ∈ S ] (⟨ fst w ∈ Lset γ ⟩ × ⟨ (w ∷ x ∷ []) ⊨ P ⟩) ∥₁) where

外围的层 Lset γ 被打包为可构造载体中的元素 Lγ。这一包可作为图公式中的常元，使公式能把搜索范围精确限制在固定的候选层内。

  opaque
    Lγ : S
    Lγ = LsetS γ oγ

等式 Lγ-fst 把这个不透明包的底层集合显式认同为 Lset γ。后文在宿主层的层与公式所用常元之间转换时，隶属证明都沿这条等式搬运。

    Lγ-fst : fst Lγ ≡ Lset γ
    Lγ-fst = refl

内部关系的编码还需要序数指数本身属于可构造宇宙。每个序数都是可构造的，而 oγ 提供了为 γ 得到这一事实所需的序数性。

    hγ : ⟨ isL γ ⟩
    hγ = isL-ord γ oγ

层序的内部实现是由编码对构成的可构造集合；最小性将在这个关系中表达。

  Rγ : S
  Rγ = relL γ hγ oγ

谓词 Mem x 记录对输入的约束，即 x ∈ X 的证据。它不对见证候选施加条件；候选的另一载体将在下一步定义为 Lset γ 的成员类型。

  Mem : S → Type (ℓ-suc ℓ)
  Mem x = ⟨ fst x ∈ fst X ⟩

序 orderAt γ oγ 作用于层成员，而非 S 的任意元素。子类型 Mγ 把界 c ∈ Lset γ 内置于每个被比较的对象中，因此最小元搜索不可能越出固定的候选层。

  private
    Mγ : Type (ℓ-suc ℓ)
    Mγ = MemOf (Lset γ)

Mγ 的元素包含一个底层集合及其属于 Lset γ 的证明。可构造层的每个成员都是可构造的，因此 memS 能把该底层集合提升到载体 S；原有的隶属证明仍保留为候选的层界。

    memS : Mγ → S
    memS c = fst c , Lset→isL γ oγ (fst c) (snd c)

候选与输入处的谓词，即 P 在「候选居前、输入居后」的环境中的对象语言满足。

    At : S → S → hProp (ℓ-suc ℓ)
    At w x = (w ∷ x ∷ []) ⊨ P

谓词 Good x 把原关系转到 orderAt γ oγ 所排序的载体上：一个层成员是合格候选，恰当其对应的 S 元素与输入 x 一同满足 P。因此，接下来的搜索排序的是 Lset γ 中的候选；它既不排序 X 中的输入，也不把候选限制到 X 中。

    Good : S → Mγ → hProp (ℓ-suc ℓ)
    Good x c = At (memS c) x

同一个底层集合可能连同两份不同的可构造性证明出现。由于可构造性是命题，S≡ 认同这两个打包后的 S 元素；沿所得路径搬运满足证明，便知重打包的层成员与原见证满足同一个 P 实例。

    toMem : (x w : S) (hw : ⟨ fst w ∈ Lset γ ⟩) → ⟨ At w x ⟩ → ⟨ Good x (fst w , hw) ⟩
    toMem x w hw = subst (λ v → ⟨ At v x ⟩) (S≡ refl)

选取在固定输入 x 及证据 m : x ∈ X 后逐点进行。该证据允许使用逐点存在假设 have；它既不说明候选属于 X，也不给 X 配备任何序。

  module Sel (x : S) (m : Mem x) where

对固定输入，假设被映到「满足条件的层成员」这一类型中。这一步只改变每个可能见证的表示；所得非空性仍带有命题截断，因此尚未选定任何特定起始成员。

    private
      nonempty : ∥ Σ[ c ∈ Mγ ] ⟨ Good x c ⟩ ∥₁
      nonempty = PT.map (λ { (w , hw , hp) → (fst w , hw) , toMem x w hw hp }) (have x m)

此时 leastOf 沿 orderAt γ oγ 下降，并返回一个实际的最小合格成员。这是特殊的消去步骤：排中律判定下降能否继续；而命题截断之所以可被消去，是因为「最小元连同其最小性证明的总类型」已经证明为命题。仅凭其中任一事实，都不足以从 nonempty 中抽取任意见证。

    opaque
      c : Mγ
      c = fst (leastOf (orderAt γ oγ) lem (Good x) nonempty)

搜索结果保留被选成员是合格候选的证明。因此，从仅仅存在走到实际最小元的过程中，原谓词并未丢失。

      c-good : ⟨ Good x c ⟩
      c-good = fst (snd (leastOf (orderAt γ oγ) lem (Good x) nonempty))

与之配套的子句给出后文所需的精确相对最小性：同一层中的任何其他合格成员，都不可能在 orderAt γ oγ 中严格低于被选者。

      minimal : (c' : Mγ) → ⟨ Good x c' ⟩ → relOf (orderAt γ oγ) c' c → Empty.⊥
      minimal = snd (snd (leastOf (orderAt γ oγ) lem (Good x) nonempty))

层序比较的是 Mγ 中的对象，而满足环境容纳的是 S 中的对象。把被选成员重打包为 e，便在不改变底层集合的前提下跨过这道接口。

    e : S
    e = memS c

由于合格性正是经同一重打包定义的，所得 S 元素立即满足 P(e,x)；这里不涉及第二次选取或新的搜索。

    e-holds : ⟨ (e ∷ x ∷ []) ⊨ P ⟩
    e-holds = c-good

被选层成员携带的隶属分量同时证明 e ∈ Lset γ。因此，谓词满足与层界来自同一个最小候选。

    e∈Lγ : ⟨ fst e ∈ Lset γ ⟩
    e∈Lγ = snd c

对带有证据 m : x ∈ X 的输入 x，函数 fn 返回这个被选候选。定义域证据显式出现，是因为存在假设只对 X 中的输入成立。

  fn : (x : S) → Mem x → S
  fn x m = Sel.e x m

在每个这样的定义域输入处，被选取值都在环境 (fn(x),x) 中满足原公式。

  fn-holds : (x : S) (m : Mem x) → ⟨ (fn x m ∷ x ∷ []) ⊨ P ⟩
  fn-holds x m = Sel.e-holds x m

同一取值属于 Lset γ。这一单独的值域陈述将在后文把可定义映射的陪域置为 Lγ；它并不表示取值属于输入集 X。

  fn-in : (x : S) (m : Mem x) → ⟨ fst (fn x m) ∈ Lset γ ⟩
  fn-in x m = Sel.e∈Lγ x m

为了用也能在 L 内表达的方式陈述最小性，设内部关系 Rγ 记录了竞争者 w' 低于 fn(x)。读出引理 relL-rep 把这一编码条目转成 orderAt γ oγ 所用的宿主层比较，而被选成员的最小性将其反驳。结论只排除 Lset γ 中满足谓词的竞争者，且只相对于这条固定的序。

  fn-least : (x : S) (m : Mem x) (w' : S) → ⟨ fst w' ∈ Lset γ ⟩ → ⟨ (w' ∷ x ∷ []) ⊨ P ⟩
           → ⟨ pr (fst w') (fst (fn x m)) ∈ fst Rγ ⟩ → Empty.⊥
  fn-least x m w' hw' hp hr = Sel.minimal x m (fst w' , hw') (toMem x w' hw' hp)
    (relL-rep γ hγ oγ (fst w' , hw') (Sel.c x m) hr)

宿主层规格 TWit w x 合并图公式必须表达的三项事实：P(w,x)、w 属于固定层，以及在 orderAt γ oγ 中不存在严格低于 w 且满足 P 的层成员。这是图取值的规格，此时图尚未被收集为内部表。

  TWit : (w x : S) → Type (ℓ-suc ℓ)
  TWit w x =
      ⟨ (w ∷ x ∷ []) ⊨ P ⟩
    × ⟨ fst w ∈ Lset γ ⟩
    × ((w' : S) → ⟨ fst w' ∈ Lset γ ⟩ → ⟨ (w' ∷ x ∷ []) ⊨ P ⟩

最后一个分量检验任意满足 w' ∈ Lset γ 与 P(w',x) 的 w'。若编码对 (w',w) 属于 Rγ，它便表示 w' 在固定层序中严格更小；这一规格所反驳的正是这种可能。

        → ⟨ pr (fst w') (fst w) ∈ fst Rγ ⟩ → Empty.⊥)

唯一性只在满足完整 TWit 规格的候选之间证明。原谓词 P 在该层中可以有许多见证；严格全序所排除的是两个不同候选既都满足 P，又都没有更小的满足者。三歧性把任意候选与被选值的比较化为下面三种情形。

  fn-unique : (x : S) (m : Mem x) (w : S) → TWit w x → fst w ≡ fst (fn x m)
  fn-unique x m w (hp , hw , mn) = go (SWO.tri∙ (orderAt γ oγ) c' (Sel.c x m))
    where
    c' : Mγ
    c' = fst w , hw

若替代候选严格低于被选者，则与最小性矛盾；若两个层成员重合，则其底层集相等。

    go : Tri∙ (relOf (orderAt γ oγ) c' (Sel.c x m)) (c' ≡ Sel.c x m)
              (relOf (orderAt γ oγ) (Sel.c x m) c')
       → fst w ≡ fst (fn x m)
    go (lt k) = Empty.rec (Sel.minimal x m c' (toMem x w hw hp) k)
    go (eq q) = cong fst q

若被选候选严格低于替代候选，便与替代候选自身的最小性矛盾；所需的比较由内部关系的填充方向供给。

    go (gt k) = Empty.rec (mn (fn x m) (fn-in x m) (fn-holds x m)
      (relL-fill γ hγ oγ (Sel.c x m) c' k))

进入有界量词后，环境为 (w',w,x)，而 P 期待 (候选,输入)。因此改名把变元 0 送到仍为 w' 的槽位 0，把变元 1 送到现为 x 的槽位 2；槽位 1 留给提议的取值 w，供 w' 与之比较。

  private
    ρ : Fin 2 → Fin 3
    ρ zero       = zero
    ρ (suc zero) = suc (suc zero)

环境一致性精确记录这两项认同：从 (w',w,x) 读取变元 0，得到 (w',x) 的第一项；改名后读取变元 1，得到其第二项。这种逐变元的一致性正是搬运整条公式 P 的满足关系所需的前提。

    ag : (w' w x : S) → Ren.Agrees ρ (w' ∷ w ∷ x ∷ []) (w' ∷ x ∷ [])
    ag w' w x zero       = refl
    ag w' w x (suc zero) = refl

最小性公式遍历 w' ∈ Lγ，并否定两项陈述的合取：编码对 (w',w) 属于 Rγ，且 P(w',x) 成立。其语义是：固定层中没有候选既在 orderAt γ oγ 中低于 w，又对同一输入见证原谓词。

  opaque
    private
      leastFo : Formula S 2
      leastFo = ∀̇∈ (con Lγ) (¬̇ (appC Rγ i0 i1 ∧̇ renameFo ρ P))

改名相容性现在认同 P 的两种读法：在 (w',w,x) 中求值 renameFo ρ P，等同于在 (w',x) 中直接求值 P。当前提议的取值 w 有意不出现在对竞争者的谓词检验中；它只出现在序比较 (w',w) 中。

      ren : (w' w x : S)
          → ⟨ (w' ∷ w ∷ x ∷ []) ⊨ renameFo ρ P ⟩ ≡ ⟨ (w' ∷ x ∷ []) ⊨ P ⟩
      ren w' w x = cong ⟨_⟩ (Ren.⊨-rename ρ P (w' ∷ w ∷ x ∷ []) (w' ∷ x ∷ []) (ag w' w x))

完整图公式把原谓词与层隶属、最小性子句合取：一个值被记录，恰当它满足谓词、位于固定层中、且在该层满足谓词的成员中最小。

    fo : Formula S 2
    fo = P ∧̇ ((var i0 ∈̇ con Lγ) ∧̇ leastFo)

向外读取 fo，可恢复语义规格的三部分：P(w,x)、隶属 w ∈ Lset γ，以及该层中没有满足谓词且被内部序记录为低于 w 的成员。公式 fo 本身不含条件 x ∈ X；这一限制在 fo 被用作 Dmap 的图公式时施加。因此，X 控制哪些输入必须取得值，而 Lset γ 控制为该输入参与比较的候选。

    fo-out : (w x : S) → ⟨ (w ∷ x ∷ []) ⊨ fo ⟩ → TWit w x
    fo-out w x (hp , (hl , hm)) =
        hp
      , subst (λ v → ⟨ fst w ∈ v ⟩) Lγ-fst hl
      , λ w' hw' hp' hr → lower (hm w' (subst (λ v → ⟨ fst w' ∈ v ⟩) (sym Lγ-fst) hw')

为得到 TWit 的最小性分量，固定竞争者 w'，并假设语义事实 pr(w',w) ∈ Rγ 与 P(w',x)。证明沿向内方向使用 appC-adequate 与改名，把这两项事实变成 fo 所否定的两个合取项的满足；有界子句随即导出矛盾。该关系条目是层序比较的对象语言编码，并不与 relOf (orderAt γ oγ) 定义相等。

          ( subst ⟨_⟩ (sym (appC-adequate Rγ i0 i1 (w' ∷ w ∷ x ∷ []))) hr
          , transport (sym (ren w' w x)) hp' ))

反过来，一个满足 TWit 的见证决定了图公式的证明。其前两个分量给出 P(w,x) 与 w ∈ Lset γ。对于有界的最小性子句，在同一层中任取 w'，并假设编码的序把 w' 排在 w 之前且 P(w',x) 成立；TWit 的最后一个分量恰好排除这一合取。

    fo-in : (w x : S) → TWit w x → ⟨ (w ∷ x ∷ []) ⊨ fo ⟩
    fo-in w x (hp , hl , mn) =
        hp
      , subst (λ v → ⟨ fst w ∈ v ⟩) (sym Lγ-fst) hl
      , λ w' hw' hc → lift (mn w' (subst (λ v → ⟨ fst w' ∈ v ⟩) Lγ-fst hw')

改名与应用充分性把这两个假设转成语义最小性所需的形式。合起来，fo-out 与 fo-in 表明 fo 恰好表达固定层中的最小见证规格。它们既不要求原谓词的见证唯一，也不比较 Lset γ 之外的候选者。

          (transport (ren w' w x) (snd hc))
          (subst ⟨_⟩ (appC-adequate Rγ i0 i1 (w' ∷ w ∷ x ∷ [])) (fst hc)))

这一精确对应使该选取成为可定义映射。映射的输入集是 X，陪域是 Lγ：对每个 x ∈ X 的证明，其取值为 fn x m，而先前的层隶属定理把该值置于 Lγ 中。图公式在环境 (取值,输入) 中读取，因此第一个变量表示选出的见证，第二个变量表示输入。

  Dmap : DefinableMap
  Dmap = record
    { dom = X ; cod = Lγ ; fn = fn
    ; into = λ x m → subst (λ v → ⟨ fst (fn x m) ∈ v ⟩) (sym Lγ-fst) (fn-in x m)
    ; graph = fo

在选出的取值处，已经证明的三项事实给出 fo 的证明：该值满足 P、属于候选层，并且其中没有更小的满足候选。反过来，任何满足 fo 的取值都携带这份完整的最小见证规格，因而等于选出的取值。这一唯一性来自两个候选各自的最小性及 orderAt γ oγ 的三歧性，而非 P 的见证唯一；由于可构造性证据是命题，底层集合的相等可提升为 S 中的相等。

    ; defines = λ x m → fo-in (fn x m) x (fn-holds x m , fn-in x m , fn-least x m)
    ; only = λ x m w h → S≡ (fn-unique x m w (fo-out w x h)) }

一旦一条公式为 X 中每个输入定义唯一取值，替换便能在 L 内收集这些取值。把图构造用于 Dmap，可得到由有序对组成的可构造集，以及使用其隶属关系所需的两个方向。

  private
    module Gr = Graph Dmap using ( F; F-in; pair-out )

把这个收集所得的集合记为 T。它的条目是有序对 (x,fn(x))，输入在前，选出的取值在后。这与公式满足所用的环境 (取值,输入) 次序相反；区分这两种约定，可避免把图公式误认成内部表本身。

  T : S
  T = Gr.F

对每个 x ∈ X，表都包含有序对 (x,fn(x))。因此，后续论证可以通过同一个可构造集的隶属关系引用这些选择，而无须对每个输入分别从仅仅非空的族中作选择。

  T-in : (x : S) (m : Mem x) → ⟨ pr (fst x) (fst (fn x m)) ∈ fst T ⟩
  T-in = Gr.F-in

反过来，条目 (x,w) ∈ T 给出证据 x ∈ X，并给出 w 的底层集合与被选取值 fn(x) 的底层集合相等。表隶属本身不返回最小性证明。在 HullCounting 中，这张表用于同步此前只在命题截断下可得的诸选择。需要单射时，还须另有底层关系的反向函数性假设，证明一个固定的相关候选不能对应两个不同输入；单射性并不单由最小选取得出。

  T-out : (x w : S) → ⟨ pr (fst x) (fst w) ∈ fst T ⟩
        → Σ[ m ∈ Mem x ] (fst w ≡ fst (fn x m))
  T-out = Gr.pair-out