Internal languages of finitely complete \((\infty , 1)\)-categories (Q2414596): Difference between revisions

Homotopy type theory has developed in ways that have closely paralleled the theory of \((\infty,1)\)-categories, and both areas have benefitted from the interplay between the two. The motivation for the paper under review is the desire for formal equivalences between various notions in the two theories. Such equivalences would allow for transport of theorems between the two areas, further strengthening our understanding of both. As a specific example, it is conjectured that \((\infty,1)\)-categories should be equivalent to syntactically presented type theories. While such a result is still unproved, the authors show that there is such an equivalence in a more restricted setting. They prove that finitely complete \((\infty,1)\)-categories are equivalent to categorical models of Martin-Löf Type Theory with dependent sums and intentional identity types. Using prior results, they reduce this result to finding an equivalence between fibration categories, as developed by Brown [3] and used extensively in homotopy theory, and tribes, developed by \textit{M. Shulman} [Math. Struct. Comput. Sci. 25, No. 5, 1203--1277 (2015; Zbl 1362.03008)] and \textit{A. Joyal} [``Notes on clans and tribes'', Preprint, \url{arXiv:1710.10238}]. To find such an equivalence, the authors make use of semi-simplicially enriched variants of both fibration categories and tribes.