The following table compares general and technical information for a number of existing and hypothetical category theory software packages. Drawn from the discussion (ft. Jamie Vicary) on May 1, 2018 at the Applied Category Theory workshop in Leiden.
| Software package | Does it exist? | Author | Goal | User interaction | Automation | How to define categories | Categorical setting | Structures it can compute | Architecture | Directed? (i.e. categories vs. groupoids) |
|---|---|---|---|---|---|---|---|---|---|---|
| HoTT libraries in Cog or Agda | Yes | Various | Research | Code | Proof assistant | Via presentations | Higher (weak) | Limits, colimits, functors | Library | No |
| Opetopic | Yes | Eric Finster | Research | Geometrically | None | Via presentations | Higher (weak) | Library | Yes | |
| Quantomatic | Yes | Aleks Kissinger et al. | Research, scale, interoperability (?) | Geometrically | Proof assistant | Via presentations | Strict, symmetric monoidal | Standalone | No | |
| Algebraic Query Language (AQL) | Yes | Ryan Wisnesky, David Spivak | Commercial, teaching | Code | Query optimizer, data migration | Explicitly, and via presentations | Monoidal | Limits, colimits, functors | Standalone + library | Yes |
| Globular | Yes | Jamie Vicary et al. | Research, publishing | Geometrically | None | Via presentations | Higher (semi-strict) | Standalone | Yes | |
| TikZit | Yes | Aleks Kissinger et al. | Publishing | LaTeX | None | Library | ||||
| Typedefs | Under development | Jelle Herold et al. | Commercial | Code | ||||||
| Proto-Quipper-M | Yes | Francisco Rios, Peter Selinger | Research | |||||||
| Rholang | Under development | Mike Stay et al. | Commercial | |||||||
| EASIK | Yes | Bob Rosebrugh et al. | Research | Geometrically | ||||||
| Cateno | Yes | Jason Morton | Research | |||||||
| PySheaf | Yes | Michael Robinson | Research | Code | ||||||
| Specware | Yes | Kestrel Institute | Commercial | |||||||
| Catlab | Under development | Evan Patterson | ||||||||
| OICOS | Under development | Viktor Winschel, Philipp Zahn | Commercial | |||||||
| Statebox | Under development | Jelle Herold et al. | Commercial | |||||||
| TikzWD | Yes | Patrick Schulz, David Spivak | Publishing | LaTeX | ||||||
| DSL for Operads | No | TBD | Simulation | Geometrically | None | Via presentations | Operads | Standalone | ||
| Common File Format for Categorical Constructions | No | TBD | Infrastructure | Code | Type-checking | Explicitly, or via presentations | All | File format |
The last two items in the table are “wish list” items identified by members of the ACT community.