Homotopy Type Theory

Martin-Löf type theory [Mar75] の Hofmann と Streicher [HS98] による groupoid model を元に, model category などのホモトピー論的概念を駆使した, 数理論理学の一般化 (?) が盛んに研究されるようになってきた。 \((\infty ,1)\)-category も使われている。 このような分野を homotopy type theory と呼ぶようである。 Blog もできている。

解説としては, Pelayo と Warren の [PW] そして, Institute for Advanced Study の The Univalent Foundation Program の作成した本 [Pro] がある。 後者には, リンク付きのスクリーン用, marginの少ない e-book版, そして印刷用と, 3種類のPDFが用意されている。 他にも, Pelayo と Warren の [PW], Rijke の修士論文, この\(n\)-Category Caféの記事で紹介されている Shulman の解説 [Shub] などがある。 Riehl の lecture notes [Rie] もある。

まずはこれらの解説を眺めてみるのがよいだろう。それによると, Hofmann と Streicher の仕事から model category と type theory に関係がありそうだと思ったのは Moerdijk で, 実際の type theory のホモトピー論の言葉による解釈は, Awodey と Warren の共同研究 [AW09] と Voevodsky の研究で独立に与えられたようである。前者は model category, 後者は simplicial set を用いたものらしいが。

Awodey と Warren の解説によると, Voevodsky の simplicial set を用いた formulation の特徴は, “Univalence Axiom” などの additional axiom が成り立つことのようである。

• univalent universe

Voevodsky がこのようなことを始めた動機については, Princeton の Institute for Advanced Study の news letter [Voe14] に書かれている。

Model category を用いた univalent universe の構成は, Cisinski の [Cis] で与えられている。

Voevodsky の考えていることについては Voevodsky のホームページで講演の slide や video, あるいは preprint を見るぐらいしか情報を得る方法はなかった。 Voevodsky が亡くなった後もこのホームページが維持されているのは有り難い。 他にも web 上の情報源はいくつかあるが, それらについては Gavlirovich と Hasson と Kaplan の [GHK] の Introduction を見るとよい。

Homotopy type theory の model としては, Voevodosky らの simplicial set を用いたものが基本的である。Shulman は[Shud; Shuc] で simplicial set の category のある種の diagram の category を用いたものが使えることを示している。また [Shue] では EI category の \((\infty ,1)\)-version で index された diagram を用いることを提案している。

代数的トポロジーの視点からは, Voevodsky の univalent foundation が面白いのは, 空間に関する証明を, ある程度計算機で自動化できる可能性があるという点ではないだろうか。 例えば, Hou は thesis [Hou17] で homotopy theory の mechanization について述べている。 また Shulman の [Shuc] の Introduction に書かれているように, 位相空間や simplicial set 以外の枠組みでホモトピー論を行なうときにも使えるようである。

ホモトピー群も扱える。 例えば, このHomotopy Type Theory の blog post では, \(\pi _1(S^1)\cong \Z \) の formal proof が与えられている。論文としては, Licata と Shulman の [LS] になっている。 Brunerie [Brua; Brub] は \(\pi _4(S^3)\cong \Z /2\Z \) を示している。James construction も扱えるらしい。

コホモロジーについても, Homotopy Type Theory の blog に Shulman が書いている。 Cell complex のコホモロジーに関する Buchholtzと Hou の [BH] もある。

ホモトピー極限については, Avigad, Kapulkin, Lumsdaine の [AKL15] で扱われている。

このblog post によると, Eilenberg-Mac Lane space も扱える ようになったらしい。

連結な spectrum は Buchholtz, van Doorn, Rijke の [BDR] で考えられている。

Hou, Finster, Licata, Lumsdaine [Hou+] は, Blakers-Massey theorem の “mechanized proof” を発見したと言っている。

ただし, このような homotopy theory と homotopy type theory の関係には色々注意すべきところがあるようで, Shulman が [Shua] の Introduction で詳しく述べている。

Arndt と Kapulkin [AK]は, この手のことを行なうための model category の条件を公理化し, logical model categoryという概念を導入している。

• logical model category

Cranch [Cra] は \((\infty ,1)\)-category を homotopy type theory に導入している。

この \(n\)-Category Caféの記事 によると, Schreiber の800ページ近くある論文 (?) [Scha] は, 数理物理で homotopy type theory の枠組みを使おうとしているものらしい。 より短かいものとして [Schb] が出た。

References

[AK]

Peter Arndt and Chris Kapulkin. Homotopy Theoretic Models of Type Theory. arXiv: 1208.5683.

[AKL15]

Jeremy Avigad, Krzysztof Kapulkin, and Peter Lefanu Lumsdaine. “Homotopy limits in type theory”. In: Math. Structures Comput. Sci. 25.5 (2015), pp. 1040–1070. arXiv: 1304 . 0680. url: https://doi.org/10.1017/S0960129514000498.

[AW09]

Steve Awodey and Michael A. Warren. “Homotopy theoretic models of identity types”. In: Math. Proc. Cambridge Philos. Soc. 146.1 (2009), pp. 45–55. arXiv: 0709.0248. url: http://dx.doi.org/10.1017/S0305004108001783.

[BDR]

Ulrik Buchholtz, Floris van Doorn, and Egbert Rijke. Higher Groups in Homotopy Type Theory. arXiv: 1802.04315.

[BH]

Ulrik Buchholtz and Kuen-Bang Hou. Cellular Cohomology in Homotopy Type Theory. arXiv: 1802.02191.

[Brua]

Guillaume Brunerie. On the homotopy groups of spheres in homotopy type theory. arXiv: 1606.05916.

[Brub]

Guillaume Brunerie. The James construction and \(\pi _{4}(S^3)\) in homotopy type theory. arXiv: 1710.10307.

[Cis]

Denis-Charles Cisinski. Univalent universes for elegant models of homotopy types. arXiv: 1406.0058.

[Cra]

James Cranch. Concrete Categories in Homotopy Type Theory. arXiv: 1311.1852.

[GHK]

Misha Gavrilovich, Assaf Hasson, and Itay Kaplan. The univalence axiom in posetal model categories. arXiv: 1111.3489.

[Hou+]

Kuen-Bang Hou, Eric Finster, Dan Licata, and Peter LeFanu Lumsdaine. A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory. arXiv: 1605.03227.

[Hou17]

Kuen-Bang Hou. “Higher-Dimesional Types in the Mechanization of Homotopy Theory”. Ph.D. Thesis. School of Computer Science, Carnegie Mellon University, Fabruary 2017. url: https://www.math.ias.edu/~favonia/thesis.html.

[HS98]

Martin Hofmann and Thomas Streicher. “The groupoid interpretation of type theory”. In: Twenty-five years of constructive type theory (Venice, 1995). Vol. 36. Oxford Logic Guides. New York: Oxford Univ. Press, 1998, pp. 83–111.

[LS]

Daniel R. Licata and Michael Shulman. Calculating the Fundamental Group of the Circle in Homotopy Type Theory. arXiv: 1301.3443.

[Mar75]

Per Martin-Löf. “An intuitionistic theory of types: predicative part”. In: Logic Colloquium ’73 (Bristol, 1973). Amsterdam: North-Holland, 1975, 73–118. Studies in Logic and the Foundations of Mathematics, Vol. 80.

[Pro]

The Univalent Foundations Program. Homotopy Type Theory: Univalent Fundation of Mathematics. url: http://homotopytypetheory.org/book/.

[PW]

Álvaro Pelayo and Michael A. Warren. Homotopy type theory and Voevodsky’s univalent foundations. arXiv: 1210.5658.

[Rie]

Emily Riehl. On the \(\infty \)-topos semantics of homotopy type theory. arXiv: 2212.06937.

[Scha]

Urs Schreiber. Differential cohomology in a cohesive infinity-topos. arXiv: 1310.7930.

[Schb]

Urs Schreiber. Quantization via Linear homotopy types. arXiv: 1402. 7041.

[Shua]

Michael Shulman. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. arXiv: 1509.07584.

[Shub]

Michael Shulman. Homotopy Type Theory: A synthetic approach to higher equalities. arXiv: 1601.05035.

[Shuc]

Michael Shulman. The univalence axiom for elegant Reedy presheaves. arXiv: 1307.6248.

[Shud]

Michael Shulman. Univalence for inverse diagrams, oplax limits, and gluing, and homotopy canonicity. arXiv: 1203.3253.

[Shue]

Michael Shulman. Univalence for inverse EI diagrams. arXiv: 1508. 02410.

[Voe14]

Vladimir Voevodsky. The Origins and Motivations of Univalent Foundations. 2014. url: https://www.ias.edu/ideas/2014/voevodsky-origins.