I once formalised some of the concepts of category theory in HOL, as far as
adjunction, without undertaking any theorem proving. I felt this to be
helpful in improving my understanding of these basic concepts
I also attempted to construct a pure theory of functors analogous to pure
set theories (i.e. something like ZFC, where you have a large Universe
consisting only of sets, except that everything in the pure functor theory
is a functor). This was done in what I then called ZF-HOL, a straightforward
axiomatisation of ZFC in HOL, back in 1988.
Previously I had done a pure function theory and some other systems with
more complicated primitive objects, all of which went through reasonably well.
However, I screwed up with the functor theory and, ended up with not enough
functors to make a foundation system, and never got round to fixing the
problem (I was only playing around with the functors).
Roger Jones http://www.cybercom.net/~rbjones/
at home rbj@campion.demon.co.uk