Jamie Vicary: Introducing homotopy.io: A proof assistant for geometrical higher category theory
Jamie Vicary, University of Cambridge
(joint work with Lukas Heidemann, Nick Hu and David Reutter)
Abstract: Weak higher categories can be difficult to work with algebraically, with the weak structure potentially leading to considerable bureaucracy. Conjecturally, every weak infty-category is equivalent to a "semistrict" one, in which unitors and associators are trivial; such a setting might reduce the burden of constructing large proofs. In this talk, I will present the proof assistant homotopy.io, which allows direct construction of composites in a finitely-generated semistrict (infty,infty)-category. The terms of the proof assistant have a geometrical interpretation as string diagrams, and interaction with the proof assistant is entirely geometrical, by clicking and dragging with the mouse, completely unlike more traditional computer algebra systems. I will give an outline of the underlying theoretical foundations, and demonstrate use of the proof assistant to construct some nontrivial homotopies, rendered in 2d and 3d. I will close with some speculations about the possible interaction of such a system with more traditional type-theoretical approaches.
nLab link: https://ncatlab.org/nlab/show/homotopy.io
arXiv: https://arxiv.org/abs/1902.03831
