  We prove coherence theorems for Frobenius pseudomonoids and snakeorators in
monoidal bicategories. As a consequence we obtain a 3d notation for proofs in
nonsymmetric multiplicative linear logic, with a geometrical notion of
equivalence, and without the need for a global correctness criterion or
thinning links. We argue that traditional proof nets are the 2d projections of
these 3d diagrams.
