\infty-type theories

arXiv2205.00798MaRDI QIDQ6398014FDOQ6398014

Authors: Hoang Kim Nguyen, Taichi Uemura 

Publication date: 2 May 2022

Abstract: 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.

Mathematics Subject Classification ID

Type theory (03B38) ((infty,1))-categories (quasi-categories, Segal spaces, etc.); (infty)-topoi, stable (infty)-categories (18N60)

This page was built for publication: $\infty$-type theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6398014)