@MISC{ALTCAT_1.MIZ,
  AUTHOR = {Trybulec, Andrzej},
  TITLE = {Categories without Uniqueness of {\rm cod} and {\rm dom}},
  SECTION1 = {Preliminaries},
  SECTION2 = {Graphs},
  SECTION3 = {Many Sorted Binary Compositions},
  SECTION4 = {Categories},
  SECTION5 = {Identities},
  SECTION6 = {Discrete categories},
  DAY = {28},
  MONTH = {February},
  YEAR = {1995},
  ADDRESS1 = {Warsaw University\\Bia{\l}ystok},
  SUMMARY = {Category theory had been formalized in Mizar quite early \cite{CAT_1.ABS}.
This had
been done closely to the handbook of S. McLane \cite{MACLANE:1}. 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. \cite{BALCERZYK}, 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 \cite{SEMAD}, in the development
the category theory in Mizar. However, the beginning is not very close to
 \cite{SEMAD}, because of the approach adopted and because we work in
Tarski-Grothendieck set theory.}}

