论范畴论中缺失的图表（第一人称版）
范畴论
2022-04-25 v1
摘要
大多数范畴论文本都以极为简略的风格写成，其中人们假定 a) 所有概念都是可可视化的，且 b) 读者仅基于最本质的线索就能重构作者心目中的图表。作为一个局外人，我曾花费数年相信绘制图表的技巧是该领域的口传文化的一部分，且内部人士能够逐行逐段阅读 CT 文本并重构其中的“缺失图表”，并为每页文本绘制一页图表，其中包含作者省略的所有图表。我的信念是错误的：文献中散落着许多绘制图表的约定，但那种统一的图表语言并不存在。在本章中，我将展示一种重构那种（想象中的）缺失图表语言的尝试：我们将看到一种可扩展的图表语言，称为 DL，它尽可能遵循 CT 文献中图表的约定，并且似乎足以用于绘制范畴论的“缺失图表”。我们的例子包括伴随、Yoneda 引理、Kan 扩张以及几何态射的“缺失图表”，以及如何在 Agda 中将其形式化。
引用
@article{arxiv.2204.10630,
title = {On the the missing diagrams in Category Theory (first-person version)},
author = {Eduardo Ochs},
journal= {arXiv preprint arXiv:2204.10630},
year = {2022}
}
备注
66 pages. arXiv admin note: substantial text overlap with arXiv:2006.15836