Pawel Sobocinski: "Algebraic theories with string diagrams"

30th of September, 2021. Part of the Topos Institute Colloquium.
-----
Abstract: In Lawvere theories the central role is played by categories with finite products. The free category with finite products on one object (FinSet^op) is the Lawvere theory of the empty algebraic theory, and the free category with finite products on a signature (of an algebraic theory) has a concrete description as a category of classical syntactic terms. But, using a theorem due to Thomas Fox, we can also capture these categories nicely using string diagrams.

The string diagrammatic approach gets you further than ordinary syntax. In a POPL 21 paper with Ivan di Liberti, Fosco Loregian and Chad Nester, we developed a Lawvere-style approach to algebraic theories with partially defined operations. It turns out that in this setting, instead of categories with finite products, the relevant concept is discrete cartesian restriction categories (dcrc). And string diagrams are the right syntax for this setting: they let us describe the free dcrc on an object and the free dcrc on a signature. I will sketch some of our results and talk about some of the ramifications, including a string diagrammatic description of categories with free finite limits.