Promonad
# Definition
A promonad $(β,β ,{}^{β})$ over a category $π$ is a profunctor $β \colon π \nrightarrow π$ together with transformations representing inclusion $({}^{β}){X,Y} \colon π(X,Y) \to β(X,Y)$ and multiplication $(β ){X,Y} \colon β(X,Y) \times β(Y,Z) \to β(X,Z)$, and such that
- the unit is natural, $(f β¨Ύ g)^β = f^β \mathbin{<} g = f \mathbin{>} g^β$;
- multiplication is natural, $f \mathbin{>} (p \mathbin{β } q) \mathbin{<} g = (f \mathbin{>} p) \mathbin{β } (q \mathbin{<} g)$;
- multiplication is dinatural, $p \mathbin{β } (f \mathbin{>} q) = (p \mathbin{<} f) \mathbin{β } q$;
- the unit is functorial, $(f β¨Ύ g)^β = f^β \mathbin{β } g^β$;
- the right action is premultiplication, $f^β \mathbin{β } p = f \mathbin{>} p$;
- the left action is posmultiplication, $p \mathbin{β } f^β = p \mathbin{<} f$;
- and multiplication is associative, $(p_{1} \mathbin{β } p_{2}) \mathbin{β } p_{3} = p_{1} \mathbin{β } (p_{2} \mathbin{β } p_{3})$.
Naturality of the multiplication, dinaturality of the multiplication and the functoriality of the unit, are redundant from the definition and can be proved from the rest of the axioms.
Equivalently, promonads are proarrow monoids in the double category of categories, where the dinatural multiplication represents a transformation from the composition of the profunctor $β$ with itself.
- Promonads and String Diagrams for Effectful Categories (Roman, 2022), Definition 3.7.
# Motivation for promonads
# Promonad homomorphism
# Promonad natural transformations
# See also
- Funny tensor as coproduct
- Funny tensor of promonads
- Pure tensor of promonads
- Promonads are id-on-objects functors
- Central product of promonads
- distributive law
- Kleisli category
- Prostrong promonad
- Strong promonad
#definition