Automated Reasoning in Category Theory

by Robert L. Constable
2004-2005

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.

Automated Reasoning in Category Theory

by Robert L. Constable 2004-2005

by Robert L. Constable
2004-2005