Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

## Isomorphisms of Categories

Andrzej Trybulec
Warsaw University, Bialystok

### Summary.

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.

#### MML Identifier: ISOCAT_1

The terminology and notation used in this paper have been introduced in the following articles [9] [5] [11] [2] [3] [1] [4] [6] [10]

Contents (PDF format)

#### Bibliography

[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.