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

This article serves as a preliminary introduction to the design of a new, open-source applied and computational category theory framework, named Categorica, built on top of the Wolfram Language. Categorica allows one to configure and manipulate abstract quivers, categories, groupoids, diagrams, functors and natural transformations, and to perform a vast array of automated abstract algebraic computations using (arbitrary combinations of) the above structures; to manipulate and abstractly reason about arbitrary universal properties, including products, coproducts, pullbacks, pushouts, limits and colimits; and to manipulate, visualize and compute with strict (symmetric) monoidal categories, including full support for automated string diagram rewriting and diagrammatic theorem-proving. In so doing, Categorica combines the capabilities of an abstract computer algebra framework (thus allowing one to compute directly with epimorphisms, monomorphisms, retractions, sections, spans, cospans, fibrations, etc.) with those of a powerful automated theorem-proving system (thus allowing one to convert universal properties and other abstract constructions into (higher-order) equational logic statements that can be reasoned about and proved using standard automated theorem-proving methods, as well as to prove category-theoretic statements directly using purely diagrammatic methods). Internally, Categorica relies upon state-of-the-art graph and hypergraph rewriting algorithms for its automated reasoning capabilities, and is able to convert seamlessly between diagrammatic/combinatorial reasoning on labeled graph representations and symbolic/abstract reasoning on underlying algebraic representations of all category-theoretic concepts. In this first of two articles introducing the design of the framework, we shall focus principally upon its handling of quivers, categories, diagrams, groupoids, functors and natural transformations, including demonstrations of both its algebraic manipulation and theorem-proving capabilities in each case.