1 Search Results for "Piceghello, Stefano"

Document
DOI: 10.4230/LIPIcs.TYPES.2019.8
Coherence for Monoidal Groupoids in HoTT

Authors: Stefano Piceghello

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)

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.
Cite as

Stefano Piceghello. Coherence for Monoidal Groupoids in HoTT. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{piceghello:LIPIcs.TYPES.2019.8,
  author =	{Piceghello, Stefano},
  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 =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.8},
  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}
}
  • Refine by Author
  • 1 Piceghello, Stefano

  • Refine by Classification
  • 1 Theory of computation → Constructive mathematics
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Coq
  • 1 coherence
  • 1 formalisation
  • 1 groupoids
  • 1 higher inductive types
  • Show More...

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2020

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact