Let $V$ be a symmetric closed monoidal category and denote with $[-,=]:V^{°} \otimes V \rightarrow V$ its internal hom. Let $j_x : 1 \rightarrow [x,x]$ be the adjoint to the left-unitor $\lambda_x : 1 \otimes x \rightarrow x$. Suppose we have a morphism $f : 1 \rightarrow x$, I want to prove that the following diagram commutes $\require{AMScd}$ \begin{CD} 1 @>{j}>> [x,x]\\ @VVjV @VV[f,1]V\\ [1,1] @>{[1,f]}>> [1,x]. \end{CD} My idea was to show that both arrows are adjoints to the same morphism $1\otimes 1 \rightarrow x$. It's relatively easy to show that the adjoint to $[1,f] \cdot j$ is $f \cdot \lambda_1$. My problem is to show the same also for $[f,1] \cdot j$.
By using the extranaturality of the evaluation $ev_{z,y} : [z,y]\otimes z \rightarrow y$, as expressed in the following commutative diagram, $\require{AMScd}$ \begin{CD} [x,x]\otimes 1 @>{[x,x]\otimes f}>> [x,x]\otimes x\\ @VV[f,1]\otimes 1V @VV{ev}V\\ [1,x]\otimes 1@>ev>>x \end{CD}
I was able to show that the adjoint to $[f,1] \cdot j$ is $ev \cdot j\otimes f$, but I don't know how to conclude that $ ev\cdot j\otimes f = f \cdot \lambda_1$ as I expected.
Apparently it was simpler than I expected.
We have \begin{align} ev \cdot j \otimes f &= ev \cdot 1 \cdot [x,x] \otimes f \cdot j\otimes 1,\\ &= ev \cdot j\otimes x \cdot 1 \otimes f, \\ &= \lambda_x \cdot 1 \otimes f, \end{align} where $ev \cdot j\otimes x = \lambda_x$ follows directly from the definition of $j$. Since $\lambda$ is natural, we have $\lambda_x \cdot 1 \otimes f = f \cdot \lambda_1$ which is exactly what I wanted to prove.