Vertical and Horizontal Isomorphisms in 2-categories Assume having a monoidal category $(\mathcal{A},I,\otimes)$ where each object has an inverse, i.e. for every object $A$ there is an object $\bar{A}$ with $A\otimes\bar{A}=\bar{A}\otimes A=I$. Then I wonder: If $f:X\rightarrow Y$ is an arrow, is $f$ invertible with respect to $\circ$ if and only if $f$ is invertible with respect to $\otimes$? The latter meaning that there is an arrow $\hat{f}:\bar{X}\rightarrow\bar{Y}$ with $f\otimes\hat{f}=\hat{f}\otimes f=I$. I'm thinking of: Define $\bar{f}:\bar{Y}\rightarrow\bar{X}$ as $\bar{X}\otimes f\otimes\bar{Y}$ (or $\bar{Y}\otimes f\otimes\bar{X}$, is it the same?). Then define $\hat{f}=\bar{f}^{-1}$. But I don't know whether that is an inverse to $f$ (wrt $\otimes$).
 A: I assume your are talking about a symmetric strict monoidial category $\mathcal{M}$. 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', that is they fit in suitable commutative diagram. However for composing bars you need to insert the symmetry isomorphism $\gamma: A\otimes B \otimes C \mapsto C \otimes B \otimes A$ in suitable places, like this $ \bar{f}:= \gamma \circ (\bar{X} \otimes f \otimes \bar{Y}): \bar{X} \otimes X \otimes \bar{Y} \to \bar{Y} \otimes X\otimes \bar{X}$.)
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.
As you suggested, define $\hat{f}:= \rho_{\bar{X}} \circ (\bar{X} \otimes \iota_Y)\circ (\bar{X} \otimes f \otimes \bar{Y}) \circ (\iota_{\bar{X}} \otimes \bar{Y})^{-1} \circ  \lambda_{\bar{Y}}^{-1}: \bar{Y} \to \bar{X}$
Where $\lambda_Y:I \otimes Y \to Y$ and $\rho_X: X \otimes I \to X$ are the designed natural isomorphims.
Exploiting the compatablity laws, this gives you $\hat{g} \circ \hat{f} = \mathrm{id}_X$ for $g:= f^{-1}$. Thus you obtain 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.
Edit:
I wonder if you obtain an endofunctor $\mathcal{M}^{op} \to \mathcal{M}$ via $X \mapsto \bar{X}$ and $f \mapsto \hat{f}$.
Well, probably you need some conditions like $\bar{\bar{X}} = X$ and $\iota_{\bar{X}} = {\iota_X}^{-1}$. I will think about. This may be also related to other direction.
A: Before answering, let me remark that it's generally considered a little weird (some would say, with tongue partly in cheek, "evil") to posit categorical axioms which enforce equalities between objects, since models of such axioms will not be invariant with respect to categorical equivalences. Such axioms ought to be replaced by enforcing corresponding isomorphisms between objects, satisfying suitable coherence axioms. 
With that in mind, let's start by putting the question a little differently: suppose that for each object $X$ we have units $\eta_X: I \to \bar{X} \otimes X$, $\eta_X': I \to X \otimes \bar{X}$, and counits $\epsilon_X: X \otimes \bar{X} \to I$, $\epsilon_X': \bar{X} \otimes X \to I$ such that the triangular equations for adjunctions $X \dashv \bar{X}$, $\bar{X} \dashv X$ hold and 
$$\eta_X' \circ \epsilon_X = 1_{X \otimes \bar{X}}, \qquad \eta_X \circ \epsilon_X' = 1_{\bar{X} \otimes X}$$ 
$$\epsilon_X \circ \eta_X' = 1_I = \epsilon_X' \circ \eta_X$$ 
(Edit: As noted by Chris and myself below, given an object $\bar{X}$ and invertible maps $\eta_X: I \to \bar{X} \otimes X$, $\phi: I \to X \otimes \bar{X}$, one can always construct an invertible map $\eta_X': I \to X \otimes \bar{X}$ such that $\epsilon_X := (\eta_X')^{-1}$ and $\epsilon_X' := (\eta_X)^{-1}$ are counits that fit into appropriate triangular equations. Details (for the more general case of 2-categories or bicategories in place of monoidal categories) are given in the nLab article mentioned in my comment.) 
Then, as you surmise, $f$ is invertible with respect to $\circ$ iff it is "invertible with respect to $\otimes$". Essentially we follow your definition of $\bar{f}$ given $f^{-1}$, defining 
$$\bar{f} = (\epsilon_X' \otimes 1_{\bar{Y}}) \circ (1_{\bar{X}} \otimes f^{-1} \otimes 1_{\bar{Y}}) \circ (1_{\bar{X}} \otimes \eta_Y)$$ 
and what we really mean by "invertible with respect to $\otimes$" is that we have equations 
$$\epsilon_Y \circ (f \otimes \bar{f}) \circ \eta_X' = 1_I = \epsilon_Y' \circ (\bar{f} \otimes f) \circ \eta_X.$$
The most perspicuous way to show these equations hold is by using string diagram calculus. Since I am not too handy with graphics, I'll just briefly sketch how to derive the first equation, leaving it to you to believe or verify that the second equation works similarly. The main steps are that 
$$\begin{array}
\epsilon_Y \circ (f \otimes \bar{f}) \circ \eta_X' & = & \epsilon_Y \circ (f \otimes 1_{\bar{Y}}) \circ (1_X \otimes \epsilon_X' \otimes 1_X \otimes 1_{\bar{Y}}) \circ (\eta_X' \otimes 1_X \otimes 1_{\bar{Y}}) \circ (f^{-1} \otimes 1_{\bar{Y}}) \circ \eta_Y' \\\ 
 & = & \epsilon_Y \circ (f \otimes 1_{\bar{Y}}) \circ (f^{-1} \otimes 1_{\bar{Y}}) \circ \eta_Y' \\\ 
 & = & \epsilon_Y \circ \eta_Y' \\\ 
 & = & 1_I
\end{array}
$$ 
where the first equation uses the definition of $\bar{f}$ and axioms of a monoidal category, the second uses a triangular equation, and the fourth uses one of the invertibility axioms for $Y$. Remaining details are similarly routine. 
