Document Open Access Logo

Category Theory in Coq 8.5

Authors Amin Timany, Bart Jacobs

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.30.pdf
  • Filesize: 0.53 MB
  • 18 pages

Document Identifiers

Author Details

Amin Timany
Bart Jacobs

Cite AsGet BibTex

Amin Timany and Bart Jacobs. Category Theory in Coq 8.5. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSCD.2016.30

Abstract

We report on our experience implementing category theory in Coq 8.5. Our work formalizes most of basic category theory, including concepts not covered by existing formalizations, in a library that is fit to be used as a general-purpose category-theoretical foundation. Our development particularly takes advantage of two features new to Coq 8.5: primitive projections for records and universe polymorphism. Primitive projections allow for well-behaved dualities while universe polymorphism provides a relative notion of largeness and smallness. The latter is one of the main contributions of this paper. It pushes the limits of the new universe polymorphism and constraint inference algorithm of Coq 8.5. In this paper we present in detail smallness and largeness in categories and the foundation they are built on top of. We furthermore explain how we have used the universe polymorphism of Coq 8.5 to represent smallness and largeness arguments by simply ignoring them and entrusting them to the universe inference algorithm of Coq 8.5. We also briefly discuss our experience throughout this implementation, discuss concepts formalized in this development and give a comparison with a few other developments of similar extent.
Keywords
  • Category Theory
  • Coq 8.5
  • Universe Polymorphism
  • Homotopy Type Theory

Metrics

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

References

  1. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the rezk completion. Mathematical Structures in Computer Science, 25(05):1010-1039, jan 2015. URL: https://github.com/benediktahrens/rezk_completion, URL: http://dx.doi.org/10.1017/s0960129514000486.
  2. Steve Awodey. Category theory. Oxford University Press, 2010. Google Scholar
  3. Bodil Biering, Lars Birkedal, and Noah Torp-Smith. Bi-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst., 29(5), August 2007. URL: http://dx.doi.org/10.1145/1275497.1275499.
  4. Lars Birkedal, Rasmus Ejlers Mogelberg, Jan Schwinghammer, and Kristian Stovring. First steps in synthetic guarded domain theory: Step-indexing in the topos of trees. In 2011 IEEE 26th Annual Symposium on Logic in Computer Science. Institute of Electrical & Electronics Engineers (IEEE), jun 2011. URL: http://dx.doi.org/10.1109/lics.2011.16.
  5. Lars Birkedal, Kristian Støvring, and Jacob Thamsborg. The category-theoretic solution of recursive metric-space equations. Theoretical Computer Science, 411(47):4102-4122, oct 2010. URL: http://dx.doi.org/10.1016/j.tcs.2010.07.010.
  6. T. Coquand. An analysis of Girard’s paradox. Technical Report RR-0531, INRIA, May 1986. URL: https://hal.inria.fr/inria-00076023.
  7. Jason Gross, Adam Chlipala, and David I. Spivak. Experience Implementing a Performant Category-Theory Library in Coq. In Interactive Theorem Proving - 5th International Conference, ITP 2014. Proceedings, pages 275-291, July 2014. URL: http://dx.doi.org/10.1007/978-3-319-08970-6_18.
  8. Jason Gross, Adam Chlipala, and David I. Spivak. Experience implementing a performant category-theory library in coq, 2014. URL: http://arxiv.org/abs/arXiv:1401.7694.
  9. Gérard P. Huet and Amokrane Saïbi. Constructive category theory. In Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 239-276, 2000. URL: http://www.lix.polytechnique.fr/coq/pylons/coq/pylons/contribs/view/ConCaT/v8.4.
  10. Bart Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999. Google Scholar
  11. Saunders Mac Lane. Categories for the working mathematician, volume 5. Springer Science &Business Media, 1978. Google Scholar
  12. The Coq development team. Coq 8.5 Reference Manual. Inria, 2015. Google Scholar
  13. Colin McLarty. Elementary Categories, Elementary Toposes. Oxford University Press, Oxford, UK, 1996. Google Scholar
  14. Adam Megacz. Category Theory in Coq. URL: http://www.megacz.com/berkeley/coq-categories/.
  15. John C. Mitchell. Foundations of Programming Languages. MIT Press, Cambridge, MA, USA, 1996. Google Scholar
  16. Daniel Peebles, James Deikun, Ulf Norell, Dan Doel, Andrea Vezzosi, Darius Jahandarie, and James Cook. copumpkin/categories. URL: https://github.com/copumpkin/categories.
  17. Antonino Salibra. Scott is always simple. In Proceedings of the 37th International Conference on Mathematical Foundations of Computer Science, MFCS'12, pages 31-45, Berlin, Heidelberg, 2012. Springer-Verlag. URL: http://dx.doi.org/10.1007/978-3-642-32589-2_3.
  18. Matthieu Sozeau and Nicolas Tabareau. Universe Polymorphism in Coq. In Interactive Theorem Proving, ITP 2014, Proceedings, pages 499-514, July 2014. URL: http://dx.doi.org/10.1007/978-3-319-08970-6_32.
  19. The Univalent Foundations Program. HoTT Version of Coq and Library. URL: https://github.com/HoTT/HoTT.
  20. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  21. Amin Timany. Categories. URL: https://github.com/amintimany/Categories/tree/FSCD16, URL: http://dx.doi.org/10.5281/zenodo.50689.
  22. Amin Timany. Categories-HoTT. URL: https://github.com/amintimany/Categories-HoTT.
  23. Amin Timany and Bart Jacobs. The Category-theoretic Solution of Recursive Ultra-metric Space Equations. Presented at CoqPL'16: The Second International Workshop on Coq for PL. URL: https://github.com/amintimany/CTDT.
  24. Amin Timany and Bart Jacobs. First Steps Towards Cumulative Inductive Types in CIC. In 12th International Colloquium on Theoretical Aspects of Computing (ICTAC 2015) 2015. Proceedings, pages 608-617, 2015. URL: http://dx.doi.org/10.1007/978-3-319-25150-9_36.
  25. Amin Timany and Bart Jacobs. Category Theory in Coq 8.5: Extended Version. Technical Report CW697, iMinds-Distrinet, KU Leuven, April 2016. URL: http://www2.cs.kuleuven.be/publicaties/rapporten/cw/CW697.abs.html.
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