Towards a Calculus of Substitution for Dinatural Transformations

Dinatural transformations are a generalisation of one of the very pillars of category theory: natural transformations. As such, they are ubiquitous in mathematics and computer science. They were proposed to give a semantics of parametric polymorphism, they correspond to proofs in intuitionistic and multiplicative linear logic, they characterise fixed point operators on many categories of domains, and have very recently been used to provide operational semantics of higher order languages as well as to model subtyping and bounded quantification in game semantics. Yet, they suffer from a troublesome shortcoming: they do not compose. A lot of effort has gone into finding subclasses of dinaturals that do compose, and many indeed were found for the specific applications above, but a general theory of compositionality is still missing.

In this talk I’ll present a sufficient and essentially necessary condition for compositionality of dinatural transformations: acyclicity of their composite “string diagrams”. I’ll also introduce a new operation of horizontal composition of dinaturals. These results provide the first steps for a full calculus of dinatural transformations that would fulfil a project started by Kelly in the 1970’s centred around the idea of substitution as a generalisation of composition.