Internal Languages of Finitely Complete $(\infty, 1)$-categories

TL;DR

This paper establishes a connection between the homotopy theory of Joyal's tribes and fibration categories, supporting the idea that certain type theories serve as internal languages for $( abla, 1)$-categories with finite limits.

Contribution

It proves the equivalence of homotopy theories and confirms a variant of the conjecture linking Martin-Löf Type Theory to $( abla, 1)$-categories with finite limits.

Findings

Homotopy theory of Joyal's tribes is equivalent to that of fibration categories.

Supports the conjecture that Martin-Löf Type Theory is the internal language of $( abla, 1)$-categories.

Provides a new perspective on the relationship between type theory and higher category theory.

Abstract

We prove that the homotopy theory of Joyal's tribes is equivalent to that of fibration categories. As a consequence, we deduce a variant of the conjecture asserting that Martin-L\"of Type Theory with dependent sums and intensional identity types is the internal language of $(\infty, 1)$-categories with finite limits.