Unbiasing symmetric monoidal categories in Lean

Robin Carlier

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 exte…