For years we have been bothered by a small mistery on categorical models of Linear Logic (star-autonomous categories) and Geometry of Interaction (compact closed categories, typically arising from traced monoidal categories via Int-construction): is there a proper intermediate structure between star-autonomous categories and compact closed categories, that is, a traced star-autonomous category which is not compact closed? We settle this issue by showing that any traced star-autonomous category is actually compact closed.

We also discuss what would happen if we remove symmetry, thus the following question: is there a non-symmetric star-autonomous category with a (suitably generalized) trace which is not pivotal? Our recent attempt suggests that the answer is again no, but the situation is much subtler than the symmetric case.

The result on the symmetric case is a joint work with Tamas Hajgato.