Jamie Vicary: Introducing homotopy.io: A proof assistant for geometrical higher category theory

Date of publication: 24. 11. 2020
Mathematics and theoretical computing seminar
Četrtek, 26. 11. 2020, od 15:00 do 16:00, spletni seminar

Zoom ID 989 0478 8985

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