After having done many tedious, robotic proofs that various arrows in a given diagram have certain properties, I've begun to wonder whether or not someone has made this automatic. You should be able to tell a program where the objects and arrows are, and which arrows have certain properties, and it should be able to list all of the provable implications.
Has this been done? Humans should no longer have to do diagram chases by hand!
I am developing a Mathematica package called WildCats which allows the computer algebra system Mathematica to perform category theory computations (even graphical computations).
The posted version 0.36 is available at https://sites.google.com/site/wildcatsformma/
A much more powerful version 0.50 will be available at the beginning of May.
The package is totally free (GPL licence), but requires the commercial Mathematica system available at www.wolfram.com. The educational, student or home editions are very moderately priced.
One of the things you can already do in Wildcats 0.36 is to apply a functor to a diagram and see the resulting diagram. In the new version 0.50, you will also be able to do diagram chasing.
Needless to say, I greatly appreciate users feedback and comments