String Diagrams for Closed Symmetric Monoidal Categories

TL;DR

This paper presents a graphical language using extended string diagrams with bracket wires to explicitly represent internal homs in closed symmetric monoidal categories, enhancing clarity and expressiveness.

Contribution

It introduces a novel graphical calculus with explicit internal hom representation, proving its soundness and completeness for category theory, logic, and programming semantics.

Findings

The diagrammatic calculus is sound and complete.

The language effectively models internal homs in various contexts.

Examples demonstrate the expressiveness of the graphical language.

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.