# Category Theory

 Title: Category Theory Author: Alexander Katovsky (apk32 /at/ cam /dot/ ac /dot/ uk) Submission date: 2010-06-20 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]. BibTeX: @article{Category2-AFP, author = {Alexander Katovsky}, title = {Category Theory}, journal = {Archive of Formal Proofs}, month = jun, year = 2010, note = {\url{https://isa-afp.org/entries/Category2.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License