谷を挟んで向かい合う ２つの学統。一方から他方へ、橋は架かった。逆方向の橋は、いま建設の途上にある。
はじめに
前回の記事では、ホモトピー型理論（HoTT、Homotopy Type Theory）の基本的な発想を追いかけました。
型を空間として、値を点として、等しさを経路（道）として読み替える。すると「等しさ」が階層をなし、$h$-level という番号で整理できるようになる ── そういう話でした。
この記事では、その先を扱います。
「等しさが階層をなす」という現象に気づいたのは、HoTT だけではありませんでした。
「等しさは階層をなす」という現象に、HoTTとはまったく別の流儀で応答した数学の流れが、２０世紀後半から並行して育っています。
そちらの学統は、言語を作り替えるアプローチではなく、既存の数学の中に階層を扱う道具を整えるという戦略が選ばれました。
この記事は、その２つの応答を並べ、それぞれの到達点と両者の間に架けられつつある、かけ橋の建設の努力の現状と今後の展望を眺めます。
前回の記事をお読みでない方にもご理解いただけるように、必要な前提は、その都度ご説明します。
この記事で扱うこと
第１に、「２つの応答」という見取り図を立てます。
第２に、Shulman の定理を扱います。
２つの応答をつなぐ橋にあたる結果です。
前回の記事では補遺で軽く触れるにとどめたので、ここで正面から解説します。
第３に、２種類の等しさを区別します。
前回の記事では扱いきれなかった、しかし極めて重要な区別です。
第４に、もう一方の応答の側で何が起きているかを見ます。
- spectral algebra（スペクトル代数）
- factorization homology（分解ホモロジー）
- 導来代数幾何
- クロマティックホモトピー論。
第５に、範囲を正確に見極めます。
これらの分野で、HoTT が直接使われているわけではありません。
そこを曖昧にしないことが、この記事のいちばんの目的です。
１. ２つの応答
同じ現象に、２つの流儀が生まれた
２０世紀の半ば、圏論という言葉が生まれて数学の見方が整理されていく中で、次のことがはっきりしてきました。
きっかけは、抽象的な研究ではありません。
代数トポロジーや代数幾何といった具体的な分野で、「同じものを、どう同じとみなすか」が繰り返し問題になったことです。
そこから、次の認識が育ちました。
「等しい」という関係は、真か偽かの２択では捉えきれない。
たとえば、２つの群 $G$ と $H$ が同型であるとき、その同型写像は複数ありうる。
「同型である」という事実だけを記録すると、どの同型を使ったかという情報が消えます。
しかし、その情報が本質的な意味を帯びてくる場面があることが気付かれてきました。
そして、同型写像どうしが「同じ」かどうかを問うと、また新しい層が現れる。
それが無限に続く。
この階層に、どう向き合うか。
数学者の間で、こうした問題意識が芽生えてきたのです。
ここで、２つの選択・アプローチが考えられました。
認識された課題を解決するために考案された２つの異なるアプローチ（応答） を紹介します。
応答その１ ── 言語を作り替える
ひとつは、数学を書き下す言語そのものを設計し直すという道です。
「等しい」を原始的な概念として据え、その等しさの証拠が複数ありうることを、言語の側に最初から組み込む。
等しさの証拠を「経路（道）」と呼び、経路どうしの等しさをまた経路として扱う。
これが HoTT、そして Univalent Foundations（一価的基礎）です。
Vladimir Voevodsky が２００９年に Univalence Axiom を提唱し、
２０１３年の体系書 "Homotopy Type Theory: Univalent Foundations of Mathematics" で体系化されました。
特徴は、計算機と本質的に結びついている点にあります。
言語として設計されているので、そのまま証明支援系に実装できます。
Coq（現 Rocq）、Agda、Cubical Agda、Lean といった処理系が、この方向を支えています。
応答その２ ── 既存の数学の道具を整える
もうひとつは、数学の言語はそのままにして、階層を扱う道具立てを整備・改良するという道です。
ここで、順序を正しておく必要があります。
この階層を先に発見したのは、こちらの側です。
しかも、HoTTよりも半世紀以上前のこと でした。
きっかけは、ループ空間だった
発見のきっかけは、抽象的な関心ではありません。
目の前にある具体的な問題 でした。
ループ空間という対象があります。
空間 $X$ の中の、ある点から出て同じ点に戻る経路（道）を、すべて集めたものです。
ここには、自然な「掛け算」が入ります。２本の経路を、順につなげばよい。
ところが、この掛け算は、結合律を厳密には満たしません。
３本の経路 $p$、$q$、$r$ をつなぐとき、$(pq)r$ と $p(qr)$ は、経路としては別物です。
前者は前半で $p$ と $q$ を消化し、後半を $r$ に使う。
後者はその逆。
途中の速度配分が違うので、経路として同一ではないのです。
しかし、両者は連続変形で移り合えます。
つまり、経路で結ばれている。
ここで、前回の記事でも見た問いが立ちます。
その変形は、一意でしょうか。
４本の経路 $pqrs$ を考えると、括弧の付け方は ５通りあります。
それぞれを結ぶ変形が複数あり、その変形どうしがまた整合するかを問える。
そして、その階層が無限に続きます。
Stasheff が、階層を書き下した
１９６３年、James Stasheff がこの階層を明示的に構成しました。
$n$ 本の掛け算の整合性を記述する多面体を、各次元ごとに作ったのです。
associahedron（結合多面体）と呼ばれます。
$n = 4$ のときは五角形、$n = 5$ のときは３次元の多面体、という具合に、次元が上がっていきます。
その全体で、「無限に続く整合性」を表現する。これが $A_\infty$-構造 です。
可換律まで含めた版が $E_\infty$-構造 で、Peter May（１９７２年）と Boardman-Vogt（１９７３年）が operad（オペラッド）という枠組みで整備しました。
この記事の後半で扱う $E_\infty$-環の「$\infty$」は、この Stasheff 以来の階層のことです。
そして、圏を高次化する
同じころ、圏論の側でも階層への対応が進みます。
圏（category）という枠組みを高次化し、対象と射だけでなく、射と射の間の射、さらにその上の射・・・という階層を扱えるようにする。
これが 高次圏論、とくに $\infty$-圏論 です。
Boardman-Vogt（１９７３年）や Joyal の基礎づけを経て、Jacob Lurie が２００９年の "Higher Topos Theory"（約９５０ページ）で現代的な基盤を築きました。
そしてその上に、代数を展開する higher algebra（高次代数）、空間の局所と大域を結ぶ factorization homology、代数幾何を拡張する 導来代数幾何 といった分野が積み上がっています。
特徴は、現代数学の主流の一部として発展してきた点にあります。
代数トポロジー、代数幾何、表現論、数理物理
── 既存の分野の問題を解くための道具として育ちました。
「応答その２」という言い方について、補足します。
これは、最初から一つの完成した理論が存在したという意味ではありません。
Stasheff の $A_\infty$-構造、operad、モデル圏、単体的集合、高次圏、$\infty$-トポス、higher algebra ── これらは、それぞれ別の問題から出発した、別々の解決策でした。
それらが後から $\infty$-圏論という共通の言語に集約されていった、というのが実際の経緯です。
この記事では便宜上ひとつの流れとして扱いますが、内実は複数の流れの合流だと捉えてください。
型理論の側は、独立に同じ構造へたどり着いた
ここが、この話でいちばん面白いところだと思います。
型理論の側が階層に行き当たったのは、位相幾何学を輸入しようとした結果ではありません。
Martin Hofmann と Thomas Streicher が１９９０年代に取り組んでいたのは、型理論の内部的な問題でした。
「等しさの証明は、すべて同一とみなしてよいか」
── これを UIP（Uniqueness of Identity Proofs、証明の一意性）と呼びます。
$a = b$ の証明が２つあったとき、その２つは必ず等しいと言えるか、という問いです。
直感的には、当たり前に思えます。
「等しい」という事実は一つだけで、その証明のしかたが違っても、結論は同じはずだ
── そう考えたくなります。
ところが、Martin-Löf の型理論から、UIP は導けないのです。
導けないことを示すには、導けないモデルを一つ作ればよい。
そこで Hofmann-Streicher が構成したのが、型を 亜群（groupoid）として解釈するモデルでした。
亜群 とは、対象と、対象どうしを結ぶ可逆な射からなる構造です。
このモデルの中では、$a = b$ の証拠が複数ありえます。
それゆえに、UIP は成り立たない。
証明終わり
── ここまでが、当初の目的でした。
しかし、その副産物として、決定的な事実が判明 します。
恒等型は、亜群の構造を持っている。
位相幾何学が半世紀かけて見つけた階層 が、まったく別の問いから、そこに現れていたのです。
Steve Awodey と Michael Warren（２００６-２００９年）、
そして Voevodsky（２００９年）は、この一致を「偶然ではない」と見ました。
両者を正面から結びつけたのが、HoTTの出発点です。
全体を一枚の図にすると
ここまでの話を、図にまとめておきます。
以降の節を読むあいだ、この地形を思い浮かべながら進んでください。
読み方は ３つです。
第１に、出発点はひとつです。
いちばん上の「等しさが階層をなす」という現象に、２つの流れが別々に応答しました。
第２に、時期がずれています。
応答その２の側は１９６３年から、応答その１の側は１９９０年代から。
左右の枝で、いちばん上の年が半世紀、時の隔たりがあります。
第３に、２つの枝が合流するのは、いちばん下だけです。
２０１９年の Shulman の結果まで、両者は交わりませんでした。
そして合流した後も、点線で示した逆方向は、まだつながっていません。
年表で見ると
２つの流れの時間差が、はっきり見えます。
| 年 | 出来事 | どちらの流れか |
|---|---|---|
| １９３５年 | Hurewicz、高次ホモトピー群 | 位相幾何学 |
| １９６３年 | Stasheff、$A_\infty$-構造。整合性の無限階層を明示 | 位相幾何学 |
| １９６７年 | Quillen、モデル圏 | 位相幾何学 |
| １９７２年 | May、operad（$E_\infty$） | 位相幾何学 |
| １９７３年 | Boardman-Vogt、$\infty$-圏の基礎づけ | 位相幾何学 |
| １９８３年 | Grothendieck "Pursuing Stacks"、ホモトピー仮説 | 位相幾何学 |
| １９９０年代 | Hofmann-Streicher、亜群モデル | 型理論 |
| ２００６-０９年 | Awodey-Warren、両者の接続 | 型理論 |
| ２００９年 | Lurie "Higher Topos Theory" | 位相幾何学 |
| ２００９年 | Voevodsky、Univalence Axiom | 型理論 |
| ２０１３年 | HoTT Book | 型理論 |
| ２０１９年 | Shulman の定理 ── 両者に橋が架かる | 両方 |
２つは、どう違うのか
並べると、性格の違いが見えます。
| 応答１（HoTT） | 応答２（$\infty$-圏論） | |
|---|---|---|
| 何であるか | 数学を書くための言語・基礎 | 数学の中の道具・理論 |
| 等しさの扱い | 言語に組み込まれた原始概念 | 圏の構造として構成する |
| 計算機との関係 | 本質的（証明支援系と一体） | 補助的（形式化は進行中） |
| 主な担い手 | 型理論・論理学・計算機科学 | 代数トポロジー・代数幾何 |
| 階層に気づいた時期 | １９９０年代 | １９６０年代 |
| 体系の成立 | ２００９-２０１３年 | １９７０年代以降 |
この２つは、長らく交わらずに発展してきました。
しかも、対等ではありません。
片方は半世紀を超える蓄積を持ち、もう片方はまだ１５年ほどの歴史しかない。
半世紀を超える蓄積を持つ学統と、まだ１５年の学統。同じ現象を見ていながら、手元にある道具の量が違う。
同じ現象を見ていながら、使う言葉も、論文の書き方も、評価の基準も違う
── そういう ２つの流れが、別々の場所で育っていたわけです。
両者が同じものを見ていることは、どうすれば確かめられるのか。
Hofmann-Streicher のモデルは、型理論の側に亜群の構造があることを示しました。
しかしそれは、ひとつのモデルの話です。
「型理論の世界と、位相幾何学が育ててきた $\infty$-圏論の世界とは、どういう関係にあるのか」という問いには、まだ答えが出ていませんでした。
そして２０１９年、その問いに答える結果が現れます。
２つの流れをつなぐ橋が、ここで架かることになります。
２. Shulman の結果 ── HoTT は、どこまで通用する言語なのか
ここまで、HoTT が「等しさを経路（道）として扱う言語」であることを見てきました。
すると、次の問いが立ちます。
この言語は、どこで通用するのでしょうか。
日本語が日本で通じ、英語が英語圏で通じるように、数学の言語にも「通じる場所」があります。HoTT で書いた議論が意味を持つのは、どういう場所なのか。
この問いに、２０１９年、Michael Shulman が答えを与えました。
まず「トポス」とは何か
答えを述べる前に、トポス（topos）という言葉を説明しておきます。
耳慣れない言葉だと思いますが、発想そのものは難しくありません。
私たちがふだん数学をするとき、土台には集合があります。
集合の要素を取り、写像を作り、部分集合を考える。
これが標準的な舞台です。
しかし、「集合と同じように振る舞うが、集合そのものではない世界」 というものが存在します。
たとえば、次のようなものです。
-
時間とともに変化する集合 ── 各時刻ごとに集合があり、時刻が進むと写像でつながっていく
-
場所ごとに違う集合 ── 空間の各点の近傍ごとに集合が決まっていて、重なる部分では貼り合う（層、sheaf と呼ばれます）
- 観測者ごとに違う集合 ── ある群の作用を持つ集合の全体
これらはいずれも、集合ではありません。
しかし、集合でできる操作のほとんどが、そのままできます。
- 直積を取る
- 写像の集まりを考える
- 部分対象を考える
こうした 「集合のように振る舞う世界」 を、まとめて トポス と呼びます。
１９６０年代に Grothendieck が代数幾何のために導入し、
その後 Lawvere と Tierney が公理的に整理しました。
この図の読み方
「ひとつの標準的な世界（集合）と、それとは違うが同じように振る舞う ３つの世界」
── これを、中央に本館、周囲に ３つの別館が建つ ローマの学堂として描きました。すべて同じ設備を備えているが、中身の原理が違うという構図です。
- 中央の本館「集合」 ── 標準的な舞台としての集合
- 同じ様式の ３別館 ── 集合と同じように振る舞うが、集合そのものではない世界
- 時間で並ぶ祠の列 ── 時間とともに変化する集合
- 重なりを綴じ合わせた礼拝堂 ── 場所ごとに違う集合（層・sheaf）
- 観測者像が円周に並ぶ館 ── 観測者ごとに違う集合（群の作用）
- 共通の設備アイコン ── 直積・写像・部分対象 ── 同じ操作ができる
- 全体を囲む門「TOPOS」 ── これらをまとめてトポスと呼ぶ
トポスには、それぞれの「内部言語」がある
トポスについて、重要な事実があります。
それぞれのトポスの中で、論理を展開できるのです。
「$x$ について、ある性質 $P(x)$ が成り立つ」といった主張を、トポスの内部で書き下し、証明できます。
このとき使う論理を、そのトポスの 内部言語（internal language）と呼びます。
ここで面白いのは、内部言語が、ふつうの論理とは少し違うことです。
多くのトポスでは、排中律（どんな命題も、真か偽かのどちらかである）が成り立ちません。
「$P$ でない、ということはない」から「$P$ である」を導けないのです。
こうした論理を 直観主義論理（intuitionistic logic）と呼びます。
つまり、こういうことです。
１-トポスの内部言語は、直観主義的な高階論理である。
トポスの中で数学をしたければ、この言語で書けばよい。
逆に、この言語で書いたことは、どのトポスでも意味を持つ。
トポスと論理の関係を、もっと詳しく
「トポスを選ぶと論理が決まる」という関係については、次の記事で詳しく扱っています。古典論理と直観主義論理がどこで分かれるのか、トポス以外にどんな「器」がありうるのかまで踏み込んだ内容です。
トポスと論理の関係 ── ひとつのトポス（数学の宇宙）を選ぶと、なぜ古典論理か直観主義論理が決まるのか ── そして、トポス以外の「器」たち
また、論理が一つではないという事実そのものを主題にした記事もあります。量子論理や圏論的量子力学まで視野に入れた地図です。
∞-トポスはその高次版
さて、ここからが本題です。
トポスは「集合のように振る舞う世界」でした。
では、「集合ではなく、空間のように振る舞う世界」 を考えたらどうなるでしょうか。
点があり、点と点を結ぶ経路（道）があり、経路と経路をつなぐ変形があり・・・と階層が続く世界。
前回の記事で見た、HoTT の型が持っていた構造です。
こうした世界を $\infty$-トポス（infinity-topos）と呼びます。
正確には Grothendieck $(\infty,1)$-トポス です。
Jacob Lurie が２００９年の "Higher Topos Theory" で体系的に整備しました。
現代の代数トポロジー、導来代数幾何、高次圏論の共通の舞台になっています。
ここで、自然とある期待が芽生えてきました。
１-トポスの内部言語が直観主義論理であるように、$\infty$-トポスの内部言語は HoTT なのではないか。
そのような期待です。
構造が、あまりにもよく対応しているからです。
| 世界 | 内部言語 | |
|---|---|---|
| 集合の一般化 | １-トポス | 直観主義的な高階論理 |
| 空間の一般化 | $\infty$-トポス | $HoTT$？ |
なぜ、それが自明でなかったのか
しかし、この期待が満たされるのかどうかを確かめるのは、容易なことではありませんでした。
立ちはだかったは、厳密さの食い違いにあります。
型理論では、ある種の等式が厳密に成り立つことを要求します。
たとえば、型を作る操作を２回行った結果が、文字どおり同じものになる、といった具合です。
ところが $\infty$-圏の側では、同じになるのは「同値なところまで」 です。
厳密に等しいわけではありません。
この食い違いを、一貫性の問題（coherence problem）と呼びます。
型理論の要求する厳密な等式を、$\infty$-トポスの側でどう実現するのか。
ここが、長らく解けなかった難所でした。
上図の読み方
「片方は厳密な一致を要求し、もう片方は同値までしか保証しない」
── この立場の隔たりを、継ぎ目がぴたりと合うことを要求する石工と、ずれても橋として通じればよしとする石工の対比として表現しました。両者の石を接ごうとして、わずかな隙間が埋まらない。そんな情景です。
期待が満たされるかを確かめるのは、容易ではなかった。立ちはだかったのは、厳密さの食い違いである。
型理論は、ある種の等式が厳密に ── 文字どおり同じものになることを要求する。
ところが ∞-圏の側では、同じになるのは「同値なところまで」で、厳密に等しいわけではない。
この食い違いを一貫性の問題（coherence problem）と呼ぶ。
型理論の要求する厳密な等式を、∞-トポスの側でどう実現するか ── ここが、長らく解けなかった難所だった。
Shulman が示したこと
２０１９年にShulmanがやってのけたのは、 この難所を解決したことです。
論文の題は "All (∞,1)-toposes have strict univalent universes" です。
示されたのは、次のことです。
任意の Grothendieck $(\infty,1)$-トポスは、strict univalent universes を持つホモトピー型理論を解釈する Quillen モデル圏によって表示できる。
言葉が多いので、順に解きほぐします。
「表示できる」（presented by）とは、そのトポスを具体的な形で書き下せる、ということです。
$\infty$-トポスは抽象的な対象で、そのままでは扱いにくい。
そこで、モデル圏という、より具体的な道具を使って表現します。
写真を撮るように、抽象的な対象の具体的な姿を取り出す
── そういうイメージです。
「HoTT を解釈する」 とは、そのモデル圏の中で、HoTTの規則がすべて成り立つということです。
型を作る、経路を作る、Univalence を使う ── これらの操作が、すべて意味を持ちます。
"strict univalent universes" の "strict" は、先ほどの一貫性の問題への回答です。
型理論が要求する厳密な等式が確かに実現されている、という意味になります。
まとめると、次のようになります。
任意の Grothendieck $(\infty,1)$-トポスは、HoTT を解釈する適切なモデル圏によって表示できる。
直感的な言い方をすれば、どんな $\infty$-トポスについても、それを HoTT で記述できるモデルを選べる、ということです。
なお、「そのトポスの内側で HoTT がそのまま動く」という言い方は、少し強すぎます。
示されたのは、トポスを表示するモデル圏が HoTT を解釈するということであり、モデル圏というステップを一段挟んでいる点は、押さえておいてください。
橋は架かった。しかし、通れるのは片方向だけである。
開通 $ホモトピー型理論 → ∞-圏論$。HoTT で証明したことは、どの ∞-トポスでも正しい（健全性、Shulman ２０１９年）
通行止め $∞-圏論 → ホモトピー型理論$。∞-トポスで成り立つことが、すべて HoTT で証明できるかは未解決（完全性、内部言語予想）
分かりやすく言い換えると、以下になります。
$\infty$-トポスの世界では、２つのものの関係は「同値」── ほぼ同じ、変形すれば移り合える ── というところまでしか言えません。
「これとこれは文字どおり等しい」と確定できる場面が、ほとんどないのです。
ところが、計算や証明を進めるには、「これはこれと等しい」と確定させ、一方を他方に置き換える操作が要ります。それができないと、議論が前に進みません。
モデル圏とは、「これはこれと等しい」と確定させ、一方を他方に置き換える操作を可能にする舞台です。
$\infty$-トポスと同じ内容を保ったまま、対象と射のあいだに厳密な等式が定まるよう組み直したもの。その上でなら、通常の計算や証明ができます。
ここで、当然の疑問が生じます。
厳密な等式を後から定めるなら、都合よく作ったものではないのか、という疑念です
その疑念はあたりません。
モデル圏で等しいとされるのは、元の $\infty$-トポスで同値だったものに限られます。
何を同値とみなすかは、扱う対象の構造によってはじめから決まっているからです。
コーヒーカップとドーナツが位相幾何学で「同じ」なのは、両者の穴の数が同じだからで、誰がやっても答えは変わりません。
モデル圏は、この動かせない事実を、計算できる形に移し替えているだけです。
だから、モデル圏の上で導いた結論は、$\infty$-トポスの世界の事実とずれません。これが、この舞台を経由してよい理由です。
では、モデル圏は、どうやってこの移し替えをするのでしょうか。
やっていることは、同値なもののそれぞれについて、「代表」をひとつ選ぶことです。
$\infty$-トポスでは、「$a$ も $b$ も $c$ も、みな同値」という状態が普通にあります。
どれも「同じようなもの」ですが、少しずつ違う。だから「どれと等しいのか」が決まらず、置き換えができませんでした。
そこでモデル圏は、同値な仲間のなかから、扱いやすいものをひとつ代表に選ぶ規則を用意します。
$a$ も $b$ も $c$ も、同じ代表に置き換える。
すると、みな同じ代表になるので、今度は文字どおり「等しい」と言えます。
等しいと言えれば、一方を他方に置き換えて計算できます。
分数と同じです。
$\frac{2}{4}$ も $\frac{3}{6}$ も、約分すれば $\frac{1}{2}$ というひとつの姿になります。
この「約分した姿」が代表です。
約分してしまえば、同じ $\frac{1}{2}$ どうし、記号ごと一致して計算に使えます。
そして、誰を代表に選ぶかは、恣意的に決められるものではありません。
約分の仕方が分数の性質から一通りに決まっているのと同じで、代表の選び方も、対象の構造から決まっています。
だから、都合よく作った代表ではないのです。
以上が、同値だったものを厳密な等式に直して計算できるようにする仕組みです。
同値なものを共通の代表に置き換えることで、厳密に等しいものへと変える。
── それが、モデル圏のしていることです。
何が言えて、何が言えないのか
ここは、この記事を通じて最も注意していただきたい箇所です。
Shulman が示したのは、片方向の議論です。
「$a$ と $b$ は等しい」といった主張について、次の２つは、本来は別のことです。
ひとつは、HoTTの規則に従って、その主張を証明できること。
もうひとつは、その主張が $\infty$-トポスという対象について、実際に成り立っていることです。
「規則で導ける」ことと「本当に成り立つ」ことは、いつも一致するとは限りません。
そこで、２つの向きを問えます。
HoTTで証明できたことは、$\infty$-トポスで本当に成り立つのか。 これが成り立つ性質を、健全性（soundness）と呼びます。
証明した結論が、必ず本当に成り立つ
── その言語が、嘘を証明しない、ということです。
逆に、$\infty$-トポスで成り立つことは、すべてHoTTで証明できるのか。
これが成り立つ性質を、完全性（completeness）と呼びます。
本当に成り立つことに、証明の取りこぼしがない、ということです。
上記の健全性と完全性のうち、Shulman が示したのは、健全性のほうだけです。
つまり、HoTT で証明したことは、どの $\infty$-トポスでも正しい。
HoTTで定理をひとつ証明すれば、それが無数の $\infty$-トポスすべてで通用するということです。
「一度書けば、どこでも通用する」に近い、強力な性質です。
一方、完全性のほうは、まだ分かっていません。
$\infty$-トポスで成り立つことが、すべて HoTT で証明できるのか？
── この問いは未解決です。
「HoTT は $\infty$-トポスの内部言語である」という主張を 内部言語予想（internal language conjecture）と呼びますが、これは今日も証明されていません。（2026年7月20日現在）
この予想の出どころについて
この着想を最初に述べたのは Steve Awodey で（２００９-２０１０年）、続いて André Joyal が２０１１年に、より具体的な形で予想として提示しました。
そのため Awodey の予想（Awodey's conjecture）とも呼ばれます。
現在の精密な定式化は、Kapulkin-Lumsdaine（２０１８年）によるものです。
歴史的経緯を追われる方は、この線をたどってください。
なお、Awodey は第１節で触れた Awodey-Warren（２００９年）── 型理論とホモトピー論を最初に正面から接続した仕事 ── の著者でもあります。この予想は、その接続の延長線上にあります。
論文の要旨も、「HoTT を $\infty$-トポスの内部的推論のための形式言語として使える」と述べるにとどまっています。「内部言語である」とは言っていません。
表にすると、こうなります。
| 主張 | 状況 | |
|---|---|---|
| 健全性 | HoTT で証明できることは、$\infty$-トポスで正しい | Shulman が証明（２０１９年） |
| 完全性 | $\infty$-トポスで正しいことは、HoTT で証明できる | 未解決 |
図にすると、向きの違いがはっきりします。
実線の矢印は通れます。点線の矢印は、通れるかどうかが分かっていません。
この記事のタイトルに「片側車線のみ開通済み」と書いたのは、この状態のことです。
用語について、ひとつ断っておきます。
ここでいう「健全性」「完全性」は、論理学で単一のモデルに対して使う通常の意味とは、完全には同じではありません。
ここでは、「HoTT の証明が、どの対象のクラスまで通用するか」という意味で、直感的にこの言葉を用いています。厳密な定式化にご関心のある方は、Shulman の論文の序節をご覧ください。
一般向けの解説では、この２つが混同されることがあります。「HoTT は $\infty$-トポスの内部言語であることが証明された」と書かれていれば、それは正確ではありません。
この結果が持つ意味
留保を置いたうえで、それでもこの結果は重要です。
理由は２つあります。
第１に、HoTT の適用範囲が確定しました。
HoTT は、単体的集合という特定のモデルの上でだけ通用する言語ではありませんでした。現代数学の主要な舞台である $\infty$-トポス全体で使える言語だと分かったのです。
第２に、証明が持ち運べるようになりました。
$\infty$-トポスは、分野ごとに違うものが使われます。代数トポロジーで使うもの、導来代数幾何で使うもの、それぞれ別です。
しかし HoTT で証明を書いておけば、どの $\infty$-トポスへ持って行っても通用します。
前回の記事で紹介した Blakers-Massey の定理が、まさにこの経路をたどりました。HoTT の中で見つかった新しい証明が、任意の $\infty$-トポスで通用することが判明し、古典的な定理よりも一般的な形の定理として発表されたのです。
「２つの応答」との関係
冒頭で述べた「２つの応答」の話に戻ります。
言語を作り替える道（HoTT）と、既存の数学の中で道具を整える道（$\infty$-圏論）
── この２つが、Shulmanによってつながりました。
HoTT で書いたことは、$\infty$-トポスで通用する。
$\infty$-トポスは、higher algebra や導来代数幾何の舞台です。
しかし、higher algebra や factorization homology を研究している数学者の大半は、HoTTを使っていません。
higher algebra や factorization homology を研究している数学者の大半は、$\infty$-圏論の標準的な道具で仕事をし続けているのです。
橋は架かった。しかし、その橋を渡って行き来する人は、まだ多くない ── それが現状です。
これは、単に彼らが HoTT を知らないからではありません。 原理的な理由を含む、いくつかの本質的な事情があります。その中身は、この記事の第５節でまとめて扱います。
３. 二種類の等しさ
Shulman の結果を正確に理解するために、ひとつ補っておかねばならない区別があります。
前回の記事では、扱いきれなかった論点です。
型理論の等しさは、ひとつではない
前回、「等しさは経路（道）である」と書きました。
これは正しいのですが、半分だけです。型理論には、性質の違う２つの等しさがあります。
判定的等しさ（judgmental equality、定義的等しさとも）── $a \equiv b$ と書きます。
これは「定義に従って計算すれば、文字どおり同じものになる」という等しさです。たとえば $2 + 2$ と $4$ は、計算すれば同じ形に行き着きます。機械がその場で判定できる、厳密な等しさです。
命題的等しさ（propositional equality）── $a = b$ と書きます。
これは「等しいことの証明（経路）が存在する」という等しさです。
前回の記事で扱ってきたのは、こちらでした。
diff で考える
プログラマの方には、次の比喩が分かりやすいと思います。
２つのファイルが「同じ」とは、どういうことでしょうか。
diff をかけて、１バイトも違わない。これが判定的等しさです。バイト列が文字どおり一致する。機械が、その場で判定できます。
しかし、もうひとつの「同じ」があります。中身のバイト列は違うが、開くとまったく同じ画像が表示される２つのファイル。圧縮形式だけが違う PNG のような場合です。
diff では「違う」と出ます。しかし、見た目は同じ。これが命題的等しさです。「同じだと示す手続きが存在する」ということであって、バイト列としては厳密には等しくない。
HoTT が扱う等しさは、本質的に後者です。 そして、$\infty$-圏論が扱う「同値」も、やはり後者です。
先ほど述べた一貫性の問題は、この２つの層の食い違いから生じます。
型理論が判定的等しさを要求する箇所で、$\infty$-圏の側は命題的等しさしか提供できない
── そういうずれです。
公理を足すと、計算が止まる
ここで、有名な事件が起きます。
Univalence Axiom を、ただの「公理」として型理論に付け加えると、計算が止まってしまうのです。
canonicity（正準性）が壊れる、と言います。
canonicity とは、「閉じた項は、必ず標準形まで計算できる」という性質です。たとえば、型 $ℕ$ の閉じた項は、必ず具体的な数字まで簡約されるべきです。
ところが、Univalence を公理として足すと、この性質が失われます。
証明は書けます。型チェックも通ります。しかし、その証明を使って実際に計算を走らせると、項が簡約されずに固まってしまう。
プログラマの方には、生々しい話だと思います。コンパイルは通るのに、実行すると値が返ってこないという状況です。
「正しさの証明」と「計算できること」が、ここで裂けるわけです。
Cubical type theory ── 裂け目を縫い合わせる
このギャップは、乗り越えられつつあります。
Cubical type theory（キュービカル型理論）です。Cohen・Coquand・Huber・Mörtberg が２０１６年ごろに構築しました。
発想は、次のようなものです。
等しさの証明（経路）を、抽象的な「区間」からの写像として、構文の中に直接書けるようにする。
前回の記事で、経路を「点と点を結ぶ道」として説明しました。位相空間論では、経路とは区間 $[0, 1]$ からの連続写像のことです。Cubical type theory は、この定義を型理論の構文に持ち込みました。
経路が、絵に描いた餅ではなく、操作できる第一級の対象になったのです。
その結果、Univalence が「公理」ではなく「定理」になりました。 付け足した公理ではなく、体系の中で証明できるものになった。だから、計算が止まりません。
Huber が、自然数についての canonicity ── 閉じた項が、ちゃんと数字まで簡約される ── を証明しています。
これを実装したのが Cubical Agda です。前回の記事で「計算できる Univalence」と紹介したのは、この体系のことでした。
４. もう一方の応答 ── ∞-圏論の側で、何が起きているか
ここからは、応答その２の側を見ていきます。
この節の位置づけを、先に明確にしておきます。
これから紹介する higher algebra、factorization homology、導来代数幾何、クロマティックホモトピー論は、HoTT の応用例ではありません。
$\infty$-圏論が、独立した数学として実際に何を生み出しているかを示す例です。
両者の関係を、あらためて整理します。
- HoTT ── 高次の等しさを、型理論の内部で直接扱う
- $\infty$-圏論 ── 高次の同値と整合性を、数学の道具として扱う
両者は深く関係しますが、この節で紹介する数学が、そのまま HoTT で書かれているわけではありません。 そこを同一視しないことが、この記事の要です。
HoTT が言語を作り替えたのに対し、こちらは既存の数学の中で階層を扱う道具を整えました。その道具で、実際にどんな数学が展開されているのか。
読者にとって最も接続しやすい入口から始めます。
４-１. spectral algebra ── 等しさが緩む代数
可換律が、厳密には成り立たない
高校で習う掛け算では、$ab = ba$ が成り立ちます。可換律です。
行列の掛け算では、これが成り立ちません。$AB \neq BA$ が普通です。
では、その中間はあるでしょうか。
$ab$ と $ba$ は、厳密には等しくない。しかし、両者を結ぶ経路（道）が存在する。
これが、$E_\infty$-環（$E_\infty$-ring、可換環スペクトルとも）という対象の姿です。
整合性が、無限に続く
さらに重要なのは、その先です。
$ab$ と $ba$ を結ぶ経路があるとして、その経路が一意とは限りません。
３つの元 $a, b, c$ があるとき、順序を入れ替える方法は複数あります。$abc \to bac \to bca$ と入れ替えるのと、$abc \to acb \to bca$ と入れ替えるのでは、経路が違う。
その２つの経路が、また経路で結ばれているか。 これを問うと、さらに上の層が現れます。
そしてこの階層が、無限に続きます。
| 層 | 何を問うているか |
|---|---|
| ０層 | 元 $a$、$b$ が存在する |
| １層 | $ab$ と $ba$ を結ぶ経路が存在する |
| ２層 | ２つの入れ替え方が、経路で結ばれている |
| ３層 | その経路どうしが、また経路で結ばれている |
| $\cdots$ | 以下、無限に続く |
「可換律がゆるい環」ではありません
ここは、誤解されやすい箇所なので、正確に述べます。
$E_\infty$-環は、「可換律がゆるく成り立つ環」ではありません。
可換律だけを取り出して「厳密ではないが経路がある」と言っているのではないのです。
可換律、結合律、単位元・・・環が満たすべきすべての規則と、それらの間のすべての整合性が、無限の階層として組織化されている対象です。
その組織化を担う道具が、May と Boardman-Vogt が整備した operad（オペラッド）でした。
何がどう整合すべきかを、次元ごとに規定する枠組みです。
$E_\infty$ の「$\infty$」は、単に「無限個のデータがある」という意味ではありません。
すべての層で、整合性が取れているという意味です。
ここが要点です。
なぜ、こんなものを考えるのか
抽象的な遊びに見えるかもしれません。
しかし、必要に迫られて生まれた概念です。
代数トポロジーには、スペクトル（spectrum）という基本的な対象があります。一般のホモロジー・コホモロジー理論を表現する道具です。
スペクトルどうしには、スマッシュ積という掛け算が入ります。
ところが、古典的な枠組み（Boardman の安定ホモトピー圏）では、この掛け算の結合律も可換律も、厳密には成り立ちませんでした。
成り立つのは、ホモトピーを除いてです。
しかも、そのホモトピーどうしの整合性が、無限に続く。
ここでも、ループ空間のときと同じ構図が現れたわけです。
そこで、その階層構造ごと扱う枠組みを作るという方針が取られました。
それが $E_\infty$-環であり、その上に展開される代数が higher algebra（高次代数）です。
なお、ひとつ補足しておきます。
１９９０年代以降、スマッシュ積が厳密に結合的・可換になるようなスペクトルのモデルが構成されました。EKMM（Elmendorf-Kříž-Mandell-May）の $S$-加群、対称スペクトル、直交スペクトルといったものです。
これらの枠組みでは、厳密に可換なモノイドを考えることができます。
しかし、ホモトピー論的に意味のある不変な概念は、依然として $E_\infty$-構造のほうです。
厳密化は技術的に可能でも、本質は無限の整合性にある。
そういう関係になっています。
この記事の冒頭で、Stasheff がループ空間の結合律から無限の階層を書き下した話をしました。
$E_\infty$-環の「$\infty$」は、まさにその階層です。
１９６３年に見つかった構造が、May と Boardman-Vogt の operad を経て整理され、Lurie が "Higher Algebra" という大著（１０００ページを超えます）で体系化しました。半世紀をかけた積み上げです。
この分野は、しばしば brave new algebra（勇敢な新しい代数）とも呼ばれます。
整数環 $ℤ$ よりもさらに基礎的な対象として、球面スペクトル $𝕊$ を据えるという発想からきた呼び名です。
４-２. factorization homology ── 局所から大域へ
問題設定
次に、factorization homology（分解ホモロジー）を見ます。
問いは、こういうものです。
多様体（なめらかに曲がった空間）の上に、代数的な構造が乗っているとする。局所の情報から、大域の情報を復元できるか。
物理の言葉で言えば、「各点での観測量が分かっているとき、空間全体での観測量が決まるか」という問いです。
この節で、ひとつだけ覚えていただければ十分です。
factorization homology とは、局所的な代数のデータを、多様体の全体にわたって「積分」し、大域的な対象を構成する理論です。
以下は、その中身と、そこから何が生まれたかの説明になります。
excision ── 貼り合わせれば決まる
David Ayala と John Francis が、２０１５年の論文 "Factorization homology of topological manifolds"（Journal of Topology 8巻4号 1045-1084頁）で、この理論を公理的に特徴づけました。
鍵になるのが、$\otimes$-excision（テンソル切除） という性質です。
多様体 $M$ を、２つの部分 $N_1$ と $N_2$ に分解し、境界で貼り合わせたとします。このとき、
$M$ 全体の値は、$N_1$ の値と $N_2$ の値を、境界の値の上でテンソル積することで得られる。
つまり、貼り合わせれば決まるということです。
Ayala-Francis が示したのは、この性質が理論を一意に特徴づけるということでした。$\otimes$-excision を満たす対称モノイダル関手は、factorization homology に限られます。
これは、特異ホモロジーにおける Eilenberg-Steenrod 公理の一般化にあたります。特異ホモロジーが Mayer-Vietoris 性質で特徴づけられるように、factorization homology は $\otimes$-excision で特徴づけられる、という構図です。
TQFT が生まれる
Ayala-Francis の論文は、さらに次のことを述べています。
それぞれの理論が、一種の位相的場の理論（TQFT）を生む。
しかも、閉じた多様体だけでなく、一般の多様体の上で観測量が定義できるという形で。
TQFT とは、ひとことで言えば「空間のつながり方を、代数的な対象に翻訳する仕組み」です。Witten が１９８８年に構築し、Atiyah が公理化しました。
ここで、$\otimes$-excision が持つ意味が見えてきます。大域的な観測量が、局所的な観測量によって強い意味で決定される ── これは、場の理論における局所性の数学的な定式化にほかなりません。
TQFT について、詳しくは
TQFT そのものについては、独立した記事で扱っています。Witten の１９８８年の仕事、Atiyah による公理化、コボルディズム、Frobenius 代数、そして Lurie のコボルディズム仮説まで、対話形式で追いかけた地図です。
量子群を、曲面の上で積分する
factorization homology が、抽象的な枠組みにとどまらないことを示す例があります。
David Ben-Zvi、Adrien Brochier、David Jordan による "Integrating quantum groups over surfaces"（Journal of Topology 11巻4号、２０１８年）です。
何をした仕事なのか、順に説明します。
量子群（quantum group）とは、リー環 $\mathfrak{g}$ の普遍包絡環 $U(\mathfrak{g})$ を、パラメータ $q$ で変形した対象です。$U_q(\mathfrak{g})$ と書かれます。
量子群という名前ですが、群ではありません。
正確には、$U_q(\mathfrak{g})$ が変形しているのは群ではなく、リー環 $\mathfrak{g}$ の普遍包絡環 $U(\mathfrak{g})$ です。$q \to 1$ で戻るのも $U(\mathfrak{g})$ であって、群ではありません。
群の対称性を記述する代数を変形したもの ── そう捉えるのが正確です。
表現論と数理物理の交差点にある対象で、結び目の不変量や統計力学の可解模型と深く結びついています。
Ben-Zvi-Brochier-Jordan は、この量子群の加群のなす圏を、曲面の上で「積分」しました。 ここでいう積分が、factorization homology のことです。
得られたのは何か。穴あき曲面の場合、指標多様体を量子化する圏が具体的に構成されます。
指標多様体（character variety）とは、曲面の基本群から、ある群への準同型を集めたものです。曲面上の局所系のモジュライ空間、と言い換えることもできます。幾何学的ラングランズ・プログラムや、Chern-Simons 理論に現れる、重要な対象です。
さらに、この構成から位相的にひねった４次元 $\mathcal{N} = 4$ 超対称 Yang-Mills 理論の一側面が得られる、と論文は述べています。Kapustin-Witten が幾何学的ラングランズのために導入した設定です。
表現論・幾何・数理物理が、一点で交わっています。
そして、この交点を成立させているのが、$\infty$-圏論の道具立てです。量子群の加群の圏を扱うには、圏の間の等しさを厳密な等式ではなく同値として扱わねばならない。まさに、この記事の主題です。
量子論理・量子計算との関係
量子計算の側から圏論に入る道もあります。圏論的量子力学、量子論理、そしてそれらが実際にどこで使われているのかについては、次の記事で扱っています。
量子論理・トポス・圏論的量子力学は何に使うの？ ── 量子コンパイラから量子インターネットまで
また、量子回路の圏論的な記述を、自然言語処理に応用する試みもあります。
４-３. 導来代数幾何 ── 点の重なり方を記憶する
交点をどう数えるか
代数幾何では、方程式で定義される図形を扱います。
ここで、古典的な問題があります。
２つの図形が交わるとき、交点をどう数えるかという問題です。
放物線 $y = x^2$ と直線 $y = 0$ は、原点で接しています。
交点は１個に見えます。
しかし、直線を少し上にずらせば、交点は２個になります。
この場合は、古典的なスキーム論で対応できます。
交点に「２個ぶん」の情報を持たせた、非被約な構造（$k[x]/(x^2)$ に対応するもの）を考えればよい。接している場合については、これで十分です。
問題は、その先にあります。
次元が合わない交差
たとえば、$4$ 次元空間の中で、$2$ 次元の図形と $2$ 次元の図形が交わるとします。
一般の位置にあれば、交点は有限個の点（$0$ 次元）になるはずです。$2 + 2 - 4 = 0$ という計算です。
ところが、２つの図形がうまく交わらず、交わりが $1$ 次元になってしまうことがあります。
次元が「合わない」交差です。
このとき、交点の重複度を素朴に計算すると、正しい答えが出ません。
Jean-Pierre Serre は、正しい重複度が、単なる積ではなく Tor 関手の交代和として書けることを示しました（Tor 公式）。
座標環のテンソル積だけでは足りず、その「高次の補正項」まで足し引きする必要があるのです。
ここで、次の問いが立ちます。
なぜ、補正項を後から足すのか。
最初から、それらを含んだ対象を考えられないのか。
可換環を、$E_\infty$-環に置き換える
導来代数幾何（derived algebraic geometry）の発想は、この問いに対する答えです。
代数幾何の基本的な部品は、可換環です。
図形は、可換環のスペクトルとして定義されます。
この可換環を、$E_\infty$-環に置き換えたらどうなるか。
すると、交わりを取る操作が、テンソル積ではなく導来テンソル積になります。
Serre が補正項として足していた高次の Tor が、最初から対象の中に含まれるのです。
「$0$ 次でどうか」だけでなく、「$1$ 次、$2$ 次、…… でどうか」という情報が、階層として保たれるわけです。
ひとつ注意しておきます。
ここで現れる階層は、前回の記事で扱った $h$-level と、文字どおり同じ構造ではありません。 導来代数幾何の高次情報は、導来関手の次数として現れるものであり、恒等型の階層とは由来が違います。
ただし、「対象そのものだけでなく、対象どうしの関係や、その関係の関係まで情報として保持する」という方向性には、明確な共通点があります。この記事で並べているのは、その方向性の一致です。
Bertrand Toën と Gabriele Vezzosi、そして Lurie が、この分野を建設しました。
なぜ、これが「複数の等しさ」の話なのか
古典的な代数幾何では、交わりは集合（あるいはスキーム）として記録されます。
「この点が交点である」という事実が、そこにある。
導来代数幾何では、それに加えて、「どのように交わっているか」が階層として記録されます。
$0$ 次の情報の上に $1$ 次の情報があり、その上に $2$ 次の情報がある。
これは、前回の記事で扱った Univalence の発想と、同じ方向を向いています。
「同型である」という事実だけでなく、どの同型を使ったかを保持する。
導来代数幾何は、それを幾何の側で行っているわけです。
そして、この階層を扱う土台になっているのが、$E_\infty$-環と $\infty$-圏です。
この記事で見てきた道具が、そのまま使われています。
４-４. クロマティックホモトピー論 ── 素数ごとの階層
spectral algebra の中でも、とくに深い階層構造を扱うのがクロマティックホモトピー論（chromatic homotopy theory）です。
球面のホモトピー群 $\pi_n(S^k)$ の構造を、素数ごとに、さらに「高さ」ごとに分解して調べる分野です。
「クロマティック」（色彩の）という名前は、光をプリズムで分解するように、ホモトピー論の対象を階層に分解することからきています。
この分野の中心にあった予想のひとつが、telescope 予想（望遠鏡予想）でした。
Douglas Ravenel が１９８４年の論文で提出したものです。
２０２３年、Robert Burklund、Jeremy Hahn、Ishan Levy、Tomer Schlank が、この予想の反例を構成しました。
反証されたのは、高さ ２以上の場合です。
高さ ０ と １ では、予想は正しいことが以前から分かっていました。
彼らが示したのは、高さ ２以上において、telescopic な局所化と chromatic な局所化が一致しないということです。
反例の構成には、代数的 $K$-理論が使われました。
２０２３年６月に発表され、１０月にプレプリントが公開されています。
１９８４年から約４０年、未解決だった問題です。
Ravenel の論文に含まれていた予想のうち、最後まで残っていたものでした。
この業績に対し、２０２６年４月、クレイ数学研究所から Clay Research Award が授与されています。
近年のホモトピー論における最大級の成果として、正式に評価されたことになります。
そして、反証の道具として使われたのも、higher algebra の枠組みでした。
４-５. Riehl-Shulman の directed type theory ── 橋を架ける試み
最後に、２つの応答をつなごうとする試みに触れます。
これまで見てきた HoTT では、経路（道）は可逆です。
$a$ から $b$ への経路があれば、$b$ から $a$ への経路もあります。
これは、等しさという関係が対称であることに対応します。
しかし、圏論で扱う射は、可逆とは限りません。*
A$ から $B$ への射があっても、逆向きの射があるとは限らない。
そこで、向きを持った経路を扱う型理論を作れないか、という発想が出てきます。
Emily Riehl と Michael Shulman が、２０１７年の論文 "A type theory for synthetic ∞-categories" で、この方向の体系を提案しました。simplicial HoTT（単体的 HoTT）とも呼ばれます。
この体系では、$\infty$-圏を「外から構成する」のではなく、型理論の中で直接扱えます。
合成的（synthetic）なアプローチと呼ばれる方針です。
なぜ、これが重要なのか。
この記事で見てきた数学 ── factorization homology も、higher algebra も、導来代数幾何も ── は、可逆でない射を本質的に使います。
ところが HoTT の経路は、すべて可逆です。
そのままでは、これらの対象を書き下せません。
directed type theory は、この制約を外そうとする試みです。
成功すれば、２つの応答が本当に一つになりうる。
次節で述べるとおり、ここは HoTT が抱える最も深い制約にあたります。
２０２４年には、Nikolai Kudasov、Emily Riehl、Jonathan Weinberger が、この体系の中で $\infty$-圏の米田補題を形式化しました。
逆方向の橋 ── directed type theory ── は、いま建設の途上にある。
工事が続いているという事実そのものが、この隔たりの深さを物語っています。
ただし、ここにも留保が必要です。
この体系における「有向 Univalence」は、追加の公理として議論されている段階であり、確立した定理ではありません。
上記の米田補題の形式化も、有向 Univalence を使わずに行われています。
橋を架ける作業は、まだ道半ば、橋は建設途中なのです。
５. HoTTの応用範囲の現状確認
ここまで、$\infty$-圏論の側で展開されている数学を見てきました。
これらの分野でHoTT は直接使われていない
spectral algebra、factorization homology、導来代数幾何、クロマティックホモトピー論
── これらを研究している数学者の大半は、HoTT を使っていません。
使っているのは、$\infty$-圏論の標準的な道具です。
Lurie の枠組み、モデル圏、単体的集合、$\infty$-亜群。
証明は、通常の数学の言葉で書かれ、通常の査読を経て発表されます。
Shulman の結果があるにもかかわらず、です。
利用されるに至らない理由
ここで、当然の疑問が出ます。
それは単に、彼らが HoTT を知らないからではないのか。
そうではありません。
Shulman も Riehl も Awodey も、この分野では知られた研究者です。
HoTT Book は大きく報じられ、Voevodsky の名前は代数幾何の側でこそ有名です。
知られていない、ということはありません。
本質的な理由が、いくつかあります。
うち最初の２つは、原理的なものです。
理由１ ── HoTT の型は、$\infty$-亜群であって $\infty$-圏ではない
これが、最も深い理由です。
前回の記事で見たとおり、HoTT の恒等型が与える経路（道）は、すべて可逆です。
$a$ から $b$ への経路があれば、それを逆にたどる経路が必ずあります。
「等しい」という関係が対称であることの、当然の帰結です。
こうした構造を $\infty$-亜群（infinity-groupoid）と呼びます。
射がすべて可逆な、$\infty$-圏の特別な場合です。
なぜ、経路がすべて可逆なのか
これは、HoTT の設計上の都合ではありません。幾何学的な必然です。
第１節の年表で触れた、Grothendieck のホモトピー仮説（１９８３年）を思い出してください。$\infty$-亜群と、位相空間のホモトピー型は、本質的に同じものである ── そう述べる予想でした。
空間の中の経路（道）は、いつでも逆にたどれます。行きがあれば帰りがある。だから、空間のホモトピー型を代数の言葉で書き直したものは、必然的に、すべての射が可逆な構造になる。
HoTT の型を「空間」として読むという第１回の出発点が、ここで制約として跳ね返ってくるわけです。空間を扱うのに適した言語だからこそ、向きのある射を扱えない。 長所と短所が、同じ根から出ています。
ところが、$\infty$-圏の射は、可逆とは限りません。
たとえば、ベクトル空間の圏で、$ℝ^3$ から $ℝ^2$ への線形写像を考えてください。
逆写像は存在しません。しかし、これは立派な射です。
そして、この記事で見てきた数学は、可逆でない射を本質的に使います。
factorization homology は、対称モノイダル $\infty$-圏に値を取ります。
その圏の射は、一般に可逆ではありません。
$E_\infty$-環の加群の圏でも、導来代数幾何の関手圏でも、同じです。
つまり、通常の HoTT が持つ恒等型（経路）だけでは、これらの非可逆な射を直接表現できないのです。
ここは、正確に区別しておきます。
HoTT の中で、圏を定義すること自体はできます。
HoTT Book の第９章は、まさにそれを扱っています。
対象の型と射の型を用意し、合成と恒等射の規則を課せばよい。
さらに「同型な対象は等しい」という条件を満たすものを univalent category（一価的圏）と呼び、圏論の標準的な結果がその中で証明されています。
問題は、$\infty$-圏です。
$1$-圏なら、射の合成が満たすべき等式は有限個です。
しかし $\infty$-圏では、合成の結合律がホモトピーとして成り立ち、そのホモトピーの整合性が無限に続く。
この無限の整合性を、HoTTの内部で書き下す方法が、まだ知られていません。
第３節で見た一貫性の問題が、ここでも立ちはだかるわけです。
「HoTT で書けば $\infty$-トポスで通用する」という Shulman の結果は、確かに成り立ちます。
しかし、$\infty$-トポスの中で $\infty$-圏を扱う議論を、HoTT の内部で展開する道は、まだ開かれていない。
向きを持った射の無限の階層を、可逆な経路の言葉だけで書くことはできないからです。
第４-５節で紹介した Riehl-Shulman の directed type theory は、まさにこの制約を外そうとする試みです。そして、それがまだ完成していないという事実が、制約の深さを物語っています。
理由２ ── HoTT は、ひとつの世界の「内側」の言葉である
もうひとつ、原理的な制約があります。
内部言語とは、ひとつのトポスの内側で語るための言葉です。
そのトポスの中に住んでいる者として、そこにある対象について語る。
ところが、この記事で扱った数学の多くは、世界の外側から語っています。
たとえば、こういう主張です。
「任意の $\infty$-トポス $\mathcal{E}$ と $\mathcal{F}$、およびその間の幾何学的射 $f$ について、…… が成り立つ」
これは、HoTT の内部では述べられません。 「すべてのトポスについて」という量化は、トポスの外側に立たなければできないからです。
$\infty$-トポスどうしを比較する、関手を構成する、複数の世界を行き来する ── 現代の代数トポロジーや導来代数幾何は、こうした操作を日常的に行います。内部言語は、そこに手が届きません。
Shulman の結果自体が、この点を象徴しています。「すべての $\infty$-トポスが HoTT を解釈する」という定理は、HoTT の内部では述べられません。 外側から見て初めて言えることです。
理由３ ── 古典論理を足すと計算が止まる
HoTTは、既定では構成的です。
排中律も選択公理も、初めから入っていません。
しかし、代数トポロジーと代数幾何は、これらを自由に使います。
Zorn の補題で極大イデアルを取る、超限帰納法で構成する、背理法で存在を示す
── 標準的な作法です。
もちろん、HoTT に排中律や選択公理を公理として足すことはできます。
しかし、そうすると canonicity が壊れます。 第３節で見た、Univalence を公理として足したときと同じ現象です。
つまり、こういう状況になります。
HoTT の最大の利点である「計算できる」という性質を捨てなければ、古典的な数学が書けない。
捨ててしまえば、わざわざ HoTT を使う理由が薄れる。
このジレンマは、いまのところ解決されていません。
理由４ ── 積み上げるべき土台が、まだない
現代の数学の定理は、単独では成立しません。
クロマティックホモトピー論で新しい定理を証明するには、その手前に何千という既知の結果が必要です。スペクトルの理論、局所化の理論、Adams スペクトル系列、Morava $K$-理論 ──。
これらは、HoTT の中には、まだほとんど形式化されていません。
つまり、HoTT で新しい定理を証明しようとすると、土台から作り直さねばならないのです。既存の道具を使えば明日にも証明できることが、HoTT では数年がかりの基盤整備から始まる。
これは原理的な障害ではなく、時間の問題です。しかし、実際に研究する者にとっては、決定的な差になります。
理由５ ── 蓄積の量が、圧倒的に違う
冒頭の年表を思い出してください。
Stasheff が１９６３年、May と Boardman-Vogt が１９７０年代前半。
$\infty$-圏論の側には、半世紀を超える定理と技法の蓄積があります。
教科書があり、標準的な道具立てがあり、それを使いこなす研究者が何世代も育っている。
HoTT が体系として成立したのは、２００９年から２０１３年にかけてです。
まだ１５年ほど。
同じ現象を扱えるとしても、手元にある道具の量が違います。
実際に定理を証明したい数学者が、蓄積の厚いほうを選ぶのは、自然なことです。
既存の学統には、半世紀の蓄積がある。橋は架かっているが、そこへ向かう理由が、まだ多くの者にはない。
整理すると
５つの理由を、性格ごとに分けておきます。
| 理由 | 性格 | 将来 |
|---|---|---|
| １. 型が $\infty$-亜群にとどまる | 原理的 | directed type theory が解決を目指す |
| ２. 内部からしか語れない | 原理的 | 内部言語という枠組み自体の制約 |
| ３. 古典論理と計算の両立 | 半ば原理的 | 未解決のジレンマ |
| ４. 土台がまだない | 実務的 | 時間が解決しうる |
| ５. 蓄積の量の差 | 実務的 | 時間が解決しうる |
図にすると、こうなります。
理由３が、２つの群のあいだにあります。
技術的な解決が見つかるかもしれませんし、見つからないかもしれない。
この図では原理的な側に置きましたが、境界上の項目だとお考えください。
理由１と２は、努力で埋まる差ではありません。
HoTT という枠組みそのものの性質から来ています。
一方、理由４と５は、時間の問題です。
形式化ライブラリが充実すれば、状況は変わりうる。
そして理由３は、その中間にあります。
技術的な解決が見つかるかもしれませんし、見つからないかもしれません。
では、２つの応答は無関係なのか
そうではありません。
同じ現象を見ていることは確かです。
等しさが階層をなすという事実に、両者は独立に気づきました。
片方はループ空間の結合律から、もう片方は「等しさの証明は一意か」という問いから
── まったく別の入口から、同じ構造にたどり着いたのです。
この一致は、偶然ではありませんでした。
Shulman の結果が、それを定理として確定させたわけです。
そして、Shulman の結果は、その関係を明確にしました。
少なくとも片方向には、確実な橋が架かっています。
さらに、橋を渡ろうとする試みは続いています。
Riehl-Shulman の directed type theory はその一例です。
$\infty$-圏論を HoTT の内部で展開できれば、２つの応答は本当に一つになるかもしれません。
ただし、それはまだ進行中の研究です。
前回の記事で述べたことの、再確認
前回の記事の冒頭で、次のように書きました。
数論、解析学、確率論といった分野で、HoTT が直接の道具として使われている例は、ほとんどありません。
いま成果が出ているのは、もともとホモトピー論的な構造を持つ領域に集中しています。
この記事で見てきたことは、その内実を具体化したものです。
ホモトピー論的な構造を持つ領域では、確かに豊かな数学が展開されています。
しかしそれは、HoTT が展開したのではなく、$\infty$-圏論が展開したものです。
HoTTの直接的な成果は、前回の記事で挙げた３つ
── Blakers-Massey の一般化、Brunerie の数の計算、構造同一性原理による証明の再利用
が中心です。
この区別を保つことが、この分野を正確に理解する鍵だと考えています。
まとめ
この記事で見てきたことを整理します。
第１に、等しさが階層をなすという現象に、２つの応答が生まれました。
言語を作り替える道（HoTT、Univalent Foundations）と、既存の数学の中に道具を整える道（$\infty$-圏論、higher algebra）。
両者は独立に、しかもまったく別の入口からこの階層にたどり着きました。
位相幾何学の側は、ループ空間の掛け算が結合律を満たさないという問題から。
型理論の側は、「等しさの証明は一意か」という内部的な問いから。
そして、時期が大きくずれています。
Stasheff が階層を書き下したのが１９６３年。
Hofmann-Streicher が亜群モデルを作ったのが１９９０年代。半世紀の差があります。
第２に、２０１９年の Shulman の結果が、両者をつなぎました。
任意の Grothendieck $(\infty,1)$-トポスが、HoTT を解釈するモデル圏で表示できる。
ただしこれは健全性であって、内部言語予想は未解決です。
第３に、型理論には ２種類の等しさがあります。
判定的等しさ（計算して文字どおり同じ）と、命題的等しさ（経路が存在する）。
この区別を踏まえないと、canonicity の問題も、Cubical type theory の意義も理解できません。
第４に、$\infty$-圏論の側では、豊かな数学が展開されています。
$E_\infty$-環では可換律がホモトピーとして成り立ち、その整合性が無限に続く。
factorization homology では、局所の観測量から大域の観測量が決まり、そこから TQFT が生まれる。
量子群を曲面上で積分すると、指標多様体の量子化が得られる。
第５に、これらの分野で HoTT は直接使われていません。
これは、知られていないからではありません。
原理的な理由があります。
HoTT の型は $\infty$-亜群 ── 経路がすべて可逆な構造 ── にとどまります。
しかし、この記事で見てきた数学は、可逆でない射を本質的に使います。
また、内部言語という枠組みは、ひとつの世界の内側からしか語れません。
複数の $\infty$-トポスを比較する議論は、外側に立たなければ書けない。
橋は架かりましたが、渡る人はまだ多くありません。
そして、その橋を広げる作業（directed type theory）が、いま進行中です。
キャプション案
橋は架かった。もう一本は、まだ途上にある。作業は、いまも続いている。
次回に向けて
次の記事では、この記事で扱いきれなかった論点を予定しています。
集合論の限界
── なぜ数学者は新しい基礎を求めたのか。選択公理、連続体仮説、Gödel の不完全性定理を経由して、Univalent Foundations が何を置き換えようとしているのかを扱います。
応用の各論
── スペクトル系列の機械証明、量子プログラミング言語への応用、大規模形式化ライブラリの現状。
分野ごとの温度差
── 数学基礎論、圏論、証明支援系、プログラミング言語理論、数理物理、AI 研究。
それぞれがHoTTをどう受け止めているか。
付録 ── 学部レベルの数学から本記事で取り上げ論文に至る学習ロードマップ
この記事では、２つの学統に属する研究論文を数多く挙げてきました。
では、それらを実際に読めるようになるには、何をどの順に学べばよいのでしょうか。
学部レベルの数学を修めた方に向けて、ひとつの道筋を示します。
全体地図
分かれ道は、圏論の後にあります。 そこまでは共通です。
段階ごとの目安
| 段階 | 内容 | 目安 |
|---|---|---|
| ０ | 学部の数学（線形代数・代数・位相） | 前提 |
| １ | 代数トポロジー | ６か月〜１年 |
| ２ | 圏論 | ３〜６か月 |
| ３-A | 型理論から HoTT へ | ６か月〜１年 |
| ３-B | ホモロジー代数からモデル圏・単体的集合へ | １〜２年 |
| ４-B | $\infty$-圏論・安定ホモトピー論 | １〜２年 |
流派１のほうが、論文に到達するまでが短くなります。
蓄積が浅いぶん、前提として要求される既知の結果が少ないためです。
第５節で述べた「蓄積の量の差」が、学習コストの側からもうかがい知ることができます。
段階１ ── 代数トポロジー
なぜ必要か
この記事に出てきたすべての概念が、ここから育っています。
経路（道）、ホモトピー、ループ空間、そして $A_\infty$-構造。
英語
- Hatcher, A. Algebraic Topology. Cambridge University Press, 2002. 著者サイトで無料公開されており、この分野の事実上の標準です
- May, J. P. A Concise Course in Algebraic Topology. University of Chicago Press, 1999. 簡潔ですが密度が高く、独学より併読向きです
和文
- 田村一郎『トポロジー』岩波書店
- 枡田幹也『代数的トポロジー』朝倉書店
- 西田吾郎『ホモトピー論』紀伊國屋書店
ここで必ず押さえること
- 基本群と、その高次版（高次ホモトピー群）
- ホモロジーとコホモロジー
- ループ空間 $\Omega X$ と、その掛け算が結合律を満たさないこと
最後の項目が、この記事の第１節そのものです。
段階２ ── 圏論
なぜ必要か
── ２つの流派のいずれもが圏論の言葉で書かれています。
ここを飛ばすと、どちらの流派に属す論文も読めこなすことは叶いません。
英語
- Riehl, E. Category Theory in Context. Dover, 2016. 著者サイトで無料公開。現代的で読みやすく、最初の一冊に適します
- Mac Lane, S. Categories for the Working Mathematician. Springer, 2nd ed., 1998. 古典。通読より参照用です
- Leinster, T. Basic Category Theory. Cambridge University Press, 2014. arXiv でも公開されています
和文
- Leinster, T.『ベーシック圏論』（土岡俊介 訳）丸善出版
- Mac Lane, S.『圏論の基礎』（三好博之・高木理 訳）丸善出版
- 圏論の歩き方委員会『圏論の歩き方』日本評論社。各分野の応用が概観できます
ここで必ず押さえること
- 関手、自然変換
- 極限と余極限
- 随伴
- 米田の補題
段階３-A ── 流派１（HoTT）への道
（まず最初に）型理論の基礎
英語
- Nederpelt, R., Geuvers, H. Type Theory and Formal Proof: An Introduction. Cambridge University Press, 2014
- Pierce, B. C. Types and Programming Languages. MIT Press, 2002. 計算機科学寄りですが、依存型の手前までを固められます
和文
- Pierce, B. C.『型システム入門 ── プログラミング言語と型の理論』（住井英二郎 監訳）オーム社
- 清水義夫『圏論による論理学 ── 高階論理とトポス』東京大学出版会
押さえること ── 単純型付きラムダ計算、Curry-Howard 対応、依存型、Martin-Löf 型理論。
（次に読むべきは）HoTT理論の本体
英語
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. 無料公開。この分野の出発点です
- Rijke, E. Introduction to Homotopy Type Theory. arXiv:2212.11082. 教科書として書かれており、演習も豊富です
読み方の助言
── HoTT Book は第１章から順に読むより、第１章・第２章（型と経路）と第６章（高次帰納型）を先に読み、第９章（圏論）と第１０章（集合論）を後回しにするほうが挫折しにくくなります。
（そして、ひたすら）手を動かす
この流派は、読むだけでは身につきません。
証明支援系で実際に書くことが、理解の中心にあります。
-
Agda ──
cubicalライブラリを使うと、計算する Univalence を体験できます -
Rocq（旧 Coq）──
UniMathおよびHoTTライブラリ - Lean 4 ── HoTT そのものではありませんが、証明支援系の作法を学ぶには最も情報が豊富です
和文
- 萩原学、アフェルト・レナルド『Coq/SSReflect/MathComp による定理証明』森北出版
段階３-B・４-B ── 流派２（$\infty$-圏論）への道
こちらは道が長くなります。順に積み上げてください。
ホモロジー代数
英語
- Weibel, C. An Introduction to Homological Algebra. Cambridge University Press, 1994
和文
- 河田敬義『ホモロジー代数』岩波書店
- 志甫淳『層とホモロジー代数』共立出版
押さえること
── 導来関手、Ext と Tor、スペクトル系列。第４-３節の Serre の Tor 公式は、ここの知識が前提です。
モデル圏
英語
- Hovey, M. Model Categories. American Mathematical Society, 1999
- Dwyer, W. G., Spalinski, J. "Homotopy theories and model categories." Handbook of Algebraic Topology, 1995. 短い入門で、無料で読めます
- Quillen, D. Homotopical Algebra. Springer, 1967. 原典
押さえること
── 弱同値、ファイブレーション、コファイブレーション、Quillen 同値。Shulman の定理の「モデル圏で表示できる」が、ここで理解できます。
単体的集合
英語
- Goerss, P., Jardine, J. F. Simplicial Homotopy Theory. Birkhäuser, 1999
- Friedman, G. "An elementary illustrated introduction to simplicial sets." Rocky Mountain Journal of Mathematics, 42(2), 2012. arXiv:0809.4221。図が豊富で、最初の一歩に適します
押さえること ── Kan 複体、幾何学的実現、単体的集合と位相空間の対応。
∞-圏論
英語
- Cisinski, D.-C. Higher Categories and Homotopical Algebra. Cambridge University Press, 2019. 著者サイトで無料公開
- Land, M. Introduction to Infinity-Categories. Birkhäuser, 2021. 教科書として書かれた、比較的新しい入門
- Riehl, E. Categorical Homotopy Theory. Cambridge University Press, 2014. 著者サイトで無料公開
- Lurie, J. Higher Topos Theory. Princeton University Press, 2009. 約９５０ページ。通読するものではなく、参照するものです
読み方の助言
── Lurie に直接向かうと、ほぼ確実に挫折します。Cisinski か Land で全体像をつかんでから、必要な箇所だけ Lurie を引く、という使い方を勧めます。
安定ホモトピー論とスペクトル
英語
- Barnes, D., Roitzheim, C. Foundations of Stable Homotopy Theory. Cambridge University Press, 2020
- Adams, J. F. Stable Homotopy and Generalised Homology. University of Chicago Press, 1974. 古典
- Lurie, J. Higher Algebra. 著者サイトで公開。$E_\infty$-環と higher algebra の標準的な参照先です
押さえること
── スペクトル、スマッシュ積、$E_\infty$-構造、operad。第４-１節が、ここに対応します。
到達点 ── この記事で挙げた論文
段階を踏んだ先に、次の論文が読めるようになります。分野ごとに、入りやすい順に並べます。
意味論・橋
| 論文 | 必要な段階 |
|---|---|
| Hofmann, M., Streicher, T. "The groupoid interpretation of type theory." 1998 | ２、３-A |
| Awodey, S., Warren, M. "Homotopy theoretic models of identity types." 2009 | ２、３-A、３-B（モデル圏） |
| Kapulkin, K., Lumsdaine, P. L., Voevodsky, V. "The Simplicial Model of Univalent Foundations." arXiv:1211.2851 | ３-A、３-B（単体的集合） |
| Shulman, M. "All (∞,1)-toposes have strict univalent universes." arXiv:1904.07004 | ３-A、４-B の全部 |
Shulman の論文が最も要求が高くなります。 型理論と $\infty$-圏論の両方を、それぞれ相当の深さまで必要とするためです。
型理論
| 論文 | 必要な段階 |
|---|---|
| Cohen, C., Coquand, T., Huber, S., Mörtberg, A. "Cubical Type Theory." 2018 | ３-A |
| Riehl, E., Shulman, M. "A type theory for synthetic ∞-categories." 2017 | ３-A、４-B |
| Kudasov, N., Riehl, E., Weinberger, J. "Formalizing the ∞-categorical Yoneda lemma." 2024 | ３-A、４-B |
∞-圏論
| 論文 | 必要な段階 |
|---|---|
| Ayala, D., Francis, J. "A factorization homology primer." Handbook of Homotopy Theory, 2020 | ４-B。この分野への入口として、まずこれを |
| Ayala, D., Francis, J. "Factorization homology of topological manifolds." 2015 | ４-B |
| Ben-Zvi, D., Brochier, A., Jordan, D. "Integrating quantum groups over surfaces." 2018 | ４-B ＋ 表現論・量子群 |
| Toën, B. "Derived Algebraic Geometry." EMS Surveys, 2014 | ４-B ＋ スキーム論 |
| Burklund, R., Hahn, J., Levy, I., Schlank, T. "K-theoretic counterexamples to Ravenel's telescope conjecture." 2023 | ４-B ＋ クロマティック理論 ＋ 代数的 $K$-理論 |
最後の２本は、この記事で挙げた中でも群を抜いて要求が高くなります。 それぞれ、専門として数年を要する分野です。
学習にあたっての助言
第１に、両方を同時に追わないでください。
どちらか一方に絞り、そちらで論文が読める水準まで到達してから、もう一方を見るほうが結果的に速くなります。両者は言葉も作法も違うため、並行すると混乱します。
第２に、無料で読める文献が非常に多い分野です。
Hatcher、Riehl（２冊）、Cisinski、HoTT Book、Rijke、Lurie（２冊）── いずれも著者サイトや arXiv で公開されています。教科書代を理由に踏みとどまる必要はありません。
第３に、流派１は手を動かすことが本体です。
証明支援系で実際に証明を書かないと、何が難しいのかが分かりません。第３節で扱った canonicity の問題も、書いてみて初めて実感できます。
第４に、流派２は「全部を理解してから進む」をやめてください。
$\infty$-圏論の文献は、前提となる既知の結果があまりに多く、順番に完全理解する読み方では進めません。必要になった箇所だけ戻るという読み方が、この分野の標準的な作法です。
第５に、日本語の文献は、段階２までは充実していますが、その先は薄くなります。
代数トポロジーと圏論までは和書で進めますが、モデル圏・$\infty$-圏論・HoTT については、英語文献に移ることを前提に計画してください。
参考文献
Shulman の定理
- Shulman, M. (2019). "All (∞,1)-toposes have strict univalent universes." arXiv:1904.07004.
- Kapulkin, K., Lumsdaine, P. L. (2018). "The homotopy theory of type theories." Advances in Mathematics, 337, 1-38.（内部言語予想の精密な定式化）
階層構造の発見
- Stasheff, J. (1963). "Homotopy associativity of H-spaces, I, II." Transactions of the AMS, 108, 275-292, 293-312.
- May, J. P. (1972). The Geometry of Iterated Loop Spaces. Lecture Notes in Mathematics 271, Springer.
- Boardman, J. M., Vogt, R. M. (1973). Homotopy Invariant Algebraic Structures on Topological Spaces. Lecture Notes in Mathematics 347, Springer.
- Elmendorf, A. D., Kříž, I., Mandell, M. A., May, J. P. (1997). Rings, Modules, and Algebras in Stable Homotopy Theory. AMS.
型理論の側からの発見
- Hofmann, M., Streicher, T. (1998). "The groupoid interpretation of type theory." In Twenty-five Years of Constructive Type Theory, Oxford University Press.
- Awodey, S., Warren, M. (2009). "Homotopy theoretic models of identity types." Mathematical Proceedings of the Cambridge Philosophical Society, 146(1), 45-55.
$\infty$-圏論・higher algebra
- Lurie, J. (2009). Higher Topos Theory. Princeton University Press.
- Lurie, J. (2017). Higher Algebra. 著者ウェブサイトで公開。
factorization homology
- Ayala, D., Francis, J. (2015). "Factorization homology of topological manifolds." Journal of Topology, 8(4), 1045-1084.
- Ayala, D., Francis, J. (2020). "A factorization homology primer." In Handbook of Homotopy Theory, Chapman and Hall/CRC.
- Ben-Zvi, D., Brochier, A., Jordan, D. (2018). "Integrating quantum groups over surfaces." Journal of Topology, 11(4).
導来代数幾何
- Serre, J.-P. (1965). Algèbre locale — Multiplicités. Lecture Notes in Mathematics 11, Springer.
- Toën, B., Vezzosi, G. (2008). "Homotopical algebraic geometry II: geometric stacks and applications." Memoirs of the AMS, 193(902).
クロマティックホモトピー論
- Burklund, R., Hahn, J., Levy, I., Schlank, T. (2023). "K-theoretic counterexamples to Ravenel's telescope conjecture." arXiv:2310.17459.
- Ravenel, D. C. (1984). "Localization with respect to certain periodic homology theories." American Journal of Mathematics, 106(2), 351-414.
- Clay Mathematics Institute (2026). "2026 Clay Research Awards." https://www.claymath.org/news/2026-clay-research-awards/
Cubical type theory
- Cohen, C., Coquand, T., Huber, S., Mörtberg, A. (2018). "Cubical Type Theory: A constructive interpretation of the univalence axiom." LIPIcs, 69.
- Vezzosi, A., Mörtberg, A., Abel, A. (2019). "Cubical Agda: A dependently typed programming language with univalence and higher inductive types." ICFP 2019.
directed type theory
- Riehl, E., Shulman, M. (2017). "A type theory for synthetic ∞-categories." Higher Structures, 1(1), 147-224.
- Kudasov, N., Riehl, E., Weinberger, J. (2024). "Formalizing the ∞-categorical Yoneda lemma." CPP 2024.
HoTT の基礎
- The Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study.
付録その２ ── 形式証明の言語を、どう学ぶか
前節の学習ロードマップで、**「証明支援系で実際に書くこと」**を流派１の中心に据えました。
しかし、ここには現実的な壁があります。
第１に、和書がほとんどありません。 数えるほどしか出ていません。
第２に、実務で使う機会に乏しいのです。 業務でこれらの言語を書く職場は、日本にはごく限られます。学んでも使う場がないという状態になりがちです。
第３に、どこから入ればよいのかが分かりません。 論理学をどこまで学べば始められるのか、どの言語をどの順に学べばよいのか、その目安が示されていません。
この節では、これらに順に答えます。
この主題については、別記事を準備しています。
学部生のタロウくんと、形式手法を専門とする新しい専任講師との対話篇として、証明支援系の学び方をより詳しく扱う予定です。この節は、その予告を兼ねた要約とお考えください。
論理学は、どこまで学べば始められるのか
いちばん多い誤解から解きます。
論理学を体系的に修めてから証明支援系に入る、という順序は必要ありません。
むしろ、それをやろうとして途中で力尽きる方が多い。数理論理学は、それ自体が広大な分野です。完全性定理、不完全性定理、モデル理論、集合論の独立性証明 ── これらを一通り学ぼうとすれば、それだけで年単位になります。
そして、その大半は、証明支援系を使うのに必要ありません。
必要なのは、これだけです
| 項目 | 必要か | 理由 |
|---|---|---|
| 命題論理の記号が読める | 必須 | 記号が読めないと、画面の表示が読めません |
| 述語論理（一階）の量化子 | 必須 | $\forall$ と $\exists$ は、証明支援系の中核です |
| 自然演繹の推論規則 | 必須 | これが、そのまま操作に対応します |
| 直観主義論理と古典論理の違い | 必須 | 排中律が使えるかどうかが、体系ごとに違います |
| Curry-Howard 対応 | 強く推奨 | 「証明はプログラムである」という発想の核心です |
| 完全性定理の証明 | 不要 | 使う分には知らなくて構いません |
| 不完全性定理 | 不要 | 教養としては面白いのですが、実作業には出てきません |
| モデル理論 | 不要 | 意味論を研究する段階になってからで十分です |
| 集合論の独立性証明 | 不要 | 別の話題です |
自然演繹の推論規則が、いちばん重要です。
なぜかというと、それがそのまま、証明支援系の操作になっているからです。
たとえば「$A \to B$ を証明するには、$A$ を仮定して $B$ を導けばよい」という含意の導入規則。これは、Lean や Rocq では intro という操作に、Agda では関数を書くことに、そのまま対応します。
規則を知っていれば、画面で何が起きているかが分かります。 知らなければ、記号の羅列にしか見えません。
目安としては
教科書の第３章あたりまで、と考えてください。
命題論理と述語論理を扱い、自然演繹の規則を一通り見て、健全性・完全性の主張だけを知る。その証明を追い切る必要はありません。
そこまで来たら、証明支援系を触り始めてください。 残りの論理学は、必要になったときに戻ればよいのです。
実際、触り始めたほうが論理学の理解も速くなります。 推論規則を頭で理解するより、機械に怒られながら覚えるほうが、はるかに身につきます。
論理学の教材
和文
- 前原昭二『記号論理入門』日本評論社。薄く、記号の読み方から入れます。最初の一冊に適します
- 小野寛晰『情報科学における論理』日本評論社。計算機科学向けで、直観主義論理と型理論への接続まで扱います。この分野に進むなら、ここが最も近い一冊です
- 戸次大介『数理論理学』東京大学出版会。丁寧で、証明を追いたい方向け
- 萩谷昌己、西崎真也『論理と計算のしくみ』岩波書店。論理と計算の対応に重心があります
- 野矢茂樹『論理学』東京大学出版会。哲学寄りですが、記号に慣れる導入としては読みやすい
和文はこの段階までは充実しています。 困るのは、この先です。
英語
- van Dalen, D. Logic and Structure. Springer, 5th ed., 2013. 標準的な教科書
- Girard, J.-Y., Lafont, Y., Taylor, P. Proofs and Types. Cambridge University Press, 1989. 無料公開。Curry-Howard 対応を扱った古典で、薄いのに密度が高い
- Sørensen, M. H., Urzyczyn, P. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006. 対応そのものを主題にした一冊
どの言語を、どの順に学ぶか
ここが、いちばん助言の欲しいところだと思います。結論から書きます。
推奨する順序
第１段階 ── Lean 4 から始める
第２段階 ── 目的に応じて分岐する
- HoTT に進みたい → Agda（
cubical） - プログラム検証に進みたい → Rocq（旧 Coq）
第３段階 ── 別の視点を得る
- Idris 2 ── 型で設計するという発想
- Isabelle/HOL ── 自動化の威力と、依存型でない体系
順に理由を述べます。
なぜ Lean 4 から始めるのか
理由は言語設計の優劣ではありません。始めやすさと、続けやすさです。
第１に、Natural Number Game があります。
ブラウザで動くゲーム形式の入門教材です。インストール不要で、自然数の性質を証明しながら操作を覚えられます。この分野で、これほど参入障壁の低い入口は他にありません。
証明支援系の学習で最大の脱落要因は、環境構築と最初の一週間です。ここを跳ばせることの価値は、他のどんな長所よりも大きい。
第２に、Mathlib があります。
現代数学を形式化した巨大なライブラリで、線形代数、位相空間、測度論、圏論、数論まで揃っています。**「証明したいことの前提が、もう証明されている」**状態から始められます。
他の言語では、まず前提から自分で作ることになります。
第３に、コミュニティが最も活発です。
これが、実は最も重要かもしれません。
この分野は、詰まったときに検索してもほぼ何も出てきません。 利用者の絶対数が少ないので、記事も回答も存在しない。独学の難易度が突出して高いのは、このためです。
Lean Zulip では、初心者の質問にも丁寧な回答がつきます。質問できる場所があるかどうかが、続くかどうかを決めます。
なぜ、Lean だけでは足りないのか
ここは、この記事の主題と直接つながる、重要な技術的事実です。
Lean 4 では、HoTT ができません。
言語の未成熟さではなく、型理論の設計そのものによる制約です。
Lean の等式 Eq は Prop という宇宙に住んでいます。そして Lean のカーネルは、Prop に対して証明の非関係性（proof irrelevance）を定義的に持っています。同じ命題の ２つの証明は、文字どおり同じものとして扱われる、という設計です。
これは、UIP（等しさの証明の一意性）が成り立つということです。
第１回の記事で述べたとおり、UIP と Univalence は両立しません。 Univalence が成り立てば、等しさの証明は複数ありうる。UIP が成り立てば、それらは常に同一。両方は言えません。
つまり、Lean を極めても、HoTT の入口には立てません。 道が違います。
（かつて Lean 2 には HoTT モードがありましたが、Lean 3 以降は廃止されています。）
HoTT に進みたいなら、Agda か Rocq に移る必要があります。
これは Lean の欠点ではありません。Lean は、古典数学の形式化に最適化された道具です。Mathlib は排中律も選択公理も自由に使います。数学者が現に使っている数学を形式化する、という目的には、これが正しい設計です。
目的が違うので、道具が違う。 それだけのことです。
第２段階の分岐
HoTT に進むなら ── Agda
--cubical オプションを付けた Cubical Agda が、計算する Univalence が実際に動く、最も成熟した環境です。第３節で扱った内容を手元で確かめることができます。
Agda には、もうひとつ独自の価値があります。
それは、穴を掘りながら書くという開発様式です。
「穴」というのは、この分野の術語です。
Agda では、証明の途中でまだ書けていない箇所を ? として残すことができます。
その ? を、穴（hole）と呼びます。
プログラミングの TODO コメントに似ていますが、決定的に違う点があります。
Agda が、その穴の中身を教えてくれるのです。
穴にカーソルを合わせると、こう表示されます。
Goal: x + zero ≡ x
————————————————————————
x : ℕ
上の行が「いま、ここで作るべきものの型」。
下の行が「そのために、手元で使えるもの」です。
何を作ればよく、何が使えるのか
── そのふたつを、処理系のほうから示してくれます。
そして穴をひとつ埋めると、次の穴が現れます。
それを埋めると、また次の穴が現れる。
証明の全体を頭の中で組み立ててから書き下すのではなく、穴を掘り進めながら対話的に育てていくという進め方になります。
この感覚は、Lean のタクティクとも Rocq とも違います。
そして、Curry-Howard 対応を体で理解するには、最も適した様式だと思います。
書いているうちに、自分が証明を構成しているのか関数を書いているのか、区別がつかなくなってくるからです。
証明の途中を ? として残すと、Agda がその場所で「いま何が使えて、何を作ればよいか」を教えてくれます。
対話しながら証明を育てる感覚は、Lean のタクティクとも Rocq とも違い、Curry-Howard 対応を体感するには最も適しています。
agda-unimath という、HoTT で数学を形式化するライブラリも育っています。
プログラム検証に進むなら ── Rocq
Software Foundations という全６巻の無料教材があります。
この分野の金字塔で、論理、プログラミング言語理論、コンパイラ検証までを一気通貫で扱います。
Rocq は最も歴史が長く、産業実績も最大です。
CompCert（検証済み C コンパイラ）が代表例になります。
Rocq でも HoTT はできます。
HoTT ライブラリと UniMath が、この上で開発されています。
HoTT と検証の両方に興味があるなら、Rocq という選択も合理的です。
ただし、構文とタクティク言語（Ltac）に独特の癖があり、Lean 4 に比べると学習の初速は落ちます。
だからこそ、Lean で証明の習慣をつけてから来るほうが楽になります。
Idris 2 の、独自の価値
Idris は、証明支援系というより、依存型を持った実用プログラミング言語として設計されています。
そのため、他の言語では得られない発想が身につきます。
「証明を書く」のではなく、「型で仕様を表現する」という感覚です。
長さを型に持つ配列、状態遷移を型で縛るプロトコル、リソースの解放漏れを型が防ぐ設計です。
証明を後から付けるのではなく、型を設計した時点で誤りが書けなくなるという発想です。
さらに Idris 2 は、量的型理論（Quantitative Type Theory）を採用しており、「この値は０回しか使わない」「ちょうど１回使う」といった線形性を型で表現できます。
実行時に消える証明と、残る値を、型が区別します。
業務のコードに、この発想だけを持ち帰ることができます。
Idris そのものを使わなくても、型で設計するという習慣はどの言語でも効果を発揮すると思われます。
順番としては、Lean か Agda で依存型に慣れた後が良ろしいかと思います。
最初に触ると、プログラミング言語としての側面に気を取られ、型理論の核心が見えにくくなります。
Isabelle/HOL の、独自の価値
Isabelle は、そもそも依存型ではありません。
高階論理（HOL）に基づいており、系譜が違います。
そのため、HoTTへの道にはつながりません。
しかし、別の理由で触る価値があります。
その価値とは、自動化の威力です。
Isabelle の Sledgehammer は、外部の自動定理証明器を並列で呼び出し、証明を探してきます。
この分野で最も強力な自動化で、「機械が証明を見つけてくる」とはどういうことかを体感できます。
Lean や Rocq を先に学んでいると、その差に驚くはずです。
逆に、Isabelleから入ると「証明支援系とはこういうものだ」と誤解しかねません。
もうひとつ、Archive of Formal Proofs という巨大な形式証明の集積があり、seL4 マイクロカーネルの完全検証という、産業応用の最大級の実績があります。
大規模検証の現場を知りたいなら、ここが最も近いと思います。
各言語の特徴一覧
| 言語 | 論理の基盤 | HoTT | 強み | 推奨学習順位 |
|---|---|---|---|---|
| Lean 4 | 依存型（Prop は証明非関係） | 不可 | Mathlib、Natural Number Game、コミュニティ | １番目 |
| Agda | 依存型 |
可（cubical） |
穴を掘る開発様式、計算する Univalence | ２番目（HoTT 志向） |
| Rocq | 依存型 |
可（HoTT、UniMath） |
Software Foundations、産業実績 | ２番目（検証志向） |
| Idris 2 | 依存型＋量的型理論 | 積極的には扱わない | 型による設計、線形性 | ３番目 |
| Isabelle/HOL | 高階論理 | 不可（体系が違う） | Sledgehammer、大規模検証実績 | ３番目 |
「HoTT 不可」の２つは、欠点ではありません。
目的が違うだけです。
この記事の文脈では区別が重要なので、敢えて明記しました。
主要な教材
いずれも無料で、質が高いものばかりです。
この分野の教材事情は、和書の少なさに反して、英語圏では極めて恵まれています。
Lean 4
- Natural Number Game ── ブラウザで動くゲーム形式の入門。インストール不要。最初の一歩として、これ以上のものはありません
- Theorem Proving in Lean 4 ── 公式の教科書。無料
- Mathematics in Lean ── 数学の形式化に特化した教材。無料
- Lean Zulip ── 公式コミュニティ
Agda
- Programming Language Foundations in Agda（PLFA）── Wadler ほか。無料。Agda で論理と型理論を学ぶなら、まずこれです
- Cubical Agda のドキュメント ── HoTT に進むなら、ここが入口になります
-
agda-unimath── HoTT による数学の形式化ライブラリ。読むだけでも学べます
Rocq（旧 Coq）
- Software Foundations ── Benjamin Pierce ほか。全６巻の無料教材。この分野の金字塔です
- Chlipala, A. Certified Programming with Dependent Types. MIT Press, 2013. 無料公開。中級以上向け
- 萩原学、アフェルト・レナルド『Coq/SSReflect/MathComp による定理証明』森北出版。数少ない和書のひとつです
Idris 2
- Brady, E. Type-Driven Development with Idris. Manning, 2017
Isabelle/HOL
- Nipkow, T., Klein, G. Concrete Semantics. Springer, 2014. 無料公開
実務で使う機会がないという問題
これは悩ましいですが、避け難い事実です。
日本に居住し、日々働いている中で、これらの言語を業務で書く機会は非常に限られます。
学んでも使う場がないまま忘れる。
よくある末路です。
対処法を４つ挙げます。
第１： 小さな自作課題を作る
「業務で使う」機会が訪れることを待たないでください。
リストの反転を２回すると元に戻る。
ソートの結果が整列している。
二分探索木の挿入が不変条件を保つ。
こうした小さな命題を、自分で立てて証明します。
地味ですが、この分野の実力は、ここでしか育ちません。
教材を読むだけでは、まったく身につかないという点で、他の技術と大きく違います。
第２： 既存の証明を壊して、直す
ライブラリから証明をひとつ持ってきて、途中の一行を消してみてください。
エラーが出た場所が、その一行が担っていた役割です。
読むだけでは見えない構造が、コードを壊すことで見えてきます。
第３： ライブラリに貢献する
Mathlib、agda-unimath、Software Foundations
── いずれもオープンです。
いきなり定理を証明する必要はありません。
誤字の修正、証明の短縮、コメントの追加から始めることができます。
レビューを受けることで、独学では得られない指摘がもらえます。
第４： コミュニティに入る
繰り返しになりますが、質問できる場所を確保してから始めてください。
Lean Zulip、Agda のメーリングリスト、Rocq の Discourse。
これらが、学習継続の成否の分かれ目です。
学習の順序（まとめ）
３つ、強調しておきます。
第１に、点線です。 論理学の続きは、必要になってから戻ればよい。先に全部やろうとしないでください。
第２に、分岐です。 Lean だけを極めても、HoTT には届きません。Univalence を扱いたいなら、Agda か Rocq へ移る必要があります。
第３に、自作の命題を証明する段階を飛ばさないでください。 教材を読み通しただけでは、この分野の力はつきません。ここだけは、代わりがありません。
Lean 4 を勧める理由と留保
前項で挙げた ３つの利点のうち、実際にいちばん効くのはコミュニティです。
Natural Number Game も Mathlib も大きな長所ですが、決定的なのは「詰まったとき、聞ける場所があるか」でしょう。
この分野は、検索してもほぼ何も出てきません。 利用者の絶対数が少なすぎて、記事も回答も存在しないのです。独学の脱落率が突出して高いのは、教材の質のためではなく、この孤立のためだと考えています。
Lean Zulip は、そこが例外的に機能しています。初心者の質問にも、丁寧な回答が返ってきます。
別の順序にも利点があります
公平を期して、Lean から始めないほうがよい場合を挙げておきます。
Curry-Howard 対応を体で理解したいなら、Agda が優れています。
Lean のタクティクは、証明を「操作の列」として書きます。便利ですが、「証明はプログラムである」という核心が、かえって見えにくくなる面があります。
Agda で ? を掘りながら関数を書いていると、自分が証明を構成しているのか関数を書いているのか、区別がつかなくなってきます。その混乱こそが、Curry-Howard 対応の理解そのものです。
型理論そのものの理解を目的にするなら、Agda を最初に置く順序には、十分な理があります。
プログラム検証が目的なら、Rocq から入るのも合理的です。
Software Foundations は、教材としての完成度が、この分野で群を抜いています。全６巻を通せば、論理・プログラミング言語理論・検証が、一続きの道として身につきます。
教材の質だけで選ぶなら、Rocq でしょう。
それでもLeanを最初に薦める理由
この記事の読者は、HoTT に興味を持たれた方だと想定しています。数学寄りの関心をお持ちで、証明支援系そのものは未経験、という方が多いのではないでしょうか。
その場合、最初の一週間を越えられるかどうかが、最大の関門になります。
環境構築でつまずき、最初の証明が通らず、そのまま離れてしまう ── この分野で最もよくある挫折の形です。
Natural Number Game でブラウザから始められることの価値は、他のどの長所よりも大きいと考えています。
そして、Lean で証明を書く習慣がついた後に Agda や Rocq へ移るのは、逆順よりもずっと楽です。 タクティクの操作感を先に身につけておくと、他の体系でも「いま何を作ろうとしているのか」が見えるようになります。
留意点
ここまでの判断は、筆者が把握している範囲での見立てです。
とくに Lean コミュニティの活発さについては、状況が変わりうるものです。また、日本語圏に限れば、Coq のほうが情報の蓄積は厚いかもしれません。
順序はあくまで目安として受け取っていただき、ご自身の目的と、実際に触れてみた感触で選び直してください。 どれから始めても、この分野に入れることに変わりはありません。