Skip to main content
2 of 4
fixed some typos

I assume your are talking about a symmetric strict monoidial category. I think, you have to choose, beside $\bar{A}$, an isomorphism $\iota_A: A \otimes \bar{A} \to I$, say. I think $\iota_A = \mathrm{id}$ for all $A$ is not possible.

For any $f: X \to Y$ and $g:Y \to X$ follows, with your definition of $\bar{\square}$ and the interchange law:

$\bar{f} \circ \bar{g} := (\bar{X} \otimes f \otimes \bar{Y}) \circ (\bar{X} \otimes g \otimes \bar{Y}) = \bar{X} \otimes f \circ g \otimes \bar{Y}: \bar{X} \otimes X \otimes \bar{Y} \to \bar{X} \otimes Y \otimes \bar{Y}$

(By the symmetry, both of your definitons of $\bar{\square}$ agree, they fit in suitable commutative diagram)

That is, $f$ and $g$ are inverse then $\bar{f}$ and $\bar{g}$ are inverse to each other. Well, of course, this is nothing the compatability laws in your monoidial category. However, $\bar{\square}$ is not a functor.

Now the passage from $\bar{f}$ to $\hat{f}:= \rho_X \circ (\bar{X} \otimes \iota_Y)\circ \bar{f} \circ (\iota_X \otimes \bar{Y})^{-1} \circ \lambda_Y^{-1}$ is by composing with isomorphisms, so also $\hat{f}$ and $\hat{g}$ will be inverse to each other as well. Where $\lambda_Y:I \otimes Y \to Y$ and $\rho_X: X \otimes I \to X$ are the designed natural isomorphims. This again just exploits the compatability laws in monoidial cats and gives you one implication.

I see, in the meantime Todd Trimble gave an answer which completly subsume mine. However as it took me some time to type it, i post it as a 'down to earth' version.