皆様、 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/1Qrg4c8XDkbO3tmns6tQwxn5lGHOrBON5LtHXXTpX... .
Clovis Eberhart (ERATO MMSD Colloquium Organizer) Email: eberhart@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.