Email Gateway (Aug 18 2022 at 15:31): Email Gateway (Aug 18 2022 at 15:31):From: Tobias Nipkow <nipkow@in.tum.de>
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!
Last updated: Apr 25 2024 at 16:19 UTC