Category Theory Using String Diagrams

TL;DR

This paper advocates for using string diagrams in category theory to combine the clarity of diagrammatic proofs with the calculational advantages, providing a topological and type-preserving approach.

Contribution

It introduces a systematic graphical framework using string diagrams for categorical proofs, enhancing clarity and expressiveness over traditional methods.

Findings

Developed string diagram formulations for key categorical concepts

Provided graphical proofs of standard categorical results

Unified diagrammatic and calculational approaches in category theory

Abstract

In work of Fokkinga and Meertens a calculational approach to category theory is developed. The scheme has many merits, but sacrifices useful type information in the move to an equational style of reasoning. By contrast, traditional proofs by diagram pasting retain the vital type information, but poorly express the reasoning and development of categorical proofs. In order to combine the strengths of these two perspectives, we propose the use of string diagrams, common folklore in the category theory community, allowing us to retain the type information whilst pursuing a calculational form of proof. These graphical representations provide a topological perspective on categorical proofs, and silently handle functoriality and naturality conditions that require awkward bookkeeping in more traditional notation. Our approach is to proceed primarily by example, systematically applying graphical techniques to many aspects of category theory. We develop string diagrammatic formulations of many common notions, including adjunctions, monads, Kan extensions, limits and colimits. We describe representable functors graphically, and exploit these as a uniform source of graphical calculation rules for many category theoretic concepts. These graphical tools are then used to explicitly prove many standard results in our proposed diagrammatic style.