Category theorists: would you use a software tool for diagramming / chasing?

Update:

• Source Code Repository

Screenshots:

Now the users can edit the default colors of arrows, nodes etc. using the ColorEditor:

Users can draw diagrams and store them into a Graph Database (Neo4j) seamlessly.

Here are the videos of the old version.

Please stay tuned to this post (or the repository / project on GitHub) for updates. You'll be able to download and try (on Windows) in < 1 month I project.

I will make two comments, one from the point of view of a user, and one from the point of view of a developer.

In software development, the MoSCoW method is used to define project priorities. You can use it to define what features your software Must have, what it Should have, what it Could have, and what it Won't have. If I were to define the priorities of this project, here's how I would define it:

Must Have:

• An Undo Button. If I lose tons of painstaking progress by mistakenly applying a functor and commuting-out other arrows/objects in my category, I would probably quit using this software until it had this feature.
• In a similar vein, there should be a save feature which allows me to read/write from a file and get the exact state of the diagrams (x/y positions included) or share it with others.

By the way, those are run-of-the-mill features, not specific to Category Theory. I mean, this is really solid if that's all it needs to have! Some polish is needed, but it's a piece of software with a well-define purpose and user base. The rest could be under "want", but are not essential.

Should Have:

• Extensible commuting, on arrow/functor/natural map/beyond level. This is extremely difficult, but the alternative is custom creation of cones, limits, exponent maps, subobject classifiers, etc. Maybe you could manage this programmatically through specific kinds of Kan Extensions.
• Keyboard shortcuts. Consider the user with motor function impairment, who might not be able to move the mouse very easily. Accessibility also helps power users, who may want their hands to stay on the keyboard for more inputs-per-second.

Could Have:

• Diagram commutativity designation. One of the problems I have when studying category theory in general is how difficult it is to figure out whether a diagram is commuting or not. Which diagram has commutativity? Should all the commuting arrows be explicitly shown? Where to draw the line on too much "ink"?
• Library of Kan Extensions.
• Label drawing. This is a surprisingly difficult problem.

Won't Have:

• One of your questions was: "Should I have functors fill in recursively?" Some people might like that, some people might feel that the software is taking over for them (I didn't read this whole article, but I think it's related: the experience of agency in HCI). Besides being overbearing, it might be impossible; imagine a functor loop, and having the categories spam objects and arrows until the software crashes.

As a developer, I have a couple of pieces of advice for the development process.

• Python is a great prototyping language. As you move forward, you should consider using a statically typed language. I know folks who work on large projects in Python, and they always complain about not knowing what types they're getting from which functions, and runtime errors when dealing with classes that they're not sure about, and the constant referencing of attributes and methods that cannot be automatically pulled by the IDE. Save yourself the pain.
• Open-source the project. Nothing is sadder when a promising project like is abandoned without details on how to run it, setting up environment, and so on. Community-building is tough. But the interest is there.

I look forward to the progress on this software.