A categorical diagram editor to help formalising commutation proofs

Abstract

I will present a categorical diagram editor (https://amblafont.github.io/graph-editor/index.html) implemented in Elm that generates Coq proof scripts (based on the UniMath library), letting the user prove manually commutation of each subdiagram. Conversely, the editor can parse a Coq goal stating equality between two composition of morphisms and generate a diagram out of it.

Date
Friday, March 18, 2022 15:00 Europe/Paris
Event
GReTA-ExACT working group
Zoom registration: click here! Please consider joining the meeting already within the 15min prior to the start of the seminar to ensure your setup is functioning properly. You may connect with either the Zoom web or Zoom desktop clients.

Please note that the meeting will be recorded and live-streamed to YouTube:

Ambroise Lafont
Ambroise Lafont
Postdoc

Since 2022, I am a postdoc in the TypeFoundry project in Cambridge. Previously, I was a postdoc in the Cogent team in Sydney. Before, I was a PhD student the Inria team Gallinette at LS2N in Nantes, supervised by Nicolas Tabareau and Tom Hirschowitz.
My research interests mainly lie in Type Theory and Category Theory: see my research and teaching statement.