Document Open Access Logo

homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories

Authors Nathan Corbyn , Lukas Heidemann , Nick Hu , Chiara Sarti , Calin Tataru , Jamie Vicary

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.30.pdf
  • Filesize: 1.8 MB
  • 26 pages

Document Identifiers

Author Details

Nathan Corbyn
  • University of Oxford, Oxford, UK
Lukas Heidemann
  • University of Oxford, Oxford, UK
Nick Hu
  • University of Oxford, Oxford, UK
Chiara Sarti
  • University of Cambridge, Cambridge, UK
Calin Tataru
  • University of Cambridge, Cambridge, UK
Jamie Vicary
  • University of Cambridge, Cambridge, UK

Funding

  • Corbyn, Nathan: EPSRC Industrial CASE Studentship
  • Hu, Nick: EPSRC Doctoral Training Partnership Scholarship [grant number 2218955]

Acknowledgements

The authors would like to thank Anastasia Courtney, Yulong Huang, and Jasper Parish for their contributions during their summer internships, Akvilė Valentukonytė and Klaudia Urbanska for their contributions during their undergraduate projects, and Manuel Araújo, Wilf Offord, and Hao Xu for extensive testing of the tool and valuable feedback. We are also grateful to the students of the "Categorical Quantum Mechanics" course at Oxford, and the "Advanced Topics in Category Theory" course at Cambridge for testing and feedback.

Cite AsGet BibTex

Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, and Jamie Vicary. homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 30:1-30:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.30

Abstract

We present the proof assistant homotopy.io for working with finitely-presented semistrict higher categories. The tool runs in the browser with a point-and-click interface, allowing direct manipulation of proof objects via a graphical representation. We describe the user interface and explain how the tool can be used in practice. We also describe the essential subsystems of the tool, including collapse, contraction, expansion, typechecking, and layout, as well as key implementation details including data structure encoding, memoisation, and rendering. These technical innovations have been essential for achieving good performance in a resource-constrained setting.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software notations and tools
Keywords
  • Higher category theory
  • proof assistant
  • string diagrams

Metrics

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

Related Versions

Supplementary Materials

References

  1. Constructing a braiding in homotopy.io. URL: https://homotopy.io/braiding-example.
  2. Nicolás Andruskiewitsch and Walter Ferrer Santos. The Beginnings of the Theory of Hopf Algebras. Acta Applicandae Mathematicae, 108(1):3-17, October 2009. URL: https://doi.org/10.1007/s10440-008-9393-1.
  3. Michael F Atiyah. Topological quantum field theory. Publications Mathématiques de l'IHÉS, 68:175-186, 1988. Google Scholar
  4. John C Baez and James Dolan. Higher-dimensional algebra and topological quantum field theory. Journal of mathematical physics, 36(11):6073-6105, 1995. Google Scholar
  5. John C Baez and Martin Neuchl. Higher dimensional algebra: I. braided monoidal 2-categories. Advances in Mathematics, 121(2):196-244, 1996. Google Scholar
  6. Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: an online proof assistant for higher-dimensional rewriting. Logical Methods in Computer Science, 14, 2018. URL: https://doi.org/10.23638/LMCS-14(1:8)2018.
  7. John W Barrett, Catherine Meusburger, and Gregor Schaumann. Gray categories with duals and their diagrams. arXiv preprint, 2012. URL: https://arxiv.org/abs/1211.0529.
  8. Yuri Bespalov and Bernhard Drabant. Hopf (bi-)modules and crossed modules in braided monoidal categories. Journal of Pure and Applied Algebra, 123(1-3):105-129, 1998. Google Scholar
  9. Simon Burton. String diagrams for higher mathematics with wiggle.py, 2023. Talk at SYCO 11. URL: https://arrowtheory.com/wiggle_demo.pdf.
  10. Giovanni de Felice, Alexis Toumi, and Bob Coecke. Discopy: Monoidal categories in python. arXiv preprint, 2020. URL: https://arxiv.org/abs/2005.02975.
  11. Antonin Delpeuch. A complete language for faceted dataflow programs. arXiv preprint, 2019. URL: https://arxiv.org/abs/1906.05937.
  12. Christoph Dorn. Associative n-categories. arXiv preprint, 2018. URL: https://arxiv.org/abs/1812.10586.
  13. Christoph Dorn and Christopher L Douglas. Manifold diagrams and tame tangles. arXiv preprint arXiv:2208.13758, 2022. Google Scholar
  14. Jean-Christophe Filliâtre and Sylvain Conchon. Type-safe modular hash-consing. In Proceedings of the 2006 Workshop on ML, pages 12-19, 2006. URL: https://doi.org/10.1145/1159876.1159880.
  15. Eric Finster and Samuel Mimram. A type-theoretical definition of weak ω-categories. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12. IEEE, 2017. URL: https://doi.org/10.1109/LICS.2017.8005124.
  16. Amar Hadzihasanovic and Diana Kessler. Data structures for topologically sound higher-dimensional diagram rewriting. arXiv preprint, 2022. URL: https://arxiv.org/abs/2209.09509.
  17. Lukas Heidemann, David Reutter, and Jamie Vicary. Zigzag normalisation for associative n-categories. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 1-13, 2022. URL: https://doi.org/10.1145/3531130.3533352.
  18. Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. Twenty-five years of constructive type theory (Venice, 1995), 36:83-111, 1998. Google Scholar
  19. Heinz Hopf. Uber Die Topologie der Gruppen-Mannigfaltigkeiten und Ihre Verallgemeinerungen. Annals of Mathematics, 42(1):22-52, 1941. Publisher: Annals of Mathematics. URL: https://doi.org/10.2307/1968985.
  20. Nick Hu, Alex Rice, and Calin Tataru. sd-visualiser, 2024. URL: https://github.com/sd-visualiser/sd-visualiser.
  21. Nick Hu, Calin Tataru, and Jamie Vicary. Coherent invertibility in associative n-categories. In preparation, 2024. Google Scholar
  22. Qi Huangfu and JA Julian Hall. Parallelizing the dual revised simplex method. Mathematical Programming Computation, 10(1):119-142, 2018. URL: https://doi.org/10.1007/s12532-017-0130-5.
  23. André Joyal and Ross Street. The geometry of tensor calculus, i. Advances in mathematics, 88(1):55-112, 1991. Google Scholar
  24. Aleks Kissinger and Vladimir Zamdzhiev. Quantomatic: A proof assistant for diagrammatic reasoning. In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 326-336. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_22.
  25. Richard Gustavus Larson and Moss Eisenberg Sweedler. An Associative Orthogonal Bilinear Form for Hopf Algebras. American Journal of Mathematics, 91(1):75, January 1969. URL: https://doi.org/10.2307/2373270.
  26. Tom Leinster. Higher operads, higher categories. Number 298 in London Mathematical Society Lecture Note Series. Cambridge University Press, 2004. Google Scholar
  27. Jacob Lurie. Higher topos theory. Princeton University Press, 2009. Google Scholar
  28. V. Lyubashenko. Modular transformations for tensor categories. Journal of Pure and Applied Algebra, 98(3):279-327, February 1995. URL: https://doi.org/10.1016/0022-4049(94)00045-K.
  29. S. Majid. Algebras and Hopf Algebras in Braided Categories, September 1995. arXiv:q-alg/9509023. URL: https://arxiv.org/abs/q-alg/9509023.
  30. Shahn Majid. Braided groups and algebraic quantum field theories. letters in mathematical physics, 22:167-175, 1991. Google Scholar
  31. John W. Milnor and John C. Moore. On the Structure of Hopf Algebras. The Annals of Mathematics, 81(2):211, March 1965. URL: https://doi.org/10.2307/1970615.
  32. David Jaz Myers. String diagrams for double categories and equipments. arXiv preprint, 2016. URL: https://arxiv.org/abs/1612.02762.
  33. David Reutter and Jamie Vicary. High-level methods for homotopy construction in associative n-categories. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785895.
  34. Emily Riehl and Dominic Verity. Elements of ∞-Category Theory, volume 194. Cambridge University Press, 2022. Google Scholar
  35. Chiara Sarti and Jamie Vicary. Posetal diagrams for logically-structured semistrict higher categories. arXiv preprint, 2023. URL: https://arxiv.org/abs/2305.11637.
  36. Christopher John Schommer-Pries. The classification of two-dimensional extended topological field theories. University of California, Berkeley, 2009. Google Scholar
  37. Pawel Sobocinski, Paul W Wilson, and Fabio Zanasi. Cartographer: A tool for string diagrammatic reasoning (tool paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  38. Moss E. Sweedler. Hopf algebras. Mathematics lecture note series. Benjamin, New York, NY, 1969. Google Scholar
  39. Calin Tataru and Jamie Vicary. A layout algorithm for higher-dimensional string diagrams. arXiv preprint, 2023. URL: https://arxiv.org/abs/2305.06938.
  40. Calin Tataru and Jamie Vicary. The theory and applications of anticolimits. arXiv preprint, 2024. URL: https://arxiv.org/abs/2401.17076.
  41. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  42. Shouchuan Zhang. Braided hopf algebras. arXiv preprint, 2005. URL: https://arxiv.org/abs/math/0511251.
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