Article
Full entry |
PDF
(0.8 MB)
Feedback
PDF
(0.8 MB)
Feedback
Keywords:
type theory; $\infty$-type theory; $(\infty,1)$-category; representable map; initial model; internal language; coherence problem
type theory; $\infty$-type theory; $(\infty,1)$-category; representable map; initial model; internal language; coherence problem
Summary:
We introduce $\infty$-type theories as an $\infty$-categorical generalization of the categorical definition of type theories introduced by the second named author. We establish analogous results to the previous work including the construction of initial models of $\infty$-type theories, the construction of internal languages of models of $\infty$-type theories, and the theory-model correspondence for $\infty$-type theories. Some structured $(\infty,1)$-categories are naturally regarded as models of some $\infty$-type theories. Thus, since every (1-categorical) type theory is in particular an $\infty$-type theory, $\infty$-type theories provide a unified framework for connections between type theories and $(\infty, 1)$-categorical structures. As an application we prove Kapulkin and Lumsdaine's conjecture that the dependent type theory with intensional identity types gives internal languages for $(\infty,1)$-categories with finite limits.
References:
[1] Anel, M., Biedermann, G., Finster, E., Joyal, A.: Goodwillie's calculus of functors and higher topos theory. J. Topol. 11 (2018), 1100-1132 DOI 10.1112/topo.12082 | MR 3989439
[2] Anel, M., Biedermann, G., Finster, E., Joyal, A.: A generalized Blakers-Massey theorem. J. Topol. 13 (2020), 1521-1553 DOI 10.1112/topo.12163 | MR 4186137
[3] Arndt, P., Kapulkin, K.: Homotopy-Theoretic Models of Type Theory. Typed lambda calculi and applications: 10th international conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011, pp 45-60 MR 2830786
[4] Avigad, J., Kapulkin, K., Lumsdaine, P. L.: Homotopy limits in type theory. Mathematical Structures in Computer Science 25 (2015), 1040-1070 DOI 10.1017/S0960129514000498 | MR 3340534
[5] Awodey, S.: Natural models of homotopy type theory. Mathematical Structures in Computer Science 28 (2018), 241-286 DOI 10.1017/S0960129516000268 | MR 3742564
[6] Awodey, S., Warren, M. A.: Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society 146 (2009), 45-55 DOI 10.1017/S0305004108001783 | MR 2461866
[7] Bocquet, R.: Coherence of strict equalities in dependent type theories. Available at https://arxiv.org/abs/2010.14166
[8] Brown, K. S.: Abstract homotopy theory and generalized sheaf cohomology. Transactions of the American Mathematical Society 186 (1973), 419-458 DOI 10.1090/S0002-9947-1973-0341469-9
[9] Brunerie, G.: On the homotopy groups of spheres in homotopy type theory: PhD thesis. Université de Nice, 2016
[10] Brunerie, G.: The James construction and $\pi_4(\Bbb{S}^3)$ in homotopy type theory. J. Automat. Reason. 63 2019], 255-284 DOI 10.1007/s10817-018-9468-2 | MR 3979632
[11] Cartmell, J. W.: Generalised algebraic theories and contextual categories: PhD thesis. Oxford University, 1978
[12] Cisinski, D.-C.: Higher categories and homotopical algebra. Cambridge studies in advanced mathematics, Cambridge University Press, 2019 MR 3931682
[13] Clairambault, P., Dybjer, P.: The biequivalence of locally cartesian closed categories and Martin-Löf type theories. Mathematical Structures in Computer Science 24 (2014), Article ID e240606 DOI 10.1017/S0960129513000881 | MR 3272793
[14] Curien, P.-L.: Substitution up to Isomorphism. Fundam. Inform. 19 (1993), 51-85 DOI 10.3233/FI-1993-191-204
[15] Dybjer, P.: Internal Type Theory. Types for proofs and programs: International workshop, TYPES ’95 Torino, Italy, June 5–8, 1995 selected papers, pages 120-134, 1996
[16] Fiore, M.: Discrete Generalised Polynomial Functors. Talk at ICALP 2012, Available at http://www.cl.cam.ac.uk/~mpf23/talks/ICALP2012.pdf
[17] Gambino, N., Kock, J.: Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society 154 (2013), 153-192 MR 3002590
[18] Garner, R.: Combinatorial structure of type dependency. Journal of Pure and Applied Algebra 219 (2015), 1885-1914 DOI 10.1016/j.jpaa.2014.07.015 | MR 3299712
[19] Gepner, D., Kock, J.: Univalence in locally cartesian closed $\infty$-categories. Forum Mathematicum 29 (2017) DOI 10.1515/forum-2015-0228 | MR 3641669
[20] Hofmann, M.: On the interpretation of type theory in locally Cartesian closed categories. Computer Science Logic, pp 427-441, 1995 DOI 10.1007/BFb0022273
[21] Hou, K.-B., Finster, E., Licata, D. R., Lumsdaine, P. L.: A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory. Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2016), pp 10, 2016 MR 3776776
[22] Isaev, V.: Algebraic Presentations of Dependent Type Theories. Available at https://arxiv.org/abs/1602.08504v3
[23] Joyal, A.: Notes on quasi-categories. Available at http://www.math.uchicago.edu/~may/IMA/Joyal.pdf
[24] Joyal, A.: Notes on clans and tribes. Available at https://arxiv.org/abs/1710.10238v1
[25] Joyal, A., Tierney, M.: Quasi-categories vs Segal spaces. Categories in algebra, geometry and mathematical physics, pages 277-326, 2007. Contemp. Math. 431 DOI 10.1090/conm/431/08278 | MR 2342834
[26] Kapulkin, K.: Locally Cartesian closed quasi-categories from type theory. Journal of Topology 10 (2017), 1029-1049 DOI 10.1112/topo.12031 | MR 3743067
[27] Kapulkin, K., Lumsdaine, P. L.: The homotopy theory of type theories. Adv. Math. 337 (2018), 1-38 DOI 10.1016/j.aim.2018.08.003 | MR 3853043
[28] Kapulkin, K., Lumsdaine, P. L.: The simplicial model of Univalent Foundations (after Voevodsky). Journal of the European Mathematical Society, 23 (2021), 2071-2126 DOI 10.4171/jems/1050 | MR 4244523
[29] Kapulkin, K., Szumiło, K.: Internal languages of finitely complete $(\infty,1)$-categories. Selecta Math. (N.S.) 25 (2019), Article ID 33, 46 pages DOI 10.1007/s00029-019-0480-0 | MR 3943478
[30] Lambek, J., Scott, P. J.: Introduction to higher order categorical logic. Cambridge University Press, 1986
[31] Lawvere, F. W.: Functorial semantics of algebraic theories: PhD thesis. Columbia University, 1963
[32] Licata, D. R., Shulman, M.: Calculating the fundamental group of the circle in homotopy type theory. 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), pages 223-232, 2013 MR 3323808
[33] Lo Monaco, G.: Dependent products and 1-inaccessible universes. Theory and Applications of Categories 37 (2021), 107-143 DOI 10.70930/tac/diffabg4 | MR 4217345
[34] Lumsdaine, P. L., Warren, M. A.: The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories. ACM Trans. Comput. Logic 16 (2015), 1-23 DOI 10.1145/2754931 | MR 3372323
[35] Lurie, J.: Higher Algebra. Available at http://www.math.harvard.edu/~lurie/papers/HA.pdf
[36] Lurie, J.: Higher Topos Theory. Princeton University Press, 2009 MR 2522659
[37] Nguyen, H. K.: Theorems in Higher Category Theory and Applications: PhD thesis. Universität Regensburg, 2019
[38] Nguyen, H. K., Raptis, G., Schrade, C.: Adjoint functor theorems for $\infty$-categories. Journal of the London Mathematical Society 101 (2020), 659-681 DOI 10.1112/jlms.12282 | MR 4093970
[39] Rasekh, N.: Complete Segal Objects. Available at https://arxiv.org/abs/1805.03561v1
[40] Rasekh, N.: Univalence in Higher Category Theory. Available at https://arxiv.org/abs/2103.12762v2
[41] Riehl, E., Verity, D.: Elements of $\infty$-Category Theory. Cambridge studies in advanced mathematics, Cambridge University Press, 2022 MR 4354541
[42] Shulman, M.: Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science 25 (2015), 1203-1277 DOI 10.1017/S0960129514000565 | MR 3340541
[43] Shulman, M.: All $(\infty,1)$-toposes have strict univalent universes. Available at https://arxiv.org/abs/1904.07004v2
[44] Szumiło, K.: Two models for the homotopy theory of cocomplete homotopy theories: PhD thesis. University of Bonn, 2014
[45] The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics. Available at https://homotopytypetheory.org/book/ MR 3204653
[46] Uemura, T.: The universal exponentiable arrow. Journal of Pure and Applied Algebra 226 (2022), 106991 DOI 10.1016/j.jpaa.2021.106991 | MR 4355947
[47] Uemura, T.: A general framework for the semantics of type theory. Mathematical Structures in Computer Science, 1-46, 2023 MR 4634095
[48] Berg, B., Moerdijk, I.: Exact completion of path categories and algebraic set theory: Part I: Exact completion of path categories. Journal of Pure and Applied Algebra 222 (2018), 3137 - 3181 DOI 10.1016/j.jpaa.2017.11.017 | MR 3795638
[49] Voevodsky, V.: B-systems. Available at https://arxiv.org/abs/1410.5389v1 MR 4337193
[50] Weber, M.: Polynomials in categories with pullbacks. Theory and Applications of Categories 30 (2015), 533-598 DOI 10.70930/tac/du5o6klz | MR 3341723
Search
Partner of
