是否有任何“推荐”的库可以在 Agda 中提供易于使用的基本范畴理论形式化？Agda 标准库似乎在这方面提供的很少。
我正在寻找入门门槛低的东西，类似于使用Semigroup标准库中定义的代数结构的方式。
例如，在我当前的项目中有几个态射概念，重载合成和恒等式的语法变得很尴尬。很自然的做法是引入一个合适的记录类型并使用 Agda 的“实例参数”机制来模拟一个Morphism类型类。但毫无疑问，这一定是一个发明了很多次的轮子。（好吧，标准库中调用Morphism了一个结构，也许可以适应这个目的，所以这不一定是最好的例子，但你明白了。）
我知道这个库，它看起来很全面，但似乎并不是特别活跃。