---
title: "可构造层内的最小见证映射"
module: L.GCH.LeastWitnessMap
lang: zh
site: "Bedrock"
description: "最小见证构成可定义映射"
stage: "证明 GCH"
reading_order: 112
canonical: https://bedrock.institute/zh/L.GCH.LeastWitnessMap.html
html: L.GCH.LeastWitnessMap.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/LeastWitnessMap.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.Renaming, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Axioms.Basic, L.Choice.StageOrders, L.Choice.InternalWellOrder, L.WellOrder.Base, L.DefinableInjection, L.GCH.CardinalSquareLaw, L.InjectionComposition]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.LeastWitnessMap.md, https://bedrock.institute/ja/L.GCH.LeastWitnessMap.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 可构造层内的最小见证映射

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

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

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

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

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

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

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

```agda
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γ` 则让同一比较能出现在对象语言的图公式中。表示引理在两种读法之间转换，但二者并非按定义相同。

```agda
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` 的集合。

```agda
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 )
```

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

```agda
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γ` 可以作为公式常元出现。第一投影则取回隶属关系与有序对编码所需的底层集合。

```agda
open hPropStructure 𝒮ʟ using ( S )
```

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

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

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

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

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

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

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

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

## 选取最小的满足成员

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

```agda
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γ`。这一包可作为图公式中的常元，使公式能把搜索范围精确限制在固定的候选层内。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

```agda
    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` 配备任何序。

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

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

```agda
    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` 中抽取任意见证。

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

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

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

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

```agda
      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`，便在不改变底层集合的前提下跨过这道接口。

```agda
    e : S
    e = memS c
```

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

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

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

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

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

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

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

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

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

```agda
  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 γ` 中满足谓词的竞争者，且只相对于这条固定的序。

```agda
  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` 的层成员。这是图取值的规格，此时图尚未被收集为内部表。

```agda
  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'` 在固定层序中严格更小；这一规格所反驳的正是这种可能。

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

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

```agda
  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
```

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

```agda
    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
```

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

```agda
    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'` 与之比较。

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

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

```agda
    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`，又对同一输入见证原谓词。

```agda
  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)` 中。

```agda
      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))
```

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

```agda
    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 γ` 控制为该输入参与比较的候选。

```agda
    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γ)` 定义相等。

```agda
          ( 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` 的最后一个分量恰好排除这一合取。

```agda
    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 γ` 之外的候选者。

```agda
          (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γ` 中。图公式在环境 `(取值,输入)` 中读取，因此第一个变量表示选出的见证，第二个变量表示输入。

```agda
  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` 中的相等。

```agda
    ; 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`，可得到由有序对组成的可构造集，以及使用其隶属关系所需的两个方向。

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

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

```agda
  T : S
  T = Gr.F
```

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

```agda
  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` 中，这张表用于同步此前只在命题截断下可得的诸选择。需要单射时，还须另有底层关系的反向函数性假设，证明一个固定的相关候选不能对应两个不同输入；单射性并不单由最小选取得出。

```agda
  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
```