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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Allen, S., et al.: Innovations in computational type theory using Nuprl. Journal of Applied Logic (to appear, 2006)
Allen, S., Constable, R., Eaton, R., Kreitz, C., Lorigo, L.: The Nuprl open logical environment. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 170–176. Springer, Heidelberg (2000)
Bancerek, G.: Concrete categories. J. formalized mathematics 13 (2001)
Bancerek, G.: Miscellaneous facts about functors. J. form. math. 13 (2001)
Bancerek, G.: Categorial background for duality theory. J. form. math. 13 (2001)
Barr, M., Wells, C.: Category Theory for Computing Science. Prentice-Hall, Englewood Cliffs (1990)
Bird, R.: A Calculus of Functions for Program Derivation, Research Topics in Functional Programming, pp. 287–307. Addison-Wesley, Reading (1990)
Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. In: Lusk, E.‘., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 111–120. Springer, Heidelberg (1988)
Constable, R., et al.: Implementing Mathematics with the Nuprl proof development system. Prentice-Hall, Englewood Cliffs (1986)
Cáccamo, M.J., Winskel, G.: A higher-order calculus for categories. Technical Report RS-01-27, BRICS, University of Aarhus (2001)
Eklund, P., et al.: A graphical approach to monad compositions. Electronic Notes in Theoretical Computer Science 40 (2002)
Eilenberg, S., MacLane, S.: General theory of natural equivalences. Trans. Amer. Math. Soc. 58, 231–244 (1945)
Glimming, J.: Logic and automation for algebra of programming. Master thesis, University of Oxford (2001)
Goguen, J.: A categorical manifesto. Mathematical Structures in Computer Science 1(1), 49–67 (1991)
Harrison, J.: Formalized mathematics. Technical report of Turku Centre for Computer Science 36 (1996)
Huet, G., Saïbi, A.: Constructive category theory. In: Joint CLICS-TYPES Workshop on Categories and Type Theory, MIT Press, Cambridge (1995)
Knuth, D., Bendix, P.: Simple word problems in universal algebra. In: Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford (1970)
Kozen, D.: Toward the automation of category theory. Technical Report 2004-1964, Computer Science Department, Cornell University (2004)
Kreitz, C.: The Nuprl Proof Development System, V5: Reference Manual and User’s Guide. Computer Science Department, Cornell University (2002)
MacLane, S.: Categories for the Working Mathematician. Springer, Heidelberg (1971)
Moggi, E.: Notions of computation and monads. Inf. and Comp. 93 (1991)
O’Keefe, G.: Towards a readable formalisation of category theory. Electronic Notes in Theoretical Computer Science, vol. 91, pp. 212–228. Elsevier, Amsterdam (2004)
Paulson, L.C.: Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)
Rydeheard, D., Burstall, R.: Computational Category Theory. Prentice-Hall, Englewood Cliffs (1988)
Reed, G.M., Roscoe, A.W., Wachter, R.F.: Topology and Category Theory in Computer Science. Oxford University Press, Oxford (1991)
Saïbi, A.: Constructive category theory (1995), http://coq.inria.fr/contribs/category.tar.gz
Simpson, C.: Category theory in ZFC (2004), coq.inria.fr/contribs/CatsInZFC.tar.gz
Takeyama, M.: Universal Structure and a Categorical Framework for Type Theory. PhD thesis, University of Edinburgh (1995)
Trybulec, A.: Some isomorphisms between functor categories. J. formalized mathematics 4 (1992)
Wadler, P.: Monads for functional programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 24–52. Springer, Heidelberg (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kozen, D., Kreitz, C., Richter, E. (2006). Automating Proofs in Category Theory. In: Furbach, U., Shankar, N. (eds) Automated Reasoning. IJCAR 2006. Lecture Notes in Computer Science(), vol 4130. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814771_34
Download citation
DOI: https://doi.org/10.1007/11814771_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37187-8
Online ISBN: 978-3-540-37188-5
eBook Packages: Computer ScienceComputer Science (R0)