ホモトピー型理論
概要
ホモトピー型理論（homotopy type theory）とは、Martin-Löf 型理論の恒等型の項を空間の道と読み、型を空間（$\infty$-亜群）として扱う理論で、Voevodsky の単一性公理と、道も生成元にもつ高次帰納的型を加えた体系である。単一性公理は、宇宙の中の型の等しさと同値を同一視する公理であり、そのもとで宇宙は集合でなく、円周の基本のループは自明でない。基本群 $\pi_1(S^1)\cong\mathbb{Z}$ などのホモトピー論の計算を型理論の中で行え、単体的集合のモデルをもつ。
前提知識: Martin-Löf型理論, ホモトピー, 亜群, ホモトピー群
Martin-Löf型理論では、恒等型 $a=_Ab$ の項は「$a$ と $b$ が等しいことの証明」であり、同じ $a,b$ の間に異なる証明がありうる。これを空間 $A$ の点 $a$ から点 $b$ への道と読み、道の間の等しさをホモトピーと読むと、型は空間（より正確には $\infty$-亜群）のように振る舞う（UFP13 Introduction, p. 3）。この読み方を基礎に、Martin-Löf 型理論に Voevodsky の 単一性公理（univalence axiom）と 高次帰納的型 を加えた体系が ホモトピー型理論（homotopy type theory、HoTT）である。
単一性公理は、宇宙の中の 2 つの型が等しいことと、それらが同値であることを同一視する。そのため、同値な構造の間で成り立つことは自動的に移り合い、「同型なものを同一視する」という数学の慣習が公理の形で正当化される。この記事では、同値と単一性公理を定義し、単一性公理から宇宙が集合でないこと、高次帰納的型としての円周 $S^1$ の基本のループが自明でないことを証明する。関数外延性の導出、$\pi_1(S^1)\cong\mathbb Z$、単体的集合によるモデル、ZFC との関係は所在を挙げて述べる。
型を空間として読む
Martin-Löf型理論 の補題「道の逆・合成と群の法則」により、道は逆と合成をもち、単位・逆・結合の法則が「道の間の道」として成り立つ。つまり各型は、点を対象、道を射とする亜群の構造を、法則が高次の道で成り立つ形でもつ（UFP13 §2.1, pp. 61–66）。型理論の操作は、論理・集合・ホモトピーの 3 つの読み方をもつ（UFP13 p. 11 の Table 1）。
| 型 | 論理 | 集合 | ホモトピー |
|---|---|---|---|
| $A$ | 命題 | 集合 | 空間 |
| $a:A$ | 証明 | 元 | 点 |
| $B(x)$ | 述語 | 集合の族 | ファイブレーション |
| $A\to B$ | 含意 | 写像の集合 | 写像空間 |
| $\sum_{x:A}B(x)$ | 存在 | 直和 | 全空間 |
| $\prod_{x:A}B(x)$ | 全称 | 直積 | 切断の空間 |
| $a=_Ab$ | 等号 | 対角集合 | 道の空間 |
関数 $f$ が道 $p$ を道 $\mathrm{ap}_f(p)$ に送ることは連続写像が道を道に送ることに、族 $P$ の輸送 $\mathrm{transport}^P(p,-)\colon P(x)\to P(y)$ はファイブレーションでの道の持ち上げにあたる（UFP13 §2.2–2.3, pp. 71–73）。
同値と単一性公理
$f,g\colon A\to B$ の間の ホモトピー とは $\prod_{x:A}(f(x)=g(x))$ の項のことで、その型を $f\sim g$ と書く（UFP13 Definition 2.4.1, p. 76）。$f\colon A\to B$ について
$$
\mathrm{isequiv}(f):\equiv\Bigl(\sum_{g:B\to A}(f\circ g\sim\mathrm{id}_B)\Bigr)\times\Bigl(\sum_{h:B\to A}(h\circ f\sim\mathrm{id}_A)\Bigr)
$$
とおき、その項をもつ $f$ を 同値 という。同値の型を $(A\simeq B):\equiv\sum_{f:A\to B}\mathrm{isequiv}(f)$ とする（UFP13 (2.4.10)・(2.4.11), p. 78）。
$g\colon B\to A$ で $f\circ g\sim\mathrm{id}_B$ かつ $g\circ f\sim\mathrm{id}_A$ となるもの（擬逆）があれば、$(g,\alpha,g,\beta)$ により $f$ は同値である。とくに $\mathrm{id}_A$ は、ホモトピー $x\mapsto\mathrm{refl}_x$ により同値である（UFP13 Example 2.4.7, p. 78）。
宇宙 $\mathcal U$ の型 $A,B$ について、道の帰納法で
$$
\mathrm{idtoeqv}\colon(A=_{\mathcal U}B)\to(A\simeq B),\qquad \mathrm{idtoeqv}(\mathrm{refl}_A)\equiv(\mathrm{id}_A,\varepsilon_A)
$$
を定める。ここで $\varepsilon_A$ は $\mathrm{id}_A$ が同値であることの上の項である。$\mathrm{idtoeqv}(p)$ の第 1 成分は、族 $X\mapsto X$ に沿う輸送 $\mathrm{transport}^{X\mapsto X}(p,-)\colon A\to B$ に等しい（UFP13 Lemma 2.10.1, p. 88）。
宇宙 $\mathcal U$ が 単一的（univalent）であるとは、任意の $A,B:\mathcal U$ について $\mathrm{idtoeqv}\colon(A=_{\mathcal U}B)\to(A\simeq B)$ が同値であることをいう。これを要請する公理を 単一性公理 という（UFP13 Axiom 2.10.3, p. 88）。
単一性公理のもとでは、$\mathrm{isequiv}(\mathrm{idtoeqv})$ の第 1 成分から、関数 $\mathrm{ua}\colon(A\simeq B)\to(A=_{\mathcal U}B)$ と、各 $e:A\simeq B$ について $\mathrm{idtoeqv}(\mathrm{ua}(e))=e$ の項が得られる。つまり同値な型は等しく、等しさの証明として同値そのものを使える。
次はこの記事では証明しない。
- 単一性公理（と関数についての定義上の $\eta$ 規則）から 関数外延性 が従う。すなわち $\mathrm{happly}\colon(f=g)\to(f\sim g)$ は同値である（UFP13 §4.9, Theorem 4.9.4–4.9.5, pp. 144–146、第 1 章の注, p. 54）。
- 半群などの代数的構造について、構造が等しいことと同型であることが一致する（UFP13 §2.14, pp. 96–99）。
- すべての型 $A:\mathcal U$ について $A+\neg A$ を与える関数は存在しない。すなわち、すべての型に対する排中律は単一性公理と両立しない（UFP13 Corollary 3.2.7, p. 111）。
型の階層
型 $A$ について次のように定める（UFP13 Definition 3.11.1, p. 124、Definition 3.3.1, p. 111、Definition 3.1.1, p. 107、Definition 3.1.7, p. 108）。
- 可縮：$a:A$ と $\prod_{x:A}(a=x)$ の項がある。
- 命題（mere proposition）：$\prod_{x,y:A}(x=y)$ の項がある。
- 集合：任意の $x,y:A$ について $x=y$ が命題である。
- 1-型：任意の $x,y:A$ について $x=y$ が集合である。
可縮な型は命題である。中心 $a$ と $c:\prod_{x}(a=x)$ があれば、$c(x)^{-1}\cdot c(y):x=y$ だからである。集合は、点の間の道が高々 1 つ（どの 2 つも等しい）型であり、Martin-Löf型理論 の定理「Hedberg の定理」により、決定可能な等号をもつ型 $\mathbf 2$・$\mathbb N$ は集合である。HoTT の数学では、ふつうの集合論の議論は集合の型の上で行い、命題は命題の型として扱う（UFP13 §3.1–3.3, pp. 107–113）。
主定理：宇宙は集合でない
Martin-Löf 型理論の道の帰納法だけからは、すべての型が集合であること（UIP）は証明できず、逆に集合でない型を実際に示すには単一性公理のような原理が要る（UFP13 §5.8, p. 171）。単一性公理を加えると、宇宙そのものが集合でなくなる。以下、関数の間の道からホモトピーを作る関数 $\mathrm{happly}\colon(f=g)\to(f\sim g)$ を、道の帰納法で $\mathrm{happly}(\mathrm{refl}_f):\equiv\lambda x.\,\mathrm{refl}_{f(x)}$ と定める（UFP13 (2.9.2), p. 86）。
$\mathcal U$ を $\mathbf 2:\mathcal U$ となる単一的な宇宙とする。このとき $\mathrm{refl}_{\mathbf 2}$ と等しくない道 $p:\mathbf 2=_{\mathcal U}\mathbf 2$ がある。とくに $\mathcal U$ は集合でない（UFP13 Example 3.1.9, p. 109）。
$\mathbf 2$ の場合分けで $\mathrm{neg}\colon\mathbf 2\to\mathbf 2$ を $\mathrm{neg}(0_{\mathbf 2}):\equiv1_{\mathbf 2}$、$\mathrm{neg}(1_{\mathbf 2}):\equiv0_{\mathbf 2}$ と定める。$\mathrm{neg}(\mathrm{neg}(0_{\mathbf 2}))\equiv0_{\mathbf 2}$、$\mathrm{neg}(\mathrm{neg}(1_{\mathbf 2}))\equiv1_{\mathbf 2}$ なので、場合分けで $\eta(0_{\mathbf 2}):\equiv\mathrm{refl}_{0_{\mathbf 2}}$、$\eta(1_{\mathbf 2}):\equiv\mathrm{refl}_{1_{\mathbf 2}}$ と定めると $\eta:\mathrm{neg}\circ\mathrm{neg}\sim\mathrm{id}_{\mathbf 2}$ である。よって $\mathrm{neg}$ は自分自身を擬逆にもち、同値 $e:\equiv(\mathrm{neg},(\mathrm{neg},\eta,\mathrm{neg},\eta)):\mathbf 2\simeq\mathbf 2$ を得る。$p:\equiv\mathrm{ua}(e)$ とおく。
$\alpha:p=\mathrm{refl}_{\mathbf 2}$ があったとして矛盾を導く。単一性公理による $\beta:\mathrm{idtoeqv}(\mathrm{ua}(e))=e$ と、$\mathrm{ap}_{\mathrm{idtoeqv}}(\alpha):\mathrm{idtoeqv}(p)=\mathrm{idtoeqv}(\mathrm{refl}_{\mathbf 2})\equiv(\mathrm{id}_{\mathbf 2},\varepsilon_{\mathbf 2})$ を合成すると、
$$
\gamma:\equiv\beta^{-1}\cdot\mathrm{ap}_{\mathrm{idtoeqv}}(\alpha):\ e=(\mathrm{id}_{\mathbf 2},\varepsilon_{\mathbf 2})
$$
を得る。第 1 成分をとると $\mathrm{ap}_{\mathrm{pr}_1}(\gamma):\mathrm{neg}=\mathrm{id}_{\mathbf 2}$ であり、$\mathrm{happly}$ を当てて $0_{\mathbf 2}$ で評価すると
$$
\mathrm{happly}(\mathrm{ap}_{\mathrm{pr}_1}(\gamma))(0_{\mathbf 2}):\ \mathrm{neg}(0_{\mathbf 2})=0_{\mathbf 2},\quad\text{すなわち}\quad 1_{\mathbf 2}=0_{\mathbf 2}
$$
である。その逆は $0_{\mathbf 2}=1_{\mathbf 2}$ の項であり、Martin-Löf型理論 の命題「真偽の 2 つの値は等しくない」（宇宙 $\mathcal U$ を使う）に反する。よって $\neg(p=\mathrm{refl}_{\mathbf 2})$ の項がある。
$\mathcal U$ が集合なら、同じ端点をもつ $p$ と $\mathrm{refl}_{\mathbf 2}$ は等しいはずなので、$\mathcal U$ は集合でない。$\square$
円周 $S^1$（下の節）を含む単一的な宇宙は 1-型でもなく、各 $n$ について $n$-型でない型がある（UFP13 Corollary 6.4.3, p. 186、Corollary 8.6.18, p. 284。この記事では証明しない）。
高次帰納的型と円周
高次帰納的型は、点だけでなく道を生成元にもつ型である。代表例が円周である。
円周 $S^1$ は、点 $\mathrm{base}:S^1$ と道 $\mathrm{loop}:\mathrm{base}=_{S^1}\mathrm{base}$ で生成される高次帰納的型である（UFP13 §6.1, p. 177）。その再帰原理は次のとおりである（UFP13 Lemma 6.2.5, p. 181）：型 $B$ と $b:B$、$\ell:b=_Bb$ に対し、
$$
f\colon S^1\to B,\qquad f(\mathrm{base})\equiv b,\qquad \mathrm{ap}_f(\mathrm{loop})=\ell
$$
となる $f$ がある。依存型の族への帰納原理もある（UFP13 §6.2, p. 181）。
$\mathrm{loop}$ は $\mathrm{refl}_{\mathrm{base}}$ と等しいとは定義から分からない。2 点を生成元にもつ $\mathbf 2$ の 2 点が等しくないのと同じく、生成元は「自由に」加えられるからである（UFP13 pp. 177–178）。実際に等しくないことは、単一性公理を使って示せる。
$\mathbf 2:\mathcal U$ となる単一的な宇宙 $\mathcal U$ があれば、$\mathrm{loop}\ne\mathrm{refl}_{\mathrm{base}}$ である（UFP13 Lemma 6.4.1, p. 185）。とくに $S^1$ は集合でない。
thm-hott-universe-not-set の道 $p:\mathbf 2=_{\mathcal U}\mathbf 2$（$p\ne\mathrm{refl}_{\mathbf 2}$）をとる。円周の再帰原理を $B:\equiv\mathcal U$（これは 1 つ上の宇宙の型である）、$b:\equiv\mathbf 2$、$\ell:\equiv p$ に当てて、$f\colon S^1\to\mathcal U$ と $\delta:\mathrm{ap}_f(\mathrm{loop})=p$ を得る。
$\alpha:\mathrm{loop}=\mathrm{refl}_{\mathrm{base}}$ があったとする。関数 $\mathrm{ap}_f\colon(\mathrm{base}=\mathrm{base})\to(f(\mathrm{base})=f(\mathrm{base}))$ の $\mathrm{ap}$ を $\alpha$ に当てると $\mathrm{ap}_f(\mathrm{loop})=\mathrm{ap}_f(\mathrm{refl}_{\mathrm{base}})$ であり、右辺は $\mathrm{ap}$ の計算規則により $\mathrm{refl}_{f(\mathrm{base})}\equiv\mathrm{refl}_{\mathbf 2}$ である。$\delta$ と合わせて
$$
p=\mathrm{ap}_f(\mathrm{loop})=\mathrm{refl}_{\mathbf 2}
$$
となり、$p\ne\mathrm{refl}_{\mathbf 2}$ に反する。よって $\mathrm{loop}\ne\mathrm{refl}_{\mathrm{base}}$ である。
最後の主張：$S^1$ が集合なら、同じ端点をもつ $\mathrm{loop}$ と $\mathrm{refl}_{\mathrm{base}}$ は等しいので、矛盾する。$\square$
UFP13 の証明は「$\mathrm{loop}=\mathrm{refl}$ ならすべての型が集合になる」ことを経由する。上の証明は宇宙への写像を 1 つだけ使う。さらに、道の合成で $\mathrm{base}=\mathrm{base}$ の型は整数の型と同値になり、$\pi_1(S^1)\cong\mathbb Z$、$n>1$ で $\pi_n(S^1)=0$ が型理論の中で証明される（UFP13 Theorem 8.1.9・Corollary 8.1.10–8.1.11, p. 264。この記事では証明しない）。位相空間の基本群の計算を、点集合位相を使わずに道の帰納法と単一性公理で行う点が HoTT の特徴である。
例と反例
- thm-hott-universe-not-set の証明の道 $p=\mathrm{ua}(e)$ に沿う輸送 $\mathrm{transport}^{X\mapsto X}(p,-)\colon\mathbf 2\to\mathbf 2$ は、$\mathrm{idtoeqv}(p)$ の第 1 成分に等しく、$\mathrm{idtoeqv}(\mathrm{ua}(e))=e$ なので $\mathrm{neg}$ に等しい。等しさ $p$ に沿って「移す」ことが、同値 $\mathrm{neg}$ で移すことになっている。
- 単位型 $\mathbf 1$ は集合である。$\mathbf 1$ の場合分けにより、どの $x,y:\mathbf 1$ についても $(x=y)+\neg(x=y)$ の項 $\mathrm{inl}(\mathrm{refl}_\star)$ が作れて等号が決定可能なので、Martin-Löf型理論 の定理「Hedberg の定理」が使える。
- 円周 $S^1$ は集合でない（thm-hott-loop-nontrivial）が、ループの型 $\mathrm{base}=\mathrm{base}$ は整数の型と同値である（UFP13 Corollary 8.1.10, p. 264）。
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| 単一性公理（thm-hott-universe-not-set） | 反映規則をもつ外延的型理論 | 宇宙が集合でないこと |
| 道の生成元 $\mathrm{loop}$（thm-hott-loop-nontrivial） | 点 $\star$ だけで生成される単位型 $\mathbf 1$ | $\mathrm{refl}$ と等しくないループの存在 |
1 行目：外延的型理論では任意の $q:x=x$ について $q\equiv\mathrm{refl}_x$ となり、すべての型が集合になる（UFP13 Exercise 2.14, p. 104）。このため外延的型理論は単一性公理と両立しない（UFP13 p. 102）。2 行目：$\mathbf 1$ は集合である（例の 2）ので、ループ $q:\star=\star$ はすべて $\mathrm{refl}_\star$ に等しい。円周が単位型と違うのは、道の生成元 $\mathrm{loop}$ をもつことだけである（UFP13 p. 178）。
モデルと集合論との関係
次はこの記事では証明しない。
- 単体的集合のモデル：到達不能基数 $\beta<\alpha$ があれば、単体的集合（Kan複体）の圏の中に、Martin-Löf 型理論の構成をすべてもち、単一性公理を満たす宇宙を 1 つもつモデルがある。したがって、ZFC に到達不能基数を 2 つ加えた体系が無矛盾なら、Martin-Löf 型理論＋単一性公理は無矛盾である（KL18 Theorem 3.4.2–3.4.3, p. 36、Introduction, p. 3）。この記事の構成と公理はすべて Kan 複体のモデルをもち、高次帰納的型のモデルは Lumsdaine と Shulman による（UFP13 p. 11）。
- 集合論の展開：HoTT の中で累積的階層 $V$ を高次帰納的型として作ると、$V$ は外延性などの多くの公理を満たし（UFP13 Theorem 10.5.8, p. 361）、選択公理のもとで ZFC のモデルになる（UFP13 Theorem 10.5.11, p. 363）。ZFC公理系 の節「型から出発する体系」も参照。
関連項目
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
