premonoidal category

Premonoidal categories

Premonoidal categories


A premonoidal category is a generalisation of a monoidal category, applied by John Power and his collaborators to denotational semantics in computer science. There, the Kleisli category of a strong monad provides a model of call-by-value? programming languages. In general, if the original category is monoidal, the Kleisli category will only be premonoidal.

Recall that a bifunctor from CC and DD to EE (for C,D,EC,D,E categories) is simply a functor to EE from the product category C×DC \times D. We can think of this as an operation which is ‘jointly functorial’. But just as a function to XX from YY and ZZ (for X,Y,ZX,Y,Z topological spaces) may be continuous in each variable yet not jointly continuous? (continuous from the Tychonoff product Y×ZY \times Z), so an operation between categories can be functorial in each variable separately yet not jointly functorial.

Recall that a monoidal category is a category CC equipped with a bifunctor C×CCC \times C \to C (equipped with extra structure such as the associator). Similarly, a premonoidal category is a category equipped with an operation C×CCC \times C \to C, which is (at least) a function on objects as shown, but one which is functorial only in each variable separately.


A binoidal category is a category CC equipped with

  • for each pair x,yx,y of objects of CC, an object xyx \otimes y;
  • for each object xx a functor xx \rtimes - whose action on objects sends yy to xyx \otimes y
  • for each object xx a functor x- \ltimes x whose action on objects sends yy to yxy \otimes x

A morphism f:xyf\colon x \to y in a binoidal category is central if, for every morphism f:xyf'\colon x' \to y', the diagrams

xx xf xy fx fy yx yf yy \array { x \otimes x' & \overset{x \rtimes f'}\to & x \otimes y' \\ \mathllap{f \ltimes x'}\downarrow & & \downarrow\mathrlap{f \ltimes y'} \\ y \otimes x' & \underset{y \rtimes f'}\to & y \otimes y' \\ }


xx xf xy fx fy yx yf yy \array { x' \otimes x & \overset{x' \rtimes f}\to & x' \otimes y \\ \mathllap{f' \ltimes x}\downarrow & & \downarrow\mathrlap{f' \ltimes y} \\ y' \otimes x & \underset{y' \rtimes f}\to & y' \otimes y \\ }

commute. In this case, we denote the common composites ff:xxyyf \otimes f'\colon x \otimes x' \to y \otimes y' and ff:xxyyf' \otimes f\colon x' \otimes x \to y' \otimes y.

A premonoidal category is a binoidal category equipped with:

  • an object II;
  • for each triple x,y,zx,y,z of objects, a central isomorphism α x,y,z:(xy)zx(yz)\alpha_{x,y,z}\colon (x \otimes y) \otimes z \to x \otimes (y \otimes z); and
  • for each object xx, central isomorphisms λ x:xIx\lambda_x\colon x \otimes I \to x and ρ x:Ixx\rho_x\colon I \otimes x \to x;

such that the following conditions hold.

  • all possible naturality squares for α\alpha, λ\lambda, and ρ\rho (which make sense since we have central morphisms) commute. Note that when written out explicitly in terms of the functors xx\rtimes - and x-\ltimes x, we need three different naturality squares for α\alpha. (But it is possible to rephrase α\alpha as a single natural transformation using the slick version below.)
  • the pentagon law holds for α\alpha, as in a monoidal category.
  • the triangle law holds for α\alpha, λ\lambda, and ρ\rho, as in a monoidal category.

A strict premonoidal category is a monoidal category in which (xy)z=x(yz)(x \otimes y) \otimes z = x \otimes (y \otimes z), xI=xx \otimes I = x, and Ix=xI \otimes x = x, and in which α x,y,z\alpha_{x,y,z}, λ x\lambda_x, and ρ x\rho_x are all identity morphisms. (We need the underlying category CC to be a strict category for this to make sense.)

Similarly, a symmetric premonoidal category is a premonoidal category equipped with a central natural isomorphism xyyxx\otimes y \cong y\otimes x (as for α\alpha, there are two naturality squares unless we use the slick approach), satisfying the usual axioms of a symmetry.

Slick version

As a strict monoidal category is a monoid in the cartesian monoidal category Cat, so a strict premonoidal category is a monoid in the symmetric monoidal category (Cat,)(Cat,\Box), where \Box is the funny tensor product.

From this point of view, a binoidal category is just a category CC with a functor CCCC \Box C \to C

It may be possible to make (Cat,)(Cat,\Box) a symmetric monoidal 2-category, in which a pseudomonoid object is precisely a non-strict premonoidal category, but if so, nobody seems to have written this up yet. It is possible, however, to describe part of the structure of a non-strict premonoidal category in terms of (Cat,)(Cat,\Box). For instance, a binoidal structure on CC is precisely a functor CCCC\Box C \to C, and the naturality of the associator α\alpha can be expressed by saying that it is a natural transformation (with central components) between functors CCCCC\Box C\Box C \to C.


  • Every monoidal category is a premonoidal category.

  • If TT is a strong monad on a monoidal category CC, then the Kleisli category C TC_T of TT inherits a premonoidal structure, such that the functor CC TC\to C_T is a strict premonoidal functor. This premonoidal structure is only a monoidal structure if TT is a commutative monad.


The central morphisms of a premonoidal category CC form a subcategory Z(C)Z(C), called the centre of CC, which is a monoidal category. This defines a right adjoint functor to the inclusion MonCatPreMonCatMonCat \hookrightarrow PreMonCat using the definition of functor of premonoidal categories in Power-Robinson 97.

In the same way that a (strict) monoidal category can be identified with a (strict) 2-category with one object, a strict premonoidal category can be identified with a sesquicategory with one object. In fact, a sesquicategory is precisely a category enriched over the monoidal category (Cat,)(Cat,\otimes) described above.


  • John Power and Edmund Robinson, Premonoidal categories and notions of computation, Math. Structures Comput. Sci., 7(5):453–468, 1997. Logic, domains, and programming languages (Darmstadt, 1995).


  • Alan Jeffrey, Premonoidal categories and a graphical view of programs, pdf file

Last revised on March 2, 2018 at 09:43:42. See the history of this page for a list of all contributions to it.