In Chapter 12 of Call-by-Push-Value, Levy states that a strong monad on a Cartesian category $\mathcal C$ is equivalent to a monad in the 2-category of $[\mathcal C^{\mathit{op}},Sets]$-enriched categories on the simple fibration $\mathit{self}~\mathcal C$ over $\mathcal C$.
I had trouble laying out the details of this and am wondering if someone can give me some help.
A $[\mathcal C^{\mathit{op}},Sets]$-enriched endofunctor on $\mathcal {self}~\mathcal C$ consists of
- A mapping on objects $(X \in \mathcal C_0) \mapsto (TX \in \mathcal C_0)$
- For each pair $X,Y \in \mathcal C_0$, a natural transformation $T_{X,Y} : \mathcal{C}(- \times X, Y) \to \mathcal{C}(- \times TX,TY)$
To show that this is a strong functor on $\mathcal C$, we must first find a family of $\mathcal C$-arrows $\mathit{t}_{X,Y} : X \times TY \to T(X \times Y)$.
Given $X,Y \in \mathcal C_0$, we have $id_{X \times Y} : X \times Y \to X \times Y$. Mapping this through $(T_{Y,X \times Y})_X$ gives an an arrow $t_{X,Y} : X \times TY \to T(X \times Y)$.
We now need to prove that the family $t_{X,Y}$ is a natural transformation from $$\mathcal - \times T- : \mathcal C^2 \to \mathcal C$$ to $$T(- \times -) : \mathcal C^2 \to \mathcal C$$
I'm struggling to figure this out.