Abstract
Dinatural transformations, which have been used to interpret the second-order λ-calculus as well as derivations in intuitionistic logic and multiplicative linear logic, 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. In this thesis we show how acyclicity of certain graphs associated to these transformations is a sufficient and essentially necessary condition that ensures that the composite of two arbitrary dinatural transformations is in turn dinatural. This leads (not straightforwardly) to the definition of 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.
This work represents the first, fundamental steps towards a Godement-like calculus of dinatural transformations as sought originally by Kelly, with the intention then to apply it to describe coherence problems abstractly. ‘ere are still fundamental difficulties that are yet to be overcome in order to achieve such a calculus, and these will be the subject of future work; however, our contribution places us well in track on the path traced by Kelly towards a Godement calculus for dinatural transformations.
| Date of Award | 4 Sept 2019 |
|---|---|
| Original language | English |
| Awarding Institution |
|
| Supervisor | Guy McCusker (Supervisor) & Alessio Guglielmi (Supervisor) |