Calculate categorically!
Maarten M. Fokkinga · Formal Aspects of Computing · 1992
Abstract Diagram chasing is an established proof technique in Category Theory. Algebraic calculation is a good alternative; made possible thanks to a notation for various unique arrows and a suitable formulation of initiality, and the calculational properties brought forward by initiality.