[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