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)}$

and

$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!