[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.


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