Show simple item record

dc.contributor.authorPiceghello, Stefano
dc.date.accessioned2021-07-02T09:15:49Z
dc.date.available2021-07-02T09:15:49Z
dc.date.created2020-09-24T09:48:57Z
dc.date.issued2020
dc.PublishedLeibniz International Proceedings in Informatics. 2020, 175 8:1-8:20.
dc.identifier.issn1868-8969
dc.identifier.urihttps://hdl.handle.net/11250/2763059
dc.description.abstractWe 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.isoengen_US
dc.publisherDagstuhl publishingen_US
dc.rightsNavngivelse 4.0 Internasjonal*
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/deed.no*
dc.titleCoherence for Monoidal Groupoids in HoTTen_US
dc.typeJournal articleen_US
dc.typePeer revieweden_US
dc.description.versionpublishedVersionen_US
dc.rights.holderCopyright 2020 The Authoren_US
cristin.ispublishedtrue
cristin.fulltextoriginal
cristin.qualitycode1
dc.identifier.doi10.4230/LIPIcs.TYPES.2019.8
dc.identifier.cristin1832843
dc.source.journalLeibniz International Proceedings in Informaticsen_US
dc.source.40175
dc.source.pagenumber8:1-8:20en_US
dc.relation.projectNorges forskningsråd: 240810en_US
dc.identifier.citationLeibniz International Proceedings in Informatics. 2020, 8, 1-20en_US
dc.source.volume175en_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

Navngivelse 4.0 Internasjonal
Except where otherwise noted, this item's license is described as Navngivelse 4.0 Internasjonal