2022/05/02 by Hoang Kim Nguyen, Nguyen, Hoang Kim, Uemura, Taichi · 2 citations
Mathematics · #18N60 (Primary) 03B38 (Secondary) #Advanced Topology and Set Theory #Algebraic structures and combinatorial models #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO)
paper · pdf · doi:10.48550/arxiv.2205.00798
openalex publication_date 2022/05/02 · openalex created_date 2022/05/05 · openalex updated_date 2026/07/28
We introduce ∞-type theories as an ∞-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 ∞-type theories, the construction of internal languages of models of ∞-type theories, and the theory-model correspondence for ∞-type theories. Some structured (∞,1)-categories are naturally regarded as models of some ∞-type theories. Thus, since every (1-categorical) type theory is in particular an ∞-type theory, ∞-type theories provide a unified framework for connections between type theories and (∞,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 (∞,1)-categories with finite limits.