Interpreting type theory in a quasicategory: a Yoneda approach
Category Theory
2025-09-04 v2 Algebraic Topology
Logic
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 -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 -types. This mapping procedure restricts so that elementary higher topoi yield models of homotopy type theory.
Keywords
Cite
@article{arxiv.2207.01967,
title = {Interpreting type theory in a quasicategory: a Yoneda approach},
author = {El Mehdi Cherradi},
journal= {arXiv preprint arXiv:2207.01967},
year = {2025}
}
Comments
33 pages, includes various corrections and improvements, removed erroneous last section (addressed in an independent paper)