Globular: an online proof assistant for higher-dimensional rewriting

Understand

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.