BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Jamie Vicary (University of Cambridge)
DTSTART:20220504T160000Z
DTEND:20220504T170000Z
DTSTAMP:20260423T024612Z
UID:TQFT/59
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/TQFT/59/">In
 troducing homotopy.io: A proof assistant for geometrical higher category t
 heory</a>\nby Jamie Vicary (University of Cambridge) as part of Topologica
 l Quantum Field Theory Club (IST\, Lisbon)\n\nLecture held in Room 3.10 (3
 rd floor\, Mathematics Department\, Instituto Superior Técnico).\n\nAbstr
 act\nWeak higher categories can be difficult to work with algebraically\, 
 with the weak structure potentially leading to considerable bureaucracy. C
 onjecturally\, every weak $\\infty$-category is equivalent to a "semistric
 t" one\, in which unitors and associators are trivial\; such a setting mig
 ht reduce the burden of constructing large proofs. In this talk\, I will p
 resent the proof assistant homotopy.io\, which allows direct construction 
 of composites in a finitely-generated semistrict $(\\infty\,\\infty)$-cate
 gory. The terms of the proof assistant have an interpretation as string di
 agrams\, and interaction with the proof assistant is entirely geometrical\
 , by clicking and dragging with the mouse\, completely unlike traditional 
 computer algebra systems. I will give an outline of the underlying theoret
 ical foundations\, and demonstrate use of the proof assistant to construct
  some nontrivial homotopies\, rendered in 2d\, 3d\, and in 4d as movies. I
  will close with some speculations about the possible interaction of such 
 a system with more traditional type-theoretical approaches. (Joint work wi
 th Nathan Corbyn\, Calin Tataru\, Lukas Heidemann\, Nick Hu and David Reut
 ter.)\n
LOCATION:https://researchseminars.org/talk/TQFT/59/
END:VEVENT
END:VCALENDAR