promonoidal functor
Definition. Let $𝕍$ and $𝕎$ be promonoidal categories. A promonoidal functor $F﹕ 𝕍 → 𝕎$ is a functor between the two categories together with transformations $$μ﹕ 𝕍(A;B⊗C) → 𝕎(FA; FB ⊗ FC),$$ $$ε ﹕ 𝕍(A) → 𝕎(FA),$$ that behave nicely with associators and unitors, satisfying $λ ⨾ F_{map} = (μ × ε) ⨾ λ$, $ρ ⨾ F_{map} = (μ × ε) ⨾ ρ$, and $α ⨾ (μ × μ) ⨾ i = (μ × μ) ⨾ i ⨾ α$.
Proposition. A promonoidal functor extends to a multifunctor between the induced multicategories.
Tags: promonoidal category, Multicategory, Promonoidals as multicategories that factor.