Dexter Kozen. Toward the Automation of Category Theory. Technical Report TR2004-1964, Computer Science Department, Cornell University, September 2004.

We introduce a sequent system for basic category-theoretic reasoning suitable for computer implementation. We illustrate its use by giving a complete formal proof that the functor categories Fun[CxD,E] and Fun[C,Fun[D,E]] are naturally isomorphic.