依存型理論：Π 型・Σ 型・恒等型・宇宙で数学を型として書く

0. この記事の要点

「すべての自然数 $n$ について $n+0=n$ が成り立つ」という主張を、計算機に検査させられる形で書くには、どうすればよいでしょうか。この記事では、命題も証明も数も、すべてを「型」と「その型の値」として書く体系を学びます。読み終えると、「すべての」「存在する」「等しい」といった論理の言葉が、型の作り方の規則として書けることが分かり、Lean というソフトで書かれた証明を読むための土台ができます。

• 依存型とは、値に依存して決まる型のことです。「各 $n$ に $P(n)$ の証明を返す関数」の型 $\Pi_{(n:\mathbb{N})}P(n)$ は $\forall n\,P(n)$ を、「$a$ と $P(a)$ の証明の組」の型 $\Sigma_{(x:A)}P(x)$ は $\exists x\,P(x)$ を表します。前章のカリー＝ハワード対応（命題を型、証明をその型の値と読む対応）が述語論理（「すべての」「存在する」を含む論理）まで広がります。
• マーティン＝レーフ型理論 (MLTT) は、Π 型・Σ 型・恒等型 $\mathrm{Id}_A(a,b)$・宇宙 $\mathcal{U}$・帰納型（自然数など）を、それぞれ形成・導入・除去・計算の 4 種類の規則で与える体系です。
• 規則だけから、型理論版の選択公理（定理 4.2）、等号の対称性・推移性・輸送（命題 5.2）、自然数の帰納法による $0+n=n$（例 6.2）、そして宇宙を使った $0\ne1$（定理 7.2）を証明します。
• Lean の論理は 構成の計算 (CIC) の一種で、命題の宇宙 Prop と型の宇宙 Type を区別します。Prop の証明は区別されない（証明の無関係性）代わりに、∃ から証人を取り出すことはできず、そこに Classical.choice が要ります（命題 8.2）。
• 関数外延性と「等号の証明の一意性」(UIP) は MLTT から証明も反証もできません（主張として述べます）。Lean はこの二つを、公理と Prop の性質で成り立たせています。

この記事で使う事前知識

• 単純型付きラムダ計算: 関数を $\lambda x.t$ で書き、すべての項に型を付ける体系。→ 単純型付きラムダ計算
• BHK 解釈: 各論理記号について「何を作れば証明したことになるか」で意味を与える解釈。$A\to B$ の証明は、$A$ の証明を $B$ の証明に変える関数。→ BHK 解釈
• β 簡約: $(\lambda x.b)\,a$ を、$b$ の中の $x$ に $a$ を代入したものに書き換える計算。→ β 簡約
• 選択公理: 空でない集合の族から、各集合の元を一斉に選べるという公理。→ 選択公理

1. 動機：「すべての $n$ について」を型で書く

1.1. 単純型の限界

前章の 単純型付きラムダ計算とカリー＝ハワード対応 では、命題 $A\to B$ を関数の型と読みました。$A\to B$ の証明は、$A$ の証明を受け取って $B$ の証明を返す関数です。

では「すべての自然数 $n$ について $n+0=n$」はどうでしょう。BHK 解釈（定義 5.1［単純型付きラムダ計算とカリー＝ハワード対応］）に従えば、その証明は「各 $n$ に $n+0=n$ の証明を対応させる方法」、つまり関数です。けれどもこの関数は、入力 $n=3$ には $3+0=3$ の証明を、入力 $n=5$ には $5+0=5$ の証明を返します。出力の型が入力の値によって変わるのです。単純型の $A\to B$ では、$B$ は $x$ によらない一つの型なので、こういう関数の型を書けません。

これを書けるようにしたのが依存型です。$\Pi_{(n:\mathbb{N})}\,(n+0=n)$ は「$n:\mathbb{N}$ を受け取り、型 $n+0=n$ の値を返す関数」の型です。Lean では ∀ n : Nat, n + 0 = n と書き、実はこれは (n : Nat) → n + 0 = n と同じものです。

1.2. 依存型はプログラミングでも便利

依存型は論理のためだけの道具ではありません。「長さ $n$ のベクトル」の型 $\mathrm{Vec}(A,n)$ は自然数 $n$ に依存する型で、これを使うと「長さの合わないベクトルの内積」はコンパイル時点で型エラーになります。

def Vec (α : Type) : Nat → Type
  | 0     => Unit
  | n + 1 => α × Vec α n

example : Vec Nat 2 := (1, 2, ())

Vec Nat 2 は Nat × (Nat × Unit) に計算され、(1, 2, ()) はその値です。型 Vec α n は値 n で決まり、型の計算に値の計算が入り込んでいます。

1.3. 集合論との違い

公理的集合論 ZFC では、一階述語論理という「論理」の上に、$\in$ についての公理を置いて「数学の対象」を作りました。論理と対象は別の層です。依存型理論では、命題も対象も型であり、証明も元も項です。論理を別に用意せず、型の規則だけで論理と数学の両方を書きます。等号さえも「$a$ と $b$ が等しいことの証明の型」$\mathrm{Id}_A(a,b)$ という型になります。

この一体性が、計算機による証明検査と相性がよいのです。証明の検査は「この項がこの型をもつか」という型検査になり、型検査は（適切に設計すれば）アルゴリズムで決定できます。Lean はこの設計の上に立っています（証明支援系 Lean の仕組み）。

2. 判断と規則の形

型理論の基本単位は判断です。

定義 2.1（判断）↗

文脈 $\Gamma=x_1{:}A_1,\ldots,x_n{:}A_n$（各 $A_i$ は前の変数に依存してよい）のもとで、次の 4 種類の判断を考える。

• $\Gamma\vdash A\ \mathsf{type}$：$A$ は型である。
• $\Gamma\vdash a:A$：$a$ は型 $A$ の項である。
• $\Gamma\vdash A\equiv B$：型 $A$ と $B$ は定義的に等しい。
• $\Gamma\vdash a\equiv b:A$：項 $a$ と $b$ は型 $A$ の項として定義的に等しい。

定義的等しさは、定義の展開と計算（β 簡約など）で互いに移り合うことを表す。$\Gamma\vdash a:A$ かつ $\Gamma\vdash A\equiv B$ なら $\Gamma\vdash a:B$ とする（変換規則）。

なぜ二種類の「等しい」を使い分けるのかを先に述べると、機械が自動で確かめられる等しさ（計算で一致する）と、人が証明して初めて言える等しさを、規則の上で区別するためです。

定義的等しさ $\equiv$ は判断であり、型 $\mathrm{Id}_A(a,b)$（§5）は命題です。前者は計算すれば確かめられる等しさ、後者は証明を要する等しさです。たとえば $n+0\equiv n$ は加法の定義から計算で従いますが、$0+n=n$ は帰納法で証明しなければなりません（例 6.2）。この区別は Lean で rfl が通るかどうかの区別として、日常的に現れます。

各型は次の 4 種類の規則で導入されます。形成（型を作る）、導入（その型の項を作る）、除去（その型の項を使う）、計算（導入した直後に除去したときの値）。前章の導入・除去と β 簡約の組をそのまま一般化したものです。

3. Π 型

定義 3.1（Π 型（依存関数型））↗

$$\frac{\Gamma\vdash A\ \mathsf{type}\quad \Gamma,x{:}A\vdash B(x)\ \mathsf{type}}{\Gamma\vdash\Pi_{(x:A)}B(x)\ \mathsf{type}}\ (\text{形成})\qquad \frac{\Gamma,x{:}A\vdash b(x):B(x)}{\Gamma\vdash\lambda x.b(x):\Pi_{(x:A)}B(x)}\ (\text{導入})$$$$\frac{\Gamma\vdash f:\Pi_{(x:A)}B(x)\quad\Gamma\vdash a:A}{\Gamma\vdash f\,a:B(a)}\ (\text{除去})\qquad (\lambda x.b(x))\,a\equiv b(a)\ (\text{計算}),\qquad f\equiv\lambda x.f\,x\ (\eta)$$

$B$ が $x$ に依存しないとき $\Pi_{(x:A)}B$ を $A\to B$ と書く。

除去規則で、結果の型が $B(a)$、つまり引数の値を代入した型になっていることが単純型との違いです。命題として読むと、$\Pi_{(x:A)}P(x)$ は $\forall x{:}A,\ P(x)$ で、除去規則は「全称命題を個別の $a$ に適用する」推論です。

通常の関数 A → B と依存関数 Π の違い。左は出力の型が常に ℕ、右は入力 n に応じて出力の型 n+0=n が変わる。

4. Σ 型と型理論版の選択公理

定義 4.1（Σ 型（依存対型））↗

形成：$\Gamma\vdash A\ \mathsf{type}$ と $\Gamma,x{:}A\vdash B(x)\ \mathsf{type}$ から $\Gamma\vdash\Sigma_{(x:A)}B(x)\ \mathsf{type}$。

導入：$\Gamma\vdash a:A$ と $\Gamma\vdash b:B(a)$ から $\Gamma\vdash(a,b):\Sigma_{(x:A)}B(x)$。

除去：$\Gamma,z{:}\Sigma_{(x:A)}B(x)\vdash C(z)\ \mathsf{type}$、$\Gamma,x{:}A,y{:}B(x)\vdash c(x,y):C((x,y))$、$\Gamma\vdash p:\Sigma_{(x:A)}B(x)$ から $\Gamma\vdash\mathrm{split}(c,p):C(p)$。

計算：$\mathrm{split}(c,(a,b))\equiv c(a,b)$。

除去規則で、目標の型 $C(z)$ が対 $z$ そのものに依存してよいことが重要です。これにより射影 $\mathrm{pr}_1(p):\equiv\mathrm{split}((x,y)\mapsto x,\,p):A$ だけでなく、$\mathrm{pr}_2(p):\equiv\mathrm{split}((x,y)\mapsto y,\,p):B(\mathrm{pr}_1(p))$ も定義できます（$C(z):\equiv B(\mathrm{pr}_1(z))$ ととると、$C((x,y))\equiv B(x)$ なので $y$ が型に合う）。

命題として読むと、$\Sigma_{(x:A)}P(x)$ の証明は「証人 $a$ と $P(a)$ の証明の組」で、BHK 解釈の $\exists x\,P(x)$ そのものです。$B$ が $x$ に依存しなければ $\Sigma_{(x:A)}B$ は直積 $A\times B$、命題としては $A\wedge B$ です。

次の定理のねらいは、「各 $x$ に対して条件を満たす $y$ がある」という証明から、「$x$ を $y$ に送る一つの関数」を取り出せることを、規則だけで示すことです。証明の方針は、Σ の証明が持っている証人を射影で取り出して関数にすることです。

定理 4.2（型理論版の選択公理）✓

型 $A,B$ と型族 $R(x,y)$（$x:A$, $y:B$）について、次の型の閉項が存在する。

$$\Bigl(\Pi_{(x:A)}\Sigma_{(y:B)}R(x,y)\Bigr)\to\Sigma_{(f:A\to B)}\Pi_{(x:A)}R(x,f(x)).$$

証明（定理 4.2）

$h:\Pi_{(x:A)}\Sigma_{(y:B)}R(x,y)$ を仮定する。$f:\equiv\lambda x.\,\mathrm{pr}_1(h\,x):A\to B$ とおく。$x:A$ について $\mathrm{pr}_2(h\,x):R(x,\mathrm{pr}_1(h\,x))$ であり、Π の計算規則により $f(x)\equiv\mathrm{pr}_1(h\,x)$ なので、変換規則によって $\mathrm{pr}_2(h\,x):R(x,f(x))$。よって $g:\equiv\lambda x.\,\mathrm{pr}_2(h\,x):\Pi_{(x:A)}R(x,f(x))$ で、$(f,g)$ が求める型の項である。全体は $\lambda h.(f,g)$。

∎

集合論の選択公理（公理 3.1［選択公理と Zorn の補題］）は ZF から証明できない独立な公理でした（定理 8.2［公理的集合論 ZFC］）。ところが型理論では、同じ形の命題が数行で定理になります。からくりは、$\Sigma$ の証明が証人 $\mathrm{pr}_1(h\,x)$ を中に持っていることです。「各 $x$ に $y$ が存在する」ことの証明がすでに $y$ の選び方を含んでいるので、選ぶ作業は要りません。Lean でもそのまま書けます。

def ac {A B : Type} {R : A → B → Type}
    (h : (x : A) → (y : B) × R x y) : (f : A → B) × ((x : A) → R x (f x)) :=
  ⟨fun x => (h x).1, fun x => (h x).2⟩

(y : B) × R x y が $\Sigma_{(y:B)}R(x,y)$、.1 と .2 が射影です。ところが、同じことを Lean の ∃（Prop の存在量化）で書くとこの証明は通りません。その理由は §8 で説明します。

5. 恒等型

「$a$ と $b$ が等しい」も命題なので、型として表します。マーティン＝レーフの恒等型は、等号の導入規則を反射律だけにし、除去規則を「反射律の場合に示せば十分」という形にしたものです。

定義 5.1（恒等型）↗

形成：$\Gamma\vdash a:A$ と $\Gamma\vdash b:A$ から $\Gamma\vdash\mathrm{Id}_A(a,b)\ \mathsf{type}$。$a=_Ab$ とも書く。

導入：$\Gamma\vdash a:A$ から $\Gamma\vdash\mathsf{refl}_a:\mathrm{Id}_A(a,a)$。

除去（J 規則）：型族 $\Gamma,x{:}A,y{:}A,p{:}\mathrm{Id}_A(x,y)\vdash C(x,y,p)\ \mathsf{type}$ と、$\Gamma,z{:}A\vdash d(z):C(z,z,\mathsf{refl}_z)$ が与えられたとき、$\Gamma\vdash a,b:A$ と $\Gamma\vdash q:\mathrm{Id}_A(a,b)$ に対して $\Gamma\vdash J(d,a,b,q):C(a,b,q)$。

計算：$J(d,a,a,\mathsf{refl}_a)\equiv d(a)$。

J 規則は「等号についての帰納法」です。$\mathrm{Id}_A$ を $\mathsf{refl}$ だけで生成された型族と見て、性質 $C$ を $\mathsf{refl}$ の場合に確かめれば、すべての等号の証明について成り立つ、と主張しています。

次の命題のねらいは、J 規則だけから、等号について普段使う性質（対称性・推移性など）が導けることを確かめることです。J 規則の使い方は、示したい性質を表す型族 $C$ と、$x=y$ が $\mathsf{refl}$ の場合（両辺が同じ $z$ の場合）の証明 $d$ を指定する、という二つの選択に尽きます。推移性の (2) で $C$ に「$\Pi_{(w:A)}$」が付くのは、$b$ と $c$ の等号の証明を後から受け取れるように、その部分を先に量化しておくためです。

命題 5.2（等号の基本性質）✓

任意の $a,b,c:A$ について、次の型の項が J 規則から構成できる。

1. （対称性）$\mathrm{Id}_A(a,b)\to\mathrm{Id}_A(b,a)$。
2. （推移性）$\mathrm{Id}_A(a,b)\to\mathrm{Id}_A(b,c)\to\mathrm{Id}_A(a,c)$。
3. （輸送）型族 $P(x)$（$x:A$）について $\mathrm{Id}_A(a,b)\to P(a)\to P(b)$。
4. （合同）関数 $f:A\to B$ について $\mathrm{Id}_A(a,b)\to\mathrm{Id}_B(f\,a,f\,b)$。

証明（命題 5.2）

いずれも J 規則の $C$ と $d$ を指定すればよい。

1. $C(x,y,p):\equiv\mathrm{Id}_A(y,x)$、$d(z):\equiv\mathsf{refl}_z:\mathrm{Id}_A(z,z)\equiv C(z,z,\mathsf{refl}_z)$。$q:\mathrm{Id}_A(a,b)$ について $J(d,a,b,q):\mathrm{Id}_A(b,a)$。
2. $C(x,y,p):\equiv\Pi_{(w:A)}\,\mathrm{Id}_A(y,w)\to\mathrm{Id}_A(x,w)$、$d(z):\equiv\lambda w.\lambda r.\,r$。$C(z,z,\mathsf{refl}_z)\equiv\Pi_{(w:A)}\mathrm{Id}_A(z,w)\to\mathrm{Id}_A(z,w)$ なので型が合う。$J(d,a,b,q)$ を $c$ と $\mathrm{Id}_A(b,c)$ の証明に適用する。
3. $C(x,y,p):\equiv P(x)\to P(y)$、$d(z):\equiv\lambda u.u$。
4. $C(x,y,p):\equiv\mathrm{Id}_B(f\,x,f\,y)$、$d(z):\equiv\mathsf{refl}_{f\,z}$。

∎

輸送 (3) は、ライプニッツの「等しいものは同じ性質をもつ」の型理論版です。Lean では J 規則は Eq.rec で、tactic cases p は等号の証明 p : a = b に J 規則を適用して $b$ を $a$ に置き換えます。

theorem my_symm {A : Type} {a b : A} (p : a = b) : b = a := by
  cases p
  rfl

def transport {A : Type} (P : A → Type) {a b : A} (p : a = b) (x : P a) : P b :=
  p ▸ x

cases p の後の目標は a = a になり、rfl（$\mathsf{refl}$）で閉じます。p ▸ x は輸送の記法です。

定理 5.3（UIP と関数外延性の独立性）※

MLTT（Π・Σ・Id・ℕ・宇宙をもつ内包的型理論）では、次の二つはどちらも証明も反証もできない。

1. （UIP：等号の証明の一意性）$\Pi_{(a,b:A)}\Pi_{(p,q:\mathrm{Id}_A(a,b))}\mathrm{Id}(p,q)$。
2. （関数外延性）$f,g:\Pi_{(x:A)}B(x)$ について $\bigl(\Pi_{(x:A)}\mathrm{Id}(f\,x,g\,x)\bigr)\to\mathrm{Id}(f,g)$。

注意 5.4（証明の所在と、その後）

主張だけを述べます。UIP については、ホフマンとシュトライヒャー (1998) が型を亜群（すべての射が可逆な圏）で、恒等型を射の集合で解釈するモデルを作り、そこでは同じ 2 点の間に異なる射があるので UIP が偽になることを示しました。UIP が成り立つモデル（集合によるモデル）もあるので、UIP は独立です。関数外延性も、成り立つモデルと成り立たないモデルの両方があります。

J 規則から UIP が出ないことは、一見すると欠陥に見えますが、ここからホモトピー型理論が生まれました。$\mathrm{Id}_A(a,b)$ を「$a$ から $b$ への道」と読むと、J 規則は道に沿った輸送、UIP の失敗は「同じ 2 点を結ぶ道が本質的に異なりうる」ことにあたります。一方、Lean は Prop の証明の無関係性（§8）によって UIP を、商型の公理 Quot.sound によって関数外延性を、それぞれ定理として成り立たせています（証明支援系 Lean の仕組み）。

6. 帰納型：自然数

定義 6.1（自然数型）↗

形成：$\vdash\mathbb{N}\ \mathsf{type}$。導入：$\vdash0:\mathbb{N}$、$n:\mathbb{N}\vdash\mathrm{succ}(n):\mathbb{N}$。

除去：型族 $\Gamma,n{:}\mathbb{N}\vdash C(n)\ \mathsf{type}$、$\Gamma\vdash c_0:C(0)$、$\Gamma\vdash c_s:\Pi_{(n:\mathbb{N})}C(n)\to C(\mathrm{succ}(n))$ から、$\Gamma,n{:}\mathbb{N}\vdash\mathrm{ind}(c_0,c_s,n):C(n)$。

計算：$\mathrm{ind}(c_0,c_s,0)\equiv c_0$、$\mathrm{ind}(c_0,c_s,\mathrm{succ}(n))\equiv c_s\,n\,\mathrm{ind}(c_0,c_s,n)$。

除去規則は、$C$ を命題と読めば数学的帰納法（定理 3.2［証明の技術］）、$C$ を定数の型 $\mathbb{N}$ と読めば原始再帰による関数の定義です。集合論では再帰的定義の原理（定理 3.3［公理的集合論 ZFC］）を定理として証明しましたが、型理論ではそれが規則そのものです。ここでは $\mathbb{N}=\{0,1,2,\ldots\}$ です。

例 6.2（加法と 0 + n = n）

加法を $m+n:\equiv\mathrm{ind}(m,\ \lambda k.\lambda r.\mathrm{succ}(r),\ n)$（$C(n):\equiv\mathbb{N}$）で定めます。計算規則から $m+0\equiv m$、$m+\mathrm{succ}(n)\equiv\mathrm{succ}(m+n)$。したがって $n+0=n$ は $\mathsf{refl}_n$ で証明できます（定義的に等しい）。

$0+n=n$ は定義的には成り立たず、帰納法が要ります。$C(n):\equiv\mathrm{Id}_{\mathbb{N}}(0+n,n)$ とおくと、$c_0:\equiv\mathsf{refl}_0:C(0)$（$0+0\equiv0$）。帰納段階では $p:\mathrm{Id}(0+n,n)$ から $\mathrm{Id}(0+\mathrm{succ}(n),\mathrm{succ}(n))\equiv\mathrm{Id}(\mathrm{succ}(0+n),\mathrm{succ}(n))$ の証明を作ればよく、命題 5.2 (4) で $\mathrm{succ}$ を両辺に施せば得られます。Lean で自分の自然数型を定義すると、除去規則がそのまま自動生成されます。

inductive MyNat where
  | zero : MyNat
  | succ : MyNat → MyNat

#check @MyNat.rec
-- @MyNat.rec : {motive : MyNat → Sort u_1} →
--   motive MyNat.zero → ((a : MyNat) → motive a → motive a.succ) → (t : MyNat) → motive t

def MyNat.add (m : MyNat) : MyNat → MyNat
  | .zero   => m
  | .succ n => .succ (m.add n)

theorem MyNat.zero_add (n : MyNat) : MyNat.zero.add n = n := by
  induction n with
  | zero => rfl
  | succ k ih => simp [MyNat.add, ih]

MyNat.rec の型が上の除去規則そのもので、motive が $C$ です。induction n with はこの MyNat.rec を適用する tactic で、zero と succ k ih の二つの場合（$c_0$ と $c_s$。ih が帰納法の仮定 $C(k)$）を書かせます。simp [MyNat.add, ih] は、加法の定義と帰納法の仮定で目標を書き換えて閉じます。

同じ形の規則で、リスト、二分木、さらに一般の帰納型（W 型）も定義できます。Lean の inductive 宣言は、構成子の型を与えると形成・導入・除去・計算の 4 つの規則を自動で生成する仕組みです。

7. 宇宙

型を値として扱い、型を返す関数（型族）を項として書くために、型の型を用意します。

定義 7.1（宇宙）↗

宇宙の列 $\mathcal{U}_0,\mathcal{U}_1,\ldots$ を置き、$\mathcal{U}_i:\mathcal{U}_{i+1}$ とする。各 $\mathcal{U}_i$ は $\mathbb{N}$、空の型 $\mathbb{0}$、1 元型 $\mathbb{1}$（元 $\star$）を含み、Π・Σ・Id で閉じている。$A:\mathcal{U}_i$ ならば $A$ は型であり、$A:\mathcal{U}_{i+1}$ でもある（累積性）。

$\mathcal{U}:\mathcal{U}$（すべての型の型が自分自身を含む）とすると、ジラールのパラドックスにより矛盾が導かれることが知られています。集合論で「すべての集合の集合」が存在しない（命題 2.2［公理的集合論 ZFC］）のと同じ事情で、宇宙を階層にするのはそのためです。Lean でも Type : Type 1、Type 1 : Type 2、… と階層になっています。

Lean の宇宙の階層。各宇宙はその下の宇宙を元として含む。Prop だけは非可述的で、証明の無関係性をもつ。

宇宙は便利さのためだけにあるのではありません。宇宙がないと証明できない基本的な命題があります。

次の定理のねらいは、「$0$ は $\mathrm{succ}(n)$ と等しくない」という当たり前に見える事実を、規則から証明することです。方針は、$0$ のときは「いつでも証明できる型」$\mathbb{1}$、$\mathrm{succ}(n)$ のときは「証明が存在しない型」$\mathbb{0}$ を返す型の関数 $P$ を作り、等しいなら $P(0)$ の値が $P(\mathrm{succ}(n))$ の値に運ばれてしまう、という矛盾を作ることです。型を返す関数を作るために宇宙が必要になります。

定理 7.2（ペアノの第 4 公理）✓

宇宙 $\mathcal{U}$ をもつ MLTT では、$\Pi_{(n:\mathbb{N})}\bigl(\mathrm{Id}_{\mathbb{N}}(0,\mathrm{succ}(n))\to\mathbb{0}\bigr)$ の閉項が存在する。すなわち $0\ne\mathrm{succ}(n)$ が証明できる。

証明（定理 7.2）

自然数の除去規則を $C(n):\equiv\mathcal{U}$（定数の型族）に使って、型族 $P:\mathbb{N}\to\mathcal{U}$ を

$$P(n):\equiv\mathrm{ind}(\mathbb{1},\ \lambda k.\lambda X.\,\mathbb{0},\ n)$$

で定める。計算規則から $P(0)\equiv\mathbb{1}$、$P(\mathrm{succ}(n))\equiv\mathbb{0}$。$p:\mathrm{Id}_{\mathbb{N}}(0,\mathrm{succ}(n))$ が与えられたとき、輸送（命題 5.2 (3)）で $\star:P(0)$ を運ぶと $P(\mathrm{succ}(n))\equiv\mathbb{0}$ の項が得られる。よって $\lambda n.\lambda p.\,\mathrm{transport}^P(p,\star)$ が求める項である。

∎

証明の要は、型を値とする関数 $P$ を帰納法で定義したところです（大きな除去）。スミス (1988) は、宇宙をもたない MLTT では $0\ne1$ が証明できないことを示しました（主張のみ）。宇宙がないと、「$0$ と $\mathrm{succ}(n)$ を区別する述語」を作る手段がないのです。Lean では同じ証明を次のように書けます。

def IsZero : Nat → Prop
  | 0     => True
  | _ + 1 => False

theorem zero_ne_succ (n : Nat) : 0 ≠ n + 1 := by
  intro h
  have t : IsZero 0 := trivial
  rw [h] at t
  exact t

IsZero が $P$ で、rw [h] at t が輸送です。t : IsZero (n + 1) は定義により False なので、exact t で証明が閉じます。

8. 構成の計算 (CIC) と Prop

Lean の論理は、MLTT とは別の系譜である構成の計算（コカンとユエ 1988）に帰納型を加えた帰納的構成の計算 (CIC) の一種です。最大の違いは、命題専用の宇宙 $\mathsf{Prop}$ を置くことです。

定義 8.1（Prop と Type）↗

宇宙を $\mathsf{Prop}:\mathsf{Type}_0:\mathsf{Type}_1:\cdots$ と並べる（Lean では $\mathsf{Sort}\ 0=\mathsf{Prop}$、$\mathsf{Sort}\ (u+1)=\mathsf{Type}\ u$）。Π 型の形成規則は、$B(x):\mathsf{Prop}$ ならば、$A$ がどの宇宙にあっても $\Pi_{(x:A)}B(x):\mathsf{Prop}$ とする（非可述性）。さらに Lean では、$P:\mathsf{Prop}$ の任意の二つの証明 $h_1,h_2:P$ は定義的に等しい（証明の無関係性）。

非可述性により、$\Pi_{(X:\mathsf{Prop})}X\to X$ のように「すべての命題について」量化した命題も、また $\mathsf{Prop}$ に属します。数学で「すべての部分集合について」と量化する感覚に近く、通常の数学を書くのに便利です。証明の無関係性は「証明はどれでも同じ」という数学者の感覚を規則にしたもので、UIP はここから直ちに従います。

その代償として、$\mathsf{Prop}$ の帰納型（∃、∨ など）からは、一般には $\mathsf{Type}$ の値を取り出せません。

次の命題のねらいは、Prop の ∃ から証人を取り出せない理由を、前の定理との矛盾として示すことです。証明の無関係性とは、同じ命題の二つの証明を区別しない、という規則です。区別しない以上、「どの証人が入っていたか」を答える関数は作れません。

命題 8.2（∃ から証人を取り出せない理由）✓

証明の無関係性のもとで、∃ n : Nat, True の証明から自然数を取り出す関数 $w$ で、$w(\langle n,h\rangle)\equiv n$ を満たすものがあるとすると、$0=1$ が導かれる。

証明（命題 8.2）

$\langle0,\mathsf{trivial}\rangle$ と $\langle1,\mathsf{trivial}\rangle$ はどちらも命題 ∃ n : Nat, True の証明なので、証明の無関係性により定義的に等しい。$w$ を施すと $0\equiv w(\langle0,\mathsf{trivial}\rangle)\equiv w(\langle1,\mathsf{trivial}\rangle)\equiv1$。これは 定理 7.2 に反する。

∎

そこで CIC では、Prop の帰納型を Prop 以外へ除去することを、構成子が高々一つで引数がすべて証明であるもの（True、And、Eq など）に限ります（部分単集合除去）。∃ はこの条件を満たしません。その結果、§4 の型理論版の選択公理を ∃ で書くには、Prop の証明から証人を「選ぶ」公理 Classical.choice が必要になります。

theorem ac_prop {A B : Type} {R : A → B → Prop}
    (h : ∀ x, ∃ y, R x y) : ∃ f : A → B, ∀ x, R x (f x) :=
  ⟨fun x => Classical.choose (h x), fun x => Classical.choose_spec (h x)⟩

#print axioms ac_prop   -- 'ac_prop' depends on axioms: [Classical.choice]

$\Sigma$ で書けば公理なしの定理、$\exists$ で書けば選択公理が要る。この差が、型理論で選択公理を考えるときの核心です。

	MLTT	CIC（Lean）
命題	型そのもの	Prop の元
宇宙	$\mathcal{U}_0:\mathcal{U}_1:\cdots$（可述的）	Prop（非可述的）$:$ Type 0 $:$ Type 1 $:\cdots$
$\exists$	$\Sigma$（証人を取り出せる）	Exists（Prop へしか除去できない）
UIP	独立	証明の無関係性から成り立つ
関数外延性	独立	Quot.sound から定理
選択	$\Sigma$ 版は定理	Classical.choice は公理

MLTT と、公理を加えない CIC の核の部分は、型検査が決定可能であり、閉じた項が正規形をもつ（したがって $\mathbb{0}$ や False の閉項は存在せず、体系は無矛盾である）ことが知られています。ただし Lean 4 の実際のカーネル（商型、証明の無関係性、整礎再帰の Acc などを備える）では、定義的同値が決定可能とは限りません（証明支援系 Lean の仕組み の 注意 3.2［証明支援系 Lean の仕組み］）。無矛盾性は ZFC と少しの大きな基数を仮定すれば示されています。それらの証明は前章の強正規化定理（定理 3.1［単純型付きラムダ計算とカリー＝ハワード対応］）のテイトの方法を、宇宙と帰納型まで大きく拡張したもので、ここでは主張だけを述べます。もちろん、第二不完全性定理（定理 6.1［ゲーデルの不完全性定理］）により、この無矛盾性の証明はその体系自身の中では行えません。

9. 演習

演習 9.1易

型 $A,B,C$ について、$(A\times B\to C)\to(A\to B\to C)$ と $(A\to B\to C)\to(A\times B\to C)$ の項を作れ。（$A\times B$ は $\Sigma_{(x:A)}B$。）

解答

前者は $\lambda f.\lambda a.\lambda b.\,f\,(a,b)$。後者は $\lambda g.\lambda p.\,g\,(\mathrm{pr}_1p)\,(\mathrm{pr}_2p)$、あるいは Σ の除去を直接使って $\lambda g.\lambda p.\,\mathrm{split}((x,y)\mapsto g\,x\,y,\ p)$。命題として読めば「$A\wedge B$ ならば $C$」と「$A$ ならば（$B$ ならば $C$）」の同値で、プログラムとしては関数のカリー化です。

演習 9.2標準

$\Pi_{(m,n:\mathbb{N})}\,\mathrm{Id}(\mathrm{succ}(m),\mathrm{succ}(n))\to\mathrm{Id}(m,n)$ の項を作れ（ペアノの第 3 公理）。

解答

前者関数 $\mathrm{pred}:\equiv\lambda n.\,\mathrm{ind}(0,\ \lambda k.\lambda r.\,k,\ n):\mathbb{N}\to\mathbb{N}$ を定める（$C(n):\equiv\mathbb{N}$）。計算規則から $\mathrm{pred}(\mathrm{succ}(k))\equiv k$。$p:\mathrm{Id}(\mathrm{succ}(m),\mathrm{succ}(n))$ に合同（命題 5.2 (4)）を $f=\mathrm{pred}$ で使うと $\mathrm{Id}(\mathrm{pred}(\mathrm{succ}(m)),\mathrm{pred}(\mathrm{succ}(n)))\equiv\mathrm{Id}(m,n)$ の項が得られる。こちらは宇宙なしで証明でき、定理 7.2 との違いは、区別に使う関数の値が $\mathbb{N}$ という「小さい」型で済むことです。

演習 9.3標準

$a:A$ を固定する。J 規則を使って、$\Pi_{(y:A)}\Pi_{(p:\mathrm{Id}_A(a,y))}\,\mathrm{Id}\bigl((a,\mathsf{refl}_a),(y,p)\bigr)$ の項を作れ。ここで右側の $\mathrm{Id}$ は型 $\Sigma_{(w:A)}\mathrm{Id}_A(a,w)$ の中の等号である。

解答

$a$ を固定したままでは J 規則が使えない（J は両端点を動かす）ので、$a$ も動かして $C(x,y,p):\equiv\mathrm{Id}_{\Sigma_{(w:A)}\mathrm{Id}_A(x,w)}\bigl((x,\mathsf{refl}_x),(y,p)\bigr)$ とおく。$C(z,z,\mathsf{refl}_z)$ は $(z,\mathsf{refl}_z)$ とそれ自身の等号なので、$d(z):\equiv\mathsf{refl}_{(z,\mathsf{refl}_z)}$ がその項である。J 規則により $J(d,a,y,p):C(a,y,p)$ で、$\lambda y.\lambda p.\,J(d,a,y,p)$ が求める項になる。「$a$ から出る道の全体」は 1 点に縮む、というホモトピー型理論の基本的な事実の一つです。UIP（$p=\mathsf{refl}_a$ そのもの）とは違い、端点 $y$ も一緒に動かしている点に注意してください。

演習 9.4易

$f:A\to B$ が「Σ の意味で全射」、すなわち $s:\Pi_{(b:B)}\Sigma_{(a:A)}\mathrm{Id}(f\,a,b)$ をもつとする。$f\circ g$ が各点で恒等写像に等しい $g:B\to A$ を構成せよ。

解答

定理 4.2 を $R(b,a):\equiv\mathrm{Id}(f\,a,b)$ に使うと、$g:B\to A$ と $\Pi_{(b:B)}\mathrm{Id}(f(g\,b),b)$ の組が得られる。具体的には $g:\equiv\lambda b.\,\mathrm{pr}_1(s\,b)$、証明は $\lambda b.\,\mathrm{pr}_2(s\,b)$。集合論では「全射は右逆写像をもつ」を選択公理を使って示しました（命題 3.2［選択公理と Zorn の補題］）が、Σ の意味の全射は右逆写像の情報をすでに含んでいます。

参考文献

• P. Martin-Löf, Intuitionistic Type Theory, Bibliopolis, 1984.
• B. Nordström, K. Petersson and J. M. Smith, Programming in Martin-Löf’s Type Theory: An Introduction, Oxford University Press, 1990.
• The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013 — 第 1 章（型理論の規則）、第 2 章（恒等型）。
• T. Coquand and G. Huet, “The calculus of constructions”, Information and Computation 76 (1988), 95–120.
• M. Hofmann and T. Streicher, “The groupoid interpretation of type theory”, in G. Sambin and J. Smith (eds.), Twenty-Five Years of Constructive Type Theory, Oxford University Press, 1998, 83–111.
• J. M. Smith, “The independence of Peano’s fourth axiom from Martin-Löf’s type theory without universes”, The Journal of Symbolic Logic 53 (1988), 840–845.