Composing dinatural transformations: Towards a calculus of substitution

Guy McCusker; Alessio Santamaria

doi:10.1016/j.jpaa.2021.106689

Composing dinatural transformations: Towards a calculus of substitution

Guy McCusker, Alessio Santamaria

Università degli Studi di Pisa

Research output: Contribution to journal › Article › peer-review

55 Downloads (Pure)

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.
This work represents the first, fundamental steps towards a substitution calculus for dinatural transform- ations as sought originally by Kelly, with the intention then to apply it to describe coherence problems abstractly. There 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 calculus of substitution for dinatural transformations.

Original language	English
Article number	106689
Number of pages	57
Journal	Journal of Pure and Applied Algebra
Volume	225
Issue number	10
Early online date	12 Jan 2021
DOIs	https://doi.org/10.1016/j.jpaa.2021.106689
Publication status	Published - 31 Oct 2021

Funding

Most of the material in this article derives from Santamaria's PhD thesis [33], written under the supervision of McCusker, and it is, in part, a detailed version of [24]. As such, Santamaria acknowledges the support of a research studentship from the University of Bath as well as EPSRC grant EP/R006865/1 and the funding support of the Ministero dell'Universit? e della Ricerca of Italy under Grant No. 201784YSZ5, PRIN2017. The authors would like to thank John Power for suggesting the notations to handle the manipulation of tuples, which we believe provided a great improvement to the exposition of our theory with respect to [24,33]. We would also like to thank Alessio Guglielmi for his valuable insights on the simplification of the proof of Theorem 2.25 with respect to [24,33]. Finally, we thank Zoran Petri? for his kind understanding of our lack of acknowledgement of his results in the past: we hope that with this paper we have finally given him the credit he deserves for his work. Most of the material in this article derives from Santamaria's PhD thesis [33] , written under the supervision of McCusker, and it is, in part, a detailed version of [24] . As such, Santamaria acknowledges the support of a research studentship from the University of Bath as well as EPSRC grant EP/R006865/1 and the funding support of the Ministero dell'Università e della Ricerca of Italy under Grant No. 201784YSZ5 , PRIN2017.

Access to Document

10.1016/j.jpaa.2021.106689Licence: Unspecified

Composing Dinatural Transformations -- accepted versionAccepted author manuscript, 467 KBLicence: CC BY-NC-ND

Cite this

@article{ea45abc86b434f688a60292b64a14a80,

title = "Composing dinatural transformations: Towards a calculus of substitution",

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{\' }{\textquoteright}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.This work represents the first, fundamental steps towards a substitution calculus for dinatural transform- ations as sought originally by Kelly, with the intention then to apply it to describe coherence problems abstractly. There 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 calculus of substitution for dinatural transformations.",

author = "Guy McCusker and Alessio Santamaria",

year = "2021",

month = oct,

day = "31",

doi = "10.1016/j.jpaa.2021.106689",

language = "English",

volume = "225",

journal = "Journal of Pure and Applied Algebra",

issn = "0022-4049",

publisher = "Elsevier B.V.",

number = "10",

}

TY - JOUR

T1 - Composing dinatural transformations: Towards a calculus of substitution

AU - McCusker, Guy

AU - Santamaria, Alessio

PY - 2021/10/31

Y1 - 2021/10/31

N2 - 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.This work represents the first, fundamental steps towards a substitution calculus for dinatural transform- ations as sought originally by Kelly, with the intention then to apply it to describe coherence problems abstractly. There 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 calculus of substitution for dinatural transformations.

AB - 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.This work represents the first, fundamental steps towards a substitution calculus for dinatural transform- ations as sought originally by Kelly, with the intention then to apply it to describe coherence problems abstractly. There 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 calculus of substitution for dinatural transformations.

U2 - 10.1016/j.jpaa.2021.106689

DO - 10.1016/j.jpaa.2021.106689

M3 - Article

SN - 0022-4049

VL - 225

JO - Journal of Pure and Applied Algebra

JF - Journal of Pure and Applied Algebra

IS - 10

M1 - 106689

ER -

Composing dinatural transformations: Towards a calculus of substitution

Abstract

Funding

Access to Document

Fingerprint

Cite this