I'm trying to find a simple proof that a monoid under Day convolution is equivalent to a lax monoidal functor (see [nCatLab](https://ncatlab.org/nlab/show/Day+convolution)). For simplicity, consider functors from $C$ to $Set$. For $F$ to be a monoid there has to be a natural transformation:


$ \mu : F \otimes F \to F $


where the tensor product is the Day convolution:


$F\otimes F := \int^{x y} C(x \otimes y, -) \times F(x) \times F(y)$


A lax monoidal functor has a natural transformation:


$F(x) \times F(y) \to F(x \otimes y)$


which we can plug in to get:


$\int^{x y} C(x \otimes y, -) \times F(x \otimes y)$


If I could only make a "change of variables" from $(x, y)$ to $x\otimes y$, like this:


$\int^{x \otimes y} C(x \otimes y, -) \times F(x \otimes y)$


I could use the ninja Yoneda lemma to perform the integral and get $F$. How do I convert this handwaving argument to a proof?



From a coend over a pair to a coend over the tensor product
This can be seen via a sequence of isomorphisms involving ends and co-ends, using the presentation of natural transformations via ends:


$$
\begin{array}{cl}
 & \int\_{xy} Fx \times Fy \to F (x \otimes y) \\
\cong& \int\_{xy} Fx \times F y \to (\int\_z C(x \otimes y,z) \to Fz) & (1) \\
\cong& \int\_{xyz} Fx \times Fy \to C(x \otimes y,z) \to Fz & (2) \\
\cong& \int\_{xyz} Fx \times Fy \times C(x \otimes y,z) \to Fz & (3) \\
\cong& \int\_z (\int^{xy} Fx \times Fy \times C(x \otimes y,z)) \to Fz & (4) \\
\cong& \int\_z (F \otimes F)z \to Fz & (5) \\
\cong& F \otimes F \Rightarrow F & (6)
\end{array}
$$


where $(1)$ is by Yoneda; $(2)$ is commuting of ends with exponentials; $(3)$ is currying; $(4)$ is currying with ends/co-ends; $(5)$ is the definition of the Day product; and $(6)$ is natural transformations as ends.


