1.Context
On page 28 of Weakly distributive categories Cockett and Seely are trying to prove the following statement:
The notions of symmetric weakly distributive categories with negation and star-autonomous categories coincide.
When dealing with the direction that any star-autonomous category carries a linear distributive structure, they write:
It is a straightforward verification to check that star-autonomous categories are weakly distributive, though the diagrams can be pretty horrid. We shall just indicate how the weak distribution $\delta_L^{L}$ is obtained, leaving the rest to the faith of the reader.
Since I do not have much faith, I tried to verify that statement myself.
2. Definition
I am working with the following definition of star-autonomous category.
Let $(C, \otimes, I, a, l,r)$ be a symmetric monoidal category. A star-autonomous structure on the monoidal category $C$ consists of an adjoint equivalence $D \dashv D’: C^{op} \xrightarrow{\sim} C$ together with bijections $\phi_{X,Y,Z}: Hom_C(X \otimes Y,DZ) \xrightarrow{\sim} Hom_C(X, D(Y \otimes Z))$ natural in $X,Y,Z$.
3. Progress
After having (supposedly) derived left distributor and right distributor (by writing them as a composition of morphisms involving $\phi$ and $\phi^{-1}$ as well as the application of functors $D$ and $D’$), I am now unsuccesfully trying to verify that the necessary diagrams given by Cockett and Seely commute.
4. Question
- Is the proof of the claim that any star-autonomous category carries a linear distributive structure given in greater detail somewhere in the literature?