Agda的分类图书馆？

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

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

例如，在我当前的项目中有几种morphism的概念，并且组合和身份的重载语法变得很笨拙。自然要做的是引入合适的记录类型，并使用Agda的“实例参数”机制来模拟Morphism类型的类。但毫无疑问，这必定是一个多次发明的轮子。（好的，在标准库中有一个叫做Morphism的结构，或许可以适应这个目的，所以这不一定是最好的例子，但你明白了。）

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

来源

2014-09-04 Roly

嗯，你连接的图书馆似乎正式被Agda祝福，它被分成主要的GitHub帐户。你对类别有什么特别的缺点吗？我怀疑它并没有像睡觉一样死去。 – jozefg 2014-09-04 13:03:59

没有特别的缺点，虽然自述文件确实有一个免责声明，说明包结构是一团糟（这可能会让习惯新库变得很痛苦）。我想我更关心它是否被广泛使用，而不是它是否处于积极的发展状态。 – Roly 2014-09-04 13:06:18

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

来源

2014-12-04 07:39:18 Roly

Agda的分类图书馆？

回答

相关问题