# 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.