Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 2 of 2
Blute-Cockett-Seely-Trimble describes a string diagram / circuit diagram / proof net calculus for linearly distributive categories, which is significantly complicated by the presence of units; as discussed in section 2.3 of the paper, some of the unit and counit links have to be “attached” to other strings to prevent diagrams that should be distinct from getting identified. However, the example given there depends on the fact that the units $\top$ and $\bot$ for the tensor and cotensor products are different; as noted therein, if $\top$ in the example were replaced by $\bot$ then the two problematic diagrams would represent the same morphism. This makes me wonder, if we have a linearly distributive category that happens to satisfy $\top=\bot$, then does the whole string diagram calculus work without these extra attachments?
This would be especially convenient because any closed monoidal category $(C,\otimes,\top)$ can be embedded by a closed functor into a linearly distributive (indeed $\ast$-autonomous) category in which $\top=\bot$, namely $Chu(C,\top)$. So we could soundly use linearly distributive string diagrams to reason about closed monoidal categories, without the need for the clunky “boxes” that are sometimes used to deal with internal-homs.
Oops, I’m not sure why I thought the embedding of $C$ in $Chu(C,d)$ is closed; it’s strong monoidal but doesn’t preserve internal-homs. So that’s not as interesting as I thought it was.
1 to 2 of 2