objectsmorphisms.tex

%% -*- coding:utf-8 -*-
\chapter{Objects and morphisms}

\section{Equality}

The important question is how we can decide whenever an
object/morphism is equal to another object/morphism. The trivial
answer is possible if the \mynameref{def:object} is a
\mynameref{def:set}. In the case we can say that 2 objects are equal
if they contain the equivalent collection of elements. Unfortunately
we cannot do the same trick for categorical \mynameref{def:object}s as
soon as they don't have any internal 
structure but can use a \mynameref{def:categorical_approach} (see \cref{ch:categorical_approach}) i.e. if we cannot use a ``microscope'' lets
use a ``telescope'' and define the equality of objects and morphisms of
a category $\cat{C}$ in the terms of whole $\cathom{C}$.

\begin{definition}[Objects equality]
\label{def:object_equality}
Two \mynameref{def:object}s $a$ and $b$ in \mynameref{def:category}
$\cat{C}$ are equal if there exists an unique
\mynameref{def:isomorphism} $a \cong_f b$. This also means that
there exists an unique isomorphism $b \cong_g a$. These two
\mynameref{def:morphism}s ($f$ and $g$) are related each other via 
the following equations: $f \circ g = \idm{a}$ and $g \circ f
= \idm{b}$. 
\end{definition}

Unlike \mynameref{def:function}s between \mynameref{def:set}s we don't
have any additional info 
\footnote{
for instance info about sets internals. i.e. which elements of the sets
are connected by the considered functions
}
about \mynameref{def:morphism}s except
category theory axioms which the morphisms satisfy 
\cite{bib:stackexchange:morphism:equality}. This leads us to the
following definition of morphims equality:
\begin{definition}[Morphisms equality]
\label{def:morphism_equality}
Two \mynameref{def:morphism}s $f$ and $g$ in \mynameref{def:category}
$\cat{C}$ are equal if the equality can be derived from the base axioms: 
\begin{itemize}
\item \mynameref{axm:composition}
\item \mynameref{axm:associativity}
\item \mynameref{def:id}: \eqref{eq:leftid}, \eqref{eq:rightid}
\end{itemize}
or \mynameref{def:commutative_diagram}s which postulate the equality.
\end{definition}
As an example lets proof the following theorem
\begin{theorem}[Identity is unique]
\label{thm:identity_unique}
The \mynameref{def:id} is unique.
\begin{proof}
Consider an \mynameref{def:object} $a$ and it's \mynameref{def:id} 
$\idm{a}$. Assume existence of a function $f: a \to a$ such that $f$ is also
identity. \eqref{eq:leftid}, for $f$ as identity, gives us
\[
f \circ \idm{a} = \idm{a}.
\]
From other side \eqref{eq:rightid} for $\idm{a}$ satisfied
\[
f \circ \idm{a} = f
\]
i.e.
\[
f = f \circ \idm{a} = \idm{a}
\] 
or
$f = \idm{a}$.
\end{proof}
\end{theorem}

\section{Initial and terminal objects}

\subsection{Initial object}

\begin{definition}[Initial object]
\label{def:initial_object}
Let $\cat{C}$ is a \mynameref{def:category}, the
\mynameref{def:object} $i \in \catob{C}$ is called
\textit{initial object} if $\forall x \in \catob{C}
\exists! f_x: i \to x \in \cathom{C}$.
\end{definition}

\begin{example}[Initial object][$\cat{Set}$]
\label{ex:set_initial_object}
Note that there is only one function from empty set to any other sets
\cite{bib:proofwiki:Empty_Mapping_is_Unique} that makes the empty set
as the \mynameref{def:initial_object} in \mynameref{def:setcategory}. 
\end{example}

\begin{theorem}[Initial object is unique]
\label{thm:initial_object_unique}
Let $\cat{C}$ is a category and $i, i' \in \catob{C}$ two
\mynameref{def:initial_object}s then there exists an unique
\mynameref{def:isomorphism} $u: i \to i'$ (see
\mynameref{def:object_equality}) 
\begin{proof}
Consider the following \mynameref{def:commutative_diagram} (see
\cref{fig:initial_object_unique}). As soon as $i$ initial object
$\exists! \, u: i \to i'$. From other side $i'$ is also initial object
and therefore $\exists! \, u^{-1}: i' \to i$. Combining them together
via composition we can get $u^{-1} \circ u: i \to i$ and $u \circ
u^{-1}: i' \to i'$. From the fact that $i$ is initial object one can
get that there exists
only one morphism $\idm{i}: i \to i$. The same is the truth for $i'$.
Therefore $u^{-1} \circ u = \idm{i}$ and $u \circ u^{-1} = \idm{i'}$.
These complete the commutative diagram build and finishes the proof. 
\begin{figure}
  \centering
  \begin{tikzpicture}[ele/.style={fill=black,circle,minimum
        width=.8pt,inner sep=1pt},every fit/.style={ellipse,draw,inner
        sep=-2pt}]

    % the texts
    
    \node[ele,label=above:$i$] (i1) at (0,3) {};    
    \node[ele,label=above:$i'$] (i2) at (3,3) {};    
    \node[ele,label=below:$i$] (i12) at (3,0) {};
    \node[ele,label=below:$i'$] (i22) at (6,0) {};

    \draw[->,thick,shorten <=2pt,shorten >=2pt] (i1) to
    node[sloped,above]{$u$} (i2);
    \draw[->,thick,shorten <=2pt,shorten >=2] (i12) to
    node[sloped,above]{$u$} (i22); 
    \draw[->,thick,shorten <=2pt,shorten >=2] (i1) to
    node[sloped,above]{$\idm{i}$} (i12); 
    \draw[->,thick,shorten <=2pt,shorten >=2] (i2) to
    node[sloped,above]{$\idm{i'}$} (i22); 
    \draw[->,thick,shorten <=2pt,shorten >=2] (i2) to
    node[right]{$u^{-1}$} (i12); 
  \end{tikzpicture}
  \caption{Commutative diagram for initial object uniqueness  proof}
  \label{fig:initial_object_unique}
\end{figure}
\end{proof}
\end{theorem}

\subsection{Terminal object}

\begin{definition}[Terminal object]
\label{def:terminal_object}
Let $\cat{C}$ is a \mynameref{def:category}, the
\mynameref{def:object} $t \in \catob{C}$ is called
\textit{terminal object} if $\forall x \in \catob{C}
\exists! g_x: x \to t \in \cathom{C}$.
\end{definition}

\begin{example}[Terminal object][$\cat{Set}$]
\label{ex:set_terminal_object}
\mynameref{def:terminal_object} in \mynameref{def:setcategory} is a set
with one element i.e \mynameref{def:singleton_set}. 
\end{example}

As you can see the initial and terminal objects are opposite each
other. I.e. if $i$ is an \mynameref{def:initial_object} in $\cat{C}$
then it will be \mynameref{def:terminal_object} in
the \mynameref{def:op_category} $\cat{C^{op}}$.

\begin{theorem}[Terminal object is unique]
\label{thm:terminal_object_unique}
Let $\cat{C}$ is a category and $t, t' \in \catob{C}$ two
\mynameref{def:terminal_object}s then there exists an unique
\mynameref{def:isomorphism} $v: t' \to t$ (see
\mynameref{def:object_equality}) 
\begin{proof}
Just got to the \mynameref{def:op_category} and revert 
\mynameref{def:arrow}s in
\cref{fig:initial_object_unique}. The result shown on
\cref{fig:terminal_object_unique} and it proofs the theorem statement.
\begin{figure}
  \centering
  \begin{tikzpicture}[ele/.style={fill=black,circle,minimum
        width=.8pt,inner sep=1pt},every fit/.style={ellipse,draw,inner
        sep=-2pt}]

    % the texts
    
    \node[ele,label=above:$t$] (t1) at (0,3) {};    
    \node[ele,label=above:$t'$] (t2) at (3,3) {};    
    \node[ele,label=below:$t$] (t12) at (3,0) {};
    \node[ele,label=below:$t'$] (t22) at (6,0) {};

    \draw[->,thick,shorten <=2pt,shorten >=2pt] (t2) to
    node[sloped,above]{$v$} (t1);
    \draw[->,thick,shorten <=2pt,shorten >=2] (t22) to
    node[sloped,above]{$v^{-1}$} (t12); 
    \draw[->,thick,shorten <=2pt,shorten >=2] (t12) to
    node[sloped,above]{$\idm{t}$} (t1); 
    \draw[->,thick,shorten <=2pt,shorten >=2] (t22) to
    node[sloped,above]{$\idm{t'}$} (t2); 
    \draw[->,thick,shorten <=2pt,shorten >=2] (t12) to
    node[right]{$v^{-1}$} (t2); 
  \end{tikzpicture}
  \caption{Commutative diagram for terminal object uniqueness proof}
  \label{fig:terminal_object_unique}
\end{figure}
\end{proof}
\end{theorem}

\subsection{Toy example}

\begin{example}[Toy example]
In our toy example \cref{fig:pl_example} the type String is
\mynameref{def:initial_object} and type Bool is the
\mynameref{def:terminal_object}.
\end{example}

\section{Product and sum}
\label{sec:product_and_sum}
\subsection{Product}
The pair of 2 objects is defined via the \mynameref{def:universalproperty} in
the following way:
\begin{definition}[Product]
\label{def:product}
Let we have a category $\cat{C}$ and $c_1, c_2 \in \catob{C}$ -two
\mynameref{def:object}s then the product of the objects $c_1, c_2$ is
another object in $\cat{C}$ $c = c_1 \times c_2$ with 2
\mynameref{def:morphism}s $\pi_1, \pi_2$ such that $c_1 = \pi_1(c),
c_2 = \pi(c)$ and the  
following universal property is satisfied: $\forall c' \in \catob{C}$
and morphisms $\pi'_1: c' \to c_1, \pi'_2: c' \to c_2$, exists unique
morphism $h$ such that the following diagram (see \cref{fig:product})
commutes, i.e. 
\begin{eqnarray}
\pi'_1 = \pi_1 \circ h, 
\nonumber \\
\pi'_2 = \pi_2 \circ h.
\label{eq:product}
\end{eqnarray}
\begin{figure}[H]
  \centering
  \begin{tikzpicture}[ele/.style={fill=black,circle,minimum
        width=.8pt,inner sep=1pt},every fit/.style={ellipse,draw,inner
        sep=-2pt}]

    % the texts
    
    \node[ele,label=left:$c_1$] (a) at (0,0) {};    
    \node[ele,label=right:$c_2$] (b) at (4,0) {};    
    \node[ele,label=below:$c$] (c) at (2,0) {};
    \node[ele,label=above:$c'$] (c') at (2,3) {};

    \draw[->,thick,shorten <=2pt,shorten >=2pt] (c) to
    node[sloped,above]{$\pi_1$} (a);
    \draw[->,thick,shorten <=2pt,shorten >=2] (c) to
    node[sloped,above]{$\pi_2$} (b); 
    \draw[->,thick,shorten <=2pt,shorten >=2] (c') to
    node[sloped,above]{$\pi'_1$} (a); 
    \draw[->,thick,shorten <=2pt,shorten >=2] (c') to
    node[sloped,above]{$\pi'_2$} (b); 
    \draw[->,thick,shorten <=2pt,shorten >=2] (c') to
    node[right]{$h$} (c); 
  \end{tikzpicture}
  \caption{Product $c = c_1 \times c_2$. $\forall c, \exists! h \in
    \cathom{C}: \pi'_1 = \pi_1 \circ h, \pi'_2 = \pi_2 \circ h$.}
  \label{fig:product}
\end{figure}
In other words $h$ factorizes $\pi'_{1,2}$.
\end{definition}

\begin{example}[Product][$\cat{Set}$]
\label{ex:set_product}
\mynameref{def:cartesian_product}: $C = A \times B = \{(a,b)| a \in
A, b \in B\}$ is the \mynameref{def:product} of two sets $A$ and $B$ in
\mynameref{def:setcategory}. 
We have only one option for $\pi_{1,2}$:
\begin{eqnarray}
\pi_1 : (a,b) \to a \in A,
\nonumber \\
\pi_2 : (a,b) \to b \in B.
\nonumber
\end{eqnarray}
Consider also another candidate: $C' = A \times A
\times B \times B =
\{(a_1,a_2,b_1, b_2)| a_{1,2} \in A, b_{1,2} \in B\}$.
There are different options for $\pi'_1$ and $\pi'_2$. Lets choose the
  following ones:
\begin{eqnarray}
\pi'_1 : (a_1,a_2,b_1, b_2) \to a_1 \in A,
\nonumber \\
\pi'_2 : (a_1,a_2,b_1, b_2) \to b_2 \in B.
\nonumber
\end{eqnarray}
We have only one morphism $h$ that satisfied conditions
\eqref{eq:product}:
\[
h: (a_1,a_2,b_1, b_2) \to (a_1, b_2) \in A \times B
\]
that is accordingly with the \mynameref{def:product} definition for $C = A
\times B$.

If $C'$ had been the \mynameref{def:product} then it would have
satisfied the following factorization conditions:
\begin{eqnarray}
\pi_1 = \pi'_1 \circ h', 
\nonumber \\
\pi_2 = \pi'_2 \circ h',
\label{eq:productex}
\end{eqnarray}
where $h'$ would have been an unique morphism.
From other side there are a lot of morphisms $h'$ which factorize
$\pi_{1,2}$ accordingly \eqref{eq:productex}:
\[
h' : (a,b) \to (a, \bar{a}, \bar{b}, b),
\] 
where $\bar{a}$ can be replaced with any element from $A$ and
$\bar{b}$ can be replaced with any element of $B$. Therefore $C'$ can
not be considered as the \mynameref{def:product} of $A$ and $B$.
\end{example}

The \mynameref{def:product} of objects will provide also a definition
for product of morphisms
\begin{definition}[Product of morphisms]
\label{def:product_of_morphisms}
Let $\cat{C}$ is a category and $a,a' \in \catob{C}$ and 
$b, b' \in \catob{C}$ are 2 pairs of \mynameref{def:object}s that admit
\cref{def:product}. Consider 2 morphisms that connects the objects: 
$f: a \to b, f': a' \to b'$ then we can create a new unique morphism that
connects the products: $f \times f': a \times a' \to b \times b'$ and
makes the diagram commute (see \cref{fig:product_of_morphisms}). 

\begin{figure}[H]
  \centering
  \begin{tikzpicture}[ele/.style={fill=black,circle,minimum
        width=.8pt,inner sep=1pt},every fit/.style={ellipse,draw,inner
        sep=-2pt}]

    % the texts
    
    \node[ele,label=above:$a$] (a) at (0,2) {};    
    \node[ele,label=above:$a \times a'$] (aa') at (2,2) {};    
    \node[ele,label=above:$a'$] (a') at (4,2) {};    
    \node[ele,label=below:$b$] (b) at (0,0) {};    
    \node[ele,label=below:$b \times b'$] (bb') at (2,0) {};    
    \node[ele,label=below:$b'$] (b') at (4,0) {};    

    \draw[->,thick,shorten <=2pt,shorten >=2pt] (a) to
    node[sloped,above]{$f$} (b);
    \draw[->,thick,shorten <=2pt,shorten >=2pt] (a') to
    node[sloped,above]{$f'$} (b');
    \draw[->,thick,shorten <=2pt,shorten >=2pt] (aa') to
    node[sloped,above]{$f \times f'$} (bb');


    \draw[->,thick,shorten <=2pt,shorten >=2pt] (aa') to
    node[sloped,above]{$\pi_a$} (a);
    \draw[->,thick,shorten <=2pt,shorten >=2] (aa') to
    node[sloped,above]{$\pi_{a'}$} (a'); 
    \draw[->,thick,shorten <=2pt,shorten >=2pt] (bb') to
    node[sloped,above]{$\pi_b$} (b);
    \draw[->,thick,shorten <=2pt,shorten >=2] (bb') to
    node[sloped,above]{$\pi_{b'}$} (b'); 
  \end{tikzpicture}
  \caption{Product of morphisms.}
  \label{fig:product_of_morphisms}
\end{figure}
\end{definition} 

\subsection{Sum}

If we invert \mynameref{def:arrow}s in \mynameref{def:product} we shall
got another 
object definition that is called sum

\begin{definition}[Sum]
\label{def:sum}
Let we have a category $\cat{C}$ and $c_1, c_2 \in \catob{C}$ -two
\mynameref{def:object}s then the sum of the objects $c_1, c_2$ is
another object in $\cat{C}$ $c = c_1 \oplus c_2$ with 2
\mynameref{def:morphism}s $i_1, i_2$ such that $c = i_1(c_1), c = i_2
(c_2)$ and the 
following \mynameref{def:universalproperty} is satisfied: $\forall c'
\in \catob{C}$ 
and morphisms $i'_1: c_1 \to c', i'_2: c_2 \to c'$, exists unique
morphism $h$ such that the following diagram (see \cref{fig:sum})
commutes, i.e. $i'_1 = h \circ i_1, i'_2 = h \circ i_2$.
\begin{figure}[H]
  \centering
  \begin{tikzpicture}[ele/.style={fill=black,circle,minimum
        width=.8pt,inner sep=1pt},every fit/.style={ellipse,draw,inner
        sep=-2pt}]

    % the texts
    
    \node[ele,label=left:$c_1$] (a) at (0,0) {};    
    \node[ele,label=right:$c_2$] (b) at (4,0) {};    
    \node[ele,label=below:$c$] (c) at (2,0) {};
    \node[ele,label=above:$c'$] (c') at (2,3) {};

    \draw[->,thick,shorten <=2pt,shorten >=2pt] (a) to
    node[sloped,above]{$i_1$} (c);
    \draw[->,thick,shorten <=2pt,shorten >=2] (b) to
    node[sloped,above]{$i_2$} (c); 
    \draw[->,thick,shorten <=2pt,shorten >=2] (a) to
    node[sloped,above]{$i'_1$} (c'); 
    \draw[->,thick,shorten <=2pt,shorten >=2] (b) to
    node[sloped,above]{$i'_2$} (c'); 
    \draw[->,thick,shorten <=2pt,shorten >=2] (c) to
    node[right]{$h$} (c'); 
  \end{tikzpicture}
  \caption{Sum $c = c_1 \oplus c_2$. $\forall c, \exists! h \in
    \cathom{C}: i'_1 = h \circ i_1, i'_2 = h \circ i_2 $.}
  \label{fig:sum}
\end{figure}
In other words $h$ factorizes $i'_{1,2}$.

The categorical sum is also called as \textit{coproduct}.
\index{coproduct}
\end{definition}

\begin{definition}[Disjoint union]
  \label{def:disjoint_union}
  Let $\{A_i: i \in I\}$ be a family of sets 
  indexed by $I$. The 
  \textit{disjoint union} \cite{wiki:disjointunion} of this family is
  the set 
  \[
  \sqcup_{i \in I} A_i = \cup_{i \in I}\left\{
  \left(x, i\right): x \in A_i
  \right\}.
  \]
  The elements of the disjoint union are ordered pairs $(x, i)$. Here $i$
  serves as an auxiliary index that indicates which $A_i$ the element $x$
  came from.
\end{definition}

\begin{example}[Sum][$\cat{Set}$]
  \label{ex:set_sum}
  \mynameref{def:disjoint_union} is the \mynameref{def:sum} of two sets $A$ and $B$ in
  \mynameref{def:setcategory}.  
\end{example}

\begin{remark}[Sum sign]
In the book we shall use $\oplus$ as the sign for the categorical
\mynameref{def:sum}. The \mynameref{def:disjoint_union} sign $\sqcup$
is also used
\footnote{but not in the book} as the sign for categorical sum
\cite{wiki:coproduct}. 
\end{remark}

\section{Category as a monoid}
\label{sec:category_as_monoid}
Consider the following definition from abstract algebra
\begin{definition}[Monoid]
  \label{def:monoid}
  The set of elements $M$ with defined binary operation $\circ$ we shall call
  as a monoid if the following conditions are satisfied.
  \begin{enumerate}
  \item Closure: $\forall a, b \in M$: $a \circ b \in M$
  \item Associativity: $\forall a, b, c \in M:$ 
    \begin{equation}
      \label{eq:monoid_associativity}
      a \circ \left( b \circ c \right) =
      \left( a \circ b \right) \circ c
    \end{equation}
  \item Identity element: $\exists e \in M$ such that $\forall a \in M$:
    \begin{equation}
      \label{eq:monoid_identity_element}
      e \circ a = a \circ e = a
    \end{equation}    
  \end{enumerate}
\end{definition}

\begin{example}[Monoid]
\mynameref{def:monoid} concept is widely spread in math. Especially
integer numbers form a monoid under summation operation. They also
form another monoid under multiplication operation. The element
\textbf{0} is used as identity in summation and \textbf{1} is used as
the identity in multiplication. 
\end{example}

\begin{example}[Monoid][$\cat{Hask}$]
There is an declaration of Monoid in $\cat{Hask}$ category
\begin{minted}{haskell}
class Monoid m where
    mappend :: m -> m -> m
    mempty :: m
\end{minted}
There is a binary operation \textbf{mappend} and the identity
\textbf{mempty}. As it was mentioned in the \mynameref{def:monoid}
definition (see \cref{def:monoid}), the binary operation should
satisfy the associativity \eqref{eq:monoid_associativity} and identity
element \eqref{eq:monoid_identity_element} properties. This is a
responsibility of a particular implementation to satisfy the
properties. For instance the standard list implementation satisfies
them:
\begin{minted}{haskell}
instance Monoid [a] where
    mappend = (++)
    mempty = []
\end{minted}
\end{example}


\begin{remark}[Monoid]
The given definition of monoid is based on its internal structure i.
e. there is a \mynameref{def:non_categorical_approach}. In
\cref{ch:monoid_categorically}  we shall continue the 
\mynameref{def:monoid} concept investigation and will give a
\mynameref{def:categorical_approach} of the concept. You can also find
there 
some notes about the concept importance in different areas
such as programming languages and math (see
\cref{ch:monoid_importance_monad}).
\end{remark}

We can consider 2 \mynameref{def:monoid}s. The first one has
\mynameref{def:product} as the binary operation and
\mynameref{def:terminal_object} as the identity element. As result we
just got an analog of multiplication in the category theory. This is why
the terminal object is often denoted as $\mathbf{1}$ and the operation
is called as the product. 

Another one is additional \mynameref{def:monoid} that has
\mynameref{def:initial_object} as the identity element and the
\mynameref{def:sum} as the binary operation. The initial object in
that case  is often denoted as $\mathbf{0}$. I.e. we can see a direct
connection with addition in algebra.

If we do such consideration then we can make a step forward and look
at the distributive law that sum and multiplication satisfy.
\begin{definition}[Distributive category]
\label{def:distributive_category}
A category $\cat{C}$ is \textit{distributive} if 
\cite{wiki:distributive_category}
it has finite
\mynameref{def:product}s and \mynameref{def:sum}s such that 
$\forall a,b,c \in \catob{C}$:
\[
(a \times b) \oplus (a \times c) \cong a \times ( b \oplus c )
\]
and 
\[
a \times 0 \cong 0
\]
where $\mathbf{0}$ is the \mynameref{def:initial_object}.
\end{definition} 

\begin{example}[Distributive category]
\label{ex:distributive_category}
\mynameref{def:setcategory} is an example 
\cite{wiki:distributive_category}
of \mynameref{def:distributive_category}

From other hand not all categories which have both product and sum are
distributive. One of such example is a category of all groups
$\cat{Grp}$ \cite{wiki:distributive_category}  where groups are
considered as objects and group homomorphisms as morphisms.  
\end{example}

\section{Exponential}
We are going to talk about functions (aka morphisms) as
\mynameref{def:object}s. 

\subsection{Definition and examples}
\begin{example}[Homset]
\label{ex:homset}
Consider 2 sets $A$ and $B$ then the set of functions between the 2 sets
forms a new set that is called as \mynameref{def:homset} and denoted
as $\catmset{A}{B}$. Thus if $A,B \in \catob{Set}$ then 
$\catmset{A}{B} \in \catob{Set}$. 
\end{example}

The construction of \mynameref{def:homset} is applied to
the \mynameref{def:setcategory} but not to an arbitrary category because
the \mynameref{def:homset} is a \mynameref{def:set} and therefore the
object in the \mynameref{def:setcategory}. I.e. if $\cat{C}$ is a
category and $a, b \in \catob{C}$ 
then the \mynameref{def:homset} $\catmset{a}{b} \in \catob{Set}$ but
we now want to construct something like to the \mynameref{def:homset}
but that is an object in $\cat{C}$. This will be called as the
function object. we shall use the universal construction
(\mynameref{def:universalproperty}) for the object definition. 

\begin{definition}[Exponential]
\label{def:exponential}
\begin{figure}
  \centering
  \begin{tikzpicture}[ele/.style={fill=black,circle,minimum
        width=.8pt,inner sep=1pt},every fit/.style={ellipse,draw,inner
        sep=-2pt}]

    % the texts
    
    \node[ele,label=above:$y'$] (z1) at (0,3) {};    
    \node[ele,label=below:$y^x$] (zy) at (0,0) {};    
    \node[ele,label=above:$y' \times x$] (z1y) at (3,3) {};
    \node[ele,label=below:$y^x \times x$] (zyy) at (3,0) {};
    \node[ele,label=below:$y$] (z) at (6,0) {};

    \draw[->,thick,shorten <=2pt,shorten >=2pt] (z1) to
    node[left]{$h$} (zy);
    \draw[->,thick,shorten <=2pt,shorten >=2] (z1y) to
    node[left]{$h \times \idm{x}$} (zyy); 
    \draw[->,thick,shorten <=2pt,shorten >=2] (z1y) to
    node[sloped,above]{$e'$} (z); 
    \draw[->,thick,shorten <=2pt,shorten >=2] (zyy) to
    node[sloped,above]{$e$} (z); 
  \end{tikzpicture}
  \caption{Exponential object}
  \label{fig:exponential}
\end{figure}
Let $\cat{C}$ is a category and $x, y \in \catob{C}$. We also assume
that $\cat{C}$ allows all \mynameref{def:product}s with $x$, i.e.
$\forall y' \in \catob{C}, \exists y' \times x$. An object $y^x$
together with a \mynameref{def:morphism} $e: y^x \times x \to y$ is 
an \textit{exponential object} if $\forall e' \in \cathom{C}$ and
$\forall y' \in \catob{C}$ exists an
unique morphism $h: y' \to y$ such that the
\mynameref{def:commutative_diagram} shown in \cref{fig:exponential}
commutes:
\[
e' = e \circ \left(h \times \idm{x} \right)
\]
\end{definition}

\begin{example}[Exponential][$\cat{Set}$]
\label{ex:exponential_set}
Lets look at the \mynameref{def:exponential} in $\cat{Set}$. We want
to show that the object corresponds to the function. Really if we want
to define a function $f: X \to Y$ then we should look at the
\mynameref{def:homset} $F = \catmset{X}{Y}$. $f \in F$ - is an element of the
\mynameref{def:homset}. For the function application we have to take
the argument $x 
\in X$ and the function we want to apply $f \in F$. Then we construct
the pair $(f,x) \in F \times X$. For the function application we have
to call a \mynameref{def:morphism} $e: F \times X \to Y$.
\footnote{$e$ from the word ``eval''}
I.e. the
application $e(f, x)$ gives us $e(f, x) = y \in Y$ - the function
value. 
\end{example}

The notation is used for ``morphisms (functions) as objects'' in the
category theory has an explanation provided in the following remark.
\begin{remark}[Exponential notation]
The \mynameref{def:homset} $\catmset{X}{Y}$ is often denoted as $Y^X$.
Why the strange notation is used? 
Lets $X$ is a \mynameref{def:singleton_set} i.e. its
\mynameref{def:cardinality} is $1$: $\left|X\right| = 1$. 
The set $Y$ has only 2
elements, i.e. its \mynameref{def:cardinality} is $2$: 
$\left|Y\right|= 2$. 

Consider a function $f: X \to Y$. How many such functions do we have?
There are really 2 functions (see \cref{fig:exponential_set_remark_x_y}).
One of them $f_1$ return the first element 
from $Y$ ($y_1$) and the other $f_2$ returns the second one ($y_2$).
The number of functions can be written as 
$2^1$. I.e. one can write for \mynameref{def:cardinality} of a set of
all functions between $X$ and $Y$ as follows
\begin{equation}
\label{eq:exponential_size}
\left|Y^X\right| = \left|Y\right|^{\left|X\right|}.
\end{equation}
\begin{figure}[H]
  \centering
  \begin{tikzpicture}[ele/.style={fill=black,circle,minimum
        width=.8pt,inner sep=1pt},every fit/.style={ellipse,draw,inner
        sep=-2pt}]

    % the texts
    \node at (0,5) {$X$};
    \node at (4,5) {$Y$};
    
    \node[ele,label=left:$x$] (x) at (0,4) {};    

    \node[ele,,label=right:$y_1$] (y1) at (4,4) {};
    \node[ele,,label=right:$y_2$] (y2) at (4,3) {};

    \node[draw,fit= (x),minimum width=1.5cm, minimum height= 1.5cm] {} ;
    \node[draw,fit= (y1) (y2),minimum width=2cm, minimum height= 2cm] {} ;  
    \draw[->,thick,shorten <=2pt,shorten >=2pt] (x) to
    node[sloped,above]{$f_1$} (y1);
    \draw[->,thick,shorten <=2pt,shorten >=2] (x) to
    node[sloped,below]{$f_2$} (y2);
  \end{tikzpicture}
  \caption{$\catmset{X}{Y}$ consists of 2 elements: $\{f_1, f_2\}$.
    Thus the cardinality of the homset is $2$}
  \label{fig:exponential_set_remark_x_y}
\end{figure}


Otherwise if we consider a function $g: Y \to X$ then we have only one
possible choice for it (see \cref{fig:exponential_set_remark_y_x}) : just return the only possible element from
$X$. I.e. $\left|X^Y\right| = 1$ that correlates with
\eqref{eq:exponential_size}. 
\begin{figure}[H]
  \centering
  \begin{tikzpicture}[ele/.style={fill=black,circle,minimum
        width=.8pt,inner sep=1pt},every fit/.style={ellipse,draw,inner
        sep=-2pt}]

    % the texts
    \node at (0,5) {$X$};
    \node at (4,5) {$Y$};
    
    \node[ele,label=left:$x$] (x) at (0,4) {};    

    \node[ele,label=right:$y_{1,2}$] (y) at (4,4) {};

    \node[draw,fit= (x),minimum width=1.5cm, minimum height= 1.5cm] {} ;
    \node[draw,fit= (y),minimum width=1.5cm, minimum height= 1.5cm] {} ;  
    \draw[->,thick,shorten <=2pt,shorten >=2pt] (y) to
    node[sloped,above]{$g$} (x);
  \end{tikzpicture}
  \caption{$\catmset{Y}{X}$ consists of 1 element: $\{g\}$.
    Thus the cardinality of the homset is $1$}
  \label{fig:exponential_set_remark_y_x}
\end{figure}
\end{remark}

\subsection{Currying in $\cat{Set}$}
In the section we shall be in the \mynameref{def:setcategory}. 
The definition of \mynameref{def:exponential} object is closely
related to notion of currying that is defined for \mynameref{def:set}s
as follows. 
\begin{definition}[Currying]
\label{def:currying_set}
Consider a function of 2 arguments:
\[
f:(X\times Y) \to Z
\]
that maps a pair (\mynameref{def:product}) of 2 sets $X$ and $Y$ into
another set $Z$.
The \textit{currying} constructs a new function
\[
h : X \to (Y \to Z)
\]
such that the following equation holds
\[
h(x)(y) = f(x,y), 
\]
where $x \in X, y \in Y$. The \textit{currying} will be denoted as 
$h = curry(f)$.
\end{definition}

\begin{remark}[Currying]
If we consider $Y^X$ is a set of functions $f : X \to Y$ then the
currying is the \mynameref{def:bijection}
\[
Y^{X_1 \times X_2} \cong \left(Y^{X_1}\right)^{X_2}.
\] 
\end{remark}
\begin{remark}[Currying and Exponential]
If we look in \cref{fig:exponential} then we can notice that 
\[
curry(e): y^x \to (x \to y),
\]
i.e. currying is used to construct a morphisms from exponential
object. 
\end{remark}

\subsection{Cartesian closed category}
\begin{definition}[Cartesian closed category]
\label{def:cartesian_closed_category}
If a category $\cat{C}$ satisfies the following conditions then it is
called \textit{Cartesian closed category}
\begin{enumerate}
\item It has \mynameref{def:terminal_object}
\item $\forall a,b \in \catob{C}$ exists \mynameref{def:product} $a
  \times b \in \catob{C}$.
\item $\forall a,b \in \catob{C}$ exists \mynameref{def:exponential}
  $a^b \in \catob{C}$
\end{enumerate}
\end{definition}

\begin{theorem}[Cartesian closed category]
\label{thm:ccc}
If $\cat{C}$ is a \mynameref{def:cartesian_closed_category} with
finite \mynameref{def:sum} then it is a
\mynameref{def:distributive_category}.
\begin{proof}
TBD
\end{proof}
\end{theorem}

\section{Programming language examples. Type algebra}

\subsection{$\cat{Hask}$ category}
\begin{example}[Initial object][$\cat{Hask}$]
If we avoid lazy evaluations in Haskell (see
\mynameref{rem:hask_lazy_eval}) then we can found several types
as candidates for initial and terminal object in Haskell. 
\label{ex:hask_initial_object}
\mynameref{def:initial_object} in \mynameref{def:haskcategory} is a
type without values 
\begin{minted}{haskell}
data Void
\end{minted}
i.e. you cannot construct a object of the type.

There is only one function from the initial object:
\begin{minted}{haskell}
absurd :: Void -> a
\end{minted}
The function is called absurd because it does absurd action. Nobody
can proof that it does not exist. For the existence proof the
following absurd argument can be used: ``Just provide me an object type
\textbf{Void} and I will provide you the result of
evaluation''.  

There is no function in opposite direction because it would had been
used for the \textbf{Void} object creation. 
\end{example}

\begin{example}[Terminal object][$\cat{Hask}$]
\label{ex:hask_terminal_object}
Terminal object (unit) in \mynameref{def:haskcategory} keeps only one element
\begin{minted}{haskell}
data () = ()
\end{minted}
i.e. you can create only one element of the type. You can use the
following function for the creation:
\begin{minted}{haskell}
unit :: a -> ()
unit _ = ()
\end{minted}
\end{example}

\begin{example}[Product][$\cat{Hask}$]
\label{ex:hask_product}
The \mynameref{def:product} in \mynameref{def:haskcategory} keeps a
pair and the constructor defined as follows
\begin{minted}{haskell}
(,) :: a -> b -> (a, b)
(,) x y = (x, y)
\end{minted}
There are 2 projectors: 
\begin{minted}{haskell}
fst :: (a, b) -> a
fst (x, _) = x
snd :: (a, b) -> b
snd (_, y) = y
\end{minted}
\end{example}

\begin{example}[Sum][$\cat{Hask}$]
\label{ex:hask_sum}
The \mynameref{def:sum} in \mynameref{def:haskcategory} defined as
follows 
\begin{minted}{haskell}
data Either a b = Left a | Right b
\end{minted}

The typical usage is via pattern matching for instance 
\begin{minted}{haskell}
factor :: (a -> c) -> (b -> c) -> Either a b -> c
factor f _ (Left x) = f x
factor _ g (Right y) = g y
\end{minted}
\end{example}

\begin{example}[Distributive category][$\cat{Hask}$]
As soon as $\cat{Hask}$ is a \mynameref{def:cartesian_closed_category}
then by \cref{thm:ccc} it is a \mynameref{def:distributive_category}
i.e. one can conclude that
\begin{minted}{haskell}
(a,Either b c)
\end{minted}
is the same to
\begin{minted}{haskell}
Either (a, b) (a, c)
\end{minted}
\end{example}

\begin{example}[Exponential][$\cat{Hask}$]
\label{ex:exponential_hask}
It's not surprisingly that the \mynameref{def:exponential} in
$\cat{Hask}$ is a function object i.e. $b^a$ can be written as  
\textbf{a -> b}.
\end{example}

\begin{example}[Type algebra]
\cref{ex:exponential_hask} gives interesting results with types
manipulations. For instance the type $a^{b+c}$ can be written as
\begin{minted}{haskell}
Either b c -> a
\end{minted}
for the function we should have both functions 
\textbf{b -> a} and \textbf{b -> c}. I.e.
the code is equivalent to the following one
\begin{minted}{haskell}
(b -> a, c -> a)
\end{minted}
These transformations correspond to the following simple algebraic
equation 
\[
a^{b+c} = a^b a^c.
\]
This is also called as \textit{type algebra}.
\end{example}

\subsection{$\cat{C\texttt{++}}$ category}
\begin{example}[Initial object][$\cat{C\texttt{++}}$]
\label{ex:cpp_initial_object}
In C\texttt{++} exists a special type that does not hold any values and as
result cannot be created: \textbf{void}.
You cannot create an object of that type i.e. you will get a compiler
error if you try.
\end{example}

\begin{example}[Terminal object][$\cat{C\texttt{++}}$]
\label{ex:cpp_terminal_object}
C\texttt{++} 17 introduced a special type that keeps only one value -
\textbf{std::monostate}:  
\begin{minted}{c++}
namespace std {
  struct monostate {};
}
\end{minted}
\end{example}

\begin{example}[Product][$\cat{C\texttt{++}}$]
\label{ex:cpp_product}
The \mynameref{def:product} in \mynameref{def:cppcategory} keeps a
pair and the constructor defined as follows
\begin{minted}{c++}
namespace std {
  template< class A, class B > struct pair {
    A first;
    B second;
  };
}
\end{minted}

There is a simple usage example
\begin{minted}{c++}
  std::pair<int, bool> p(0, false);

  std::cout << "First projector: " << p.first << std::endl;
  std::cout << "Second projector: " << p.second << std::endl;

\end{minted}
Really any \textbf{struct} or \textbf{class} can be
considered as a product. 
\end{example}

\begin{example}[Sum][$\cat{C\texttt{++}}$]
  \label{ex:cpp_sum}
  If we consider \mynameref{def:object}s as types then
  \mynameref{def:sum} is an object that can be either one or another
  type. The corresponding C/C\texttt{++} construction that provides an ability
  to keep one of two types is \textbf{union}. 

  %% There is an \textbf{Either} implementation from
  %% \mynameref{ex:hask_sum} 
  %% \begin{minted}{c++}
  %%   template <typename A, typename B> class Either
  %%   {
  %%   public:
  %%     Either(const Either& e) : is_left_(e.is_left_){
  %%       if (is_left_){
  %%         data.l = e.data.l;      
  %%       } else {
  %%         data.r = e.data.r;      
  %%       }    
  %%     }
  %%     ~Either(){
  %%       if (is_left_){
  %%         data.l.~A();      
  %%       } else {
  %%         data.r.~B();      
  %%       }        
  %%     }      
  %%     Either(const A& l) : data(l), is_left_(true){
  %%     }
  %%     Either(const B& r) : data(r), is_left_(false){
  %%     }
  %%     const A& left() const {
  %%       if (!is_left_){
  %%         throw std::logic_error("no left");      
  %%       }    
  %%       return data.l;    
  %%     }
  %%     const B& right() const {
  %%       if (is_left_){
  %%         throw std::logic_error("no right");      
  %%       }    
  %%       return data.r;    
  %%     }
  %%   private:
  %%     union Data {
  %%       Data() {}
  %%       Data( const A& a) : l(a) {}
  %%       Data (const B& b) : r(b) {}
  %%       ~Data() {}
  %%       A l;
  %%       B r;
  %%     } data;       
  %%     bool is_left_;  
  %%   };
  %% \end{minted}
  %% The usage example:
  %% \begin{minted}{c++}
  %%   template <typename A, typename B, typename C, typename D>
  %%   auto factor(A f, B g, const Either<C, D>& either) {
  %%     try {
  %%       return f(either.left());               
  %%     }
  %%     catch(...) {
  %%       return g(either.right());                              
  %%     }
  %%   };
    
  %%   auto stringLength = [](std::string s) {
  %%     return static_cast<int>(s.size()); };
  %%   auto id = [](auto x) { return x; };
          
  %%   Either<std::string, int> str = std::string("abc");
  %%   std::cout << "String length:" <<
  %%   factor<>(stringLength, id, str) << std::endl;
  %%   Either<std::string, int> i = 4;
  %%   std::cout << "id(int):" <<
  %%   factor<>(stringLength, id, i) << std::endl;
  %% \end{minted}

  C\texttt{++}17 suggests \textbf{std:variant} as a safe replacement
  for \textbf{union}. The example of the \textbf{factor}
  function is below
  \begin{minted}{c++}
    template <typename A, typename B, typename C, typename D>
    auto factor(A f, B g, const std::variant<C, D>& either) {
      try {
        return f(std::get<C>(either));               
      }
      catch(...) {
        return g(std::get<D>(either));                              
      }
    };
  \end{minted}
  The simple usage as follows:
  \begin{minted}{c++}
    std::variant<std::string, int> var = std::string("abc");
    std::cout << "String length:" <<
    factor<>(stringLength, id, var) << std::endl;
    var = 4;
    std::cout << "id(int):" <<
    factor<>(stringLength, id, var) << std::endl;    
  \end{minted}

\end{example}
TBD
\subsection{$\cat{Scala}$ category}
\begin{example}[Initial object][$\cat{Scala}$]
\label{ex:scala_initial_object}
We used a same trick as for \mynameref{ex:hask_initial_object} in
\mynameref{def:haskcategory} and define
\mynameref{def:initial_object} in \mynameref{def:scalacategory} as a
type without values 
\begin{minted}{scala}
sealed trait Void
\end{minted}
i.e. you cannot construct a object of the type.
\end{example}

\begin{example}[Terminal object][$\cat{Scala}$]
\label{ex:scala_terminal_object}
We used a same trick as for \mynameref{ex:hask_terminal_object}
in \mynameref{def:haskcategory} and define
\mynameref{def:terminal_object} in \mynameref{def:scalacategory} as a
type with only one value
\begin{minted}{scala}
abstract final class Unit extends AnyVal
\end{minted}
TBD
i.e. you can create only one element of the type.
\end{example}

TBD

\section{Quantum mechanics}
\begin{example}[Initial object][$\cat{FdHilb}$]
\label{ex:quant_initial_object}
we shall use a Hilber space of dimensional 0 as the
\mynameref{def:initial_object}. I.e. the set that does not have any
states in it.
\end{example}

\begin{example}[Terminal object][$\cat{FdHilb}$]
  \label{ex:quant_terminal_object}
we shall use a Hilber space of dimensional 1 as the
\mynameref{def:terminal_object}. I.e. the set of complex numbers
$\mathbb{C}$.   
\end{example}

\begin{example}[Product][$\cat{FdHilb}$]
  \label{ex:quant_product}
  The \mynameref{def:product} in \mynameref{def:fdhilbcategory} is a
  \mynameref{def:fdhilb_direct_sum}.
\end{example}

\begin{example}[Sum][$\cat{FdHilb}$]
  \label{ex:quant_sum}
  The \mynameref{def:sum} in \mynameref{def:fdhilbcategory} is a
  \mynameref{def:fdhilb_direct_sum}.
\end{example}

TBD