Toward the Automation of Category Theory
Dexter C. Kozen · eCommons (Cornell University) · 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[C × D, E] and Fun[C, Fun[D, E]] are naturally isomorphic.