Agda的类库？

Question

有没有什么“推荐”的库，可以在Agda中提供一个易于使用的基本范畴理论的形式化？Agda标准库在这方面提供的似乎很少。

我正在寻找具有低入门门槛的东西，类似于如何使用标准库中定义的代数结构，如Semigroup。

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

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

Answer 1

我使用的是上面提到的Categories库，虽然我只使用了它的基本特性，但到目前为止它看起来还不错。

Answer 2

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