Email Gateway (Feb 03 2026 at 15:36): Email Gateway (Feb 03 2026 at 15:36):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Another entry revisits sets and pays careful attentions to their cardinalities to formalize small and large categories. Warning: set theory inside (https://xkcd.com/982/).
'Sets' Revisited: Working with a Large Category in Isabelle/HOL
by Eugene W. Stark
We revisit the problem of formalization of the category of sets and functions in Isabelle/HOL, regarding it as a paradigm for the formalization of other large categories. We follow a general plan in which we extend the “category” locale from our previous article with a few axioms that allow us to pass back and forth between objects and arrows internal to the category and “real” sets and functions external to it. Using this setup, we prove the standard properties of the category of sets as consequences of the properties of the external notions. A key feature is the inclusion of an axiom that allows us to obtain objects internal to the category corresponding to externally given sets. To avoid inconsistency, our framework axiomatizes a notion of “smallness” and only asserts the existence of objects corresponding to small sets. We give two “top-level” interpretations of our “sets category” locale. One uses “finite” as the notion of smallness and uses only standard HOL for its construction, which results in a small category. The other uses the axiomatic extension of HOL given by Paulson to construct an interpretation that incorporates infinite sets as well, resulting in a large (but locally small) category.
https://www.isa-afp.org/entries/Sets_Revisited.html
Enjoy!
Last updated: Feb 22 2026 at 05:16 UTC