Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

**Andrzej Trybulec**- Warsaw University, Bialystok

- We continue the development of the category theory basically following [8] (compare also [7]). We define the concept of isomorphic categories and prove basic facts related, e.g. that the Cartesian product of categories is associative up to the isomorphism. We introduce the composition of a functor and a transformation, and of transformation and a functor, and afterwards we define again those concepts for natural transformations. Let us observe, that we have to duplicate those concepts because of the permissiveness: if a functor $F$ is not naturally transformable to $G$, then natural transformation from $F$ to $G$ has no fixed meaning, hence we cannot claim that the composition of it with a functor as a transformation results in a natural transformation. We define also the so called horizontal composition of transformations ([8], p.~140, exercise {\bf 4}.{\bf 2},{\bf 5}(C)) and prove {\em interchange law} ([7], p.44). We conclude with the definition of equivalent categories.

Contents (PDF format)

- [1]
Czeslaw Bylinski.
Basic functions and operations on functions.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [3]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Czeslaw Bylinski.
Introduction to categories and functors.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Czeslaw Bylinski.
Some basic properties of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [6]
Czeslaw Bylinski.
Subcategories and products of categories.
*Journal of Formalized Mathematics*, 2, 1990. - [7] Saunders Mac Lane. \em Categories for the Working Mathematician, volume 5 of \em Graduate Texts in Mathematics. Springer Verlag, New York, Heidelberg, Berlin, 1971.
- [8] Zbigniew Semadeni and Antoni Wiweger. \em Wst\c ep do teorii kategorii i funktorow, volume 45 of \em Biblioteka Matematyczna. PWN, Warszawa, 1978.
- [9]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [10]
Andrzej Trybulec.
Natural transformations. Discrete categories.
*Journal of Formalized Mathematics*, 3, 1991. - [11]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989.

[ Download a postscript version, MML identifier index, Mizar home page]