# The word problem for double categories

## TL;DR

This paper presents a quadratic algorithm to solve the word problem in free double categories by translating it into the well-understood word problem for 2-categories, simplifying reasoning and revealing that double categories are not more expressive than 2-categories.

## Contribution

It introduces a translation method from double categories to 2-categories that enables efficient decision procedures for diagram equality.

## Key findings

- Quadratic algorithm for diagram equality in free double categories.
- Double categories are not more expressive than 2-categories.
- The translation helps reason about double categories using 2-category language.

## Abstract

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.