standard-library - Agda 的分类库？

Question

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

我正在寻找入门阈值低的东西，类似于人们如何使用代数结构，例如 Semigroup在标准库中定义。

例如，在我当前的项目中有几个态射的概念，重载组合和恒等式的语法变得很尴尬。自然的做法是引入合适的记录类型并使用 Agda 的“实例参数”机制来模拟 Morphism类型类。但毫无疑问，这一定是一个被发明了很多次的轮子。 (好吧，标准库中有一个名为 Morphism 的结构，它也许可以适应这个目的，所以这不一定是最好的例子，但你明白了。)

我知道 this library ，看起来很全面，但似乎不是特别活跃。

Answer 1

我正在使用 Categories库如上所述，虽然我只使用它的基本功能，但到目前为止看起来还不错。