Document Open Access Logo

Coherence for Monoidal Groupoids in HoTT

Author Stefano Piceghello

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2019.8.pdf
  • Filesize: 0.6 MB
  • 20 pages

Document Identifiers

Author Details

Stefano Piceghello
  • Department of Informatics and Department of Mathematics, University of Bergen, Norway

Acknowledgements

The author wishes to thank Kristian S. Alfsvåg, Marc Bezem, Floris van Doorn, Bjœrn Ian Dundas, Peter Dybjer, Favonia and Håkon R. Gylterud for providing valuable insight on the topic and the anonymous reviewers for constructive comments, and acknowledges the support of the Centre for Advanced Study (CAS) in Oslo, Norway, which funded and hosted the research project Homotopy Type Theory and Univalent Foundations during the 2018/19 academic year.

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.TYPES.2019.8

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
Keywords
  • homotopy type theory
  • coherence
  • monoidal categories
  • groupoids
  • higher inductive types
  • formalisation
  • Coq

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Sten Agerholm, Ilya Beylin, and Peter Dybjer. A comparison of HOL and ALF formalizations of a categorical coherence theorem. In Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics, pages 17-32, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0105394.
  2. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, and Bas Spitters. The HoTT library: A formalization of homotopy type theory in Coq, 2016. URL: http://arxiv.org/abs/1610.04591.
  3. Benno van den Berg and Richard Garner. Types are weak ω-groupoids. Proceedings of the London Mathematical Society, 102(2):370-394, 2011. URL: https://doi.org/10.1112/plms/pdq026.
  4. Ilya Beylin. An ALF Proof of Mac Lane’s Coherence Theorem. Licensiate thesis (revision: 5.26), Department of Computing Science, Chalmers / Göteborg University, 1997. Google Scholar
  5. Ilya Beylin and Peter Dybjer. Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, pages 47-61, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-61780-9_61.
  6. Guillaume Brunerie. On the homotopy groups of spheres in homotopy type theory, June 2016. URL: http://arxiv.org/abs/1606.05916.
  7. Guillaume Brunerie, Kuen-Bang Hou (Favonia), Evan Cavallo, Tim Baumann, Eric Finster, Jesper Cockx, Christian Sattler, Chris Jeris, Michael Shulman, et al. Homotopy Type Theory in Agda. URL: https://github.com/HoTT/HoTT-Agda.
  8. Floris van Doorn. On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory, 2018. URL: http://arxiv.org/abs/1808.10690.
  9. Floris van Doorn, Jakob von Raumer, and Ulrik Buchholtz. Homotopy Type Theory in Lean. Lecture Notes in Computer Science, pages 479-495, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_30.
  10. Mike Gordon. Introduction to the HOL System. In 1991 International Workshop on the HOL Theorem Proving System and Its Applications, pages 2-3, August 1991. URL: https://doi.org/10.1109/HOL.1991.596265.
  11. The HoTT library. URL: https://github.com/HoTT/HoTT.
  12. INRIA - The Coq Proof Assistant. URL: https://coq.inria.fr/.
  13. Gregory Maxwell Kelly. On MacLane’s conditions for coherence of natural associativities, commutativities, etc. Journal of Algebra, 1(4):397-402, 1964. URL: https://doi.org/10.1016/0021-8693(64)90018-3.
  14. Tom Leinster. Higher operads, higher categories, volume 298 of London Mathematical Society lecture note series. Cambridge University Press, Cambridge, 2004. URL: https://doi.org/10.1017/CBO9780511525896.
  15. Daniel R. Licata and Guillaume Brunerie. A Cubical Approach to Synthetic Homotopy Theory. In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 92-103, 2015. URL: https://doi.org/10.1109/LICS.2015.19.
  16. Daniel R. Licata and Michael Shulman. Calculating the fundamental group of the circle in homotopy type theory. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '13, pages 223-232, Washington, DC, USA, 2013. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2013.28.
  17. Peter LeFanu Lumsdaine. Weak ω-categories from intensional type theory. Logical Methods in Computer Science, Volume 6, Issue 3, September 2010. URL: https://doi.org/10.2168/LMCS-6(3:24)2010.
  18. Peter LeFanu Lumsdaine and Michael Shulman. Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society, pages 1-50, June 2019. URL: https://doi.org/10.1017/s030500411900015x.
  19. Saunders Mac Lane. Categories for the working mathematician, volume 5 of Graduate texts in mathematics. Springer, New York, 2nd ed. edition, 1998. Google Scholar
  20. Lena Magnusson. The Implementation of ALF - a Proof Editor based on Martin-Löf’s Monomorphic Type Theory with Explicit Substitution. PhD Thesis, Göteborg University and Chalmers University of Technology, 1995. Google Scholar
  21. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
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 About DROPS Imprint Privacy Contact