A Formalization of Category Theory in NaDSet

ID
TR-90-23
Authors
Paul C. Gilmore and George K. Tsiknis
Publishing date
August 1990
Abstract
This paper was presented to the Sixth Workshop on Mathematical Foundations of Programming Semantics held at Queen's University, May 15-19, 1990. Because of the increasing use of category theory in programming semantics, the formalization of the theory, that is the provision of an effective definition of what constitutes a derivation for category theory, takes on an increasing importance. Nevertheless, no suitable logic within which the theory can be formalized has been provided. The classical set theories of Zermelo-Fraenkel and Godel-Bernays, for example, are not suitable because of the use category theory makes of self-referencing abstractions, such as in the theorem that the set of categories forms a category. In this paper, a formalization of category theory and a proof of the cited theorem is provided within the logic and set theory NaDSet. NaDSet definitions for natural transformations and functor categories are given and an equivalence relation on categories is defined. Additional definitions and discussions on products, comma categories, universals limits and adjoints are presented. They provide evidence that any construct, not only in categories, but also in toposes, sheaves, triples and similar theories can be formalized within NaDSet.