Re: Mechanization of category theory

Bernd Ingo Dahn (dahn@mathematik.hu-berlin.de)
Fri, 22 Mar 1996 09:06:37 +0100

Category theory has been formalized in MIZAR in the following verified articles.

Ingo Dahn

55. CAT_1
Introduction to Categories and Functors
by Czes{\l}aw Byli\'nski
Received October 25, 1989

102. CAT_2
Subcategories and Products of Categories
by Czes{\l}aw Byli\'nski
Received May 31, 1990

217. OPPCAT_1
Opposite Categories and Contravariant Functors
by Czes\l aw Byli\'nski
Received February 13, 1991

225. NATTRA_1
Natural Transformations. Discrete Categories
by Andrzej Trybulec
Received May 15, 1991

236. ENS_1
Category Ens
by Czes{\l}aw Byli\'nski
Received August 1, 1991

241. GRCAT_1
Categories of Groups
by Michal Muzalewski
Received October 3, 1991

252. ISOCAT_1
Isomorphisms of Categories
by Andrzej Trybulec
Received November 22, 1991

254. RINGCAT1
Category of Rings
by Micha{\l} Muzalewski
Received December 5, 1991

255. MODCAT_1
Category of Left Modules
by Micha{\l} Muzalewski
Received December 12, 1991

265. COMMACAT
Comma Category
by Grzegorz Bancerek and Agata Darmochwa\l
Received February 20, 1992

269. CAT_3
Products and Coproducts in Categories
by Czes{\l}aw Byli\'nski
Received May 11, 1992

276. ISOCAT_2
Some Isomorphisms Between Functor Categories
by Andrzej Trybulec
Received June 5, 1992

295. CAT_4
Cartesian Categories
by Czes{\l}aw Byli\'nski
Received October 27, 1992

363. CAT_5
Categorial Categories and Slice Categories
by Grzegorz Bancerek
Received October 24, 1994

379. ALTCAT_1
Categories without Uniqueness of { \bf cod } and { \bf dom }
by Andrzej Trybulec
Received February 28, 1995

390. INDEX_1
Indexed Category
by Grzegorz Bancerek
Received June 8, 1995