Homotopy.io
Jul 1, 2024·
,
,
,
,
Nathan Corbyn
Lukas Heidemann
Nick Hu
Chiara Sarti
Calin Tataru
Jamie Vicary
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.
Type
Publication
9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Authors
PhD Student
I am a PhD student at the Department of Computer Science and Technology,
University of Cambridge, working on higher categories and type theory.