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

## Natural transformations. Discrete categories

Andrzej Trybulec
Warsaw University, Bialystok

### Summary.

We present well known concepts of category theory: natural transformations and functor categories, and prove propositions related to. Because of the formalization it proved to be convenient to introduce some auxiliary notions, for instance: transformations. We mean by a transformation of a functor $F$ to a functor $G$, both covariant functors from $A$ to $B$, a function mapping the objects of $A$ to the morphisms of $B$ and assigning to an object $a$ of $A$ an element of $\mathop{\rm Hom}(F(a),G(a))$. The material included roughly corresponds to that presented on pages 18,129-130,137-138 of the monography ([9]). We also introduce discrete categories and prove some propositions to illustrate the concepts introduced.

#### MML Identifier: NATTRA_1

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

#### Contents (PDF format)

1. Preliminaries
2. Application of a functor to a morphism
3. Transformations
4. Natural transformations
5. Functor category
6. Discrete categories

#### Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. 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. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.
[7] Czeslaw Bylinski. Subcategories and products of categories. Journal of Formalized Mathematics, 2, 1990.
[8] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[9] Zbigniew Semadeni and Antoni Wiweger. \em Wst\c ep do teorii kategorii i funktorow, volume 45 of \em Biblioteka Matematyczna. PWN, Warszawa, 1978.
[10] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[11] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[12] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[13] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.