\documentclass{article}
\input{packages}
\input{def}

\homework{Limits}

\begin{document}
\maketitle

\begin{exercise}
Prove that for any object $\ob{A}$ of any category~$\cat{C}$, the object $\ob{A} \with \top$ (if it exists) is isomoprhic to $\ob{A}$.
\end{exercise}

\begin{proof}
Let $\mo{f} : \ob{A} \mto \ob{A} \with \top$ be defined as $\langle \id_\ob{A}, \langle \rangle \rangle$.
Let $\mo{g} : \ob{A} \with \top \mto \ob{A}$ be defined as $\pi_\ob{A}$.
$\mo{f} \cocomp \mo{g} = \langle \id_\ob{A}, \langle \rangle \rangle \cocomp \pi_\ob{A} = \id_\ob{A}$ by the nature of projections, proving one direction.
$\mo{g} \cocomp \mo{f} \cocomp \pi_\top : \ob{A} \with \top \mto \top$ equals $\id_{\ob{A} \with \top} \cocomp \pi_\top : \ob{A} \with \top \mto \top$ since all morphisms from the same domain to $\top$ are equal by the nature of terminal objects.
Also, $\mo{g} \cocomp \mo{f} \cocomp \pi_\ob{A} = \pi_\ob{A} \cocomp \langle \id_\ob{A}, \langle \rangle \rangle \cocomp \pi_\ob{A} = \pi_\ob{A} \cocomp \id_\ob{A} = \pi_\ob{A} = \id_{\ob{A} \with \top} \cocomp \pi_\ob{A}$.
Thus, since all morphisms to a product that behave the same after being followed by both projections must be equal, we have $\mo{g} \cocomp \mo{f} = \id_{\ob{A} \with \top}$.
So, $\mo{f}$ and $\mo{g}$ are inverses of each other, making $\ob{A}$ isomorphic to $\ob{A} \with \top$.
\end{proof}

\begin{exercise}
Prove that, in any 2-category, if morphisms $\ob{C}_1 \xmto{\mo{f}_1} \ob{C}_2$ and $\ob{C}_2 \xmto{\mo{f}_2} \ob{C}_3$ are both left adjoints, then their composition $\mo{f}_1 \cocomp \mo{f}_2$ is also a left adjoint.
\end{exercise}

\begin{proof}
Let $\langle \ob{C}_1, \ob{C}_2, \mo{f}_1, \mo{g}_1, \eta_1, \varepsilon_1, \prf{f}_1, \prf{g}_1 \rangle$ and $\langle \ob{C}_2, \ob{C}_3, \mo{f}_2, \mo{g}_2, \eta_2, \varepsilon_2, \prf{f}_2, \prf{g}_2 \rangle$ be some adjunctions that $\mo{f}_1$ and $\mo{f}_2$ are the left adjoints of.
Then $\langle \ob{C}_1, \ob{C}_3, \mo{f}_1 \cocomp \mo{f}_2, \mo{g}_2 \cocomp \mo{g}_1, \eta, \varepsilon, \prf{f}, \prf{g} \rangle$ is an adjuction that $\mo{f}_1 \cocomp \mo{f}_2$ is the left adjoint of, where $\eta$, $\varepsilon$, $\prf{f}$, and $\prf{g}$ are defined as follows:
\begin{description}
\item[$\eta : \ob{C}_1 \nto \mo{f}_1 \cocomp \mo{f}_2 \cocomp \mo{g}_2 \cocomp \mo{g}_1 =$]
\begin{tikzpicture}[baseline=(e2.base)]
\node(f1) at (-1.5,0) {$\mo{f}_1$};
\node(f2) at (-.5,0) {$\mo{f}_2$};
\node(g2) at (.5,0) {$\mo{g}_2$};
\node(g1) at (1.5,0) {$\mo{g}_1$};
\node(e2)[circle,draw] at (0,-1) {$\eta_2$};
\node(e1)[circle,draw] at (0,-2) {$\eta_1$};
\draw[->] (e1.north west) .. controls +(-.5,.5) and ($(f1.south) + (0,-.5)$) .. (f1.south);
\draw[->] (e2.north west) .. controls +(-.25,.25) and ($(f2.south) + (0,-.25)$) .. (f2.south);
\draw[->] (e2.north east) .. controls +(.25,.25) and ($(g2.south) + (0,-.25)$) .. (g2.south);
\draw[->] (e1.north east) .. controls +(.5,.5) and ($(g1.south) + (0,-.5)$) .. (g1.south);
\end{tikzpicture}
\item[$\varepsilon : \mo{g}_2 \cocomp \mo{g}_1 \cocomp \mo{f}_1 \cocomp \mo{f}_2 \nto \ob{C}_3 =$]
\begin{tikzpicture}[baseline=(e2.base)]
\node(f1) at (-1.5,0) {$\mo{g}_2$};
\node(f2) at (-.5,0) {$\mo{g}_1$};
\node(g2) at (.5,0) {$\mo{f}_1$};
\node(g1) at (1.5,0) {$\mo{f}_2$};
\node(e2)[circle,draw] at (0,1) {$\varepsilon_1$};
\node(e1)[circle,draw] at (0,2) {$\varepsilon_2$};
\draw[<-] (e1.south west) .. controls +(-.5,-.5) and ($(f1.north) + (0,.5)$) .. (f1.north);
\draw[<-] (e2.south west) .. controls +(-.25,-.25) and ($(f2.north) + (0,.25)$) .. (f2.north);
\draw[<-] (e2.south east) .. controls +(.25,-.25) and ($(g2.north) + (0,.25)$) .. (g2.north);
\draw[<-] (e1.south east) .. controls +(.5,-.5) and ($(g1.north) + (0,.5)$) .. (g1.north);
\end{tikzpicture}
\item[$\prf{f}$] is given by
\begin{tikzpicture}[baseline=(eta2.base)]
\node(f12) at (0,0) {$\mo{f}_1$};
\node(f22) at (1,0) {$\mo{f}_2$};
\node(eta2)[circle,draw] at (2,-2) {$\eta_2$};
\node(eta1)[circle,draw] at (2,-3) {$\eta_1$};
\node(eps2)[circle,draw] at (3,-1) {$\varepsilon_2$};
\node(eps1)[circle,draw] at (3,-2) {$\varepsilon_1$};
\node(f11) at (4,-4) {$\mo{f}_1$};
\node(f21) at (5,-4) {$\mo{f}_2$};
\draw[->] (eta1.north west) .. controls +(-.5,.5) and ($(f12.south) + (0,-1.5)$) .. (f12.south);
\draw[->] (eta2.north west) .. controls +(-.25,.25) and ($(f22.south) + (0,-1)$) .. (f22.south);
\draw[->] (eta2) -- node[above left]{$\mo{g}_2$} (eps2);
\draw[->] (eta1) -- node[below right]{$\mo{g}_1$} (eps1);
\draw[<-] (eps1.south east) .. controls +(.5,-.5) and ($(f11.north) + (0,1)$) .. (f11.north);
\draw[<-] (eps2.south east) .. controls +(.25,-.25) and ($(f21.north) + (0,1.5)$) .. (f21.north);
\end{tikzpicture}
equals
\begin{tikzpicture}[baseline=(eta2.base)]
\node(f12) at (0,0) {$\mo{f}_1$};
\node(f22) at (1,0) {$\mo{f}_2$};
\node(f11) at (4,-4) {$\mo{f}_1$};
\node(f21) at (5,-4) {$\mo{f}_2$};
\draw[->] (f11.north) .. controls +(0,1.5) and ($(f12.south) + (0,-1.5)$) .. (f12.south);
\draw[->] (f21.north) .. controls +(0,1.5) and ($(f22.south) + (0,-1.5)$) .. (f22.south);
\end{tikzpicture}
due to $\prf{f}_1$ and $\prf{f}_2$.
\item[$\prf{g}$] is given by
\begin{tikzpicture}[baseline=(eta2.base)]
\node(f12) at (0,0) {$\mo{g}_1$};
\node(f22) at (-1,0) {$\mo{g}_2$};
\node(eta2)[circle,draw] at (-2,-2) {$\eta_2$};
\node(eta1)[circle,draw] at (-2,-3) {$\eta_1$};
\node(eps2)[circle,draw] at (-3,-1) {$\varepsilon_2$};
\node(eps1)[circle,draw] at (-3,-2) {$\varepsilon_1$};
\node(f11) at (-4,-4) {$\mo{g}_1$};
\node(f21) at (-5,-4) {$\mo{g}_2$};
\draw[->] (eta1.north east) .. controls +(.5,.5) and ($(f12.south) + (0,-1.5)$) .. (f12.south);
\draw[->] (eta2.north east) .. controls +(.25,.25) and ($(f22.south) + (0,-1)$) .. (f22.south);
\draw[->] (eta2) -- node[above right]{$\mo{f}_2$} (eps2);
\draw[->] (eta1) -- node[below left]{$\mo{f}_1$} (eps1);
\draw[<-] (eps1.south west) .. controls +(-.5,-.5) and ($(f11.north) + (0,1)$) .. (f11.north);
\draw[<-] (eps2.south west) .. controls +(-.25,-.25) and ($(f21.north) + (0,1.5)$) .. (f21.north);
\end{tikzpicture}
equals
\begin{tikzpicture}[baseline=(eta2.base)]
\node(f12) at (0,0) {$\mo{g}_1$};
\node(f22) at (-1,0) {$\mo{g}_2$};
\node(f11) at (-4,-4) {$\mo{g}_1$};
\node(f21) at (-5,-4) {$\mo{g}_2$};
\draw[->] (f11.north) .. controls +(0,1.5) and ($(f12.south) + (0,-1.5)$) .. (f12.south);
\draw[->] (f21.north) .. controls +(0,1.5) and ($(f22.south) + (0,-1.5)$) .. (f22.south);
\end{tikzpicture}
due to $\prf{g}_1$ and $\prf{g}_2$.
\end{description}
\end{proof}

\begin{exercise}
The monoid $\alg{A} \with \alg{B}$ is commutative if both $\alg{A}$ and $\alg{B}$ are commutative, and in that case is (with the appropriate projection homomorphisms) also the product of $\alg{A}$ and $\alg{B}$ in $\cat{CommMon}$.
Prove that there are morphisms $\kappa_\alg{A}$ and $\kappa_\alg{B}$ demonstrating that $\alg{A} \with \alg{B}$ is also the coproduct of $\alg{A}$ and $\alg{B}$ in $\cat{CommMon}$.
That is, prove that $\cat{CommMon}$ has \emph{biproducts}, meaning it has products and coproducts and they coincide on objects.
\end{exercise}

\begin{proof}
Define the underlying function of $\kappa_\alg{A} : \alg{A} \mto \alg{A} \with \alg{B}$ to be $\lambda a.\; \langle a, e_\alg{B} \rangle$.
This clearly preserves identity and multilplication, making $\kappa_\alg{A}$ a monoid homomorphism.
Similarly, $\kappa_\alg{B} = \langle \lambda b.\; \langle e_\alg{A}, b \rangle, \noprf, \noprf \rangle$.

Given a monoid~$\alg{C}$ and monoid homomorphisms $\mo{f}_\alg{A} : \alg{A} \mto \alg{C}$ and $\mo{f}_\alg{B} : \alg{B} \mto \alg{C}$, define the underlying function of $[\mo{f}] : \alg{A} \with \alg{B} \mto \alg{C}$ to be $\lambda \langle a, b \rangle.\; f_\alg{A}(a) +_\alg{C} f_\alg{B}(b)$.
We have to show this is a monoid morphism.
It distributes since $[\mo{f}](\langle a_1, b_1 \rangle +_{\alg{A} \with \alg{B}} \langle a_2, b_2 \rangle) = [\mo{f}](\langle a_1 +_\alg{A} a_2, b_1 +_\alg{B} b_2 \rangle) = f_\alg{A}(a_1 +_\alg{A} a_2) +_\alg{C} f_\alg{B}(b_1 +_\alg{B} b_2) = f_\alg{A}(a_1) +_\alg{C} f_\alg{A}(a_2) +_\alg{C} f_\alg{B}(b_1) +_\alg{C} f_\alg{B}(b_2) = f_\alg{A}(a_1) +_\alg{C} f_\alg{B}(b_1) +_\alg{C} f_\alg{A}(a_2) +_\alg{C} f_\alg{B}(b_2) = [\mo{f}](\langle a_1, b_1 \rangle) +_\alg{C} [\mo{f}](\langle a_2, b_2 \rangle)$.
It preserves identity since $[\mo{f}](e_{\alg{A} \with \alg{B}}) = [\mo{f}](\langle e_\alg{A}, e_\alg{B} \rangle) = f_\alg{A}(e_\alg{A}) +_\alg{C} f_\alg{B}(e_\alg{B}) = e_\alg{C} +_\alg{C} e_\alg{C} = e_\alg{C}$.

Given an $a : A$, $[\mo{f}](\kappa_\alg{A}(a)) = [\mo{f}](\langle a, e_\alg{B} \rangle) = f_\alg{A}(a) + f_\alg{B}(e_\alg{B}) = f_\alg{A}(a) + e_\alg{C} = f_\alg{A}(a)$, so $\kappa_\alg{A} \cocomp [\mo{f}]$ equals $\mo{f}_\alg{A}$.
Similarly, $\kappa_\alg{B} \cocomp [\mo{f}]$ equals $\mo{f}_\alg{B}$.

Lastly, suppose $\mo{g} : \alg{A} \with \alg{B} \mto \alg{C}$ also has the property that $\kappa_\alg{A} \cocomp \mo{g}$ equals $\mo{f}_\alg{A}$ and $\kappa_\alg{B} \cocomp \mo{g}$ equals $\mo{f}_\alg{B}$.
To be a monoid homomorphism, since for any $a : A$ and $b : B$ the sum $\langle a, e_\alg{B} \rangle +_{\alg{A} \with \alg{B}} \langle e_\alg{A}, b \rangle$ equals $\langle a, b \rangle$, we know that $g(\langle a, b \rangle) = g(\langle a, e_\alg{B} \rangle +_{\alg{A} \with \alg{B}} \langle e_\alg{A}, b \rangle) = g(\kappa_\alg{A}(a) +_{\alg{A} \with \alg{B}} \kappa_\alg{B}(b)) = g(\kappa_\alg{A}(a)) +_\alg{C} g(\kappa_\alg{B}(b)) = f_\alg{A}(a) +_\alg{C} f_\alg{B}(b) = [\mo{f}](\langle a, b \rangle)$.
Thus, any such $\mo{g}$ must equal $[\mo{f}]$, proving uniqueness.
\end{proof}

\end{document}