论文标题
在类别理论中的缺失图（第一人称版本）上
On the the missing diagrams in Category Theory (first-person version)
论文作者
论文摘要
大多数类别理论的文本都以一种非常简短的风格编写，其中人们假装a）所有概念都是可视化的，b）读者可以重建作者仅基于最重要的提示而想到的图表。作为局外人，我花了多年的时间认为，绘图图的技术是该领域口头文化的一部分，并且内部人员可以读取有关CT的文本，以按段落和段落划分“缺少图表”，并根据段落划分段落，并为每一页的图表绘制所有图表的页面。我的信念是错误的：有很多惯例用于绘制图表，这些图表散布在文献中，但是统一的图解语言不存在。在本章中，我将展示一种尝试重建缺少图表的（虚构的）语言：我们将看到一种可扩展的图形语言，称为DL，该语言称为DL，该语言遵循CT文献中图表的惯例，并在任何可能的情况下似乎足以用于绘制类别论的“缺失图”。我们的示例包括针对附件的“缺失图”，Yoneda引理，KAN扩展和几何形态的“缺失图”以及如何在AGDA中形式化它们。
Most texts on Category Theory are written in a very terse style, in which people pretend a) that all concepts are visualizable, and b) that the readers can reconstruct the diagrams that the authors had in mind based on only the most essential cues. As an outsider I spent years believing that the techniques for drawing diagrams were part of the oral culture of the field, and that the insiders could read texts on CT reconstructing the "missing diagrams" in them line by line and paragraph by paragraph, and drawing for each page of text a page of diagrams with all the diagrams that the authors had omitted. My belief was wrong: there are lots of conventions for drawing diagrams scattered through the literature, but that unified diagrammatic language did not exist. In this chapter I will show an attempt to reconstruct that (imaginary) language for missing diagrams: we will see an extensible diagrammatic language, called DL, that follows the conventions of the diagrams in the literature of CT whenever possible and that seems to be adequate for drawing "missing diagrams" for Category Theory. Our examples include the "missing diagrams" for adjunctions, for the Yoneda Lemma, for Kan extensions, and for geometric morphisms, and how to formalize them in Agda.
