[002U] 有限余積

自然数型の他にも重要な帰納的型がある。最も簡単な帰納的型は空型である。

-空型(empty type) $\mathbf {0}:\mathcal {U}(0)$ を構成できる。
- $c:\mathbf {0}$ を要素、 $$i$$ を階数、 $A:\mathbf {0}\to \mathcal {U}(i)$ を型の族とすると、要素 $\mathord {\textnormal {\textsf {ind}}}_{\mathbf {0}}(c,A):A(c)$ を構成できる。

空型には構成子が一つも与えられていない。よって、型理論の中の人にとっては $\mathbf {0}$ の要素は存在しないはずである。言い換えれば、 $\mathbf {0}$ の要素は矛盾(contradiction)を表し、帰納法原理は矛盾からはすべてを導けること、爆発原理(principle of explosionまたはex falso quodlibet)を意味する。

次に簡単な帰納的型は余積である。

[002Z] 規則

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型とする。

-余積(coproduct) $A+B:\mathcal {U}(i)$ を構成できる。
-要素 $$a:A$$ に対して、要素 $\mathord {\textnormal {\textsf {in}}}_{1}(a):A+B$ を構成できる。
-要素 $$b:B$$ に対して、要素 $\mathord {\textnormal {\textsf {in}}}_{2}(b):A+B$ を構成できる。
- $$c:A+B$$ を要素、 $$j$$ を階数、 $D:A+B\to \mathcal {U}(j)$ を型の族、 $d_{1}:\prod _{x:A}D(\mathord {\textnormal {\textsf {in}}}_{1}(x))$ を要素、 $d_{2}:\prod _{y:B}D(\mathord {\textnormal {\textsf {in}}}_{2}(y))$ を要素とすると、要素 $\mathord {\textnormal {\textsf {ind}}}_{+}(c,D,d_{1},d_{2}):D(c)$ を構成できる。
- $$a:A$$ を要素、 $$j$$ を階数、 $D:A+B\to \mathcal {U}(j)$ を型の族、 $d_{1}:\prod _{x:A}D(\mathord {\textnormal {\textsf {in}}}_{1}(x))$ を要素、 $d_{2}:\prod _{y:B}D(\mathord {\textnormal {\textsf {in}}}_{2}(y))$ を要素とすると、 $\mathord {\textnormal {\textsf {ind}}}_{+}(\mathord {\textnormal {\textsf {in}}}_{1}(a),D,d_{1},d_{2})\equiv d_{1}(a)$ と定義される。
- $$b:B$$ を要素、 $$j$$ を階数、 $D:A+B\to \mathcal {U}(j)$ を型の族、 $d_{1}:\prod _{x:A}D(\mathord {\textnormal {\textsf {in}}}_{1}(x))$ を要素、 $d_{2}:\prod _{y:B}D(\mathord {\textnormal {\textsf {in}}}_{2}(y))$ を要素とすると、 $\mathord {\textnormal {\textsf {ind}}}_{+}(\mathord {\textnormal {\textsf {in}}}_{2}(b),D,d_{1},d_{2})\equiv d_{2}(b)$ と定義される。

$\mathord {\textnormal {\textsf {in}}}_{1}$ と $\mathord {\textnormal {\textsf {in}}}_{2}$ が $$A+B$$ の構成子であり、帰納法原理はやはりこれらの構成子のみを使って得られるものだけが $$A+B$$ の要素であることを表す。

余積のパターンマッチは次のようになる。

[008F] 記法

$\mathord {\textnormal {\textsf {ind}}}_{+}$ を使って関数を定義するには次のような言い回しをする。

-関数 $f:\prod _{z:A+B}D(z)$ を $\lambda z.\mathord {\textnormal {\textsf {ind}}}_{+}(z,D,d_{1},d_{2})$ と定義する。
-関数 $f:\prod _{z:A+B}D(z)$ を $f(\mathord {\textnormal {\textsf {in}}}_{1}(x))\equiv d_{1}(x)$ と $f(\mathord {\textnormal {\textsf {in}}}_{2}(y))\equiv d_{2}(y)$ で定義する。
- $$z:A+B$$ を要素とする。要素 $$f(z):D(z)$$ を $f(\mathord {\textnormal {\textsf {in}}}_{1}(x))\equiv d_{1}(x)$ と $f(\mathord {\textnormal {\textsf {in}}}_{2}(y))\equiv d_{2}(y)$ で定義する。