# The ICICS/CS Reading Room

## UBC CS TR-90-23 Summary

- No on-line copy of this technical report is available.

- 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
help@cs.ubc.ca.