Mario RomΓ‘n

Prostrong promonad

4 min read

prostrong-promonad

Definition

Let be a promonoidal category. We write for the protensor and for the prounit. We write and for their respective profunctor actions.

A prostrong promonad is a promonad over a promonoidal category , with actions , endowed with two prostrenghts

∫^{X' ∈ 𝕍} β„‚(Y;Y') Γ— 𝕍(X,Y';Z) \right) β†’ \left( ∫^{Z' ∈ 𝕍} 𝕍(X,Y;Z') Γ— β„‚(Z';Z) \right).$$ These must satisfy the following axioms. 0. 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\};$$ 1. 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^∘).$$ 2. 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\};$$ 3. 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\};$$ 4. 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\};$$ 5. 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](James%20Hefford) is studying pre-pro-monoidal categories. - *Conjecture*. A pre-promonoidal category with a chosen centre (a [Proeffectful category](notes/pieces/Proeffectful%20categories.md)) is a prostrong promonad. Tags: [promonad](notes/pieces/promonad.md), [multicategory - promonoidal category](notes/pieces/multicategory%20-%20promonoidal%20category.md)

Graph View

Backlinks