2026-07-23T22:31:36Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13072 2024-03-06T10:51:13Z ddc:004 open_access

Coherence for Monoidal Groupoids in HoTT Piceghello, Stefano homotopy type theory coherence monoidal categories groupoids higher inductive types formalisation Coq We present a proof of coherence for monoidal groupoids in homotopy type theory. An important role in the formulation and in the proof of coherence is played by groupoids with a free monoidal structure; these can be represented by 1-truncated higher inductive types, with constructors freely generating their defining objects, natural isomorphisms and commutative diagrams. All results included in this paper have been formalised in the proof assistant Coq. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Stefano Piceghello 2020 Is Part Of LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2019.8 urn:nbn:de:0030-drops-130722 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.8 eng https://creativecommons.org/licenses/by/3.0/legalcode