使用 Categorica 在 Wolfram 语言中实现应用范畴论 I：图、函子与纤维化

本文初步介绍了一个名为 Categorica 的新型开源应用与计算范畴论框架的设计，该框架构建于 Wolfram 语言之上。Categorica 允许用户配置和操作抽象的箭图、范畴、广群、图、函子和自然变换，并使用上述结构的（任意组合）执行大量自动化的抽象代数计算；操作并抽象推理任意的泛性质，包括积、余积、拉回、推出、极限和余极限；以及操作、可视化和计算严格（对称）幺半范畴，包括对自动弦图重写和图解定理证明的全面支持。通过这种方式，Categorica 将抽象计算机代数框架的能力（从而允许用户直接计算满态射、单态射、收缩、截面、张成、余张成、纤维化等）与强大的自动定理证明系统的能力（从而允许用户将泛性质和其他抽象构造转换为（高阶）等式逻辑语句，这些语句可以使用标准的自动定理证明方法进行推理和证明，以及使用纯粹的图解方法直接证明范畴论陈述）相结合。在这两篇介绍该框架设计的文章的第一篇中，我们将主要关注其对图、范畴、态射、群胚、函子和自然变换的处理，包括在每种情况下展示其代数操作和定理证明的能力。