It's well-known that being cocartesian is a property of a symmetric monoidal category: $(\mathcal C,I,\otimes,\sigma)$ is cocartesian if and only if the following conditions are satisfied:

  1. Every object $C \in \mathcal C$ has a commutative monoid structure $I \xrightarrow {u_C} C \overset{m_C}{\leftarrow} C \otimes C$;

  2. With respect to the commutative monoid structures of (1), every morphism is a homomorphism (in other words, $u: const_I \Rightarrow 1_{\mathcal C}: \mathcal C \rightrightarrows \mathcal C$ and $m: \otimes \circ \Delta \Rightarrow 1_{\mathcal C}: \mathcal C \rightrightarrows \mathcal C$ are natural transformations -- here $\Delta: \mathcal C \to \mathcal C \times \mathcal C$ is the diagonal functor);

  3. The commutative monoid structures of (1) satisfy $u_{C \otimes D} = u_C \otimes u_D$ and $m_{C \otimes D} = m_C \otimes m_D \circ (1_C \otimes \sigma_{D,C} \otimes 1_D)$ (in other words, $u$ and $m$ are monoidal natural transformations, where $\otimes$ has been made into a monoidal functor in the canonical way using the symmetry $\sigma$).

More precisely, if the data of (1,2,3) exists, then it is essentially unique, and exhibits $(\mathcal C, I, \otimes, \sigma)$ as cocartesian in the sense that $I$ is initial, and the maps $C \xrightarrow{1_C \otimes u_D} C \otimes D \overset{u_C \otimes 1_D}{\leftarrow} D$ are coproduct coprojections.

But what if $(\mathcal C, I,\otimes)$ is monoidal but not known to be symmetric monoidal?


  1. Is the forgetful 2-functor from cocartesian monoidal categories to monoidal categories fully faithful?

I believe the answer to (1) is yes, as I'll sketch below. If this is correct, then "being cocartesian" is a property of a monoidal category. We can then ask:

  1. What is this property, explicitly?

Partial progress:

One might guess that the following conditions suffice:

  1. Every object $C \in \mathcal C$ is a monoid object $(C,u_C,m_C)$.

  2. Every morphism is a morphism of monoid objects.

Under these conditions, I can show that

  • The unit $I$ is the initial object;

  • There is a functorial construction of a morphism $C \otimes D \xrightarrow{m_E\circ(f\otimes g)} E$ from morphisms $f: C \to E, g: D \to E$, which restricts appropriately along the "candidate coproduct inclusions" $C \xrightarrow{1_C \otimes u_D} C \otimes D \overset{u_C \otimes 1_D}{\leftarrow} D$;

  • (If $\mathcal C$ has split idempotents) binary coproducts $C \amalg D$ exist, and are functorially split subobjects of $C \otimes D$, splitting the idempotent $m_{C \otimes D} \circ (1_C\otimes u_D \otimes u_C \otimes 1_D)$.

So I can show that $\mathcal C$ is cocartesian iff (1,2) hold and in addition the following condition is satisfied:

  1. For all $C,D \in \mathcal C$, $m_{C \otimes D} \circ(1_C \otimes u_D \otimes u_C \otimes 1_D) = 1_{C\otimes D}$

But I'm not quite sure how to motivate (3), nor am I sure whether it is superfluous.

  • 1
    $\begingroup$ Isn't it the case that a suitable property is "$\otimes$ has a right adjoint", per your answer to Monoidal categories whose tensor has a left adjoint? Or do you explicitly want a property in the form "every object is a monoid [...]"? $\endgroup$
    – varkor
    Commented Jan 27, 2021 at 19:59
  • $\begingroup$ @varkor Wow, that's a great point... somehow I went through that whole thing thinking as though I were in a symmetric monoidal setting, not really registering that symmetry was neither stipulated nor used! So I suppose that gives an answer! But yes, I do think it would be desireable to have a formulation based around monoid structures. The point of departure here is the description in terms of commutative monoid structures in the symmetric case, and the question of whether it's really necessary to assume symmetry / commutativity ("surely it should come for free via Eckmann-Hilton!") $\endgroup$
    – Tim Campion
    Commented Jan 27, 2021 at 20:09
  • 1
    $\begingroup$ For 1., aren't you satisfied with the naive proof ? That just takes a monoidal functor and shows that it preserves finite coproducts, and that in fact the structural morphisms are induced by the universal property of coproducts. I tried to think about 2. as well and reached the same conclusion, with the exact same condition (3) - I'm not sure how to remove it $\endgroup$ Commented Jan 27, 2021 at 20:47

1 Answer 1


I don't have a counterexample to show that (3) is not superfluous, but I can provide some motivation for it. First, let us recall what is probably the most well known characterisation of cartesian monoidal categories in this spirit.

Proposition A. A symmetric monoidal category $(\mathcal M, \otimes, I)$ is cartesian if and only if there exist monoidal natural transformations $\varepsilon : ({-}) \Rightarrow I$ and $\delta : ({-}) \Rightarrow ({-}) \otimes ({-})$ equipping each object with the structure of a counital comagma.

This, for instance, is the version of the characterisation that is currently mentioned on the nLab page for semicartesian monoidal categories. In particular, note that cocommutativity and coassociativity are redundant.

If we permit ourselves to indulge in some centipede mathematics, we are led to wonder whether there are any other redundant assumptions in the proposition above. If we carry out the usual proof, we notice a few things.

  1. Associativity of $\otimes$ is never used. Thus, it suffices to take $\mathcal M$ to be a unital magmal category.
  2. In proving terminality of $I$, we only need that $\varepsilon$ satisfies the unit part of the monoidal natural transformation laws. Thus, it suffices to take $\varepsilon$ to be a unital natural transformation.
  3. In proving that $\otimes$ is the cartesian product, we only need that $\delta$ satisfies the multiplication part of the monoidal natural transformation laws. Thus, it suffices to take $\delta$ to be a magmal natural transformation.

Unfortunately, this seems as far as we can go. In particular, we need a symmetry $\sigma$ in order that $({-}) \otimes ({-})$ be a monoidal functor, which is necessary to ask that $\delta$ is a magmal natural transformation. However, if we examine the proof further, we see that magmality of $\delta$ is used in exactly one place: to establish commutativity of the following diagram (the magmality condition is precisely the commutativity of the left-hand triangle). Symmetry requirement However, the top composite in the diagram above admits a simpler description that does not involve the symmetry. Reduced symmetry requirement Thus, rather than require symmetry of $({-}) \otimes ({-})$ and magmality of $\delta$, it suffices to ask for the outer triangle above (which I shall call $(*)$) to commute. This eliminates the dependency on the symmetry, allowing for the original proposition to be simplified further.

Proposition A'. A unital magmal category $(\mathcal M, \otimes, I)$ is cartesian if and only if there exists a unital natural transformation $\varepsilon : ({-}) \Rightarrow I$ and a natural transformation $\delta : ({-}) \Rightarrow ({-}) \otimes ({-})$ equipping each object with the structure of a counital comagma, such that $(*)$ commutes for all $A, B \in \mathcal M$.

What does this tell us? In addition to requiring each object to be a counital comagma, and each morphism to be a homomorphism (this is naturality of $\varepsilon$ and $\delta$), we require two compatibility conditions: a compatibility condition of $\varepsilon$ with the unit $I$, and a compatibility condition of $\delta$ with the tensor $\otimes$. These are both natural conditions. However, when we drop symmetry, the compatibility condition for $\delta$ is no longer directly expressible. This necessitates its rewriting into the form $(*)$. Therefore, $(*)$ is essentially the compatibility condition between $\delta$ and $\otimes$. Of course, $(*)$ is precisely your condition (3). In fact, it is also possible to drop the unitality condition on $\varepsilon$, as this may be derived from naturality.

(Incidentally, Proposition A' appears to be more general than any other characterisation I can find in the literature. This extra generality does seem to actually be useful, too: for instance, it facilitates a direct proof that a monoidal category whose tensor product has a right adjoint is cocartesian, without using Day convolution or the Eckmann–Hilton argument.)

Update: I have since found almost exactly the same characterisation in Melliès's Categorical Semantics of Linear Logic (Proposition 16 and the following remark). However, he doesn't observe that unitality of $\varepsilon$ may be derived, and associativity of the tensor product is never used.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.