Algebra and its Applications—Spring 2023
Earlier sessions are available here.
Please note that the schedule is still in flux.
Schedule
- Jan 12
- Organizational meeting
- Jan 19 & Jan 26
- Feb 2
- Feb 9
- Feb 16
- Reese Madsen
- Feb 23
- Brandon Story
- Mar 2
- Brandon Story
- Mar 9
- Matthew Winters
- Mar 16 No meeting (Spring Break)
- Mar 23
- Matthew Winters
- Mar 30
- Apr 6
- Apr 13
- Cindy Lester
- Apr 20
- Cindy Lester
- Apr 27
Talks
Ettore Aldrovandi
Title: Computer based formalization of Group Theory and Categorical Algebra in Homotopy Type Theory.
Abstract: I describe some work in progress in collaboration with Keri D’angelo (Cornell — CS) to formalize crossed modules of groups, hence groups, in Homotopy Type Theory using the Agda proof assistant. No previous knowledge of Type Theory or Agda is required, and I will sketch the main concepts: types, univalence and h-level. I will also illustrate how to pass to higher h-levels beyond sets, thus enabling one to do “categorical algebra without categories.”