From: Mikhail Chekhov <firstname.lastname@example.org>
I am working on an experimental formalization of the foundations of
category theory in the object logic ZFC in HOL in Isabelle. I have already
provided a brief overview of this work in the following post on the mailing
However, today I decided to make a significant part of this (ongoing) work
available publicly: https://gitlab.com/category-theory-for-zfc-in-hol.
Please note that this post is merely a project announcement about a work in
- If you would like to build this development, you will also need to
download and build the following prerequisite:
https://gitlab.com/user9716869/Isabelle-Complement-Library. However, the
formal proof documents should be readily available from the repositories.
- I always welcome any form of contributions: reviews, objective
criticism, general advice, corrections, further material, etc.
- I cannot emphasize more that the repositories present a snapshot of an
ongoing development, not a completed work. Thus, please do not judge this
work too harshly on a variety of rough spots and dark corners that you may
encounter, if you decide to take a close look at this development.
Last updated: Dec 08 2021 at 08:24 UTC