Re: Mechanization of category theory

HAGIYA Masami (hagiya@is.s.u-tokyo.ac.jp)
Fri, 22 Mar 1996 18:08:30 +0900

We also have a thesis by an undergraduate student. He formally proved
fundamental theorems on category theory up to Yoneda's Lemma. The
purpose of the thesis was to compare formalization by set theory (in
Mizar) and formalization by type theory.

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.