---
title: "符号化された単射"
module: L.Coding.Injection
lang: ja
site: "Bedrock"
description: "符号化された単射"
stage: "順序数，単射，基数"
reading_order: 88
canonical: https://bedrock.institute/ja/L.Coding.Injection.html
html: L.Coding.Injection.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Injection.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Model, V.Presentation]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/L.Coding.Injection.md, https://bedrock.institute/zh/L.Coding.Injection.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 符号化された単射

後の基数論では、対象言語が量化できるグラフと、集合の小さな要素型の間の実際の単射という二つの表現を往復する。この溝は三層で埋める。まず対象言語には、グラフが単射であることを言う論理式、すでにある一価性の条項の鏡像が必要になる。次に、一価性とちょうどの定義域を仮定すれば、グラフは値が構成可能モデルの要素にとどまる本物の関数として読める。最後にその関数は、指定された定義域と値域の標準的な小さな提示へ移る。本章は単射性の論理式を加え、Cantor-Bernstein と GCH の構成が使う二段階の読み戻しを実行する。

この構成自体は構成的です。周囲の議論は `LEM (ℓ-suc ℓ)` を仮定していますが、以下の証明はそれを使いません。グラフの値の存在は切り詰められていますが、一価性により像のファイバー全体が命題になるため、選択原理なしに切り詰めを消去してその一意な要素を得られます。

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

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

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

`S` を構成可能モデルの台とします。`S` の要素は `V ℓ` の周囲の集合と、その構成可能性の証明からなるため、グラフについての主張は第一射影について述べられます。適用、一価性、正確な定義域を表す論理式は、内部の充足をこれらの射影されたグラフの事実と結び付けます。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _≐_; _⇒̇_; ∀̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
```

第二の読み戻しには標準的な提示の道具が必要です。集合はインデックス型とインデックス付けの写しで提示され、`member` はインデックスを明示的な所属証明に変え、`fiber` は逆に実際のインデックスを返します。切り詰められた存在ではなくです。`Σ≡Prop` は第二成分が命題のとき、依存対の等しさを第一成分の等しさへ帰着させます。像のファイバーも模型の台の対もこの仕方で扱われます。

```agda
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; svAt; svAt-out; domAt; domAt-in )
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.Data.Sigma using ( Σ≡Prop )
```

ここでの真理値は、命題であることの証明を添えた命題であり、充足関係は `hProp` 上の論理結合子を直接使います。充足の判断 `_⊨_` は構成可能な構造 `𝒮ʟ` に対して述べられるので、`γ ⊨ svAt zero` のような判断は、妥当性の同一視を通して射影された集合についての主張になります。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )

open hPropStructure 𝒮ʟ using ( S )
```

有界絶対性は、構成可能モデルでの充足を、割り当てを `fst` で射影した後の充足と結び付けます。この橋は妥当性定理を適用する箇所で用いられますが、それだけで `Extract.toFun` が単射になるわけではありません。単射性は後で独立な仮定 `ij` として加わります。

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

## 対象言語における単射性

妥当性の観点では、## 対象言語における単射性

一価的なグラフは引数を固定して値を比較します。同じ第一成分を持つ二つの項目の第二成分は一致する、というものです。単射性はその鏡像で、値を固定して引数を比較します。具体的には、`(x, y)` と `(x', y)` がともにグラフに属するなら、`x` と `x'` の第一成分は等しくなければなりません。これを対象言語の論理式として述べることで、基数論はモデルの内部で単射なグラフを量化できるようになります。

論理式は割り当て `x′ ∷ x ∷ y ∷ γ` を束縛します。スロット 0 は `x′`、1 は `x`、2 は `y` で、もとのグラフのスロット `f` は `f + 3` になります。二つの前提は `(x,y)` と `(x′,y)` がそのグラフに属すことを述べ、結論は `x` と `x′` を等置します。したがって出力を固定して入力を比較し、一価性とちょうど対をなします。

```agda
injAt : ∀ {n} → Fin n → Formula S n
injAt f = ∀̇ (∀̇ (∀̇ (
      appAt (suc (suc (suc f))) (suc zero) (suc (suc zero))
  ⇒̇ (appAt (suc (suc (suc f))) zero (suc (suc zero))
  ⇒̇ (var (suc zero) ≐ var zero)))))
```

読み戻しでは変数の添字 `f` と模型要素からなる割り当て `γ` を固定します。`Holds₀ x y` は射影された事実で、`x` と `y` の底の集合の順序対が底のグラフ、すなわち変数 `f` が `γ` から選ぶ項目に属すということです。以下の両方向は、適用の条項の充足の判断をこの `Holds₀` と比べるもので、妥当性のパスが議論の要になります。

```agda
module _ {n : ℕ} (f : Fin n) (γ : S ^ n) where
  private
    Holds₀ : S → S → Type (ℓ-suc ℓ)
    Holds₀ x y = ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩

    at₁ : (y x x' : S)
```

パス `at₁` は、拡張された割り当て `x' ∷ x ∷ y ∷ γ` での最初の適用条項の妥当性を記録します。そこでの充足は、対 `(x, y)` のグラフへの所属という射影された事実と同一視されます。この同一視は命題どうしの等しさであり、所定の変数の添字での `appAt-adequate` によって与えられるので、どちらの方向へも輸送できます。

```agda
        → ((x' ∷ x ∷ y ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc zero) (suc (suc zero)))
        ≡ (pr (fst x) (fst y) ∈ fst (lookup f γ))
    at₁ y x x' = appAt-adequate (suc (suc (suc f))) (suc zero) (suc (suc zero))
                   (x' ∷ x ∷ y ∷ γ)

    at₂ : (y x x' : S)
```

パス `at₂` はもう一つの条項についての同じ主張です。変数 `0` と `2` での適用の充足は、対 `(x', y)` のグラフへの所属という射影された事実と等しくなります。二つのパスの違いは、対の符号にどちらの第一成分を入れるかだけで、これこそ単射性が利用する非対称です。

```agda
        → ((x' ∷ x ∷ y ∷ γ) ⊨ appAt (suc (suc (suc f))) zero (suc (suc zero)))
        ≡ (pr (fst x') (fst y) ∈ fst (lookup f γ))
    at₂ y x x' = appAt-adequate (suc (suc (suc f))) zero (suc (suc zero))
                   (x' ∷ x ∷ y ∷ γ)

  injAt-out : ⟨ γ ⊨ injAt f ⟩
```

外向きの `injAt-out` は、論理式が `γ` で成り立つ証明と二つの所属の事実 `Holds₀ x y`、`Holds₀ x' y` から出発します。三つの量化子を具体化すると、拡張された割り当てでの含意の本体の充足証明が得られ、所属の事実を `at₁` と `at₂` の逆向きに輸送して、二つの前件の条項の充足証明に変えます。最後の `fst x ≡ fst x'` はモデルの等しさの中で読み取ります。

```agda
            → (y x x' : S) → Holds₀ x y → Holds₀ x' y → fst x ≡ fst x'
  injAt-out h y x x' p q = h y x x'
    (subst ⟨_⟩ (sym (at₁ y x x')) p) (subst ⟨_⟩ (sym (at₂ y x x')) q)

  injAt-in : ((y x x' : S) → Holds₀ x y → Holds₀ x' y → fst x ≡ fst x')
           → ⟨ γ ⊨ injAt f ⟩
```

内向きの `injAt-in` は同じ輸送を順方向に行います。`Holds₀` についての射影された単射性を仮定として与えると、二つの所属の事実を `at₁` と `at₂` そのものに沿って輸送して二つの前件の充足を得、仮定が論理式の結論の求める等しさを出します。二つの方向を合わせて、この論理式が単射性に対して過不足なく妥当であることが分かります。

```agda
  injAt-in h y x x' p q = h y x x'
    (subst ⟨_⟩ (at₁ y x x') p) (subst ⟨_⟩ (at₂ y x x') q)
```

## モデルに値を取る単射を取り出す

グラフが一価でちょうどの定義域を持つと仮定すると、定義域の各要素はグラフの中に何らかの像を持ちますが、それはもっぱら存在するだけの像です。定義域への所属が与えるのは命題の切り詰めであって、選ばれた証人ではありません。一価性がこの状況を変えます。入力を固定すると、「出力と、その対がグラフに属する証明」の組の型が命題であることが示され、切り詰められた値はいつでも命題へ消去できます。したがってグラフはモデルに値を取る本物の関数を与え、単射性まで仮定すれば本物の単射になります。この第一の読み戻しは値を台の要素のまま保つ形で、後の証明がコード化されたグラフを参照し続けるときに使われます。

この節は、グラフ `F` と定義域 `D` を模型の要素として、二つの充足の仮定とともに取ります。変数ゼロでのグラフの一価性と、`D` のすべての要素が `F` の下で値を持つと言うちょうどの定義域の条項です。環境 `γ` はそれらを、充足の判断が期待する固定の順序でまとめます。

```agda
module Extract (F D : S)
               (sv : ⟨ (F ∷ D ∷ []) ⊨ svAt zero ⟩)
               (dm : ⟨ (F ∷ D ∷ []) ⊨ domAt zero (suc zero) ⟩) where

  γ : S ^ 2
  γ = F ∷ D ∷ []
```

`Holds x y` は、底の対が底のグラフに属すという射影された所属です。ファイバー `Fib x` は出力 `y` にこの証明を添えた組で、その要素はグラフが `x` で取る候補の値であり、それぞれが本当に値であることの証明書を伴います。

```agda
  Holds : S → S → Type (ℓ-suc ℓ)
  Holds x y = ⟨ pr (fst x) (fst y) ∈ fst F ⟩

  Fib : S → Type (ℓ-suc ℓ)
  Fib x = Σ[ y ∈ S ] Holds x y

  isPropFib : (x : S) → isProp (Fib x)
```

`Fib x` が命題であることを示すには、`(y,p)` と `(y′,q)` を比較します。一価性からまずパス `fst y ≡ fst y′` が得られます。内側の `Σ≡Prop` は、`S` の要素の第二成分である `isL` の証明が命題であることを使い、このパスを `y ≡ y′` へ持ち上げます。外側の `Σ≡Prop` は、グラフ所属の証明が命題であることを使い、その等しさを `Fib x` の二要素の等しさへ持ち上げます。これは別々の二つの証明無関係性の段階であり、周囲の集合の等しさが構成可能性だけから従うという意味ではありません。

```agda
  isPropFib x (y , p) (y' , q) =
    Σ≡Prop (λ w → snd (pr (fst x) (fst w) ∈ fst F))
      (Σ≡Prop (λ z → snd (isL z)) (svAt-out zero γ sv x y y' p q))

  toVal : (x : S) → ∥ Fib x ∥₁ → Fib x
  toVal x = PT.rec (isPropFib x) (λ z → z)
```

`Fib x` が命題なので、`toVal` は値の切り詰められた存在 `∥ Fib x ∥₁` を実際のファイバーへ消去できます。選択がここに隠れていそうで、そうではありません。命題の切り詰めは命題値の任意の対象へ消去できるので、排中律も代表的な元の選出も要りません。定義域 `Dom` は入力に `D` への所属の射影された証明を添えてまとめ、`fib` は `domAt-in` から得た各入力の切り詰められた像を `toVal` に通します。

```agda
  Dom : Type (ℓ-suc ℓ)
  Dom = Σ[ x ∈ S ] ⟨ fst x ∈ fst D ⟩

  fib : (u : Dom) → Fib (fst u)
  fib (x , m) = toVal x (domAt-in zero (suc zero) γ dm x m)

  toFun : Dom → S
```

関数 `toFun` は定義域の要素を、その一意なファイバーに含まれる出力 `y : S` へ送ります。捨てるのは付随するグラフ所属の証明だけで、出力はモデルの要素のままなので構成可能性の証明書を保持します。定理 `toFun-graph` は、捨てた所属の証拠をファイバーの第二成分として取り出します。

```agda
  toFun u = fst (fib u)

  toFun-graph : (u : Dom) → Holds (fst u) (toFun u)
  toFun-graph u = snd (fib u)

  module _ (ij : ⟨ γ ⊨ injAt zero ⟩) where

    toFun-inj : (u v : Dom) → fst (toFun u) ≡ fst (toFun v)
```

グラフの単射性まで仮定すると、`toFun-inj` は値の等しさを引数の等しさに変えます。`toFun u` と `toFun v` の底の集合が等しければ、`u` のグラフの等式をそのパスに沿って輸送して、両方の項目が同じ値、すなわち `toFun v` について語るようにし、`injAt-out` が二つの引数を比較して `fst u` と `fst v` の第一成分の等しさを返します。結果は射影された第一成分について述べられ、後続の基数論が `Dom` の要素を比較するときの形です。

```agda
              → fst (fst u) ≡ fst (fst v)
    toFun-inj u v e = injAt-out zero γ ij (toFun v) (fst u) (fst v)
      (subst (λ w → ⟨ pr (fst (fst u)) w ∈ fst F ⟩) e (toFun-graph u))
      (toFun-graph v)
```

## 小さな台に制限する

関数 `toFun` は「模型の要素と所属の証明」の対に作用しますが、この台は基数の議論で数えることができません。最後の段階では両端を標準的な小さな提示に置き換えます。定義域は `D` のインデックス型に、値域は呼び出し側が指定する集合 `C` のインデックス型になり、呼び出し側はグラフのどの値も `C` に属すことを証明するだけで済みます。グラフの三つの条項、一価性、ちょうどの定義域、単射性は、ここでまとめて仮定します。提示の層がもたらすのは明示性です。標準的な埋め込みのファイバーが命題値であるため、`D` や `C` への所属はインデックスから読み出せ、インデックスへ読み戻せます。

パラメータは、ここで働く三つの構成可能集合、グラフ `F`、定義域 `D`、値域 `C` を名指します。最初の三つの仮定は、Extract と toFun-inj が使った充足の主張そのものです。最後の `ran` が新しいもので、入力 `x` と、対 `(x, y)` がグラフに属すような値 `y` に対して、`y` の底の集合が `C` の底の集合に属すことを証明書として与えます。これは値域の制限を呼び出し側の仮定として述べたもので、この節自身はグラフが特定の値域を持って作られたと仮定しません。

```agda
module Small (F D C : S)
             (sv : ⟨ (F ∷ D ∷ []) ⊨ svAt zero ⟩)
             (dm : ⟨ (F ∷ D ∷ []) ⊨ domAt zero (suc zero) ⟩)
             (ij : ⟨ (F ∷ D ∷ []) ⊨ injAt zero ⟩)
             (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩
```

内側のモジュールは、`F` と `D` と先の二つの充足の証明で Extract を改めて開くので、前節の構成はすべて接頭辞付きの名前で使えます。そして `toS` は `D` の標準的な提示のインデックス `m` を模型の要素に変えます。第一成分は提示された集合そのものであり、第二成分はその構成可能性の証明書で、`isL-trans` により、明示的な所属 `member (fst D) m` と `D` 自身が構成可能である証明書から得られます。推移性はまさに必要な原理です。構成可能集合の要素は構成可能です。

```agda
                  → ⟨ fst y ∈ fst C ⟩) where

  module E = Extract F D sv dm

  toS : ⟪ fst D ⟫ → S
  toS m = ⟪ fst D ⟫↪ m
        , isL-trans {x = fst D} {y = ⟪ fst D ⟫↪ m} (member (fst D) m) (snd D)
```

各小さなインデックスは、Extract の意味でも定義域の要素と見なされねばならず、`at` がその組を与えます。模型の要素 `toS m` と明示的な所属の証明 `member (fst D) m` です。`at m` を `E.toFun` でグラフに通すと値が得られ、値域の仮定がこの値が `C` に属すことを証明します。標準的な提示での所属 `⟪ fst C ⟫↪ k ≡ fst (E.toFun (at m))` は、命題値のファイバーを持つ埋め込みのファイバーなので、`fiber` は切り詰められた存在ではなく、実際のインデックス `k` とパスの組を返します。

```agda
  at : ⟪ fst D ⟫ → E.Dom
  at m = toS m , member (fst D) m

  fib : (m : ⟪ fst D ⟫)
      → Σ[ k ∈ ⟪ fst C ⟫ ] (⟪ fst C ⟫↪ k ≡ fst (E.toFun (at m)))
  fib m = fiber (fst C)
```

パスを捨てると `small` が得られます。`D` のインデックス型から `C` のインデックス型への関数で、各定義域のインデックスは、グラフの下での像に対応するインデックスへ送られます。ここで二つの表現が合流します。`small` は固定された宇宙レベルの型の間の写しであり、数え上げの議論が求める形そのものであり、保持されたパスを通してグラフと結び付いています。

```agda
    (ran (toS m) (E.toFun (at m)) (E.toFun-graph (at m)))

  small : ⟪ fst D ⟫ → ⟪ fst C ⟫
  small m = fst (fib m)

  small-inj : (m n : ⟪ fst D ⟫) → small m ≡ small n → m ≡ n
  small-inj m n e = ↪-inj {a = fst D} {m = m} {n = n}
```

`small` の単射性は、インデックスの等しさを提示の中を通して辿ることで証明されます。`small m ≡ small n` から、`snd (fib m)` を逆向きにたどって `m` での提示された値を得、埋め込みの下での合同が等しさを運び、`snd (fib n)` が `n` での提示された値に着きます。三つのパスを正にこの方向でつなぐことで、二つの値の底の集合が等しくなります。続いて Extract の単射性が二つの入力の底の集合の等しさを与え、`↪-inj`、すなわち定義域の提示の埋め込みのインデックス上の単射性が `m ≡ n` を結論します。ここでは二つの異なる単射性の事実が働いており、一つはグラフについて、もう一つは標準的な埋め込みについてで、どちらも他方で代用できません。

```agda
    (E.toFun-inj ij (at m) (at n)
      (sym (snd (fib m)) ∙ cong ⟪ fst C ⟫↪ e ∙ snd (fib n)))
```

## まとめ

`injAt` は符号化グラフの単射性をモデル内部で表します。一価性と正確な定義域から `Extract.toFun` はグラフを `L` に値を取る関数として読み、独立な仮定 `ij` を加えて初めて `Extract.toFun-inj` が得られます。指定された値域条件の下で、`Small.small` はこの単射を定義域と値域の標準的な小さな要素型へ移します。切り詰めの段階では像のファイバーの一意性を、提示の段階では埋め込みのファイバーが命題であることを使います。