Coherence for Frobenius pseudomonoids and the geometry of linear proofs
Logic in Computer Science
2023-06-22 v5
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.
Keywords
Cite
@article{arxiv.1601.05372,
title = {Coherence for Frobenius pseudomonoids and the geometry of linear proofs},
author = {Lawrence Dunn and Jamie Vicary},
journal= {arXiv preprint arXiv:1601.05372},
year = {2023}
}