Agda 的类别库？

Question

是否有任何“推荐”库可以在 Agda 中提供易于使用的基本范畴论形式化？ Agda 标准库似乎在这方面提供的很少。

我正在寻找入门门槛较低的东西，类似于如何使用标准库中定义的

Semigroup

等代数结构。

例如，我当前的项目中有几种态射的概念，并且组合和恒等的重载语法变得很尴尬。自然的做法是引入合适的记录类型并使用 Agda 的“实例参数”机制来模拟

Morphism

类型类。但毫无疑问，这一定是一个被发明了很多次的轮子。 （好吧，标准库中有一个名为

Morphism

的结构，也许可以适应这个目的，所以这不一定是最好的例子，但你明白了。）

我知道这个库，它看起来很全面，但似乎不是特别活跃。

Answer 1

我正在使用上面提到的Categories库，虽然我只使用它的基本功能，但到目前为止似乎还不错。

Answer 2

编辑： 以下内容写于 2022 年 2 月时正确的是：

这是一个老问题，但它仍然在谷歌和其他搜索中得到点击，所以：事实上的库现在是agda-categories。

---

但现在到了 2024 年 10 月，情况不再如此了。如果想在“纯”MLTT 中进行类别论，那么agda-categories 仍然是最佳选择。但如果有人想要“book HoTT”，那么agda-unimath也有大量的范畴论。

如果想要立方类型理论，有两种选择：agda-cubical库和1lab。在它们之间进行选择很复杂，因为它们有不同的理念。

作为其中一个库的维护者，我过于偏见，无法提供可靠的意见。但也没有那么偏见，以至于我不想确保“世界”知道这些选择。