The principle at work here is that while call-by-push-value gives us a
syntax for an adjunction (between value and computation categories)
with a syntax for the profunctor the adjunction represents (the term
morphisms), we can also consider the \emph{Kleisli} categories of the
adjunction, which are equivalent to the images of the $\u F$ and $U$
types.
%
These are precisely the categories corresponding to call-by-value and
call-by-name languages respectively.
%
Then we can ask in what sense the connectives extend from functors on
the value and computation categories to ``functors'' on the
corresponding Kleisli and co-Kleisli categories.
%
We put ``functor'' in quotes because in fact, these will not quite
satisfy the ordinary sense of functoriality in multiple arguments.
%
Instead, the functors will be \emph{separately functorial} in each
argument, whereas ordinarily functor in several argument means
\emph{jointly functorial}.
%
So for example let $\cat C, \cat D , \cat E$ be categories, then we
would say that a separately functorial function $F : \cat C, \cat D
\to \cat E$ would consist of first an action on objects $F_0 : \cat
C_0, \cat D_0 \to \Cat E_0$ and then two actions: taking any object $d
\in D_0$ to a functor $F(-,id_d) : \cat C \to \cat E$ and similarly
one taking any object $c \in C_0$ to a functor $F(id_c,=): \cat D \to
\cat E$.
%
Then we have two candidates for a true joint functorial action that
are in general not equal: $F(f,id)\circ F(id,g)$ and vice-versa
$F(id,g) \circ F(f,id)$.
%
The fact that these are \emph{not} models the fact that evaluation
order matters.

\begin{theorem}[Effectful Functors]
  Given a call-by-push-value adjunction model $V,C,R,F,U$ and given
  any jointly functorial functor $G : D_1,\ldots,D_n \to E$ where all
  of $D_1,\ldots,D_n,E$ are either $V,C,V^o,C^o$, that is
  \emph{strong} in that for each argument category $D_i$, there are
  morphisms of one of the following forms (whichever is well-sorted
  for $G$ and $D_i$)

  \[ G(D_1,\ldots,F(D_i),\ldots,D_n) \to F(G(D_1,\ldots,D_n)) \]
  \[ G(D_1,\ldots,U(D_i),\ldots,D_n) \to F(G(D_1,\ldots,D_n)) \]
  \[ G(D_1,\ldots,F(D_i),\ldots,D_n) \to U(G(D_1,\ldots,D_n)) \]
  \[ G(D_1,\ldots,U(D_i),\ldots,D_n) \to U(G(D_1,\ldots,D_n)) \]
  
  then there is an
  associated separately functorial functor $\hat G : \hat
  D_1,\ldots,\hat D_n \to \hat E$ where

  
  \begin{align*}
    \hat V = F(V)\\
    \hat C = U(C)\\
    \hat D^o = (\hat D)^o
  \end{align*}
\end{theorem}
\begin{proof}
  
\end{proof}