Every proof assistant: introducing homotopy.io – a proof assistant for geometric...
source link: https://math.andrej.com/2020/11/24/homotopy-io/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Every proof assistant: introducing homotopy.io – a proof assistant for geometrical higher category theory
- 24 November 2020
- Andrej Bauer
- 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.ioAbstract:
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
Post a comment:
$⋯$
for inline and $$⋯$$
for display LaTeX formulas,
and <pre>⋯</pre>
for display code. Your E-mail address is only used to compute
your Gravatar and is not stored anywhere.
Comments are moderated through pull requests.
Name
Website
Comment
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK