Unbiasing symmetric monoidal categories in Lean

TL;DR

This paper formalizes the unbiasing process for symmetric monoidal categories in Lean 4, extending the structure to a Cat-valued pseudofunctor and leveraging coherence theorems and bicategory encodings.

Contribution

It introduces a formalization of unbiasing symmetric monoidal categories in Lean 4, incorporating higher arity tensor products and coherence via advanced categorical constructs.

Findings

Successful formalization within Lean 4 and Mathlib

Extension to a Cat-valued pseudofunctor capturing higher arities

Implementation of Mac Lane's coherence theorem in the formal setting

Abstract

We present a formalization in Lean 4, within the framework of the mathematical library Mathlib, of the unbiasing process for symmetric monoidal categories. This is realized by extending the data of a symmetric monoidal category to a Cat-valued pseudofunctor from the (2,1)-category of spans of finite sets, encoding tensor products of higher arities and their coherences. The construction relies on a formalization of Mac Lane's coherence theorem using Piceghello's presentation of free symmetric monoidal categories as symmetric lists, and uses an encoding of universal formulas via an appropriate Kleisli bicategory.