diagrams in computer algebra

Question to the list: I am very much interested, does there exist any practically usable system for the "computer algebra style" work with diagrams. I.e. not just write down the diagrams (like XyPic) but for example for diagram chasing, verification of commutativity in any interesting classes of categories with structure etc. As I remember there were some systems permitting computation of some limits in very limited classes of categories, also some heavy attempts of formalisation in some general purpose proof assistants but I do not know about anything else. Regards to all Sergei Soloviev [For admin and other information see: http://www.mta.ca/~cat-dist/ ]