If $A \cong I$ in a monoidal category, then any arrow $X \otimes A \to Y \otimes A$ decompose into $(X \to Y) \otimes 1$ The question is originated from the answer of this post. Let me make it precise first. Suppose $(\mathcal{A}, \otimes, I)$ is a monoidal category and $A\in \mathcal{A}$ is an object isomorphic to $I$. Then for any morphism $g:X \otimes A \to Y \otimes A$ in $\mathcal{A}$ there is a unique morphism $f:X\to Y$ such that $g = f \otimes 1_A$.
$\textbf{Attempt}$
Let $k:A \to I$ be an isomorphism. Given any such $g$, there is an arrow
$$X \xrightarrow{\rho^{-1}} X \otimes I \xrightarrow{1 \otimes k^{-1}} X \otimes A \xrightarrow{g} Y \otimes A \xrightarrow{1 \otimes k} Y \otimes I \xrightarrow{\rho} Y$$
(and I think that's the only way to construct a morphism $X \to Y$). But I don't see how this map tensoring with the identity gives you $g$. I believe it is just some sort of combining different diagrams together + the interchange law, as you normally do proofs in monoidal category. I have no clue on the uniqueness part of the morphism either. Any help is appreciate.
 A: You can show that if $g$ is of the form $f \otimes 1_A$ then your composite returns $f$: use functoriality of the tensor product to cancel out the $1 \otimes k$'s and then use naturality of $\rho$.
At the same time, your construction is clearly invertible, because it's given by composing with the invertible morphisms $1 \otimes k$ and $\rho$. Therefore if we define $f$ to be your composite
$$X \xrightarrow{\rho^{-1}} X \otimes I \xrightarrow{1 \otimes k^{-1}} X \otimes A \xrightarrow{g} Y \otimes A \xrightarrow{1 \otimes k} Y \otimes I \xrightarrow{\rho} Y$$
we can look at applying the inverse of your construction to get
$$X \otimes A \xrightarrow{1 \otimes k} X \otimes I \xrightarrow{\rho} X \xrightarrow{f} Y \xrightarrow{\rho^{-1}} Y \otimes I \xrightarrow{1 \otimes k^{-1}} Y \otimes A$$
This will give both $g$ (because that's what we started with) and $f \otimes 1_A$ (because as we saw in the first part we could have started with that and got the same $f$). Therefore $g$ and $f \otimes 1_A$ are equal, and this establishes your construction as being the inverse of the function given by tensoring by $1_A$.
A: A briefer, though perhaps less satisfying, argument: since $A$ is isomorphic to $I$ and by definition $(-)\otimes I$ is naturally isomorphic to the identity functor, also $(-)\otimes A$ is naturally isomorphic to the identity functor, say via $\alpha$. Then we have a natural isomorphisms $\mathrm{Hom}(X,Y)\to \mathrm{Hom}(X,A\otimes Y)$ and $\mathrm{Hom}(X,A\otimes Y)\to \mathrm{Hom}(A\otimes X,A\otimes Y)$ given by post- and pre-composition with $\alpha$.
