Email Gateway (Oct 11 2024 at 14:54): Email Gateway (Oct 11 2024 at 14:54):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce a new entry by a couple of new contributors, James Baxter and Dustin Bryant.
The Elementary Theory of the Category of Sets
Category theory presents a formulation of mathematical structures in terms of common properties of those structures. A particular formulation of interest is the Elementary Theory of the Category of Sets (ETCS), which is an axiomatization of set theory in category theory terms. This axiomatization provides an unusual view of sets, where the functions between sets are regarded as more important than the elements of the sets. We formalise an axiomatization of ETCS on top of HOL, following the presentation given by Halvorson in "The Logic in Philosophy of Science". We also build some other set theoretic results on top of the axiomatization, including Cantor's diagonalization theorem and mathematical induction. We additionally define a system of quantified predicate logic within the ETCS axiomatization.
We have other formal developments of category theory, but unlike a certain other mathematical library, we take a permissive view of possible overlaps.
https://www.isa-afp.org/entries/Category_Set.html
Larry
Last updated: Jan 04 2025 at 20:18 UTC