[logic-ml] ERATO Project Colloquium by Nick Hu (16:30 on May 17th)

[Shinya KATSUMATA]

皆様、
ERATO蓮尾プロジェクトで以下の講演を予定しており、ご案内いたします。
勝股
----------
Dear all,

On Tuesday May 17th, Nick Hu, (a doctoral student at the University of
Oxford) will give a talk, homotopy.io: a proof assistant for
finitely-presented globular n-categories, for our project colloquium
at 16:30. Further details can be found below.

If you would like to attend, please register through the following Google form:
https://forms.gle/6PoGNEfJVHLYDAdKA 
We later send you a zoom link by an email (using BCC).

For the latest information about ERATO colloquium / seminar, please see the webpage https://docs.google.com/document/d/1Qrg4c8XDkbO3tmns6tQwxn5lGHOrBON5LtHXXTpXDeA/edit?usp=sharing .

Clovis Eberhart (ERATO MMSD Colloquium Organizer)
Email: eberhart at nii.ac.jp
-------
Tuesday May 17th, 16:30

Speaker: Nick Hu (University of Oxford)
Title:
homotopy.io: a proof assistant for finitely-presented globular n-categories

Abstract:
String diagrams present a convenient calculus for monoidal
categories which appeal to topological intuitions and quotient
out 'bureaucratic' coherence data. When regions are coloured
(i.e. information-carrying), they analogously provide a
graphical calculus for bicategories. Generalising,
n-categories are difficult to define and manipulate
algebraically, but intuitively correspond to an n-dimensional
string diagram calculus. For n > 3, manipulating n-dimensional
string diagrams quickly becomes unwieldy and error-prone.
Towards this aim, we introduce the proof assistant
homotopy.io.