Prolinearly distributive category
Definition. A prolinear category is a category $ℂ$ endowed with two promonoidal structures, $(ℂ,⊗,⊤)$ and $(ℂ,⅋,⊥)$, and two frobenius natural isomorphisms relating them $$\begin{aligned} & \left(∫^{W} ℂ(A ; C ⅋ W) × ℂ(W ⊗ B ; D) \right) \overset{ϕ₁}→ ℂ(A ⊗ B; C ⅋ D), \\ & \left(∫^{W} ℂ(A ⊗ W ; C) × ℂ(B ; W ⅋ D) \right) \overset{ϕ₁}→ ℂ(A ⊗ B; C ⅋ D), \end{aligned}$$ such that every formal equation out of these frobenius isomorphisms and the coherence isomorphisms of the promonoidal categories holds.