Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: About closed symmetric monoidal categories

Jean-Baptiste Vienney (Dec 01 2023 at 16:25):

In Intuitionnisitic Multiplicative Linear Logic (IMLL) which is the logic of closed symmetric monoidal categories, there is this inference rule:
$\frac{A \vdash B \qquad C \vdash D}{A,B \multimap C \vdash D}$
I don't know how to translate it in category theory. If I have a morphism $f:A \rightarrow B$ and a morphism $g:C \rightarrow D$ in a closed symmetric monoidal categories with closure $- \otimes X \dashv X \multimap -$, how do I obtain a morphism $A \otimes (B \multimap C) \rightarrow D$?

I need a bit of training in closed symmetric monoidal categories ahah, I'm a newbie (I was trying to understand if we can translate something about (vector valued) distributions in the framework of closed monoidal differential categories but I'm not very comfortable with the closed part :face_with_hand_over_mouth: ).

Mike Shulman (Dec 01 2023 at 16:31):

$A\otimes (B\multimap C) \xrightarrow{f\otimes 1} B\otimes (B\multimap C) \xrightarrow{\mathrm{eval}} C \xrightarrow{g} D$.

Jean-Baptiste Vienney (Dec 01 2023 at 16:31):

Awesome, thanks!