Toward the Automation of Category Theory
Cornell University Ithaca United States
Pagination or Media Count:
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 FunC D, E and FunC, FunD, E are naturally isomorphic.
- Computer Programming and Software