Category Theory

Alexander Katovsky 📧

June 20, 2010

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This article presents a development of Category Theory in Isabelle/HOL. A Category is defined using records and locales. Functors and Natural Transformations are also defined. The main result that has been formalized is that the Yoneda functor is a full and faithful embedding. We also formalize the completeness of many sorted monadic equational logic. Extensive use is made of the HOLZF theory in both cases. For an informal description see here [pdf].
BSD License

Topics

Theories of Category2