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

TL;DR

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, which combines the capabilities of an abstract computer algebra framework with those of a powerful automated theorem-proving system.

Abstract

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). 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.

Figures (29)

• Figure 1: On the left, the AbstractQuiver object for a simple (three-object, two-arrow) quiver. On the right, the AbstractCategory object for the three-object, six-morphism category that is freely generated by this quiver.
• Figure 2: On the left, the AbstractCategory object for a simple (four-object, ten-morphism) category, showing all algebraic equivalences between morphisms that must hold by virtue of the identity and associativity axioms of category theory. On the right, the AbstractCategory object for a slightly larger (five-object, fifteen-morphism) category, again showing all algebraic equivalences between morphisms that must hold by virtue of the identity and associativity axioms of category theory.
• Figure 3: On the left, the AbstractCategory object for a simple category with the object equivalence ${X = Y}$ specified, showing the labeled graph representations of the category both with and without algebraic equivalences imposed. On the right, the AbstractCategory object for a simple category with the morphism equivalence ${\left( f_1 : X \to Y \right) = \left( f_2 : X \to Y \right)}$ specified, showing the labeled graph representations of the category both with and without algebraic equivalences imposed.
• Figure 4: On the left, the AbstractCategory object corresponding to a simple (not yet commutative) square diagram, illustrating that the diagram is not commutative and showing that the morphism equivalence ${i \circ f = h \circ g}$ is the minimal algebraic condition necessary to force the diagram to commute. On the right, the AbstractCategory object for the commutative case of this same square diagram, with the morphism equivalence ${i \circ f = h \circ g}$ imposed, demonstrating that this equivalence is indeed sufficient to force the diagram to commute.
• Figure 5: On the left, the AbstractCategory object corresponding to a slightly more complex (not yet commutative) oblong diagram, illustrating that the diagram is not yet commutative and computing the minimum set of morphism equivalences necessary to force the diagram to commute. On the right, the AbstractCategory object for the commutative case of this same oblong diagram, with the aforementioned morphism equivalences imposed, demonstrating that these equivalences are indeed sufficient to force the diagram to commute.