Cartesian monoidal star-autonomous categories

Question

Disclaimer: This is a crosspost (see MathStackexchange). Apologies if cross-posting is frowned upon. However, it seems that on Stackexchange there are not many people familiar with star-autonomous categories.

1. Question
Any rigid cartesian monoidal category is trivial (see here). Star-autonomy is a generalization of rigidity. Are there (non-trivial) examples of star-autonomous cartesian monoidal categories? Neither Zhen Lin's nor Martin Brandenburg's arguments for the rigid case seem to be easily adaptable to star-autonomous categories.

2. Additional remarks
I use the following definition:
A monoidal category $(C, \otimes,I)$ carries a star-autonomous structure if there exists an equivalence of categories $S: C^{op} \xrightarrow{\sim} C$ with inverse $S’$ such that there there are bijections $\phi_{X,Y,Z}: \operatorname{Hom}_C(X \otimes Y,SZ) \xrightarrow{\sim} \operatorname{Hom}_C(X, S(Y \otimes Z))$ natural in $X,Y,Z.$

I tried the category Pos of posets and monotone maps. This category is cartesian closed. The product is the product order. The set of monotone maps between two posets becomes a poset by setting $$f \leq g \text{ for } f,g: X \rightarrow Y \text{ if } f(x)\leq g(x) \text{ for all } x\in X.$$ Does this category admit a star-autonomous structure? Is it even self-dual? If on objects one sets $S(X):=X^{op}$ with $X^{op}$ the dual poset, it is not clear to me how to define the mapping on morphisms in order to obtain a duality functor. In the category of sup-lattices such a definition is possible, but it uses the existence of joins.

Answer 1

[I'm going to assume $S' \cong S$, which holds in every symmetric monoidal $*$-autonomous category. (See e.g. Lemma 5.6 of this paper.) This applies here since cartesianness implies symmetry. Part of the proof also works with weaker assumptions, such as merely that the monoidal unit is terminal. Hat tip to Todd Trimble for indicating what this answer really should be.]

Proposition: The cartesian monoidal $*$-autonomous categories are exactly those that are equivalent to Boolean algebras (with $S$ being negation and $\land$ as monoidal structure).

Proof: Every Boolean algebra, considered as a posetal category, is a $*$-autonomous cartesian monoidal category, since both $x \land y \le \lnot z$ and $x \le \lnot(y \land z)$ are equivalent to $x \land y \land z = \bot$.

For the other direction, let us first show that such a category $C$ must be a preorder; this is also known as Joyal's Lemma.

Taking $Z := SI$ produces an isomorphism $$1 \cong \mathrm{Hom}_C(X \otimes Y,I) \cong \mathrm{Hom}_C(X \otimes Y,SSI) \cong \mathrm{Hom}_C(X,S(Y \otimes SI))$$ natural in $X$ and $Y$. This yields an isomorphism $S(Y \otimes S'I) \cong I$ natural in $Y$ by Yoneda, or equivalently $Y \otimes S'I \cong SI$. Hence the dualizing object $SI$ is "absorbing" for the monoidal structure, and since $S$ is a contravariant equivalence, we also know that it is initial.

But now $SI \otimes SI \cong SI$ together with initiality shows that the two product projections $SI \otimes SI \to SI$ are equal. Hence any two parallel morphisms $f,g : A \to SI$ are equal for any $A$. But then since $$ \mathrm{Hom}_C(X,Y) \cong \mathrm{Hom}_C(X\otimes SY,SI), $$ we can conclude that any two parallel morphisms are equal, and $C$ is equivalent to a poset.

In the poset case, the cartesian monoidal structure must be $\land$, so we have a meet-semilattice, and $S$ is an antitone involution with $$ x \land y \le Sz \quad \Longleftrightarrow \quad x \le S(y \land z). $$ But then it follows that $C$ is a Heyting algebra, $Sx = (x \to \bot)$ is negation, and every element is equal to its double negation. Therefore $C$ is a Boolean algebra. $\Box$

---

By the way, $\mathbf{Pos}$ is not contravariant equivalent to itself, for example because it has a strict initial object but not a strict terminal object.