[0033] ファイバー余積

ファイバー余積は汎用的な高次帰納的型である。

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

-ファイバー余積(fiber coproduct) $A\mathbin {{}_{f}\smash {+}_{g}}B:\mathcal {U}(i)$ を構成できる。
-要素 $$a:A$$ に対して、要素 $\mathord {\textnormal {\textsf {in}}}_{1}(a):A\mathbin {{}_{f}\smash {+}_{g}}B$ を構成できる。
-要素 $$b:B$$ に対して、要素 $\mathord {\textnormal {\textsf {in}}}_{2}(b):A\mathbin {{}_{f}\smash {+}_{g}}B$ を構成できる。
-要素 $$c:C$$ に対して、同一視 $\mathord {\textnormal {\textsf {glue}}}(c):\mathord {\textnormal {\textsf {in}}}_{1}(f(c))=\mathord {\textnormal {\textsf {in}}}_{2}(g(c))$ を構成できる。
- $d:A\mathbin {{}_{f}\smash {+}_{g}}B$ を要素、 $$j$$ を階数、 $E:A\mathbin {{}_{f}\smash {+}_{g}}B\to \mathcal {U}(j)$ を型の族、 $e_{1}:\prod _{x:A}E(\mathord {\textnormal {\textsf {in}}}_{1}(x))$ と $e_{2}:\prod _{y:B}E(\mathord {\textnormal {\textsf {in}}}_{2}(y))$ を関数、 $p:\prod _{z:C}e_{1}(f(z))=_{\mathord {\textnormal {\textsf {glue}}}(z)}^{E}e_{2}(g(z))$ を同一視とすると、要素 $\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}(d,E,e_{1},e_{2},p):E(d)$ を構成できる。
- $$a:A$$ を要素、 $$j$$ を階数、 $E:A\mathbin {{}_{f}\smash {+}_{g}}B\to \mathcal {U}(j)$ を型の族、 $e_{1}:\prod _{x:A}E(\mathord {\textnormal {\textsf {in}}}_{1}(x))$ と $e_{2}:\prod _{y:B}E(\mathord {\textnormal {\textsf {in}}}_{2}(y))$ を関数、 $p:\prod _{z:C}e_{1}(f(z))=_{\mathord {\textnormal {\textsf {glue}}}(z)}^{E}e_{2}(g(z))$ を同一視とすると、 $\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}(\mathord {\textnormal {\textsf {in}}}_{1}(a),E,e_{1},e_{2},p)\equiv e_{1}(a)$ と定義される。
- $$b:B$$ を要素、 $$j$$ を階数、 $E:A\mathbin {{}_{f}\smash {+}_{g}}B\to \mathcal {U}(j)$ を型の族、 $e_{1}:\prod _{x:A}E(\mathord {\textnormal {\textsf {in}}}_{1}(x))$ と $e_{2}:\prod _{y:B}E(\mathord {\textnormal {\textsf {in}}}_{2}(y))$ を関数、 $p:\prod _{z:C}e_{1}(f(z))=_{\mathord {\textnormal {\textsf {glue}}}(z)}^{E}e_{2}(g(z))$ を同一視とすると、 $\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}(\mathord {\textnormal {\textsf {in}}}_{2}(b),E,e_{1},e_{2},p)\equiv e_{2}(b)$ と定義される。
- $$c:C$$ を要素、 $$j$$ を階数、 $E:A\mathbin {{}_{f}\smash {+}_{g}}B\to \mathcal {U}(j)$ を型の族、 $e_{1}:\prod _{x:A}E(\mathord {\textnormal {\textsf {in}}}_{1}(x))$ と $e_{2}:\prod _{y:B}E(\mathord {\textnormal {\textsf {in}}}_{2}(y))$ を関数、 $p:\prod _{z:C}e_{1}(f(z))=_{\mathord {\textnormal {\textsf {glue}}}(z)}^{E}e_{2}(g(z))$ を同一視とすると、同一視 $\mathord {\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}\mathord {\textnormal {\textsf {-}}}\mathord {\textnormal {\textsf {glue}}}}(c,E,e_{1},e_{2},p):\mathord {\textnormal {\textsf {apd}}}(\lambda d.\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}(d,E,e_{1},e_{2},p),\mathord {\textnormal {\textsf {glue}}}(c))=p(c)$ を構成できる。

高次帰納的型も通常の帰納的型と同様にいくつかの構成子によって定められる。ファイバー余積の場合、 $\mathord {\textnormal {\textsf {in}}}_{1}$ と $\mathord {\textnormal {\textsf {in}}}_{2}$ と $\mathord {\textnormal {\textsf {glue}}}$ が構成子である。 $\mathord {\textnormal {\textsf {in}}}_{1}$ と $\mathord {\textnormal {\textsf {in}}}_{2}$ は $A\mathbin {{}_{f}\smash {+}_{g}}B$ の要素を構成する普通の構成子である。 $\mathord {\textnormal {\textsf {glue}}}$ が同一視を構成するという点が新しい。要素を構成する構成子はpoint constructorと、同一視を構成する構成子はpath constructorと呼ばれることもある。

残りの規則はファイバー余積の帰納法原理で、型 $A\mathbin {{}_{f}\smash {+}_{g}}B$ が $\mathord {\textnormal {\textsf {in}}}_{1}$ と $\mathord {\textnormal {\textsf {in}}}_{2}$ と $\mathord {\textnormal {\textsf {glue}}}$ で自由に生成されることを表す。ただし、 $\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}(\mathord {\textnormal {\textsf {in}}}_{1}(a),E,e_{1},e_{2},p)\equiv e_{1}(a)$ と $\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}(\mathord {\textnormal {\textsf {in}}}_{2}(b),E,e_{1},e_{2},p)\equiv e_{2}(b)$ は定義であるのに対し、 $\mathord {\textnormal {\textsf {apd}}}(\lambda d.\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}(d,E,e_{1},e_{2},p),\mathord {\textnormal {\textsf {glue}}}(c))=p(c)$ は同一視を構成する。理想的には $\mathord {\textnormal {\textsf {apd}}}(\lambda d.\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}(d,E,e_{1},e_{2},p),\mathord {\textnormal {\textsf {glue}}}(c))\equiv p(c)$ と定義したいところだが、これは単なる $\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}$ の定義ではなく $\mathord {\textnormal {\textsf {ind}}}_{\mathbin {{}_{.}\smash {+}_{.}}}$ と $\mathord {\textnormal {\textsf {apd}}}$ に関する複合的な定義である。 $\mathord {\textnormal {\textsf {apd}}}$ はプリミティヴではなく我々が構成した関数([007I])なので、それに関する新たな定義の正当性は無い。

ファイバー余積を使って構成できる型には次のようなものがある。

[007V] 定義

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型とする。関数 $f:A\to \mathbf {1}$ を $\lambda \_.\mathord {\star }$ とする。懸垂(suspension) $\mathord {\textnormal {\textsf {Susp}}}(A):\mathcal {U}(i)$ を $\mathbf {1}\mathbin {{}_{f}\smash {+}_{f}}\mathbf {1}$ と定義する。

[003M] 定義

自然数 $n:\mathbb {N}$ に対して、 $$n$$ 次元球面( $$n$$ -dimensional sphere) $\mathbb {S}^{n}:\mathcal {U}(0)$ を次のように定義する。

-便宜的に $$-1$$ 次元球面 $\mathbb {S}^{-1}$ を $\mathbf {0}$ と定義する。
- $\mathbb {S}^{0}\equiv \mathord {\textnormal {\textsf {Susp}}}(\mathbb {S}^{-1})$
- $\mathbb {S}^{\mathord {\textnormal {\textsf {succ}}}(n)}\equiv \mathord {\textnormal {\textsf {Susp}}}(\mathbb {S}^{n})$

[007W] 定義

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。関数 $g:A\to \mathbf {1}$ を $\lambda \_.\mathord {\star }$ とする。 $$f$$ のコファイバー(cofiber) $\mathord {\textnormal {\textsf {Cofiber}}}(f)$ を $B\mathbin {{}_{f}\smash {+}_{g}}\mathbf {1}$ と定義する。

位相幾何学において、CW複体は、 $$n$$ 次元球を境界( $$n-1$$ 次元球面)に沿って貼り付ける操作を繰り返して得られる空間である。 $$n$$ 次元球が可縮であることをふまえると、 $$n$$ 次元球を境界 $f:\mathbb {S}^{n-1}\to X$ に沿って空間 $$X$$ に貼り付けたものは $$f$$ のコファイバーとホモトピー同値である。したがって、型理論において、 $f:\mathbb {S}^{n-1}\to X$ の形の関数のコファイバーを取る操作を繰り返すことで有限CW複体(のホモトピー型)を構成できる。