文件名称：premonoidal:Agda编码的类前类别
文件大小：11KB
文件格式：ZIP
更新时间：2024-04-28 15:27:04
Agda
前类 我想为{对称，半笛卡尔直角，笛卡尔直角}前正弦类别中的每个等效类定义一个规范的代表。 在Agda（此项目）中，这使得定义求解器成为可能，该求解器自动证明等效表达式（相同等效类中的表达式）相等。 在Haskell（我的项目）中，这使得生成需要最少类型类数量的代码变得更加容易。 使用Agda-2.6.1.1和agda-stdlib-1.4进行了测试。 规范代表和求解器 以下等式适用于任何类别： (id >>> f) >>> (g >>> id) ≡ f >>> id >>> g 我的可以自动证明该方程式。 该页面详细介绍了该技术，但是关键的一步是将这两个方面都转换为标准表示f >>> (g >>> id) 。 同样，在任何，都有一些方程式： a (b (c d)) a (b (c d)) | |
【文件预览】：
premonoidal-master
----compile.sh(244B)
----compile_continuously.sh(254B)
----src()
--------Category()
----.gitignore(8B)
----README.md(11KB)