We solve the word problem for free double categories without equations between generators by translating it to the word problem for 2-categories. This yields a quadratic algorithm deciding the equality of diagrams in a free double category. The translation is of interest in its own right since and can for instance be used to reason about double categories with the language of 2-categories, sidestepping the pinwheel problem. It also shows that although double categories are formally more general than 2-categories, they are not actually more expressive, explaining the rarity of applications of this notion.
Keywords: double categories, word problem, string diagrams
2010 MSC: 18D05
Theory and Applications of Categories, Vol. 35, 2020, No. 1, pp 1-18.
Published 2020-01-02.
TAC Home