A coherence theorem for pseudonatural transformations

TL;DR

This paper establishes coherence theorems for bicategories, pseudofunctors, and pseudonatural transformations, utilizing rewriting techniques and introducing new concepts like white-categories and partial coherence.

Contribution

It extends coherence results to pseudonatural transformations by developing new rewriting methods and concepts, filling gaps in existing approaches.

Findings

Proves coherence for bicategories and pseudofunctors using Squier's Theorem.

Introduces white-categories and partial coherence for pseudonatural transformations.

Develops new rewriting techniques to complete the coherence proof.

Abstract

We prove coherence theorems for bicategories, pseudofunctors and pseudonatural transformations. These theorems boil down to proving the coherence of some free $(4,2)$-categories. In the case of bicategories and pseudofunctors, existing rewriting techniques based on Squier's Theorem allow us to conclude. In the case of pseudonatural transformations this approach only proves the coherence of part of the structure, and we use a new rewriting result to conclude. To this end, we introduce the notions of white-categories and partial coherence.