effectful category

An effectful category is an identity-on-objects functor $\mathbb{V}\to C$ from a monoidal category $\mathbb{V}$ (representing the pure morphisms, or “values”) to a premonoidal category $C$ (representing the effectful morphisms, or “computations”), that strictly preserves all of the premonoidal structure and whose image is central.

An effectful category $\mathbb{V}\to C$ is strict when both its monoidal and premonoidal categories are. A Freyd category (Levy, 2004) is an effectful category where the pure morphisms form a cartesian monoidal category.

Effectful categories assemble into the 2-category of effectful categories.

• device category

References.

• Promonads and String Diagrams for Effectful Categories (Roman, 2022)
• Call-By-Push-Value, A Functional-Imperative Synthesis (Levy, 2004)

Tags: premonoidal category.