Show simple item record

dc.contributor.authorPiceghello, Stefano
dc.date.accessioned2021-11-22T09:09:54Z
dc.date.available2021-11-22T09:09:54Z
dc.date.issued2021-12-03
dc.date.submitted2021-11-09T01:52:40Z
dc.identifiercontainer/f3/7b/83/fa/f37b83fa-9256-4374-beeb-7d810d50cd0e
dc.identifier.isbn9788230847114
dc.identifier.isbn9788230867723
dc.identifier.urihttps://hdl.handle.net/11250/2830640
dc.description.abstractHomotopy 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.en_US
dc.language.isoengen_US
dc.publisherThe University of Bergenen_US
dc.rightsAttribution-NonCommercial-NoDerivs (CC BY-NC-ND)
dc.rights.urihttps://creativecommons.org/licenses/by-nc-nd/4.0/
dc.titleCoherence for Monoidal and Symmetric Monoidal Groupoids in Homotopy Type Theoryen_US
dc.typeDoctoral thesisen_US
dc.date.updated2021-11-09T01:52:40Z
dc.rights.holderCopyright the Author.en_US
dc.contributor.orcidhttps://orcid.org/0000-0002-4588-4386
dc.description.degreeDoktorgradsavhandling
fs.unitcode12-11-0


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

Attribution-NonCommercial-NoDerivs (CC BY-NC-ND)
Except where otherwise noted, this item's license is described as Attribution-NonCommercial-NoDerivs (CC BY-NC-ND)