正本：FormalLab/TypeTheory/IdentityTypes.lean

第32章：同一性型・輸送・外延性原理#

二つの式が計算によって同じ形になる場合と、同じ対象であるという証拠を項として持つ場合では、何が異なるのでしょうか。さらに、等しい添字に属する二つのファイバーの値を比較するには、一方を他方のファイバーへ移さなければなりません。依存型では等式は結論だけでなく、型を変える入力になります。

本章では同一性型の形成・反射・除去・計算を通常の規則とLeanの Eq で対照します。経路帰納法から輸送、関数による等式の写像、依存関数による等式の写像を導きます。その上で判断的等しさ、命題的等式、関数外延性、等式反映を区別し、HoTTへ進むときLeanの基礎体系をそのまま同一視できない理由を明示します。

反射性だけから等式証拠を作る#

型 A と二項 x,y:A に対し、同一性型を Id_A(x,y) と書きます。標準的な導入規則は反射性です。

\frac{\Gamma\vdash A\;\mathsf{type}\qquad \Gamma\vdash x:A\qquad\Gamma\vdash y:A} {\Gamma\vdash \mathsf{Id}_A(x,y)\;\mathsf{type}} \quad(\mathsf{Id}\text{-form}) \qquad \frac{\Gamma\vdash x:A} {\Gamma\vdash \mathsf{refl}_x:\mathsf{Id}_A(x,x)} \quad(\mathsf{Id}\text{-intro}).

任意の等式証拠 p : Id_A(x,y) を使う基本原理は、反射の場合だけを証明すれば一般の p へ拡張できる 経路帰納法です。Martin-Löf型理論では通常 J と呼ばれる除去子で表します。

Leankernel-checked counterpartL34–48

namespace FormalLab.TypeTheory.IdentityTypes

universe u v

def J {α : Type u} {x : α}
    (motive : (y : α) → x = y → Sort v)
    (reflexiveCase : motive x rfl)
    {y : α} (path : x = y) : motive y path := by
  cases path
  exact reflexiveCase

theorem J_refl {α : Type u} {x : α}
    (motive : (y : α) → x = y → Sort v)
    (reflexiveCase : motive x rfl) :
    J motive reflexiveCase rfl = reflexiveCase := rfl

J_refl は証明を別に探して得た等式ではなく、path が rfl のとき J の定義が直接 reflexiveCase へ計算される規則です。一般理論ではこの種の計算一致を判断的等しさで表し、同一性型の項として与える等式と分けます。Leanコードでは rfl で検査できる定義的計算として現れます。

等しい添字の間で値を輸送する#

型族 P : A → Type、等式 p : x = y、値 u : P x があるとき、u を P y へ移す操作を transport P p u と書きます。経路が反射なら始域と終域は同じファイバーなので値をそのまま返します。

Leankernel-checked counterpartL61–72

def transport {α : Type u} (P : α → Type v) {x y : α}
    (path : x = y) (value : P x) : P y := by
  cases path
  exact value

theorem transport_refl {α : Type u} (P : α → Type v) {x : α} (value : P x) :
    transport P rfl value = value := rfl

def cast {α β : Type u} (path : α = β) : α → β :=
  transport (fun type => type) path

example (n : Nat) : cast (show Nat = Nat from rfl) n = n := rfl

通常の関数型では等しい値を引数へ代入しても終域は変わりません。依存型では添字の置換により結果型自体が P x から P y へ変わるため、輸送が式の一部になります。ベクトルの長さ等式を使って値を移す場面で現れるcastは、実装上の偶然ではなく同一性型の除去原理の帰結です。

関数は等式を、依存関数は輸送された等式を保存する#

通常の関数 f : A → B は x = y を f x = f y へ送ります。依存関数 f : (x:A) → P x の二つの値は異なるファイバーに属するため、左辺を輸送してから比較します。

\begin{aligned} \mathsf{ap}_f &: (x=_A y)\to(f(x)=_B f(y)),\\ \mathsf{apd}_f(p) &: \mathsf{transport}^{P}(p,f(x))=_{P(y)}f(y). \end{aligned}

Leankernel-checked counterpartL92–104

theorem ap {α : Type u} {β : Type v} (f : α → β) {x y : α} : x = y → f x = f y
  | rfl => rfl

theorem apd {α : Type u} {P : α → Type v} (f : (x : α) → P x) {x y : α}
    (path : x = y) : transport P path (f x) = f y := by
  cases path
  rfl

theorem inverse {α : Type u} {x y : α} : x = y → y = x
  | rfl => rfl

theorem concatenate {α : Type u} {x y z : α} : x = y → y = z → x = z
  | rfl, rfl => rfl

連結した経路に沿う輸送は、二回の輸送と命題的に一致します。

Leankernel-checked counterpartL107–118

theorem transport_concatenate {α : Type u} (P : α → Type v)
    {x y z : α} (first : x = y) (second : y = z) (value : P x) :
    transport P second (transport P first value) =
      transport P (concatenate first second) value := by
  cases first
  cases second
  rfl

theorem ap_identity {α : Type u} {x y : α} (path : x = y) :
    ap (fun value => value) path = path := by
  cases path
  rfl

反転と連結により等式証拠は向きと合成を持ちます。高次同一性を保つ型理論では、これらを点を対象、経路を射とする高次群oid構造の入口として読みます。ただし本章のLean証明が、HoTTの全高次構造や一価性をすでに実装したことにはなりません。

判断的等しさと命題的等式を区別する#

判断的等しさ t ≡ u は型検査で用いる計算上の一致で、通常は対象言語の項として量化しません。命題的等式 p : t = u は型を持つ証拠で、関数へ渡し、反転し、連結できます。

((fun x => x) a) ≡ a はβ計算による判断的等しさである。
n + 0 = n は n が変数なら帰納法を要する命題的等式である。
p : x = y を得ても、型検査器が全ての文脈で x と y を定義的に同一視する等式反映は従わない。

等式証拠を場合分けすればその分岐内で添字が精密化されます。これは証拠を除去した結果であり、任意の命題的等式を判断的等しさへ変える一般規則ではありません。

関数外延性は点ごとの等式から関数等式へ進む#

任意の x で f x = g x なら f = g とする関数外延性は、関数の観察方法に即した原理です。 Leanでは funext により利用できますが、単なるβ計算ではありません。逆向きは関数へ等式を適用する ap から構成できます。

\frac{\Gamma,x:A\vdash p_x:f(x)=_B g(x)} {\Gamma\vdash \mathsf{funext}(p):f=_{A\to B}g}.

Leankernel-checked counterpartL149–156

theorem pointwiseOfFunctionEquality {α : Type u} {β : Type v}
    {f g : α → β} (equal : f = g) : ∀ x, f x = g x := by
  intro x
  exact ap (fun function => function x) equal

theorem functionEqualityOfPointwise {α : Type u} {β : Type v}
    {f g : α → β} (pointwise : ∀ x, f x = g x) : f = g :=
  funext pointwise

外延性原理は何を同じ対象とみなすかを強めます。命題外延性、一価性、等式反映はそれぞれ別の原理であり、関数外延性という名称から一括して導きません。Leanの Eq : α → α → Prop は証明無関連性の対象です。 HoTTで同一性型の高次情報を計算対象として保つ基礎とは振舞いが異なります。後の章では、対象理論を Lean内に別に記述する範囲とLean自身の等式を利用する範囲を明示します。

要点#

同一性型は反射で導入し、経路帰納法 J で任意の等式証拠を除去する。
輸送は等しい添字のファイバー間で値を移し、依存型における置換を表す。
ap は関数による等式の像、apd は輸送を伴う依存関数による像である。
判断的等しさは計算上の一致、命題的等式は操作できる証拠であり、等式反映は別原理である。
関数外延性、命題外延性、一価性、証明無関連性をそれぞれ区別する。

研究史と文献案内#

Martin-Löf型理論 [ML84] は同一性型を形成・導入・除去・計算規則から読む基準文献です。版と時期により型理論の規則が異なるため、後世の J という名称やHoTTの経路解釈を1984年講義録へ無差別に帰属させません。依存型と判断体系の現代的展開は [PFPL16]、Leanの Eq と除去規則の現行仕様は [LEAN-REF] を参照してください。高次群oid解釈と一価性は後のHoTT章で別の文献史として扱います。

問題#

`J` から対称性と推移性を再構成する#

inverse と concatenate を直接のパターンマッチを使わず、J だけから定義してください。motiveの各引数がどの端点と経路に依存するかを通常の型理論記法で書きます。反射の場合の計算結果を rfl で検査し、導入規則一つから群oid的操作二つが導かれる依存を説明できれば完了です。

ベクトルの長さ等式に沿って輸送する#

Vector α n と等式 p : n = m から Vector α n → Vector α m を transport で定義してください。 p が反射の場合の計算を確認し、連結した等式に沿う二回の輸送と、連結後の一回の輸送が命題的に等しいことを証明します。どの等式が判断的に成立し、どこで経路帰納法が必要か分類してください。

四つの外延性原理を比較する#

関数外延性、命題外延性、等式反映、一価性について、仮定と結論を型判断で書いてください。Leanで利用できる形、追加原理が必要な形、Leanの Prop による証明無関連性と緊張する形を区別します。一つを仮定しただけで別の原理まで得たとする誤った推論を作り、不足する前提を指摘すれば完了です。