Coherent confluence modulo relations and double groupoids

TL;DR

This paper develops a method to compute coherent presentations of n-categories with rewrite relations modulo axioms, using double groupoids to encode confluence and coherence diagrams, with applications in algebraic structures.

Contribution

It introduces a novel procedure for coherence in n-categories modulo axioms, utilizing double groupoid structures to handle complex rewriting systems.

Findings

Applicable to rewriting systems modulo commutation in monoids

Handles isotopy relations in monoidal categories

Addresses inverse relations in groups

Abstract

A coherent presentation of an n-category is a presentation by generators, relations and relations among relations. Confluent and terminating rewriting systems generate coherent presentations, whose relations among relations are defined by confluence diagrams of critical branchings. This article introduces a procedure to compute coherent presentations when the rewrite relations are defined modulo a set of axioms. Our coherence results are formulated using the structure of n-categories enriched in double groupoids, whose horizontal cells represent rewriting paths, vertical cells represent the congruence generated by the axioms and square cells represent coherence cells induced by diagrams of confluence modulo. We illustrate our constructions on rewriting systems modulo commutation relations in commutative monoids, isotopy relations in pivotal monoidal categories, and inverse relations in groups.