Mechanization of category theory

Clemens Ballarin (Clemens.Ballarin@cl.cam.ac.uk)
Thu, 21 Mar 1996 16:11:48 +0100

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 anybody's
earlier experiences.

Thanks in advance,

Clemens