@@ -445,7 +445,7 @@ We now turn to the most important way of obtaining op-prederivators.

\begin{example}

Let $F : \C\to\C'$ be a functor and suppose that $\C$ and $\C'$ are cocomplete. The morphism induced by $F$ at the level of represented op-ederivators is cocontinuous if and only if $F$ is cocontinuous in the usual sense.

\end{example}

\begin{paragr}

\begin{paragr}\label{paragr:prederequivadjun}

As in any $2$-category, the notions of equivalence and adjunction make sense in $\PPder$. Precisely, we have that:

\begin{itemize}

\item[-] A morphism of op-prederivators $F : \sD\to\sD'$ is an equivalence when there exists a morphism $G : \sD' \to\sD$ such that $FG$ is isomorphic to $\mathrm{id}_{\sD'}$ and $GF$ is isomorphic to $\mathrm{id}_{\sD}$; the morphism $G$ is a \emph{quasi-inverse} of $F$.

...

...

@@ -507,7 +507,7 @@ We now turn to the most important way of obtaining op-prederivators.

\]

\end{proposition}

\begin{proof}

Let $\alpha : F' \circ\gamma\Rightarrow F\circ\gamma$ be the $2$-morphism of op-prederivators defined \emph{mutatis mutandis} as in \ref{paragr:prelimgonzalez} but at the level of op-prederivators. Proposition \ref{prop:gonz} gives us that for every small category $A$, the functor $F'_A$ is absolutely totally left derivable with $(F'_A,\alpha_A)$ its total left derived functor. This proves that $F'$ is strongly left derivable and $(F',\alpha)$ is the left derived morphism of op-prederivators of $F$.

Let $\alpha : F' \circ\gamma\Rightarrow F\circ\gamma$ be the $2$-morphism of op-prederivators defined \emph{mutatis mutandis} as in \ref{paragr:prelimgonzalez} but at the level of op-prederivators. Proposition \ref{prop:gonz} gives us that for every small category $A$, the functor $F'_A$ is absolutely totally left derivable with $(F'_A,\alpha_A)$ its total left derived functor. This means exactly that $F'$ is strongly left derivable and $(F',\alpha)$ is the left derived morphism of op-prederivators of $F$.