Unbiasing symmetric monoidal categories in Lean
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2603.00896
curl -X POST /api/v1/records/arxiv/2603.00896/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2603.00896/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'