| Title:
|
$\infty$-type theories (English) |
| Author:
|
Uemura, Taichi |
| Author:
|
Nguyen, Hoang Kim |
| Language:
|
English |
| Journal:
|
Higher Structures |
| ISSN:
|
2209-0606 |
| Volume:
|
9 |
| Issue:
|
1 |
| Year:
|
2025 |
| Pages:
|
179-226 |
| Summary lang:
|
English |
| . |
| Category:
|
math |
| . |
| 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. (English) |
| Keyword:
|
type theory |
| Keyword:
|
$\infty$-type theory |
| Keyword:
|
$(\infty,1)$-category |
| Keyword:
|
representable map |
| Keyword:
|
initial model |
| Keyword:
|
internal language |
| Keyword:
|
coherence problem |
| MSC:
|
03B38 |
| MSC:
|
18N60 |
| idZBL:
|
Zbl 08141785 |
| idMR:
|
MR4918787 |
| DOI:
|
10.21136/HS.2025.04 |
| . |
| Date available:
|
2026-03-13T14:18:03Z |
| Last updated:
|
2026-03-13 |
| Stable URL:
|
http://hdl.handle.net/10338.dmlcz/153485 |
| . |
| Reference:
|
[1] Anel, M., Biedermann, G., Finster, E., Joyal, A.: Goodwillie's calculus of functors and higher topos theory.J. Topol. 11 (2018), 1100-1132 MR 3989439, 10.1112/topo.12082 |
| Reference:
|
[2] Anel, M., Biedermann, G., Finster, E., Joyal, A.: A generalized Blakers-Massey theorem.J. Topol. 13 (2020), 1521-1553 MR 4186137, 10.1112/topo.12163 |
| Reference:
|
[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 |
| Reference:
|
[4] Avigad, J., Kapulkin, K., Lumsdaine, P. L.: Homotopy limits in type theory.Mathematical Structures in Computer Science 25 (2015), 1040-1070 MR 3340534, 10.1017/S0960129514000498 |
| Reference:
|
[5] Awodey, S.: Natural models of homotopy type theory.Mathematical Structures in Computer Science 28 (2018), 241-286 MR 3742564, 10.1017/S0960129516000268 |
| Reference:
|
[6] Awodey, S., Warren, M. A.: Homotopy theoretic models of identity types.Mathematical Proceedings of the Cambridge Philosophical Society 146 (2009), 45-55 MR 2461866, 10.1017/S0305004108001783 |
| Reference:
|
[7] Bocquet, R.: Coherence of strict equalities in dependent type theories.Available at https://arxiv.org/abs/2010.14166 |
| Reference:
|
[8] Brown, K. S.: Abstract homotopy theory and generalized sheaf cohomology.Transactions of the American Mathematical Society 186 (1973), 419-458 10.1090/S0002-9947-1973-0341469-9 |
| Reference:
|
[9] Brunerie, G.: On the homotopy groups of spheres in homotopy type theory: PhD thesis.Université de Nice, 2016 |
| Reference:
|
[10] Brunerie, G.: The James construction and $\pi_4(\Bbb{S}^3)$ in homotopy type theory.J. Automat. Reason. 63 2019], 255-284 MR 3979632, 10.1007/s10817-018-9468-2 |
| Reference:
|
[11] Cartmell, J. W.: Generalised algebraic theories and contextual categories: PhD thesis.Oxford University, 1978 |
| Reference:
|
[12] Cisinski, D.-C.: Higher categories and homotopical algebra.Cambridge studies in advanced mathematics, Cambridge University Press, 2019 MR 3931682 |
| Reference:
|
[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 MR 3272793, 10.1017/S0960129513000881 |
| Reference:
|
[14] Curien, P.-L.: Substitution up to Isomorphism.Fundam. Inform. 19 (1993), 51-85 10.3233/FI-1993-191-204 |
| Reference:
|
[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 |
| Reference:
|
[16] Fiore, M.: Discrete Generalised Polynomial Functors.Talk at ICALP 2012, Available at http://www.cl.cam.ac.uk/~mpf23/talks/ICALP2012.pdf |
| Reference:
|
[17] Gambino, N., Kock, J.: Polynomial functors and polynomial monads.Mathematical Proceedings of the Cambridge Philosophical Society 154 (2013), 153-192 MR 3002590 |
| Reference:
|
[18] Garner, R.: Combinatorial structure of type dependency.Journal of Pure and Applied Algebra 219 (2015), 1885-1914 MR 3299712, 10.1016/j.jpaa.2014.07.015 |
| Reference:
|
[19] Gepner, D., Kock, J.: Univalence in locally cartesian closed $\infty$-categories.Forum Mathematicum 29 (2017) MR 3641669, 10.1515/forum-2015-0228 |
| Reference:
|
[20] Hofmann, M.: On the interpretation of type theory in locally Cartesian closed categories.Computer Science Logic, pp 427-441, 1995 10.1007/BFb0022273 |
| Reference:
|
[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 |
| Reference:
|
[22] Isaev, V.: Algebraic Presentations of Dependent Type Theories.Available at https://arxiv.org/abs/1602.08504v3 |
| Reference:
|
[23] Joyal, A.: Notes on quasi-categories.Available at http://www.math.uchicago.edu/~may/IMA/Joyal.pdf |
| Reference:
|
[24] Joyal, A.: Notes on clans and tribes.Available at https://arxiv.org/abs/1710.10238v1 |
| Reference:
|
[25] Joyal, A., Tierney, M.: Quasi-categories vs Segal spaces.Categories in algebra, geometry and mathematical physics, pages 277-326, 2007. Contemp. Math. 431 MR 2342834, 10.1090/conm/431/08278 |
| Reference:
|
[26] Kapulkin, K.: Locally Cartesian closed quasi-categories from type theory.Journal of Topology 10 (2017), 1029-1049 MR 3743067, 10.1112/topo.12031 |
| Reference:
|
[27] Kapulkin, K., Lumsdaine, P. L.: The homotopy theory of type theories.Adv. Math. 337 (2018), 1-38 MR 3853043, 10.1016/j.aim.2018.08.003 |
| Reference:
|
[28] Kapulkin, K., Lumsdaine, P. L.: The simplicial model of Univalent Foundations (after Voevodsky).Journal of the European Mathematical Society, 23 (2021), 2071-2126 MR 4244523, 10.4171/jems/1050 |
| Reference:
|
[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 MR 3943478, 10.1007/s00029-019-0480-0 |
| Reference:
|
[30] Lambek, J., Scott, P. J.: Introduction to higher order categorical logic.Cambridge University Press, 1986 |
| Reference:
|
[31] Lawvere, F. W.: Functorial semantics of algebraic theories: PhD thesis.Columbia University, 1963 |
| Reference:
|
[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 |
| Reference:
|
[33] Lo Monaco, G.: Dependent products and 1-inaccessible universes.Theory and Applications of Categories 37 (2021), 107-143 MR 4217345, 10.70930/tac/diffabg4 |
| Reference:
|
[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 MR 3372323, 10.1145/2754931 |
| Reference:
|
[35] Lurie, J.: Higher Algebra.Available at http://www.math.harvard.edu/~lurie/papers/HA.pdf |
| Reference:
|
[36] Lurie, J.: Higher Topos Theory.Princeton University Press, 2009 MR 2522659 |
| Reference:
|
[37] Nguyen, H. K.: Theorems in Higher Category Theory and Applications: PhD thesis.Universität Regensburg, 2019 |
| Reference:
|
[38] Nguyen, H. K., Raptis, G., Schrade, C.: Adjoint functor theorems for $\infty$-categories.Journal of the London Mathematical Society 101 (2020), 659-681 MR 4093970, 10.1112/jlms.12282 |
| Reference:
|
[39] Rasekh, N.: Complete Segal Objects.Available at https://arxiv.org/abs/1805.03561v1 |
| Reference:
|
[40] Rasekh, N.: Univalence in Higher Category Theory.Available at https://arxiv.org/abs/2103.12762v2 |
| Reference:
|
[41] Riehl, E., Verity, D.: Elements of $\infty$-Category Theory.Cambridge studies in advanced mathematics, Cambridge University Press, 2022 MR 4354541 |
| Reference:
|
[42] Shulman, M.: Univalence for inverse diagrams and homotopy canonicity.Mathematical Structures in Computer Science 25 (2015), 1203-1277 MR 3340541, 10.1017/S0960129514000565 |
| Reference:
|
[43] Shulman, M.: All $(\infty,1)$-toposes have strict univalent universes.Available at https://arxiv.org/abs/1904.07004v2 |
| Reference:
|
[44] Szumiło, K.: Two models for the homotopy theory of cocomplete homotopy theories: PhD thesis.University of Bonn, 2014 |
| Reference:
|
[45] The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics.Available at https://homotopytypetheory.org/book/ MR 3204653 |
| Reference:
|
[46] Uemura, T.: The universal exponentiable arrow.Journal of Pure and Applied Algebra 226 (2022), 106991 MR 4355947, 10.1016/j.jpaa.2021.106991 |
| Reference:
|
[47] Uemura, T.: A general framework for the semantics of type theory.Mathematical Structures in Computer Science, 1-46, 2023 MR 4634095 |
| Reference:
|
[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 MR 3795638, 10.1016/j.jpaa.2017.11.017 |
| Reference:
|
[49] Voevodsky, V.: B-systems.Available at https://arxiv.org/abs/1410.5389v1 MR 4337193 |
| Reference:
|
[50] Weber, M.: Polynomials in categories with pullbacks.Theory and Applications of Categories 30 (2015), 533-598 MR 3341723, 10.70930/tac/du5o6klz |
| . |
