Automated Reasoning in Category Theory
I will present a semi-automated proof system for basic
category-theoretic reasoning. Its proof calculus is an implementation
of the sequent system from Dexter Kozen's paper "Toward the automation
of category theory". I will demonstrate the capabilities of the proof
strategy by automating the proof that the functor categories
Fun[CxD,E] and Fun[C,Dun[D,E] are isomorphic.