Categories without Uniqueness of \rm cod and \rm dom

Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

Categories without Uniqueness of \rm cod and \rm dom

Andrzej Trybulec: Warsaw University, Bialystok

Summary.

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.

MML Identifier: ALTCAT_1

The terminology and notation used in this paper have been introduced in the following articles [14] [7] [19] [15] [20] [2] [4] [5] [3] [12] [8] [9] [16] [17] [11] [18]