Constructing symmetric monoidal bicategories functorially

TL;DR

This paper introduces a functorial method to construct symmetric monoidal bicategories from monoidal double categories satisfying a lifting condition, simplifying the verification of coherence laws in various mathematical contexts.

Contribution

It provides a general, functorial construction of monoidal bicategories from double categories, preserving structures like monoidal functors and transformations, with broad applications.

Findings

Constructs monoidal bicategories from double categories using a lifting condition

Ensures preservation of monoidal structures and functors in the construction

Applies to examples like algebras, bimodules, spans, and parametrized spectra

Abstract

We present a method of constructing monoidal, braided monoidal, and symmetric monoidal bicategories from corresponding types of monoidal double categories that satisfy a lifting condition. Many important monoidal bicategories arise naturally in this way, and applying our general method is much easier than explicitly verifying the coherence laws of a monoidal bicategory for each example. Abstracting from earlier work in this direction, we express the construction as a functor between locally cubical bicategories that preserves monoid objects; this ensures that it also preserves monoidal functors, transformations, adjunctions, and so on. Examples include the monoidal bicategories of algebras and bimodules, categories and profunctors, sets and spans, open Markov processes, parametrized spectra, and various functors relating them.