Applied Category Theory in the Wolfram Language using Categorica I: Diagrams, Functors and Fibrations

这篇文章作为一个初步介绍，介绍了一个新的、基于Wolfram语言的开源应用和计算范畴论框架——Categorica的设计。Categorica允许用户配置和操作抽象的quivers、范畴、群组、图表、函子和自然变换，并使用上述结构的任意组合执行广泛的自动抽象代数计算；抽象地推理和操作任意的普遍性质，包括积、余积、拉回、推出、极限和余极限；以及操作、可视化和计算严格（对称）单纯范畴，包括完全支持自动字符串图重写和图形定理证明。通过这样做，Categorica结合了抽象计算机代数框架的能力（因此允许直接使用epimorphisms、monomorphisms、retractions、sections、spans、cospans、fibrations等进行计算）和强大的自动定理证明系统的能力（因此允许将普遍性质和其他抽象构造转换为（高阶）等式逻辑语句，可以使用标准的自动定理证明方法进行推理和证明，也可以直接使用纯图形方法证明范畴论语句）。在介绍框架设计的两篇文章中的第一篇，我们将主要关注它对quivers、范畴、图表、群组、函子和自然变换的处理，包括在每种情况下它的代数操作和定理证明能力的演示。

介绍Categorica框架，解决抽象代数计算和自动推理问题。

Categorica框架结合了抽象计算代数和自动推理系统，实现了对抽象代数结构的计算、可视化和自动推理。

Categorica框架可以处理抽象的quivers、categories、groupoids、diagrams、functors和natural transformations，同时支持自动化的定理证明和字符串图重写。实验展示了框架在代数计算和定理证明方面的能力，框架也提供了开源代码。

最近的相关研究包括基于范畴论的自动推理系统和抽象代数计算框架，如Homotopy Type Theory和Lean Theorem Prover。