Coherence theorem for symmetric monoidal categories

Stream: maths

[Robin Carlier]

Dear all,

I am pleased to announce the public release of a formalization project that has kept me quite busy for the last few months: formalizing "unbiased" versions of symmetric monoidal categories, and linking these unbiased definitions to the ones that we have in mathlib. The repository can be found here.

By "unbiased" symmetric monoidal categories, I mean versions of the notion where tensor product functors are available in all arities, and have natural actions of permutations.
Formally, the objects I think of as unbiased symmetric monoidal categories are pseudofunctors BurnsideFintype ⥤ᵖ Cat that preserve products, where BurnsideFintype is the (2,1)-category of spans of finite types, i.e the bicategory of spans in FintypeCat where non-invertible 2-morphisms are discarded. This point of view on symmetric monoidal categories was taken (in a suitably higher categorical setting) by Cranch in his 2009 thesis as a way to model symmetric monoidal infinity-categories. My repo formalizes the construction of such a pseudofunctor from Mathlib's version of a symmetric monoidal category.

The main technical difficulty in this project is that the classical constructor for a symmetric monoidal category only requires low-arity data and involves finitely many diagrams, while the construction of a pseudofunctor as above requires coherence of this data in arbitrary arity. Quite unsurprisingly, the main ingredient in the construction is Mac Lane’s coherence theorem.
Following similar constructions found in S. Piceghello’s thesis, who formalized part of the coherence theorem in a Rocq + HoTT setting, I was able to formalize the coherence theorem as a symmetric monoidal equivalence of categories between the free symmetric monoidal category on a finite type J and the Pi-category J → Core (FintypeCat), where the latter has the monoidal structure coming from the disjoint sum of types. The main idea (due to Piceghello), is to introduce and study an intermediate category of symmetric lists on a type, which is a categorified version of Multiset. The link between symmetric lists and finite sets, which was not fully formalized in the HoTT setting, comes from a correspondence between the relations that define hom-types in symmetric lists and the presentation of permutations as a Coxeter group (which is why I formalized this presentation).

You can find a small overview of the results in the repo in this file, and some extra information on the repo content in the README.

(Small clarification edit: the project is now at the "yay I did it sorry-free" stage, and some code in here definitely needs some clean-up!)