Interpreting type theory in a quasicategory: a Yoneda approach

2022/07/05 by El Mehdi Cherradi, Cherradi, El Mehdi · 1 citation
Mathematics · #Advanced Topics in Algebra #Algebraic Topology (math.AT) #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO)

paper · pdf · doi:10.48550/arxiv.2207.01967

openalex publication_date 2022/07/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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)-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 Π-types. This mapping procedure restricts so that elementary higher topoi yield models of homotopy type theory.

Cited by

• Internal languages of locally cartesian closed (∞,1)-categories

Related

• The Yoneda embedding in simplicial type theory
• Type theory and homotopy
• Models of Type Theory with Strict Equality
• Concrete Categories in Homotopy Type Theory
• The homotopy theory of type theories