nLab Kelly-Mac Lane graph

Idea

A diagrammatic calculus for closed categories, akin to proof nets in linear logic and more generally string diagrams for monoidal categories and related categorical structures of “linear” type.

Related concepts

• proof net

• Trimble rewiring

References

The concept was actually introduced in

• Samuel Eilenberg, Max Kelly, A generalization of the functorial calculus, J. Algebra 3 (1966), 366–375.

They have come to be known as “Kelly–Mac Lane graphs” principally on account of their application to coherence problems for closed categories in the treatment

• Max Kelly, Saunders MacLane, Coherence in closed categories, JPAA 1 (1971), 97–140 (web)

Reviews include

• Dominic Hughes, Simple free star-autonomous categories and full coherence, Journal of Pure and Applied Algebra, Volume 216, Issue 11, 2012, Pages 2386-2410, DOI, arxiv

• John Baez, Classical versus quantum lambda-calculus. From lambda-terms to string diagrams, Nov. 2006 (pdf)

• Eugenia Cheng, section 1 of A relationship between trees and Kelly–Mac Lane graphs, Math. Proc. Camb. Phil. Soc. (2006), 141, 33 (pdf), arxiv