Abstract

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.

This is work in progress. Comments are appreciated.