Bifunctor Theorem and strictification tensor product for double categories with lax double functors

We introduce a candidate for the inner hom for $Db{l}_{lx}^{st}$, the category of strict double categories and lax double functors, and characterize a lax double functor into it obtaining a lax double quasi-functor. The latter consists of a pair of lax double functors with four 2-cells resembling distributive laws. We extend this characterization to a 2-category isomorphism $q\text{x}{\text{Lax}}_{hop}(\text{Aa}\times \text{Bb},\text{Cc})\text{iso}{\text{Lax}}_{hop}(\text{Aa},\mathrm{⟦}\text{Bb},\text{Cc}\mathrm{⟧})$. We show that instead of a Gray monoidal product in $Db{l}_{lx}^{st}$ we obtain a product that in a sense strictifies lax double quasi-functors. We prove a bifunctor theorem by which certain type of lax double quasi-functors give rise to lax double functors on the Cartesian product, extend it to a 2-functor $q\text{x}{\text{Lax}}_{hop}^{ns}(\text{Aa}\times \text{Bb},\text{Cc})\to {\text{Lax}}_{hop}(\text{Aa}\times \text{Bb},\text{Cc})$ and show how it restricts to a biequivalence. The (un)currying 2-functors are studied. We prove that a lax double functor from the trivial double category is a monad in the codomain double category, and show that our above 2-functor in the form $q\text{x}{\text{Lax}}_{hop}(\ast \times \ast ,\text{Dd})\to {\text{Lax}}_{hop}(\ast ,\text{Dd})$ recovers the specification $\text{Comp}(\text{HH}(\text{Dd})):\text{Mnd}\text{Mnd}(\text{HH}(\text{Dd}))\to \text{Mnd}(\text{HH}(\text{Dd}))$ of the natural transformation $\text{Comp}$ introduced by Street, where $\text{HH}(\text{Dd})$ is the horizontal 2-category of $\text{Dd}$.