Iteration 2-theories (Q5930757)

Algebraically complete categories are important for computer science. Actually, they are exactly those categories in which one may define recursive data types in a canonical way as initial solutions of recursive functorial equations corresponding to data type specifications. An algebraically complete category \({\mathcal C}\) with a collection \({\mathcal F}\) of functors \({\mathcal C}^{n+p} \rightarrow {\mathcal C}^{n}, n, p \geq 0\), implicitly specifies a dagger operation \(F \longmapsto F^{\dagger}\) on the functors in \({\mathcal F}\). This operation can be extended to natural transformations \(\tau : F \rightarrow G\) between functors \(F\), \(G\) in \({\mathcal F}\). Viewing the functors in \({\mathcal F}\) and their natural transformations as a 2-theory, i.e., a 2-category with Cartesian structure, one obtains a dagger operation defined on all 2-cells. This dagger operation, defined both on functors and on natural transformations, or more generally, on horizontal and vertical morphisms, interacts smoothly with the categorical and Cartesian structure. The study of this interaction is the topic of the present paper. The authors give an axiomatic treatment. Then they introduce a new concept, iteration 2-theories, that generalizes (ordered) iteration theories. By describing explicitly the structure of the free iteration 2-theories, they show that the axioms of iteration 2-theories capture, up to isomorphism, the dagger operation in algebraically complete categories. Their description involves regular trees and they consider some applications of the axioms of iteration 2-theories for manipulating tree transformations.