Old - Monoidal profunctor
Definition. A monoidal profunctor between two monoidal categories $ℂ$ and $𝔻$ is a profunctor $P \colon ℂ \to 𝔻$ between the underlying categories, endowed with maps $$(\boxtimes) \colon P(X;Y) × P(X’,Y’) \to P(X ⊗ X’; Y ⊗ Y’),$$ $$n \colon 1 \to P(I;I),$$ that are natural and that moreover satisfy
- associativity, $α > (p \boxtimes (q \boxtimes r)) < α = ((p \boxtimes q) \boxtimes r)$,
- left unitality, $λ > (n \boxtimes p) < λ = p$,
- right unitality, $ρ > (p \boxtimes n) < ρ = p$.