Coherence for rewriting 2-theories

TL;DR

This paper develops general coherence theorems for finitary Lawvere 2-theories within term rewriting, enabling explicit presentations of complex algebraic structures like higher Thompson groups and iterated monoidal categories.

Contribution

It introduces two coherence theorems applicable to different classes of rewriting 2-theories, providing new categorical presentations and proofs for complex algebraic structures.

Findings

Constructed explicit presentations for higher Thompson groups.

Developed a new proof of coherence for iterated monoidal categories.

Established coherence theorems for non-confluent, non-terminating 2-theories.

Abstract

General coherence theorems are constructed that yield explicit presentations of categorical and algebraic objects. The categorical structures involved are finitary discrete Lawvere 2-theories, though they are approached within the language of term rewriting theory. Two general coherence theorems are obtained. The first applies to terminating and confluent rewriting 2-theories. This result is exploited to construct systematic presentations for the higher Thompson groups and the Higman-Thompson groups. The presentations are categorically interesting as they arise from higher-arity analogues of the Stasheff/Mac Lane coherence axioms, which involve phenomena not present in the classical binary axioms. The second general coherence theorem holds for 2-theories that are not necessarily confluent or terminating and is used to construct a new proof of coherence for iterated monoidal categories, which arise as categorical models of iterated loop spaces and fail to be confluent.