Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

homotopy.io: a proof assistant for finitely-presented globular $n$-categories

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

TL;DR

homotopy.io provides a browser-based proof assistant for finitely-presented semistrict globular $n$-categories, enabling graphical construction and manipulation of $n$-diagrams via a point-and-click interface. It encodes $n$-cells as inductive zigzag diagrams and implements core operations—collapse, contraction, expansion, typechecking, and layout—with a memoisation-enabled rendering pipeline in Rust/WASM. The system supports coherent invertible generators across all dimensions, allows formalization of higher-categorical proofs (e.g., Eckmann–Hilton) in an in-browser environment, and outlines extensions toward Hopf modules, functors, and duals. By combining a lightweight frontend with a rigorous semistrict higher-category model, homotopy.io aims to accelerate proof development, visualization, and sharing in higher category theory research.

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.

homotopy.io: a proof assistant for finitely-presented globular $n$-categories

TL;DR

homotopy.io provides a browser-based proof assistant for finitely-presented semistrict globular -categories, enabling graphical construction and manipulation of -diagrams via a point-and-click interface. It encodes -cells as inductive zigzag diagrams and implements core operations—collapse, contraction, expansion, typechecking, and layout—with a memoisation-enabled rendering pipeline in Rust/WASM. The system supports coherent invertible generators across all dimensions, allows formalization of higher-categorical proofs (e.g., Eckmann–Hilton) in an in-browser environment, and outlines extensions toward Hopf modules, functors, and duals. By combining a lightweight frontend with a rigorous semistrict higher-category model, homotopy.io aims to accelerate proof development, visualization, and sharing in higher category theory research.

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.
Paper Structure (26 sections, 5 theorems, 7 equations, 27 figures, 1 table)

This paper contains 26 sections, 5 theorems, 7 equations, 27 figures, 1 table.

Table of Contents

  1. Introduction
  2. Mathematical context
  3. Related work
  4. Acknowledgements
  5. Using the tool
  6. Adding generators.
  7. Manipulating the workspace.
  8. Theorems.
  9. View control.
  10. Generator options.
  11. Image export.
  12. Example: Eckmann-Hilton
  13. Core data structures
  14. Diagrams
  15. Rewrites
  16. ...and 11 more sections

Key Result

Lemma 1

For a Hopf algebra $H$ in a braided monoidal category, we have $\sigma \circ \eta = \eta$.

Figures (27)

  • Figure 1: The associator 3-diagram shown in both 2D and 3D (https://beta.homotopy.io/p/2402.00001).
  • Figure 2: A real-life 3D print of the associator 3-diagram.
  • Figure 3: A string diagram and the corresponding zigzag encoding.
  • Figure 4: The interface of the proof assistant.
  • Figure 5: The scalars $\alpha$ and $\beta$ in our signature for the Eckmann-Hilton argument.
  • ...and 22 more figures

Theorems & Definitions (9)

  • Lemma 1
  • Lemma 2: majidalgebras1995
  • proof
  • Lemma 3: bespalov1998hopf
  • proof
  • Lemma 4: bespalov1998hopf
  • proof
  • Theorem 5: Fundamental Theorem of Hopf Modules larsonassociative1969,bespalov1998hopf
  • proof