---
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.Injection, L.Cardinal]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/L.DefinableInjection.md, https://bedrock.institute/zh/L.DefinableInjection.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 定義可能な単射を内部コードにする

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

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

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

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

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

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

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

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
```

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

```agda
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.Injection {ℓ} lem using ( injAt; injAt-in )
```

集合 `a` と `b` に対して、`InjCode F a b` はちょうど四つの成分をもちます。グラフ `F` が一価であること、その定義域が正確に `a` であること、単射的であること、そしてそこに現れるすべての値が `b` に属することです。最初の三つは対象言語の論理式についての充足判断であり、第四の成分はホスト側で述べる値の範囲の条件です。`InjL a b` は、そのような `F` と符号の存在を命題的切り詰めに入れます。

```agda
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
```

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

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
```

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

```agda
open hPropStructure 𝒮ʟ using ( S )
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
```

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

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

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

`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) → ⟨ fst x ∈ˢ fst dom ⟩ → S
    into    : (x : S) (m : ⟨ fst x ∈ˢ fst dom ⟩) → ⟨ fst (fn x m) ∈ˢ fst cod ⟩
```

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

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

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

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

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

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

```agda
module Graph (M : DefinableMap) where
  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 → snd ((w ∷ x ∷ []) ⊨ graph)) (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(fst x,fst y) ∈ fst F` が与えられると、`pair-out` は `m : x ∈ dom` と `e : fst y ≡ fst(fn x m)` を返します。フィールド `into x m` は `fst(fn x m)` が `fst cod` に属することを証明します。したがって所属は `sym e` に沿って、選ばれた値から `y` へ輸送し、`y ∈ cod` を得ます。これは像が終域に含まれることだけを示し、終域の各要素が現れるとは主張しません。

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

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

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

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

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