Coherence of Proof-Net Categories

TL;DR

This paper introduces proof-net categories related to linear logic, proves a coherence theorem for them, and explores their connection to star-autonomous categories, enhancing understanding of categorical structures in logic.

Contribution

It defines proof-net categories, establishes a coherence theorem for them, and links these categories to star-autonomous categories, extending categorical logic theory.

Findings

Proves a coherence theorem for proof-net categories

Establishes a connection to star-autonomous categories

Extends coherence results to include the mix principle

Abstract

The notion of proof-net category defined in this paper is closely related to graphs implicit in proof nets for the multiplicative fragment without constant propositions of linear logic. Analogous graphs occur in Kelly's and Mac Lane's coherence theorem for symmetric monoidal closed categories. A coherence theorem with respect to these graphs is proved for proof-net categories. Such a coherence theorem is also proved in the presence of arrows corresponding to the mix principle of linear logic. The notion of proof-net category catches the unit free fragment of the notion of star-autonomous category, a special kind of symmetric monoidal closed category.