Mechanization of category theory

Has anybody experience in mechanizing category theory or knows of such work? I'm about to implement basic parts of category theory in a tactical theorem prover based on higher order logic. I would appreciate to learn from anybodies earlier experiences. Thanks in advance, Clemens