Bifunctor - Ryan Brewer

Bifunctor

A bifunctor is a functor from a product category to another category. This is useful because it gives a notion of two-argument functor (hence the name).

The definition and laws can be derived from the definition of a functor and a product category, but the main points are that the condition of "functoriality" becomes a condition of "bifunctoriality:" Given two product-category morphisms \(h, k\) and \(f, g\), bifunctoriality of a bifunctor \(F\) states that \(F((h, k)\circ(f, g))=F(h\circ f, k\circ g)\). This really is just functoriality, specialized to the case of a product category in the domain of the functor.

The most important bifunctors to be aware of are those formed by monoidal products. The cartesian product \(A\times B\) gives a bifunctor \(-\times-\) from \(C\times C\) to \(C\) for any cartesian category \(C\). Other monoidal products \(\otimes\) in monoidal categories give bifunctors \(-\otimes-\) from \(C\times C\) to \(C\) for any monoidal category \(C\). This includes the coproduct \(-+-\).

No, the very notion of a product category \(C\times D\) does not give a bifunctor from \(\texttt{Cat}\times\texttt{Cat}\) to \(\texttt{Cat}\), at least not in the way we've defined it so far. This is because we're thinking of functors as arrows in \(\texttt{Cat}\), which doesn't contain itself, and because we're thinking of product categories as the cartesian product in \(\texttt{Cat}\), which doesn't contain itself. So we'd need to lift all of these definitions up a level if we want to talk about \(\texttt{Cat}\times\texttt{Cat}\) as a category, and \(\texttt{Cat}\times\texttt{Cat}\to\texttt{Cat}\) as a functor. However, this lifting is so routine and unproblematic that we generally ignore it, and happily talk about bifunctors from \(\texttt{Cat}\times\texttt{Cat}\) to \(\texttt{Cat}\).

It may also help to notice that the cartesian products are there already, whether we like them or not, and bifunctors just introduce mappings between them. So there's nothing wrong with a cartesian product bifunctor, even if cartesian products are used to define bifunctors. The definition of cartesian product doesn't depend on bifunctors at all, so there's no circularity.

There are interesting cases where regular category-theoretic morphism composition forms a bifunctor. For example, if you take the homset of an object \(A\) to itself in some category \(C\), then you know any two elements in that set can be composed. Furthermore, the composition is associative and has an identity (\(id_A\)). So this set forms a monoid. If we take these morphisms as the objects of a category, then it's a monoidal category, where composition is the monoidal product. Since it's a monoidal product, we know there's a bifunctor \(-\circ-\). This is really a thing for 2-categories, since that's where the morphisms between objects form categories. (Though I will point out that technically, all 1-categories are at least 2-categories in some way or another, since any set (including homsets) can be used as the objects of a category, perhaps just a discrete one, where the morphisms are set-theoretic equality. It's just that these situations are boring enough that we ignore them.)