Coherence for Frobenius pseudomonoids and the geometry of linear proofs

Abstract

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.

References in corpus (6)

• Quasistrict symmetric monoidal 2-categories via wire diagrams
• Towards 3-Dimensional Rewriting Theory
• Simple multiplicative proof nets with units
• On dualizable objects in monoidal bicategories, framed surfaces and the Cobordism Hypothesis
• Frobenius algebras and planar open string topological field theories
• Extended 3-dimensional bordism as the theory of modular objects

Cited by in corpus (7)

• Quantum Natural Language Processing on Near-Term Quantum Computers
• DisCoPy: Monoidal Categories in Python
• Shaded Tangles for the Design and Verification of Quantum Programs (Extended Abstract)
• Shaded tangles for the design and verification of quantum circuits
• Coherence for braided and symmetric pseudomonoids
• Traced monoidal categories as algebraic structures in $\mathbf{Prof}$
• Traced Monoidal Categories as Algebraic Structures in Prof