ftp://nicosia.is.s.u-tokyo.ac.jp/pub/staff/mohri/ST.ps
-- Masami Hagiya (University of Tokyo)
---"On Formalization of Category Theory"
by Takahisa Mohri
(in March 1995)
Abstract
Category theory is important in several areas of computer science, such as semantics and implementation of functional and imperative programming languages, the design of programs, typing, et. On the other hand, in reserches called formalized mathematics, various areas of mathematics are formalized and formal proofs are checked on computers. Category theory is also one of the objects of these researches.
For category theory, there are some formalizations based on set theory or type theory(Martin-L\"of style, ECC).
In this paper, we compare the advantage and disadvantage of these formalizations. In particular, in advanced category theory including notions of functor category,set-valued functor, etc., the ability to deal with higher-order concepts and notions of sets is necessary. From this point of view, as an example, we attempt to prove Yoneda's Lemma based on each formalization.
Then we discuss which is the best method of formalization of category theory, and actually implement it on a proof system. Finally we examine required functions of a proof system for the formalization of category theory and problems on the implementation.