Coherence for Monoidal Groupoids in HoTT
Journal article, Peer reviewed
Published version
Åpne
Permanent lenke
https://hdl.handle.net/11250/2763059Utgivelsesdato
2020Metadata
Vis full innførselSamlinger
- Department of Informatics [899]
- Registrations from Cristin [9371]
Originalversjon
Leibniz International Proceedings in Informatics. 2020, 8, 1-20 10.4230/LIPIcs.TYPES.2019.8Sammendrag
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.