ホモトピー型理論

かつて、内包型理論における型とその同一性型を群状体とみなすという考えは、数学的な俗説であった。この考えが意味的に初めて厳密にされたのは、1994年のマルティン・ホフマンとトーマス・シュトライヒャーの論文「群状体モデルは同一性証明の一意性を否定する」^{[ 2 ]}であり、彼らは内包型理論が群状体の圏にモデルを持つことを示した。これは、型理論の最初の真の「ホモトピー的」モデルであったが、「1次元」に過ぎなかった（集合の圏における従来のモデルはホモトピー的に0次元であった）。

彼らの後続論文^{[ 3 ]}は、ホモトピー型理論におけるその後のいくつかの発展を予見していた。例えば、彼らは群状モデルが「宇宙拡張性」と呼ばれる規則を満たすことを指摘した。これは、 10年後にウラジーミル・ヴォエヴォツキーが提案した一価性公理の1型への制限に他ならない。（ただし、1型の公理は、 「同値性」の一貫した概念を必要としないため、定式化が著しく簡単である。）彼らはまた、「同型性を等号とする圏」を定義し、高次元群状モデルでは、そのような圏に対して「同値性は等号である」と予想した。これは後にベネディクト・アーレンス、クシシュトフ・カプルキン、マイケル・シュルマンによって証明された。^{[ 4 ]}

内包型理論の最初の高次元モデルは、2005 年にSteve Awodeyと彼の学生 Michael Warren によってQuillen モデル圏を使用して構築されました。これらの結果は、Warren が「内包型理論のホモトピー モデル」というタイトルの講演を行った FMCS 2006 会議^{[ 5 ]}で初めて公開されました。この講演は、彼の学位論文の概要としても機能しました (出席した学位論文委員会は Awodey、Nicola Gambino、Alex Simpson でした)。概要は、Warren の学位論文の概要の要約に含まれています。^{[ 6 ]}

2006年にウプサラ大学で開催されたアイデンティティ型に関するワークショップ^{[ 7 ]}では 、内包型理論と因子分解システムの関係について2つの講演が行われた。1つはリチャード・ガーナーによる「型理論のための因子分解システム」^{[ 8 ]}、もう1つはマイケル・ウォーレンによる「モデル圏と内包的アイデンティティ型」である。関連するアイデアは、スティーブ・アウォディによる「高次元圏の型理論」とトーマス・ストライヒャーによる「アイデンティティ型と弱いオメガ群：いくつかのアイデアといくつかの問題」の講演で議論された。同じ会議で、ベンノ・ファン・デン・ベルクは「弱いオメガ圏としての型」と題した講演を行い、後にリチャード・ガーナーとの共同論文の主題となったアイデアの概要を述べた。

高次元モデルの初期の構築はすべて、依存型理論のモデルに典型的な整合性の問題に対処する必要があり、さまざまな解決策が開発されました。そのような解決策の1つは2009年にVoevodskyによって、もう1つは2010年にvan den BergとGarnerによって提示されました。^{[ 9 ]} Voevodskyの構成に基づいて構築された一般的な解決策は、最終的に2014年にLumsdaineとWarrenによって提示されました。^{[ 10 ]}

2007年のPSSL86で^{[ 11 ]} 、Awodeyは「ホモトピー型理論」というタイトルの講演を行った（これはAwodeyが造語したこの用語の最初の公的な使用例である^{[ 12 ]} ）。AwodeyとWarrenは、 2007年にarXivプレプリントサーバーに投稿され^{[ 13 ]} 、2009年に出版された論文「同一性型のホモトピー理論的モデル」で彼らの結果をまとめた。より詳細なバージョンは、2008年にWarrenの学位論文「構成的型理論のホモトピー理論的側面」に掲載された。

ほぼ同時期に、ウラジーミル・ヴォエヴォツキーは、数学の実践的な形式化のための言語の探索という文脈で、独自に型理論を研究していた。2006年9月、彼はTypesメーリングリストに「ホモトピーラムダ計算に関する非常に短いメモ」^{[ 14 ]}を投稿し、依存積、和、宇宙を持つ型理論と、この型理論のKan単体集合のモデルの概要を示した。このノートは「ホモトピーλ計算は（現時点では）仮説的な型システムである」という記述で始まり、「現時点では、私が上で述べたことの多くは推測のレベルにある。ホモトピー圏におけるTSモデルの定義でさえ自明ではない」という記述で終わっている。これは、2009年まで解決されなかった複雑な整合性の問題を指している。このノートには、パス空間によってモデル内で解釈されると主張された「等価型」の構文的定義が含まれていたが、ペル・マルティン＝レーフの同一性型に関する規則は考慮されていなかった。また、宇宙をサイズに加えてホモトピー次元によって階層化していたが、このアイデアは後にほとんど放棄された。

構文面では、ベンノ・ファン・デン・ベルクは2006年に、内包型理論における型の同一性型の塔は、マイケル・バタニンの言う「球状代数的」な意味でのω-圏、実際にはω-群圏の構造を持つはずだと推測した。これは後にファン・デン・ベルクとガーナーが論文「型は弱いω-群圏である」（2008年発表）^{[ 15 ]}で、またピーター・ラムズデインが論文「内包型理論からの弱いω-圏」（2009年発表）および2010年の博士論文「型理論からの高次圏」^{[ 16 ]でそれぞれ独立に証明した。}

単価ファイブレーションの概念は、2006 年初頭に Voevodsky によって導入されました。^{[ 17 ]} しかし、Martin-Löf 型理論のすべての説明が、空のコンテキストでは同一性型が反射性のみを含む可能性があるという性質を主張していたため、Voevodsky は、これらの同一性型が単価宇宙と組み合わせて使用​​できることを 2009 年まで認識しませんでした。特に、既存の Martin-Löf 型理論に公理を追加するだけで単価性を導入できるという考えは、2009 年になって初めて現れました。^{[ a ] [ b ]}

また、2009年にヴォエヴォツキーはカン複体における型理論モデルの詳細をさらに解明し、普遍的なカンファイブレーションの存在が型理論の圏論的モデルにおける整合性の問題を解決するために利用できることを指摘した。彼はまた、AKバウスフィールドのアイデアを用いて、この普遍的なファイブレーションが単葉であることを証明した。すなわち、ファイバー間のペアワイズホモトピー同値の関連ファイブレーションは、基底のパス空間ファイブレーションと同値である。

ヴォエヴォツキーは、ユニバレンスを公理として定式化するために、「f は同値である」という文を表す型が（関数外延性の仮定の下で）（-1）切断（つまり、存在する場合は縮約可能）であるという重要な性質を持つ「同値性」を構文的に定義する方法を見つけた。これにより、ホフマンとストライヒャーの「宇宙外延性」を高次元に一般化して、ユニバレンスの構文的記述を与えることができた。また、同値性と縮約性の定義を用いて、証明支援系Rocq（以前はCoqとして知られていた）で「合成ホモトピー理論」の重要な部分を開発し始めた。これが後に「Foundations」、最終的には「UniMath」と呼ばれるライブラリの基礎となった。^{[ 19 ]}

様々な研究の流れが統合され始めたのは、2010年2月にカーネギーメロン大学で行われた非公式の会合で、ヴォエヴォツキーがカン複体における自身のモデルと、ロクの自身のバージョンを、アウォディ、ウォーレン、ラムズデイン、ロバート・ハーパー、ダン・リカタ、マイケル・シュルマンらを含むグループに発表した時だった。この会合では、圏論における同値を随伴同値に改善するという考え方に基づき、すべてのホモトピー同値が（ヴォエヴォツキーの言う「良いコヒーレントな意味において」）同値であるという証明の概要が（ウォーレン、ラムズデイン、リカタ、シュルマンによって）示された。その後まもなく、ヴォエヴォツキーは、一価性公理が関数外延性を意味することを証明した。

次の重要な出来事は、 2011年3月にオーバーヴォルファッハ数学研究所で開催された、スティーブ・アウォディ、リチャード・ガーナー、ペル・マーティン＝レーフ、ウラジミール・ヴォエヴォツキーが主催した「構成的型理論のホモトピー解釈」と題されたミニワークショップでした。^{[ 20 ]}このワークショップのCoqチュートリアルの一環として、アンドレイ・バウアーはヴォエヴォツキーのアイデアに基づいて（ただし、彼のコードは実際には使用せずに）小さなCoqライブラリを作成しました^{[ 21 ]}。これが最終的に「HoTT」Coqライブラリの最初のバージョンの核となりました^{[ 22 ]}（後者の最初のコミット^{[ 23 ]}はマイケル・シュルマンによるもので、「アンドレイ・バウアーのファイルに基づいて開発され、多くのアイデアはウラジミール・ヴォエヴォツキーのファイルから取られている」と記されています）。オーバーヴォルファッハ会議から生まれた最も重要なものの1つは、ラムズデイン、シュルマン、バウアー、ウォーレンによる高次帰納型の基本概念でした。参加者はまた、単一性公理が正準性を満たすかどうか（いくつかの特殊なケースは肯定的に解決されているものの、まだ未解決です^{[ 24 ] [ 25 ]}）、単一性公理に非標準モデルがあるかどうか（シュルマンによって肯定的に回答されています）、(半)単体型をどのように定義するか（2つの等価型を持つ型理論であるヴォエヴォツキーのホモトピー型システム（HTS）では可能ですが、MLTTではまだ未解決です）など、重要な未解決問題のリストを作成しました。

オーバーヴォルファッハのワークショップの後まもなく、ホモトピー型理論のウェブサイトとブログ^{[ 26 ]}が開設され、この分野はその名前で普及し始めた。この期間の重要な進歩の一部は、ブログの履歴から知ることができる。^{[ 27 ]}

HoTTは、型理論の「命題を型として扱う」解釈を修正したバージョンを採用しており、それによれば、型は命題を表すことができ、項は証明を表すことができる。しかし、HoTTでは、標準的な「命題を型として扱う」場合とは異なり、「単なる命題」が特別な役割を果たす。これは大まかに言えば、命題的等価性を除いて、項が最大で1つしかない型である。これらは、証明とは無関係であるという点で、一般的な型よりも従来の論理命題に近い。

ホモトピー型理論の基本概念はパスです。HoTTでは、型は${\displaystyle a=b}$は、その地点からのすべてのパスのタイプです。${\displaystyle a}$要点を言うと${\displaystyle b}$（したがって、点の証明は${\displaystyle a}$1ポイントに等しい${\displaystyle b}$地点からの経路と同じものです${\displaystyle a}$要点を言うと${\displaystyle b}$.) 任意の時点で${\displaystyle a}$タイプのパスが存在する${\displaystyle a=a}$等号の反射的性質に対応する。 タイプのパス${\displaystyle a=b}$反転させて、タイプのパスを形成できます${\displaystyle b=a}$等号の対称性に対応する。 2 つのパス${\displaystyle a=b}$応答${\displaystyle b=c}$連結して、次のタイプのパスを形成できます。${\displaystyle a=c}$これは等号の推移律に対応する。

最も重要なのは、経路が与えられた場合${\displaystyle p:a=b}$、そして何らかの性質の証明${\displaystyle P(a)}$証明は経路に沿って「転送」することができる${\displaystyle p}$その性質の証明を与える${\displaystyle P(b)}$（言い換えれば、型 のオブジェクト）${\displaystyle P(a)}$型のオブジェクトに変換できます${\displaystyle P(b)}$これは等式の代入性質に対応します。ここで、HoTTと古典数学の重要な違いが現れます。古典数学では、2つの値の等式が成立すると、${\displaystyle a}$そして${\displaystyle b}$設立されました、${\displaystyle a}$そして${\displaystyle b}$その後は、両者の区別を気にすることなく、互換的に使用できます。ただし、ホモトピー型理論では、複数の異なる経路が存在する可能性があります。${\displaystyle a=b}$また、物体を2つの異なる経路に沿って輸送すると、2つの異なる結果が得られます。したがって、ホモトピー型理論において置換特性を適用する際には、どの経路を使用しているかを明示する必要があります。

一般的に、「命題」には複数の異なる証明が存在する可能性がある。（例えば、すべての自然数という型を命題とみなした場合、すべての自然数が証明となる。）命題に証明が1つしかない場合でも、${\displaystyle a}$経路の空間${\displaystyle a=a}$何らかの点で非自明である可能性がある。「単なる命題」とは、空であるか、自明な経路空間を持つ点が 1 つだけ含まれる型のことである。

人々が書いていることに注目してください${\displaystyle a=b}$のために${\displaystyle Id_{A}(a,b)}$これにより、タイプが残ります${\displaystyle A}$の${\displaystyle a,b}$暗黙的。混同しないでください。${\displaystyle id_{A}:A\to A}$、上の恒等関数を表す${\displaystyle A}$[ ^{c ]​}

2つの機能${\displaystyle f,g:A\rightarrow B}$点ごとの同一視によりホモトピーとなる：^{[ 29 ]： 2.4.1}

${\displaystyle f\sim g:\equiv \prod _{x:A}f(x)=g(x)}$

2つのタイプの等価性${\displaystyle A}$そして${\displaystyle B}$ある宇宙に属する${\displaystyle U}$関数によって定義される${\displaystyle f:A\rightarrow B}$ホモトピーに関する撤回と切断が存在することの証明とともに： ^{[ 29 ]： 2.4.11、2.4.10}

${\displaystyle A\simeq B:\equiv \sum _{f:A\rightarrow B}{\text{isequiv}}(f)}$、 どこ

${\displaystyle {\text{isequiv}}(f):\equiv \left(\sum _{g:B\rightarrow A}(f\circ g)\sim id_{B}\right)\times \left(\sum _{h:B\rightarrow A}(h\circ f)\sim id_{A}\right)}$

以下の一元性公理と合わせて、非循環的な「${\displaystyle \infty }$-同型性」は「同一性」に拡張された。^{[ 37 ]}

${\displaystyle A\simeq B:\equiv {\text{f:A\leftrightarrows B:g\ {\text{が存在し、}\ g\circ f\simeq id_{A}\ {\text{および}\ f\circ g\simeq id_{B}} が成り立つ}$

上記のように同値関係となる関数を定義することで、パスを同値関係に変換する標準的な方法が存在することを示すことができる。言い換えれば、次のタイプの関数が存在する。

${\displaystyle (A=B)\to (A\simeq B),}$

これは、型を表します${\displaystyle A,B}$等しいものは、特に同等でもある。

単価性公理によれば、この関数はそれ自体が同値である。^{[ 29 ] : 115 [ 18 ] : 4–6} したがって、次のようになる。

${\displaystyle (A=B)\simeq (A\simeq B)}$

「言い換えれば、同一性は等価性と同値である。特に、『等価な型は同一である』と言うことができる。」^{[ 29 ]： 4}

マルティン・ヘッツェル・エスカルドは、一価性の性質がマルティン・レーフ型理論（MLTT）とは独立していることを示した。^{[ 18 ]： 6 [ d ]} これは、型等価性が型理論のすべての構成と互換性があるためである^{[ 29 ]： 2.6-2.15}。

支持者たちは、HoTTによって数学的証明をコンピュータ証明支援のためのコンピュータプログラミング言語に以前よりもはるかに簡単に変換できると主張している。彼らは、このアプローチによってコンピュータが難しい証明を検証できる可能性が高まると主張している。^{[ 38 ]} しかし、これらの主張は普遍的に受け入れられているわけではなく、多くの研究活動や証明支援はHoTTに基づいていない。

HoTTは、論理数学命題の等価性をホモトピー理論に関連付ける一価性公理を採用しています。${\displaystyle a=b}$これは、2つの異なる記号が同じ値を持つという数学的命題である。ホモトピー型理論では、これは記号の値を表す2つの形状が位相的に同値であることを意味する。^{[ 38 ]}

ETHチューリッヒ理論研究所所長のジョバンニ・フェルダー氏は、これらの同値関係はホモトピー理論の方が包括的であるため、より適切に定式化できると主張している。ホモトピー理論は「a が b に等しい」理由だけでなく、その導出方法も説明する。集合論では、この情報を別途定義する必要があり、支持者たちは、それが数学的命題をプログラミング言語に変換することをより困難にすると主張している。^{[ 38 ]}

2015年現在、ホモトピー型理論における一価性公理の計算挙動をモデル化し、形式的に分析するための集中的な研究作業が進行中である。^{[ 39 ]}

立方体型理論は、ホモトピー型理論に計算的な内容を与えようとする試みの一つである。

しかし、半単体型などの特定のオブジェクトは、厳密等価性の概念を参照せずに構築することはできないと考えられています。そのため、パスを尊重するファイブラント型と、そうでない非ファイブラント型に型を分割するさまざまな2レベル型理論が開発されてきました。デカルト立方体計算型理論は、ホモトピー型理論に完全な計算解釈を与える最初の2レベル型理論です。^{[ 40 ]}