Globular: an online proof assistant for higher-dimensional rewriting

TL;DR

Globular is an online proof assistant designed for higher-dimensional category theory, providing graphical visualization, interactive proof construction, and type checking, making formalization more accessible and integrable with research papers.

Contribution

It introduces a web-based tool that enables formalization and verification of higher-dimensional proofs with visual and interactive features, a novel approach in this research area.

Findings

Supports formalization in logic, topology, and algebra

Provides graphical visualization of proofs

Enables hyperlinking from research papers

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.