论文标题
在QuasicateGory中解释类型理论：Yoneda方法
Interpreting type theory in a quasicategory: a Yoneda approach
论文作者
论文摘要
我们利用更高版本的Yoneda嵌入来构建从给定的QuasicateGory，一种简单地富集的类别，作为行为良好的简单模型类别的子类别，其简单神经与以前的QuasicateGory相当。然后，我们表明，当QuasicateGory在本地笛卡尔封闭时，就可以进一步将这种简单类别赋予足够的结构，以提供Martin-Löf类型理论的模型。这种对应关系限制了，因此可以看到基本较高的topoi对同型类型理论进行建模。
We make use of a higher version of the Yoneda embedding to construct, from a given quasicategory, a simplicially enriched category, as a subcategory of a well-behaved simplicial model category, whose simplicial nerve is equivalent to the former quasicategory. We then show that, when the quasicategory is locally cartesian closed, it is possible to further endow such a simplicial category with enough structure for it to provide a model of Martin-Löf type theory. This correspondence restricts so that elementary higher topoi are seen to model homotopy type theory.
