There were many, many amazing discussions at the just-finished Applied Category Theory workshop in Leiden, but my favorites were two that discussed the need for an “approximate” category theory, especially in applications to the sciences.
One of the first things we realized (even if it took about an hour to figure out) was that we were really talking about three different problems:
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.
