Toward the Automation of Category Theory
MetadataShow full item record
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.
computer science; technical report
Previously Published As