类型论与一致纤束的 Kripke-Joyal 力迫
逻辑
2024-05-10 v2 范畴论
摘要
我们引入了一种新方法，用于精确关联预层范畴中的某些代数结构与其内部类型论的判定。该方法提供了一种系统化方式来组织复杂的图示推理，并推广了著名的逻辑 Kripke-Joyal 力迫。作为一个应用，我们证明了同伦类型论中所考虑的代数弱分解系统的若干性质。
引用
@article{arxiv.2110.14576,
title = {Kripke-Joyal forcing for type theory and uniform fibrations},
author = {S. Awodey and N. Gambino and S. Hazratpour},
journal= {arXiv preprint arXiv:2110.14576},
year = {2024}
}
备注
v2. 56 pages. Minor changes following referee report. To appear in Selecta Mathematica, New Series