Skip to main content
PRL Project

Automating Proofs in Category Theory

by Dexter Kozen, Christoph Kreitz, Eva Richter

Proceedings of 3rd International Joint Conference on Automated Reasoning (IJCAR 2006)

  • unofficial copies PDF, PS

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[CxD,E] and Fun[C,Fun[D,E]] are naturally isomorphic.

bibTex ref: KKR06

cite link