Homotopy Type Theory｜ホモトピー型理論
1. 誰が開発したのか？
HoTTは2000年代後半から2010年代初頭にかけての共同研究の成果で、中心人物は以下の2名です。
- ウラジーミル・ヴォエヴォドスキー (Vladimir Voevodsky):フィールズ賞受賞者。数学の基礎をより強固に、かつコンピュータで扱える形にするため、単価性（Univalence）の概念を導入しました。
- スティーブ・アウディ (Steve Awodey):カーネギーメロン大学の哲学者・論理学者。型理論の「同一性（Identity type）」が、ホモトピー論における「パス（Path）」の構造を持つことを発見しました。
2012年から2013年にかけて、プリンストン高等研究所（IAS）に世界中の数学者が集まり、共同で『The HoTT Book』を執筆したことで、一つの学問分野として確立されました。
2. どのような先行定理・理論を踏襲しているか？
HoTTは、全くのゼロから生まれたわけではなく、以下の3つの大きな流れを統合しています。
- マーティン＝レーフの型理論 (Martin-Löf Type Theory):1970年代に提案された、数学の証明をプログラムとして扱うための枠組み。HoTTの直接的な「言語」にあたります。
- カリー＝ハワード同型対応 (Curry-Howard Correspondence):「証明」と「プログラム」、「論理式」と「型」が同じものであるという原理です。
- ホモトピー論と高次カテゴリ論:空間の連続的な変形を扱う幾何学。特に、Quillenのモデル圏や、Grothendieckの「追求（Pursuing Stacks）」などの幾何学的な洞察が、型理論の抽象的な構造と一致することが判明しました。
3. なぜ開発されたのか？（開発の動機）
主な動機は「数学の公理性証明困難の克服」です。
- 数学の巨大化と複雑化:現代数学の証明はあまりに長く複雑になり、人間が査読するだけではミスを防げない限界に来ていました。
- 既存の集合論（ZFC）の限界:従来の集合論はコンピュータで扱うには不向きで、また「同型な構造を同一視する」という機能性を直接記述できませんでした。
- 構成的数学の実現:「存在する」というなら、その「作り方（プログラム）」も示すべきだという構成主義的な立場を、幾何学のレベルまで拡張しようとしました。
4. どのような発展のあるPostulate（要請）なのか？
HoTTの核心は、単価性公理 (Univalence Axiom) という新しい公理系を導入したことにあります。
単価性公理の内容
簡略化して書くと以下のようになります：
(A = B) ≃ (A ≃ B)
（型 A と型 B が等しいことと、それらが同型であることは、同値である）
この公理がもたらす発展
- 構造輸送の自動化:一度「自然数」について証明した定理を、それと同型な別のデータ構造（例えばバイナリ表現）に対して、改めて証明することなく「等しいから」という理由で自動的に適用できます。
- 高次帰納型 (Higher Inductive Types, HITs):点だけでなく、「道（パス）」や「面」を定義に含む新しいデータ型を作れます。これにより、円周や球体といった図形を「プログラムの型」として直接定義できるようになりました。
- 数学のデジタル化:CoqやAgdaなどの言語を用いることで、数学の教科書を丸ごと「実行可能なプログラム」として記述し、100%の正確性を保証する道が開かれました。