Search

Effectful category

Last updated Nov 4, 2022

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

An effectful category $𝕍 → ℂ$ 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.