I am reading Closed Categories, Eilenberg and Kelly, 65 and get extremely confused by one equivalence proof of coherence conditions.
In particular, I am struggling with the following equivalence:
where $\pi : Hom(A \otimes B , C) \to Hom(A, [B , C])$ is the usual natural isomorphism induced by the adjoint pair $-\otimes B \dashv [B , -]$. $\eta$ and $\epsilon$ are the unit and counit transformations of the adjoint.
$a, l, r$ are the associator, left unitor and right unitor of the monodal component.
$L : [B,C] \to [ [A , B], [A , C]]$ is the internal left composition transformation.
$p : [A \otimes B, C] \to [A, [B , C]]$ is the currying transformation.
$i : A \to [ u, A ]$ is the natural isomorphism, where $u$ is the monoidal unit.
In the paper, it claims that the diagrams in the image are equivalent. I understand that MCC4 and CC4 are equivalent and they imply MC4. But I have got no idea why MC4 also implies MCC4 or CC4.
In particular, in the proof in the paper, computation 1 is performed. The computation begins with applying $\pi$ twice to MC4, which eventually concludes
$$p[r , 1]\eta = [1, i] \eta$$
then the paper concludes $p[r, 1] = [1, i]$ which corresponds to the bottom left corner of the diagram on the right. This step confuses me. How does this work?
I also know MCC4 and CC4 equals to $\pi(\pi(\epsilon r))$, but that doesn't seem to help solve the problem.
I still don't know how the proof above works but there is another way to prove it by making use of the naturality of $i$.
consider the following computation
$$ \begin{align} p[r,1] &= \pi(\pi(\epsilon r)) \tag*{naturality of $\pi$} \\ &= \pi([1,\epsilon] \circ\pi(r)) \\ &= \pi([1,\epsilon] \circ i) \tag*{naturality of $i$}\\ &= \pi(i\epsilon) \tag*{naturality of $\epsilon$}\\ &= \pi(\pi^{-1}[1,i]) \\ &= [1,i] \end{align} $$
this is mechanized in
https://github.com/agda/agda-categories/blob/master/Categories/Category/Monoidal/Closed/IsClosed.agda#L265