# From a coend over a pair to a coend over the tensor product

I'm trying to find a simple proof that a monoid under Day convolution is equivalent to a lax monoidal functor (see nCatLab). 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?

• The case of sets does not simplify the question. The general case works exactly the same. Mar 10 '17 at 11:04

$$\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.