$\infty$-type theories

TL;DR

This paper introduces $ abla$-type theories as an $ abla$-categorical extension of type theories, establishing initial models, internal languages, and a correspondence between models and theories, unifying type theories with $( abla,1)$-categorical structures.

Contribution

It generalizes categorical type theories to $ abla$-type theories within an $ abla$-categorical framework, including new constructions and a proof of a conjecture relating dependent type theory to $( abla,1)$-categories.

Findings

Constructed initial models of $ abla$-type theories

Established the theory-model correspondence for $ abla$-type theories

Proved the conjecture linking dependent type theory with $( abla,1)$-categories

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.