License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2019.8
URN: urn:nbn:de:0030-drops-130722
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13072/
Go to the corresponding LIPIcs Volume Portal

Piceghello, Stefano

Coherence for Monoidal Groupoids in HoTT

pdf-format:
LIPIcs-TYPES-2019-8.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{piceghello:LIPIcs:2020:13072,
  author =	{Stefano Piceghello},
  title =	{{Coherence for Monoidal Groupoids in HoTT}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Marc Bezem and Assia Mahboubi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13072},
  URN =		{urn:nbn:de:0030-drops-130722},
  doi =		{10.4230/LIPIcs.TYPES.2019.8},
  annote =	{Keywords: homotopy type theory, coherence, monoidal categories, groupoids, higher inductive types, formalisation, Coq}
}

Keywords: homotopy type theory, coherence, monoidal categories, groupoids, higher inductive types, formalisation, Coq
Collection: 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Issue Date: 2020
Date of publication: 24.09.2020
Supplementary Material: Formalised proofs are available at https://github.com/spiceghello/FSMG.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI