Strictification tensor product of 2-categories

TL;DR

This paper introduces a new strictification construction for the tensor product of 2-categories, establishing an isomorphism that generalizes the free distributive law, with implications for the structure of lax and strict 2-functors.

Contribution

It provides two isomorphic constructions of a 2-category tensor product that generalizes the free distributive law for 2-categories, linking lax and strict functor categories.

Findings

Established an isomorphism between lax functor categories and strict 2-functor categories.

Constructed a 2-category tensor product satisfying a universal property.

Discussed dual constructions related to the tensor product.

Abstract

Given 2-categories $\mathcal{C}$ and $\mathcal{D}$, let $\textrm{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}\boxtimes\mathcal{D}$ satisfying $\textrm{Lax}(\mathcal{C},\textrm{Lax}(\mathcal{D},\mathcal{E})) \cong [\mathcal{C}\boxtimes \mathcal{D},\mathcal{E}]_\mathrm{lnt}$, hence generalising the case of the free distributive law $1\boxtimes 1$. We also discuss dual constructions.