In Natural deduction and coherence for weakly distributive categories Blute et al. claim to give a presentation of the free (non-symmetric) linearly distributive category $\operatorname{PNet_E}(C)$ on a labelled polygraph $C$ (modulo a set of equations $E$). In other words, they construct the free linearly distributive category on a category. They show in Theorem 3.4 that the category defined in section 3.3 (page 262) is indeed linearly distributive (they use the older terminology "weakly distributive"). I added in the details of their sketched proof and am convinced that it is correct.
In theorem 3.5 they then claim that $\operatorname{PNet_E}(C)$ is the free linearly distributive on a polygraph modulo equations $E$. I am unsure about their proof of Theorem 3.5. They write:
It suffices to show that all the rules of surgery are consequences of the axioms of weak distributivity. This can be done best by translating the rules back into morphisms and checking that indeed the diagrams in question must commute. To do this one must complete the surgical rules to morphisms and make explicit the tensor/cotensor arrangement of the free wires.
The reductions and expansions for the tensor and cotensor [par] are fairly obivously valid — indeed they are essentially the polycategorical bijections $$ \frac{\Gamma \vdash \Delta}{\otimes \ \Gamma \vdash \Delta} \qquad \frac{\Gamma \vdash \Delta}{\Gamma \vdash \oplus \ \Delta} $$
Firstly, …
I do not see how some of the reductions are forced by the linearly distributive structure. The expansions (7) and (8) follow from the fact that $\otimes$ and $\oplus$ are required to be bifunctors, i.e. that $id_A \ast id_B=id_{A\ast B}$ for $\ast \in \{\otimes, \oplus\}$. However, what about the reductions (1) and (2)?
These read as: 
Certainly, the following surgical rule holds by the functoriality of $\otimes$:
For all components $f,g,h,k$ with suitable input and output ports we have
However, I do not see how the general surgical rule (1) is supposed to follow from the last picture. Shouldn‘t one do a case distinction depending on how the "double-bident" occurs in a proof net? What do the polycategorical bijections have to do with it? When the authors speak of "making explicit the tensor/cotensor arrangement of the free wires", aren‘t there many possible ways of tensoring/cotensoring/attaching (co)tensor links to free wires, especially in the non-symmetric case?
The questions smell like they are related to the section entitled "representability" in this paper by Cockett and Pastro, though I am not exactly sure how. Maybe this is of help anyway.
Secondly, …
call a proof net transformational if it is under the surgical rules equivalent to a composition, a $\otimes$-tensoring or a $\oplus$-tensoring of the structure morphisms of the linearly distributive category $\operatorname{PNet_E}(C)$. (In other words, a proof net with one input and one output is transformational if it "represents" a morphism in the linearly distributive category $\operatorname{PNet_E}(C)$.)
The authors do not show (nor mention) that any planar proof net is a transformational proof net. Is this trivial? Or are Blute et al. actually only considering transformational proof nets as morphisms of the category $\operatorname{PNet_E}(C)$?
EDIT:
Maybe one might make some sense of Theorem 3.5 as follows. Define the two-tensor-polycategory (see Definition 1.3. in CS) $\operatorname{PolyNet_E}(C)$. Its objects are the same as the ones of $\operatorname{PNet_E}(C)$. Its morphisms are the following proof structures:
All proof nets (not only those with both one input and one output) in the positive fragment of linear logic with non-logical axioms being:
- the morphisms in $C$.
- the $(\otimes I)$- and the $(\oplus E)$-link. (These will play the role of the family of morphisms $m$ and $\omega$ in a polycategory. See Definition 1.3 in CS.)
One then imposes suitable surgical relations on the morphisms. To obtain a polycategory one has to impose both surgical reductions mentioned above, since a two-tensor-polycategory is required to satisfy $f=f^{\otimes_i}\circ m$ for $f: \Gamma_1,A,B,\Gamma_2 \rightarrow \Gamma_3$, where $m_{A,B}:A,B \rightarrow A \otimes B$ is part of the datum of a two-tensor polycategory (see Definition 1.3 in CS).
One guess would be that, modulo all the surgical rules, the polycategory $\operatorname{PolyNet_E}(C)$ is the free two-tensor-polycategory on $C$ (i.e. the object-component of the left adjoint to the forgetful functor $U:\mathbf{PolyCat_{\otimes\oplus}} \rightarrow \mathbf{Cat}$).
Theorem 2.1 in CS shows how to obtain a linearly distributive category from a two-tensor polycategory. The linearly distributive category one obtains from $\operatorname{PolyNet_E}(C)$ should be $\operatorname{PNet_E}(C)$. Why $\operatorname{PNet_E}(C)$ is the free linearly distributive category on $C$ is still not clear to me, however. Why should the underlying linearly distributive category of a free two-tensor-polycategory be free?
