在拟范畴中解释类型论:一种Yoneda方法
范畴论
2025-09-04 v2 代数拓扑
逻辑
摘要
我们利用高阶Yoneda嵌入,从给定拟范畴构造一个tribe,作为良态单纯模型范畴的子范畴,其呈现与前述拟范畴相同的 -范畴。随后我们表明,当该拟范畴局部笛卡尔闭时,可进一步赋予此tribe足够结构,使之提供带 -类型的Martin-Löf类型论的模型。该映射过程可限制为:初等高阶topos给出同伦类型论的模型。
引用
@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}
}
备注
33 pages, includes various corrections and improvements, removed erroneous last section (addressed in an independent paper)