Theory CZH_Introduction
chapter‹Introduction›
theory CZH_Introduction
imports ZFC_in_HOL.ZFC_Typeclasses
begin
section‹Background›
text‹
This article presents a foundational framework
that will be used for the formalization of
elements of the theory of 1-categories in the object logic
‹ZFC in HOL› (\<^cite>‹"paulson_zermelo_2019"›, also see
\<^cite>‹"barkaoui_partizan_2006"›) of the formal proof assistant
‹Isabelle› \<^cite>‹"paulson_natural_1986"› in future articles.
It is important to note that this chapter serves as
an introduction to the entire development and not merely
its foundational part.
There already exist several formalizations of the foundations of category
theory in Isabelle. In the context of the work presented here, the most relevant
formalizations (listed in the chronological order) are
\<^cite>‹"caccamo_higher-order_2001-1" and "caccamo_higher-order_2001"›,
\<^cite>‹"okeefe_category_2005"›, \<^cite>‹"katovsky_category_2010"› and
\<^cite>‹"stark_category_2016"›.
Arguably, the most well developed and maintained entry is
\<^cite>‹"stark_category_2016"›: it subsumes the majority of the content of
\<^cite>‹"okeefe_category_2005"› and \<^cite>‹"katovsky_category_2010"›.
From the perspective of the methodology that was chosen for the formalization,
this work differs significantly from the aforementioned previous work.
In particular, the categories are modelled as terms of the type \<^typ>‹V›
and no attempt is made to generalize the concept of a category to arbitrary
types. The inspiration for the chosen approach is drawn from
\<^cite>‹"feferman_set-theoretical_1969"›,
\<^cite>‹"sica_doing_2006"› and \<^cite>‹"shulman_set_2008"›.
The primary references for this work are
‹Categories for the Working Mathematician› \<^cite>‹"mac_lane_categories_2010"›
by Saunders Mac Lane, ‹Category Theory in Context›
by Emily Riehl \<^cite>‹"riehl_category_2016"› and
‹Categories and Functors› by Bodo Pareigis \<^cite>‹"bodo_categories_1970"›.
The secondary sources of information include the textbooks
\<^cite>‹"adamek_abstract_2006"› and \<^cite>‹"hungerford_algebra_2003"›,
as well as several online encyclopedias
(including \<^cite>‹"noauthor_nlab_nodate"›,
\<^cite>‹"noauthor_wikipedia_2001"›,
\<^cite>‹"noauthor_proofwiki_nodate"›
and \<^cite>‹"noauthor_encyclopedia_nodate"›).
Of course, inspiration was also drawn from the previous formalizations of
category theory in Isabelle.
It is likely that none of the content that is formalized in this work
is original in nature. However, explicit citations
are not provided for many results that were deemed to be trivial.
›
section‹Related and previous work›
text‹
To the best knowledge of the author, this work is the first attempt
to develop a formalization of elements of category theory in the
object logic ZFC in HOL by modelling categories as terms of the type \<^typ>‹V›.
However, it should be noted that the formalization of category theory in
\<^cite>‹"katovsky_category_2010"› largely rested
on the object logic HOL/ZF \<^cite>‹"barkaoui_partizan_2006"›, which is
equiconsistent with the ZFC in HOL \<^cite>‹"paulson_zermelo_2019"›.
Nonetheless, in \<^cite>‹"katovsky_category_2010"›, the objects and arrows
associated with categories were modelled as terms of arbitrary
types. The object logic HOL/ZF was used for the exposition of
the category ‹Set› of all sets and functions between them
and a variety of closely related concepts.
In this sense, the methodology employed in
\<^cite>‹"katovsky_category_2010"› could be seen as a combination of the
methodology employed in this work and the methodology followed in
\<^cite>‹"okeefe_category_2005"› and \<^cite>‹"stark_category_2016"›.
Furthermore, in \<^cite>‹"chen_hotg_2021"›,
the authors have experimented with the formalization of category
theory in Higher-Order Tarski-Grothendieck (HOTG)
theory \<^cite>‹"brown_higher-order_2019"› using a methodology that
shares many similarities with the approach that was chosen in this study.
The formalizations of various elements of category theory
in other proof assistants are abundant.
While a survey of such formalizations is outside of the scope of
this work, it is important to note that there exist at least two examples
of the formalization of elements of category theory in a set-theoretic setting
similar to the one that is used in this work.
More specifically, elements of category theory were formalized in
the Tarski-Grothendieck Set Theory in the Mizar proof assistant
\<^cite>‹"noauthor_association_nodate"› (and
published in the associated electronic journal
\<^cite>‹"grabowski_preface_2014"›)
and the proof assistant Metamath
\<^cite>‹"megill_metamath_2019"›.
The following references contain some of the
relevant articles in \<^cite>‹"grabowski_preface_2014"›, but the list may not be
exhaustive:
\<^cite>‹"bylinski_introduction_1990" and "bylinski_subcategories_1990" and "bylinski_opposite_1991" and "trybulec_natural_1991" and "bylinski_category_1991" and "muzalewski_categories_1991" and "trybulec_isomorphisms_1991" and "muzalewski_category_1991" and "muzalewski_category_1991-1" and "bancerek_comma_1991" and "bylinski_products_1991" and "trybulec_isomorphisms_1992" and "bylinski_cartesian_1992" and "bancerek_categorial_1996" and "trybulec_categories_1996" and "bancerek_indexed_1996" and "trybulec_functors_1996" and "nieszczerzewski_category_1997" and "kornilowicz_categories_1997" and "kornilowicz_composition_1998" and "bancerek_concrete_2001" and "kornilowicz_products_2012" and "riccardi_object-free_2013" and "golinski_coproducts_2013" and "riccardi_categorical_2015" and "riccardi_exponential_2015"›.
›
end