Mario RomΓ‘n

Search

Search IconIcon to open search

Prostrong promonad

Last updated Oct 7, 2024

prostrong-promonad

# 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.

Tags: promonad, multicategory - promonoidal category