dc.contributor.author | Piceghello, Stefano | |
dc.date.accessioned | 2021-07-02T09:15:49Z | |
dc.date.available | 2021-07-02T09:15:49Z | |
dc.date.created | 2020-09-24T09:48:57Z | |
dc.date.issued | 2020 | |
dc.Published | Leibniz International Proceedings in Informatics. 2020, 175 8:1-8:20. | |
dc.identifier.issn | 1868-8969 | |
dc.identifier.uri | https://hdl.handle.net/11250/2763059 | |
dc.description.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. | en_US |
dc.language.iso | eng | en_US |
dc.publisher | Dagstuhl publishing | en_US |
dc.rights | Navngivelse 4.0 Internasjonal | * |
dc.rights.uri | http://creativecommons.org/licenses/by/4.0/deed.no | * |
dc.title | Coherence for Monoidal Groupoids in HoTT | en_US |
dc.type | Journal article | en_US |
dc.type | Peer reviewed | en_US |
dc.description.version | publishedVersion | en_US |
dc.rights.holder | Copyright 2020 The Author | en_US |
cristin.ispublished | true | |
cristin.fulltext | original | |
cristin.qualitycode | 1 | |
dc.identifier.doi | 10.4230/LIPIcs.TYPES.2019.8 | |
dc.identifier.cristin | 1832843 | |
dc.source.journal | Leibniz International Proceedings in Informatics | en_US |
dc.source.40 | 175 | |
dc.source.pagenumber | 8:1-8:20 | en_US |
dc.relation.project | Norges forskningsråd: 240810 | en_US |
dc.identifier.citation | Leibniz International Proceedings in Informatics. 2020, 8, 1-20 | en_US |
dc.source.volume | 175 | en_US |