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

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

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

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

  Lγ-fst : Lγ .fst ≡ 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 = ⟨ x .fst ∈ X .fst ⟩

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

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

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

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

候选与输入处的谓词，即 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

对每个固定输入，这个谓词面向公式的形式使用原有二元公式 P。层元素经 memS 供给环境的第一项，固定输入供给第二项。经过检查的读取是自反的，所以这个包不增加任何数学假设，只把 Good 中已有的句法显露出来。

  definedGood : (x : S) → FOL.Semantics.FormulaPredicate 𝒮ʟ Mγ S id (Good x)
  definedGood x = FOL.Semantics.presented  P (λ c → memS c ∷ x ∷ []) (λ c → refl)

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

  toMem : (x w : S) (hw : ⟨ w .fst ∈ Lset γ ⟩) → ⟨ At w x ⟩ → ⟨ Good x (w .fst , 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 = map₁ (λ { (w , hw , hp) → (w .fst , hw) , toMem x w hw hp }) (have x m)

opaque
  c : Mγ
  c = (leastOfFormula (orderAt γ oγ) (definedGood x) lem nonempty) .fst

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

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

e : S
e = memS c

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

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

对带有证据 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) → ⟨ (fn x m) .fst ∈ 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) → ⟨ w' .fst ∈ Lset γ ⟩ → ⟨ (w' ∷ x ∷ []) ⊨ P ⟩
         → ⟨ pr (w' .fst) ((fn x m) .fst) ∈ Rγ .fst ⟩ → ⊥₀
fn-least x m w' hw' hp hr = Sel.minimal x m (w' .fst , hw') (toMem x w' hw' hp)
  (relL-rep γ hγ oγ (w' .fst , 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 ⟩
  × ⟨ w .fst ∈ Lset γ ⟩
  × ((w' : S) → ⟨ w' .fst ∈ Lset γ ⟩ → ⟨ (w' ∷ x ∷ []) ⊨ P ⟩

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

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

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

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

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

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

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

  go (gt k) = ⊥₀-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  → Fin 
  ρ 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 
    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 
  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 → ⟨ w .fst ∈ v ⟩) Lγ-fst hl
    , λ w' hw' hp' hr → lower (hm w' (subst (λ v → ⟨ w' .fst ∈ 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 → ⟨ w .fst ∈ v ⟩) (sym Lγ-fst) hl
    , λ w' hw' hc → lift (mn w' (subst (λ v → ⟨ w' .fst ∈ v ⟩) Lγ-fst hw')

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

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

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

Dmap : DefinableMap
Dmap = record
  { dom = X ; cod = Lγ ; fn = fn
  ; into = λ x m → subst (λ v → ⟨ (fn x m) .fst ∈ 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 (x .fst) ((fn x m) .fst) ∈ T .fst ⟩
T-in = Gr.F-in

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

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