English

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 (,1)(\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.

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)