What do you think of this visual category theory tool? See any issues? Would you use it? The idea behind it is that every category theoretical definition is made with visual diagrams.  One reason this is good is that we don't have to do as much language processing which is hard IMO.
Here is a mockup of the design in mspaint.

You can probably already figure out what it means.  The green portion is the implication part of the definition, the rest is the conditional part.  Namely, that diagram can easily be translated to:

Given a functor $F : C \to D$, $F$ is faithful if for any $f,g : X\to Y$ in $C$, if $F(f) = F(g) $ in $D$, then $f = g$.

So the idea is that any diagram asserted is implicitly asserted to be commutative, so all diagrams commute.
You can apply diagrammed definitions / theorems to a diagram that you draw, and thus do the some of the work of a mathematician quicker and in a format that you can share with others, in a pretty-looking form.  
Of course one tool it will have is diagram chasing, which after I get the app to understand these diagrams, should be straightforward enough.
It will be a desktop application written in PyQt5.  Would you use it in your work or as a notetaking or teaching tool?
Asserted existence arrows will be done with a dotted arrow.  I will not support special types of arrows such as $\twoheadrightarrow$, but instead prefer the word epimorphism drawn next to the arrow.  
 A: 
One reason this is good is that we don't have to do as much language processing which is hard IMO.

"We" being the developers of the software, or the users of the software? Because:
(a) in general, humans are language-processing machines, which is why games like 'Charades' and 'Pictionary' can be amusing; it's often more challenging to convey information precisely using imagery than it is by using language directly.
(b) there are many humans (such as myself) who regularly find spatially-based information more difficult to comprehend than syntactically-based information (which is why i find category theory's diagram-chasing to be challenging, and which is why algebraic topology helps me develop my 'visual intuition', so to speak). Just because many people find e.g. learning by watching a video to be easier than learning by reading an article (which i don't), don't assume this is universally (or even mostly) true.
It might be useful to read up on the history of the success of 'visual programming languages' compared to the general ongoing success of text-based programming languages; there are reasons why visually-based programming languages keep being proposed, yet haven't become the dominant paradigm.
