Agda的分类库？

Question

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

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

例如,在我当前的项目中有几种态射的概念,并且组合和身份的重载语法变得笨拙.自然要做的是引入一个合适的记录类型,并使用Agda的"实例参数"机制来模拟一个Morphism类型类.但毫无疑问,这必须是多次发明的轮子.(好吧,Morphism在标准库中调用了一个可能适合此目的的结构,所以这不一定是最好的例子,但你明白了.)

我知道这个库看起来很全面,但似乎并不特别活跃.

Answer 1

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