Let $C$ be a category with, for each $X \in \text{Obj}(C)$, a comonad $F(X) : C \rightarrow C$ and a monad $G(X) : C \rightarrow C$, such that $F(X) \vdash G(X)$, i.e. there is for each $X, Y, Z$, an isomorphism $$ [F(X)(Y), Z]_C \cong [Y, G(X)(Z)]_C $$ natural in $Y$ and $Z$. Further suppose that there is a natural transformation $F(f) : F(X) \implies F(Y)$ for each $f : X \rightarrow Y$, and likewise for $G$, making all of the relevant diagrams commute.
This forms a semantics for typed lambda calculus. My question is whether this forces $F$ to be product. I suspect that it does, but cannot manage to show it.