Weak units, universal cells, and coherence via universality for bicategories

TL;DR

This paper develops a new framework for bicategories using poly-bicategories and merge-bicategories, introducing universal cells and weak units to achieve semi-strictification in higher-dimensional categories.

Contribution

It introduces merge-bicategories and a semi-strictification theorem, advancing the understanding of coherence and strictification in higher-dimensional categorical structures.

Findings

Recovered bicategory structure via weak units

Established equivalences between morphisms and transformations

Proved semi-strictification for merge-bicategories

Abstract

Poly-bicategories generalise planar polycategories in the same way as bicategories generalise monoidal categories. In a poly-bicategory, the existence of enough 2-cells satisfying certain universal properties (representability) induces coherent algebraic structure on the 2-graph of single-input, single-output 2-cells. A special case of this theory was used by Hermida to produce a proof of strictification for bicategories. No full strictification is possible for higher-dimensional categories, seemingly due to problems with 2-cells that have degenerate boundaries; it was conjectured by C. Simpson that semi-strictification excluding units may be possible. We study poly-bicategories where 2-cells with degenerate boundaries are barred, and show that we can recover the structure of a bicategory through a different construction of weak units. We prove that the existence of these units is equivalent to the existence of 1-cells satisfying lower-dimensional universal properties, and study the relation between preservation of units and universal cells. Then, we introduce merge-bicategories, a variant of poly-bicategories with more composition operations, which admits a natural monoidal closed structure, giving access to higher morphisms. We derive equivalences between morphisms, transformations, and modifications of representable merge-bicategories and the corresponding notions for bicategories. Finally, we prove a semi-strictification theorem for representable merge-bicategories with a choice of composites and units.