Document Open Access Logo

Globular: An Online Proof Assistant for Higher-Dimensional Rewriting

Authors Krzysztof Bar, Aleks Kissinger, Jamie Vicary

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2016.34.pdf
  • Filesize: 1.13 MB
  • 11 pages

Document Identifiers

Subject Classification

Keywords
  • higher category theory
  • higher-dimensional rewriting
  • interactive theorem proving

Metrics

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

Abstract

This article introduces Globular, an online proof assistant for the
formalization and verification of proofs in higher-dimensional
category theory. The tool produces graphical visualizations of
higher-dimensional proofs, assists in their construction with a
point-and-click interface, and performs type checking to prevent
incorrect rewrites. Hosted on the web, it has a low barrier to use,
and allows hyperlinking of formalized proofs directly from research
papers. It allows the formalization of proofs from logic, topology and
algebra which are not formalizable by other methods, and we give
several examples.

Cite As Get BibTex

Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: An Online Proof Assistant for Higher-Dimensional Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 34:1-34:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSCD.2016.34

Author Details

Krzysztof Bar
Aleks Kissinger
Jamie Vicary

References

  1. John C. Baez and Aaron D. Lauda. Higher-dimensional algebra V: 2-groups. Theory and Applications of Categories, 12:423-491, 2004. URL: http://www.tac.mta.ca/tac/volumes/12/14/12-14abs.html.
  2. John W. Barrett, Catherine Meusburger, and Gregor Schaumann. Gray categories with duals and their diagrams. J. Diff. Geom., to appear. URL: http://arxiv.org/abs/1211.0529.
  3. Eric Finster. The Orchard proof assistant. URL: https://github.com/ericfinster/orchard.
  4. Yves Guiraud. Polygraphs for termination of left-linear term rewriting systems. 2007. URL: http://arxiv.org/abs/cs/0702040.
  5. HoTT Formalisations in Coq and Agda. URL: http://homotopytypetheory.org/coq.
  6. André Joyal and Ross Street. The geometry of tensor calculus, I. Adv. Math., 88(1):55-112, 1991. URL: http://dx.doi.org/10.1016/0001-8708(91)90003-p.
  7. Aleks Kissinger and Vladimir Zamdzhiev. Quantomatic: A proof assistant for diagrammatic reasoning. In CADE-25 - 25th International Conference on Automated Deduction, volume 9195 of LNCS. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-21401-6_22.
  8. Joachim Kock. Frobenius Algebras and 2D Topological Quantum Field Theories. Cambridge University Press (CUP), 2003. URL: http://dx.doi.org/10.1017/cbo9780511615443.
  9. Stephen Lack. A coherent approach to pseudomonads. Adv. Math., 152(2):179-202, 2000. URL: http://dx.doi.org/10.1006/aima.1999.1881.
  10. Yves Lafont. Algebra and geometry of rewriting. Applied Categorical Structures, 15(4):415-437, 2007. URL: http://dx.doi.org/10.1007/s10485-007-9083-6.
  11. Tom Leinster. A survey of definitions of n-category. Theory and Applications of Categories, 10(1):1-70, 2002. http://arxiv.org/abs/math/0107188. URL: http://tac.mta.ca/tac/volumes/10/1/10-01abs.html.
  12. Shahn Majid. A Quantum Groups Primer. Cambridge University Press (CUP), 2002. URL: http://dx.doi.org/10.1017/cbo9780511549892.
  13. MathForum. Perko pair knots. URL: http://mathforum.org/mathimages/index.php/Perko_pair_knots.
  14. Samuel Mimram. Towards 3-dimensional rewriting theory. Logical Methods in Computer Science, 10(2), 2014. URL: http://dx.doi.org/10.2168/LMCS-10(2:1)2014.
  15. Bodo Pareigis. In Stefaan Caenepeel and Fred Van Oystaeyen, editors, Hopf Algebras in Noncommutative Geometry and Physics, chapter On Symbolic Computations in Braided Monoidal Categories, pages 269-280. CRC Press, 2004. Google Scholar
  16. Kenneth A. Perko. On the classification of knots. Proceedings of the AMS, 45(2):262-262, 1974. URL: http://dx.doi.org/10.1090/s0002-9939-1974-0353294-x.
  17. Piotr Pstragowski. On dualizable objects in monoidal bicategories. Master’s thesis, Bonn University, 2014. URL: http://arxiv.org/abs/1411.6691.
  18. Saavedra Rivano. Catégories Tannakiennes, volume 265 of Lecture Notes in Mathematics. Springer Berlin Heidelberg, 1972. URL: http://dx.doi.org/10.1007/bfb0059108.
  19. Ross Street. Quantum Groups. Cambridge University Press (CUP), 2007. URL: http://dx.doi.org/10.1017/cbo9780511618505.
  20. The Globular Team. Globular documentation. URL: https://ncatlab.org/nlab/show/Globular.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact