形式化无穷范畴 Yoneda 引理

形式化的 1-范畴理论构成了各类数学证明库的核心组成部分。然而,从代数拓扑到理论物理等对象具有“高阶结构”的领域中,更为精细的结果依赖于无穷维范畴而非 1-维范畴,且无穷范畴理论迄今难以被计算机形式化。利用一个名为 Rzk 的新证明辅助器——其设计用于支持 Riehl-Shulman 的同伦类型论单纯形扩张以进行合成无穷范畴理论——我们提供了无穷范畴理论结果的首次形式化。这尤其包括 Yoneda 引理的形式化,该引理常被视为范畴理论的基本定理,其大致陈述了给定范畴中的一个对象由它与该范畴中所有其他对象的关系所决定。我们框架的一个关键特征是,得益于合成理论,许多构造自动是自然或函子性的。我们计划使用 Rzk 形式化无穷范畴理论的进一步结果,例如极限与余极限理论以及伴随。