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 <>
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
However, today I decided to make a significant part of this (ongoing) work
available publicly:
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: 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