Dan wrote:

> I'm not sure if this relevant for the current discussion, but I wanted to point out that if a map is functorial in each argument it's not a sufficient condition to conclude that it's a functor. We need an additional coherence condition, known as the "interchange law"; for example, see the bifunctor lemma stated in [chapter 7](https://www.andrew.cmu.edu/course/80-413-713/notes/chap07.pdf) from Awodey's book.

There are a couple of different ways to get your hands on a functor \\(F: \mathcal{A} \times \mathcal{B} \times \mathcal{C} \\) . Awodey is assuming we have categories \\(\mathcal{A} , \mathcal{B}, \mathcal{C} \\) and two maps:

A) a map sending each pair of objects \\((a,b) \in \mathbf{Ob}(\mathcal{A}) \times \mathbf{Ob}(\mathcal{B})\\) to an object of \\(\mathcal{C}\\);

B) a map I'll call \\(F\\) sending each pair of morphisms \\((f,g) \in \mathbf{Mor}(\mathcal{A}) \times \mathbf{Mor}(\mathcal{B})\\) to a morphism of \\(\mathcal{C}\\).

He gives a necessary and sufficient condition for this data to come from a (unique) functor from \\(\mathcal{A} \times \mathcal{B}\\) to \\( \mathcal{C} \\). Namely, we need

1. \\(F\\) preserves composition in each argument separately and

2. The **interchange law** \\( F(f,1) \circ F(1,g) = F(1,g) \circ F(f,1) \\) holds, where I'm writing \\(1\\) for a bunch of different identity morphisms (the only ones that make the equation parse.)

But there's another equivalent way to state conditions 1 and 2, which is sometimes just as easy to check. Namely, we can simply require that

\[ F(1_x,1_y) = 1_{(x,y)} \]


\[ F(f,g) \circ F(f',g') = F(f \circ f', g \circ g') .\]

This just says straight out that our would-be functor is a functor!