How to construct an internal hom functor for a closed monoidal category? I am studying closed monoidal category through Wikipedia and nLab. There could be misconceptions in my post. Please let me know in that case.
Definition of a Closed Monoidal Category
Let $M$ be a symmetric monoidal category. $M$ is closed if and only if there are:

*

*an assignment $[-,-]$, called an internal hom of $M$, sending each pair $(b,c)$ of objects in $M$ to some object $[b,c]$ in $M$, and each pair $(1_b,h)$ of morphisms in $M$ to some morphism $[1_b,h]$ in $M$, and

*an assignment $\eta$, called currying of $M$, sending each triple $(a,b,c)$ of objects in $M$ to some function $\eta_{a,b,c}:\operatorname{Hom}(a\otimes b,c)\to\operatorname{Hom}(a,[b,c])$,

such that for all object $b$ in $M$:

*

*$[b,-]$, sending $c$ to $[b,c]$ and $h$ to $[1_b,h]$, is a functor;

*$\eta_{-,b,-}:\operatorname{Hom}(-\otimes b,-)\to\operatorname{Hom}(-,[b,-])$ is a natural isomorphism.

(I did not use the term "right adjoint" in the definition, but I know what it is, so you can use that concept in the answer.)
Question
How does one prove that the internal hom above can be extended in a unique way to a functor $[-,-]:M^{\operatorname{op}}\times M\to M$ such that $\eta:\operatorname{Hom}(-\otimes-,-)\to\operatorname{Hom}([-,-],-)$ is a natural isomorphism?
My Attempt
Let $g:b'\to b$ and $h:c\to c'$ be morphisms in $M$. We should define $[g,h]$, and then check that $[-,-]$ becomes a functor and $\eta$ becomes a natural isomorphism. The requirement that $\eta$ should be a natural transformation forces the following diagram to commute:
$\require{AMScd}$
\begin{CD}
\operatorname{Hom}([b,c]\otimes b,c) @>{\eta_{[b,c],b,c}}>> \operatorname{Hom}([b,c],[b,c])\\
@VVV @VVV\\
\operatorname{Hom}([b,c]\otimes b',c') @>{\eta_{[b,c],b',c'}}>> \operatorname{Hom}([b,c],[b',c'])
\end{CD}
So there is only one way to define $[g,h]$. Namely,
\begin{equation}
[g,h] = \eta_{[b,c],b',c'}(h\circ(\eta_{[b,c],b,c}^{-1}(1_{[b,c]}))\circ(1_{[b,c]}\otimes g))\text{.}
\end{equation}
I proved that $[1_b,1_c]=1_{[b,c]}$ for all objects $b,c$ in $M$. But I could not prove that $[g',h']\circ[g,h]=[g\circ g',h'\circ h]$. Both sides of the equation becomes too messy when spelled out.
 A: Nice work so far! I think breaking down the definition of this functor into smaller pieces will be helpful.
Given a morphism $g : b' \to b$ and an object $c$, we define $[g,1_c] : [b,c] \to [b',c]$ to be
$$\eta_{[b,c],b',c}(\eta_{[b,c],b,c}^{-1}(1_{[b,c]}) \circ (1_{[b,c]} \otimes g)).$$
Then we verify two conditions:

*

*$[g_1 \circ g_2, 1_c] = [g_2, 1_c] \circ [g_1, 1_c]$ for all morphisms $g_1 : b' \to b$, $g_2 : b'' \to b'$, and all objects $c$.

*$[1_{b'}, h] \circ [g,1_c] = [g, 1_{c'}] \circ [1_b, h]$ for all morphisms $g : b' \to b$ and $h : c \to c'$.

From these two facts it follows that defining $[g, h] = [g, 1_{c'}] \circ [1_b, h]$ makes $[{-},{=}]$ into a functor. This is general phenomenon: to define a functor $C_1 \times C_2 \to D$, you just need to describe the functoriality in each component and then check that they "commute" (in the sense of condition 2 above).
Unfortunately I don't have time to write a full answer right now, but I hope this helps you finish the proof -- the benefit of doing it this way is that you only have to deal with two morphisms (instead of four) at any time.

For condition 1, we equivalently need to verify that the following diagram commutes:

(Check that this is really equivalent!). The three morphisms in this diagram also appeared in the commutative squares witnessing the naturality of $\eta$ (the square you drew in your post). So we paste those squares around the outside as follows:

Now check that the squares & triangles marked in red commute, and use the fact that the colored arrows are isomorphisms to deduce that the inner triangle commutes.
Apologies for the poor handwriting, I hope it's still understandable!
