Technical Reports

The ICICS/CS Reading Room

UBC CS TR-90-23 Summary

A Formalization of Category Theory in NaDSet, August 1990 Paul C. Gilmore and George K. Tsiknis

This paper was presented to the Sixth Workshop on Mathematical Foundations of Programming Semantics held at Queen's University, May 15-19, 1990. \nBecause 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.

If you have any questions or comments regarding this page please send mail to