Email Gateway (Mar 03 2021 at 20:13): Email Gateway (Mar 03 2021 at 20:13):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
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
list:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-January/msg00002.html.
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
progress.
Remarks:
- 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.
Kind Regards,
Mikhail Chekhov
Last updated: Jan 04 2025 at 20:18 UTC