3-functoriality of the lax Gray tensor product

Question

In Formal category theory: adjointness for 2-categories, Gray defines a tensor product of 2-categories, now more commonly known as the lax Gray tensor product, which I will denote by $\otimes_l$. For 2-categories $\mathcal A, \mathcal B, \mathcal C$, there are natural isomorphisms between

1. 2-functors $\mathcal A \otimes_l \mathcal B \to \mathcal C$
2. 2-functors $\mathcal A \to [\mathcal B, \mathcal C]_{\mathrm{lax}}$ into the 2-category of 2-functors and lax natural transformations
3. 2-functors $\mathcal B \to [\mathcal A, \mathcal C]_{\mathrm{oplax}}$ into the 2-category of 2-functors and oplax natural transformations

Gray proves that this tensor product, together with the terminal 2-category and the above correspondences, define a nonsymmetric monoidal category that is closed on both sides (Theorem 1,4.14 ibid.).

2-categories, 2-functors, 2-natural transformations, and modifications form a 3-category $2\text{-}\mathbf{Cat}$, and so we might hope that the lax Gray tensor product moreover defines a closed nonsymmetric 3-dimensional monoidal structure on $2\text{-}\mathbf{Cat}$. Such a statement is not as intimidating as it might at first seem, since everything is strict: since the lax Gray tensor product does define a one-dimensional monoidal structure, to show this monoidal structure is indeed 3-dimensional, it suffices to show that the lax Gray tensor product is 3-functorial and that the associator and unitor for this monoidal structure are 3-natural.

However, most references on the Gray tensor product appear only to treat it 1-categorically. From a cursory search, I was not able to find a reference for even the 2-functoriality of the Gray tensor product.

Does there exist a reference for the 3-functoriality of the lax Gray tensor product, and for the 3-naturality of the associator and unitor for the corresponding monoidal structure, or may they be derived straightforwardly from the existing literature? Alternatively, is there an obstruction to 3-functoriality or 3-naturality?

I would be interested in knowing about partial references – e.g. for the 2-functoriality of the lax Gray tensor product, and 2-naturality of the associator and unitors – if no references for the 3-functoriality may be found. I would also be interested in the same questions for the pseudo Gray tensor product, though I am primarily interested in the lax notion.

Answer 1

The lax Gray tensor product is not a two-variable 2-functor.

If it were, we'd have a functor $Fun(A,B) \times Fun(C,D) \to Fun(A \otimes_l C, B \otimes_l D)$ extending the set map $Ob Fun(A, B) \times Ob Fun(C, D) \to Ob Fun(A \otimes_l C, B \otimes_l D)$. Consider the case when $A = C = [0]$ is a point and $B = D = [1]$ is an arrow. Then we'd have a functor $[1] \times [1] \to [1] \otimes_l [1]$ extending the set map which is the identity on objects. That is, we'd have a commuting square living in the walking lax commutative square in an identity-on-objects way. There is no such functor.

There is a map in the other direction, reflecting the fact that the identity functor is a lax monoidal functor from the lax Gray tensor to the cartesian product. But the identity is not a lax monoidal functor from the cartesian product to the lax Gray tensor.

Morally, $n$-functors "don't shift category number". The lax Gray tensor product is too busy shifting category number (e.g. $m$-category $\otimes_l$ $n$-category = $(m+n)$-category) to be $n$-functorial.