String Diagrams for Closed Symmetric Monoidal Categories

TL;DR

The paper develops a complete, diagrammatic language for closed symmetric monoidal categories by extending string diagrams with bracket wires to reveal the internal hom. It defines a rigorous syntax, a comprehensive set of equations, and proves that the resulting category is the free closed symmetric monoidal category on a given closed monoidal signature, via normalisation and decomposition techniques. Through motivating examples like currying, lambda-calculus encoding, and self-enrichment, it demonstrates the practical expressiveness and geometric intuition of the approach. The work situates itself among related diagrammatic formalisms, addresses coherence phenomena, and proposes avenues for future work including hypergraph interpretations and biclosed variants with potential for tool-assisted reasoning.

Abstract

We introduce a graphical language for closed symmetric monoidal categories based on an extension of string diagrams with special bracket wires representing internal homs. These bracket wires make the structure of the internal hom functor explicit, allowing standard morphism wires to interact with them through a well-defined set of graphical rules. We establish the soundness and completeness of the diagrammatic calculus, and illustrate its expressiveness through examples drawn from category theory, logic and programming language semantics.

Figures (26)

• Figure 1: Local manipulations.
• Figure 3: The proof of \ref{['lemma:bigCupSplit']}
• Figure 4: Generators for string diagrams with brackets.
• Figure 5: Full syntax of string diagrams with brackets.
• Figure 5: The proof of symmetry for the rightward cup.

Theorems & Definitions (36)

• Definition 2.1
• Definition 2.2
• Definition 2.3
• Definition 2.4
• Definition 2.5
• Remark
• Theorem 2.6
• proof
• Lemma 2.7
• proof