A strong dinatural transformation is a notion of natural transformation between two functors that is stronger than a dinatural transformation.
Unlike dinatural transformations, strong dinatural transformations can always be composed. They have close connections to parametricity in computer science.
Let be functors. A strong dinatural transformation consists of, for each , a component , such that for any morphism in and any span in , if the square on the left commutes, then the outer hexagon also commutes:
If the pullback exists in , it suffices to assert this when the square on the left is the defining one of that pullback. On the other hand, if has a separator (such as ), it suffices to assert this when is the separator.
By comparison, a dinatural transformation asserts this condition only when with the span consisting of and .
Originally introduced (as strong dinatural transformations) in Definition 2.7 of
Further developments:
Philip S Mulry. Strong monads, algebras and fixed points. Applications of Categories in Computer Science 177 (1992), 202–216
Robert Paré and Leopoldo Román. Dinatural numbers. Journal of Pure and Applied Algebra 128, 1 (1998), 33–92
A. Eppendahl, Parametricity and Mulry’s Strong Dinaturality, https://qmro.qmul.ac.uk/xmlui/bitstream/handle/123456789/4501/768_Eppendahl_12-1999.pdf?sequence=1
Varmo Vene. Parametricity and Strong Dinaturality. (2006). https://www.ioc.ee/~tarmo/tday-voore/vene-slides.pdf
Jennifer Hackett and Graham Hutton. Programs for cheap!. In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, 115–126.
Tarmo Uustalu. Strong dinaturality and initial algebras. 12th Nordic Wksh. on Programming Theory, NWPT 2 (2000).
Tarmo Uustalu. A Note on Strong Dinaturality, Initial Algebras and Uniform Parameterized Fixpoint Operators. In FICS. 77–82.
Strong dinatural transformations are called paranatural transformations in:
Last revised on October 27, 2023 at 22:29:46. See the history of this page for a list of all contributions to it.