范畴论中缺失的图表（第一人称版本）
摘要：类别论的大多数文字都以非常简练的方式书写，假装所有的概念都是可视化的，读者只能根据最基本的线索重建作者头脑中的图表。作为一个门外汉，我花了多年的时间相信绘图技巧是该领域口耐文化的一部分，内行人可以从头到尾地阅读类别论的文本，逐行逐段地重新构建其中的“缺失图表”，并为每页文本绘制一张作者省略的所有图表的图示。我的信仰是错误的：绘制图表的惯例在文献中分散地存在，但并不存在统一的图表语言。在本章中，我将展示一种试图重构（想象中的）缺失图表语言的尝试：我们将看到一个可扩展的图表语言，称为DL，尽可能遵循类别论文献中的图表惯例，并且似乎适用于绘制类别论的“缺失图表”。我们的例子包括伴随性、Yoneda引理、Kan扩展和几何变态的“缺失图表”，以及如何在Agda中形式化它们。
作者：Eduardo Ochs
论文ID：2204.10630
分类：Category Theory
分类简称：math.CT
提交时间：2022-04-25