# Mario Román

Search

Last updated Nov 4, 2022

## # Definition

A strong promonad over a monoidal category $𝕍$ is a promonad $(ℂ,★,∘)$ endowed with a pair of strength operators $$(◑)﹕ℂ(X₀;Y₀) × 𝕍(X₁,Y₁) → ℂ(X₀⊗X₁; Y₀⊗Y₁),$$ $$(◐)﹕𝕍(X₀;Y₀) × ℂ(X₁,Y₁) → ℂ(X₀⊗X₁; Y₀⊗Y₁),$$ satisfying the following axioms up to coherence

1. naturality, $(f \mathbin{◑} u) < (v,w) = (f < v) \mathbin{◑} (u ⨾ w)$, and $(u ◐ f) < (v,w) = (u ⨾ v) ◐ (f < w)$,
2. unitality, $f \mathbin{◐} id_I = id_I \mathbin{◐} f = f$,
3. associativity, $(f \mathbin{◐} u) \mathbin{◐} v = f \mathbin{◐} (u ⊗ v)$, and $u \mathbin{◐} (v \mathbin{◐} f) = (u ⊗ v) \mathbin{◐} f$,
4. preserving units, $u^∘ \mathbin{◑} v = (u ⊗ v)^∘ = u \mathbin{◐} v^∘$,
5. preserving multiplication, $(f \mathbin{★} g) \mathbin{◑} (u ⨾ v) = (f \mathbin{◑} u) \mathbin{★} (g \mathbin{◑} v)$, and $(u ⨾ v) \mathbin{◐} (f \mathbin{★} g) = (u \mathbin{◐} f) \mathbin{★} (v \mathbin{◐} g)$,
6. and compatibility, $u \mathbin{◐} (f \mathbin{◑} v) = (u \mathbin{◐} f) \mathbin{◑} v$.

## # Correspondence with effectful categories

Strong promonads may be read as Arrows (Hughes), or effectful categories that particularize into Freyd categories when the base is cartesian.

There is a one-to-one correspondence between strong promonads and locally small effectful categories (Heunen, Jacobs; Theorem 5.4).