---
title: "定義可能な単射を内部コードにする"
module: L.DefinableInjection
lang: ja
site: "Bedrock"
description: "定義可能な単射を内部コードにする"
stage: "順序数，単射，基数"
reading_order: 90
canonical: https://bedrock.institute/ja/L.DefinableInjection.html
html: L.DefinableInjection.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/DefinableInjection.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Recursion, L.Recursion.Graph, L.Coding.Model, L.Coding.Injection, L.Cardinal]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/L.DefinableInjection.md, https://bedrock.institute/zh/L.DefinableInjection.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 )
```

宇宙レベル `ℓ` と、この排中律のインスタンスを固定する。ここでの数学的な問題は、ホスト側の値を定める規則から、`L` が量化できる集合を得ることである。その規則自体が `L` に入るのではない。論理式が `L` のある集合上でその値を記述し、置換が構成可能な関数グラフを作り、単射性の証明がそのグラフに内部の基数比較で用いる符号を与える。

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

```agda
open import FOL.ZFStructure using ( module hPropView )
open import FOL.Syntax
  using ( Formula; var; _∈̇_; _∧̇_; _⇒̇_; ¬̇_; ∃̇_; ∀̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Recursion {ℓ} lem using ( Recursion )
open import L.Recursion.Graph {ℓ} lem
  using () renaming ( module Graph to RecursionGraph )
open import L.Coding.Model {ℓ}
  using ( svAt; svAt-in; svAt-out; domAt; domAt-in; domAt-out; domAt-intro
        ; valuesInAt; valuesInAt-in; valuesInAt-out )
open import L.Coding.Injection {ℓ} lem
  using ( injAt; injAt-in; injAt-out )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL; IsCardinalL )
```

`L` の外側で値を定める規則を記述しても、それだけでは `L` が量化できる対象にはならない。モデルの内部で基数を比較するには、その値を順序対として記録する構成可能集合が必要である。そこで本章では、定義可能性と各点での一意性から、置換によってそのグラフを集める方法を考える。

唯一の古典的パラメータは、水準 `ℓ-suc ℓ` における排中律である。本章の初等的な段階、たとえば一意性の証明、所属の輸送、命題的切り詰めを命題へ消去する操作は構成的である。このパラメータが必要になるのは、一般の置換定理によって関数グラフを `L` の要素として集めるときである。選択公理はどの形でも用いない。

ここでは三種類の対象を区別する必要がある。論理式は、構成可能な台の要素を定数とする一階言語に属する。充足関係は、その論理式を `L` 上の構造で解釈する。そして `pr` は、基礎集合の順序対を周囲の階層で表すクラトフスキー符号である。後で定義の論理式を読むときは値が先、入力が後であるが、集められた関数グラフの項目は `pr(入力,値)` となる。

証明は三つの数学的な形を順に通る。再帰は、定義域、値を定める論理式、そして定義域の各点で充足する値のファイバーが可縮であることの証明からなる。そのグラフ構成は置換によって順序対を集め、一価性と正確な定義域を証明する。最後に `injAt` が、残る単射性の条件、すなわち同じ出力をもつ二つの項目の入力が等しいことを表す。

集合 `a` と `b` に対して、`InjCode F a b` はちょうど四つの成分をもつ。グラフ `F` が一価であること、その定義域が正確に `a` であること、単射的であること、そしてそこに現れるすべての値が `b` に属することである。四条件にはいずれも対応する対象言語の論理式があり、値域条件には先に構成した `valuesInAt` を用いる。`InjL a b` は、そのような `F` と符号の存在を命題的切り詰めに入れる。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
open hPropView 𝒮ʟ using ( S )
open hPropView 𝒮ᵥ using ( _∈ˢ_ )
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _⊨ᵐ_ )
open AbsL using () renaming ( _⊨ᵐ_ to _⊨_ )
```

## 単射符号を一つの論理式として読む

`InjCode` の四条件は、グラフ、定義域、終域という三つの指定位置をもつ一つの対象論理式で表せる。最初の三つの連言は、一価性、正確な定義域、単射性の論理式を再利用する。最後の連言は入力と出力を量化し、グラフが両者を関係づけるなら出力が終域の位置に属すと述べる。したがってホスト層の値域フィールドを不可視と仮定するのではなく、このインターフェースで検査済みの論理式に結び付ける。

```agda
injCodeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
injCodeAt f A B = svAt f ∧̇ domAt f A ∧̇ injAt f
                  ∧̇ valuesInAt f B
```

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

```agda
module InjCodeAt {n : ℕ} (f A B : Fin n) (γ : Vec S n) where
```

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

```agda
  private
    F D C : S
    F = lookup f γ
    D = lookup A γ
    C = lookup B γ

  read : ⟨ γ ⊨ injCodeAt f A B ⟩ → InjCode F D C
  read (sv , dm , ij , ran) =
      svAt-in zero (F ∷ D ∷ []) (λ x y y' p q → svAt-out f γ sv x y y' p q)
    , domAt-intro zero (suc zero) (F ∷ D ∷ []) (λ x →
          (λ h → rec₁ ((x .fst ∈ D .fst) .snd)
                   (λ { (y , p) → domAt-out f A γ dm x y p }) h)
        , (λ hx → domAt-in f A γ dm x hx))
    , injAt-in zero (F ∷ D ∷ []) (λ y x x' p q → injAt-out f γ ij y x x' p q)
    , valuesInAt-out f B γ ran

  fill : InjCode F D C → ⟨ γ ⊨ injCodeAt f A B ⟩
  fill (sv , dm , ij , ran) =
      svAt-in f γ (λ x y y' p q → svAt-out zero (F ∷ D ∷ []) sv x y y' p q)
    , domAt-intro f A γ (λ x →
          (λ h → rec₁ ((x .fst ∈ D .fst) .snd)
                   (λ { (y , p) → domAt-out zero (suc zero) (F ∷ D ∷ []) dm x y p }) h)
        , (λ hx → domAt-in zero (suc zero) (F ∷ D ∷ []) dm x hx))
    , injAt-in f γ (λ y x x' p q → injAt-out zero (F ∷ D ∷ []) ij y x x' p q)
    , valuesInAt-in f B γ ran
```

</div>
</details>

グラフの位置を存在量化すると `InjL` の論理式が得られ、残る二つの位置が定義域と終域を名指す。その意味論的な存在は初めから命題的に切り詰められており、`InjL` とちょうど一致する。先の `read` と `fill` をその切り詰めの内側で写せば、グラフを選ばずに両方向が得られる。

```agda
injLAt : ∀ {n} → Fin n → Fin n → Formula S n
injLAt A B = ∃̇ (injCodeAt zero (suc A) (suc B))
```

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

```agda
module InjLAt {n : ℕ} (A B : Fin n) (γ : Vec S n) where
```

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

```agda
  private
    D C : S
    D = lookup A γ
    C = lookup B γ

  read : ⟨ γ ⊨ injLAt A B ⟩ → InjL D C
  read = map₁ (λ { (F , code) → F , InjCodeAt.read zero (suc A) (suc B) (F ∷ γ) code })

  fill : InjL D C → ⟨ γ ⊨ injLAt A B ⟩
  fill = map₁ (λ { (F , code) → F , InjCodeAt.fill zero (suc A) (suc B) (F ∷ γ) code })
```

</div>
</details>

内部の基数性とは、候補のどの要素にも候補からの単射が存在しないという主張である。次の論理式はそれをそのまま述べる。より小さいかもしれない要素を束縛した後、その候補への所属から `injLAt` 論理式の否定を導く。読み取りで変換する必要があるのは単射の論理式だけであり、外側の全称量化、含意、否定は `IsCardinalL` がすでに使う関数型へ計算される。

```agda
cardinalAt : ∀ {n} → Fin n → Formula S n
cardinalAt K = ∀̇ ((var zero ∈̇ var (suc K))
                  ⇒̇ ¬̇ injLAt (suc K) zero)
```

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

```agda
module CardinalAt {n : ℕ} (K : Fin n) (γ : Vec S n) where
```

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

```agda
  private
    κ : S
    κ = lookup K γ

  read : ⟨ γ ⊨ cardinalAt K ⟩ → IsCardinalL κ
  read h δ δ∈κ inj = lower
    (h δ δ∈κ (InjLAt.fill (suc K) zero (δ ∷ γ) inj))

  fill : IsCardinalL κ → ⟨ γ ⊨ cardinalAt K ⟩
  fill c δ δ∈κ sat = lift
    (c δ δ∈κ (InjLAt.read (suc K) zero (δ ∷ γ) sat))
```

</div>
</details>

二つの型理論上の事実がこの証明を支える。依存対の第二成分が命題値なら、`Σ≡Prop` は第一成分の間のパスを対全体の間のパスへ持ち上げる。命題的切り詰めは、要素が存在するという事実だけを残す。グラフを読み戻す補題 `pair-out` は、行き先のファイバーが命題なので、命題的切り詰めに入った由来の証人をそこへ消去できる。最後の段階では `∣_∣₁` を用いて、具体的なグラフと符号を隠する。どちらの操作も、証人の族を大域的に選ばない。

台 `S` は `L` 上の構造から来る。要素 `x : S` は、周囲の集合 `x .fst` と、それが構成可能であることを示す命題値の証明からなる。所属の記法は周囲の階層から取るため、レコード内の式は `x .fst ∈ˢ dom .fst` のように基礎集合を明示的に比較する。構成が `L` の要素を返す必要があるときには、構成可能性の証明が第二成分として残っている。

記法 `_⊨_` は、周囲の階層を構成可能集合に制限して得られる構造での充足関係を表す。したがって `(y ∷ x ∷ []) ⊨ graph` は、`L` の要素を `graph` の二つの自由な位置に入れて解釈する。`AbsL` という名前は、任意の論理式が `L` と周囲の階層との間で絶対的だと主張するものではない。本章で使うのは制限された構造の意味論と、すでに証明された置換定理である。

## 関数が定義可能であるとは何か

`DefinableMap` はまず `L` の二つの要素 `dom` と `cod` を指定し、それらが順序数や基数であるとは仮定しない。ホスト側の値を定める規則 `fn` は、`x : S` と `x` が `dom` に属する証拠 `m` の組に対してだけ定義される。定義域の外で値を与える必要はない。この型では `fn x m` が `m` に言及してもかまわない。所属は命題なので、そのような二つの証明は等しく、合同性によって対応する値も等しくなる。フィールド `into` は、選ばれた各値が `cod` に属することを証明する。

```agda
record DefinableMap : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    dom cod : S
    fn      : (x : S) → ⟨ x .fst ∈ˢ dom .fst ⟩ → S
    into    : (x : S) (m : ⟨ x .fst ∈ˢ dom .fst ⟩) → ⟨ (fn x m) .fst ∈ˢ cod .fst ⟩
```

残るフィールドは、ホスト側の値を対象言語の論理式に結びつける。`graph` は二つの自由な位置をもち、`S` の要素を定数として含むことができ、Δ₀ 論理式である必要はない。各 `x ∈ dom` に対して、`defines` は選ばれた値を先、`x` を後に置いた環境で論理式が成り立つことを証明し、`only` は論理式を満たす任意の `y` がその選ばれた値と `S` の中で等しいことを証明する。これらの条件は `dom` の外の入力を制約せず、`only` は候補 `y` が `cod` に属するとも仮定しない。選ばれた値が終域に入ることは、別のフィールド `into` が与える。

```agda
    graph   : Formula S 2
    defines : (x : S) (m : ⟨ x .fst ∈ˢ dom .fst ⟩)
            → ⟨ (fn x m ∷ x ∷ []) ⊨ graph ⟩
    only    : (x : S) (m : ⟨ x .fst ∈ˢ dom .fst ⟩) (y : S)
            → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x m
```

## グラフの項目を順序対として符号化する

関数グラフは集合として表すため、各入出力項目をまず順序対として表す。定義論理式は第一の意味論的な位置で値を、第二の位置で入力を読むが、集合による符号化は対応する項目を `pr(入力,値)` として格納する。グラフを構成し、後でその内容を読み戻すには、この二つの順序を区別し続ける必要がある。

## L の内部でグラフを構成する

最初の構成が仮定するのは、定義可能性と関数性だけである。`M` から `L` の要素である完全な関数グラフを作り、その順序対の項目を正確に入れ、読み取る方法を得る。単射性は次の段階まで保留する。同じグラフ構成は、最小証人の表のように、目的上単射である必要のない定義可能な写像にも適用できるからである。

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

```agda
module Graph (M : DefinableMap) where
```

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

```agda
  open DefinableMap M public
```

再帰に必要な仮定を満たすため、`dom` と `graph` をそのまま用い、定義域の各点で充足する値のファイバーに中心があることを証明する。その中心は `(fn x m, defines x m)`、すなわち与えられた値とその充足の証明である。所属の証拠 `m` はそのまま `fn` に渡されるので、この構成は値を定める規則を `dom` の外へ拡張しない。この段階では `into` も単射性も必要ない。

```agda
  private
    R : Recursion
    R = record
      { dom = dom ; graph = graph
      ; funct = λ x m → (fn x m , defines x m)
```

残る仕事は、各候補 `(y,h)` をその中心へ収縮することである。フィールド `only` は `y ≡ fn x m` を与えるが、可縮性には中心から候補へのパスが必要なので `sym` を用いる。第二成分は充足の証明であり、したがって命題である。そこで `Σ≡Prop` が、向きを反転した値の等しさを依存対全体の等しさへ持ち上げる。これにより、必要な一意存在が構成的に証明される。

```agda
          , λ { (y , h) → Σ≡Prop (λ w → ((w ∷ x ∷ []) ⊨ graph) .snd) (sym (only x m y h)) } }
```

ここで置換により、順序対としての値を構成可能集合 `F` に集める。補助的な対の論理式が二つの順序を調整する。もとの関係は `(値,入力)` として解釈されるが、`F` の要素は `pr(入力,値)` である。`F-in` は指定された各項目を入れ、`F-out` は命題的切り詰めのもとで、すべての要素がそのような項目に由来することを述べる。`x` と `y` を固定すると、`pair-out` は `pr(x,y)` が `F` に属することから、定義域の証明と等式 `y = fn(x)` を得る。この除去が正当なのは、`Fib x y` が命題だからである。ここでは所属の証明無関係性と、`V` における等しさが命題値であることを用いる。これらの読み取りから、`sv` が表す一価性と、`dm` が表す定義域が正確に `dom` であることが従う。`F` の形成には置換定理が使われるため、与えられた排中律に依存する。その後の読み取りに選択は入らない。

```agda
  open RecursionGraph R public
    using ( Mem; isPropMem; F; F-in; F-out; Fib; isPropFib; pair-out; γ; sv; dm )
```

最終的な符号の第四条件は、値が終域に入ることである。実際のグラフ項目 `pr(x,fst .fst y) ∈ F .fst` が与えられると、`pair-out` は `m : x ∈ dom` と `e : y .fst ≡ (fn x m) .fst` を返す。フィールド `into x m` は `(fn x m) .fst` が `cod .fst` に属することを証明する。したがって所属は `sym e` に沿って、選ばれた値から `y` へ輸送し、`y ∈ cod` を得る。これは像が終域に含まれることだけを示し、終域の各要素が現れるとは主張しない。

```agda
  ran : (x y : S) → ⟨ pr (x .fst) (y .fst) ∈ F .fst ⟩ → ⟨ y .fst ∈ cod .fst ⟩
  ran x y h = subst (λ w → ⟨ w ∈ cod .fst ⟩) (sym e) (into x m)
    where
    m = (pair-out x y h) .fst
    e = (pair-out x y h) .snd
```

</div>
</details>

## 外部の単射性から符号化された単射へ

このグラフを単射の符号にするには、実質的に新しい仮定として単射性を加える必要がある。`dom` への所属の証明を伴う二つの入力について、選ばれた値の基礎集合が等しければ、入力の基礎集合も等しいと仮定する。`fn` の型は所属の証明に依存しているので、その引数は明示されたままである。証明無関係性は異なる所属の証明の間の整合性を保証するが、仮定自体は二つの入力で実際に与えられた証拠について述べられる。その結論は `injAt` の等号の条項が要求する強さと正確に一致する。

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

```agda
module Inj (M : DefinableMap)
           (inj : (x : S) (m : ⟨ x .fst ∈ˢ (DefinableMap.dom M) .fst ⟩)
                  (x' : S) (m' : ⟨ x' .fst ∈ˢ (DefinableMap.dom M) .fst ⟩)
                → (DefinableMap.fn M x m) .fst ≡ (DefinableMap.fn M x' m') .fst
                → x .fst ≡ x' .fst) where
```

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

`Graph M` を開くことで、すでに構成した `F` と証明済みの性質を単射の場合にも使えるようにする。これにより、数学的に有用な二種類の結論が同時に得られる。後の構成でグラフを名指したり組み合わせたりする必要があるなら、具体的な `F` とその符号を保てる。一方 `injL` を使えば、符号化された単射が何か存在することだけを残せる。この違いは、具体的なデータとその命題的な存在との違いである。

```agda
  open Graph M public
```

論理式 `injAt zero` は出力 `y` を固定し、二つの入力 `x` と `x'` を比較する。`pr(x,y)` と `pr(x',y)` がともに `F` に属するなら、入力が等しいと述べる。最初の項目に `pair-out` を適用すると `e : y = fn(x)` が得られ、二番目からは `e' : y = fn(x')` が得られる。同時に、必要な二つの定義域の証明も得られる。したがって `sym e ∙ e'` はパス `fn(x) = fn(x')` であり、ホスト側の仮定 `inj` がこれを `x = x'` に変え、`injAt-in` がその性質を充足判断 `ij` に移す。この議論が使うのは単射性であって、`only` だけではない。`only` は一つの固定された入力で出力を比較し、一価性を支えるものである。

```agda
  ij : ⟨ γ ⊨ injAt zero ⟩
  ij = injAt-in zero γ (λ y x x' p q →
    let (m , e)   = pair-out x y p
        (m' , e') = pair-out x' y q
    in inj x m x' m' (sym e ∙ e'))
```

四つ組 `sv , dm , ij , ran` は、`InjCode F dom cod` の四つのフィールドを順に満たす。`sv` は一価性を、`dm` はグラフの定義域が正確に `dom` であることを、`ij` は対象言語での単射性を証明し、三つとも環境 `F ∷ dom ∷ []` で述べられる。最後の `ran` は、`F` に現れる値が `cod` に属することをホスト側で述べる。この符号は全射性を主張しないので、`cod` への単射を表し、全単射を表すものではない。

```agda
  code : InjCode F dom cod
  code = sv , dm , ij , ran
```

最後に、具体的な対 `(F,code)` を命題的切り詰めに入れる。得られる項 `injL : InjL dom cod` は、単射の符号をもつ構成可能な関数グラフが存在することを述べ、どのグラフを構成したかは忘れる。基数比較に必要なのはこの命題であり、求める結論が再び命題であるときに消去できる。具体的なデータが必要な構成では、具体化したモジュールの中で `F` と `code` をそれぞれ引き続き使える。したがって `L` に内部化されたのは符号化された関数グラフであり、外部の規則そのものではない。

```agda
  injL : InjL dom cod
  injL = ∣ F , code ∣₁
```

</div>
</details>