The uniformity principle on traced monoidal categories (Q1769599): Difference between revisions

\textit{A. Joyal, R. Street} and \textit{D. Verity} [Math. Proc. Camb. Philos. Soc. 119, 447-468 (1996; Zbl 0845.18005)] introduced traces on a monoidal category \(\mathcal C\) as certain natural mappings \(T^X_{A,B} : {\mathcal C}(A \otimes X, B \otimes X) \to {\mathcal C}(A,B)\). In graphical presentation traces appear as loops. An arrow \(h \in {\mathcal C}(X,Y)\) is said to be strict if for every \(f \in {\mathcal C}(A \otimes X, B \otimes X)\), \(g \in {\mathcal C}(A \otimes Y, B \otimes Y)\) such that \((\text{ id}_B \otimes h) \circ f = g \circ (\text{ id}_A \otimes h)\) we have \(T^X_{AB}(f) = T^Y_{AB}(g)\). A uniformity principle on a traced monoidal category is a class \(\mathcal S\) of strict arrows in \(\mathcal C\). On categories with finite products, the Hyland-Hasegawa correspondence says that traces coincide with Conway fixpoint operators. Moreover, an arrow is strict with respect to a trace if and only if it is strict with respect to the corresponding Conway operator (Theorem 5.2, proved in Appendix A). The main topic of the present paper is the construction of new traced monoidal categories from known ones. It is observed that even though traces do not survive common categorical constructions applicable to traced monoidal categories, the uniformity principle helps to select a traced full subcategory. The first example, which is the traced monoidal category of strict maps viewed as a full subcategory of the arrow category \({\mathcal C}^\to\), reproduces the Scott induction principle for Conway operators. The author then discusses other examples and their possible characterization as suitable enriched limits. Previously, a nearly identical version of the paper appears on pages 137--155 of ``Proceedings of the conference on category theory and computer science'' published as Volume 69 of Electronic Notes in Theoretical Computer Science by Elsevier, 2003.