**Puzzle 162**

Piggyback on Dan's answer in [comment#20](https://forum.azimuthproject.org/discussion/comment/19801/#Comment_19801), I think one can make the answer shorter by combining the two cases there into one.

To avoid level slip, let's clarify the objects and morphisms on different levels before we start. To prove that the functors \$$\mathrm{Disc}\$$ and \$$\mathrm{Ob}\$$ are left and right adjoints to each other, our main focus is

* The \$$\mathrm{Hom}\$$-functors
\begin{align} \mathbf{Cat}(\mathrm{Disc}(-), =) &: \mathbf{Set}^{\mathrm{op}} \times \mathbf{Cat} \to \mathbf{Set} \\\\ \mathbf{Set}(-, \mathrm{Ob}(=)) &: \mathbf{Set}^{\mathrm{op}} \times \mathbf{Cat} \to \mathbf{Set}. \end{align}
and

* we want to show that there is a natural isomorphism \$$\alpha\$$ (i.e. an invertible natural transformation) from \$$\mathbf{Cat}(\mathrm{Disc}(-), =)\$$ to \$$\mathbf{Set}(-, \mathrm{Ob}(=))\$$
$\alpha:\mathbf{Cat}(\mathrm{Disc}(-), =) \Longrightarrow \mathbf{Set}(-, \mathrm{Ob}(=))$

This is our **top and most abstract level**.

To understand \$$\mathbf{Cat}(\mathrm{Disc}(-), =)\$$, \$$\mathbf{Set}(-, \mathrm{Ob}(=))\$$, and \$$\alpha\$$, we need to bring it down to a more concrete level by considering the images of these functors on some particular elements. Hence, let's pick a fixed element \$$(S, \mathcal{C})\$$ from the domain \$$\mathbf{Set}^{\mathrm{op}} \times \mathbf{Cat}\$$.

* The images under the two functors are, obviously, \$$\mathbf{Cat}(\mathrm{Disc}(S), \mathcal{C})\$$ and \$$\mathbf{Set}(S, \mathrm{Ob}(\mathcal{C}))\$$. Moreover, \$$\alpha\$$ will "generate" a morphism between these two objects

\begin{matrix}
\mathbf{Cat}(\mathrm{Disc}(S), \mathcal{C}) \\\\
\\\\
\alpha_{S,\mathcal{C}} \downarrow \\\\
\\\\
\mathbf{Set}(S, \mathrm{Ob}(\mathcal{C}))&
\end{matrix}
I think of it as "**one level down**".

In order to prove the naturality of \$$\alpha\$$, we need to consider the naturality square
$\begin{matrix} \mathbf{Cat}(\mathrm{Disc}(S), \mathcal{C}) & \rightarrow & \mathbf{Cat}(\mathrm{Disc}(T), \mathcal{D}) \\\\ \alpha_{S,\mathcal{C}} \downarrow & & \alpha_{T,\mathcal{D}} \downarrow \\\\ \mathbf{Set}(S, \mathrm{Ob}(\mathcal{C})) & \rightarrow & \mathbf{Set}(T, \mathrm{Ob}(\mathcal{D})) \end{matrix}$
where \$$(T, \mathcal{D})\$$ is just another fixed element in \$$\mathbf{Set}^{\mathrm{op}} \times \mathbf{Cat}\$$ and the "right edge" of the naturality square is just another manifestation of \$$\alpha\$$ at the element \$$(T, \mathcal{D})\$$. However, we still have to understand the "horizontal edges" of the naturality square. To this end, we first have to choose any fixed morphism

* \$$(\mathbf{f}, \mathbf{F}):(S, \mathcal{C})\to (T, \mathcal{D})\$$.

I consider this **"two levels down"** because this is a morphism belongs to the domain of \$$\mathbf{Cat}(\mathrm{Disc}(-), =)\$$ and \$$\mathbf{Set}(-, \mathrm{Ob}(=))\$$.

Then we have to bring \$$(\mathbf{f}, \mathbf{F})\$$ "one level up" by considering its images under \$$\mathbf{Cat}(\mathrm{Disc}(-), =)\$$ and \$$\mathbf{Set}(-, \mathrm{Ob}(=))\$$. Namely, \$$\mathbf{Cat}(\mathrm{Disc}(\mathbf{f}), \mathbf{F})\$$ and \$$\mathbf{Set}(\mathbf{f}, \mathrm{Ob}(\mathbf{F}))\$$. It is these two morphisms that contribute to the "horizontal edges" of the naturality square
$\begin{matrix} \mathbf{Cat}(\mathrm{Disc}(S), \mathcal{C}) & \overset{\mathbf{Cat}(\mathrm{Disc}(\mathbf{f}), \mathbf{F})}\longrightarrow & \mathbf{Cat}(\mathrm{Disc}(T), \mathcal{D}) \\\\ \alpha_{S,\mathcal{C}} \downarrow & & \alpha_{T,\mathcal{D}} \downarrow \\\\ \mathbf{Set}(S, \mathrm{Ob}(\mathcal{C})) & \underset{\mathbf{Set}(\mathbf{f}, \mathrm{Ob}(\mathbf{F}))}\longrightarrow & \mathbf{Set}(T, \mathrm{Ob}(\mathcal{D})) \end{matrix}$

Now we are ready to prove the naturality of \$$\alpha\$$. Namely, we have to show that

$\mathbf{Set}(\mathbf{f}, \mathrm{Ob}(\mathbf{F}))\circ\alpha_{S,\mathcal{C}}(\mathbf{G})=\alpha_{T,\mathcal{D}}\circ\mathbf{Cat}(\mathrm{Disc}(\mathbf{f}), \mathbf{F})(\mathbf{G})\quad\quad \forall \mathbf{G}\in \mathbf{Cat}(\mathrm{Disc}(S), \mathcal{C})$

Below is just the same as [the proof](https://forum.azimuthproject.org/discussion/comment/19801/#Comment_19801) provided by Dan but combining the 2 cases there into a single case.

Starting from the left side, we have

$\mathbf{Set}(\mathbf{f}, \mathrm{Ob}(\mathbf{F}))\circ\alpha_{S,\mathcal{C}}(\mathbf{G})=\mathrm{Ob}(\mathbf{F})\circ\alpha_{S,\mathcal{C}}(\mathbf{G})\circ\mathbf{f}$
according to the definition of the Hom-functor in Lecture 52.

Moreover, what \$$\alpha_{S,\mathcal{C}}\$$ does is sending functors in \$$\mathbf{Cat}(\mathrm{Disc}(S), \mathcal{C})\$$ to the set function on objects, that is, \$$\alpha_{S,\mathcal{C}}\$$ acts the same as the functor \$$\mathrm{Ob}\$$ on \$$\mathbf{Cat}(\mathrm{Disc}(S), \mathcal{C})\$$. Hence, we further have
$\mathrm{Ob}(\mathbf{F})\circ\alpha_{S,\mathcal{C}}(\mathbf{G})\circ\mathbf{f}=\mathrm{Ob}(\mathbf{F})\circ\mathrm{Ob}(\mathbf{G})\circ\mathbf{f}$

Next, Dan recognized that the composition \$$\mathrm{Ob}\circ\mathrm{Disc}\$$ is the same as the identity function on the set \$$\mathbf{Set}^\text{op}(S,T)\$$, so
$\mathrm{Ob}(\mathbf{F})\circ\mathrm{Ob}(\mathbf{G})\circ\mathbf{f}=\mathrm{Ob}(\mathbf{F})\circ\mathrm{Ob}(\mathbf{G})\circ\mathrm{Ob}(\mathrm{Disc}(\mathbf{f}))$

Since \$$\mathrm{Ob}\$$ is a functor, it preserves compositions. We can further imply
\begin{matrix}
\mathrm{Ob}(\mathbf{F})\circ\mathrm{Ob}(\mathbf{G})\circ\mathrm{Ob}(\mathrm{Disc}(\mathbf{f}))&=&\mathrm{Ob}(\mathbf{F}\circ\mathbf{G}\circ\mathrm{Disc}(\mathbf{f}))\\\\
&:=&\mathrm{Ob}\circ\\mathbf{Cat}(\mathrm{Disc}(\mathbf{f}), \mathbf{F})(\mathbf{G})\\\\
&:=&\alpha_{T,\mathcal{D}}\circ\mathbf{Cat}(\mathrm{Disc}(\mathbf{f}), \mathbf{F})(\mathbf{G}),
\end{matrix}

which we invoked, again, the definitions of \$$\alpha_{T,\mathcal{D}}\$$ and \$$\mathbf{Cat}(\mathrm{Disc}(\mathbf{f}), \mathbf{F})\$$.

This shows that \$$\mathbf{Set}(\mathbf{f}, \mathrm{Ob}(\mathbf{F}))\circ\alpha_{S,\mathcal{C}}(\mathbf{G})=\alpha_{T,\mathcal{D}}\circ\mathbf{Cat}(\mathrm{Disc}(\mathbf{f}), \mathbf{F})(\mathbf{G})\$$ for all \$$\mathbf{G}\in \mathbf{Cat}(\mathrm{Disc}(S), \mathcal{C})\$$.