Equivalence between lax monoidal functors and monoids in the functor category. I'm trying to go through the details of Proposition 3.4 of:
https://ncatlab.org/nlab/show/Day+convolution
For whatever reason, I don't see how to translate the conditions of a lax monoidal functor into a monoidal object of the functor category. I understand how to get the multiplication and unit maps of the monoid via the natural isomorphism from the maps defining the lax monoidal functor, but then proving something like the unit diagram for a monoidal object escapes me.
In more detail: Suppose $F: \mathcal{C} \to \mathcal{V}$ is lax monoidal. Then we have by definition maps $$ \lambda: I_\mathcal{V}\to F(I_\mathcal{C}) \\ \phi_{x,y}: F(x)\otimes F(y)\to F(x\otimes y). $$ The Yoneda lemma gives us a map $\bar{\lambda}:y(I)\to F$ and the natural isomorphism given by the definition of day convolution as a left kan extension gives a map $\bar{\phi}:F\otimes_{Day} F\to F$. How does one then show that the composition $$ y(I)\otimes F \overset{\bar{\lambda}\otimes id}\to F\otimes F \overset{\bar{\phi}}\to F $$ is then the same as the left identity natural isomorphism in the monoidal structure given by day convolution?
 A: I strongly suspect that there should be a cleaner, higher level proof of this fact. However, here's a concrete computation.
As I understand it, you're trying to show that a lax monoidal structure on $F$ induces a monoid structure on $F$ with respect to Day convolution on the functor category.
Where you're getting stuck is showing that the left unitality condition on the lax monoidal structure translates into left unitality for the monoidal structure.
First, what is the left unitor for the Day convolution monoidal structure anyway?
Let's consider. Let $\newcommand\C{\mathcal{C}}\newcommand\V{\mathcal{V}}F,X:\C\to \V$ be functors.
$$
\newcommand\Day{\mathrm{Day}}
\newcommand\uln{\underline}
\newcommand\oln\overline
\begin{align*}
[\C,\V](\uln{\C}(I_\C,-)\otimes_{\Day}F,X) &\simeq [\C\times\C,\V](\uln\C(I_\C,-)\otimes_\V F-,X\circ\otimes_\C)
\\
&\simeq \int_{c,c'\in\C}\V(\uln\C(I_\C,c)\otimes_\V Fc',X(c\otimes_\C c')
)
\\
&\simeq 
\int_{c,c'\in\C}\V(\uln\C(I_\C,c),\uln\V(Fc',X(c\otimes_\C c')))
\\
&\simeq \int_{c\in\C}\V(I_\V,\uln{\V}(Fc',X(I_\C\otimes_\C c')))
\\
&\simeq
\int_{c'\in\C}\V(Fc',X(I_\C\otimes_\C c'))
\\
&\simeq 
\int_{c'\in\C}\V(Fc',Xc')
\\
&\simeq
[\C,\V](F,X).
\end{align*}
$$
Arguments:

*

*Definition of left Kan extension

*Expansion of natural transformations into end

*I'm assuming $\V$ is closed monoidal and adjointing over

*(Enriched) Yoneda lemma applied to $c$. (Composing with the map $I_\V\to \uln\C(I_\C,I_\C)$ induces a bijection)

*Adjoint back over and compose with the inverse of the left unitor in $\V$

*left unitor in $\C$

*The end computes natural transformations

Side note We don't actually have to adjoint over and back, but I'm trying to avoid essentially reproving the enriched Yoneda lemma.
To find the left unitor we set $X=F$ and trace $1_F$ backwards through the chain.
Alternatively to prove that $ \oln{\phi}(\oln{\lambda}\otimes 1_F)$ is the left unitor, we can put that at the top and trace it forwards.
Let $$\tilde{\phi}_{c,c'} : F(c)\to \uln{V}(F(c'),F(c\otimes_{\C}c'))$$ be the adjoint of $$\phi_{c,c'} : F(c)\otimes_\V F(c')\to F(c\otimes_{\C}c').$$
Let $\iota_c:I_\V\to \uln\C(c,c)$ be the unit maps of the enriched category $\uln\C$.
Then we can trace through:
$$
\newcommand\of[1]{\left({#1}\right)}
\begin{align*}
\oln\phi\circ(\oln\lambda\otimes_{\Day} 1_F)&\mapsto \phi\circ (\oln\lambda\otimes_V 1_F)
\\
&\mapsto
\of{\phi_{c,c'}\circ (\oln\lambda_c\otimes_\V 1_{F,c'})}_{c,c'\in\C}
\\
&\mapsto
\of{\tilde\phi_{c,c'}\circ \oln\lambda_c}_{c,c'\in\C}
\\
&\mapsto
\of{\tilde\phi_{I_\C,c'}\circ \oln\lambda_{I_\C}\circ \iota_{I_\C}}_{c'\in\C}
\\
&\mapsto
\of{\phi_{I_\C,c'}\circ (\lambda \otimes 1_{F,c'})\circ \ell^{\V,-1}_{Fc'}}_{c'\in\C}
\\
&\mapsto
\of{F(\ell^\C_{c'})\circ \phi_{I_\C,c'}\circ (\lambda \otimes 1_{F,c'})\circ \ell^{\V,-1}_{Fc'}}_{c'\in\C}
\\
&\mapsto
F(\ell^\C_{-})\circ \phi_{I_\C,-}\circ (\lambda \otimes 1_{F,-})\circ \ell^{\V,-1}_{F-}
= 1_F
\end{align*}
$$
Explanation:

*

*$\oln\phi$ is the adjunct of $\phi$

*Expansion into components

*Adjointing over using $\V$ is closed monoidal

*Apply the Yoneda lemma to find the corresponding map by evaluating at the corepresenting object and composing with the identity morphism.

*Adjoint back over and compose with $\V$'s left unitor. Note that $\oln\lambda_{I_\C}\circ\iota_{I_\C}$ is $\lambda$, since we defined $\oln\lambda$ by Yoneda in the first place.

*Compose with the left unitor in $\C$

*Tried to write it in a componentless fashion, and then used the lax monoidal left unit identity.

