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
