[isabelle] New AFP entry: Category Theory



We have a new formalization of Category Theory by Alexander Katovsky:

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.
http://afp.sourceforge.net/entries/Category2.shtml

Enjoy!





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.