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

- 2-functors $\mathcal A \otimes_l \mathcal B \to \mathcal C$
- 2-functors $\mathcal A \to [\mathcal B, \mathcal C]_{\mathrm{lax}}$ into the 2-category of 2-functors and lax natural transformations
- 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 cursor 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.