構成可能な段階における最小の証人の写像

この章を読むか、読書案内と依存マップで別のルートを選べます。

各入力 x ∈ X について、P(w,x) を満たす w ∈ Lset γ があることを、命題的切り詰めのもとでだけ知っているとします。この各点での存在だけでは、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 の内部でも表せる形で最小性を述べるため、比較候補 w' が fn(x) より小さいことを内部関係 Rγ が記録していると仮定します。読み出し補題 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 を満たし、候補の段階に属し、その段階にはそれより小さく 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