Strictification tensor product of 2-categories

Abstract

Given 2-categories $\mathcal{C}$ and $\mathcal{D}$, let $\text{Lax}(\mathcal{C},\mathcal{D})$ denote the 2-category of lax functors, lax natural transformations and modifications, and $[\mathcal{C},\mathcal{D}{]}_{\mathrm{lnt}}$ its full sub-2-category of (strict) 2-functors. We give two isomorphic constructions of a 2-category $\mathcal{C}⊠\mathcal{D}$ satisfying $\text{Lax}(\mathcal{C},\text{Lax}(\mathcal{D},\mathcal{E}))\cong [\mathcal{C}⊠\mathcal{D},\mathcal{E}{]}_{\mathrm{lnt}}$, hence generalising the case of the free distributive law $1⊠1$. We also discuss dual constructions.