{"id":"arxiv/2603.00896","url":"https://arxiv.org/abs/2603.00896","tags":["math.CT","cs.LO"],"score":0,"title":"Unbiasing symmetric monoidal categories in Lean","domain":"math.CT","source":"arxiv","authors":["Robin Carlier"],"reviews":0,"subject":"math.CT","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-03-01","reactions":{}}