论同伦类型理论的 ∞-拓扑斯语义
范畴论
2024-03-04 v3 代数拓扑
逻辑
摘要
许多关于同伦类型理论（homotopy type theory）与 univalence 公理的入门介绍都忽略了这一新形式系统在传统基于集合的基础中的语义。这篇综述性文章作为 CIRM-Luminy 的逻辑与高阶结构研讨会上一个三部分迷你课程的讲义，试图梳理当前最新进展：先介绍 Voevodsky 的非值化基础（univalent foundations）的单纯形模型，再巡览 Shulman 的宏大推广，后者给出了同伦类型理论在任意 ∞-拓扑斯（∞-topos）中带有严格非值化宇宙的解释。正如我们将要解释的，这一成果是学界共同努力抽象并精简原始论证以及发展新的推理路线的产物。
引用
@article{arxiv.2212.06937,
title = {On the $\infty$-topos semantics of homotopy type theory},
author = {Emily Riehl},
journal= {arXiv preprint arXiv:2212.06937},
year = {2024}
}
备注
These lecture notes were written to accompany a mini-course delivered at CIRM - Luminy from 21-25 February 2022. Video is available at https://www.carmin.tv/en/collections/logic-and-higher-structures-logique-et-structures-superieures; v2 incorporates feedback from the referee; v3 is the final journal version with updated section numbers to conform to journal style