Interpreting type theory in a quasicategory: a Yoneda approach

TL;DR

This paper develops a method using a higher Yoneda embedding to interpret quasicategories as tribes within simplicial model categories, enabling models of Martin-Löf type theory with Pi-types, especially for locally cartesian closed cases.

Contribution

It introduces a novel construction linking quasicategories to tribes via a higher Yoneda embedding, facilitating models of homotopy type theory from elementary higher topoi.

Findings

Constructs tribes from quasicategories using a higher Yoneda embedding.

Shows that locally cartesian closed quasicategories can model Martin-Löf type theory.

Elementary higher topoi can serve as models of homotopy type theory.

Abstract

We make use of a higher version of the Yoneda embedding to construct, from a given quasicategory, a tribe, as a subcategory of a well-behaved simplicial model category, that presents the same $(\infty,1)$-category as the former quasicategory. We then show that, when the quasicategory is locally cartesian closed, it is possible to further endow such a tribe with enough structure for it to provide a model of Martin-L\"of type theory with $\Pi$-types. This mapping procedure restricts so that elementary higher topoi yield models of homotopy type theory.