Papers With

← All papers
First page of Unbiasing symmetric monoidal categories in Lean

Unbiasing symmetric monoidal categories in Lean

Robin Carlier

math.CT Mar 1, 2026 · v1
formalization category-theory mathlib
Read PDF arXiv abstract
TL;DR
Formalizes the unbiasing process for symmetric monoidal categories in Lean 4 within Mathlib.
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.
Problem

Symmetric monoidal categories in Lean's Mathlib require biased binary tensor products, making higher-arity tensor products and their coherences cumbersome to work with formally.

Approach

The authors formalize the unbiasing process for symmetric monoidal categories in Lean 4 within Mathlib. They extend 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 uses a formalization of Mac Lane's coherence theorem via Piceghello's presentation of free symmetric monoidal categories as symmetric lists, and an encoding of universal formulas via a Kleisli bicategory.

Results

The formalization provides a complete unbiasing construction within Mathlib's framework, enabling seamless manipulation of higher-arity tensor products with automatically derived coherence isomorphisms.