Composing Dinatural Transformations: Towards a Calculus of Substitution

TL;DR

This paper advances the theory of dinatural transformations by providing a semantic proof of Petric's theorem, defining a generalized functor category, and establishing a compositional calculus with associative horizontal composition.

Contribution

It introduces a semantic proof of Petric's theorem, constructs a generalized functor category, and defines a compositional calculus for dinatural transformations with associative horizontal composition.

Findings

Semantic proof of Petric's theorem

Definition of a generalized functor category

Establishment of associative horizontal composition

Abstract

Dinatural transformations, which generalise the ubiquitous natural transformations to the case where the domain and codomain functors are of mixed variance, fail to compose in general; this has been known since they were discovered by Dubuc and Street in 1970. Many ad hoc solutions to this remarkable shortcoming have been found, but a general theory of compositionality was missing until Petric, in 2003, introduced the concept of g-dinatural transformations, that is, dinatural transformations together with an appropriate graph: he showed how acyclicity of the composite graph of two arbitrary dinatural transformations is a sufficient and essentially necessary condition for the composite transformation to be in turn dinatural. Here we propose an alternative, semantic rather than syntactic, proof of Petric's theorem, which the authors independently rediscovered with no knowledge of its prior existence; we then use it to define a generalised functor category, whose objects are functors of mixed variance in many variables, and whose morphisms are transformations that happen to be dinatural only in some of their variables. We also define a notion of horizontal composition for dinatural transformations, extending the well known version for natural transformations, and prove it is associative and unitary. Horizontal composition embodies substitution of functors into transformations and vice-versa, and is intuitively reflected from the string-diagram point of view by substitution of graphs into graphs.