Composing dinatural transformations: towards a calculus of substitution (Q2031559)

\textit{G. M. Kelly} [Lect. Notes Math. 281, 106--147 (1972; Zbl 0243.18016)] argued that an \textit{abstract theory of coherence} requires a tidy \textit{calculus of substitution} for functors of several variables and appropriately general kinds of natural transformations, generalizing the usual \textit{Godement calculus} [\textit{R. Godement}, Topologie algébrique et théorie des faisceaux. Paris: Hermann \& Cie (1958; Zbl 0080.16201), Appendice] for ordinary functors and ordinary natural transformations. One could say that the five rules of the functorial calculus set down by Godement are in fact equivalent to claiming that vertical and horizontal compositions of natural transformations as well as sequential composition of functors are associative, unitary and pursuant to the usual interchange law. With the notion of \textit{graph} of a natural transformation, Kelly introduced a full Godement calculus for covariant functors only, running into troubles when trying to deal with the mixed-variance case. This paper aims to consider transformations between \textit{mixed-variance} functors, recognizing that they are a straightfoward generalization of \textit{dinatural transformations} [\textit{E. Dubuc} and \textit{R. Street}, Lect. Notes Math. 137, 126--137 (1970; Zbl 0222.18004)] in several variables. A synopsis of the paper, consisting of four sections, goes as follows. \begin{itemize} \item \textit{Z. Petrić} [Ann. Pure Appl. Logic 122, No. 1--3, 131--173 (2003; Zbl 1036.18001)] succeeded in finding a sufficient and essentially necessary condition for two consecutive g-dinatural transformations to compose, while the same result was rediscovered by [ISBN 978-3-95977-088-0, pp. 33:1-33:22]. The proof of the former is purely syntactic, while the one of the latter is semantic, interpreting the composite graph as a \textit{Petri net} [\textit{C. A. Petri}, in: Inf. Process., Proc. IFIP Congr. Munich 27 August-1 September 1962, 386--390 (1963; Zbl 0146.14404)]. \S 2 gives a proof of the result different from both. \item \S 3 defines a working notion of horizontal compostion, as is expected to play the role of substitution of dinaturals into dinaturals. \item \S 4 forms a generalized functor category \(\left\{ \mathbb{B} ,\mathbb{C}\right\} \) by dint of \S 2, where transformations have to be equipped with complicated Petri nets, and upon composition the graphs are linked simply along the common interface without collapsing entire connected components into a single transition. It is demonstrated that \(\left\{ \mathbb{B},-\right\} \)\ is of a left adjoint \(-\circ\mathbb{B}\), giving rise to the definition of a category of formal substitutions \(\mathbb{A} \circ\mathbb{B}\)\ as a generalization of Kelly's one. \end{itemize}