在 Agda 中形式化范畴论
计算机科学中的逻辑
2021-03-04 v2
摘要
范畴论在现代数学中的普遍性与渗透性使其成为形式化工作中频繁而有用的目标。然而由于多种原因，它形式化的难度相当大。Agda 目前（即 2020 年）还没有一个标准的、可用的范畴论形式化。我们记录了为解决这一困境所做的工作。形式化过程揭示了许多潜在的设计选择，我们给出、论证并解释了我们所选取的那些。特别地，我们发现相对于标准教科书中的定义或证明，替代定义或替代证明可能更有优势，并且能更平滑地“契合”Agda 的类型论。一些在标准教科书中被视为等价的定义，结果却作出了不同的“宇宙层级”假设，其中某些比其他的更具多态性。我们也密切关注工程问题，以使该库能与 Agda 自身标准库良好集成，并尽可能兼容 Agda 中受支持的类型论。
引用
@article{arxiv.2005.07059,
title = {Formalizing of Category Theory in Agda},
author = {Jason Z. S. Hu and Jacques Carette},
journal= {arXiv preprint arXiv:2005.07059},
year = {2021}
}