Automating Proofs in Category Theory

Abstract. We introduce a semi-automated proof system for basic category-theoretic reasoning. It is based on a first-order sequent calculus that captures the basic properties of categories, functors and natural transformations as well as a small set of proof tactics that automate proof search in this calculus. We demonstrate our approach by automating the proof that the functor categories Fun[C ? D, E] and Fun[C, Fun[D, E]] are naturally isomorphic.

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Dexter Kozen, Christoph Kreitz, Eva Richter
• Keywords: Automated Reasoning, Basic Category-theoretic Reasoning, CADE 2006, First-order Sequent Calculus, Functor Categories Fun[c