Old - Definition of strong promonad
# 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
- naturality, $(f \mathbin{β} u) < (v,w) = (f < v) \mathbin{β} (u β¨Ύ w)$, and $(u β f) < (v,w) = (u β¨Ύ v) β (f < w)$,
- unitality, $f \mathbin{β} id_I = id_I \mathbin{β} f = f$,
- associativity, $(f \mathbin{β} u) \mathbin{β} v = f \mathbin{β} (u β v)$, and $u \mathbin{β} (v \mathbin{β} f) = (u β v) \mathbin{β} f$,
- preserving units, $u^β \mathbin{β} v = (u β v)^β = u \mathbin{β} v^β$,
- 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)$,
- and compatibility, $u \mathbin{β} (f \mathbin{β} v) = (u \mathbin{β} f) \mathbin{β} v$.