Mario RomΓ‘n


Search IconIcon to open search

Old - Definition of strong promonad

Last updated May 24, 2023

# Definition

A strong promonad over a monoidal category $𝕍$ is a promonad $(β„‚,β˜…,∘)$ endowed with a pair of strength operators $$(β—‘)οΉ•β„‚(Xβ‚€;Yβ‚€) Γ— 𝕍(X₁,Y₁) β†’ β„‚(Xβ‚€βŠ—X₁; Yβ‚€βŠ—Y₁),$$ $$(◐)﹕𝕍(Xβ‚€;Yβ‚€) Γ— β„‚(X₁,Y₁) β†’ β„‚(Xβ‚€βŠ—X₁; Yβ‚€βŠ—Y₁),$$ satisfying the following axioms up to coherence

  1. naturality, $(f \mathbin{β—‘} u) < (v,w) = (f < v) \mathbin{β—‘} (u β¨Ύ w)$, and $(u ◐ f) < (v,w) = (u β¨Ύ v) ◐ (f < w)$,
  2. unitality, $f \mathbin{◐} id_I = id_I \mathbin{◐} f = f$,
  3. associativity, $(f \mathbin{◐} u) \mathbin{◐} v = f \mathbin{◐} (u βŠ— v)$, and $u \mathbin{◐} (v \mathbin{◐} f) = (u βŠ— v) \mathbin{◐} f$,
  4. preserving units, $u^∘ \mathbin{β—‘} v = (u βŠ— v)^∘ = u \mathbin{◐} v^∘$,
  5. preserving multiplication, $(f \mathbin{β˜…} g) \mathbin{β—‘} (u β¨Ύ v) = (f \mathbin{β—‘} u) \mathbin{β˜…} (g \mathbin{β—‘} v)$, and $(u β¨Ύ v) \mathbin{◐} (f \mathbin{β˜…} g) = (u \mathbin{◐} f) \mathbin{β˜…} (v \mathbin{◐} g)$,
  6. and compatibility, $u \mathbin{◐} (f \mathbin{β—‘} v) = (u \mathbin{◐} f) \mathbin{β—‘} v$.