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

\homework{Adjunctions}

\begin{document}
\maketitle

\begin{exercise}
Prove that the inclusion functor $\cat{Set} \xmono{I} \cat{Rel}$ has a right adjoint.
You may use any of the equivalent definitions of adjunction.
For clarification, $I$ is the functor mapping each set $X$ (an object of $\cat{Set}$) to the set $X$ (also an object of $\cat{Rel}$) and each function $X \to Y$ (a morphism of $\cat{Set}$) to the relation $\lambda \langle x, y \rangle.\; f(x) = y$ (a morphism of $\cat{Rel}$).
\end{exercise}

\begin{proof}
There is a functor $\Set : \cat{Rel} \mto \cat{Set}$ mapping each set $X$ to the set $\Set X$ and each relation $R : X \times Y \to Prop$ to the function $\lambda \vec{x}.\; \{y : Y \mid \exists x \in \vec{x}.\; x \mathrel{R} y\}$.
The identity relation $\lambda \langle x_1, x_2 \rangle. x_1 = x_2$ gets mapped to the function $\lambda \vec{x}.\; \{x_2 : X \mid \exists x_1 \in \vec{x}.\; x_1 = x_2\}$ which is simply the identity function.
The composition relation $\lambda \langle x, z \rangle.\; \exists y : Y.\; x \mathrel{R_1} y \wedge y \mathrel{R_2} z$ gets mapped to the function $\lambda \vec{x}.\; \{z : Z \mid \exists x \in \vec{x}.\; \exists y : Y.\; x \mathrel{R_1} y \wedge y \mathrel{R_2} z\}$ which equals $\lambda \vec{x}.\; \{z : Z \mid \exists y \in \{y : Y \mid \exists x \in \vec{x}.\; x \mathrel{R_1} y\}.\; y \mathrel{R_2} z\}$, proving distributivity.

Given a $\cat{Rel}$-object $Y$, define the $\cat{Rel}$-morphism $\varepsilon_Y : I(\Set(Y)) \mto Y$ to be the binary relation $\lambda \langle \vec{y}, y \rangle.\; y \in \vec{y}$.
Given another $\cat{Rel}$-morphism from some $I(X)$ to $Y$, i.e.~a binary relation $R : X \times Y \to \Prop$, the unique corresponding $\cat{Set}$-morphism from $X$ to $\Set(Y)$ is the function $\lambda x.\; \{y : Y \mid x \mathrel{R} y\}$.
The $\cat{Rel}$-composition $I(\lambda x.\; \{y : Y \mid x \mathrel{R} y\}) \cocomp (\lambda \langle \vec{y}, y \rangle.\; y \in \vec{y})$ is by definition the binary relation $\lambda \langle x, y \rangle.\; \exists \vec{y} : \Set(Y).\; \{y : Y \mid x \mathrel{R} y\} = \vec{y} \wedge y \in \vec{y}$, which is equivalent to simply $R$.
Furthermore, for any function $f : X \to \Set Y$, the composition $\lambda \langle x, y \rangle.\; \exists \vec{y} : \Set Y.\; f(x) = \vec{y} \wedge y \in \vec{y}$ is equivalent to $\lambda \langle x, y \rangle.\; y \in f(x)$, which is equivalent to $R$ if and only if $f(x) = \{y : Y \mid \exists x : X.\; x \mathrel{R} y\}$, making the function corresponding to $R$ unique.
\end{proof}
\vspace{-.25in}

\begin{wrapfigure}{r}{6cm}
\begin{tikzpicture}
\node(n1) at (0,0) {$\N$};
\node(r1)[circle,draw] at (1,2) {$\mathtt{repeat}$};
\node(r2)[circle,draw] at (-1,4) {$\mathtt{repeat}$};
\node(f)[circle,draw] at (1,6) {$\mathtt{flatten}$};
\node(s)[circle,draw] at (-1,8) {$\mathtt{sum}$};
\node(n2) at (0,10) {$\N$};
\draw[->] (n1.north) .. controls +(0,1) and ($(r1.south) + (0,-1)$) .. (r1.south);
\draw[->] (r1) -- node[below left]{$\N$} (r2);
\draw[->] (r1.north east) .. controls +(1,1) and ($(f.south east) + (1,-1)$) .. node[right]{$\List$} (f.south east);
\draw[->] (r2.north west) .. controls +(-1,1) and ($(s.south west) + (-1,-1)$) .. node[left]{$\N$} (s.south west);
\draw[->] (r2) -- node[below right]{$\List$} (f);
\draw[->] (f) -- node[below left]{$\List$} (s);
\draw[->] (s.north) .. controls +(0,1) and ($(n2.south) + (0,-1)$) .. (n2.south);
\end{tikzpicture}
\end{wrapfigure}
~
\begin{exercise}
There is a functor from $\cat{1}$ to $\cat{Set}$ picking out the empty set, and another functor from $\cat{1}$ to $\cat{Set}$ picking out the singleton set.
One is the left adjoint to the unique functor from $\cat{Set}$ to $\cat{1}$, and the other is the right adjoint to the unique functor from $\cat{Set}$ to $\cat{1}$.
Determine and prove which is which.
\end{exercise}

\begin{proof}
The functor~$F : \cat{1} \mto \cat{Set}$ picking out the empty set is the left adjoint to the unique functor $\langle \rangle$ from $\cat{Set}$ to $\cat{1}$ (whose only object we call $\star$).
For any $X : \cat{Set}$ and $\star : \cat{1}$, both $M_\cat{Set}(F(\star), X)$ and $M_\cat{1}(\star, \langle\rangle(X))$ have only one element, making them isomorphic.
Furthermore, since $\cat{1}$ has only one morphism, this isomorphism is guaranteed to be natural, making this an adjunction.

The functor~$G : \cat{1} \mto \cat{Set}$ picking out the singleton set is the right adjoint to the unique functor $\langle \rangle$ from $\cat{Set}$ to $\cat{1}$ (whose only object we call $\star$).
For any $X : \cat{Set}$ and $\star : \cat{1}$, both $M_\cat{1}(\langle\rangle(X), \star)$ and $M_\cat{Set}(X, G(\star))$ have only one element, making them isomorphic.
Furthermore, since $\cat{1}$ has only one morphism, this isomorphism is guaranteed to be natural, making this an adjunction.
\end{proof}

\begin{exercise}
$\N : \cat{1} \mto \cat{Set}$ maps the only object of $\cat{1}$ to the set $\N$.
$\mathtt{repeat}$ is the natural transformation from $\N$ to $\N \cocomp \List$ (i.e.~$\List(\N)$) mapping the sole object of $\cat{1}$ to the function mapping $n$ to the length-$n$ list $[n, \dots, n]$.
$\mathtt{sum}$ is the natural transformation from $\N \cocomp \List$ to $\N$ mapping the sole object of $\cat{1}$ to the function mapping a list of numbers and returns its sum.

The string diagram to the right denotes a natural transformation from the functor $\N : \cat{1} \mto \cat{Set}$ to itself ($\N$ maps the only object of $\cat{1}$ to the set $\N$).
In particular, this means it describes a function from $\N$ to $\N$.
Determine what that function is in terms of basic arithmetic.
(No proof necessary; the purpose of this is to learn the notation.)
\end{exercise}

\begin{proof}
The function is $\lambda n.\; n^3$.
The program described by the diagram is $\lambda n.\; \mathtt{sum}(\mathtt{flatten}(\mathtt{map}_\mathtt{repeat}(\mathtt{repeat}(n))))$.
\end{proof}

\end{document}