Coherence for Monoidal and Symmetric Monoidal Groupoids in Homotopy Type Theory

Abstract

Homotopy Type Theory (HoTT) is a variant of Martin-Löf Type Theory (MLTT) developed in such a way that types can be interpreted as infinity-groupoids, where the iterated construction of identity types represents the different layers of higher path space objects. HoTT can be used as a foundation of mathematics, and the proofs produced in its language can be verified with the aid of specific proof assistant software. In this thesis, we provide a formulation and a formalization of coherence theorems for monoidal and symmetric monoidal groupoids in HoTT.

In order to design 1-types FMG(X) and FSMG(X) representing the free monoidal and the free symmetric monoidal groupoid on a 0-type X of generators, we use higher inductive types (HITs), which apply the functionality of inductive definitions to the higher groupoid structure of types given by the identity types. Coherence for monoidal groupoids is established by showing a monoidal equivalence between FMG(X) and the 0-type list(X) of lists over X. For symmetric monoidal groupoids, we prove a symmetric monoidal equivalence between FSMG(X) and a simpler HIT slist(X) based on lists, whose paths and 2-paths make for an auxiliary symmetric structure on top of the monoidal structure already present on list(X).

Part of the thesis is devoted to the proof that the subuniverse BS_* of finite types is equivalent to the type slist(1), where 1 is the unit type, and hence that the former is a free symmetric monoidal groupoid. As an intermediate step, we show a symmetric monoidal equivalence between slist(1) and an indexed HIT del_* of deloopings of symmetric groups. The proof of a symmetric monoidal equivalence between del_* and BS_* rests on a few, unformalized statements. Assuming this equivalence, we are able to prove that, in a free symmetric monoidal groupoid, all diagrams involving symmetric monoidal expressions without repetitions commute.

This work is accompanied by a computer verification in the proof assistant Coq, which covers most of the results we present in this thesis.