---
title: "構成可能な段階における最小の証人の写像"
module: L.GCH.LeastWitnessMap
lang: ja
site: "Bedrock"
description: "最小の証人が定義可能な写像をなす"
stage: "GCH の証明"
reading_order: 112
canonical: https://bedrock.institute/ja/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.Semantics, 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/zh/L.GCH.LeastWitnessMap.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

```agda
open import FOL.ZFStructure using ( module hPropView )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_; ¬̇_; ∀̇∈ )
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Semantics
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
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 )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
  using ( SWO; leastOfFormula; 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 )
```

各入力 `x ∈ X` について、`P(w,x)` を満たす `w ∈ Lset γ` があることを、命題的切り詰めのもとでだけ知っているとする。この各点での存在だけでは、`L` の内部にグラフはまだ得られない。一つの論理式が値を一意に定める必要があるからである。この章では、固定された段階の正準な狭義整列順序を使って条件を満たす最小の候補を選び、その選択を論理式で表し、グラフを `L` の集合として集める。最小性はこの段階とこの順序に相対的であり、`P` 自体は多数の証人をもってかまわない。

古典論理は、固定した排中律の仮定を通して入る。段階上の正準な順序も、すでにこの仮定に依存している。実際の最小要素の探索での役割は明確である。整礎的に降下する各段階で、条件を満たすより小さい段階の要素が単に存在するかを判定する。命題的切り詰めを除去する先は、最小の証人からなる全体型が命題であると示した後の、その型だけである。任意の切り詰めから証人を取り出す一般的方法が得られるわけではない。

求めるグラフは、集合論の一階対象言語で表さなければならない。`P(w,x)` が成り立つことに加えて、`w` が選んだ段階に属し、その段階には `P` を満たすより小さい要素がないことも論理式で述べる必要がある。後者は有界の全称量化子で表し、より小さい候補を環境へ挿入した後も、名前替えによってもとの二変数論理式の意味を保つ。

ここでは段階順序を二通りに読む必要がある。ホスト側の狭義整列順序は最小要素の探索を支え、符号化された順序対からなる構成可能集合 `Rγ` は、同じ比較を対象言語のグラフ論理式に現する。表示補題は二つの読みの間を移るが、両者を定義によって同一視するものではない。

狭義整列順序は、最小要素を得る操作と三分性の両方を与える。前者は単に非空な候補族から値を選び、後者は完全な最小性の仕様を満たす二つの候補が一致することを示す。その仕様を論理式で表した後、置換によって得られた入力と値の対を `L` の集合として集める。

命題的切り詰めは、どの初期候補が存在するかを意図的に隠する。この切り詰めを除去できるのは、目標を最小要素の全体型へ変え、その目標自体が命題であると示した後だけである。構成可能集合の等しさも証明成分には依存しないので、議論全体で底の集合の等しさがあれば十分である。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
```

台 `S` は、周囲の集合と、それが構成可能であるという証明を組にする。したがって入力と候補は充足環境の項目となり、包まれた段階 `Lγ` と順序関係 `Rγ` は論理式の定数として現れる。第一射影によって、所属と順序対の符号化に必要な底の集合を取り出せる。

```agda
open hPropView 𝒮ʟ 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} → x .fst ≡ y .fst → x ≡ y
  S≡ = Σ≡Prop (λ v → (isL v) .snd)
```

## 条件を満たす最小の要素を選ぶ

最小の証人のモジュールは、四つのデータを受け取る。順序数性をもつ順序数の指数 `γ` が段階を決め、集合 `X` が入力を制約し、二項の論理式 `P` が述語であり、`X` の各入力に対して、段階から来るある候補がそこで述語を充足すると、単に、仮定される。候補は段階 `Lset γ` の全体から取られ、入力は `X` に制約される。

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

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

</summary>
<div class="submodule-fold-content">

周囲の段階 `Lset γ` を、構成可能な台の要素 `Lγ` としてまとめる。この包みはグラフ論理式の定数として現れ、探索範囲を固定された候補の段階に正確に制限できる。

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

等式 `Lγ-fst` は、この不透明な包みの底の集合を `Lset γ` と同一視する。後でホスト側の段階と論理式が使う定数との間を移るとき、所属の証明はこの等式に沿って輸送される。

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

順序 `orderAt γ oγ` が作用するのは段階の要素であり、`S` の任意の要素ではない。部分型 `Mγ` は、比較される各対象に境界 `c ∈ Lset γ` を組み込むので、最小要素の探索が固定された候補の段階の外へ出ることはない。

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

`Mγ` の要素は、底の集合と、その集合が `Lset γ` に属するという証明を含む。構成可能な段階の各要素は構成可能なので、`memS` はその底の集合を台 `S` へ移せる。もとの所属の証明は、候補に対する段階の境界としてそのまま残る。

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

候補と入力のもとでの述語とは、`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
```

固定した各入力について、この述語の論理式に面する形は、もとの二項論理式 `P` を使う。段階の要素が `memS` を通して環境の第一成分を、固定入力が第二成分を与える。検査済みの読みは反射的なので、このパッケージは新しい数学的仮定を加えず、`Good` にすでにある構文を露出させるだけである。

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

同じ底の集合が、構成可能性の二つの証明を伴って現れることがある。構成可能性は命題なので、`S≡` は二つの包まれた `S` の要素を同一視する。得られたパスに沿って充足の証明を輸送すれば、組み直した段階の要素が、もとの証人と同じ `P` の実例を満たすと分かる。

```agda
    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` に順序が入ることも意味しない。

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

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

</summary>
<div class="submodule-fold-content">

固定した入力について、仮定を条件を満たす段階の要素の型へ写す。ここで変わるのは各候補の表現だけである。得られる非空性は命題的切り詰めの中にとどまり、特定の出発要素はまだ選ばれていない。

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

ここで `leastOfFormula` は `orderAt γ oγ` に沿って降下し、条件を満たす実際の最小要素を返す。その入力 `definedGood x` は、探索される述語の対象言語の論理式、環境、読み取り定理を運ぶ。これは特別な除去の段階である。排中律が降下を続けられるかを判定し、最小要素とその最小性の証明からなる全体型がすでに命題だと示されているため、命題的切り詰めを除去できる。どちらか一方だけでは、`nonempty` から任意の証人を取り出すことは正当化されない。

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

探索の結果には、選ばれた要素が良い候補であるという証明も残る。したがって、単なる存在から実際の最小要素へ進んでも、もとの述語は失われない。

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

対になる条項は、後で必要となる正確な相対的最小性を与える。同じ段階の他の良い要素が、`orderAt γ oγ` において選ばれた要素より真に小さくなることはない。

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

段階の順序が比較するのは `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γ : ⟨ e .fst ∈ Lset γ ⟩
    e∈Lγ = c .snd
```

</div>
</details>

証拠 `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) → ⟨ (fn x m) .fst ∈ Lset γ ⟩
  fn-in x m = Sel.e∈Lγ x m
```

`L` の内部でも表せる形で最小性を述べるため、比較候補 `w'` が `fn(x)` より小さいことを内部関係 `Rγ` が記録していると仮定する。読み出し補題 `relL-rep` は、この符号化された項目を `orderAt γ oγ` が使うホスト側の比較へ移し、選ばれた要素の最小性がそれを反駁する。結論が排除するのは `Lset γ` にある充足候補だけであり、しかもこの固定された順序に関してだけである。

```agda
  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` を満たす段階の要素がないことである。これはグラフの値の仕様であり、この時点ではグラフはまだ内部の表として集められていない。

```agda
  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'` が固定された段階順序で真に小さいことを意味し、仕様はまさにその可能性を退ける。

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

一意性を示す範囲は、完全な `TWit` の仕様を満たす候補に限られる。もとの述語 `P` は段階の中に多数の証人をもってよいのである。狭義全順序が排除するのは、異なる二つの候補がともに `P` を満たし、しかも両方により小さい充足候補がないという状況である。三分性により、任意の候補と選ばれた値との比較は、次の三場合に分かれる。

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

代替の候補が選ばれたものより真に下なら、最小性と矛盾する。二つの段階の要素が一致すれば、底の集合が等しくなる。

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

選ばれた候補が代替の候補より真に下なら、代替の候補自身の最小性と矛盾する。欠けていた比較は、内部の関係の埋めの方向によって供給される。

```agda
    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` のために残す。

```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 → ⟨ 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γ)` と定義的に等しいわけではない。

```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 → ⟨ 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 γ` の外にある候補との比較も、ここには加えられていない。

```agda
          (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γ` に入る。グラフ論理式は環境 `(値,入力)` で読まれるので、第一変数が選ばれた証人を、第二変数が入力を表す。

```agda
  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` を満たし、候補の段階に属し、その段階にはそれより小さく `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 (x .fst) ((fn x m) .fst) ∈ T .fst ⟩
  T-in = Gr.F-in
```

逆に、項目 `(x,w) ∈ T` からは、証拠 `x ∈ X` と、`w` の底の集合が選ばれた値 `fn(x)` の底の集合に等しいことが得られる。表への所属そのものは、最小性の証明を返さない。`HullCounting` では、この表を使って、それまでは命題的切り詰めのもとでしか得られなかった選択をそろえる。単射が必要な場合には、基礎となる関係について逆向きの関数性を別に仮定し、一つの関係する候補が異なる二つの入力に対応しないことを示す。単射性は最小選択だけから従うものではない。

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

</div>
</details>