Globular: an online proof assistant for higher-dimensional rewriting

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.

References in corpus (4)

• Higher-Dimensional Algebra V: 2-Groups
• Towards 3-Dimensional Rewriting Theory
• On dualizable objects in monoidal bicategories, framed surfaces and the Cobordism Hypothesis
• Polygraphs for termination of left-linear term rewriting systems

Cited by in corpus (7)

• The algebra of entanglement and the geometry of composition
• DisCoPy: Monoidal Categories in Python
• Operads for complex system design specification, analysis and synthesis
• Knowledge Representation in Bicategories of Relations
• Normalization for planar string diagrams and a quadratic equivalence algorithm
• Representable diagrammatic sets as a model of weak higher categories
• Adapting a Formal Model Theory to Applications in Augmented Personalized Medicine