论文标题
组成DIN自然转化：朝着替代的计算
Composing Dinatural Transformations: Towards a Calculus of Substitution
论文作者
论文摘要
DIN Natural Transformations将无处不在的自然转化推广到域和Codomain函子具有混合差异的情况下，通常无法构成；自1970年被Dubuc and Street发现以来，已经知道了这一点。已经发现了许多临时解决方案，但是已经缺少了综合性的一般理论，直到Petric在2003年的Petric介绍了G-Dinalal Transformation的概念，即DIAN NATARATION转换的概念，即与适当的图表相结合：他是两种形式的结构，他的本质上是必不可少的二合性效果，是对二合性的含量的结合，是对二合性的含量的结合，并介绍了对二元的转换。反过来又是dinatural。在这里，我们提出了一种替代性，语义而不是句法的证据，证明了Petric定理，作者对此独立地重新发现了该定理，却不知道其先前的存在。然后，我们使用它来定义广义函子类别，其对象是许多变量中混合差异的函子，并且其形态是变换，仅在其某些变量中才恰好是dinatual。我们还为DIN自然转化定义了水平组成的概念，扩展了众所周知的自然转化版本，并证明它是关联和统一的。水平组成体现了函子代替转换，反之亦然，并且通过将图形替换为图形，可以直观地反映出字符串数字的观点。
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.
