Multiplication and division by a morphism under the “inner composition” in closed monoidal categories I asked this a week ago at math.stackexchange, without success, so I hope it will be appropriate here.
Let ${\mathcal C}$ be a symmetric closed monoidal category, and let me denote the internal hom-functor by a fraction
$$
(X,Y)\mapsto\frac{Y}{X},
$$
so that we have an isomorphism of functors
$$
\operatorname{Mor}(A\otimes B,C)\cong \operatorname{Mor}\left(A,\frac{C}{B}\right).
$$
As is known, ${\mathcal C}$ is an enriched category over itself. For each objects $A,B,C$ let me denote by $\bullet_{A,B,C}$ the "inner composition" in ${\mathcal C}$ as in an enriched category, i.e. the morphism 
$$
\bullet_{A,B,C}:\frac{C}{B}\otimes\frac{B}{A}\to\frac{C}{A}
$$
with the corresponding properties.

I wonder if the following identity always holds
  $$
\bullet_{A,C,D}\circ\left(1_{\frac{D}{C}}\otimes\frac{\varphi}{1_A}\right)= 
\bullet_{A,B,D}\circ\left(\frac{1_D}{\varphi}\otimes1_{\frac{B}{A}}\right)
$$
  (for arbitrary objects $A,B,C,D$ and for arbitrary morphism $\varphi:B\to C$).


This is strange, I can prove this only in the case when the unit $I$ is a separating object in ${\mathcal C}$ (what does not always hold). Is it possible that there is a counterexample?
 A: Yes, this equation follows from the axioms of closed monoidal categories. I think the easiest way to prove this is to show that the corresponding pair of multimaps $\frac{D}{C}, \frac{B}{A} \to \frac{D}{A}$ are equal in any closed multicategory, which you can do by expressing them as (ordered linear) lambda terms and checking that they have the same normal form.
Let $b:B \vdash \varphi:C$ be an arbitrary term with one free variable $b$.
Define two terms $t_1$ and $t_2$ of type
$$
f:\frac{D}{C}, g:\frac{B}{A} \vdash t_i : \frac{D}{A}
$$
by
$$
t_1 := \lambda a.f ((\lambda a'.\varphi[g(a')/b])a)
$$
$$
t_2 := \lambda a.(\lambda b'.f (\varphi[b'/b]))(g(a))
$$
where "$t[u/x]$" denotes the capture-avoiding substitution of the term $u$ for the variable $x$ in $t$.
These correspond to the two morphisms $\bullet_{A,C,D}\circ\left(1_{\frac{D}{C}}\otimes\frac{\varphi}{1_A}\right)$ and $\bullet_{A,B,D}\circ\left(\frac{1_D}{\varphi}\otimes1_{\frac{B}{A}}\right)$, respectively,
but both $t_1$ and $t_2$ normalize (after one $\beta$-reduction) to the same term
$$
t = \lambda a.f (\varphi[g(a)/b])
$$
which proves that the two morphisms are equivalent modulo the equations of closed monoidal categories.
(In the above I have been implicitly treating your $\otimes$ as a comma, but if we want to be completely rigorous about this we can work with a closed representable multicategory.)
A: Noam’s answer is already good and complete, but here is alternate answer phrased more elementarily in terms of the symmetric monoidal category structure.  We want to show
$$\bullet_{A,C,D}\circ\left(1_{[C,D]}\otimes[1_A,\varphi]\right)= 
\bullet_{A,B,D}\circ\left([\varphi,1_D]\otimes 1_{[A,B]}\right) : [C,D] \otimes [A,B] \to [A,D] $$
It’s enough to show their corresponding exponential transpose maps $[C,D] \otimes [A,B] \otimes A \to D$ agree.  But for these, we have:
$$ \newcommand{\ev}{\operatorname{ev}} 
\ev_{A,D} \circ \left( (\bullet_{A,C,D} \circ(1_{[C,D]}\otimes[1_A,\varphi])) \otimes 1_A \right) \\
= \ev_{A,D} \circ (\bullet_{A,C,D} \otimes 1_A)\circ\left(1_{[C,D]}\otimes[1_A,\varphi] \otimes 1_A\right) \\
= \ev_{C,D} \circ (1_{[C,D]} \otimes \ev_{A,C})\circ \left(1_{[C,D]}\otimes[1_A,\varphi] \otimes 1_A\right) \\
= \ev_{C,D} \circ (1_{[C,D]} \otimes (\ev_{A,C} \circ ([1_A,\varphi] \otimes 1_A)))
\\
= \ev_{C,D} \circ (1_{[C,D]} \otimes (\varphi \circ \ev_{A,B})) \\
= \ev_{C,D} \circ (1_{[C,D]} \otimes \varphi) \circ (1_{[C,D]} \otimes \ev_{A,B})
 $$
and a similar calculation shows 
$$ \ev_{A,D} \circ \left( (\bullet_{A,B,D}\circ([\varphi,1_D]\otimes 1_{[A,B]})) \otimes 1_A \right)  = \ev_{C,D} \circ (1_{[C,D]} \otimes \varphi) \circ (1_{[C,D]} \otimes \ev_{A,B}).$$
Each step is just using either the monoidal category laws, or the fact that the maps $\bullet_{A,C,D}$, $[1_A,\varphi]$ are defined by their exponential transpose maps.
(Please excuse my using the notation $[A,B]$ for mapping objects, since I’m more familiar with it than the fraction notation $\frac{B}{A}$.)
