Bifunctoriality vs. separate functoriality

src/content/1.8/Functoriality.tex

@@ -35,15 +35,10 @@ \section{Bifunctors}
 identity morphisms $(\id, \id)$. So a Cartesian product of categories
 is indeed a category.
 
-But an easier way to think about bifunctors is that they are functors in
-both arguments. So instead of translating functorial laws ---
+An easier way to think about bifunctors would be to consider them functors in
+each argument separately. So instead of translating functorial laws ---
 associativity and identity preservation --- from functors to bifunctors,
-it's enough to check them separately for each argument. If you have a
-mapping from a pair of categories to a third category, and you prove
-that it is functorial in each argument separately (i.e., keeping the
-other argument constant), then the mapping is automatically a bifunctor.
-By \newterm{functorial} I mean that it acts on morphisms like an honest
-functor.
+it would be enough to check them separately for each argument. However, in general, separate functoriality is not enough to prove joint functoriality. Categories in which joint functoriality fails are called \textit{premonoidal}.
 
 Let's define a bifunctor in Haskell. In this case all three categories
 are the same: the category of Haskell types. A bifunctor is a type
@@ -67,8 +62,7 @@ \section{Bifunctors}
 \code{(f a b -> f c d)}, operating on types
 generated by the bifunctor's type constructor. There is a default
 implementation of \code{bimap} in terms of \code{first} and
-\code{second}, which shows that it's enough to have functoriality in
-each argument separately to be able to define a bifunctor.  (This is not true in general in category theory, because the two maps may not commute: \code{first g . second h} might not be the same as \code{second h . first g}.)
+\code{second}. (As mentioned before, this doesn't always work, because the two maps may not commute, that is \code{first g . second h} may not be the same as \code{second h . first g}.)
 
 \begin{figure}[H]
 \centering