Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Towards a formalization of elements of the fou...


view this post on Zulip 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: Dec 08 2021 at 08:24 UTC