Mario RomΓ‘n


Search IconIcon to open search

Effectful category

Last updated May 18, 2023

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.

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

# References