# Mario RomΓ‘n

Search

Last updated May 3, 2024

## # Definition

Let $π$ be a promonoidal category. We write $π(β’,β’;β’)$ for the protensor and $π(\bullet)$ for the prounit. We write $(>_l,>_r,<)$ and $(<)$ for their respective profunctor actions.

A prostrong promonad is a promonad $(β,β ,β)$ over a promonoidal category $π$, with actions $(>,<)$, endowed with two prostrenghts $$(β_l)οΉ \left( β«^{X’ β π} β(X;X’) Γ π(X’,Y;Z) \right) β \left( β«^{Z’ β π} π(X,Y;Z’) Γ β(Z’;Z) \right),$$ $$(β_r)οΉ \left( β«^{X’ β π} β(Y;Y’) Γ π(X,Y’;Z) \right) β \left( β«^{Z’ β π} π(X,Y;Z’) Γ β(Z’;Z) \right).$$ These must satisfy the following axioms.

1. Naturality.
(v \mathbin{>} h) \mathbin{β}_l p = \left{\begin{aligned} & let\\ h \mathbin{β}_l p β (p’ \mid h’)\\ in\\ \\ & (v \mathbin{>}_l p’ \mid h’) \end{aligned}\right}; \quad h \mathbin{β_r} (v \mathbin{>_l} p) = \left{\begin{aligned} & let\\ h \mathbin{β}_r p β (p’ \mid h’)\\ in\\ \\ & (v \mathbin{>}_l p’ \mid h’) \end{aligned}\right}; h \mathbin{β_l} (v \mathbin{>_r} p) = \left{\begin{aligned} & let\\ h \mathbin{β}_l p β (p’ \mid h’)\\ in\\ \\ & (v \mathbin{>}_r p’ \mid h’) \end{aligned}\right}; \quad (v \mathbin{>} h) \mathbin{β_r} p = \left{\begin{aligned} & let\\ h \mathbin{β}_r p β (p’ \mid h’)\\ in\\ \\ & (v \mathbin{>}_r p’ \mid h’) \end{aligned}\right}; h \mathbin{β_l} (p \mathbin{<} w) = \left{\begin{aligned} & let\\ h \mathbin{β}_l p β (p’ \mid h’)\\ in\\ \\ & (p’ \mid h’ \mathbin{<} w) \end{aligned}\right}; \quad h \mathbin{β_r} (p \mathbin{<} w) = \left{\begin{aligned} & let\\ h \mathbin{β}_r p β (p’ \mid h’)\\ in\\ \\ & (p’ \mid h’ \mathbin{<} w) \end{aligned}\right};
2. Neutrality. $$v^β \mathbin{β}_l (p \mathbin{<} w) = (v \mathbin{>}_l p \mid w^β); \quad v^β \mathbin{β}_r (p \mathbin{<} w) = (v \mathbin{>}_r p \mid w^β).$$
3. Multiplicativity. (h \mathbin{β } k) \mathbin{β}_l p = \left{\begin{aligned} & let\\ k \mathbin{β}_l p β (p’ \mid k’)\\ in\\ \\ & let\\ h \mathbin{β}_l p’ β (p’’ \mid h’)\\ in\\ \\ & (p’’ \mid h’ \mathbin{β } k’)\\ \end{aligned}\right}; \quad (h \mathbin{β } k) \mathbin{β}_r p = \left{\begin{aligned} & let\\ k \mathbin{β}_r p β (p’ \mid k’)\\ in\\ \\ & let\\ h \mathbin{β}_r p’ β (p’’ \mid h’)\\ in\\ \\ & (p’’ \mid h’ \mathbin{β } k’)\\ \end{aligned}\right};
4. Unitality. h \mathbin{<} Ξ»(u\mid p) = \left{\begin{aligned} & let\\ h \mathbin{β}_r p β (p’ \mid h’)\\ in\\ \\ & Ξ»(u \mid p’) \mathbin{>} h' \end{aligned}\right};\quad h \mathbin{<} Ο(u\mid p) = \left{\begin{aligned} & let\\ h \mathbin{β}_l p β (p’ \mid h’)\\ in\\ \\ & Ο(u \mid p’) \mathbin{>} h' \end{aligned}\right};
5. Associativity. \left{\begin{aligned} & let\\ h \mathbin{β}_l w β (w’ \mid h’)\\ in\\ \\ & let\\ h’ \mathbin{β}_l v β (h’’ \mid v’)\\ in\\ \\ & let\\ Ξ±(w’ \mid v’) β (w’’ \mid v’’)\\ in\\ \\ & (w’’ \mid v’’ \mid h’’) \end{aligned}\right} = \left{\begin{aligned} & let\\ Ξ±(w \mid v) β (w’ \mid v’)\\ in\\ \\ & let\\ h \mathbin{β}_l v β (v’’ \mid h’)\\ in\\ \\ & (w’ \mid v’’ \mid h’) \end{aligned}\right}; \left{\begin{aligned} & let\\ Ξ±(w \mid v) β (w’ \mid v’)\\ in\\ \\ & let\\ h \mathbin{β}_r w’ β (w’’ \mid h’)\\ in\\ \\ & let\\ h’ \mathbin{β}_r v’ β (h’’ \mid v’’)\\ in\\ \\ & (w’’ \mid v’’ \mid h’’) \end{aligned}\right} = \left{\begin{aligned} & let\\ Ξ±(w \mid v) β (w’ \mid v’)\\ in\\ \\ & let\\ h \mathbin{β}_r v’ β (v’’ \mid h’)\\ in\\ \\ & (w’ \mid v’’ \mid h’) \end{aligned}\right};
6. Compatibility. \left{\begin{aligned} & let\\ h \mathbin{β}_r w β (w’ \mid h’)\\ in\\ \\ & let\\ h’ \mathbin{β}_l v β (v’ \mid h’’)\\ in\\ \\ & (w’ \mid v’ \mid h’’) \end{aligned}\right} = \left{\begin{aligned} & let\\ Ξ±(w \mid v) β (w’ \mid v’)\\ in\\ \\ & let\\ h \mathbin{β}_l w’ β (w’’ \mid h’)\\ in\\ \\ & let\\ h’ \mathbin{β}_r v’ β (v’’ \mid h’’)\\ in\\ \\ & (w’’ \mid v’’ \mid h’’) \end{aligned}\right}

## # Questions

Can we use prostrong promonads as an alternative definition of pre-promonoidal categories? This would be similar to using strong promonads as the definition of premonoidal category. James Hefford is studying pre-pro-monoidal categories.

• Conjecture. A pre-promonoidal category with a chosen centre (a Proeffectful category) is a prostrong promonad.