Interpreting type theory in a quasicategory: a Yoneda approach

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 $(\mathrm{\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öf type theory with $\mathrm{\Pi }$-types. This mapping procedure restricts so that elementary higher topoi yield models of homotopy type theory.