Volume 7, 1995

University of Bialystok

Copyright (c) 1995 Association of Mizar Users

**Andrzej Trybulec**- Warsaw University, Bialystok

- Category theory had been formalized in Mizar quite early [6]. This had been done closely to the handbook of S. McLane [10]. In this paper we use a different approach. Category is a triple $$\langle O, {\{ \langle o_1,o_2 \rangle \}}_{o_1,o_2 \in O}, {\{ \circ_{o_1,o_2,o_3}\}}_{o_1,o_2,o_3 \in O} \rangle$$ where $\circ_{o_1,o_2,o_3}: \langle o_2,o_3 \rangle \times \langle o_1,o_2 \rangle \to \langle o_1, o_3 \rangle$ that satisfies usual conditions (associativity and the existence of the identities). This approach is closer to the way in which categories are presented in homological algebra (e.g. [1], pp.58-59). We do not assume that $\langle o_1,o_2 \rangle$'s are mutually disjoint. If $f$ is simultaneously a morphism from $o_1$ to $o_2$ and $o_1'$ to $o_2$ ($o_1 \neq o_1'$) than different compositions are used ($\circ_{o_1,o_2,o_3}$ or $\circ_{o_1',o_2,o_3}$) to compose it with a morphism $g$ from $o_2$ to $o_3$. The operation $g\cdot f$ has actually six arguments (two visible and four hidden: three objects and the category).\par We introduce some simple properties of categories. Perhaps more than necessary. It is partially caused by the formalization. The functional categories are characterized by the following properties: \begin{itemize} \item quasi-functional that means that morphisms are functions (rather meaningless, if it stands alone) \item semi-functional that means that the composition of morphism is the composition of functions, provided they are functions. \item pseudo-functional that means that the composition of morphisms is the composition of functions. \end{itemize} For categories pseudo-functional is just quasi-functional and semi-functional, but we work in a bit more general setting. Similarly the concept of a discrete category is split into two: \begin{itemize} \item quasi-discrete that means that $\langle o_1,o_2 \rangle$ is empty for $o_1 \neq o_2$ and \item pseudo-discrete that means that $\langle o, o \rangle$ is trivial, i.e. consists of the identity only, in a category. \end{itemize}\par We plan to follow Semadeni-Wiweger book [13], in the development the category theory in Mizar. However, the beginning is not very close to [13], because of the approach adopted and because we work in Tarski-Grothendieck set theory.

- Preliminaries
- Graphs
- Many Sorted Binary Compositions
- Categories
- Identities
- Discrete categories

- [1] Stanislaw Balcerzyk. \em Wstep do algebry homologicznej, volume 34 of \em Biblioteka Matematyczna. PWN, Warszawa, 1972.
- [2]
Jozef Bialas.
Group and field definitions.
*Journal of Formalized Mathematics*, 1, 1989. - [3]
Czeslaw Bylinski.
Binary operations.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [6]
Czeslaw Bylinski.
Introduction to categories and functors.
*Journal of Formalized Mathematics*, 1, 1989. - [7]
Czeslaw Bylinski.
Some basic properties of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [8]
Czeslaw Bylinski.
A classical first order language.
*Journal of Formalized Mathematics*, 2, 1990. - [9]
Czeslaw Bylinski.
Cartesian categories.
*Journal of Formalized Mathematics*, 4, 1992. - [10] Saunders Mac Lane. \em Categories for the Working Mathematician, volume 5 of \em Graduate Texts in Mathematics. Springer Verlag, New York, Heidelberg, Berlin, 1971.
- [11]
Beata Madras.
Product of family of universal algebras.
*Journal of Formalized Mathematics*, 5, 1993. - [12]
Michal Muzalewski and Wojciech Skaba.
Three-argument operations and four-argument operations.
*Journal of Formalized Mathematics*, 2, 1990. - [13] Zbigniew Semadeni and Antoni Wiweger. \em Wst\c ep do teorii kategorii i funktorow, volume 45 of \em Biblioteka Matematyczna. PWN, Warszawa, 1978.
- [14]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [15]
Andrzej Trybulec.
Tuples, projections and Cartesian products.
*Journal of Formalized Mathematics*, 1, 1989. - [16]
Andrzej Trybulec.
Function domains and Fr\aenkel operator.
*Journal of Formalized Mathematics*, 2, 1990. - [17]
Andrzej Trybulec.
Many-sorted sets.
*Journal of Formalized Mathematics*, 5, 1993. - [18]
Andrzej Trybulec.
Many sorted algebras.
*Journal of Formalized Mathematics*, 6, 1994. - [19]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [20]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989.

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