Your language?
Jan, 2018
Sun Mon Tue Wed Thu Fri Sat
1 2 3 4 5 6
7 8 9 10 11 12 13
14 15 16 17 18 19 20
21 22 23 24 25 26 27
28 29 30 31

Homotopy Type Theory

Martin-Löf type theory [ ML75 ] Hofmann Streicher [ HS98 ] による groupoid model , model category などの ホモトピ 使 した 理論理 (?) んに 研究 されるようにな てきた ( , 1)-category 使 われている のような homotopy type theory ぶようである Blog もできて いる

としては , Pelayo Warren [ PW14 ] そして , Institute for Advanced Study The Univalent Foundation Program した がある には , リンク きの スクリ , margin ない e-book , そして , 3 PDF されている にも , Pelayo Warren [ PW14 ] , Rijke 修士 , この n -Category Café されている Shulman [ Shub ] などが ある

まずはこれらの めてみるのがよいだろう それによると , 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 かれている

Model category いた univalent universe , Cisinski [ Cis ] えられ ている

Voevodsky えていることについては Voevodsky ムペ slide video, あるいは preprint るぐらいしか 方法 はなか にも web はいくつかあるが , それらについては Gavlirovich Hasson Kaplan [ GHK15 ] Introduction るとよい

Homotopy type theory model としては , Voevodosky らの simplicial set たものが である Shulman [ Shu15 Shuc ] simplicial set category のある diagram category いたものが 使 えることを している また [ Shud ] では EI category ( , 1)-version index された diagram いることを して いる

トポロジ からは , Voevodsky univalent foundation いのは , する をある 程度 できる があるという ではないだろ うか また Shulman [ Shuc ] Introduction かれているように , simplicial set みで ホモトピ なうときにも 使 えるようで ある

ホモトピ える えば , この Homotopy Type Theory blog post , π 1 ( S 1 ) ~= formal proof えられている としては , Licata Shulman [ LS13 ] にな ている Brunerie [ Bru ] π 4 ( S 3 ) ~= 2 して いる

コホモロジ についても , Homotopy Type Theory blog Shulman いて いる

ホモトピ については , Avigad, Kapulkin, Lumsdaine [ AKL15 ] われて いる

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

Hou, Finster, Licata, Lumsdaine [ HFLL ] , Blakers-Massey theorem “mechanized proof” したと ている

ただし , このような homotopy theory homotopy type theory には すべきところがあるようで , Shulman [ Shua ] Introduction しく べて いる

Arndt Kapulkin [ AK11 ] , この のことを なうための model category , logical model category という 導入 している

  • logical model category

Cranch [ Cra ] ( , 1)-category homotopy type theory 導入 して いる

この n -Category Café によると , Schreiber 800 くある (?) [ Scha ] , homotopy type theory みを 使 おうとしているものらしい より かいものとして [ Schb ]

References

[AK11]     Peter Arndt and Krzysztof Kapulkin. Homotopy-theoretic models of type theory. In Typed lambda calculi and applications , volume 6690 of Lecture Notes in Comput. Sci. , pages 45–60. Springer, Heidelberg, 2011, arXiv:1208.5683 .

[AKL15]     Jeremy Avigad, Krzysztof Kapulkin, and Peter Lefanu Lumsdaine. Homotopy limits in type theory. Math. Structures Comput. Sci. , 25(5):1040–1070, 2015, arXiv:1304.0680 .

[AW09]     Steve Awodey and Michael A. Warren. Homotopy theoretic models of identity types. Math. Proc. Cambridge Philos. Soc. , 146(1):45–55, 2009, arXiv:0709.0248 .

[Bru]     Guillaume Brunerie. On the homotopy groups of spheres in homotopy type theory, arXiv:1606.05916 .

[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 .

[GHK15]     Misha Gavrilovich, Assaf Hasson, and Itay Kaplan. The univalence axiom in posetal model categories. J. Logic Comput. , 25(3):669–682, 2015, arXiv:1111.3489 .

[HFLL]     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 .

[HS98]     Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory (Venice, 1995) , volume 36 of Oxford Logic Guides , pages 83–111. Oxford Univ. Press, New York, 1998.

[LS13]     Daniel R. Licata and Michael Shulman. Calculating the fundamental group of the circle in homotopy type theory. In 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013) , pages 223–232. IEEE Computer Soc., Los Alamitos, CA, 2013, arXiv:1301.3443 .

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

[PW14]     Álvaro Pelayo and Michael A. Warren. Homotopy type theory and Voevodsky’s univalent foundations. Bull. Amer. Math. Soc. (N.S.) , 51(4):597–648, 2014, arXiv:1210.5658 .

[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 EI diagrams, arXiv:1508.02410 .

[Shu15]     Michael Shulman. Univalence for inverse diagrams and homotopy canonicity. Math. Structures Comput. Sci. , 25(5):1203–1277, 2015, arXiv:1203.3253 .