# Every proof assistant: introducing homotopy.io – a proof assistant for geometrical higher category theory

- 24 November 2020
- Talks, Every proof assistant

After a short pause, our next talk in the series will be given by Jamie Vicary, who will present a proof assistant in which the proofs are drawn!

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

Time:Thursday, November 26, 2020 from 15:00 to 16:00 (Central European Time, UTC+1)

Location:online at Zoom ID 989 0478 8985

Speaker:Jamie Vicary (University of Cambridge)

Proof assistant:homotopy.io

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. (Joint work with Lukas Heidemann, Nick Hu and David Reutter.)

References:

- David Reutter, Jamie Vicary:
High-level methods for homotopy construction in associative n-categories, arXiv:1902.03831 preprint, February 2019.- homotopy.io at Lab

**How to comment on this blog:**At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention

`andrejbauer@mathstodon.xyz`

, I will
gladly respond.
You are also welcome to contact me directly.