  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.
